Truncation: Lemma lem:truncate and Lemma lem:pnqn

Work package WP5 of the bridge plan. Source lines 1662–1696 (Lemma 4.4, P09) and 1732–1788 (Lemma 4.5, P10). Notation: W_n^M = cyclicSum (G (k n)) M (List.ofFn ω) under bridgeLaw μ n = P(· | S_n = -1), q_n = qProb μ (G (k n)) (M n) n, p_n = pProb μ (G (k n)) (M n), π_n = markProb μ G k n, 𝒯^n_{U_n} ~ uniformFringeLaw μ n. "(n π_n) bounded" is the hypothesis ∃ C, ∀ᶠ n in admissibleSizes μ, n π_n ≤ C of PoissonApproximationStatement.

Main statements

• tendsto_paperTVDist_cyclicSum_truncated (Lemma lem:truncate(i)): under (M) and bounded n π_n, d_TV(W_n^{M_n}, W_n^∞) → 0 along admissible sizes; tendsto_paperTVDist_cyclicSum_markedCountLaw: the same against markedCountLaw μ G k n.
• tendsto_mul_qProb_sub_mul_markProb, tendsto_paperTVDist_poisson_qProb_markProb (Lemma lem:truncate(ii)): n q_n - n π_n → 0 and d_TV(Po(n q_n), Po(n π_n)) → 0.
• eventually_abs_qProb_sub_markProb_le, isEquivalent_qProb_markProb: q_n ∼ π_n under (M).
• isLittleO_walkVecLaw_firstMarked_abs_sum_gt(_admissible) (Lemma lem:pnqn(i)): P(I_1^{(M_n)} = 1, |S_{M_n}| > r_n) = o(p_n), r_n = √(a_{M_n} a_n) (needs only the toolkit and the cutoff; marginal tightness replaces functional tightness, F6).
• isEquivalent_pProb_qProb, isEquivalent_pProb_qProb_markProb (Lemma lem:pnqn(ii)): p_n ∼ q_n (toolkit and cutoff only; ratio limit at compatible endpoints, F4) and q_n ∼ π_n (Assumption (M)).

Lemma lem:truncate needs neither the toolkit nor IsCutoff; π_n = 0 is allowed throughout (IsEquivalent and cond of a null event handle it, F13).

theorem PoissonDeclumping.Bridge.measureReal_inter_eq_mul_cond {Ω : Type u_1} [MeasurableSpace Ω] (ν : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure ν] {s : Set Ω} (hs : MeasurableSet s) (t : Set Ω) : ν.real (s ∩ t) = ν.real s * ν[|s].real t

ν(s ∩ t) = ν(s) ν(t | s) in ℝ, also when ν(s) = 0.

theorem PoissonDeclumping.Bridge.qProb_eq_sub_mul_cond (μ : PMF ℕ) (G : PlaneTree → Prop) (M n : ℕ) : qProb μ G M n = (uniformFringeLaw μ n).real {T : PlaneTree | G T} - (uniformFringeLaw μ n).real {T : PlaneTree | G T} * (uniformFringeLaw μ n)[|{T : PlaneTree | G T}].real {T : PlaneTree | M < T.vertexCount}

q = P(G(𝒯^n_{U_n}) = 1) (1 - P(|𝒯^n_{U_n}| > M | G(𝒯^n_{U_n}) = 1)).

theorem PoissonDeclumping.Bridge.eventually_abs_qProb_sub_markProb_le {μ : PMF ℕ} {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hmic : Microscopic μ G k M) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in admissibleSizes μ, |qProb μ (G (k n)) (M n) n - markProb μ G k n| ≤ ε * markProb μ G k n

Under Assumption (M): |q_n - π_n| ≤ ε π_n eventually along admissible sizes (source lines 1694–1695: q_n - π_n = (P(G(𝒯^n_{U_n}) = 1) - π_n) - P(G(𝒯^n_{U_n}) = 1, |𝒯^n_{U_n}| > M_n)).

Lemma lem:truncate

theorem PoissonDeclumping.Bridge.tendsto_paperTVDist_cyclicSum_truncated {μ : PMF ℕ} {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hmic : Microscopic μ G k M) (hbd : ∃ (C : ℝ), ∀ᶠ (n : ℕ) in admissibleSizes μ, ↑n * markProb μ G k n ≤ C) : Filter.Tendsto (fun (n : ℕ) => paperTVDist (MeasureTheory.Measure.map (fun (ω : Fin n → ℤ) => Cyclic.cyclicSum (G (k n)) (↑(M n)) (List.ofFn ω)) (Lukasiewicz.bridgeLaw μ n)) (MeasureTheory.Measure.map (fun (ω : Fin n → ℤ) => Cyclic.cyclicSum (G (k n)) ⊤ (List.ofFn ω)) (Lukasiewicz.bridgeLaw μ n))) (admissibleSizes μ) (nhds 0)

Lemma lem:truncate(i) (source lines 1675–1693): under Assumption (M) and bounded n π_n, d_TV(W_n^{M_n}, W_n^n) → 0 under P(· | S_n = -1), where W_n^n = W_n^∞ is the full count (markedCountLaw_eq). Proof: the coupling bound d_TV ≤ n P(G(𝒯^n_{U_n}) = 1, |𝒯^n_{U_n}| > M_n) (paperTVDist_cyclicSum_truncated_le), which is o(n π_n) by (M).

theorem PoissonDeclumping.Bridge.tendsto_paperTVDist_cyclicSum_markedCountLaw {μ : PMF ℕ} {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hmic : Microscopic μ G k M) (hbd : ∃ (C : ℝ), ∀ᶠ (n : ℕ) in admissibleSizes μ, ↑n * markProb μ G k n ≤ C) : Filter.Tendsto (fun (n : ℕ) => paperTVDist (MeasureTheory.Measure.map (fun (ω : Fin n → ℤ) => Cyclic.cyclicSum (G (k n)) (↑(M n)) (List.ofFn ω)) (Lukasiewicz.bridgeLaw μ n)) (markedCountLaw μ G k n)) (admissibleSizes μ) (nhds 0)

Lemma lem:truncate(i), with the law of the marked count #{u ∈ 𝒯^n : G_{k_n}(𝒯^n_u)} (Lemma lem:RW, markedCountLaw_eq).

theorem PoissonDeclumping.Bridge.tendsto_mul_qProb_sub_mul_markProb {μ : PMF ℕ} {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hmic : Microscopic μ G k M) (hbd : ∃ (C : ℝ), ∀ᶠ (n : ℕ) in admissibleSizes μ, ↑n * markProb μ G k n ≤ C) : Filter.Tendsto (fun (n : ℕ) => ↑n * qProb μ (G (k n)) (M n) n - ↑n * markProb μ G k n) (admissibleSizes μ) (nhds 0)

Lemma lem:truncate(ii), first half (source lines 1694–1696): n q_n - n π_n → 0.

theorem PoissonDeclumping.Bridge.tendsto_paperTVDist_poisson_qProb_markProb {μ : PMF ℕ} {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hmic : Microscopic μ G k M) (hbd : ∃ (C : ℝ), ∀ᶠ (n : ℕ) in admissibleSizes μ, ↑n * markProb μ G k n ≤ C) : Filter.Tendsto (fun (n : ℕ) => paperTVDist (ProbabilityTheory.poissonMeasure (↑n * qProb μ (G (k n)) (M n) n).toNNReal) (ProbabilityTheory.poissonMeasure (↑n * markProb μ G k n).toNNReal)) (admissibleSizes μ) (nhds 0)

Lemma lem:truncate(ii) (source line 1696): d_TV(Po(n q_n), Po(n π_n)) → 0, via d_TV(Po(x), Po(y)) ≤ |x - y|.

Lemma lem:pnqn

theorem PoissonDeclumping.Bridge.isEquivalent_qProb_markProb {μ : PMF ℕ} {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hmic : Microscopic μ G k M) : Asymptotics.IsEquivalent (admissibleSizes μ) (fun (n : ℕ) => qProb μ (G (k n)) (M n) n) (markProb μ G k)

q_n ∼ π_n under Assumption (M) (source lines 1778–1783, uniform-vertex representation).

theorem PoissonDeclumping.Bridge.ae_dvd_sum_add {μ : PMF ℕ} {a : ℕ → ℝ} {d : ℕ} {L : ℝ} (hloc : LatticeLocal μ a d L) (m : ℕ) : ∀ᵐ (b : Fin m → ℤ) ∂Lukasiewicz.walkVecLaw μ m, ↑d ∣ ∑ i : Fin m, b i + ↑m

The walk lives on its lattice: d ∣ S_m + m almost surely (from LatticeLocal.support).

theorem PoissonDeclumping.Bridge.indicator_one_mem_Icc {X : Type u_1} (s : Set X) (x : X) : 0 ≤ s.indicator 1 x ∧ s.indicator 1 x ≤ 1

A {0,1}-indicator takes values in [0, 1].

theorem PoissonDeclumping.Bridge.integrable_walkVecLaw_of_abs_le (μ : PMF ℕ) {m : ℕ} {f : (Fin m → ℤ) → ℝ} (C : ℝ) (h : ∀ (b : Fin m → ℤ), |f b| ≤ C) : MeasureTheory.Integrable f (Lukasiewicz.walkVecLaw μ m)

A bounded real function of (X_1, …, X_m) is integrable.

theorem PoissonDeclumping.Bridge.isLittleO_walkVecLaw_firstMarked_abs_sum_gt {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) (G : ℕ → PlaneTree → Prop) (k : ℕ → ℕ) {M : ℕ → ℕ} (hM : IsCutoff M) : (fun (n : ℕ) => (Lukasiewicz.walkVecLaw μ (M n)).real {ω : Fin (M n) → ℤ | Cyclic.FirstMarked (G (k n)) (↑(M n)) (List.ofFn ω) ∧ √(a (M n) * a n) < |↑(∑ i : Fin (M n), ω i)|}) =o[Filter.atTop] fun (n : ℕ) => pProb μ (G (k n)) (M n)

Lemma lem:pnqn(i) (source lines 1747–1771), along atTop: with r_n = √(a_{M_n} a_n), P(I_1^{(M_n)} = 1, |S_{M_n}| > r_n) = o(p_n). Only the cutoff properties and marginal tightness (tight, correction F6) are used.

theorem PoissonDeclumping.Bridge.isLittleO_walkVecLaw_firstMarked_abs_sum_gt_admissible {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) (G : ℕ → PlaneTree → Prop) (k : ℕ → ℕ) {M : ℕ → ℕ} (hM : IsCutoff M) : (fun (n : ℕ) => (Lukasiewicz.walkVecLaw μ (M n)).real {ω : Fin (M n) → ℤ | Cyclic.FirstMarked (G (k n)) (↑(M n)) (List.ofFn ω) ∧ √(a (M n) * a n) < |↑(∑ i : Fin (M n), ω i)|}) =o[admissibleSizes μ] fun (n : ℕ) => pProb μ (G (k n)) (M n)

Lemma lem:pnqn(i) along admissible sizes.

theorem PoissonDeclumping.Bridge.isEquivalent_pProb_qProb {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) (G : ℕ → PlaneTree → Prop) (k : ℕ → ℕ) {M : ℕ → ℕ} (hM : IsCutoff M) : Asymptotics.IsEquivalent (admissibleSizes μ) (fun (n : ℕ) => pProb μ (G (k n)) (M n)) fun (n : ℕ) => qProb μ (G (k n)) (M n) n

Lemma lem:pnqn(ii), first half (source lines 1740–1775): p_n ∼ q_n, by the Markov property at time M_n, the ratio limit Ψ_{n-M_n}(-1 - S_{M_n}) / Ψ_n(-1) → 1 on {|S_{M_n}| ≤ r_n} at compatible endpoints (correction F4: S_{M_n} ≡ -M_n (mod d) almost surely), the bound Ψ_{n-M_n}(·) / Ψ_n(-1) ≤ C, and part (i). No assumption on the marks.

theorem PoissonDeclumping.Bridge.isEquivalent_pProb_qProb_markProb {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hM : IsCutoff M) (hmic : Microscopic μ G k M) : (Asymptotics.IsEquivalent (admissibleSizes μ) (fun (n : ℕ) => pProb μ (G (k n)) (M n)) fun (n : ℕ) => qProb μ (G (k n)) (M n) n) ∧ Asymptotics.IsEquivalent (admissibleSizes μ) (fun (n : ℕ) => qProb μ (G (k n)) (M n) n) (markProb μ G k)

Lemma lem:pnqn(ii) (source lines 1732–1788): under Assumption (M), p_n ∼ q_n ∼ π_n along admissible sizes. (π_n = 0 is allowed: IsEquivalent then forces p_n = q_n = 0.)