First Variation of a Compact Tilted Expectation

Proved

FunctionalInequalities.Probability.Posterior.expectation_hasDerivAt_of_compact_readable

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

bkl2026functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes the compact-prior first-variation statement related to Equation (67) of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), Equation (67), p. 19.

Let $\mu$ be a probability measure on a topological, measurable, second-countable Borel space with compact support. Let $\phi,g$ be continuous and let $f$ be measurable. Assume that for some $C\ge0$ , $\lVert f(x)\rVert\le C$ on $\operatorname{supp}\mu$ . For the tilted probability measure with exponent $\phi+t g$ , the expectation satisfies

\left.\frac{d}{dt}\right|_{t=0}\int f\,d\bigl(\mu.\operatorname{tilted}(\phi+t g)\bigr) =\operatorname{Cov}_{\mu.\operatorname{tilted}(\phi)}(f,g).

The notation Measure.tilted denotes the normalized exponential tilt. This lemma is the basic first-variation formula for compact posterior measures.

Original Lean declaration header

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

theorem expectation_hasDerivAt_of_compact (μ : ProbabilityMeasure Ω)
    (hc : IsCompact (μ : Measure Ω).support) {φ g f : Ω → ℝ}
    (hφ : Continuous φ) (hg : Continuous g) (hf : Measurable f) {C : ℝ} (hC : 0 ≤ C)
    (hfb : ∀ x ∈ (μ : Measure Ω).support, ‖f x‖ ≤ C) :
    HasDerivAt (fun t : ℝ => ∫ x, f x ∂((μ : Measure Ω).tilted (fun x => φ x + t * g x)))
      (covariance f g ((μ : Measure Ω).tilted φ)) 0

Module navigation

Module: Probability/Posterior/CompactPrior.

Supporting theorems: hasDerivAt_weighted_integral_of_compact.

Previous: hasDerivAt_weighted_integral_of_compact · Next: norm_integral_tilted_le_of_compact.

Source excerpt, lines 134–139 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Posterior_CompactPrior

open MeasureTheory Filter Topology ProbabilityTheory
variable {Ω : Type*} [TopologicalSpace Ω] [MeasurableSpace Ω] [BorelSpace Ω]
  [SecondCountableTopology Ω]

Formal statement


theorem FunctionalInequalities.Probability.Posterior.expectation_hasDerivAt_of_compact_readable (μ : ProbabilityMeasure Ω)
    (hc : IsCompact (μ : Measure Ω).support) {φ g f : Ω → ℝ}
    (hφ : Continuous φ) (hg : Continuous g) (hf : Measurable f) {C : ℝ} (hC : 0 ≤ C)
    (hfb : ∀ x ∈ (μ : Measure Ω).support, ‖f x‖ ≤ C) :
    HasDerivAt (fun t : ℝ => ∫ x, f x ∂((μ : Measure Ω).tilted (fun x => φ x + t * g x)))
      (covariance f g ((μ : Measure Ω).tilted φ)) 0 := by sorry

Source

Source: Bizeul–Klartag–Lehec, Presenting a proof of the Kannan–Lovász–Simonovits conjecture (arXiv:2610.05474v1), Equation (67), p. 19 (unnumbered display) and the compact stage before it. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/Posterior/CompactPrior.lean#L131-L171 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.Posterior.CompactPrior`, declaration `FunctionalInequalities.Probability.Posterior.expectation_hasDerivAt_of_compact`; the repository is private at upload time).

View graph