Moment Generating Function of the Laplace Measure

Proved

FunctionalInequalities.Probability.Line.laplaceMeasure_mgf_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This lemma states the moment generating function of the Laplace measure within the indicated parameter range.

Let $\beta,w\in\mathbb R$ satisfy $\beta>0$ and $|w|<\beta$ . Let $\eta_\beta=$ laplaceMeasure $\beta$ , the measure on $\mathbb R$ with Lebesgue density $(\beta/2)e^{-\beta|s|}$ . Then

s\mapsto e^{ws}\in L^1(\eta_\beta),\qquad M_{\eta_\beta}(w)=\frac{\beta^2}{\beta^2-w^2},

where $M_{\eta_\beta}(w)=\int e^{ws}\,d\eta_\beta(s)$ is ProbabilityTheory.mgf applied to the identity random variable.

This gives a law-level exponential-integrability and transform formula, restricted to $|w|<\beta$ .

Original Lean declaration header

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

theorem laplaceMeasure_mgf {β w : ℝ} (hβ : 0 < β) (hw : |w| < β) :
    Integrable (fun s : ℝ => Real.exp (w * s)) (laplaceMeasure β) ∧
      mgf id (laplaceMeasure β) w = β ^ 2 / (β ^ 2 - w ^ 2)

Module navigation

Module: Probability/Line/Laplace.

Supporting theorems: integral_exp_mul_laplaceDensity.

Previous: integral_exp_mul_laplaceDensity.

Source excerpt, lines 237–239 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Line_Laplace

open MeasureTheory
open ProbabilityTheory Filter Set

Formal statement


theorem FunctionalInequalities.Probability.Line.laplaceMeasure_mgf_readable {β w : ℝ} (hβ : 0 < β) (hw : |w| < β) :
    Integrable (fun s : ℝ => Real.exp (w * s)) (laplaceMeasure β) ∧
      mgf id (laplaceMeasure β) w = β ^ 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#L236-L256 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.Line.Laplace`, declaration `FunctionalInequalities.Probability.Line.laplaceMeasure_mgf`; the repository is private at upload time).

View graph