2 papers
cs.LO2026
From the Dirichlet Integral to Lobachevsky's Formula: A Formalization in Lean 4
Daniel Goldberg, Antoine Vinciguerra
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…
cs.LO2026
A Formalization of the Laplace Transform and Its Inversion in Lean 4
Daniel Goldberg, Antoine Vinciguerra
We present a Lean 4 formalization of the Laplace transform for complex-valued functions, its fundamental operational rules, and a Bromwich-type inversion theorem proved through rea…