Standardization by Covariance Whitening

This is the standardization construction for compactly supported log-concave laws.

Let $E$ be a complete finite-dimensional real inner-product space with its Borel measurable structure, and let $\mu$ be a probability measure on $E$. Assume: (1) $\mu$ is log-concave; (2) its support is compact; (3) its covariance operator $A=\operatorname{Cov}(\mu)$ is positive; and (4) $A$ is a unit, hence invertible.

Then there exist a probability measure $\eta$ and a continuous linear equivalence $W:E\simeq E$ such that

and

The declaration packages centering and covariance whitening into an isotropic compactly supported law. It is a reduction tool and asserts existence, not uniqueness.

Original Lean declaration header

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

theorem exists_standardized [CompleteSpace E] [FiniteDimensional ℝ E]
    [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
    (μ : ProbabilityMeasure E) (hLC : LogConcave μ)
    (hc : IsCompact (μ : Measure E).support)
    (hpos : (Covariance.operator (μ : Measure E)).IsPositive)
    (hunit : IsUnit (Covariance.operator (μ : Measure E))) :
    ∃ (η : ProbabilityMeasure E) (W : E ≃L[ℝ] E),
      (W : E →L[ℝ] E) = inverseSqrt (Covariance.operator (μ : Measure E)) ∧
      KLS.Isotropic η ∧ LogConcave η ∧ IsCompact (η : Measure E).support ∧
      (η : Measure E) = (μ : Measure E).map (fun x => W (x - ∫ y, y ∂(μ : Measure E)))

Module navigation

Module: KLS/BKL/CompactReduction.

Definition modules: Probability/Covariance/Basic, Probability/LogConcave, KLS/Isotropic, Analysis/Operator/InverseSqrt.

Supporting theorems: inverseSqrt_mul_mul_inverseSqrt, Covariance.operator_map_continuousLinearEquiv, memLp_id_two, of_continuousLinearEquiv_map.

Previous: inner_self_pos_of_norm_sub_one_lt · Next: cumulantBound_of_compact.

Source excerpt, lines 239–248 · Frozen source 408915f.