1.2. Uniform approximation and leave-one-out concentration🔗

Lemma1.2.1

uses 0used by 1✓L∃∀N

Tagsscalarconcentrationsource-chen-shao-2001fidelity-project-variant

Uniform leave-one-out concentration. Suppose \mathbb EX_i=0, \mathbb E X_i^2<\infty, and \sum_i\operatorname{Var}(X_i)=1. If \gamma<\infty, then, for W^{(i)}=W-X_i, every i\in I, and all a\le b, \Pr(a\le W^{(i)}\le b) \le \sqrt2\,(b-a)+2(\sqrt2+1)\gamma.

Lean code for Lemma1.2.1●1 theorem

theoremdefined in ProbabilityApproximation/ChenShao/Concentration.lean

complete

theorem ProbabilityTheory.concentration_leaveOneOut.{u_1, u_2} {ι : Type u_1}
  {Ω : Type u_2} [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : ι → Ω → ℝ} [DecidableEq ι]
  (hX : ∀ (j : ι), MeasureTheory.MemLp (X j) 2 μ)
  (hXmeas : ∀ (j : ι), Measurable (X j))
  (h_indep : ProbabilityTheory.iIndepFun X μ)
  (h_mean : ∀ (j : ι), ∫ (ω : Ω), X j ω ∂μ = 0)
  (hvar : ∑ j, ProbabilityTheory.variance (X j) μ = 1)
  (h3 : ∀ (j : ι), MeasureTheory.Integrable (fun ω => |X j ω| ^ 3) μ)
  (i : ι) {a b : ℝ} (hab : a ≤ b) :
  μ.real
      {ω |
        a ≤ ProbabilityTheory.leaveOneOut X i ω ∧
          ProbabilityTheory.leaveOneOut X i ω ≤ b} ≤
    √2 * (b - a) + 2 * (√2 + 1) * ProbabilityTheory.thirdMomentSum X μ

theorem ProbabilityTheory.concentration_leaveOneOut.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : ι → Ω → ℝ} [DecidableEq ι]
  (hX :
    ∀ (j : ι),
      MeasureTheory.MemLp (X j) 2 μ)
  (hXmeas : ∀ (j : ι), Measurable (X j))
  (h_indep :
    ProbabilityTheory.iIndepFun X μ)
  (h_mean :
    ∀ (j : ι), ∫ (ω : Ω), X j ω ∂μ = 0)
  (hvar :
    ∑ j,
        ProbabilityTheory.variance (X j)
          μ =
      1)
  (h3 :
    ∀ (j : ι),
      MeasureTheory.Integrable
        (fun ω => |X j ω| ^ 3) μ)
  (i : ι) {a b : ℝ} (hab : a ≤ b) :
  μ.real
      {ω |
        a ≤
            ProbabilityTheory.leaveOneOut
              X i ω ∧
          ProbabilityTheory.leaveOneOut X
              i ω ≤
            b} ≤
    √2 * (b - a) +
      2 * (√2 + 1) *
        ProbabilityTheory.thirdMomentSum X
          μ

Leave-one-out concentration (CGS Lemma 3.1 form):
`P(a ≤ W⁽ⁱ⁾ ≤ b) ≤ √2 (b - a) + 2(√2 + 1) γ` with `γ = ∑ E|Xⱼ|³`.

The proof follows the concentration-kernel argument of Chen and Shao (2001), Section 3, especially Proposition 3.2 and equations (3.2)--(3.6), printed pp. 239--241. The constants above are the proved project variant; they are not asserted to be the paper's 1.5 and 3.3\delta constants under its extra small-truncation hypothesis.

Theorem1.2.2

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

Tagsscalarberry-esseensource-chen-shao-2005fidelity-explicit-coarse-constant

Uniform third-moment Berry--Esseen theorem. Suppose \mathbb EX_i=0, \mathbb E|X_i|^3<\infty, and \sum_i\operatorname{Var}(X_i)=1. Then, for every x\in\mathbb R, \left|\Pr(W\le x)-\Phi(x)\right|\le30\gamma.

Lean code for Theorem1.2.2●2 declarations

defdefined in ProbabilityApproximation/ChenShao/UniformBerryEsseen.lean

complete

def ProbabilityTheory.thirdMomentBerryEsseenConstant : ℝ

def ProbabilityTheory.thirdMomentBerryEsseenConstant :
  ℝ

Explicit third-moment constant (CGS path with `|f'|≤2`, `|f|≤√(2π)/2`).

Breakdown targeting constant `30`:
* Stein residual ≤ `(3/2)(2 + √(2π)/2) γ ≈ 4.88 γ`
* Concentration upgrade ≤ `(3.5√2 + 2) γ ≈ 6.95 γ` (CGS (3.30))
* Safety margin for formalization gaps in comparison constants → `30`.

theoremdefined in ProbabilityApproximation/ChenShao/UniformBerryEsseen.lean

complete

theorem ProbabilityTheory.uniformBerryEsseen_thirdMoment.{u_1, u_2}
  {ι : Type u_1} {Ω : Type u_2} [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {X : ι → Ω → ℝ} [DecidableEq ι]
  (hX : ∀ (k : ι), MeasureTheory.MemLp (X k) 2 μ)
  (hXmeas : ∀ (k : ι), Measurable (X k))
  (h_indep : ProbabilityTheory.iIndepFun X μ)
  (h_mean : ∀ (k : ι), ∫ (ω : Ω), X k ω ∂μ = 0)
  (hvar : ∑ k, ProbabilityTheory.variance (X k) μ = 1)
  (h3 : ∀ (k : ι), MeasureTheory.Integrable (fun ω => |X k ω| ^ 3) μ)
  (x : ℝ) :
  |↑(ProbabilityTheory.cdf
              (MeasureTheory.Measure.map (fun ω => ∑ i, X i ω) μ))
          x -
        ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1))
          x| ≤
    ProbabilityTheory.thirdMomentBerryEsseenConstant *
      ProbabilityTheory.thirdMomentSum X μ

theorem ProbabilityTheory.uniformBerryEsseen_thirdMoment.{u_1,
    u_2}
  {ι : Type u_1} {Ω : Type u_2}
  [Fintype ι] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : ι → Ω → ℝ} [DecidableEq ι]
  (hX :
    ∀ (k : ι),
      MeasureTheory.MemLp (X k) 2 μ)
  (hXmeas : ∀ (k : ι), Measurable (X k))
  (h_indep :
    ProbabilityTheory.iIndepFun X μ)
  (h_mean :
    ∀ (k : ι), ∫ (ω : Ω), X k ω ∂μ = 0)
  (hvar :
    ∑ k,
        ProbabilityTheory.variance (X k)
          μ =
      1)
  (h3 :
    ∀ (k : ι),
      MeasureTheory.Integrable
        (fun ω => |X k ω| ^ 3) μ)
  (x : ℝ) :
  |↑(ProbabilityTheory.cdf
              (MeasureTheory.Measure.map
                (fun ω => ∑ i, X i ω) μ))
          x -
        ↑(ProbabilityTheory.cdf
              (ProbabilityTheory.gaussianReal
                0 1))
          x| ≤
    ProbabilityTheory.thirdMomentBerryEsseenConstant *
      ProbabilityTheory.thirdMomentSum X μ

Pure linear third-moment Berry-Esseen: `|F-Phi| ≤ 30 γ` for all `γ`.

The proof is the concentration-inequality Stein route developed by Chen and Shao (2005), Sections 5.1--5.2, printed pp. 31--35, with a deliberately coarse kernel-checked constant 30. It does not claim the sharper truncated constant 4.1 in Chen and Shao (2001), Theorem 2.1, printed pp. 237--238.