From the Dirichlet Integral to Lobachevsky's Formula: A Formalization in Lean 4
Daniel Goldberg, Antoine Vinciguerra
cs.LO
Aug 7, 2026 · v1
TL;DR
Formalizes the Dirichlet integral, the sinc-to-Heaviside cutoff, and Lobachevsky's integral 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 conditionally convergent and its sinc function is not Lebesgue integrable on the positive half-line, complicating formalization. Classical evaluation methods hide uniform tail estimates that are hard to formalize directly.
Approach
The Dirichlet integral is represented as a limit of integrals over bounded intervals rather than a Lebesgue integral. Instead of the Feynman exponential-factor argument, the proof passes through the absolutely integrable sinc-squared function, evaluated via differentiation under the integral sign and dominated convergence. An identity between truncated integrals transfers the value back to the Dirichlet integral. Lobachevsky's formula is obtained using density of cosine polynomials from Mathlib's Fourier analysis on AddCircle.
Results
Formalizes the Dirichlet integral value pi/2, convergence of the Dirichlet cutoff to the Heaviside function, several quadratic and bilinear trigonometric integral identities, and Lobachevsky's integral formula for continuous periodic functions with reflection symmetry.
