Posterior Mean Radius Bound

Proved

FunctionalInequalities.KLS.BKL.Localization.norm_posteriorMean_le_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This statement bounds the norm of the posterior mean by the radius of a ball containing the prior support.

Let $\mu$ be a probability law on $\operatorname{EuclideanSpace}(\mathbb{R},\operatorname{Fin}n)$ . Let $r\ge0$ and assume

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

For every posterior parameter $p=(c,Q)$ , the posterior mean satisfies

\left\|a(\mu;c,Q)\right\|\le r,

where $a(\mu;c,Q)$ is posteriorMean. The estimate is an a-priori geometric bound used in posterior energy arguments.

Original Lean declaration header

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

theorem norm_posteriorMean_le {r : ℝ} (hr : 0 ≤ r)
    (hsupp : (μ : Measure (EuclideanSpace ℝ (Fin n))).support ⊆ Metric.closedBall 0 r) (p : Param n) :
    ‖posteriorMean μ p.1 p.2‖ ≤ r

Module navigation

Module: KLS/BKL/Localization/Energy/Bound.

Definition modules: Probability/Posterior/Generator, KLS/BKL/Localization/Coefficients.

Previous: posterior_energy_transfer · Next: exists_cumulantEnergy_le.

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

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_Energy_Bound

open MeasureTheory
open FunctionalInequalities.Probability.Posterior FunctionalInequalities.Analysis
variable {n : ℕ}
variable (μ : MeasureTheory.ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
  (hc : IsCompact (μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin n))).support)

Formal statement


theorem FunctionalInequalities.KLS.BKL.Localization.norm_posteriorMean_le_readable {r : ℝ} (hr : 0 ≤ r)
    (hsupp : (μ : Measure (EuclideanSpace ℝ (Fin n))).support ⊆ Metric.closedBall 0 r) (p : Param n) :
    ‖posteriorMean μ p.1 p.2‖ ≤ r := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/Localization/Energy/Bound.lean#L172-L190 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.Localization.Energy.Bound`, declaration `FunctionalInequalities.KLS.BKL.Localization.norm_posteriorMean_le`; the repository is private at upload time).

View graph