Berry–Esseen Bounds for Independent Sums

2.9. The identity-covariance replacement induction🔗

Lemma2.9.1
uses 1used by 1✓L∃∀N
Tagsbentkusgaussian-replacementinductionmomentssource-bentkus-2004fidelity-explicit-trivial-branches

The small-cardinality and large-summand induction branches. Let X_1,\ldots,X_n be independent centered L^3 random vectors in \mathbb R^d, assume that \operatorname{Cov}(\sum_iX_i)=I_d, and put \beta=\sum_i\mathbb E\|X_i\|^3. Then \sum_i\mathbb E\|X_i\|^2=d, \qquad d^3\le n\beta^2. If d>0, M\ge0, and n\le d^3M^2, then 1\le M\beta; hence, for every probability measure \nu on \mathbb R^d and every set A, \left|\Pr\left(\sum_iX_i\in A\right)-\nu(A)\right|\le M\beta. Separately, if one summand satisfies \mathbb E\|X_k\|^2\ge\tfrac14, then 1\le8\,\mathbb E\|X_k\|^3.

Lean code for Lemma2.9.1●5 theorems
  • theoremdefined in ProbabilityApproximation/Bentkus/InductionBranches.lean
    complete
    theorem ProbabilityTheory.sum_integral_norm_sq_eq_dimension_of_identityCovariance.{u_1}
  {n d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX3 : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 3 μ)
  (h_indep : ProbabilityTheory.iIndepFun X μ)
  (hX0 : ∀ (i : Fin n), ∫ (ω : Ω), X i ω ∂μ = 0)
  (hidentity :
    ∀ (x y : EuclideanSpace ℝ (Fin d)),
      ((ProbabilityTheory.covarianceBilin
              (MeasureTheory.Measure.map (fun ω => ∑ i, X i ω) μ))
            x)
          y =
        inner ℝ x y) :
  ∑ i, ∫ (ω : Ω), ‖X i ω‖ ^ 2 ∂μ = ↑d
    theorem ProbabilityTheory.sum_integral_norm_sq_eq_dimension_of_identityCovariance.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX3 :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 3 μ)
  (h_indep :
    ProbabilityTheory.iIndepFun X μ)
  (hX0 :
    ∀ (i : Fin n),
      ∫ (ω : Ω), X i ω ∂μ = 0)
  (hidentity :
    ∀ (x y : EuclideanSpace ℝ (Fin d)),
      ((ProbabilityTheory.covarianceBilin
              (MeasureTheory.Measure.map
                (fun ω => ∑ i, X i ω) μ))
            x)
          y =
        inner ℝ x y) :
  ∑ i, ∫ (ω : Ω), ‖X i ω‖ ^ 2 ∂μ = ↑d
    For centered independent summands with identity total covariance, the sum of the individual
second norm moments is exactly the ambient dimension.
  • theoremdefined in ProbabilityApproximation/Bentkus/InductionBranches.lean
    complete
    theorem ProbabilityTheory.dimension_cube_le_card_mul_thirdMomentSum_sq.{u_1}
  {n d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX3 : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 3 μ)
  (h_indep : ProbabilityTheory.iIndepFun X μ)
  (hX0 : ∀ (i : Fin n), ∫ (ω : Ω), X i ω ∂μ = 0)
  (hidentity :
    ∀ (x y : EuclideanSpace ℝ (Fin d)),
      ((ProbabilityTheory.covarianceBilin
              (MeasureTheory.Measure.map (fun ω => ∑ i, X i ω) μ))
            x)
          y =
        inner ℝ x y) :
  ↑d ^ 3 ≤ ↑n * (∑ i, ∫ (ω : Ω), ‖X i ω‖ ^ 3 ∂μ) ^ 2
    theorem ProbabilityTheory.dimension_cube_le_card_mul_thirdMomentSum_sq.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX3 :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 3 μ)
  (h_indep :
    ProbabilityTheory.iIndepFun X μ)
  (hX0 :
    ∀ (i : Fin n),
      ∫ (ω : Ω), X i ω ∂μ = 0)
  (hidentity :
    ∀ (x y : EuclideanSpace ℝ (Fin d)),
      ((ProbabilityTheory.covarianceBilin
              (MeasureTheory.Measure.map
                (fun ω => ∑ i, X i ω) μ))
            x)
          y =
        inner ℝ x y) :
  ↑d ^ 3 ≤
    ↑n *
      (∑ i, ∫ (ω : Ω), ‖X i ω‖ ^ 3 ∂μ) ^ 2
    The exact Hölder consequence used for Bentkus's small-cardinality branch.
  • theoremdefined in ProbabilityApproximation/Bentkus/InductionBranches.lean
    complete
    theorem ProbabilityTheory.small_cardinality_thirdMomentSum_lower.{u_1} {n d : ℕ}
  {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)} (hd : 0 < d) {M : ℝ}
  (hM : 0 ≤ M) (hsmall : ↑n ≤ ↑d ^ 3 * M ^ 2)
  (hX3 : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 3 μ)
  (h_indep : ProbabilityTheory.iIndepFun X μ)
  (hX0 : ∀ (i : Fin n), ∫ (ω : Ω), X i ω ∂μ = 0)
  (hidentity :
    ∀ (x y : EuclideanSpace ℝ (Fin d)),
      ((ProbabilityTheory.covarianceBilin
              (MeasureTheory.Measure.map (fun ω => ∑ i, X i ω) μ))
            x)
          y =
        inner ℝ x y) :
  1 ≤ M * ∑ i, ∫ (ω : Ω), ‖X i ω‖ ^ 3 ∂μ
    theorem ProbabilityTheory.small_cardinality_thirdMomentSum_lower.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hd : 0 < d) {M : ℝ} (hM : 0 ≤ M)
  (hsmall : ↑n ≤ ↑d ^ 3 * M ^ 2)
  (hX3 :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 3 μ)
  (h_indep :
    ProbabilityTheory.iIndepFun X μ)
  (hX0 :
    ∀ (i : Fin n),
      ∫ (ω : Ω), X i ω ∂μ = 0)
  (hidentity :
    ∀ (x y : EuclideanSpace ℝ (Fin d)),
      ((ProbabilityTheory.covarianceBilin
              (MeasureTheory.Measure.map
                (fun ω => ∑ i, X i ω) μ))
            x)
          y =
        inner ℝ x y) :
  1 ≤ M * ∑ i, ∫ (ω : Ω), ‖X i ω‖ ^ 3 ∂μ
    If `n ≤ d³ M²`, identity covariance forces `M ∑ E ‖Xᵢ‖³ ≥ 1`.
  • theoremdefined in ProbabilityApproximation/Bentkus/InductionBranches.lean
    complete
    theorem ProbabilityTheory.probability_error_le_M_mul_thirdMomentSum_of_small_cardinality.{u_1}
  {n d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  {ν : MeasureTheory.Measure (EuclideanSpace ℝ (Fin d))}
  [MeasureTheory.IsProbabilityMeasure ν] (hd : 0 < d) {M : ℝ}
  (hM : 0 ≤ M) (hsmall : ↑n ≤ ↑d ^ 3 * M ^ 2)
  (hX3 : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 3 μ)
  (h_indep : ProbabilityTheory.iIndepFun X μ)
  (hX0 : ∀ (i : Fin n), ∫ (ω : Ω), X i ω ∂μ = 0)
  (hidentity :
    ∀ (x y : EuclideanSpace ℝ (Fin d)),
      ((ProbabilityTheory.covarianceBilin
              (MeasureTheory.Measure.map (fun ω => ∑ i, X i ω) μ))
            x)
          y =
        inner ℝ x y)
  (A : Set (EuclideanSpace ℝ (Fin d))) :
  |(MeasureTheory.Measure.map (fun ω => ∑ i, X i ω) μ).real A -
        ν.real A| ≤
    M * ∑ i, ∫ (ω : Ω), ‖X i ω‖ ^ 3 ∂μ
    theorem ProbabilityTheory.probability_error_le_M_mul_thirdMomentSum_of_small_cardinality.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  {ν :
    MeasureTheory.Measure
      (EuclideanSpace ℝ (Fin d))}
  [MeasureTheory.IsProbabilityMeasure ν]
  (hd : 0 < d) {M : ℝ} (hM : 0 ≤ M)
  (hsmall : ↑n ≤ ↑d ^ 3 * M ^ 2)
  (hX3 :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 3 μ)
  (h_indep :
    ProbabilityTheory.iIndepFun X μ)
  (hX0 :
    ∀ (i : Fin n),
      ∫ (ω : Ω), X i ω ∂μ = 0)
  (hidentity :
    ∀ (x y : EuclideanSpace ℝ (Fin d)),
      ((ProbabilityTheory.covarianceBilin
              (MeasureTheory.Measure.map
                (fun ω => ∑ i, X i ω) μ))
            x)
          y =
        inner ℝ x y)
  (A : Set (EuclideanSpace ℝ (Fin d))) :
  |(MeasureTheory.Measure.map
              (fun ω => ∑ i, X i ω)
              μ).real
          A -
        ν.real A| ≤
    M * ∑ i, ∫ (ω : Ω), ‖X i ω‖ ^ 3 ∂μ
    Bentkus's small-cardinality branch as a ready-to-use probability-error estimate.
  • theoremdefined in ProbabilityApproximation/Bentkus/InductionBranches.lean
    complete
    theorem ProbabilityTheory.large_secondMoment_thirdMoment_lower.{u_1, u_2}
  {Ω : Type u_1} {E : Type u_2} [MeasurableSpace Ω]
  [NormedAddCommGroup E] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → E}
  (hX3 : MeasureTheory.MemLp X 3 μ)
  (hlarge : 1 / 4 ≤ ∫ (ω : Ω), ‖X ω‖ ^ 2 ∂μ) :
  1 ≤ 8 * ∫ (ω : Ω), ‖X ω‖ ^ 3 ∂μ
    theorem ProbabilityTheory.large_secondMoment_thirdMoment_lower.{u_1,
    u_2}
  {Ω : Type u_1} {E : Type u_2}
  [MeasurableSpace Ω]
  [NormedAddCommGroup E]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : Ω → E}
  (hX3 : MeasureTheory.MemLp X 3 μ)
  (hlarge :
    1 / 4 ≤ ∫ (ω : Ω), ‖X ω‖ ^ 2 ∂μ) :
  1 ≤ 8 * ∫ (ω : Ω), ‖X ω‖ ^ 3 ∂μ
    A summand whose second norm moment is at least `1/4` has third norm moment at least `1/8`.
This is the moment conversion used after detecting a large individual covariance.

These are the two trivial branches at the start of Section 3 in Bentkus (2004), printed p. 403. The first is the Hölder calculation and \Delta\le1 argument immediately after equation (3.1) for n\le d^3M^2; the second is the large-individual-covariance exclusion immediately before equation (3.2). These are precisely the moment consequences used before the nontrivial Taylor induction begins.

Lemma2.9.2
Statement uses 2
Statement dependency previews
Preview
Theorem 2.2.8
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagsbentkusgaussian-replacementleave-one-outwhiteningsource-bentkus-2004fidelity-explicit-small-moment-branch

Leave-one-out whitening in the small-second-moment branch. Under identity total covariance, fix k and suppose that \mathbb E\|X_k\|^2<\frac14. If U_k=\sum_{i\ne k}X_i and S_k=\operatorname{Cov}(U_k), then S_k is positive definite. Its inverse square root T_k=S_k^{-1/2} satisfies \|T_kx\|\le2\|x\|, \qquad \|T_kx\|^3\le8\|x\|^3. Consequently, for every L^3 random vector Z on any measure space, \int\|T_kZ\|^3\le8\int\|Z\|^3.

Lean code for Lemma2.9.2●4 theorems
  • theoremdefined in ProbabilityApproximation/Bentkus/LeaveOneOutWhitening.lean
    complete
    theorem ProbabilityTheory.bentkusLeaveOneOutCovarianceMatrix_posDef_of_integral_norm_sq_lt_quarter.{u_1}
  {n d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX3 : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 3 μ)
  (h_indep : ProbabilityTheory.iIndepFun X μ)
  (hX0 : ∀ (i : Fin n), ∫ (ω : Ω), X i ω ∂μ = 0)
  (hidentity :
    ∀ (x y : EuclideanSpace ℝ (Fin d)),
      ((ProbabilityTheory.covarianceBilin
              (MeasureTheory.Measure.map (fun ω => ∑ i, X i ω) μ))
            x)
          y =
        inner ℝ x y)
  (k : Fin n) (hk : ∫ (ω : Ω), ‖X k ω‖ ^ 2 ∂μ < 1 / 4) :
  (ProbabilityTheory.bentkusLeaveOneOutCovarianceMatrix μ X k).PosDef
    theorem ProbabilityTheory.bentkusLeaveOneOutCovarianceMatrix_posDef_of_integral_norm_sq_lt_quarter.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX3 :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 3 μ)
  (h_indep :
    ProbabilityTheory.iIndepFun X μ)
  (hX0 :
    ∀ (i : Fin n),
      ∫ (ω : Ω), X i ω ∂μ = 0)
  (hidentity :
    ∀ (x y : EuclideanSpace ℝ (Fin d)),
      ((ProbabilityTheory.covarianceBilin
              (MeasureTheory.Measure.map
                (fun ω => ∑ i, X i ω) μ))
            x)
          y =
        inner ℝ x y)
  (k : Fin n)
  (hk :
    ∫ (ω : Ω), ‖X k ω‖ ^ 2 ∂μ < 1 / 4) :
  (ProbabilityTheory.bentkusLeaveOneOutCovarianceMatrix
      μ X k).PosDef
    Under identity total covariance, removing a summand whose second norm moment is below
`1 / 4` leaves a positive-definite covariance matrix.
  • theoremdefined in ProbabilityApproximation/Bentkus/LeaveOneOutWhitening.lean
    complete
    theorem ProbabilityTheory.norm_bentkusWhiteningCLM_leaveOneOut_apply_le_two.{u_1}
  {n d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX3 : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 3 μ)
  (h_indep : ProbabilityTheory.iIndepFun X μ)
  (hX0 : ∀ (i : Fin n), ∫ (ω : Ω), X i ω ∂μ = 0)
  (hidentity :
    ∀ (x y : EuclideanSpace ℝ (Fin d)),
      ((ProbabilityTheory.covarianceBilin
              (MeasureTheory.Measure.map (fun ω => ∑ i, X i ω) μ))
            x)
          y =
        inner ℝ x y)
  (k : Fin n) (hk : ∫ (ω : Ω), ‖X k ω‖ ^ 2 ∂μ < 1 / 4)
  (x : EuclideanSpace ℝ (Fin d)) :
  ‖(ProbabilityTheory.bentkusWhiteningCLM
          (ProbabilityTheory.bentkusLeaveOneOutCovarianceMatrix μ X k))
        x‖ ≤
    2 * ‖x‖
    theorem ProbabilityTheory.norm_bentkusWhiteningCLM_leaveOneOut_apply_le_two.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX3 :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 3 μ)
  (h_indep :
    ProbabilityTheory.iIndepFun X μ)
  (hX0 :
    ∀ (i : Fin n),
      ∫ (ω : Ω), X i ω ∂μ = 0)
  (hidentity :
    ∀ (x y : EuclideanSpace ℝ (Fin d)),
      ((ProbabilityTheory.covarianceBilin
              (MeasureTheory.Measure.map
                (fun ω => ∑ i, X i ω) μ))
            x)
          y =
        inner ℝ x y)
  (k : Fin n)
  (hk : ∫ (ω : Ω), ‖X k ω‖ ^ 2 ∂μ < 1 / 4)
  (x : EuclideanSpace ℝ (Fin d)) :
  ‖(ProbabilityTheory.bentkusWhiteningCLM
          (ProbabilityTheory.bentkusLeaveOneOutCovarianceMatrix
            μ X k))
        x‖ ≤
    2 * ‖x‖
    The inverse square root of a leave-one-out covariance with lower spectral bound `3 / 4`
expands Euclidean norms by at most a factor of `2`.
  • theoremdefined in ProbabilityApproximation/Bentkus/LeaveOneOutWhitening.lean
    complete
    theorem ProbabilityTheory.norm_bentkusWhiteningCLM_leaveOneOut_apply_pow_three_le.{u_1}
  {n d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX3 : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 3 μ)
  (h_indep : ProbabilityTheory.iIndepFun X μ)
  (hX0 : ∀ (i : Fin n), ∫ (ω : Ω), X i ω ∂μ = 0)
  (hidentity :
    ∀ (x y : EuclideanSpace ℝ (Fin d)),
      ((ProbabilityTheory.covarianceBilin
              (MeasureTheory.Measure.map (fun ω => ∑ i, X i ω) μ))
            x)
          y =
        inner ℝ x y)
  (k : Fin n) (hk : ∫ (ω : Ω), ‖X k ω‖ ^ 2 ∂μ < 1 / 4)
  (x : EuclideanSpace ℝ (Fin d)) :
  ‖(ProbabilityTheory.bentkusWhiteningCLM
            (ProbabilityTheory.bentkusLeaveOneOutCovarianceMatrix μ X
              k))
          x‖ ^
      3 ≤
    8 * ‖x‖ ^ 3
    theorem ProbabilityTheory.norm_bentkusWhiteningCLM_leaveOneOut_apply_pow_three_le.{u_1}
  {n d : ℕ} {Ω : Type u_1}
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX3 :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 3 μ)
  (h_indep :
    ProbabilityTheory.iIndepFun X μ)
  (hX0 :
    ∀ (i : Fin n),
      ∫ (ω : Ω), X i ω ∂μ = 0)
  (hidentity :
    ∀ (x y : EuclideanSpace ℝ (Fin d)),
      ((ProbabilityTheory.covarianceBilin
              (MeasureTheory.Measure.map
                (fun ω => ∑ i, X i ω) μ))
            x)
          y =
        inner ℝ x y)
  (k : Fin n)
  (hk : ∫ (ω : Ω), ‖X k ω‖ ^ 2 ∂μ < 1 / 4)
  (x : EuclideanSpace ℝ (Fin d)) :
  ‖(ProbabilityTheory.bentkusWhiteningCLM
            (ProbabilityTheory.bentkusLeaveOneOutCovarianceMatrix
              μ X k))
          x‖ ^
      3 ≤
    8 * ‖x‖ ^ 3
    Cubing the leave-one-out whitening norm estimate produces the factor `8` used in the
third-moment remainder.
  • theoremdefined in ProbabilityApproximation/Bentkus/LeaveOneOutWhitening.lean
    complete
    theorem ProbabilityTheory.integral_norm_bentkusWhiteningCLM_leaveOneOut_pow_three_le.{u_1,
    u_2}
  {n d : ℕ} {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω]
  [MeasurableSpace Ω'] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ] {ν : MeasureTheory.Measure Ω'}
  {X : Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX3 : ∀ (i : Fin n), MeasureTheory.MemLp (X i) 3 μ)
  (h_indep : ProbabilityTheory.iIndepFun X μ)
  (hX0 : ∀ (i : Fin n), ∫ (ω : Ω), X i ω ∂μ = 0)
  (hidentity :
    ∀ (x y : EuclideanSpace ℝ (Fin d)),
      ((ProbabilityTheory.covarianceBilin
              (MeasureTheory.Measure.map (fun ω => ∑ i, X i ω) μ))
            x)
          y =
        inner ℝ x y)
  (k : Fin n) (hk : ∫ (ω : Ω), ‖X k ω‖ ^ 2 ∂μ < 1 / 4)
  {Z : Ω' → EuclideanSpace ℝ (Fin d)}
  (hZ3 : MeasureTheory.MemLp Z 3 ν) :
  ∫ (ω : Ω'),
      ‖(ProbabilityTheory.bentkusWhiteningCLM
              (ProbabilityTheory.bentkusLeaveOneOutCovarianceMatrix μ X
                k))
            (Z ω)‖ ^
        3 ∂ν ≤
    8 * ∫ (ω : Ω'), ‖Z ω‖ ^ 3 ∂ν
    theorem ProbabilityTheory.integral_norm_bentkusWhiteningCLM_leaveOneOut_pow_three_le.{u_1,
    u_2}
  {n d : ℕ} {Ω : Type u_1} {Ω' : Type u_2}
  [MeasurableSpace Ω] [MeasurableSpace Ω']
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {ν : MeasureTheory.Measure Ω'}
  {X :
    Fin n → Ω → EuclideanSpace ℝ (Fin d)}
  (hX3 :
    ∀ (i : Fin n),
      MeasureTheory.MemLp (X i) 3 μ)
  (h_indep :
    ProbabilityTheory.iIndepFun X μ)
  (hX0 :
    ∀ (i : Fin n),
      ∫ (ω : Ω), X i ω ∂μ = 0)
  (hidentity :
    ∀ (x y : EuclideanSpace ℝ (Fin d)),
      ((ProbabilityTheory.covarianceBilin
              (MeasureTheory.Measure.map
                (fun ω => ∑ i, X i ω) μ))
            x)
          y =
        inner ℝ x y)
  (k : Fin n)
  (hk : ∫ (ω : Ω), ‖X k ω‖ ^ 2 ∂μ < 1 / 4)
  {Z : Ω' → EuclideanSpace ℝ (Fin d)}
  (hZ3 : MeasureTheory.MemLp Z 3 ν) :
  ∫ (ω : Ω'),
      ‖(ProbabilityTheory.bentkusWhiteningCLM
              (ProbabilityTheory.bentkusLeaveOneOutCovarianceMatrix
                μ X k))
            (Z ω)‖ ^
        3 ∂ν ≤
    8 * ∫ (ω : Ω'), ‖Z ω‖ ^ 3 ∂ν
    Integrated third moments increase by at most a factor of `8` under leave-one-out
whitening.  The random vector being transformed may live on a different measure space.

This is the small-individual-covariance branch introduced after equation (3.2) in Bentkus (2004), printed pp. 403--404. The paper writes P_k^2=\operatorname{Cov}(U_k) and Q_k=P_k^{-1} and, after excluding the large-covariance trivial case, assumes \|Q_k\|\le2; this gives the third-moment factor 2^3=8.

Theorem2.9.3
Statement uses 18
Statement dependency previews
Preview
Theorem 2.2.4
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagsbentkusgaussian-replacementinductionsource-bentkus-2004fidelity-exact-identity-covariance

Identity-covariance convex-set replacement bound. There is an absolute constant C>0 such that, for every d,n\in\mathbb N with d>0, every probability space (\Omega,\mathcal F,\mu), and every family X_i:\Omega\to\mathbb R^d indexed by i\in\operatorname{Fin}(n) satisfying X_i\in L^3(\mu), mutual independence, and \int_\Omega X_i\,d\mu=0, if W=\sum_iX_i has identity covariance in the bilinear sense \operatorname{Cov}_{\mu\circ W^{-1}}(x,y)=\langle x,y\rangle \qquad\text{for every }x,y\in\mathbb R^d, one has, for every measurable convex A\subseteq\mathbb R^d, \left|(\mu\circ W^{-1})(A)-\gamma_d(A)\right| \le C d^{1/4}\sum_{i\in\operatorname{Fin}(n)} \int_\Omega\|X_i(\omega)\|^3\,d\mu(\omega), where \gamma_d is standard Gaussian measure on \mathbb R^d.

Lean code for Theorem2.9.3●1 theorem
  • theoremdefined in ProbabilityApproximation/Bentkus/Induction.lean
    complete
    theorem ProbabilityTheory.exists_bentkus_identity_covariance_constant.{u} :
  ∃ C, 0 < C ∧ ProbabilityTheory.BentkusIdentityCovarianceBound C
    theorem ProbabilityTheory.exists_bentkus_identity_covariance_constant.{u} :
  ∃ C,
    0 < C ∧
      ProbabilityTheory.BentkusIdentityCovarianceBound
        C
    The standardized Bentkus induction admits one absolute constant.

This is the identity-covariance specialization of Bentkus (2004), Theorem 1.2, printed p. 401, and the standardized setup in equation (3.1), printed p. 403. The leave-one-out induction begins with equation (3.2), printed p. 403; the rotation and replacement estimates in equations (3.4)--(3.15) occupy printed pp. 404--405, and the proof continues through printed p. 409. Bentkus leaves the absolute constant unspecified; tracking constants through the preceding estimates gives one absolute choice.