Smoothness of Posterior Expectation in the Linear Parameter

Proved

FunctionalInequalities.Probability.Posterior.contDiff_posteriorExpectation_c_readable

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

bkl2026functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement formalizes smoothness in the linear parameter for the compact posterior and is partially related to Equation (67), p. 19, of Bizeul–Klartag–Lehec (arXiv:2610.05474v1).

Let $E$ be a finite-dimensional real inner-product space and let $\mu$ be a compactly supported probability measure. Let $f:E\to\mathbb R$ be measurable, let $C\in\mathbb R$ satisfy $0\leq C$ , and assume $\|f(x)\|\leq C$ on the support of $\mu$ . Fix a continuous linear map $Q:E\to E$ .

Then the posterior expectation posteriorExpectation μ c Q f is infinitely continuously differentiable as a function of $c\in E$ :

\operatorname{ContDiff}_{\mathbb R}^{\infty} \left(c\mapsto \operatorname{posteriorExpectation}(\mu,c,Q,f)\right).

The assertion includes $Q=0$ and does not require symmetry of $Q$ . It concerns only the $c$ variable, with $Q$ fixed.

Original Lean declaration header

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

theorem contDiff_posteriorExpectation_c (μ : 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) :
    ContDiff ℝ ∞ (fun c => posteriorExpectation μ c Q f)

Module navigation

Module: Probability/Posterior/Generator.

Supporting theorems: contDiff_weighted_integral_quadraticExponent_of_compact.

Previous: contDiff_weighted_integral_quadraticExponent_of_compact · Next: fderiv_posteriorExpectation_c_apply.

Source excerpt, lines 92–95 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Posterior_Generator

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

Formal statement


theorem FunctionalInequalities.Probability.Posterior.contDiff_posteriorExpectation_c_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) :
    ContDiff ℝ ∞ (fun c => posteriorExpectation μ c Q f) := 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/Generator.lean#L91-L110 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.Posterior.Generator`, declaration `FunctionalInequalities.Probability.Posterior.contDiff_posteriorExpectation_c`; the repository is private at upload time).

View graph