Berry–Esseen Bounds for Independent Sums

1.4. One-sided truncation🔗

Proposition1.4.1
uses 0
Used by 2
Reverse dependency previews
Preview
Theorem 1.5.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsscalarupper-truncationsource-chen-shao-2005fidelity-explicit-constant

Comparison with one-sided truncation. Suppose \mathbb EX_i=0, \mathbb E|X_i|^3<\infty, \sum_i\operatorname{Var}(X_i)=1, and \gamma\le1. Put \bar X_i=X_i\mathbf1_{\{X_i\le1\}} and \bar W=\sum_i\bar X_i. For every z\ge2, \Pr(W>z) \le \Pr(\bar W>z)+\frac{45\gamma}{1+z^3}, and hence |\Pr(W\le z)-\Phi(z)| \le |\Pr(\bar W\le z)-\Phi(z)|+\frac{45\gamma}{1+z^3}.

Lean code for Proposition1.4.1●4 declarations
  • defdefined in ProbabilityApproximation/ChenShao/UpperTruncation.lean
    complete
    def ProbabilityTheory.upperTruncatedFamily.{u_1, u_2} {ι : Type u_1}
  {Ω : Type u_2} (X : ι → Ω → ℝ) : ι → Ω → ℝ
    def ProbabilityTheory.upperTruncatedFamily.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2}
  (X : ι → Ω → ℝ) : ι → Ω → ℝ
    The coordinatewise one-sided truncation `ξ̄ᵢ = ξᵢ 1_{ξᵢ ≤ 1}`.
  • defdefined in ProbabilityApproximation/ChenShao/UpperTruncation.lean
    complete
    def ProbabilityTheory.upperTruncatedSum.{u_1, u_2} {ι : Type u_1}
  {Ω : Type u_2} [Fintype ι] (X : ι → Ω → ℝ) : Ω → ℝ
    def ProbabilityTheory.upperTruncatedSum.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] (X : ι → Ω → ℝ) : Ω → ℝ
    The sum of the one-sided truncated family.
  • theoremdefined in ProbabilityApproximation/ChenShao/UpperTruncation.lean
    complete
    theorem ProbabilityTheory.measureReal_sumX_upperTail_le_upperTruncatedTail_add.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  [DecidableEq ι] {X : ι → Ω → ℝ} (hXmeas : ∀ (i : ι), Measurable (X i))
  (hX3 : ∀ (i : ι), MeasureTheory.MemLp (X i) 3 μ)
  (hX_indep : ProbabilityTheory.iIndepFun X μ)
  (hX_mean : ∀ (i : ι), ∫ (ω : Ω), X i ω ∂μ = 0)
  (hX_variance : ∑ i, ProbabilityTheory.variance (X i) μ = 1)
  (hgamma : ∑ i, ∫ (ω : Ω), |X i ω| ^ 3 ∂μ ≤ 1) {z : ℝ} (hz : 2 ≤ z) :
  μ.real {ω | z < ProbabilityTheory.sumX X ω} ≤
    μ.real {ω | z < ProbabilityTheory.upperTruncatedSum X ω} +
      (45 * ∑ i, ∫ (ω : Ω), |X i ω| ^ 3 ∂μ) / (1 + z ^ 3)
    theorem ProbabilityTheory.measureReal_sumX_upperTail_le_upperTruncatedTail_add.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  [DecidableEq ι] {X : ι → Ω → ℝ}
  (hXmeas : ∀ (i : ι), Measurable (X i))
  (hX3 :
    ∀ (i : ι),
      MeasureTheory.MemLp (X i) 3 μ)
  (hX_indep :
    ProbabilityTheory.iIndepFun X μ)
  (hX_mean :
    ∀ (i : ι), ∫ (ω : Ω), X i ω ∂μ = 0)
  (hX_variance :
    ∑ i,
        ProbabilityTheory.variance (X i)
          μ =
      1)
  (hgamma :
    ∑ i, ∫ (ω : Ω), |X i ω| ^ 3 ∂μ ≤ 1)
  {z : ℝ} (hz : 2 ≤ z) :
  μ.real
      {ω |
        z < ProbabilityTheory.sumX X ω} ≤
    μ.real
        {ω |
          z <
            ProbabilityTheory.upperTruncatedSum
              X ω} +
      (45 *
          ∑ i,
            ∫ (ω : Ω), |X i ω| ^ 3 ∂μ) /
        (1 + z ^ 3)
    Chen--Shao (2005), (6.13)--(6.14), with explicit constants: when the total third moment is at
most one and `z ≥ 2`, replacing every summand by its one-sided truncation changes the upper tail by
at most `45 γ / (1 + z³)`.
  • theoremdefined in ProbabilityApproximation/ChenShao/UpperTruncation.lean
    complete
    theorem ProbabilityTheory.abs_cdf_sumX_sub_gaussian_le_upperTruncated_add.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  [DecidableEq ι] {X : ι → Ω → ℝ} (hXmeas : ∀ (i : ι), Measurable (X i))
  (hX3 : ∀ (i : ι), MeasureTheory.MemLp (X i) 3 μ)
  (hX_indep : ProbabilityTheory.iIndepFun X μ)
  (hX_mean : ∀ (i : ι), ∫ (ω : Ω), X i ω ∂μ = 0)
  (hX_variance : ∑ i, ProbabilityTheory.variance (X i) μ = 1)
  (hgamma : ∑ i, ∫ (ω : Ω), |X i ω| ^ 3 ∂μ ≤ 1) {z : ℝ} (hz : 2 ≤ z) :
  |↑(ProbabilityTheory.cdf
              (MeasureTheory.Measure.map (ProbabilityTheory.sumX X) μ))
          z -
        ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1))
          z| ≤
    |↑(ProbabilityTheory.cdf
                (MeasureTheory.Measure.map
                  (ProbabilityTheory.upperTruncatedSum X) μ))
            z -
          ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1))
            z| +
      (45 * ∑ i, ∫ (ω : Ω), |X i ω| ^ 3 ∂μ) / (1 + z ^ 3)
    theorem ProbabilityTheory.abs_cdf_sumX_sub_gaussian_le_upperTruncated_add.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  [DecidableEq ι] {X : ι → Ω → ℝ}
  (hXmeas : ∀ (i : ι), Measurable (X i))
  (hX3 :
    ∀ (i : ι),
      MeasureTheory.MemLp (X i) 3 μ)
  (hX_indep :
    ProbabilityTheory.iIndepFun X μ)
  (hX_mean :
    ∀ (i : ι), ∫ (ω : Ω), X i ω ∂μ = 0)
  (hX_variance :
    ∑ i,
        ProbabilityTheory.variance (X i)
          μ =
      1)
  (hgamma :
    ∑ i, ∫ (ω : Ω), |X i ω| ^ 3 ∂μ ≤ 1)
  {z : ℝ} (hz : 2 ≤ z) :
  |↑(ProbabilityTheory.cdf
              (MeasureTheory.Measure.map
                (ProbabilityTheory.sumX X)
                μ))
          z -
        ↑(ProbabilityTheory.cdf
              (ProbabilityTheory.gaussianReal
                0 1))
          z| ≤
    |↑(ProbabilityTheory.cdf
                (MeasureTheory.Measure.map
                  (ProbabilityTheory.upperTruncatedSum
                    X)
                  μ))
            z -
          ↑(ProbabilityTheory.cdf
                (ProbabilityTheory.gaussianReal
                  0 1))
            z| +
      (45 *
          ∑ i,
            ∫ (ω : Ω), |X i ω| ^ 3 ∂μ) /
        (1 + z ^ 3)
    CDF form of the one-sided truncation comparison.  Any normal-approximation bound for the
upper-truncated sum transfers to the original sum with the explicit large-jump error.

The event decomposition is in Section 6.2, equations (6.13)--(6.14), of Chen and Shao (2005), printed p. 44. The displayed 45 is the explicit constant proved by the formal large-jump and leave-one-out estimates.