Exponential-Norm Integrability Under a Compact Prior

Proved

FunctionalInequalities.Probability.Posterior.integrable_exp_norm_mul_of_compact_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement formalizes an integrability estimate for compactly supported posterior weights.

Let $E$ be a finite-dimensional real inner-product space and let $\mu$ be a probability measure on $E$ whose measure-theoretic support is compact. Let $f:E\to\mathbb R$ be measurable. Let $C\in\mathbb R$ satisfy $0\leq C$ , and assume

\|f(x)\|\leq C

for every $x$ in the support of $\mu$ . For any continuous linear map $Q:E\to E$ and any $s\in\mathbb R$ , the function

x\mapsto e^{s\|x\|}\left\|e^{E_{0,Q}(x)}f(x)\right\|

is integrable with respect to $\mu$ , where quadraticExponent 0 Q x is $E_{0,Q}(x)$ :

\int e^{s\|x\|}\left\|e^{E_{0,Q}(x)}f(x)\right\|\,d\mu(x)<\infty.

This compact-support estimate supplies the domination needed for smooth parameter differentiation of posterior integrals.

Original Lean declaration header

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

theorem integrable_exp_norm_mul_of_compact (μ : ProbabilityMeasure E)
    (hc : IsCompact (μ : Measure E).support) {f : E → ℝ} (hf : Measurable f)
    {C : ℝ} (_hC : 0 ≤ C) (hfb : ∀ x ∈ (μ : Measure E).support, ‖f x‖ ≤ C)
    (Q : E →L[ℝ] E) (s : ℝ) :
    Integrable (fun x => Real.exp (s * ‖x‖) * ‖Real.exp (quadraticExponent 0 Q x) * f x‖) (μ : Measure E)

Module navigation

Module: Probability/Posterior/Generator.

Definition modules: Probability/Posterior/Exponent.

Next: contDiff_weighted_integral_quadraticExponent_of_compact.

Source excerpt, lines 34–38 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Posterior_Generator

open MeasureTheory Filter Topology ProbabilityTheory
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]

Formal statement


theorem FunctionalInequalities.Probability.Posterior.integrable_exp_norm_mul_of_compact_readable (μ : ProbabilityMeasure E)
    (hc : IsCompact (μ : Measure E).support) {f : E → ℝ} (hf : Measurable f)
    {C : ℝ} (_hC : 0 ≤ C) (hfb : ∀ x ∈ (μ : Measure E).support, ‖f x‖ ≤ C)
    (Q : E →L[ℝ] E) (s : ℝ) :
    Integrable (fun x => Real.exp (s * ‖x‖) * ‖Real.exp (quadraticExponent 0 Q x) * f x‖) (μ : Measure E) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/Posterior/Generator.lean#L33-L58 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.Posterior.Generator`, declaration `FunctionalInequalities.Probability.Posterior.integrable_exp_norm_mul_of_compact`; the repository is private at upload time).

View graph