Berry–Esseen Bounds for Independent Sums

1.8. Reflection and the nonuniform theorem🔗

Theorem1.8.1
Statement uses 3
Statement dependency previews
Preview
Theorem 1.2.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagsscalarreductionreflectionsource-chen-shao-2005fidelity-exact

Reduction from upper-truncated decay to the nonuniform theorem. Suppose an absolute A\ge0 satisfies the central exponential estimate in the preceding node for all finite families. Then there is an absolute C=270+54A>0 such that every centered independent family with finite third moments and unit total variance satisfies, for all x\in\mathbb R, \left|\Pr(W\le x)-\Phi(x)\right| \le\frac{C\gamma}{1+|x|^3}.

Lean code for Theorem1.8.1●5 declarations
  • defdefined in ProbabilityApproximation/ChenShao/NonuniformReduction.lean
    complete
    def ProbabilityTheory.nonuniformReductionConstant (A : ℝ) : ℝ
    def ProbabilityTheory.nonuniformReductionConstant
  (A : ℝ) : ℝ
    Explicit release constant obtained from a truncated exponential-decay estimate with constant
`A`.
  • theoremdefined in ProbabilityApproximation/ChenShao/NonuniformReduction.lean
    complete
    theorem ProbabilityTheory.nonuniformReductionConstant_pos {A : ℝ} (hA : 0 ≤ A) :
  0 < ProbabilityTheory.nonuniformReductionConstant A
    theorem ProbabilityTheory.nonuniformReductionConstant_pos
  {A : ℝ} (hA : 0 ≤ A) :
  0 <
    ProbabilityTheory.nonuniformReductionConstant
      A
  • theoremdefined in ProbabilityApproximation/ChenShao/CDFReflection.lean
    complete
    theorem ProbabilityTheory.cdf_gaussian_error_le_of_nonneg_of_map_neg
  (ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure ν]
  {K : ℝ}
  (hν :
    ∀ (x : ℝ),
      0 ≤ x →
        |↑(ProbabilityTheory.cdf ν) x -
              ↑(ProbabilityTheory.cdf
                    (ProbabilityTheory.gaussianReal 0 1))
                x| ≤
          K / (1 + x ^ 3))
  (hneg :
    ∀ (x : ℝ),
      0 ≤ x →
        |↑(ProbabilityTheory.cdf
                    (MeasureTheory.Measure.map (fun z => -z) ν))
                x -
              ↑(ProbabilityTheory.cdf
                    (ProbabilityTheory.gaussianReal 0 1))
                x| ≤
          K / (1 + x ^ 3))
  (x : ℝ) :
  |↑(ProbabilityTheory.cdf ν) x -
        ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1))
          x| ≤
    K / (1 + |x| ^ 3)
    theorem ProbabilityTheory.cdf_gaussian_error_le_of_nonneg_of_map_neg
  (ν : MeasureTheory.Measure ℝ)
  [MeasureTheory.IsProbabilityMeasure ν]
  {K : ℝ}
  (hν :
    ∀ (x : ℝ),
      0 ≤ x →
        |↑(ProbabilityTheory.cdf ν) x -
              ↑(ProbabilityTheory.cdf
                    (ProbabilityTheory.gaussianReal
                      0 1))
                x| ≤
          K / (1 + x ^ 3))
  (hneg :
    ∀ (x : ℝ),
      0 ≤ x →
        |↑(ProbabilityTheory.cdf
                    (MeasureTheory.Measure.map
                      (fun z => -z) ν))
                x -
              ↑(ProbabilityTheory.cdf
                    (ProbabilityTheory.gaussianReal
                      0 1))
                x| ≤
          K / (1 + x ^ 3))
  (x : ℝ) :
  |↑(ProbabilityTheory.cdf ν) x -
        ↑(ProbabilityTheory.cdf
              (ProbabilityTheory.gaussianReal
                0 1))
          x| ≤
    K / (1 + |x| ^ 3)
    A nonuniform standard-Gaussian CDF estimate for a probability measure and its reflection on
nonnegative thresholds yields the corresponding estimate at every real threshold.
  • theoremdefined in ProbabilityApproximation/ChenShao/NonuniformReduction.lean
    complete
    theorem ProbabilityTheory.nonuniformBerryEsseen_nonnegative_of_upperTruncated_decay.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : ι → Ω → ℝ} (hXmeas : ∀ (i : ι), Measurable (X i))
  (hX3 : ∀ (i : ι), MeasureTheory.MemLp (X i) 3 μ)
  (h_indep : ProbabilityTheory.iIndepFun X μ)
  (h_mean : ∀ (i : ι), ∫ (ω : Ω), X i ω ∂μ = 0)
  (hvar : ∑ i, ProbabilityTheory.variance (X i) μ = 1) {A : ℝ}
  (hA : 0 ≤ A)
  (hcentral :
    ∀ (z : ℝ),
      2 ≤ z →
        ProbabilityTheory.thirdMomentSum X μ ≤ 1 →
          |↑(ProbabilityTheory.cdf
                      (MeasureTheory.Measure.map
                        (ProbabilityTheory.upperTruncatedSum X) μ))
                  z -
                ↑(ProbabilityTheory.cdf
                      (ProbabilityTheory.gaussianReal 0 1))
                  z| ≤
            A * Real.exp (-z / 2) *
              ProbabilityTheory.thirdMomentSum X μ)
  (z : ℝ) :
  0 ≤ z →
    |↑(ProbabilityTheory.cdf
                (MeasureTheory.Measure.map (ProbabilityTheory.sumX X)
                  μ))
            z -
          ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1))
            z| ≤
      ProbabilityTheory.nonuniformReductionConstant A *
          ProbabilityTheory.thirdMomentSum X μ /
        (1 + z ^ 3)
    theorem ProbabilityTheory.nonuniformBerryEsseen_nonnegative_of_upperTruncated_decay.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : ι → Ω → ℝ}
  (hXmeas : ∀ (i : ι), Measurable (X i))
  (hX3 :
    ∀ (i : ι),
      MeasureTheory.MemLp (X i) 3 μ)
  (h_indep :
    ProbabilityTheory.iIndepFun X μ)
  (h_mean :
    ∀ (i : ι), ∫ (ω : Ω), X i ω ∂μ = 0)
  (hvar :
    ∑ i,
        ProbabilityTheory.variance (X i)
          μ =
      1)
  {A : ℝ} (hA : 0 ≤ A)
  (hcentral :
    ∀ (z : ℝ),
      2 ≤ z →
        ProbabilityTheory.thirdMomentSum X
              μ ≤
            1 →
          |↑(ProbabilityTheory.cdf
                      (MeasureTheory.Measure.map
                        (ProbabilityTheory.upperTruncatedSum
                          X)
                        μ))
                  z -
                ↑(ProbabilityTheory.cdf
                      (ProbabilityTheory.gaussianReal
                        0 1))
                  z| ≤
            A * Real.exp (-z / 2) *
              ProbabilityTheory.thirdMomentSum
                X μ)
  (z : ℝ) :
  0 ≤ z →
    |↑(ProbabilityTheory.cdf
                (MeasureTheory.Measure.map
                  (ProbabilityTheory.sumX
                    X)
                  μ))
            z -
          ↑(ProbabilityTheory.cdf
                (ProbabilityTheory.gaussianReal
                  0 1))
            z| ≤
      ProbabilityTheory.nonuniformReductionConstant
            A *
          ProbabilityTheory.thirdMomentSum
            X μ /
        (1 + z ^ 3)
    A central exponential-decay estimate for the one-sided truncated sum implies the public cubic
estimate for the original sum at every nonnegative threshold.
  • theoremdefined in ProbabilityApproximation/ChenShao/NonuniformReduction.lean
    complete
    theorem ProbabilityTheory.exists_nonuniformBerryEsseen_of_upperTruncated_decay.{uι,
    uΩ}
  (A : ℝ) (hA : 0 ≤ A)
  (hcentral :
    ∀ {ι : Type uι} {Ω : Type uΩ} [inst : Fintype ι]
      [inst_1 : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω)
      [MeasureTheory.IsProbabilityMeasure μ] (X : ι → Ω → ℝ),
      (∀ (i : ι), Measurable (X i)) →
        (∀ (i : ι), MeasureTheory.MemLp (X i) 3 μ) →
          ProbabilityTheory.iIndepFun X μ →
            (∀ (i : ι), ∫ (ω : Ω), X i ω ∂μ = 0) →
              ∑ i, ProbabilityTheory.variance (X i) μ = 1 →
                ∀ (z : ℝ),
                  2 ≤ z →
                    ProbabilityTheory.thirdMomentSum X μ ≤ 1 →
                      |↑(ProbabilityTheory.cdf
                                  (MeasureTheory.Measure.map
                                    (ProbabilityTheory.upperTruncatedSum
                                      X)
                                    μ))
                              z -
                            ↑(ProbabilityTheory.cdf
                                  (ProbabilityTheory.gaussianReal 0 1))
                              z| ≤
                        A * Real.exp (-z / 2) *
                          ProbabilityTheory.thirdMomentSum X μ) :
  ∃ C,
    0 < C ∧
      ∀ {ι : Type uι} {Ω : Type uΩ} [inst : Fintype ι]
        [inst_1 : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω)
        [MeasureTheory.IsProbabilityMeasure μ] (X : ι → Ω → ℝ),
        (∀ (i : ι), Measurable (X i)) →
          ProbabilityTheory.iIndepFun X μ →
            (∀ (i : ι), ∫ (ω : Ω), X i ω ∂μ = 0) →
              (∀ (i : ι), MeasureTheory.MemLp (X i) 3 μ) →
                ∑ i, ProbabilityTheory.variance (X i) μ = 1 →
                  ∀ (x : ℝ),
                    |↑(ProbabilityTheory.cdf
                                (MeasureTheory.Measure.map
                                  (fun ω => ∑ i, X i ω) μ))
                            x -
                          ↑(ProbabilityTheory.cdf
                                (ProbabilityTheory.gaussianReal 0 1))
                            x| ≤
                      (C * ∑ i, ∫ (ω : Ω), |X i ω| ^ 3 ∂μ) /
                        (1 + |x| ^ 3)
    theorem ProbabilityTheory.exists_nonuniformBerryEsseen_of_upperTruncated_decay.{uι,
    uΩ}
  (A : ℝ) (hA : 0 ≤ A)
  (hcentral :
    ∀ {ι : Type uι} {Ω : Type uΩ}
      [inst : Fintype ι]
      [inst_1 : MeasurableSpace Ω]
      (μ : MeasureTheory.Measure Ω)
      [MeasureTheory.IsProbabilityMeasure
          μ]
      (X : ι → Ω → ℝ),
      (∀ (i : ι), Measurable (X i)) →
        (∀ (i : ι),
            MeasureTheory.MemLp (X i) 3
              μ) →
          ProbabilityTheory.iIndepFun X
              μ →
            (∀ (i : ι),
                ∫ (ω : Ω), X i ω ∂μ = 0) →
              ∑ i,
                    ProbabilityTheory.variance
                      (X i) μ =
                  1 →
                ∀ (z : ℝ),
                  2 ≤ z →
                    ProbabilityTheory.thirdMomentSum
                          X μ ≤
                        1 →
                      |↑(ProbabilityTheory.cdf
                                  (MeasureTheory.Measure.map
                                    (ProbabilityTheory.upperTruncatedSum
                                      X)
                                    μ))
                              z -
                            ↑(ProbabilityTheory.cdf
                                  (ProbabilityTheory.gaussianReal
                                    0 1))
                              z| ≤
                        A *
                            Real.exp
                              (-z / 2) *
                          ProbabilityTheory.thirdMomentSum
                            X μ) :
  ∃ C,
    0 < C ∧
      ∀ {ι : Type uι} {Ω : Type uΩ}
        [inst : Fintype ι]
        [inst_1 : MeasurableSpace Ω]
        (μ : MeasureTheory.Measure Ω)
        [MeasureTheory.IsProbabilityMeasure
            μ]
        (X : ι → Ω → ℝ),
        (∀ (i : ι), Measurable (X i)) →
          ProbabilityTheory.iIndepFun X
              μ →
            (∀ (i : ι),
                ∫ (ω : Ω), X i ω ∂μ = 0) →
              (∀ (i : ι),
                  MeasureTheory.MemLp
                    (X i) 3 μ) →
                ∑ i,
                      ProbabilityTheory.variance
                        (X i) μ =
                    1 →
                  ∀ (x : ℝ),
                    |↑(ProbabilityTheory.cdf
                                (MeasureTheory.Measure.map
                                  (fun
                                      ω =>
                                    ∑ i,
                                      X i
                                        ω)
                                  μ))
                            x -
                          ↑(ProbabilityTheory.cdf
                                (ProbabilityTheory.gaussianReal
                                  0 1))
                            x| ≤
                      (C *
                          ∑ i,
                            ∫ (ω : Ω),
                              |X i ω| ^
                                3 ∂μ) /
                        (1 + |x| ^ 3)
    A universal central estimate for one-sided truncated sums composes with the reduction into the
frozen scalar release theorem.

The positive-threshold argument follows Chen and Shao (2005), Section 6.2, printed pp. 44--48: the uniform theorem handles bounded x, the truncation comparison handles large jumps, and e^{-x/2}\le54/(1+x^3) for x\ge2. Reflection of the law supplies negative thresholds with the atom-safe (-x)+\varepsilon limit required by the closed-half-line CDF convention.

Theorem1.8.2
uses 1used by 0✓L∃∀N
Tagsprincipal-theoremsource-bikelissource-chen-shao-2005scalarfidelity-exact

Finite-third-moment nonuniform Berry--Esseen theorem. There is an absolute constant C>0 with the following property. Let I be a finite index set, let (\Omega,\mathcal F,\mathbb P) be a probability space, and let (X_i)_{i\in I} be independent measurable real-valued random variables satisfying \mathbb E X_i=0, \qquad \mathbb E|X_i|^3<\infty, \qquad \sum_{i\in I}\operatorname{Var}(X_i)=1. Writing W=\sum_{i\in I}X_i, \qquad \gamma=\sum_{i\in I}\mathbb E|X_i|^3, for every x\in\mathbb R one has \left|\Pr(W\le x)-\Phi(x)\right| \le \frac{C\gamma}{1+|x|^3}, where \Phi is the distribution function of a standard normal random variable.

Lean code for Theorem1.8.2●1 theorem
  • theoremdefined in ProbabilityApproximation/ChenShao/NonuniformBerryEsseen.lean
    complete
    theorem ProbabilityTheory.nonuniformBerryEsseen.{uι, uΩ} :
  ∃ C,
    0 < C ∧
      ∀ {ι : Type uι} {Ω : Type uΩ} [inst : Fintype ι]
        [inst_1 : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω)
        [MeasureTheory.IsProbabilityMeasure μ] (X : ι → Ω → ℝ),
        (∀ (i : ι), Measurable (X i)) →
          ProbabilityTheory.iIndepFun X μ →
            (∀ (i : ι), ∫ (ω : Ω), X i ω ∂μ = 0) →
              (∀ (i : ι), MeasureTheory.MemLp (X i) 3 μ) →
                ∑ i, ProbabilityTheory.variance (X i) μ = 1 →
                  ∀ (x : ℝ),
                    |↑(ProbabilityTheory.cdf
                                (MeasureTheory.Measure.map
                                  (fun ω => ∑ i, X i ω) μ))
                            x -
                          ↑(ProbabilityTheory.cdf
                                (ProbabilityTheory.gaussianReal 0 1))
                            x| ≤
                      (C * ∑ i, ∫ (ω : Ω), |X i ω| ^ 3 ∂μ) /
                        (1 + |x| ^ 3)
    theorem ProbabilityTheory.nonuniformBerryEsseen.{uι,
    uΩ} :
  ∃ C,
    0 < C ∧
      ∀ {ι : Type uι} {Ω : Type uΩ}
        [inst : Fintype ι]
        [inst_1 : MeasurableSpace Ω]
        (μ : MeasureTheory.Measure Ω)
        [MeasureTheory.IsProbabilityMeasure
            μ]
        (X : ι → Ω → ℝ),
        (∀ (i : ι), Measurable (X i)) →
          ProbabilityTheory.iIndepFun X
              μ →
            (∀ (i : ι),
                ∫ (ω : Ω), X i ω ∂μ = 0) →
              (∀ (i : ι),
                  MeasureTheory.MemLp
                    (X i) 3 μ) →
                ∑ i,
                      ProbabilityTheory.variance
                        (X i) μ =
                    1 →
                  ∀ (x : ℝ),
                    |↑(ProbabilityTheory.cdf
                                (MeasureTheory.Measure.map
                                  (fun
                                      ω =>
                                    ∑ i,
                                      X i
                                        ω)
                                  μ))
                            x -
                          ↑(ProbabilityTheory.cdf
                                (ProbabilityTheory.gaussianReal
                                  0 1))
                            x| ≤
                      (C *
                          ∑ i,
                            ∫ (ω : Ω),
                              |X i ω| ^
                                3 ∂μ) /
                        (1 + |x| ^ 3)
    Nonuniform Berry--Esseen theorem for independent centered finite families with total variance
one and finite absolute third moments. The constant is absolute: it is chosen before the index
type, probability space, family, and threshold. The scalar theorem specified in
`.agents/SPEC.md` is obtained from Chen--Shao (2005), Section 6 together with the standard
truncation and reflection reductions.

This finite-third-moment form is historically due to Bikelis. Theorem 2.2 and the discussion following it in Chen and Shao (2001), printed pp. 238--239, prove the stronger truncated-moment version. The proof formalized here follows Section 6.2 of Chen and Shao (2005), printed pp. 44--48. The universal central R_{2,2} estimate and the atom-safe reflection step are both included in the associated kernel-checked declaration.