Removing the bridge conditioning: Lemma lem:error_est and Corollary cor:pip

Work package WP5 of the bridge plan. Source lines 1631–1658 (Lemma 4.2, Corollary 4.3), inventory step P08. Notation: Ψ_m(x) = walkProb μ m x, walkVecLaw μ n is the law of (X_1, …, X_n), bridgeLaw μ n its conditioning on S_n = -1, qProb/pProb as in Bridge/Truncation0.lean, π_n = markProb μ G k n.

Main statements

• exists_cond_take_le (Lemma lem:error_est, corrected as in F1): one constant C depending only on the toolkit such that, for N_n → ∞, m_n = o(N_n), z_n = o(a_{N_n}), eventually P(H(X_1..X_{m_n}) | S_{N_n} = k) ≤ C P(H(X_1..X_{m_n})) for every compatible endpoint |k| ≤ z_n (Ψ_{N_n}(k) ≠ 0) and every event H.
• cond_walkVecLaw_real_eq, qProb_le_inv_mul: q ≤ Ψ_n(-1)⁻¹ P(G(𝒯) = 1) at every n.
• exists_qProb_le_mul_markProb (Corollary cor:pip, at every admissible size, F5): q_n ≤ C π_n for all admissible n ≥ 1.

theorem PoissonDeclumping.Bridge.exists_cond_take_le {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) : ∃ (C : ℝ), 0 < C ∧ ∀ {N m : ℕ → ℕ} {z : ℕ → ℝ}, Filter.Tendsto N Filter.atTop Filter.atTop → ((fun (n : ℕ) => ↑(m n)) =o[Filter.atTop] fun (n : ℕ) => ↑(N n)) → (z =o[Filter.atTop] fun (n : ℕ) => a (N n)) → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (k : ℤ), |↑k| ≤ z n → walkProb μ (↑(N n)) k ≠ 0 → ∀ (H : List ℤ → Prop), (Lukasiewicz.walkVecLaw μ (N n))[|{ω : Fin (N n) → ℤ | ∑ i : Fin (N n), ω i = k}].real {ω : Fin (N n) → ℤ | H (List.take (m n) (List.ofFn ω))} ≤ C * (Lukasiewicz.walkVecLaw μ (m n)).real {ω : Fin (m n) → ℤ | H (List.ofFn ω)}

Lemma lem:error_est (source lines 1633–1648), corrected for periodic laws (F1): one constant C > 0, depending only on the toolkit, such that for all total lengths N_n → ∞, window lengths m_n = o(N_n) and endpoint ranges z_n = o(a_{N_n}), eventually in n, for every endpoint k with |k| ≤ z_n and Ψ_{N_n}(k) ≠ 0 and for every event H on the first m_n increments, P(H(X_1, …, X_{m_n}) | S_{N_n} = k) ≤ C P(H(X_1, …, X_{m_n})).

The source's sup_{|k| ≤ z_n} ranges over zero-probability endpoints in the periodic case; here k ranges over the compatible endpoints Ψ_{N_n}(k) ≠ 0, and the constant is uniform in N, m, z, n, k, H. Proof as in the source: Markov property at time m_n (cond_real_take), Ψ_{N_n}(k) ≥ L / (2 a_{N_n}) (eventually_bounds) and Ψ_{N_n - m_n} ≤ C / a_{N_n} (exists_le_div_of_le_two_mul).

theorem PoissonDeclumping.Bridge.cond_walkVecLaw_real_eq (μ : PMF ℕ) (n : ℕ) (s : ℤ) (A : Set (Fin n → ℤ)) : (Lukasiewicz.walkVecLaw μ n)[|{ω : Fin n → ℤ | ∑ i : Fin n, ω i = s}].real A = (walkProb μ (↑n) s)⁻¹ * (Lukasiewicz.walkVecLaw μ n).real ({ω : Fin n → ℤ | ∑ i : Fin n, ω i = s} ∩ A)

P(A | S_n = s) = Ψ_n(s)⁻¹ P(A, S_n = s) in ℝ.

theorem PoissonDeclumping.Bridge.qProb_le_inv_mul (μ : PMF ℕ) (G : PlaneTree → Prop) (M n : ℕ) : qProb μ G M n ≤ (walkProb μ (↑n) (-1))⁻¹ * (PlaneTree.bienayme μ).real {T : PlaneTree | G T}

The crude bound q ≤ Ψ_n(-1)⁻¹ P(G(𝒯) = 1), valid for every n and every cutoff.

theorem PoissonDeclumping.Bridge.exists_qProb_le_mul_markProb {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) (G : ℕ → PlaneTree → Prop) (k : ℕ → ℕ) {M : ℕ → ℕ} (hM : (fun (n : ℕ) => ↑(M n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), 1 ≤ n → PlaneTree.Admissible μ n → qProb μ (G (k n)) (M n) n ≤ C * markProb μ G k n

Corollary cor:pip (source lines 1651–1658), at every admissible size (correction F5): for any sequence M = o(n), there is C with q_n ≤ C π_n for every admissible n ≥ 1. Neither positivity nor divergence of M is needed.