Whitening Preserves Low-Moment Convergence

This statement constructs affine whitening maps that preserve convergence of moments through degree four.

Let $E$ be a finite-dimensional real inner-product space with its Borel measurable structure. Let $(λ_k)$ and $μ$ be probability measures on $E$, and assume Isotropic μ. Fix $R\in\mathbb R$. Suppose:

1. every $λ_k$ and $μ$ give measure zero to the complement of the closed ball $\overline B(0,R)$;
2. for every $d\le4$ and every $v:\operatorname{Fin}(d)\to E$, the mixed moments of $λ_k$ converge to those of $μ$.

Then there exist continuous linear equivalences $L_k:E\simeq_L E$ and centers $c_k\in E$ such that, for all sufficiently large $k$,

$$\int L_k(x-c_k)\,dλ_k(x)=0,$$

and, for every $u,v\in E$,

$$\int \langle u,L_k(x-c_k)\rangle\langle v,L_k(x-c_k)\rangle\,dλ_k(x)=\langle u,v\rangle.$$

Moreover, the mixed moments of the transformed laws through degree four converge to the corresponding moments of $μ$. This is the affine whitening step in the regular approximation.

Original Lean declaration header

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

theorem exists_whitening_tendsto_moments [MeasurableSpace E] [BorelSpace E] {lam : ℕ → ProbabilityMeasure E}
    {μ : ProbabilityMeasure E} (hiso : Isotropic μ) {R : ℝ}
    (hsupp : ∀ k, (lam k : Measure E) (closedBall (0 : E) R)ᶜ = 0)
    (hμsupp : (μ : Measure E) (closedBall (0 : E) R)ᶜ = 0)
    (hmom : ∀ d : ℕ, d ≤ 4 → ∀ v : Fin d → E,
      Tendsto (fun k => ∫ x, ∏ i, ⟪v i, x⟫ ∂(lam k : Measure E)) atTop
        (𝓝 (∫ x, ∏ i, ⟪v i, x⟫ ∂(μ : Measure E)))) :
    ∃ (L : ℕ → E ≃L[ℝ] E) (c : ℕ → E),
      (∀ᶠ k in atTop, ∫ x, L k (x - c k) ∂(lam k : Measure E) = 0 ∧
        ∀ u v : E, ∫ x, ⟪u, L k (x - c k)⟫ * ⟪v, L k (x - c k)⟫ ∂(lam k : Measure E) = ⟪u, v⟫) ∧
      ∀ d : ℕ, d ≤ 4 → ∀ v : Fin d → E,
        Tendsto (fun k => ∫ x, ∏ i, ⟪v i, L k (x - c k)⟫ ∂(lam k : Measure E)) atTop
          (𝓝 (∫ x, ∏ i, ⟪v i, x⟫ ∂(μ : Measure E)))

Module navigation

Module: KLS/LogConcave/BallConditioning.

Definition modules: KLS/Isotropic.

Supporting theorems: covariance_tendsto_one, whitening_sequence.

Previous: whitening_sequence.

Source excerpt, lines 461–473 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_BallConditioning

open MeasureTheory Set Metric Filter
open scoped Topology RealInnerProductSpace MatrixOrder Matrix.Norms.L2Operator
variable {E : Type*}
variable [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]

theorem FunctionalInequalities.KLS.exists_whitening_tendsto_moments_readable [MeasurableSpace E] [BorelSpace E] {lam : ℕ → ProbabilityMeasure E}
    {μ : ProbabilityMeasure E} (hiso : Isotropic μ) {R : ℝ}
    (hsupp : ∀ k, (lam k : Measure E) (closedBall (0 : E) R)ᶜ = 0)
    (hμsupp : (μ : Measure E) (closedBall (0 : E) R)ᶜ = 0)
    (hmom : ∀ d : ℕ, d ≤ 4 → ∀ v : Fin d → E,
      Tendsto (fun k => ∫ x, ∏ i, ⟪v i, x⟫ ∂(lam k : Measure E)) atTop
        (𝓝 (∫ x, ∏ i, ⟪v i, x⟫ ∂(μ : Measure E)))) :
    ∃ (L : ℕ → E ≃L[ℝ] E) (c : ℕ → E),
      (∀ᶠ k in atTop, ∫ x, L k (x - c k) ∂(lam k : Measure E) = 0 ∧
        ∀ u v : E, ∫ x, ⟪u, L k (x - c k)⟫ * ⟪v, L k (x - c k)⟫ ∂(lam k : Measure E) = ⟪u, v⟫) ∧
      ∀ d : ℕ, d ≤ 4 → ∀ v : Fin d → E,
        Tendsto (fun k => ∫ x, ∏ i, ⟪v i, L k (x - c k)⟫ ∂(lam k : Measure E)) atTop
          (𝓝 (∫ x, ∏ i, ⟪v i, x⟫ ∂(μ : Measure E))) := by sorry