The Chen–Stein error terms b_1 and b_2: Proposition prop:b1 and Lemma lem:boundb2

Work package WP5 of the bridge plan. Source lines 1615–1619 and 1709–1725 (the Chen–Stein setting), 1797–1807 (Proposition 4.6) and 1815–1857 (Lemma 4.7, P11, audit finding 5).

The indicators are I_{i+1}^{(M)}(X_1, …, X_n) = 1_{cycEvent G M n i} (0-based i : Fin n) on the probability space (Fin n → ℤ, P(· | S_n = -1)), and the neighbourhoods are B_i = cycNbhd n M i = {j : |i - j|_cyc < M}. The error terms errorB1, errorB2, errorB3 are literally the three sums of ChenStein.prop_AGG for P = bridgeLaw μ n, E = cycEvent G M n, B = cycNbhd n M; b_3 is only defined here (it is bounded in the endpoint-smoothing package).

Main statements

• cycDist, cycNbhd, mem_cycNbhd_self, card_cycNbhd_le (|B_i| ≤ 2M), cycGap and cycGap_mem_Icc_or (bookkeeping of cyclic gaps).
• cycEvent, errorB1, errorB2, errorB3; bridgeLaw_real_cycEvent (P(E_i) = q), sum_bridgeLaw_real_cycEvent (∑ P(E_i) = n q), cyclicSum_ofFn_eq_sum_indicator (W_n^M = ∑ 1_{E_i}).
• exists_paperTVDist_cyclicSum_le_errorTerms: Proposition prop:AGG instantiated, d_TV(W_n^M, Po(n q)) ≤ 2 (b_1 + b_2 + b_3(f)) for some ‖f‖_∞ ≤ 1.
• errorB1_le, tendsto_mul_two_mul_cutoff_mul_qProb_sq, tendsto_errorB1 (Proposition prop:b1): b_1 ≤ n · 2M_n · q_n² → 0 for bounded n π_n.
• bridgeLaw_real_cycEvent_inter, errorB2_le (cyclic exchangeability: b_2 ≤ 2n ∑_{ℓ=1}^{M-1} P(I_1 I_{1+ℓ} | S_n = -1)), firstMarked_pair_take_iff (locality of the pair in the first 2M increments), tendsto_errorB2 (Lemma lem:boundb2).

The pair at cyclic distance ℓ < M_n sits at forward gap ℓ or n - ℓ; both are reduced to gap ℓ by rotating the cycle (cycGap_mem_Icc_or, bridgeLaw_real_cycEvent_inter), so only P(I_1 I_{1+ℓ} | S_n = -1) with 1 ≤ ℓ ≤ M_n - 1 is bounded, by Lemma lem:error_est on the first 2 M_n increments and the two-start bound of Bridge/PairBound.lean.

Cyclic distance and neighbourhoods

def PoissonDeclumping.Bridge.cycDist (n i j : ℕ) : ℕ

The cyclic distance |i - j|_cyc = min(|i - j|, n - |i - j|) (source lines 1617, 1715), with |i - j| = max i j - min i j.

Equations

• PoissonDeclumping.Bridge.cycDist n i j = min (max i j - min i j) (n - (max i j - min i j))

def PoissonDeclumping.Bridge.cycNbhd (n M : ℕ) (i : Fin n) : Finset (Fin n)

The Chen–Stein neighbourhood B_i = {j ∈ [n] : |i - j|_cyc < M} (source lines 1617, 1715), with 0-based indices Fin n.

Equations

• PoissonDeclumping.Bridge.cycNbhd n M i = {j : Fin n | PoissonDeclumping.Bridge.cycDist n ↑i ↑j < M}

theorem PoissonDeclumping.Bridge.mem_cycNbhd {n M : ℕ} {i j : Fin n} : j ∈ cycNbhd n M i ↔ cycDist n ↑i ↑j < M

theorem PoissonDeclumping.Bridge.mem_cycNbhd_self {n M : ℕ} (hM : 0 < M) (i : Fin n) : i ∈ cycNbhd n M i

def PoissonDeclumping.Bridge.cycGap (n i j : ℕ) : ℕ

The forward gap from i to j on the cycle ℤ / nℤ, in {0, …, n - 1}: j ≡ i + gap.

Equations

• PoissonDeclumping.Bridge.cycGap n i j = if i ≤ j then j - i else j + n - i

theorem PoissonDeclumping.Bridge.cycGap_inj_right {n i j j' : ℕ} (hi : i < n) (hj : j < n) (hj' : j' < n) (h : cycGap n i j = cycGap n i j') : j = j'

theorem PoissonDeclumping.Bridge.cycGap_inj_left {n i j j' : ℕ} (hj : j < n) (hj' : j' < n) (h : cycGap n j i = cycGap n j' i) : j = j'

theorem PoissonDeclumping.Bridge.cycGap_mem_Icc_or {n M i j : ℕ} (hi : i < n) (hj : j < n) (hne : j ≠ i) (h : cycDist n i j < M) : cycGap n i j ∈ Finset.Icc 1 (M - 1) ∨ cycGap n j i ∈ Finset.Icc 1 (M - 1)

A neighbour j ≠ i of i is at forward gap ℓ ∈ [1, M - 1] from i, or i is at forward gap ℓ ∈ [1, M - 1] from j.

theorem PoissonDeclumping.Bridge.card_cycNbhd_le (n M : ℕ) (i : Fin n) : (cycNbhd n M i).card ≤ 2 * M

|B_i| ≤ 2 M (source line 1803).

theorem PoissonDeclumping.Bridge.rotate_rotate_cycGap {β : Type u_1} {x : List β} {n i j : ℕ} (hx : x.length = n) (hi : i < n) (hj : j < n) : (x.rotate i).rotate (cycGap n i j) = x.rotate j

Rotating by i and then by the gap from i to j is rotating by j.

The cyclic indicator events and the Chen–Stein error terms

def PoissonDeclumping.Bridge.cycEvent (G : PlaneTree → Prop) (M n : ℕ) (i : Fin n) : Set (Fin n → ℤ)

The event {I_{i+1}^{(M)}(X_1, …, X_n) = 1} (0-based index i : Fin n).

Equations

• PoissonDeclumping.Bridge.cycEvent G M n i = {ω : Fin n → ℤ | PoissonDeclumping.Cyclic.FirstMarked G (↑M) ((List.ofFn ω).rotate ↑i)}

theorem PoissonDeclumping.Bridge.measurableSet_cycEvent (G : PlaneTree → Prop) (M n : ℕ) (i : Fin n) : MeasurableSet (cycEvent G M n i)

noncomputable def PoissonDeclumping.Bridge.errorB1 (μ : PMF ℕ) (G : PlaneTree → Prop) (M n : ℕ) : ℝ

The error term b_1 = ∑_i ∑_{j ∈ B_i} q_i q_j of Proposition prop:AGG for the indicators I_i^{(M)} under P(· | S_n = -1) (source lines 1607, 1719).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PoissonDeclumping.Bridge.errorB2 (μ : PMF ℕ) (G : PlaneTree → Prop) (M n : ℕ) : ℝ

The error term b_2 = ∑_i ∑_{j ∈ B_i \ {i}} E[I_i I_j] (source lines 1607, 1719).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PoissonDeclumping.Bridge.errorB3 (μ : PMF ℕ) (G : PlaneTree → Prop) (M n : ℕ) (f : ℕ → ℝ) : ℝ

The error term b_3 = ∑_i |E[(I_i - q_i) f(1 + ∑_{j ∉ B_i} I_j)]| (source lines 1607, 1721–1725), for a test function f.

Equations

• One or more equations did not get rendered due to their size.

theorem PoissonDeclumping.Bridge.bridgeLaw_real_cycEvent (μ : PMF ℕ) (G : PlaneTree → Prop) (M n : ℕ) (i : Fin n) : (Lukasiewicz.bridgeLaw μ n).real (cycEvent G M n i) = qProb μ G M n

Every cyclic indicator has bridge probability q (cyclic exchangeability, source line 1724).

theorem PoissonDeclumping.Bridge.sum_bridgeLaw_real_cycEvent (μ : PMF ℕ) (G : PlaneTree → Prop) (M n : ℕ) : ∑ i : Fin n, (Lukasiewicz.bridgeLaw μ n).real (cycEvent G M n i) = ↑n * qProb μ G M n

λ = ∑_i P(I_i^{(M)} = 1 | S_n = -1) = n q.

theorem PoissonDeclumping.Bridge.cyclicSum_ofFn_eq_sum_indicator (G : PlaneTree → Prop) (M : ℕ) {n : ℕ} (ω : Fin n → ℤ) : Cyclic.cyclicSum G (↑M) (List.ofFn ω) = ∑ i : Fin n, (cycEvent G M n i).indicator 1 ω

W_n^M = ∑_i I_i^{(M)} as a sum of indicators of the events cycEvent.

theorem PoissonDeclumping.Bridge.exists_paperTVDist_cyclicSum_le_errorTerms (μ : PMF ℕ) (G : PlaneTree → Prop) {M n : ℕ} (hn : PlaneTree.Admissible μ n) (hM : 0 < M) : ∃ (f : ℕ → ℝ), (∀ (k : ℕ), |f k| ≤ 1) ∧ paperTVDist (MeasureTheory.Measure.map (fun (ω : Fin n → ℤ) => Cyclic.cyclicSum G (↑M) (List.ofFn ω)) (Lukasiewicz.bridgeLaw μ n)) (ProbabilityTheory.poissonMeasure (↑n * qProb μ G M n).toNNReal) ≤ 2 * (errorB1 μ G M n + errorB2 μ G M n + errorB3 μ G M n f)

Proposition prop:AGG instantiated (source lines 1615–1619, 1709–1725): at every admissible n and cutoff M ≥ 1, with P = P(· | S_n = -1), E_i = {I_{i+1}^{(M)} = 1} and B_i = cycNbhd n M i, there is f with ‖f‖_∞ ≤ 1 such that d_TV(W_n^M, Po(n q)) ≤ 2 (b_1 + b_2 + b_3(f)).

Bounding b_1 (Proposition prop:b1)

theorem PoissonDeclumping.Bridge.errorB1_le (μ : PMF ℕ) (G : PlaneTree → Prop) (M n : ℕ) : errorB1 μ G M n ≤ ↑n * (2 * ↑M) * qProb μ G M n ^ 2

b_1 ≤ n · 2M · q² (source line 1803).

theorem PoissonDeclumping.Bridge.errorB1_nonneg (μ : PMF ℕ) (G : PlaneTree → Prop) (M n : ℕ) : 0 ≤ errorB1 μ G M n

b_1 is nonnegative.

theorem PoissonDeclumping.Bridge.isBigO_mul_mul_markProb_sq_one {μ : PMF ℕ} {G : ℕ → PlaneTree → Prop} {k : ℕ → ℕ} (hbd : ∃ (C : ℝ), ∀ᶠ (n : ℕ) in admissibleSizes μ, ↑n * markProb μ G k n ≤ C) : (fun (n : ℕ) => ↑n * (↑n * markProb μ G k n ^ 2)) =O[admissibleSizes μ] fun (x : ℕ) => 1

Bounded mean: n² π_n² = O(1) along admissible sizes.

theorem PoissonDeclumping.Bridge.tendsto_mul_cutoff_mul_markProb_sq {μ : PMF ℕ} {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hM : IsCutoff M) (hbd : ∃ (C : ℝ), ∀ᶠ (n : ℕ) in admissibleSizes μ, ↑n * markProb μ G k n ≤ C) : Filter.Tendsto (fun (n : ℕ) => ↑n * ↑(M n) * markProb μ G k n ^ 2) (admissibleSizes μ) (nhds 0)

n M_n π_n² → 0 along admissible sizes when (n π_n) is bounded and M_n = o(n).

theorem PoissonDeclumping.Bridge.tendsto_mul_two_mul_cutoff_mul_qProb_sq {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hM : IsCutoff M) (hbd : ∃ (C : ℝ), ∀ᶠ (n : ℕ) in admissibleSizes μ, ↑n * markProb μ G k n ≤ C) : Filter.Tendsto (fun (n : ℕ) => ↑n * (2 * ↑(M n)) * qProb μ (G (k n)) (M n) n ^ 2) (admissibleSizes μ) (nhds 0)

Proposition prop:b1 (source lines 1797–1807): if (n π_n) is bounded, then n · 2M_n · q_n² → 0 along admissible sizes (via Corollary cor:pip).

theorem PoissonDeclumping.Bridge.tendsto_errorB1 {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hM : IsCutoff M) (hbd : ∃ (C : ℝ), ∀ᶠ (n : ℕ) in admissibleSizes μ, ↑n * markProb μ G k n ≤ C) : Filter.Tendsto (fun (n : ℕ) => errorB1 μ (G (k n)) (M n) n) (admissibleSizes μ) (nhds 0)

Proposition prop:b1 (source lines 1797–1807): if (n π_n) is bounded, then b_1^n → 0 along admissible sizes.

Bounding b_2 (Lemma lem:boundb2)

noncomputable def PoissonDeclumping.Bridge.pairBridge (μ : PMF ℕ) (G : PlaneTree → Prop) (M n ℓ : ℕ) : ℝ

E[I_1^{(M)} I_{1+ℓ}^{(M)} | S_n = -1].

Equations

• One or more equations did not get rendered due to their size.

theorem PoissonDeclumping.Bridge.bridgeLaw_real_cycEvent_inter (μ : PMF ℕ) (G : PlaneTree → Prop) (M n : ℕ) (i j : Fin n) : (Lukasiewicz.bridgeLaw μ n).real (cycEvent G M n i ∩ cycEvent G M n j) = pairBridge μ G M n (cycGap n ↑i ↑j)

Cyclic exchangeability for pairs: P(I_{i+1} = I_{j+1} = 1 | S_n = -1) only depends on the forward gap from i to j (source line 1823, "by cyclic invariance").

theorem PoissonDeclumping.Bridge.errorB2_le (μ : PMF ℕ) (G : PlaneTree → Prop) (M n : ℕ) : errorB2 μ G M n ≤ ↑n * (2 * ∑ ℓ ∈ Finset.Icc 1 (M - 1), pairBridge μ G M n ℓ)

b_2 ≤ 2 n ∑_{ℓ=1}^{M-1} E[I_1^{(M)} I_{1+ℓ}^{(M)} | S_n = -1] (cyclic exchangeability; the pairs at cyclic distance ℓ are at forward gap ℓ or n - ℓ).

theorem PoissonDeclumping.Bridge.firstMarked_pair_take_iff {G : PlaneTree → Prop} {M ℓ K : ℕ} {x : List ℤ} (hℓ : ℓ + M ≤ K) (hK : K ≤ x.length) : Cyclic.FirstMarked G (↑M) (List.take K x) ∧ Cyclic.FirstMarked G (↑M) ((List.take K x).rotate ℓ) ↔ Cyclic.FirstMarked G (↑M) x ∧ Cyclic.FirstMarked G (↑M) (x.rotate ℓ)

Locality of the pair event: for ℓ + M ≤ K ≤ |x|, the pair I_1^{(M)} I_{1+ℓ}^{(M)} only reads the first K entries.

theorem PoissonDeclumping.Bridge.errorB2_nonneg (μ : PMF ℕ) (G : PlaneTree → Prop) (M n : ℕ) : 0 ≤ errorB2 μ G M n

b_2 is nonnegative.

theorem PoissonDeclumping.Bridge.exists_eventually_errorB2_le {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hM : IsCutoff M) : ∃ (C₀ : ℝ), 0 < C₀ ∧ ∀ᶠ (n : ℕ) in admissibleSizes μ, errorB2 μ (G (k n)) (M n) n ≤ 2 * C₀ * (↑n * ↑(M n) * markProb μ G k n ^ 2 + ↑n * ∑ ℓ ∈ Finset.Icc 1 (M n), pairProb μ G k n ℓ)

The bound on b_2 from the proof of Lemma lem:boundb2 (source lines 1815–1857), without the bounded-mean hypothesis: eventually along admissible sizes, b_2 ≤ 2 C₀ (n M_n π_n² + n ∑_{ℓ=1}^{M_n} A_n(ℓ)).

theorem PoissonDeclumping.Bridge.tendsto_errorB2 {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hM : IsCutoff M) (hC : NonClustering μ G k M) (hbd : ∃ (C : ℝ), ∀ᶠ (n : ℕ) in admissibleSizes μ, ↑n * markProb μ G k n ≤ C) : Filter.Tendsto (fun (n : ℕ) => errorB2 μ (G (k n)) (M n) n) (admissibleSizes μ) (nhds 0)

Lemma lem:boundb2 (source lines 1815–1857, audit finding 5): under Assumption (C) and bounded n π_n, b_2^n → 0 along admissible sizes. Proof: cyclic exchangeability (errorB2_le), bridge removal (Lemma lem:error_est with N_n = n, window 2 M_n, endpoint -1), the two-start bound P(I_1 I_{1+ℓ}) ≤ π_n² + A_n(ℓ) (walkVecLaw_real_pair_le_markProb, proved by conditioning on ζ), and ∑_{ℓ ≤ M_n} A_n(ℓ) = o(n π_n²).