Isotropic Standardization of a Compact Posterior

This is a canonical standardization statement related to the posterior in Equation (67) of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), Equation (67), p. 19.

Let $E$ be a finite-dimensional real inner-product space with Borel measurable structure. Let $\mu$ be an isotropic probability measure with compact support, let $c\in E$, and let $Q:E\to E$ be continuous linear. Then there exists a continuous linear equivalence $W:E\simeq_L E$ such that

and the pushforward by $W$ of the posterior centered at its mean is isotropic:

The posterior is compactPosterior μ hc c Q, and the covariance operator is Covariance.operator. The conclusion is existential and applies only under the compact-support and finite-dimensional hypotheses shown.

Original Lean declaration header

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

theorem Isotropic.exists_inverseSqrt_equiv_isotropic_standardized (μ : ProbabilityMeasure E)
    (hc : IsCompact (μ : Measure E).support) (hiso : KLS.Isotropic μ) (c : E) (Q : E →L[ℝ] E) :
    ∃ W : E ≃L[ℝ] E,
      (W : E →L[ℝ] E) = inverseSqrt (Covariance.operator (compactPosterior μ hc c Q : Measure E)) ∧
      KLS.Isotropic (Probability.mapContinuousLinearEquiv
        (Probability.translateLaw (compactPosterior μ hc c Q) (-posteriorMean μ c Q)) W)

Module navigation

Module: KLS/BKL/Posterior/Standardization.

Definition modules: Probability/Posterior/Generator, Probability/Covariance/Basic, KLS/Isotropic, Analysis/Operator/InverseSqrt, Probability/Transport, Probability/Posterior/CompactDomain.

Supporting theorems: inverseSqrt_mul_mul_inverseSqrt, Covariance.inner_operator_self_pos_of_affineSupport_eq_top, Covariance.operator_map_continuousLinearEquiv.

Source excerpt, lines 34–39 · Frozen source 408915f.