Berry–Esseen Bounds for Independent Sums

1.7. The central nonuniform estimate🔗

Theorem1.7.1
Statement uses 3
Statement dependency previews
Preview
Lemma 1.6.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagsscalarcentral-estimatesource-chen-shao-2005fidelity-explicit-constant

Central exponential estimate for the upper-truncated sum. There is an absolute constant A=184+\frac32 C_{\mathrm{inc}}\ge0 such that, for every finite independent measurable family with \mathbb EX_i=0, \mathbb E|X_i|^3<\infty, and \sum_i\operatorname{Var}(X_i)=1, for every z\ge2, \left|\Pr(\bar W\le z)-\Phi(z)\right| \le A e^{-z/2}\gamma.

Lean code for Theorem1.7.1●3 declarations
  • defdefined in ProbabilityApproximation/ChenShao/NonuniformBerryEsseen.lean
    complete
    def ProbabilityTheory.upperTruncatedNonuniformConstant : ℝ
    def ProbabilityTheory.upperTruncatedNonuniformConstant :
  ℝ
    Explicit constant in the central exponential estimate for the one-sided truncated sum.
  • theoremdefined in ProbabilityApproximation/ChenShao/NonuniformBerryEsseen.lean
    complete
    theorem ProbabilityTheory.upperTruncatedNonuniformConstant_nonneg :
  0 ≤ ProbabilityTheory.upperTruncatedNonuniformConstant
    theorem ProbabilityTheory.upperTruncatedNonuniformConstant_nonneg :
  0 ≤
    ProbabilityTheory.upperTruncatedNonuniformConstant
  • theoremdefined in ProbabilityApproximation/ChenShao/NonuniformBerryEsseen.lean
    complete
    theorem ProbabilityTheory.abs_cdf_upperTruncatedSum_sub_gaussian_le_exp_thirdMomentSum.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : ι → Ω → ℝ} (hXmeas : ∀ (i : ι), Measurable (X i))
  (hX2 : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ)
  (h_indep : ProbabilityTheory.iIndepFun X μ)
  (h_mean : ∀ (i : ι), ∫ (ω : Ω), X i ω ∂μ = 0)
  (hvar : ∑ i, ProbabilityTheory.variance (X i) μ = 1)
  (h3 : ∀ (i : ι), MeasureTheory.Integrable (fun ω => |X i ω| ^ 3) μ)
  {z : ℝ} (hz : 2 ≤ z) :
  |↑(ProbabilityTheory.cdf
              (MeasureTheory.Measure.map
                (ProbabilityTheory.upperTruncatedSum X) μ))
          z -
        ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1))
          z| ≤
    ProbabilityTheory.upperTruncatedNonuniformConstant *
        Real.exp (-z / 2) *
      ProbabilityTheory.thirdMomentSum X μ
    theorem ProbabilityTheory.abs_cdf_upperTruncatedSum_sub_gaussian_le_exp_thirdMomentSum.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : ι → Ω → ℝ}
  (hXmeas : ∀ (i : ι), Measurable (X i))
  (hX2 :
    ∀ (i : ι),
      MeasureTheory.MemLp (X i) 2 μ)
  (h_indep :
    ProbabilityTheory.iIndepFun X μ)
  (h_mean :
    ∀ (i : ι), ∫ (ω : Ω), X i ω ∂μ = 0)
  (hvar :
    ∑ i,
        ProbabilityTheory.variance (X i)
          μ =
      1)
  (h3 :
    ∀ (i : ι),
      MeasureTheory.Integrable
        (fun ω => |X i ω| ^ 3) μ)
  {z : ℝ} (hz : 2 ≤ z) :
  |↑(ProbabilityTheory.cdf
              (MeasureTheory.Measure.map
                (ProbabilityTheory.upperTruncatedSum
                  X)
                μ))
          z -
        ↑(ProbabilityTheory.cdf
              (ProbabilityTheory.gaussianReal
                0 1))
          z| ≤
    ProbabilityTheory.upperTruncatedNonuniformConstant *
        Real.exp (-z / 2) *
      ProbabilityTheory.thirdMomentSum X μ
    Chen--Shao's one-sided truncated central estimate.  The four contributions are
`8` (`R₁`), `8` (`R₃`), `168` (`R₂,₁`), and
`(3 / 2) * steinProductIncrementConstant` (`R₂,₂`).

This is the finite-third-moment specialization of the conclusion assembled in Section 6.2, equations (6.16)--(6.24), of Chen and Shao (2005), printed pp. 45--48. The four explicit contributions are 8 from R_1, 8 from R_3, 168 from R_{2,1}, and (3/2)C_{\mathrm{inc}} from R_{2,2}.