2.3. Whitening and covariance normalization🔗

Theorem2.3.1

uses 0

Used by 3

Reverse dependency previews

Preview

Theorem 2.3.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagsbentkuswhiteningcovariancesource-bentkus-2004fidelity-exact-positive-square-root

Whitening a positive-definite covariance. Let S be a positive-definite real d\times d matrix, let R=S^{1/2} be its positive square root, and set T=R^{-1}=S^{-1/2}. Then TST=I_d. Equivalently, regarding these matrices as continuous linear maps, T\bigl(S(Tx)\bigr)=x\qquad(x\in\mathbb R^d).

Lean code for Theorem2.3.1●2 theorems

theoremdefined in ProbabilityApproximation/Bentkus/Whitening.lean

complete

theorem ProbabilityTheory.bentkusWhiteningMatrix_mul_self {d : ℕ}
  (S : Matrix (Fin d) (Fin d) ℝ) (hS : S.PosDef) :
  ProbabilityTheory.bentkusWhiteningMatrix S * S *
      ProbabilityTheory.bentkusWhiteningMatrix S =
    1

theorem ProbabilityTheory.bentkusWhiteningMatrix_mul_self
  {d : ℕ} (S : Matrix (Fin d) (Fin d) ℝ)
  (hS : S.PosDef) :
  ProbabilityTheory.bentkusWhiteningMatrix
          S *
        S *
      ProbabilityTheory.bentkusWhiteningMatrix
        S =
    1

Conjugating a positive-definite covariance matrix by its whitening matrix gives identity.

theoremdefined in ProbabilityApproximation/Bentkus/Whitening.lean

complete

theorem ProbabilityTheory.bentkusWhiteningCLM_covariance_comp (d : ℕ)
  (S : Matrix (Fin d) (Fin d) ℝ) (hS : S.PosDef)
  (x : EuclideanSpace ℝ (Fin d)) :
  (ProbabilityTheory.bentkusWhiteningCLM S)
      ((Matrix.toEuclideanCLM S)
        ((ProbabilityTheory.bentkusWhiteningCLM S) x)) =
    x

theorem ProbabilityTheory.bentkusWhiteningCLM_covariance_comp
  (d : ℕ) (S : Matrix (Fin d) (Fin d) ℝ)
  (hS : S.PosDef)
  (x : EuclideanSpace ℝ (Fin d)) :
  (ProbabilityTheory.bentkusWhiteningCLM
        S)
      ((Matrix.toEuclideanCLM S)
        ((ProbabilityTheory.bentkusWhiteningCLM
            S)
          x)) =
    x

The threefold operator composition `S⁻¹ᐟ² ∘ S ∘ S⁻¹ᐟ²` is the identity.

Bentkus (2004), defines the positive covariance square root C by C^2=\operatorname{Cov}(S_n) in the notation preceding Theorem 1.1, printed p. 400, and uses C^{-1} in the normalization following equation (3.1), printed p. 403. The formal statement makes the resulting C^{-1}C^2C^{-1}=I identity explicit.

Theorem2.3.2

uses 1used by 1✓L∃∀N

Tagsbentkuswhiteninggaussian-transportsource-bentkus-2004fidelity-exact-pushforward

Gaussian pushforward under whitening. Under the preceding hypotheses, let T=S^{-1/2} and let R=S^{1/2}. These maps are mutually inverse continuous linear equivalences, and their Gaussian pushforwards satisfy T_\#N(0,S)=N(0,I_d), \qquad R_\#N(0,I_d)=N(0,S).

Lean code for Theorem2.3.2●5 declarations

defdefined in ProbabilityApproximation/Bentkus/Whitening.lean

complete

def ProbabilityTheory.bentkusWhiteningMatrix {d : ℕ}
  (S : Matrix (Fin d) (Fin d) ℝ) : Matrix (Fin d) (Fin d) ℝ

def ProbabilityTheory.bentkusWhiteningMatrix
  {d : ℕ} (S : Matrix (Fin d) (Fin d) ℝ) :
  Matrix (Fin d) (Fin d) ℝ

The inverse positive square root used to whiten a positive-definite covariance matrix.

defdefined in ProbabilityApproximation/Bentkus/Whitening.lean

complete

def ProbabilityTheory.bentkusWhiteningCLM {d : ℕ}
  (S : Matrix (Fin d) (Fin d) ℝ) :
  EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d)

def ProbabilityTheory.bentkusWhiteningCLM
  {d : ℕ} (S : Matrix (Fin d) (Fin d) ℝ) :
  EuclideanSpace ℝ (Fin d) →L[ℝ]
    EuclideanSpace ℝ (Fin d)

The continuous linear whitening map associated to `S`.

defdefined in ProbabilityApproximation/Bentkus/Whitening.lean

complete

def ProbabilityTheory.bentkusWhiteningEquiv {d : ℕ}
  (S : Matrix (Fin d) (Fin d) ℝ) (hS : S.PosDef) :
  EuclideanSpace ℝ (Fin d) ≃L[ℝ] EuclideanSpace ℝ (Fin d)

def ProbabilityTheory.bentkusWhiteningEquiv
  {d : ℕ} (S : Matrix (Fin d) (Fin d) ℝ)
  (hS : S.PosDef) :
  EuclideanSpace ℝ (Fin d) ≃L[ℝ]
    EuclideanSpace ℝ (Fin d)

The whitening map bundled as a continuous linear equivalence.

theoremdefined in ProbabilityApproximation/Bentkus/Whitening.lean

complete

theorem ProbabilityTheory.map_multivariateGaussian_bentkusWhiteningEquiv {d : ℕ}
  (S : Matrix (Fin d) (Fin d) ℝ) (hS : S.PosDef) :
  MeasureTheory.Measure.map
      (⇑(ProbabilityTheory.bentkusWhiteningEquiv S hS))
      (ProbabilityTheory.multivariateGaussian 0 S) =
    ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d))

theorem ProbabilityTheory.map_multivariateGaussian_bentkusWhiteningEquiv
  {d : ℕ} (S : Matrix (Fin d) (Fin d) ℝ)
  (hS : S.PosDef) :
  MeasureTheory.Measure.map
      (⇑(ProbabilityTheory.bentkusWhiteningEquiv
          S hS))
      (ProbabilityTheory.multivariateGaussian
        0 S) =
    ProbabilityTheory.stdGaussian
      (EuclideanSpace ℝ (Fin d))

Whitening sends the centered Gaussian with covariance `S` to standard Gaussian measure.

theoremdefined in ProbabilityApproximation/Bentkus/Whitening.lean

complete

theorem ProbabilityTheory.map_stdGaussian_bentkusWhiteningEquiv_symm {d : ℕ}
  (S : Matrix (Fin d) (Fin d) ℝ) (hS : S.PosDef) :
  MeasureTheory.Measure.map
      (⇑(ProbabilityTheory.bentkusWhiteningEquiv S hS).symm)
      (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d))) =
    ProbabilityTheory.multivariateGaussian 0 S

theorem ProbabilityTheory.map_stdGaussian_bentkusWhiteningEquiv_symm
  {d : ℕ} (S : Matrix (Fin d) (Fin d) ℝ)
  (hS : S.PosDef) :
  MeasureTheory.Measure.map
      (⇑(ProbabilityTheory.bentkusWhiteningEquiv
            S hS).symm)
      (ProbabilityTheory.stdGaussian
        (EuclideanSpace ℝ (Fin d))) =
    ProbabilityTheory.multivariateGaussian
      0 S

Standard Gaussian transported back through the square root has covariance `S`.

This is the Gaussian part of the rescaling S_n\mapsto C^{-1}S_n and Z\mapsto C^{-1}Z immediately after equation (3.1) in Bentkus (2004), printed p. 403; the covariance-square-root notation is introduced before Theorem 1.1, printed p. 400.

Theorem2.3.3

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 2.3.4

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagsbentkuswhiteningstandardized-theoremsource-bentkus-2004fidelity-exact-contract

The identity-covariance theorem contract. Let X_1,\ldots,X_n be independent, centered L^3 random vectors, suppose that their sum W has positive-definite covariance S, and put \widehat X_i=S^{-1/2}X_i. Then \sum_i\widehat X_i=S^{-1/2}W, the family (\widehat X_i)_i remains independent and centered, and \operatorname{Cov}\!\left(\sum_i\widehat X_i\right)=I_d. For a fixed constant C, the identity-covariance contract asserts that every such normalized family and every measurable convex B\subseteq\mathbb R^d satisfy \left|\Pr\left(\sum_i\widehat X_i\in B\right)-\gamma_d(B)\right| \le C d^{1/4}\sum_i\mathbb E\|\widehat X_i\|^3. Here \gamma_d denotes standard Gaussian measure on \mathbb R^d.

Lean code for Theorem2.3.3●6 declarations

defdefined in ProbabilityApproximation/Bentkus/Whitening.lean

complete

def ProbabilityTheory.bentkusWhitenedSummand.{u_1} {n d : ℕ} {Ω : Type u_1}
  (S : Matrix (Fin d) (Fin d) ℝ)
  (X : Fin n → Ω → EuclideanSpace ℝ (Fin d)) (i : Fin n) (ω : Ω) :
  EuclideanSpace ℝ (Fin d)

def ProbabilityTheory.bentkusWhitenedSummand.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  (S : Matrix (Fin d) (Fin d) ℝ)
  (X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d))
  (i : Fin n) (ω : Ω) :
  EuclideanSpace ℝ (Fin d)

The transformed summand family used in the covariance-normalized Bentkus theorem.

theoremdefined in ProbabilityApproximation/Bentkus/Whitening.lean

complete

theorem ProbabilityTheory.sum_bentkusWhitenedSummand.{u_1} {n d : ℕ}
  {Ω : Type u_1} (S : Matrix (Fin d) (Fin d) ℝ)
  (X : Fin n → Ω → EuclideanSpace ℝ (Fin d)) :
  (fun ω => ∑ i, ProbabilityTheory.bentkusWhitenedSummand S X i ω) =
    ⇑(ProbabilityTheory.bentkusWhiteningCLM S) ∘ fun ω => ∑ i, X i ω

theorem ProbabilityTheory.sum_bentkusWhitenedSummand.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  (S : Matrix (Fin d) (Fin d) ℝ)
  (X :
    Fin n →
      Ω → EuclideanSpace ℝ (Fin d)) :
  (fun ω =>
      ∑ i,
        ProbabilityTheory.bentkusWhitenedSummand
          S X i ω) =
    ⇑(ProbabilityTheory.bentkusWhiteningCLM
          S) ∘
      fun ω => ∑ i, X i ω

Whitening commutes with the finite sum of summands.

theoremdefined in ProbabilityApproximation/Bentkus/Whitening.lean

complete

theorem ProbabilityTheory.iIndepFun_bentkusWhitenedSummand.{u_1} {n d : ℕ}
  {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  (S : Matrix (Fin d) (Fin d) ℝ)
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (h_indep : ProbabilityTheory.iIndepFun X μ) :
  ProbabilityTheory.iIndepFun
    (ProbabilityTheory.bentkusWhitenedSummand S X) μ

theorem ProbabilityTheory.iIndepFun_bentkusWhitenedSummand.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  (S : Matrix (Fin d) (Fin d) ℝ)
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (h_indep :
    ProbabilityTheory.iIndepFun X μ) :
  ProbabilityTheory.iIndepFun
    (ProbabilityTheory.bentkusWhitenedSummand
      S X)
    μ

Measurable postcomposition by the whitening operator preserves mutual independence.

theoremdefined in ProbabilityApproximation/Bentkus/Whitening.lean

complete

theorem ProbabilityTheory.integral_bentkusWhitenedSummand_eq_zero.{u_1}
  {n d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ]
  (S : Matrix (Fin d) (Fin d) ℝ)
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 3 μ)
  (h_mean : ∀ (i : Fin n), ∫ (ω : Ω), X i ω ∂μ = 0) (i : Fin n) :
  ∫ (ω : Ω), ProbabilityTheory.bentkusWhitenedSummand S X i ω ∂μ = 0

theorem ProbabilityTheory.integral_bentkusWhitenedSummand_eq_zero.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ]
  (S : Matrix (Fin d) (Fin d) ℝ)
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 3 μ)
  (h_mean :
    ∀ (i : Fin n),
      ∫ (ω : Ω), X i ω ∂μ = 0)
  (i : Fin n) :
  ∫ (ω : Ω),
      ProbabilityTheory.bentkusWhitenedSummand
        S X i ω ∂μ =
    0

Centering is preserved by whitening.

theoremdefined in ProbabilityApproximation/Bentkus/Whitening.lean

complete

theorem ProbabilityTheory.covarianceBilin_map_sum_bentkusWhitenedSummand_eq_inner.{u_1}
  {n d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  (S : Matrix (Fin d) (Fin d) ℝ) (hS : S.PosDef)
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 3 μ)
  (hcov :
    ∀ (x y : EuclideanSpace ℝ (Fin d)),
      ((ProbabilityTheory.covarianceBilin
              (MeasureTheory.Measure.map (fun ω => ∑ i, X i ω) μ))
            x)
          y =
        x.ofLp ⬝ᵥ S.mulVec y.ofLp)
  (x y : EuclideanSpace ℝ (Fin d)) :
  ((ProbabilityTheory.covarianceBilin
          (MeasureTheory.Measure.map
            (fun ω =>
              ∑ i, ProbabilityTheory.bentkusWhitenedSummand S X i ω)
            μ))
        x)
      y =
    inner ℝ x y

theorem ProbabilityTheory.covarianceBilin_map_sum_bentkusWhitenedSummand_eq_inner.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  (S : Matrix (Fin d) (Fin d) ℝ)
  (hS : S.PosDef)
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 3 μ)
  (hcov :
    ∀ (x y : EuclideanSpace ℝ (Fin d)),
      ((ProbabilityTheory.covarianceBilin
              (MeasureTheory.Measure.map
                (fun ω => ∑ i, X i ω) μ))
            x)
          y =
        x.ofLp ⬝ᵥ S.mulVec y.ofLp)
  (x y : EuclideanSpace ℝ (Fin d)) :
  ((ProbabilityTheory.covarianceBilin
          (MeasureTheory.Measure.map
            (fun ω =>
              ∑ i,
                ProbabilityTheory.bentkusWhitenedSummand
                  S X i ω)
            μ))
        x)
      y =
    inner ℝ x y

Under the frozen covariance hypothesis, the whitened sum has identity covariance.

defdefined in ProbabilityApproximation/Bentkus/Whitening.lean

complete

def ProbabilityTheory.BentkusIdentityCovarianceBound.{u_1} (C : ℝ) : Prop

def ProbabilityTheory.BentkusIdentityCovarianceBound.{u_1}
  (C : ℝ) : Prop

The normalized theorem proved by Bentkus's induction: total covariance is identity and the
comparison law is standard Gaussian.

This is the standardized estimate (3.1) and the rescaling paragraph immediately after it in Bentkus (2004), printed p. 403. The formal contract isolates precisely the identity-covariance theorem that the induction must supply; it does not assume that induction has been proved.

Theorem2.3.4

Statement uses 2

Statement dependency previews

Preview

Theorem 2.3.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

Tagsbentkuswhiteningconvex-set-transportsource-bentkus-2004fidelity-exact-one-set-reduction

One-set transport from the standardized estimate. Let S be positive definite, T=S^{-1/2}, W=\sum_iX_i, and B=T(A). Write \gamma_S for centered Gaussian measure with covariance S. An invertible linear map preserves convexity, and the two event identities are \Pr(TW\in B)=\Pr(W\in A), \qquad \gamma_{I_d}(B)=\gamma_S(A). Consequently, any identity-covariance bound at the single set B transports to \left|\Pr(W\in A)-\gamma_S(A)\right| \le C d^{1/4}\sum_i\mathbb E\|S^{-1/2}X_i\|^3.

Lean code for Theorem2.3.4●7 declarations

defdefined in ProbabilityApproximation/Bentkus/Whitening.lean

complete

def ProbabilityTheory.bentkusWhitenedSet {d : ℕ}
  (S : Matrix (Fin d) (Fin d) ℝ) (hS : S.PosDef)
  (A : Set (EuclideanSpace ℝ (Fin d))) : Set (EuclideanSpace ℝ (Fin d))

def ProbabilityTheory.bentkusWhitenedSet
  {d : ℕ} (S : Matrix (Fin d) (Fin d) ℝ)
  (hS : S.PosDef)
  (A : Set (EuclideanSpace ℝ (Fin d))) :
  Set (EuclideanSpace ℝ (Fin d))

Image of a set under the whitening equivalence.

theoremdefined in ProbabilityApproximation/Bentkus/Whitening.lean

complete

theorem ProbabilityTheory.isConvexSet_bentkusWhitenedSet {d : ℕ}
  (S : Matrix (Fin d) (Fin d) ℝ) (hS : S.PosDef)
  {A : Set (EuclideanSpace ℝ (Fin d))}
  (hA : Convexity.IsConvexSet ℝ A) :
  Convexity.IsConvexSet ℝ (ProbabilityTheory.bentkusWhitenedSet S hS A)

theorem ProbabilityTheory.isConvexSet_bentkusWhitenedSet
  {d : ℕ} (S : Matrix (Fin d) (Fin d) ℝ)
  (hS : S.PosDef)
  {A : Set (EuclideanSpace ℝ (Fin d))}
  (hA : Convexity.IsConvexSet ℝ A) :
  Convexity.IsConvexSet ℝ
    (ProbabilityTheory.bentkusWhitenedSet
      S hS A)

An invertible linear whitening map preserves convexity.

theoremdefined in ProbabilityApproximation/Bentkus/Whitening.lean

complete

theorem ProbabilityTheory.map_sum_apply_bentkusWhitenedSet.{u_1} {n d : ℕ}
  {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ] (S : Matrix (Fin d) (Fin d) ℝ)
  (hS : S.PosDef) {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 3 μ)
  (A : Set (EuclideanSpace ℝ (Fin d))) :
  (MeasureTheory.Measure.map
        (fun ω => ∑ i, ProbabilityTheory.bentkusWhitenedSummand S X i ω)
        μ)
      (ProbabilityTheory.bentkusWhitenedSet S hS A) =
    (MeasureTheory.Measure.map (fun ω => ∑ i, X i ω) μ) A

theorem ProbabilityTheory.map_sum_apply_bentkusWhitenedSet.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  (S : Matrix (Fin d) (Fin d) ℝ)
  (hS : S.PosDef)
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 3 μ)
  (A : Set (EuclideanSpace ℝ (Fin d))) :
  (MeasureTheory.Measure.map
        (fun ω =>
          ∑ i,
            ProbabilityTheory.bentkusWhitenedSummand
              S X i ω)
        μ)
      (ProbabilityTheory.bentkusWhitenedSet
        S hS A) =
    (MeasureTheory.Measure.map
        (fun ω => ∑ i, X i ω) μ)
      A

The whitened-sum event in the image set is exactly the original-sum event.

theoremdefined in ProbabilityApproximation/Bentkus/Whitening.lean

complete

theorem ProbabilityTheory.stdGaussian_apply_bentkusWhitenedSet {d : ℕ}
  (S : Matrix (Fin d) (Fin d) ℝ) (hS : S.PosDef)
  (A : Set (EuclideanSpace ℝ (Fin d))) :
  (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d)))
      (ProbabilityTheory.bentkusWhitenedSet S hS A) =
    (ProbabilityTheory.multivariateGaussian 0 S) A

theorem ProbabilityTheory.stdGaussian_apply_bentkusWhitenedSet
  {d : ℕ} (S : Matrix (Fin d) (Fin d) ℝ)
  (hS : S.PosDef)
  (A : Set (EuclideanSpace ℝ (Fin d))) :
  (ProbabilityTheory.stdGaussian
        (EuclideanSpace ℝ (Fin d)))
      (ProbabilityTheory.bentkusWhitenedSet
        S hS A) =
    (ProbabilityTheory.multivariateGaussian
        0 S)
      A

The standard-Gaussian event in the whitened image is exactly the original Gaussian event.

theoremdefined in ProbabilityApproximation/Bentkus/Whitening.lean

complete

theorem ProbabilityTheory.bentkus_convex_set_whitening_reduction.{u_1} (C : ℝ)
  {d n : ℕ} {Ω : Type u_1} [MeasurableSpace Ω]
  (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ]
  (X : Fin n → Ω → EuclideanSpace ℝ (Fin d))
  (S : Matrix (Fin d) (Fin d) ℝ) (hS : S.PosDef)
  (hX : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 3 μ)
  (A : Set (EuclideanSpace ℝ (Fin d)))
  (hbound :
    |((MeasureTheory.Measure.map
                (fun ω =>
                  ∑ i, ProbabilityTheory.bentkusWhitenedSummand S X i ω)
                μ)
              (ProbabilityTheory.bentkusWhitenedSet S hS A)).toReal -
          ((ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin d)))
              (ProbabilityTheory.bentkusWhitenedSet S hS A)).toReal| ≤
      C * ↑d ^ (1 / 4) *
        ∑ i,
          ∫ (ω : Ω),
            ‖ProbabilityTheory.bentkusWhitenedSummand S X i ω‖ ^ 3 ∂μ) :
  |((MeasureTheory.Measure.map (fun ω => ∑ i, X i ω) μ) A).toReal -
        ((ProbabilityTheory.multivariateGaussian 0 S) A).toReal| ≤
    C * ↑d ^ (1 / 4) *
      ∑ i,
        ∫ (ω : Ω),
          ‖(Matrix.toEuclideanCLM (CFC.sqrt S)⁻¹) (X i ω)‖ ^ 3 ∂μ

theorem ProbabilityTheory.bentkus_convex_set_whitening_reduction.{u_1}
  (C : ℝ) {d n : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  (μ : MeasureTheory.Measure Ω)
  [MeasureTheory.IsProbabilityMeasure μ]
  (X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d))
  (S : Matrix (Fin d) (Fin d) ℝ)
  (hS : S.PosDef)
  (hX :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 3 μ)
  (A : Set (EuclideanSpace ℝ (Fin d)))
  (hbound :
    |((MeasureTheory.Measure.map
                (fun ω =>
                  ∑ i,
                    ProbabilityTheory.bentkusWhitenedSummand
                      S X i ω)
                μ)
              (ProbabilityTheory.bentkusWhitenedSet
                S hS A)).toReal -
          ((ProbabilityTheory.stdGaussian
                (EuclideanSpace ℝ
                  (Fin d)))
              (ProbabilityTheory.bentkusWhitenedSet
                S hS A)).toReal| ≤
      C * ↑d ^ (1 / 4) *
        ∑ i,
          ∫ (ω : Ω),
            ‖ProbabilityTheory.bentkusWhitenedSummand
                  S X i ω‖ ^
              3 ∂μ) :
  |((MeasureTheory.Measure.map
              (fun ω => ∑ i, X i ω) μ)
            A).toReal -
        ((ProbabilityTheory.multivariateGaussian
              0 S)
            A).toReal| ≤
    C * ↑d ^ (1 / 4) *
      ∑ i,
        ∫ (ω : Ω),
          ‖(Matrix.toEuclideanCLM
                  (CFC.sqrt S)⁻¹)
                (X i ω)‖ ^
            3 ∂μ

**Bentkus whitening reduction, at one set.**  Once the identity-covariance estimate has been
proved for the whitened family and the image of `A`, this theorem transports that estimate back to
the original variables and covariance matrix.  This is the reduction described after Theorem 1.1
of Bentkus (2004).

theoremdefined in ProbabilityApproximation/Bentkus/Whitening.lean

complete

theorem ProbabilityTheory.bentkus_convex_set_bound_of_identity_covariance_bound.{u}
  (C : ℝ) (hC : ProbabilityTheory.BentkusIdentityCovarianceBound C)
  {d n : ℕ} (hd : 0 < d) {Ω : Type u} [MeasurableSpace Ω]
  (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ]
  (X : Fin n → Ω → EuclideanSpace ℝ (Fin d))
  (S : Matrix (Fin d) (Fin d) ℝ)
  (hX : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 3 μ)
  (h_indep : ProbabilityTheory.iIndepFun X μ)
  (hX0 : ∀ (i : Fin n), ∫ (ω : Ω), X i ω ∂μ = 0) (hS : S.PosDef)
  (hcov :
    ∀ (x y : EuclideanSpace ℝ (Fin d)),
      ((ProbabilityTheory.covarianceBilin
              (MeasureTheory.Measure.map (fun ω => ∑ i, X i ω) μ))
            x)
          y =
        x.ofLp ⬝ᵥ S.mulVec y.ofLp)
  (A : Set (EuclideanSpace ℝ (Fin d))) (hA : MeasurableSet A)
  (hAconv : Convexity.IsConvexSet ℝ A) :
  |((MeasureTheory.Measure.map (fun ω => ∑ i, X i ω) μ) A).toReal -
        ((ProbabilityTheory.multivariateGaussian 0 S) A).toReal| ≤
    C * ↑d ^ (1 / 4) *
      ∑ i,
        ∫ (ω : Ω),
          ‖(Matrix.toEuclideanCLM (CFC.sqrt S)⁻¹) (X i ω)‖ ^ 3 ∂μ

theorem ProbabilityTheory.bentkus_convex_set_bound_of_identity_covariance_bound.{u}
  (C : ℝ)
  (hC :
    ProbabilityTheory.BentkusIdentityCovarianceBound
      C)
  {d n : ℕ} (hd : 0 < d) {Ω : Type u}
  [MeasurableSpace Ω]
  (μ : MeasureTheory.Measure Ω)
  [MeasureTheory.IsProbabilityMeasure μ]
  (X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d))
  (S : Matrix (Fin d) (Fin d) ℝ)
  (hX :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 3 μ)
  (h_indep :
    ProbabilityTheory.iIndepFun X μ)
  (hX0 :
    ∀ (i : Fin n),
      ∫ (ω : Ω), X i ω ∂μ = 0)
  (hS : S.PosDef)
  (hcov :
    ∀ (x y : EuclideanSpace ℝ (Fin d)),
      ((ProbabilityTheory.covarianceBilin
              (MeasureTheory.Measure.map
                (fun ω => ∑ i, X i ω) μ))
            x)
          y =
        x.ofLp ⬝ᵥ S.mulVec y.ofLp)
  (A : Set (EuclideanSpace ℝ (Fin d)))
  (hA : MeasurableSet A)
  (hAconv : Convexity.IsConvexSet ℝ A) :
  |((MeasureTheory.Measure.map
              (fun ω => ∑ i, X i ω) μ)
            A).toReal -
        ((ProbabilityTheory.multivariateGaussian
              0 S)
            A).toReal| ≤
    C * ↑d ^ (1 / 4) *
      ∑ i,
        ∫ (ω : Ω),
          ‖(Matrix.toEuclideanCLM
                  (CFC.sqrt S)⁻¹)
                (X i ω)‖ ^
            3 ∂μ

A dimension-free identity-covariance Bentkus bound transports to the corresponding bound for
an arbitrary positive-definite total covariance.  This packages the whitening reduction for the
complete theorem interface while keeping the probabilistic induction entirely in standardized
coordinates.

theoremdefined in ProbabilityApproximation/Bentkus/Whitening.lean

complete

theorem ProbabilityTheory.exists_bentkus_convex_set_constant_of_identity_covariance_bound.{u}
  (hidentity :
    ∃ C, 0 < C ∧ ProbabilityTheory.BentkusIdentityCovarianceBound C) :
  ∃ C,
    0 < C ∧
      ∀ {d n : ℕ},
        0 < d →
          ∀ {Ω : Type u} [inst : MeasurableSpace Ω]
            (μ : MeasureTheory.Measure Ω)
            [MeasureTheory.IsProbabilityMeasure μ]
            (X : Fin n → Ω → EuclideanSpace ℝ (Fin d))
            (S : Matrix (Fin d) (Fin d) ℝ),
            (∀ (i : Fin n), MeasureTheory.MemLp (X i) 3 μ) →
              ProbabilityTheory.iIndepFun X μ →
                (∀ (i : Fin n), ∫ (ω : Ω), X i ω ∂μ = 0) →
                  S.PosDef →
                    (∀ (x y : EuclideanSpace ℝ (Fin d)),
                        ((ProbabilityTheory.covarianceBilin
                                (MeasureTheory.Measure.map
                                  (fun ω => ∑ i, X i ω) μ))
                              x)
                            y =
                          x.ofLp ⬝ᵥ S.mulVec y.ofLp) →
                      ∀ (A : Set (EuclideanSpace ℝ (Fin d))),
                        MeasurableSet A →
                          Convexity.IsConvexSet ℝ A →
                            |((MeasureTheory.Measure.map
                                        (fun ω => ∑ i, X i ω) μ)
                                      A).toReal -
                                  ((ProbabilityTheory.multivariateGaussian
                                        0 S)
                                      A).toReal| ≤
                              C * ↑d ^ (1 / 4) *
                                ∑ i,
                                  ∫ (ω : Ω),
                                    ‖(Matrix.toEuclideanCLM
                                            (CFC.sqrt S)⁻¹)
                                          (X i ω)‖ ^
                                      3 ∂μ

theorem ProbabilityTheory.exists_bentkus_convex_set_constant_of_identity_covariance_bound.{u}
  (hidentity :
    ∃ C,
      0 < C ∧
        ProbabilityTheory.BentkusIdentityCovarianceBound
          C) :
  ∃ C,
    0 < C ∧
      ∀ {d n : ℕ},
        0 < d →
          ∀ {Ω : Type u}
            [inst : MeasurableSpace Ω]
            (μ : MeasureTheory.Measure Ω)
            [MeasureTheory.IsProbabilityMeasure
                μ]
            (X :
              Fin n →
                Ω →
                  EuclideanSpace ℝ
                    (Fin d))
            (S :
              Matrix (Fin d) (Fin d) ℝ),
            (∀ (i : Fin n),
                MeasureTheory.MemLp (X i)
                  3 μ) →
              ProbabilityTheory.iIndepFun
                  X μ →
                (∀ (i : Fin n),
                    ∫ (ω : Ω), X i ω ∂μ =
                      0) →
                  S.PosDef →
                    (∀
                        (x y :
                          EuclideanSpace ℝ
                            (Fin d)),
                        ((ProbabilityTheory.covarianceBilin
                                (MeasureTheory.Measure.map
                                  (fun
                                      ω =>
                                    ∑ i,
                                      X i
                                        ω)
                                  μ))
                              x)
                            y =
                          x.ofLp ⬝ᵥ
                            S.mulVec
                              y.ofLp) →
                      ∀
                        (A :
                          Set
                            (EuclideanSpace
                              ℝ (Fin d))),
                        MeasurableSet A →
                          Convexity.IsConvexSet
                              ℝ A →
                            |((MeasureTheory.Measure.map
                                        (fun
                                            ω =>
                                          ∑
                                            i,
                                            X
                                              i
                                              ω)
                                        μ)
                                      A).toReal -
                                  ((ProbabilityTheory.multivariateGaussian
                                        0
                                        S)
                                      A).toReal| ≤
                              C *
                                  ↑d ^
                                    (1 /
                                      4) *
                                ∑ i,
                                  ∫ (ω :
                                    Ω),
                                    ‖(Matrix.toEuclideanCLM
                                            (CFC.sqrt
                                                S)⁻¹)
                                          (X
                                            i
                                            ω)‖ ^
                                      3 ∂μ

An absolute identity-covariance constant yields Bentkus's full positive-definite covariance
theorem by whitening.

Bentkus (2004), uses invariance of the set class under invertible symmetric linear maps in condition (i), printed p. 401, and applies the transformation C^{-1} immediately after equation (3.1), printed p. 403. This node is the one-set form of that reduction and yields exactly the normalization in Theorem 1.1, equation (1.1), printed p. 400.