Berry–Esseen Bounds for Independent Sums

1.1. The half-line Stein equation🔗

Definition1.1.1

uses 0

Used by 3

Reverse dependency previews

Preview

Theorem 1.1.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagsscalarsteinsource-chen-shao-2005fidelity-exact

Indicator Stein solution. For z,w\in\mathbb R, put h_z(w)=\mathbf 1_{\{w\le z\}}-\Phi(z),\qquad f_z(w)=e^{w^2/2}\int_{-\infty}^{w}h_z(t)e^{-t^2/2}\,dt. The function f_z is continuous and nonnegative. At every w\ne z it is differentiable and satisfies f'_z(w)-wf_z(w)=h_z(w). With the everywhere-defined representative f'_z(w)=wf_z(w)+h_z(w), one has, for every z,w\in\mathbb R, |wf_z(w)|\le1,\qquad |f'_z(w)|\le2, \qquad 0\le f_z(w)\le\frac{\sqrt{2\pi}}2.

Lean code for Definition1.1.1●7 declarations

defdefined in ProbabilityApproximation/Stein/IndicatorSolution.lean

complete

def ProbabilityTheory.steinSolution (z w : ℝ) : ℝ

def ProbabilityTheory.steinSolution
  (z w : ℝ) : ℝ

Indicator Stein solution:
`f_z(w) = e^{w²/2} ∫_{-∞}^w (1_{x≤z} - Φ(z)) e^{-x²/2} dx`.

defdefined in ProbabilityApproximation/Stein/IndicatorSolution.lean

complete

def ProbabilityTheory.steinSolutionDeriv (z w : ℝ) : ℝ

def ProbabilityTheory.steinSolutionDeriv
  (z w : ℝ) : ℝ

Pointwise extension of the Stein derivative (classical for `w ≠ z`).

theoremdefined in ProbabilityApproximation/Stein/IndicatorSolution.lean

complete

theorem ProbabilityTheory.stein_equation (z w : ℝ) (hw : w ≠ z) :
  deriv (ProbabilityTheory.steinSolution z) w -
      w * ProbabilityTheory.steinSolution z w =
    ProbabilityTheory.steinIntegrand z w

theorem ProbabilityTheory.stein_equation (z w : ℝ)
  (hw : w ≠ z) :
  deriv
        (ProbabilityTheory.steinSolution
          z)
        w -
      w *
        ProbabilityTheory.steinSolution z
          w =
    ProbabilityTheory.steinIntegrand z w

theoremdefined in ProbabilityApproximation/Stein/IndicatorSolution.lean

complete

theorem ProbabilityTheory.steinSolution_nonneg (z w : ℝ) :
  0 ≤ ProbabilityTheory.steinSolution z w

theorem ProbabilityTheory.steinSolution_nonneg
  (z w : ℝ) :
  0 ≤ ProbabilityTheory.steinSolution z w

The indicator Stein solution is nonnegative.

theoremdefined in ProbabilityApproximation/Stein/IndicatorSolution.lean

complete

theorem ProbabilityTheory.abs_mul_steinSolution_le_one (z w : ℝ) :
  |w * ProbabilityTheory.steinSolution z w| ≤ 1

theorem ProbabilityTheory.abs_mul_steinSolution_le_one
  (z w : ℝ) :
  |w *
        ProbabilityTheory.steinSolution z
          w| ≤
    1

Full bound `|w · f_z(w)| ≤ 1` for all real `w, z`.

theoremdefined in ProbabilityApproximation/Stein/IndicatorSolution.lean

complete

theorem ProbabilityTheory.abs_steinSolutionDeriv_le_two (z w : ℝ) :
  |ProbabilityTheory.steinSolutionDeriv z w| ≤ 2

theorem ProbabilityTheory.abs_steinSolutionDeriv_le_two
  (z w : ℝ) :
  |ProbabilityTheory.steinSolutionDeriv z
        w| ≤
    2

Bound `|steinSolutionDeriv z w| ≤ 2` (coarse; sharpens to 1 with lower mills).

theoremdefined in ProbabilityApproximation/Stein/IndicatorSolution.lean

complete

theorem ProbabilityTheory.abs_steinSolution_le_sqrt_two_pi_div_two (z w : ℝ) :
  |ProbabilityTheory.steinSolution z w| ≤ √(2 * Real.pi) / 2

theorem ProbabilityTheory.abs_steinSolution_le_sqrt_two_pi_div_two
  (z w : ℝ) :
  |ProbabilityTheory.steinSolution z w| ≤
    √(2 * Real.pi) / 2

Bound `|f_z(w)| ≤ √(2π)/2`.

This is the half-line specialization of Chen and Shao (2005), Section 2.2, Lemma 2.2 and equations (2.3)--(2.9), printed pp. 10--11. The displayed integral fixes the same (-\infty,z] convention as the library CDF.

Theorem1.1.2

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 1.5.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagsscalarsteinnonuniformsource-chen-shao-2005fidelity-exact-tail-majorants

Tail-sensitive derivative bounds and the integrated Stein equation. Write \Phi for the standard Gaussian distribution function. The derivative of the indicator Stein solution has the two exact forms \begin{aligned} f'_x(w) &=(1-\Phi(x)) \left(1+w\sqrt{2\pi}\,e^{w^2/2}\Phi(w)\right), &&w\le x,\\ f'_x(w) &=\Phi(x) \left(w\sqrt{2\pi}\,e^{w^2/2}(1-\Phi(w))-1\right), &&x<w. \end{aligned} In particular, if x>0 and w\le0, then |f'_x(w)|\le2(1-\Phi(x)), while, if x\ge2 and |w|\le x/2, then |f'_x(w)| \le(1-\Phi(x)) \left(1+\sqrt{2\pi}\,\frac x2 e^{x^2/8}\right). Finally, for a finite sum W=\sum_iX_i of measurable square-integrable variables, \Pr(W\le x)-\Phi(x) =\mathbb E f'_x(W)-\mathbb E[Wf_x(W)].

Lean code for Theorem1.1.2●5 theorems

theoremdefined in ProbabilityApproximation/ChenShao/NonuniformStein.lean

complete

theorem ProbabilityTheory.steinSolutionDeriv_of_le {x w : ℝ} (hw : w ≤ x) :
  ProbabilityTheory.steinSolutionDeriv x w =
    (1 -
        ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1))
          x) *
      (1 +
        w * √(2 * Real.pi) * Real.exp (w ^ 2 / 2) *
          ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1))
            w)

theorem ProbabilityTheory.steinSolutionDeriv_of_le
  {x w : ℝ} (hw : w ≤ x) :
  ProbabilityTheory.steinSolutionDeriv x
      w =
    (1 -
        ↑(ProbabilityTheory.cdf
              (ProbabilityTheory.gaussianReal
                0 1))
          x) *
      (1 +
        w * √(2 * Real.pi) *
            Real.exp (w ^ 2 / 2) *
          ↑(ProbabilityTheory.cdf
                (ProbabilityTheory.gaussianReal
                  0 1))
            w)

Closed form of `steinSolutionDeriv` on `{w ≤ x}`.

theoremdefined in ProbabilityApproximation/ChenShao/NonuniformStein.lean

complete

theorem ProbabilityTheory.steinSolutionDeriv_of_gt {x w : ℝ} (hw : x < w) :
  ProbabilityTheory.steinSolutionDeriv x w =
    ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) x *
      (w * √(2 * Real.pi) * Real.exp (w ^ 2 / 2) *
          (1 -
            ↑(ProbabilityTheory.cdf
                  (ProbabilityTheory.gaussianReal 0 1))
              w) -
        1)

theorem ProbabilityTheory.steinSolutionDeriv_of_gt
  {x w : ℝ} (hw : x < w) :
  ProbabilityTheory.steinSolutionDeriv x
      w =
    ↑(ProbabilityTheory.cdf
            (ProbabilityTheory.gaussianReal
              0 1))
        x *
      (w * √(2 * Real.pi) *
            Real.exp (w ^ 2 / 2) *
          (1 -
            ↑(ProbabilityTheory.cdf
                  (ProbabilityTheory.gaussianReal
                    0 1))
              w) -
        1)

Closed form of `steinSolutionDeriv` on `{x < w}`.

theoremdefined in ProbabilityApproximation/ChenShao/NonuniformStein.lean

complete

theorem ProbabilityTheory.abs_steinSolutionDeriv_le_two_mul_tail {x w : ℝ}
  (hx : 0 < x) (hw : w ≤ 0) :
  |ProbabilityTheory.steinSolutionDeriv x w| ≤
    2 *
      (1 -
        ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) x)

theorem ProbabilityTheory.abs_steinSolutionDeriv_le_two_mul_tail
  {x w : ℝ} (hx : 0 < x) (hw : w ≤ 0) :
  |ProbabilityTheory.steinSolutionDeriv x
        w| ≤
    2 *
      (1 -
        ↑(ProbabilityTheory.cdf
              (ProbabilityTheory.gaussianReal
                0 1))
          x)

theoremdefined in ProbabilityApproximation/ChenShao/NonuniformStein.lean

complete

theorem ProbabilityTheory.abs_steinSolutionDeriv_le_majorant_of_abs_le_half
  {x w : ℝ} (hx : 2 ≤ x) (hw : |w| ≤ x / 2) :
  |ProbabilityTheory.steinSolutionDeriv x w| ≤
    (1 -
        ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1))
          x) *
      (1 + √(2 * Real.pi) * (x / 2) * Real.exp (x ^ 2 / 8))

theorem ProbabilityTheory.abs_steinSolutionDeriv_le_majorant_of_abs_le_half
  {x w : ℝ} (hx : 2 ≤ x)
  (hw : |w| ≤ x / 2) :
  |ProbabilityTheory.steinSolutionDeriv x
        w| ≤
    (1 -
        ↑(ProbabilityTheory.cdf
              (ProbabilityTheory.gaussianReal
                0 1))
          x) *
      (1 +
        √(2 * Real.pi) * (x / 2) *
          Real.exp (x ^ 2 / 8))

Pointwise majorant of `|f'_x|` when `|w| ≤ x/2`, `x ≥ 2`.

theoremdefined in ProbabilityApproximation/ChenShao/NonuniformStein.lean

complete

theorem ProbabilityTheory.cdf_sub_eq_integral_steinSolutionDeriv_sub_Wf.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : ι → Ω → ℝ} (hX : ∀ (k : ι), MeasureTheory.MemLp (X k) 2 μ)
  (hXmeas : ∀ (k : ι), Measurable (X k)) (x : ℝ) :
  ↑(ProbabilityTheory.cdf
            (MeasureTheory.Measure.map (ProbabilityTheory.sumX X) μ))
        x -
      ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) x =
    ∫ (ω : Ω),
        ProbabilityTheory.steinSolutionDeriv x
          (ProbabilityTheory.sumX X ω) ∂μ -
      ∫ (ω : Ω),
        ProbabilityTheory.sumX X ω *
          ProbabilityTheory.steinSolution x
            (ProbabilityTheory.sumX X ω) ∂μ

theorem ProbabilityTheory.cdf_sub_eq_integral_steinSolutionDeriv_sub_Wf.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : ι → Ω → ℝ}
  (hX :
    ∀ (k : ι),
      MeasureTheory.MemLp (X k) 2 μ)
  (hXmeas : ∀ (k : ι), Measurable (X k))
  (x : ℝ) :
  ↑(ProbabilityTheory.cdf
            (MeasureTheory.Measure.map
              (ProbabilityTheory.sumX X)
              μ))
        x -
      ↑(ProbabilityTheory.cdf
            (ProbabilityTheory.gaussianReal
              0 1))
        x =
    ∫ (ω : Ω),
        ProbabilityTheory.steinSolutionDeriv
          x
          (ProbabilityTheory.sumX X
            ω) ∂μ -
      ∫ (ω : Ω),
        ProbabilityTheory.sumX X ω *
          ProbabilityTheory.steinSolution
            x
            (ProbabilityTheory.sumX X
              ω) ∂μ

Stein equation integrated form: `F(x) − Φ(x) = E[f'_x(W) − W f_x(W)]`.

The two closed forms are the half-line specialization of Chen and Shao (2005), equation (8.3), printed p. 54, derived from the solution in equation (2.3), printed pp. 9--10. The Mills bounds in equation (8.1) and sign estimates in equations (8.4)--(8.5), printed pp. 54--55, give the displayed tail majorants; the |w|\le x/2 specialization is used in the proof of equation (6.17), printed p. 46. The integrated identity is equation (1.4), printed p. 4, and the first equality in the residual expansion (6.16), printed p. 46.