Papers With

← All papers
First page of From the Dirichlet Integral to Lobachevsky's Formula: A Formalization in Lean 4

From the Dirichlet Integral to Lobachevsky's Formula: A Formalization in Lean 4

Daniel Goldberg, Antoine Vinciguerra

cs.LO Aug 7, 2026 · v3
formalization mathlib analysis
Read PDF arXiv abstract Code
TL;DR
Formalizes the Dirichlet integral, the Dirichlet cutoff, trigonometric integral identities, and Lobachevsky's formula in Lean 4, using Mathlib's Fourier analysis.
Abstract
We formalize the Dirichlet integral and several of its classical applications in the Lean 4 proof assistant. Since the sinc function is not Lebesgue integrable on the positive half-line, the Dirichlet integral must be represented as the limit of integrals over bounded intervals. To avoid the difficulty of removing an exponential factor from a conditionally convergent integral, we instead pass through the absolutely integrable function \(\operatorname{sinc}^2\). We evaluate its integral by differentiation under the integral sign and dominated convergence, and then recover the Dirichlet integral from an identity between truncated integrals. Using these results, we formalize the convergence of the Dirichlet cutoff to the Heaviside function and derive several quadratic and bilinear trigonometric integral identities. Finally, we formalize Lobachevsky's integral formula for continuous periodic functions satisfying a reflection symmetry, using the density of cosine polynomials obtained from Mathlib's Fourier analysis on the additive circle.
Problem

The Dirichlet integral of sinc is only conditionally convergent, so it cannot be stated as a Lebesgue integral. The classical Feynman-style proof also hides a uniform tail estimate that is hard to formalize. The goal is to formalize the Dirichlet integral and its classical applications in Lean 4.

Approach

The Dirichlet integral is stated as a limit of integrals over bounded intervals. The authors avoid the Feynman exponential-factor argument and instead evaluate the absolutely integrable sinc^2 integral, using differentiation under the integral sign and dominated convergence. An identity between truncated integrals of sinc and sinc^2 then transfers the value to the Dirichlet integral. Lobachevsky's formula is proved for cosine modes first, then extended by uniform approximation via density of cosine polynomials, obtained from Mathlib's Fourier analysis on AddCircle π.

Results

Formalized results include the Dirichlet integral and convergence of the rescaled Dirichlet cutoff to the Heaviside function, with continuity and boundedness of the cutoff. Several quadratic and bilinear trigonometric integral identities are also formalized, along with Lobachevsky's integral formula for continuous π-periodic functions with reflection symmetry.