Gaussian Law Laplace Transform

Proved

FunctionalInequalities.KLS.LogConcave.GaussianSmoothing.gaussianLaw_laplace_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is the Laplace-transform formula for the Gaussian law gaussianLaw.

Let $E$ be a finite-dimensional real inner-product space with Borel measurable structure, let $s>0$ , and let $z\in E$ . Then

\int_E e^{\langle z,y\rangle}\,d\gamma_s(y) =\exp\left(\frac{\|z\|^2}{4s}\right),

where $\gamma_s=\texttt{gaussianLaw }s$ . Completeness of $E$ is not required by the declaration. The formula identifies the normalization used for the Gaussian smoothing and supports the subsequent moment identities.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.LogConcave.GaussianSmoothing. Shown in its original module context. Proof omitted.

theorem gaussianLaw_laplace {s : ℝ} (hs : 0 < s) (z : E) :
    (∫ y, Real.exp ⟪z, y⟫ ∂(gaussianLaw (V := E) s)) = Real.exp (‖z‖ ^ 2 / (4 * s))

Module navigation

Module: KLS/LogConcave/Density/GaussianSmoothing/Moments.

Definition modules: KLS/LogConcave/Density/GaussianSmoothing/Basic.

Previous: gaussianLaw_exp_norm_integrable · Next: gaussianLaw_mean_zero.

Source excerpt, lines 79–80 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Density_GaussianSmoothing_Moments

open scoped RealInnerProductSpace ContDiff
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
omit [CompleteSpace E]

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.GaussianSmoothing.gaussianLaw_laplace_readable {s : ℝ} (hs : 0 < s) (z : E) :
    (∫ y, Real.exp ⟪z, y⟫ ∂(gaussianLaw (V := E) s)) = Real.exp (‖z‖ ^ 2 / (4 * s)) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/Density/GaussianSmoothing/Moments.lean#L77-L105 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.Density.GaussianSmoothing.Moments`, declaration `FunctionalInequalities.KLS.LogConcave.GaussianSmoothing.gaussianLaw_laplace`; the repository is private at upload time).

View graph