The Arratia–Goldstein–Gordon Chen–Stein bound

Proposition prop:AGG of the source (lines 1597–1614). For indicators I_i = 1_{E_i} on a probability space, with q_i = P(E_i), λ = ∑ q_i, W = ∑ I_i, and neighbourhoods B_i ∋ i, there is one function f with ‖f‖_∞ ≤ 1 such that

d_TV(W, Po(λ)) ≤ 2 (b_1 + b_2 + b_3),

where b_1 = ∑_i ∑_{j ∈ B_i} q_i q_j, b_2 = ∑_i ∑_{j ∈ B_i \ {i}} E[I_i I_j] and b_3 = ∑_i |E[(I_i - q_i) f(1 + ∑_{j ∉ B_i} I_j)]|; d_TV is the probability-normalized distance paperTVDist.

The proof is the standard Chen–Stein argument: choose an event A attaining the distance, take the Stein solution f = f_A (bounded by one, PoissonDeclumping.ChenStein.SteinSolution), and decompose λ f(W+1) - W f(W) along the neighbourhoods. Instead of AGG's sharper Stein factors we use only ‖f_A‖ ≤ 1, hence |f_A(x + d) - f_A(x)| ≤ 2d; this gives the slightly stronger d_TV ≤ 2 b_1 + 2 b_2 + b_3 (exists_paperTVDist_le_two_mul_add).

theorem PoissonDeclumping.ChenStein.abs_pointwise_le {f : ℕ → ℝ} (hf : ∀ (k : ℕ), |f k| ≤ 1) {q : ℝ} (hq : 0 ≤ q) {n u v : ℕ} (hn : n ≤ 1) : |q * (f (n + u + v + 1) - f (1 + v)) - ↑n * (f (n + u + v) - f (1 + v))| ≤ 2 * q * (↑n + ↑u) + 2 * (↑n * ↑u)

The pointwise neighbourhood estimate behind the Chen–Stein decomposition. Here n = I_i, u = ∑_{j ∈ B_i \ {i}} I_j, v = ∑_{j ∉ B_i} I_j, so W = n + u + v.

theorem PoissonDeclumping.ChenStein.natCast_indicator_one {Ω : Type u_1} (s : Set Ω) (ω : Ω) : ↑(s.indicator 1 ω) = s.indicator 1 ω

The natural-number and real indicators agree after casting.

theorem PoissonDeclumping.ChenStein.indicator_one_le_one {Ω : Type u_1} (s : Set Ω) (ω : Ω) : s.indicator 1 ω ≤ 1

theorem PoissonDeclumping.ChenStein.abs_map_sub_poissonMeasure_le {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] [Fintype ι] [DecidableEq ι] (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (E : ι → Set Ω) (hE : ∀ (i : ι), MeasurableSet (E i)) (B : ι → Finset ι) (hB : ∀ (i : ι), i ∈ B i) {r : NNReal} (hr : 0 < r) (hrE : ↑r = ∑ i : ι, P.real (E i)) (A : Set ℕ) : |(MeasureTheory.Measure.map (fun (ω : Ω) => ∑ i : ι, (E i).indicator 1 ω) P).real A - (ProbabilityTheory.poissonMeasure r).real A| ≤ 2 * ∑ i : ι, ∑ j ∈ B i, P.real (E i) * P.real (E j) + 2 * ∑ i : ι, ∑ j ∈ B i \ {i}, P.real (E i ∩ E j) + ∑ i : ι, |∫ (ω : Ω), ((E i).indicator 1 ω - P.real (E i)) * steinSolution r A (1 + ∑ j ∈ Finset.univ \ B i, (E j).indicator 1 ω) ∂P|

Chen–Stein bound for a fixed event. For every rate r > 0 equal to ∑ P(E_i) and every A ⊆ ℕ, the discrepancy P(W ∈ A) - Po(r)(A) is bounded by 2 b_1 + 2 b_2 + b_3(f_A) with the Stein solution f_A = steinSolution r A.

theorem PoissonDeclumping.ChenStein.exists_paperTVDist_le_two_mul_add {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] [Fintype ι] [DecidableEq ι] (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (E : ι → Set Ω) (hE : ∀ (i : ι), MeasurableSet (E i)) (B : ι → Finset ι) (hB : ∀ (i : ι), i ∈ B i) (lam : NNReal) (hlam : ↑lam = ∑ i : ι, P.real (E i)) : ∃ (f : ℕ → ℝ), (∀ (k : ℕ), |f k| ≤ 1) ∧ paperTVDist (MeasureTheory.Measure.map (fun (ω : Ω) => ∑ i : ι, (E i).indicator 1 ω) P) (ProbabilityTheory.poissonMeasure lam) ≤ 2 * ∑ i : ι, ∑ j ∈ B i, P.real (E i) * P.real (E j) + 2 * ∑ i : ι, ∑ j ∈ B i \ {i}, P.real (E i ∩ E j) + ∑ i : ι, |∫ (ω : Ω), ((E i).indicator 1 ω - P.real (E i)) * f (1 + ∑ j ∈ Finset.univ \ B i, (E j).indicator 1 ω) ∂P|

Chen–Stein bound, sharper constants. With the indicators I_i = 1_{E_i}, q_i = P(E_i), λ = ∑ q_i and neighbourhoods B_i ∋ i, some f with |f| ≤ 1 gives d_TV(W, Po(λ)) ≤ 2 b_1 + 2 b_2 + b_3(f). The rate is passed as lam : ℝ≥0 with its defining equation; the degenerate case λ = 0 is included.

theorem PoissonDeclumping.ChenStein.exists_paperTVDist_le_AGG {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] [Fintype ι] [DecidableEq ι] (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (E : ι → Set Ω) (hE : ∀ (i : ι), MeasurableSet (E i)) (B : ι → Finset ι) (hB : ∀ (i : ι), i ∈ B i) (lam : NNReal) (hlam : ↑lam = ∑ i : ι, P.real (E i)) : ∃ (f : ℕ → ℝ), (∀ (k : ℕ), |f k| ≤ 1) ∧ paperTVDist (MeasureTheory.Measure.map (fun (ω : Ω) => ∑ i : ι, (E i).indicator 1 ω) P) (ProbabilityTheory.poissonMeasure lam) ≤ 2 * (∑ i : ι, ∑ j ∈ B i, P.real (E i) * P.real (E j) + ∑ i : ι, ∑ j ∈ B i \ {i}, P.real (E i ∩ E j) + ∑ i : ι, |∫ (ω : Ω), ((E i).indicator 1 ω - P.real (E i)) * f (1 + ∑ j ∈ Finset.univ \ B i, (E j).indicator 1 ω) ∂P|)

Proposition prop:AGG (Arratia–Goldstein–Gordon), for an arbitrary finite index type and a rate lam given with its defining equation lam = ∑ i, P(E i): there is one f with ‖f‖_∞ ≤ 1 such that d_TV(W, Po(λ)) ≤ 2 (b_1 + b_2 + b_3).

theorem PoissonDeclumping.ChenStein.prop_AGG {Ω : Type u_3} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (n : ℕ) (E : Fin n → Set Ω) (hE : ∀ (i : Fin n), MeasurableSet (E i)) (B : Fin n → Finset (Fin n)) (hB : ∀ (i : Fin n), i ∈ B i) : ∃ (f : ℕ → ℝ), (∀ (k : ℕ), |f k| ≤ 1) ∧ paperTVDist (MeasureTheory.Measure.map (fun (ω : Ω) => ∑ i : Fin n, (E i).indicator 1 ω) P) (ProbabilityTheory.poissonMeasure (∑ i : Fin n, P.real (E i)).toNNReal) ≤ 2 * (∑ i : Fin n, ∑ j ∈ B i, P.real (E i) * P.real (E j) + ∑ i : Fin n, ∑ j ∈ B i \ {i}, P.real (E i ∩ E j) + ∑ i : Fin n, |∫ (ω : Ω), ((E i).indicator 1 ω - P.real (E i)) * f (1 + ∑ j ∈ Finset.univ \ B i, (E j).indicator 1 ω) ∂P|)

Proposition prop:AGG in the source's notation (lines 1600–1614): indicators I^n_i = 1_{E i} indexed by [n] = Fin n on a probability space, q^n_i = P(E i), λ^n = ∑ q^n_i, W^n = ∑ I^n_i, and B^n_i ⊆ [n] with i ∈ B^n_i. There exists f_n with ‖f_n‖_∞ ≤ 1 such that d_TV(W^n, Po(λ^n)) ≤ 2 (b^n_1 + b^n_2 + b^n_3), where d_TV is the [0, 1]-valued paperTVDist.