Boundary cases: Lemma lem:extreme_means

Work package WP7 (first half) of the bridge plan. Source lines 1997–2089 (Lemma 4.10, proof step P13). Notation as in Bridge/Truncation.lean and Bridge/ErrorTerms.lean: W_n^M = cyclicSum (G (k n)) (M n) (List.ofFn ω) under bridgeLaw μ n = P(· | S_n = -1), I_{i+1}^{(M)} = 1_{cycEvent G M n i}, q_n = qProb, p_n = pProb, π_n = markProb μ G k n. The paper writes μ_n = n q_n (line 2024); here that is n * qProb … (correction F15: μ is the offspring law).

Main statements

• walkVecLaw_real_two_blocks_inter_sum_le: the two-block Markov formula (walkVecLaw_real_two_blocks_inter_sum) under a uniform bound on Ψ_{n-m₁-m₂}, giving P(H₁(X_1..X_{m₁}), H₂(X_{j+1}..X_{j+m₂}), S_n = s) ≤ K P(H₁) P(H₂).
• eventually_pairBridge_le (separated pairs, source lines 2042–2079): for every δ > 0, eventually along admissible sizes, P(I_1 = I_{1+ℓ} = 1 | S_n = -1) ≤ (1 + δ) p_n² uniformly for M_n ≤ ℓ ≤ n - M_n. Only the toolkit and the cutoff are used. The two blocks are independent only under the unconditioned law; the bridge weight Ψ_{n-2M_n}(-1 - S_{M_n} - Z) / Ψ_n(-1) is ≤ 1 + δ on the good blocks (|S| ≤ r_n and S ≡ -M_n (mod d), compatible endpoints, F4/F15) and bounded on the bad blocks, whose probability is o(p_n) (Lemma lem:pnqn(i)).
• integral_cyclicSum_sq, bridgeLaw_real_le_abs_cyclicSum_sub_le (Chebyshev), sum_sum_cycEvent_inter_le (diagonal + nearby + separated pairs).
• exists_eventually_errorB2_le, eventually_errorB2_le (nearby pairs, source lines 2029–2040): b_2 = o((n π_n)²) under (C), with no assumption on the size of n π_n.
• tendsto_bridgeLaw_one_le_cyclicSum (Lemma lem:extreme_means(i)) and tendsto_bridgeLaw_abs_cyclicSum_div_sub_one (Lemma lem:extreme_means(ii)).

Two disjoint blocks under the bridge

theorem PoissonDeclumping.Bridge.walkVecLaw_real_two_blocks_inter_sum_le (μ : PMF ℕ) {m₁ j m₂ n : ℕ} (hj : m₁ ≤ j) (hn : j + m₂ ≤ n) (H₁ H₂ : List ℤ → Prop) (s : ℤ) {K : ℝ} (hK0 : 0 ≤ K) (hK : ∀ (a : Fin m₁ → ℤ), H₁ (List.ofFn a) → ∀ (c : Fin m₂ → ℤ), H₂ (List.ofFn c) → walkProb μ (↑(n - m₁ - m₂)) (s - ∑ i : Fin m₁, a i - ∑ i : Fin m₂, c i) ≤ K) : (Lukasiewicz.walkVecLaw μ n).real {ω : Fin n → ℤ | H₁ (List.take m₁ (List.ofFn ω)) ∧ H₂ (List.take m₂ (List.drop j (List.ofFn ω))) ∧ ∑ i : Fin n, ω i = s} ≤ K * (Lukasiewicz.walkVecLaw μ m₁).real {a : Fin m₁ → ℤ | H₁ (List.ofFn a)} * (Lukasiewicz.walkVecLaw μ m₂).real {c : Fin m₂ → ℤ | H₂ (List.ofFn c)}

Two disjoint blocks with a bounded bridge weight (source lines 2058–2075): for m₁ ≤ j, j + m₂ ≤ n, if Ψ_{n-m₁-m₂}(s - S_{m₁} - S'_{m₂}) ≤ K whenever both blocks satisfy their events, then P(H₁(X_1..X_{m₁}), H₂(X_{j+1}..X_{j+m₂}), S_n = s) ≤ K P(H₁) P(H₂).

theorem PoissonDeclumping.Bridge.walkVecLaw_real_not_dvd {μ : PMF ℕ} {a : ℕ → ℝ} {d : ℕ} {L : ℝ} (hloc : LatticeLocal μ a d L) (m : ℕ) : (Lukasiewicz.walkVecLaw μ m).real {b : Fin m → ℤ | ¬↑d ∣ ∑ i : Fin m, b i + ↑m} = 0

The null event {d ∤ S_m + m}.

theorem PoissonDeclumping.Bridge.eventually_pairBridge_le {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) (G : ℕ → PlaneTree → Prop) (k : ℕ → ℕ) {M : ℕ → ℕ} (hM : IsCutoff M) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in admissibleSizes μ, ∀ (ℓ : ℕ), M n ≤ ℓ → ℓ + M n ≤ n → pairBridge μ (G (k n)) (M n) n ℓ ≤ (1 + ε) * pProb μ (G (k n)) (M n) ^ 2

Separated pairs (source lines 2042–2079, claim of the proof of Lemma lem:extreme_means(ii)): for every δ > 0, eventually along admissible sizes, P(I_1^{(M_n)} = I_{1+ℓ}^{(M_n)} = 1 | S_n = -1) ≤ (1 + δ) p_n² for every ℓ with M_n ≤ ℓ ≤ n - M_n (pairs at cyclic distance at least M_n, by cyclic exchangeability). Proof: the two-block Markov formula at the bridge endpoint -1 (the blocks are independent under the unconditioned law only), the ratio limit Ψ_{n-2M_n}(-1 - S_{M_n} - Z) / Ψ_n(-1) ≤ 1 + δ/2 for |S_{M_n}|, |Z| ≤ r_n = √(a_{M_n} a_n) at compatible endpoints (S ≡ -M_n mod d almost surely, F4/F15), the bound Ψ_{n-2M_n}(·) ≤ C Ψ_n(-1) elsewhere, and P(I_1^{(M_n)} = 1, |S_{M_n}| > r_n) = o(p_n) (Lemma lem:pnqn(i)). Toolkit and cutoff only.

Second moment of the truncated count

theorem PoissonDeclumping.Bridge.integrable_bridgeLaw_of_abs_le (μ : PMF ℕ) {n : ℕ} {f : (Fin n → ℤ) → ℝ} (C : ℝ) (h : ∀ (ω : Fin n → ℤ), |f ω| ≤ C) : MeasureTheory.Integrable f (Lukasiewicz.bridgeLaw μ n)

A bounded function of (X_1, …, X_n) is integrable under the bridge.

theorem PoissonDeclumping.Bridge.cyclicSum_cast_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 1_{E_i} in ℝ.

theorem PoissonDeclumping.Bridge.integral_cyclicSum_sq (μ : PMF ℕ) (G : PlaneTree → Prop) (M n : ℕ) : ∫ (ω : Fin n → ℤ), ↑(Cyclic.cyclicSum G (↑M) (List.ofFn ω)) ^ 2 ∂Lukasiewicz.bridgeLaw μ n = ∑ i : Fin n, ∑ j : Fin n, (Lukasiewicz.bridgeLaw μ n).real (cycEvent G M n i ∩ cycEvent G M n j)

Second moment: E[(W_n^M)² | S_n = -1] = ∑_i ∑_j P(I_i = I_j = 1 | S_n = -1).

theorem PoissonDeclumping.Bridge.bridgeLaw_real_le_abs_cyclicSum_sub_le (μ : PMF ℕ) (G : PlaneTree → Prop) {M n : ℕ} (hn : PlaneTree.Admissible μ n) {t : ℝ} (ht : 0 < t) : (Lukasiewicz.bridgeLaw μ n).real {ω : Fin n → ℤ | t ≤ |↑(Cyclic.cyclicSum G (↑M) (List.ofFn ω)) - ↑n * qProb μ G M n|} ≤ (∑ i : Fin n, ∑ j : Fin n, (Lukasiewicz.bridgeLaw μ n).real (cycEvent G M n i ∩ cycEvent G M n j) - (↑n * qProb μ G M n) ^ 2) / t ^ 2

Chebyshev's inequality for W_n^M under P(· | S_n = -1): for t > 0, P(|W_n^M - n q| ≥ t) ≤ (∑_i ∑_j P(I_i = I_j = 1) - (n q)²) / t².

theorem PoissonDeclumping.Bridge.sum_sum_cycEvent_inter_le (μ : PMF ℕ) (G : PlaneTree → Prop) {M n : ℕ} (hM : 0 < M) {S : ℝ} (hS0 : 0 ≤ S) (hS : ∀ (ℓ : ℕ), M ≤ ℓ → ℓ + M ≤ n → pairBridge μ G M n ℓ ≤ S) : ∑ i : Fin n, ∑ j : Fin n, (Lukasiewicz.bridgeLaw μ n).real (cycEvent G M n i ∩ cycEvent G M n j) ≤ ↑n * qProb μ G M n + errorB2 μ G M n + ↑n ^ 2 * S

Splitting the second moment into diagonal, nearby and separated pairs: if every pair at cyclic distance at least M has bridge probability at most S, then ∑_i ∑_j P(I_i = I_j = 1) ≤ n q + b_2 + n² S.

Nearby pairs

theorem PoissonDeclumping.Bridge.eventually_errorB2_le {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hM : IsCutoff M) (hC : NonClustering μ G k M) {η : ℝ} (hη : 0 < η) : ∀ᶠ (n : ℕ) in admissibleSizes μ, errorB2 μ (G (k n)) (M n) n ≤ η * (↑n * markProb μ G k n) ^ 2

Nearby pairs (source lines 2029–2040): under Assumption (C) and M_n = o(n), b_2 = o((n π_n)²) along admissible sizes, with no assumption on the size of n π_n.

theorem PoissonDeclumping.Bridge.chebyshev_arith {N π q p δ θ b : ℝ} (hN : 0 ≤ N) (hq0 : 0 ≤ q) (hp0 : 0 ≤ p) (hδ0 : 0 ≤ δ) (hδ1 : δ ≤ 1) (hδθ : 28 * δ ≤ θ) (hθ0 : 0 < θ) (hqπ : q ≤ 2 * π) (hpq : p ≤ (1 + δ) * q) (hNπ : 2 / θ + 1 ≤ N * π) (hb : b ≤ θ * (N * π) ^ 2) : N * q + b + N ^ 2 * ((1 + δ) * p ^ 2) - (N * q) ^ 2 ≤ 3 * θ * (N * π) ^ 2

The arithmetic of the Chebyshev bound in Lemma lem:extreme_means(ii): with N q ≤ 2 N π, p ≤ (1 + δ) q, 28 δ ≤ θ, N π ≥ 2/θ + 1 and b ≤ θ (N π)², N q + b + N² (1 + δ) p² - (N q)² ≤ 3 θ (N π)².

Lemma lem:extreme_means

theorem PoissonDeclumping.Bridge.tendsto_bridgeLaw_one_le_cyclicSum {μ : PMF ℕ} {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hmic : Microscopic μ G k M) (h0 : Filter.Tendsto (fun (n : ℕ) => ↑n * markProb μ G k n) (admissibleSizes μ) (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => (Lukasiewicz.bridgeLaw μ n).real {ω : Fin n → ℤ | 1 ≤ Cyclic.cyclicSum (G (k n)) (↑(M n)) (List.ofFn ω)}) (admissibleSizes μ) (nhds 0)

Lemma lem:extreme_means(i) (source lines 2010, 2019–2021): under Assumption (M), if n π_n → 0, then W_n^{M_n} → 0 in probability under P(· | S_n = -1); since W_n^{M_n} is integer valued this is P(W_n^{M_n} ≥ 1 | S_n = -1) → 0. Proof: Markov's inequality and E[W_n^{M_n} | S_n = -1] = n q_n ≤ 2 n π_n eventually.

theorem PoissonDeclumping.Bridge.tendsto_bridgeLaw_abs_cyclicSum_div_sub_one {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hM : IsCutoff M) (hmic : Microscopic μ G k M) (hC : NonClustering μ G k M) (hdiv : Filter.Tendsto (fun (n : ℕ) => ↑n * markProb μ G k n) (admissibleSizes μ) Filter.atTop) {ε : ℝ} (hε : 0 < ε) : Filter.Tendsto (fun (n : ℕ) => (Lukasiewicz.bridgeLaw μ n).real {ω : Fin n → ℤ | ε < |↑(Cyclic.cyclicSum (G (k n)) (↑(M n)) (List.ofFn ω)) / (↑n * markProb μ G k n) - 1|}) (admissibleSizes μ) (nhds 0)

Lemma lem:extreme_means(ii) (source lines 2012, 2023–2088): under Assumptions (M) and (C), if n π_n → ∞, then W_n^{M_n} / (n π_n) → 1 in probability under P(· | S_n = -1).

Proof (Chebyshev): Var(W_n^{M_n}) ≤ n q_n + b_2 + n² max_{sep} P(I_i = I_j = 1) - (n q_n)² (bridgeLaw_real_le_abs_cyclicSum_sub_le, sum_sum_cycEvent_inter_le); the diagonal term is n q_n = o((n π_n)²), the nearby pairs give b_2 = o((n π_n)²) (eventually_errorB2_le), and separated pairs have probability ≤ (1 + δ) p_n² (eventually_pairBridge_le), with p_n ∼ q_n ∼ π_n (Lemma lem:pnqn).