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 real-variable integration and the Dirichlet integral. As an application, we formalize the Laplace-domain solution of the harmonic oscillator and identify its transform with that of $\sin(ωt)$. We also discuss the principal analytic and formalization challenges encountered in the development.

翻译：暂无翻译