Berry–Esseen Bounds for Independent Sums

1.5. Stein exchange and residual decomposition🔗

Theorem1.5.1
Statement uses 2
Statement dependency previews
Preview
Definition 1.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagsscalarsteinupper-truncationsource-chen-shao-2005fidelity-exact-noncentered-form

Noncentered Stein exchange for the upper-truncated sum. Let Y_i=\bar X_i, \bar W=\sum_iY_i, and \bar W^{(i)}=\bar W-Y_i. Define K_i(t)=\mathbb E\!\left[|Y_i| \mathbf1_{\{\min(0,Y_i)\le t\le\max(0,Y_i)\}}\right]. If the X_i have finite second moments, then, for every z\in\mathbb R, \mathbb E[\bar W f_z(\bar W)] =\sum_i\int_{\mathbb R}\mathbb E[f'_z(\bar W^{(i)}+t)]K_i(t)\,dt +\sum_i\mathbb EY_i\,\mathbb E[f_z(\bar W^{(i)})].

Lean code for Theorem1.5.1●2 theorems
  • theoremdefined in ProbabilityApproximation/ChenShao/UpperTruncatedStein.lean
    complete
    theorem ProbabilityTheory.stein_identity_sum_leaveOneOut_noncentered.{u_1, u_2}
  {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {Y : ι → Ω → ℝ} [DecidableEq ι]
  (hY : ∀ (k : ι), MeasureTheory.MemLp (Y k) 2 μ)
  (hYmeas : ∀ (k : ι), Measurable (Y k))
  (h_indep : ProbabilityTheory.iIndepFun Y μ) (z : ℝ) :
  ∫ (ω : Ω),
      ProbabilityTheory.sumX Y ω *
        ProbabilityTheory.steinSolution z
          (ProbabilityTheory.sumX Y ω) ∂μ =
    ∑ i,
        ∫ (ω : Ω),
          ∫ (t : ℝ),
            ProbabilityTheory.kernelDensityFwd (Y i ω) t *
              ProbabilityTheory.steinSolutionDeriv z
                (ProbabilityTheory.leaveOneOut Y i ω + t) ∂μ +
      ∑ i,
        (∫ (ω : Ω), Y i ω ∂μ) *
          ∫ (ω : Ω),
            ProbabilityTheory.steinSolution z
              (ProbabilityTheory.leaveOneOut Y i ω) ∂μ
    theorem ProbabilityTheory.stein_identity_sum_leaveOneOut_noncentered.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {Y : ι → Ω → ℝ} [DecidableEq ι]
  (hY :
    ∀ (k : ι),
      MeasureTheory.MemLp (Y k) 2 μ)
  (hYmeas : ∀ (k : ι), Measurable (Y k))
  (h_indep :
    ProbabilityTheory.iIndepFun Y μ)
  (z : ℝ) :
  ∫ (ω : Ω),
      ProbabilityTheory.sumX Y ω *
        ProbabilityTheory.steinSolution z
          (ProbabilityTheory.sumX Y
            ω) ∂μ =
    ∑ i,
        ∫ (ω : Ω),
          ∫ (t : ℝ),
            ProbabilityTheory.kernelDensityFwd
                (Y i ω) t *
              ProbabilityTheory.steinSolutionDeriv
                z
                (ProbabilityTheory.leaveOneOut
                    Y i ω +
                  t) ∂μ +
      ∑ i,
        (∫ (ω : Ω), Y i ω ∂μ) *
          ∫ (ω : Ω),
            ProbabilityTheory.steinSolution
              z
              (ProbabilityTheory.leaveOneOut
                Y i ω) ∂μ
    Noncentered leave-one-out Stein exchange.  The second sum is the mean correction that vanishes
for centered coordinates but must be retained for one-sided truncations.
  • theoremdefined in ProbabilityApproximation/ChenShao/UpperTruncatedStein.lean
    complete
    theorem ProbabilityTheory.stein_identity_upperTruncatedSum.{u_1, u_2}
  {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  [DecidableEq ι] {X : ι → Ω → ℝ}
  (hX : ∀ (k : ι), MeasureTheory.MemLp (X k) 2 μ)
  (hXmeas : ∀ (k : ι), Measurable (X k))
  (h_indep : ProbabilityTheory.iIndepFun X μ) (z : ℝ) :
  ∫ (ω : Ω),
      ProbabilityTheory.upperTruncatedSum X ω *
        ProbabilityTheory.steinSolution z
          (ProbabilityTheory.upperTruncatedSum X ω) ∂μ =
    ∑ i,
        ∫ (ω : Ω),
          ∫ (t : ℝ),
            ProbabilityTheory.kernelDensityFwd
                (ProbabilityTheory.upperTruncatedFamily X i ω) t *
              ProbabilityTheory.steinSolutionDeriv z
                (ProbabilityTheory.leaveOneOut
                    (ProbabilityTheory.upperTruncatedFamily X) i ω +
                  t) ∂μ +
      ∑ i,
        (∫ (ω : Ω), ProbabilityTheory.upperTruncatedFamily X i ω ∂μ) *
          ∫ (ω : Ω),
            ProbabilityTheory.steinSolution z
              (ProbabilityTheory.leaveOneOut
                (ProbabilityTheory.upperTruncatedFamily X) i ω) ∂μ
    theorem ProbabilityTheory.stein_identity_upperTruncatedSum.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  [DecidableEq ι] {X : ι → Ω → ℝ}
  (hX :
    ∀ (k : ι),
      MeasureTheory.MemLp (X k) 2 μ)
  (hXmeas : ∀ (k : ι), Measurable (X k))
  (h_indep :
    ProbabilityTheory.iIndepFun X μ)
  (z : ℝ) :
  ∫ (ω : Ω),
      ProbabilityTheory.upperTruncatedSum
          X ω *
        ProbabilityTheory.steinSolution z
          (ProbabilityTheory.upperTruncatedSum
            X ω) ∂μ =
    ∑ i,
        ∫ (ω : Ω),
          ∫ (t : ℝ),
            ProbabilityTheory.kernelDensityFwd
                (ProbabilityTheory.upperTruncatedFamily
                  X i ω)
                t *
              ProbabilityTheory.steinSolutionDeriv
                z
                (ProbabilityTheory.leaveOneOut
                    (ProbabilityTheory.upperTruncatedFamily
                      X)
                    i ω +
                  t) ∂μ +
      ∑ i,
        (∫ (ω : Ω),
            ProbabilityTheory.upperTruncatedFamily
              X i ω ∂μ) *
          ∫ (ω : Ω),
            ProbabilityTheory.steinSolution
              z
              (ProbabilityTheory.leaveOneOut
                (ProbabilityTheory.upperTruncatedFamily
                  X)
                i ω) ∂μ
    Chen--Shao (2005), (6.16): the noncentered Stein exchange for the one-sided truncated family.

This is the noncentered form of the exchange used in Section 6.2, equation (6.16), of Chen and Shao (2005), printed p. 45. Retaining the second sum is essential: one-sided truncation generally makes \mathbb EY_i<0.

Theorem1.5.2
Statement uses 2
Statement dependency previews
Preview
Theorem 1.1.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Lemma 1.6.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsscalarsteinresidualssource-chen-shao-2005fidelity-exact

The R_1+R_2+R_3 identity. Set q=1-\sum_i\mathbb E\bar X_i^2,\qquad T=\sum_i\int_{\mathbb R}\mathbb E[f'_z(\bar W^{(i)}+t)]K_i(t)\,dt, and M=\sum_i\mathbb E\bar X_i\,\mathbb E[f_z(\bar W^{(i)})]. Define R_1=q\,\mathbb E f'_z(\bar W),\qquad R_2=(1-q)\mathbb E f'_z(\bar W)-T,\qquad R_3=-M. If \mathbb EX_i=0, \sum_i\operatorname{Var}(X_i)=1, and \gamma<\infty, then 0\le q\le\gamma; moreover, without the centering and variance assumptions needed for that bound, the exact identity \Pr(\bar W\le z)-\Phi(z)=R_1+R_2+R_3 holds whenever the coordinates have finite second moments.

Lean code for Theorem1.5.2●6 declarations
  • defdefined in ProbabilityApproximation/ChenShao/UpperTruncatedResidual.lean
    complete
    def ProbabilityTheory.upperTruncatedMissingSecondMoment.{u_1, u_2}
  {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [MeasurableSpace Ω]
  (X : ι → Ω → ℝ) (μ : MeasureTheory.Measure Ω) : ℝ
    def ProbabilityTheory.upperTruncatedMissingSecondMoment.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [MeasurableSpace Ω]
  (X : ι → Ω → ℝ)
  (μ : MeasureTheory.Measure Ω) : ℝ
    Second-moment mass removed by one-sided truncation.
  • defdefined in ProbabilityApproximation/ChenShao/UpperTruncatedResidual.lean
    complete
    def ProbabilityTheory.upperTruncatedR1.{u_1, u_2} {ι : Type u_1}
  {Ω : Type u_2} [Fintype ι] [MeasurableSpace Ω] (X : ι → Ω → ℝ)
  (μ : MeasureTheory.Measure Ω) (z : ℝ) : ℝ
    def ProbabilityTheory.upperTruncatedR1.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [MeasurableSpace Ω]
  (X : ι → Ω → ℝ)
  (μ : MeasureTheory.Measure Ω) (z : ℝ) :
  ℝ
    `R₁`: the second-moment mass removed by truncation, multiplied by `E f'_z(W̄)`.
  • defdefined in ProbabilityApproximation/ChenShao/UpperTruncatedResidual.lean
    complete
    def ProbabilityTheory.upperTruncatedR2.{u_1, u_2} {ι : Type u_1}
  {Ω : Type u_2} [Fintype ι] [MeasurableSpace Ω] [DecidableEq ι]
  (X : ι → Ω → ℝ) (μ : MeasureTheory.Measure Ω) (z : ℝ) : ℝ
    def ProbabilityTheory.upperTruncatedR2.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [MeasurableSpace Ω]
  [DecidableEq ι] (X : ι → Ω → ℝ)
  (μ : MeasureTheory.Measure Ω) (z : ℝ) :
  ℝ
    `R₂`: the difference between the retained kernel mass applied at the full truncated sum and
the leave-one-out kernel exchange.
  • defdefined in ProbabilityApproximation/ChenShao/UpperTruncatedResidual.lean
    complete
    def ProbabilityTheory.upperTruncatedR3.{u_1, u_2} {ι : Type u_1}
  {Ω : Type u_2} [Fintype ι] [MeasurableSpace Ω] [DecidableEq ι]
  (X : ι → Ω → ℝ) (μ : MeasureTheory.Measure Ω) (z : ℝ) : ℝ
    def ProbabilityTheory.upperTruncatedR3.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [MeasurableSpace Ω]
  [DecidableEq ι] (X : ι → Ω → ℝ)
  (μ : MeasureTheory.Measure Ω) (z : ℝ) :
  ℝ
    `R₃`: the sign-adjusted noncentered mean correction.
  • theoremdefined in ProbabilityApproximation/ChenShao/UpperTruncatedResidual.lean
    complete
    theorem ProbabilityTheory.upperTruncatedMissingSecondMoment_le_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_mean : ∀ (i : ι), ∫ (ω : Ω), X i ω ∂μ = 0)
  (hvar : ∑ i, ProbabilityTheory.variance (X i) μ = 1)
  (h3 : ∀ (i : ι), MeasureTheory.Integrable (fun ω => |X i ω| ^ 3) μ) :
  ProbabilityTheory.upperTruncatedMissingSecondMoment X μ ≤
    ProbabilityTheory.thirdMomentSum X μ
    theorem ProbabilityTheory.upperTruncatedMissingSecondMoment_le_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_mean :
    ∀ (i : ι), ∫ (ω : Ω), X i ω ∂μ = 0)
  (hvar :
    ∑ i,
        ProbabilityTheory.variance (X i)
          μ =
      1)
  (h3 :
    ∀ (i : ι),
      MeasureTheory.Integrable
        (fun ω => |X i ω| ^ 3) μ) :
  ProbabilityTheory.upperTruncatedMissingSecondMoment
      X μ ≤
    ProbabilityTheory.thirdMomentSum X μ
  • theoremdefined in ProbabilityApproximation/ChenShao/UpperTruncatedResidual.lean
    complete
    theorem ProbabilityTheory.cdf_upperTruncatedSum_sub_gaussian_eq_R1_add_R2_add_R3.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : ι → Ω → ℝ} [DecidableEq ι] (hXmeas : ∀ (i : ι), Measurable (X i))
  (hX2 : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ)
  (h_indep : ProbabilityTheory.iIndepFun X μ) (z : ℝ) :
  ↑(ProbabilityTheory.cdf
            (MeasureTheory.Measure.map
              (ProbabilityTheory.upperTruncatedSum X) μ))
        z -
      ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) z =
    ProbabilityTheory.upperTruncatedR1 X μ z +
        ProbabilityTheory.upperTruncatedR2 X μ z +
      ProbabilityTheory.upperTruncatedR3 X μ z
    theorem ProbabilityTheory.cdf_upperTruncatedSum_sub_gaussian_eq_R1_add_R2_add_R3.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : ι → Ω → ℝ} [DecidableEq ι]
  (hXmeas : ∀ (i : ι), Measurable (X i))
  (hX2 :
    ∀ (i : ι),
      MeasureTheory.MemLp (X i) 2 μ)
  (h_indep :
    ProbabilityTheory.iIndepFun X μ)
  (z : ℝ) :
  ↑(ProbabilityTheory.cdf
            (MeasureTheory.Measure.map
              (ProbabilityTheory.upperTruncatedSum
                X)
              μ))
        z -
      ↑(ProbabilityTheory.cdf
            (ProbabilityTheory.gaussianReal
              0 1))
        z =
    ProbabilityTheory.upperTruncatedR1 X μ
          z +
        ProbabilityTheory.upperTruncatedR2
          X μ z +
      ProbabilityTheory.upperTruncatedR3 X
        μ z
    Exact Chen--Shao (2005), (6.16), residual identity.

This is Section 6.2, equation (6.16), of Chen and Shao (2005), printed p. 45, with the missing second-moment mass and nonzero truncated means made explicit.