Berry–Esseen Bounds for Independent Sums

1.6. Estimates for the residual terms🔗

Lemma1.6.1
Statement uses 2
Statement dependency previews
Preview
Lemma 1.3.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagsscalarsteinresidualssource-chen-shao-2005fidelity-explicit-constant

Exponential bounds for R_1 and R_3. Under the centered, unit-total-variance, finite-third-moment hypotheses above, for every z\ge2, |R_1|\le8e^{-z/2}\gamma,\qquad |R_3|\le8e^{-z/2}\gamma.

Lean code for Lemma1.6.1●2 theorems
  • theoremdefined in ProbabilityApproximation/ChenShao/UpperTruncatedSteinBounds.lean
    complete
    theorem ProbabilityTheory.abs_upperTruncatedR1_le.{u_1, u_2} {Ω : Type u_1}
  [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} [Fintype ι]
  [DecidableEq ι] {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.upperTruncatedR1 X μ z| ≤
    8 * Real.exp (-z / 2) * ProbabilityTheory.thirdMomentSum X μ
    theorem ProbabilityTheory.abs_upperTruncatedR1_le.{u_1,
    u_2}
  {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {ι : Type u_2} [Fintype ι]
  [DecidableEq ι] {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.upperTruncatedR1 X μ
        z| ≤
    8 * Real.exp (-z / 2) *
      ProbabilityTheory.thirdMomentSum X μ
    Chen--Shao (2005), (6.17), with explicit constant `8`.
  • theoremdefined in ProbabilityApproximation/ChenShao/UpperTruncatedSteinBounds.lean
    complete
    theorem ProbabilityTheory.abs_upperTruncatedR3_le.{u_1, u_2} {Ω : Type u_1}
  [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} [Fintype ι]
  [DecidableEq ι] {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.upperTruncatedR3 X μ z| ≤
    8 * Real.exp (-z / 2) * ProbabilityTheory.thirdMomentSum X μ
    theorem ProbabilityTheory.abs_upperTruncatedR3_le.{u_1,
    u_2}
  {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {ι : Type u_2} [Fintype ι]
  [DecidableEq ι] {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.upperTruncatedR3 X μ
        z| ≤
    8 * Real.exp (-z / 2) *
      ProbabilityTheory.thirdMomentSum X μ
    Chen--Shao (2005), (6.18), with explicit constant `8`.

These are the explicit formal versions of Chen and Shao (2005), Section 6.2, equations (6.17)--(6.18), printed p. 45. The source records an unspecified absolute constant; the kernel-checked proof obtains 8 in both inequalities.

Theorem1.6.2
uses 1
Used by 2
Reverse dependency previews
Preview
Lemma 1.6.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsscalarsteinexpected-kernelsource-chen-shao-2005fidelity-exact

Deterministic expected-kernel representation and split of R_2. For K_i(t)=\mathbb E[|\bar X_i|\mathbf1_{\{\min(0,\bar X_i)\le t\le \max(0,\bar X_i)\}}], one has \int_{\mathbb R}K_i(t)\,dt=\mathbb E\bar X_i^2. Writing F=\mathbb E f'_z(\bar W), the residual is R_2=\sum_i\int_{\mathbb R} \bigl(F-\mathbb E f'_z(\bar W^{(i)}+t)\bigr)K_i(t)\,dt. Using f'_z(w)=wf_z(w)+\mathbf1_{\{w\le z\}}-\Phi(z) splits this exactly as R_2=R_{2,1}+R_{2,2}, where R_{2,1}=\sum_i\int \bigl(\Pr(\bar W\le z)-\Pr(\bar W^{(i)}+t\le z)\bigr)K_i(t)\,dt and R_{2,2}=\sum_i\int \bigl(\mathbb E[\bar Wf_z(\bar W)] -\mathbb E[(\bar W^{(i)}+t)f_z(\bar W^{(i)}+t)]\bigr)K_i(t)\,dt.

Lean code for Theorem1.6.2●6 declarations
  • defdefined in ProbabilityApproximation/ChenShao/UpperTruncatedExpectedKernel.lean
    complete
    def ProbabilityTheory.upperTruncatedExpectedKernel.{u_1, u_2} {ι : Type u_1}
  {Ω : Type u_2} [MeasurableSpace Ω] (X : ι → Ω → ℝ)
  (μ : MeasureTheory.Measure Ω) (i : ι) (t : ℝ) : ℝ
    def ProbabilityTheory.upperTruncatedExpectedKernel.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [MeasurableSpace Ω] (X : ι → Ω → ℝ)
  (μ : MeasureTheory.Measure Ω) (i : ι)
  (t : ℝ) : ℝ
    The expected forward kernel of the one-sided truncated coordinate `X̄ᵢ`.
  • theoremdefined in ProbabilityApproximation/ChenShao/UpperTruncatedExpectedKernel.lean
    complete
    theorem ProbabilityTheory.integral_upperTruncatedExpectedKernel.{u_1, u_2}
  {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : ι → Ω → ℝ} [DecidableEq ι]
  (hX2 : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ)
  (hXmeas : ∀ (i : ι), Measurable (X i)) (i : ι) :
  ∫ (t : ℝ), ProbabilityTheory.upperTruncatedExpectedKernel X μ i t =
    ∫ (ω : Ω), ProbabilityTheory.upperTruncatedFamily X i ω ^ 2 ∂μ
    theorem ProbabilityTheory.integral_upperTruncatedExpectedKernel.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : ι → Ω → ℝ} [DecidableEq ι]
  (hX2 :
    ∀ (i : ι),
      MeasureTheory.MemLp (X i) 2 μ)
  (hXmeas : ∀ (i : ι), Measurable (X i))
  (i : ι) :
  ∫ (t : ℝ),
      ProbabilityTheory.upperTruncatedExpectedKernel
        X μ i t =
    ∫ (ω : Ω),
      ProbabilityTheory.upperTruncatedFamily
          X i ω ^
        2 ∂μ
  • theoremdefined in ProbabilityApproximation/ChenShao/UpperTruncatedExpectedKernel.lean
    complete
    theorem ProbabilityTheory.upperTruncatedR2_eq_sum_integral_expectedKernel.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : ι → Ω → ℝ} [DecidableEq ι]
  (hX2 : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ)
  (hXmeas : ∀ (i : ι), Measurable (X i))
  (h_indep : ProbabilityTheory.iIndepFun X μ) (z : ℝ) :
  ProbabilityTheory.upperTruncatedR2 X μ z =
    ∑ i,
      ∫ (t : ℝ),
        (∫ (ω : Ω),
              ProbabilityTheory.steinSolutionDeriv z
                (ProbabilityTheory.upperTruncatedSum X ω) ∂μ -
            ∫ (ω : Ω),
              ProbabilityTheory.steinSolutionDeriv z
                (ProbabilityTheory.leaveOneOut
                    (ProbabilityTheory.upperTruncatedFamily X) i ω +
                  t) ∂μ) *
          ProbabilityTheory.upperTruncatedExpectedKernel X μ i t
    theorem ProbabilityTheory.upperTruncatedR2_eq_sum_integral_expectedKernel.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : ι → Ω → ℝ} [DecidableEq ι]
  (hX2 :
    ∀ (i : ι),
      MeasureTheory.MemLp (X i) 2 μ)
  (hXmeas : ∀ (i : ι), Measurable (X i))
  (h_indep :
    ProbabilityTheory.iIndepFun X μ)
  (z : ℝ) :
  ProbabilityTheory.upperTruncatedR2 X μ
      z =
    ∑ i,
      ∫ (t : ℝ),
        (∫ (ω : Ω),
              ProbabilityTheory.steinSolutionDeriv
                z
                (ProbabilityTheory.upperTruncatedSum
                  X ω) ∂μ -
            ∫ (ω : Ω),
              ProbabilityTheory.steinSolutionDeriv
                z
                (ProbabilityTheory.leaveOneOut
                    (ProbabilityTheory.upperTruncatedFamily
                      X)
                    i ω +
                  t) ∂μ) *
          ProbabilityTheory.upperTruncatedExpectedKernel
            X μ i t
    Deterministic expected-kernel form of `R₂`.
  • defdefined in ProbabilityApproximation/ChenShao/UpperTruncatedExpectedKernel.lean
    complete
    def ProbabilityTheory.upperTruncatedR21.{u_1, u_2} {ι : Type u_1}
  {Ω : Type u_2} [Fintype ι] [MeasurableSpace Ω] [DecidableEq ι]
  (X : ι → Ω → ℝ) (μ : MeasureTheory.Measure Ω) (z : ℝ) : ℝ
    def ProbabilityTheory.upperTruncatedR21.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [MeasurableSpace Ω]
  [DecidableEq ι] (X : ι → Ω → ℝ)
  (μ : MeasureTheory.Measure Ω) (z : ℝ) :
  ℝ
    `R₂,₁`: the indicator jump in the expected-kernel representation of `R₂`.
  • defdefined in ProbabilityApproximation/ChenShao/UpperTruncatedExpectedKernel.lean
    complete
    def ProbabilityTheory.upperTruncatedR22.{u_1, u_2} {ι : Type u_1}
  {Ω : Type u_2} [Fintype ι] [MeasurableSpace Ω] [DecidableEq ι]
  (X : ι → Ω → ℝ) (μ : MeasureTheory.Measure Ω) (z : ℝ) : ℝ
    def ProbabilityTheory.upperTruncatedR22.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [MeasurableSpace Ω]
  [DecidableEq ι] (X : ι → Ω → ℝ)
  (μ : MeasureTheory.Measure Ω) (z : ℝ) :
  ℝ
    `R₂,₂`: the increment of `w ↦ w f_z(w)` in the expected-kernel representation of `R₂`.
  • theoremdefined in ProbabilityApproximation/ChenShao/UpperTruncatedExpectedKernel.lean
    complete
    theorem ProbabilityTheory.upperTruncatedR2_eq_R21_add_R22.{u_1, u_2}
  {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : ι → Ω → ℝ} [DecidableEq ι]
  (hX2 : ∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ)
  (hXmeas : ∀ (i : ι), Measurable (X i))
  (h_indep : ProbabilityTheory.iIndepFun X μ) (z : ℝ) :
  ProbabilityTheory.upperTruncatedR2 X μ z =
    ProbabilityTheory.upperTruncatedR21 X μ z +
      ProbabilityTheory.upperTruncatedR22 X μ z
    theorem ProbabilityTheory.upperTruncatedR2_eq_R21_add_R22.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : ι → Ω → ℝ} [DecidableEq ι]
  (hX2 :
    ∀ (i : ι),
      MeasureTheory.MemLp (X i) 2 μ)
  (hXmeas : ∀ (i : ι), Measurable (X i))
  (h_indep :
    ProbabilityTheory.iIndepFun X μ)
  (z : ℝ) :
  ProbabilityTheory.upperTruncatedR2 X μ
      z =
    ProbabilityTheory.upperTruncatedR21 X
        μ z +
      ProbabilityTheory.upperTruncatedR22
        X μ z
    Exact Chen--Shao split `R₂ = R₂,₁ + R₂,₂`, with the Gaussian-CDF constant canceled between
the two derivative expectations.

This is the split immediately after equation (6.18) in Chen and Shao (2005), Section 6.2, printed pp. 45--46. Fubini and leave-one-out independence supply the deterministic kernels used in the formal statement.

Lemma1.6.3
Statement uses 2
Statement dependency previews
Preview
Proposition 1.3.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagsscalarconcentrationresidualssource-chen-shao-2005fidelity-explicit-constant

Indicator part of R_2. Under the centered, unit-total-variance, finite-third-moment hypotheses, for every z\in\mathbb R, |R_{2,1}|\le168e^{-z/2}\gamma.

Lean code for Lemma1.6.3●1 theorem
  • theoremdefined in ProbabilityApproximation/ChenShao/UpperTruncatedIndicator.lean
    complete
    theorem ProbabilityTheory.abs_upperTruncatedR21_le_exp_thirdMomentSum.{u_1, u_2}
  {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : ι → Ω → ℝ} [DecidableEq ι] (hXmeas : ∀ (i : ι), Measurable (X i))
  (h_indep : ProbabilityTheory.iIndepFun X μ)
  (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) μ)
  (z : ℝ) :
  |ProbabilityTheory.upperTruncatedR21 X μ z| ≤
    168 * Real.exp (-z / 2) * ProbabilityTheory.thirdMomentSum X μ
    theorem ProbabilityTheory.abs_upperTruncatedR21_le_exp_thirdMomentSum.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : ι → Ω → ℝ} [DecidableEq ι]
  (hXmeas : ∀ (i : ι), Measurable (X i))
  (h_indep :
    ProbabilityTheory.iIndepFun X μ)
  (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) μ)
  (z : ℝ) :
  |ProbabilityTheory.upperTruncatedR21 X μ
        z| ≤
    168 * Real.exp (-z / 2) *
      ProbabilityTheory.thirdMomentSum X μ
    Chen--Shao (2005), Section 6: the indicator residual has exponential decay with an explicit
absolute constant.  The proof in fact holds for every `z`; in particular it supplies the `z ≥ 2`
branch used by the upper-truncated nonuniform theorem.

The argument formalizes the two orientations of the conditional interval estimate in Section 6.2, equations (6.19) and (6.21)--(6.22), of Chen and Shao (2005), printed p. 46. The source uses an unspecified constant; the formal concentration constants yield 168.

Lemma1.6.4
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 1✓L∃∀N
Tagsscalarsteinresidualssource-chen-shao-2005fidelity-explicit-constant

Stein-product increment estimate. Let g_z(w)=(wf_z(w))' away from z, with the everywhere-defined representative obtained from the two one-sided formulas. There is an explicit absolute constant C_{\mathrm{inc}}>0 such that, under the centered and unit-total-variance hypotheses, for every i\in I, z\ge2, and s,t\le1, \left|\mathbb E\bigl[(\bar W^{(i)}+t)f_z(\bar W^{(i)}+t) -(\bar W^{(i)}+s)f_z(\bar W^{(i)}+s)\bigr]\right| \le C_{\mathrm{inc}}e^{-z/2}(|s|+|t|). In addition, bf_z(b)-af_z(a)=\int_a^b g_z(u)\,du for every a,b\in\mathbb R, including intervals crossing z.

Lean code for Lemma1.6.4●4 declarations
  • defdefined in ProbabilityApproximation/ChenShao/SteinProductDerivative.lean
    complete
    def ProbabilityTheory.steinProductDeriv (z w : ℝ) : ℝ
    def ProbabilityTheory.steinProductDeriv
  (z w : ℝ) : ℝ
    The pointwise extension of `(w * f_z(w))'` across the unique possible kink `w = z`.
  • theoremdefined in ProbabilityApproximation/ChenShao/SteinProductDerivative.lean
    complete
    theorem ProbabilityTheory.mul_steinSolution_sub_eq_integral_steinProductDeriv
  (z a b : ℝ) :
  b * ProbabilityTheory.steinSolution z b -
      a * ProbabilityTheory.steinSolution z a =
    ∫ (w : ℝ) in a..b, ProbabilityTheory.steinProductDeriv z w
    theorem ProbabilityTheory.mul_steinSolution_sub_eq_integral_steinProductDeriv
  (z a b : ℝ) :
  b *
        ProbabilityTheory.steinSolution z
          b -
      a *
        ProbabilityTheory.steinSolution z
          a =
    ∫ (w : ℝ) in a..b,
      ProbabilityTheory.steinProductDeriv
        z w
    FTC for `w f_z(w)`, valid even when the interval crosses the single kink `z`.
  • defdefined in ProbabilityApproximation/ChenShao/SteinProductIncrement.lean
    complete
    def ProbabilityTheory.steinProductIncrementConstant : ℝ
    def ProbabilityTheory.steinProductIncrementConstant :
  ℝ
    Explicit absolute constant for the truncated Stein-product increment estimate.
  • theoremdefined in ProbabilityApproximation/ChenShao/SteinProductIncrement.lean
    complete
    theorem ProbabilityTheory.abs_integral_steinProductIncrement_upperTruncated_le_abs_add.{u_1,
    u_2}
  {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} [Fintype ι]
  [DecidableEq ι] {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) (i : ι)
  {z s t : ℝ} (hz : 2 ≤ z) (hs : s ≤ 1) (ht : t ≤ 1) :
  |∫ (ω : Ω),
        ProbabilityTheory.steinProductIncrement z
          (ProbabilityTheory.leaveOneOut
            (ProbabilityTheory.upperTruncatedFamily X) i)
          s t ω ∂μ| ≤
    ProbabilityTheory.steinProductIncrementConstant *
        Real.exp (-z / 2) *
      (|s| + |t|)
    theorem ProbabilityTheory.abs_integral_steinProductIncrement_upperTruncated_le_abs_add.{u_1,
    u_2}
  {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {ι : Type u_2} [Fintype ι]
  [DecidableEq ι] {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)
  (i : ι) {z s t : ℝ} (hz : 2 ≤ z)
  (hs : s ≤ 1) (ht : t ≤ 1) :
  |∫ (ω : Ω),
        ProbabilityTheory.steinProductIncrement
          z
          (ProbabilityTheory.leaveOneOut
            (ProbabilityTheory.upperTruncatedFamily
              X)
            i)
          s t ω ∂μ| ≤
    ProbabilityTheory.steinProductIncrementConstant *
        Real.exp (-z / 2) *
      (|s| + |t|)
    Orientation-free absolute-value form of the truncated Stein-product increment estimate.

This is Lemma 6.5 and equations (6.23)--(6.24) of Chen and Shao (2005), printed pp. 46--48. The formal constant is C_{\mathrm{inc}}=C_{\mathrm{low}}+3(\sqrt{2\pi}/2+2)e^2e^{e^2-3}.

Lemma1.6.5
Statement uses 2
Statement dependency previews
Preview
Theorem 1.6.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagsscalarsteinresidualssource-chen-shao-2005fidelity-explicit-constant

Stein-product part of R_2. Leave-one-out independence gives, for every i, \mathbb E[\bar Wf_z(\bar W)] =\mathbb E_{\bar X_i}\mathbb E_{\bar W^{(i)}} [(\bar W^{(i)}+\bar X_i)f_z(\bar W^{(i)}+\bar X_i)]. Consequently, under the centered, unit-total-variance, finite-third-moment hypotheses and for every z\ge2, |R_{2,2}|\le \frac32 C_{\mathrm{inc}}e^{-z/2}\gamma.

Lean code for Lemma1.6.5●2 theorems
  • theoremdefined in ProbabilityApproximation/ChenShao/UpperTruncatedProduct.lean
    complete
    theorem ProbabilityTheory.integral_upperTruncatedSteinProduct_eq_iterated_leaveOneOut.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [DecidableEq ι]
  [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ}
  (hXmeas : ∀ (i : ι), Measurable (X i))
  (h_indep : ProbabilityTheory.iIndepFun X μ) (i : ι) (z : ℝ) :
  ∫ (ω : Ω),
      ProbabilityTheory.upperTruncatedSum X ω *
        ProbabilityTheory.steinSolution z
          (ProbabilityTheory.upperTruncatedSum X ω) ∂μ =
    ∫ (ξ : Ω),
      ∫ (ω : Ω),
        (ProbabilityTheory.leaveOneOut
              (ProbabilityTheory.upperTruncatedFamily X) i ω +
            ProbabilityTheory.upperTruncatedFamily X i ξ) *
          ProbabilityTheory.steinSolution z
            (ProbabilityTheory.leaveOneOut
                (ProbabilityTheory.upperTruncatedFamily X) i ω +
              ProbabilityTheory.upperTruncatedFamily X i ξ) ∂μ ∂μ
    theorem ProbabilityTheory.integral_upperTruncatedSteinProduct_eq_iterated_leaveOneOut.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [DecidableEq ι]
  [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : ι → Ω → ℝ}
  (hXmeas : ∀ (i : ι), Measurable (X i))
  (h_indep :
    ProbabilityTheory.iIndepFun X μ)
  (i : ι) (z : ℝ) :
  ∫ (ω : Ω),
      ProbabilityTheory.upperTruncatedSum
          X ω *
        ProbabilityTheory.steinSolution z
          (ProbabilityTheory.upperTruncatedSum
            X ω) ∂μ =
    ∫ (ξ : Ω),
      ∫ (ω : Ω),
        (ProbabilityTheory.leaveOneOut
              (ProbabilityTheory.upperTruncatedFamily
                X)
              i ω +
            ProbabilityTheory.upperTruncatedFamily
              X i ξ) *
          ProbabilityTheory.steinSolution
            z
            (ProbabilityTheory.leaveOneOut
                (ProbabilityTheory.upperTruncatedFamily
                  X)
                i ω +
              ProbabilityTheory.upperTruncatedFamily
                X i ξ) ∂μ ∂μ
    Leave-one-out independence factors the Stein product of the full upper-truncated sum into an
outer coordinate integral and an inner leave-one-out integral.
  • theoremdefined in ProbabilityApproximation/ChenShao/UpperTruncatedProduct.lean
    complete
    theorem ProbabilityTheory.abs_upperTruncatedR22_le_exp_thirdMomentSum.{u_1, u_2}
  {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [DecidableEq ι]
  [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.upperTruncatedR22 X μ z| ≤
    3 / 2 * ProbabilityTheory.steinProductIncrementConstant *
        Real.exp (-z / 2) *
      ProbabilityTheory.thirdMomentSum X μ
    theorem ProbabilityTheory.abs_upperTruncatedR22_le_exp_thirdMomentSum.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [DecidableEq ι]
  [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.upperTruncatedR22 X μ
        z| ≤
    3 / 2 *
          ProbabilityTheory.steinProductIncrementConstant *
        Real.exp (-z / 2) *
      ProbabilityTheory.thirdMomentSum X μ
    Chen--Shao (2005), equation (6.20): the Stein-product component of `R₂` decays
exponentially.  The explicit factor `3 / 2` records the two exact expected-kernel moment
contributions rather than absorbing them into an unspecified constant.

This completes the integration step in Chen and Shao (2005), Section 6.2, equation (6.20), printed p. 46. The factor 3/2 is the sum of the exact first absolute moment of the expected kernel, 1/2, and the product of its total mass with the coordinate first moment, bounded by 1.