Posterior Covariance Operator Radius Bound

Proved

FunctionalInequalities.KLS.opNorm_covariance_compactPosterior_le_sq_radius_readable

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

bkl2026functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes a covariance-radius estimate related to the compact posterior stage before Equation (67) of Bizeul–Klartag–Lehec (arXiv:2610.05474v1).

Let $E$ be a finite-dimensional real inner-product space, let $\mu$ be a probability law with compact support, and let $r\ge0$ . Assume

\operatorname{supp}(\mu)\subseteq\overline{B}(0,r).

For arbitrary $c\in E$ and continuous linear $Q:E\to E$ , let $\mu_{c,Q}$ be the compact posterior. Then the operator norm of its covariance operator satisfies

\left\|\operatorname{Cov}(\mu_{c,Q})\right\|\le r^2.

The estimate bounds posterior covariance uniformly in the finite parameters $c$ and $Q$ whenever the prior is supported in a ball of radius $r$ .

Original Lean declaration header

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

theorem opNorm_covariance_compactPosterior_le_sq_radius (μ : ProbabilityMeasure E)
    (hc : IsCompact (μ : Measure E).support) {r : ℝ} (hr : 0 ≤ r)
    (hsupp : (μ : Measure E).support ⊆ Metric.closedBall (0 : E) r) (c : E) (Q : E →L[ℝ] E) :
    ‖Covariance.operator (compactPosterior μ hc c Q : Measure E)‖ ≤ r ^ 2

Module navigation

Module: KLS/BKL/Posterior/Covariance.

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

Supporting theorems: covariance_sq_le_variance_mul_variance.

Source excerpt, lines 173–176 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Posterior_Covariance

open MeasureTheory
open FunctionalInequalities.Probability.Posterior FunctionalInequalities.Analysis
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]

Formal statement


theorem FunctionalInequalities.KLS.opNorm_covariance_compactPosterior_le_sq_radius_readable (μ : ProbabilityMeasure E)
    (hc : IsCompact (μ : Measure E).support) {r : ℝ} (hr : 0 ≤ r)
    (hsupp : (μ : Measure E).support ⊆ Metric.closedBall (0 : E) r) (c : E) (Q : E →L[ℝ] E) :
    ‖Covariance.operator (compactPosterior μ hc c Q : Measure E)‖ ≤ r ^ 2 := 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/KLS/BKL/Posterior/Covariance.lean#L170-L282 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.Posterior.Covariance`, declaration `FunctionalInequalities.KLS.opNorm_covariance_compactPosterior_le_sq_radius`; the repository is private at upload time).

View graph