Joint Smoothness of the Posterior Covariance Operator

Proved

FunctionalInequalities.Probability.Posterior.contDiff_posteriorCovariance_joint_readable

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

bkl2026functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement formalizes joint smoothness of the posterior covariance operator.

Let $E$ be a finite-dimensional real inner-product space and let $\mu$ be a probability measure with compact support. For each parameter pair $(c,Q)\in E\times(E\to_L E)$ , let compactPosterior μ hc c Q be the corresponding compact posterior and let Covariance.operator denote its covariance operator.

The operator-valued map

(c,Q)\longmapsto \operatorname{Covariance.operator}(\mu_{c,Q})

is infinitely continuously differentiable in the operator norm:

\operatorname{ContDiff}_{\mathbb R}^{\infty} \left((c,Q)\mapsto\operatorname{Covariance.operator}(\mu_{c,Q})\right).

No isotropy or symmetry assumption on $Q$ is present. The result is a finite-dimensional coordinate reconstruction of the joint covariance regularity.

Original Lean declaration header

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

theorem contDiff_posteriorCovariance_joint (μ : ProbabilityMeasure E)
    (hc : IsCompact (μ : Measure E).support) :
    ContDiff ℝ ∞ (fun p : E × (E →L[ℝ] E) =>
      Covariance.operator (compactPosterior μ hc p.1 p.2 : Measure E))

Module navigation

Module: Probability/Posterior/JointRegularity.

Definition modules: Probability/Covariance/Basic, Probability/Posterior/CompactDomain.

Supporting theorems: contDiff_covariance_pair_joint.

Previous: contDiff_covariance_pair_joint.

Source excerpt, lines 298–301 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Posterior_JointRegularity

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

Formal statement


theorem FunctionalInequalities.Probability.Posterior.contDiff_posteriorCovariance_joint_readable (μ : ProbabilityMeasure E)
    (hc : IsCompact (μ : Measure E).support) :
    ContDiff ℝ ∞ (fun p : E × (E →L[ℝ] E) =>
      Covariance.operator (compactPosterior μ hc p.1 p.2 : Measure E)) := 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/JointRegularity.lean#L296-L325 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.Posterior.JointRegularity`, declaration `FunctionalInequalities.Probability.Posterior.contDiff_posteriorCovariance_joint`; the repository is private at upload time).

View graph