Exponential Integral Against the Laplace Density

Proved

FunctionalInequalities.Probability.Line.integral_exp_mul_laplaceDensity_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This lemma evaluates the exponentially weighted Laplace density on its stated local parameter range.

Let $\beta,w\in\mathbb R$ satisfy $\beta>0$ and $|w|<\beta$ . Define $\rho_\beta(s)=(\beta/2)e^{-\beta|s|}$ , the function laplaceDensity $\beta$ . With Lebesgue measure $ds$ on $\mathbb R$ ,

s\mapsto e^{ws}\rho_\beta(s)\in L^1(ds),\qquad \int_{\mathbb R}e^{ws}\rho_\beta(s)\,ds=\frac{\beta^2}{\beta^2-w^2}.

The statement supplies the density-level integrability and integral needed for the Laplace moment generating function. It makes no assertion for $|w|\ge\beta$ .

Original Lean declaration header

Within namespace FunctionalInequalities.Probability.Line. Shown in its original module context. Proof omitted.

theorem integral_exp_mul_laplaceDensity {β w : ℝ} (hβ : 0 < β) (hw : |w| < β) :
    MeasureTheory.Integrable (fun s => Real.exp (w * s) * laplaceDensity β s) ∧
      ∫ s, Real.exp (w * s) * laplaceDensity β s = β ^ 2 / (β ^ 2 - w ^ 2)

Module navigation

Module: Probability/Line/Laplace.

Next: laplaceMeasure_mgf.

Source excerpt, lines 106–108 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Line_Laplace

Formal statement


theorem FunctionalInequalities.Probability.Line.integral_exp_mul_laplaceDensity_readable {β w : ℝ} (hβ : 0 < β) (hw : |w| < β) :
    MeasureTheory.Integrable (fun s => Real.exp (w * s) * laplaceDensity β s) ∧
      ∫ s, Real.exp (w * s) * laplaceDensity β s = β ^ 2 / (β ^ 2 - w ^ 2) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/Line/Laplace.lean#L104-L234 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.Line.Laplace`, declaration `FunctionalInequalities.Probability.Line.integral_exp_mul_laplaceDensity`; the repository is private at upload time).

View graph