Skip to content
DraconiticResearch
Search Sources API
194,161 studies31 sourcesUpdated 43 min ago
PreprintCC BY 4.0HAL

A Formalization of the Laplace Transform and Its Inversion in Lean 4

  • Daniel Goldberg
  • Antoine Vinciguerra
Open at sourcePDFCite

Abstract

We present a Lean 4 formalization of the Laplace transform for complex-valued functions, its fundamental operational rules, and a Bromwich-type inversion theorem. Because the contour-integration and residue-theorem infrastructure required by the classical proof is not yet available in mathlib to the required extent, the inversion argument is carried out through real-variable integration. Its decisive ingredient is a formalization of the Dirichlet integral. As an application, we formalize the Laplacetransform calculation for the harmonic oscillator. The same Dirichlet development yields as a further consequence Lobachevsky's integral formula. We also discuss the principal formalization challenges.

Related

  1. Global Regularity for the 3D Incompressible Navier–Stokes Equations via the Frohmanian Symplectic Tether: Lean 4 Formalization and Conditional Cubic Comparison Framework (v2.1)
    Benjamin Frohman
    Zenodo (CERN European Organization for Nuclear Research)PreprintLicence not stated6 citedGeneral mathematicsOpenAlex
  2. Formalization of Landau damping in the Vlasov--Poisson equations in Lean
    Jacob Bedrossian
    arXivPreprintarXiv licenceFull textAnalysis & PDEsarXiv
  3. A Lean Formalization of the Hamilton--Perelman Proof of the Three-Dimensional Poincaré Conjecture
    Ziyang Qin, Yuan Liao, Ayush Khaitan +1
    arXivPreprintCC BY 4.0Full textGeometry & topologyarXiv
  4. A Lean Formalization of the Hamilton--Perelman Proof of Thurston's Geometrization Conjecture
    Yuan Liao, Ziyang Qin, Jui-Hui Chung +7
    arXivPreprintCC BY 4.0Full textGeometry & topologyarXiv
  5. Formalization of Sullivan's No Wandering Domains Theorem in Lean
    Ziang Li, Yusheng Luo
    arXivPreprintarXiv licenceFull textMathematical physicsarXiv

Cite

BibTeXRIS
BibTeX
@misc{goldberg2026formalization,
  title = {{A Formalization of the Laplace Transform and Its Inversion in Lean 4}},
  author = {Daniel Goldberg and Antoine Vinciguerra},
  howpublished = {HAL},
  year = {2026},
  month = sep,
  url = {https://hal.science/hal-05747629v1},
  note = {CC BY 4.0},
}
RIS
TY  - UNPB
TI  - A Formalization of the Laplace Transform and Its Inversion in Lean 4
AU  - Daniel Goldberg
AU  - Antoine Vinciguerra
PY  - 2026
DA  - 2026/09/12
PB  - HAL
UR  - https://hal.science/hal-05747629v1
AB  - We present a Lean 4 formalization of the Laplace transform for complex-valued functions, its fundamental operational rules, and a Bromwich-type inversion theorem. Because the contour-integration and residue-theorem infrastructure required by the classical proof is not yet available in mathlib to the required extent, the inversion argument is carried out through real-variable integration. Its decisive ingredient is a formalization of the Dirichlet integral. As an application, we formalize the Laplacetransform calculation for the harmonic oscillator. The same Dirichlet development yields as a further consequence Lobachevsky's integral formula. We also discuss the principal formalization challenges.
ER  -