Assembly of Theorems thm:PoissonApproximation and thm:PoissonApproximation2

Work package WP7 (second half) of the bridge plan. Source lines 1555–1595 (strategy), 2092–2143 (proof of Theorem 1.1, step P14) and 2305–2330 (proof of Theorem 1.2).

The only ingredient not proved upstream of this file is Proposition prop:b3bis (P4.8, b_3 → 0, endpoint-smoothing package). It enters as an explicit hypothesis: hb3 in the per-law theorems, ErrorB3Statement in the paper-level statements. Everything else is proved: Lemma lem:RW (markedCountLaw_eq), Lemma lem:truncate, Proposition prop:AGG (exists_paperTVDist_cyclicSum_le_errorTerms), Proposition prop:b1, Lemma lem:boundb2, Lemma lem:pnqn, Lemma lem:extreme_means (Bridge/ExtremeMeans.lean), Lemma lem:root_declumping(i)–(iii) and the toolkit derived from (H_α) (Stable.stableToolkit).

Main statements

• conditioned_real_markCount_mem: Lemma lem:RW for events.
• tendsto_paperTVDist_markedCountLaw_of_b3 (Theorem 1.1, bounded mean), tendsto_bridgeLaw_abs_cyclicSum_length_div_sub_one and poissonApproximation_divergent (Theorem 1.1, divergent mean: LLN and divergence in probability).
• poissonApproximation_of_b3: the two conclusions of PoissonApproximationStatement for one law with the toolkit, given (M), (C) and hb3.
• poissonApproximation2_of_b3: the two conclusions of PoissonApproximation2Statement for one law with the toolkit, given (S) for G, (C) for Ghat and hb3 for Ghat.
• ErrorB3Statement, poissonApproximationStatement_of_b3, poissonApproximation2Statement_of_b3: the paper-level statements from Proposition prop:b3bis.

Transfer between trees and the bridge

theorem PoissonDeclumping.Bridge.conditioned_real_markCount_mem (μ : PMF ℕ) (G : ℕ → PlaneTree → Prop) (k : ℕ → ℕ) (n : ℕ) (S : Set ℕ) : (PlaneTree.conditioned μ n).real {T : PlaneTree | PlaneTree.markCount (G (k n)) T ∈ S} = (Lukasiewicz.bridgeLaw μ n).real {ω : Fin n → ℤ | Cyclic.cyclicSum (G (k n)) (↑n) (List.ofFn ω) ∈ S}

Lemma lem:RW for events: for every set S ⊆ ℕ, P(#{u ∈ 𝒯^n : G_{k_n}(𝒯^n_u) = 1} ∈ S) = P(W_n^n ∈ S | S_n = -1).

Theorem thm:PoissonApproximation, bounded mean

theorem PoissonDeclumping.Bridge.tendsto_paperTVDist_markedCountLaw_of_b3 {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hM : IsCutoff M) (hmic : Microscopic μ G k M) (hC : NonClustering μ G k M) (hbd : ∃ (C : ℝ), ∀ᶠ (n : ℕ) in admissibleSizes μ, ↑n * markProb μ G k n ≤ C) (hb3 : ∀ (f : ℕ → ℕ → ℝ), (∀ (n w : ℕ), |f n w| ≤ 1) → Filter.Tendsto (fun (n : ℕ) => errorB3 μ (G (k n)) (M n) n (f n)) (admissibleSizes μ) (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => paperTVDist (markedCountLaw μ G k n) (ProbabilityTheory.poissonMeasure (↑n * markProb μ G k n).toNNReal)) (admissibleSizes μ) (nhds 0)

Theorem thm:PoissonApproximation(i), conditional on Proposition prop:b3bis (source lines 2104–2121): if (n π_n) is bounded and b_3 → 0 for every family of test functions bounded by 1, then d_TV(N_n, Po(n π_n)) → 0. Proof: Lemma lem:RW and Lemma lem:truncate(i) (W_n^n vs W_n^{M_n}), Proposition prop:AGG with the cyclic neighbourhoods (exists_paperTVDist_cyclicSum_le_errorTerms, test functions chosen for each admissible n), b_1, b_2 → 0 (Proposition prop:b1, Lemma lem:boundb2), hb3, and Lemma lem:truncate(ii) (Po(n q_n) vs Po(n π_n)).

Theorem thm:PoissonApproximation, divergent mean

theorem PoissonDeclumping.Bridge.tendsto_bridgeLaw_abs_cyclicSum_length_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)) (↑n) (List.ofFn ω)) / (↑n * markProb μ G k n) - 1|}) (admissibleSizes μ) (nhds 0)

Theorem thm:PoissonApproximation(ii), law of large numbers on the bridge (source lines 2126–2139): if n π_n → ∞, then W_n^n / (n π_n) → 1 in probability under P(· | S_n = -1). Proof: Lemma lem:extreme_means(ii) for W_n^{M_n}, and Markov's inequality for W_n^n - W_n^{M_n} ≥ 0, whose bridge expectation is n P(G(𝒯^n_{U_n}) = 1, |𝒯^n_{U_n}| > M_n) = o(n π_n) by (M) (integral_cyclicSum_sub_truncated).

theorem PoissonDeclumping.Bridge.poissonApproximation_divergent {μ : 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) : (∀ (ε : ℝ), 0 < ε → Filter.Tendsto (fun (n : ℕ) => (PlaneTree.conditioned μ n).real {T : PlaneTree | ε < |↑(PlaneTree.markCount (G (k n)) T) / (↑n * markProb μ G k n) - 1|}) (admissibleSizes μ) (nhds 0)) ∧ ∀ (K : ℕ), Filter.Tendsto (fun (n : ℕ) => (PlaneTree.conditioned μ n).real {T : PlaneTree | PlaneTree.markCount (G (k n)) T ≤ K}) (admissibleSizes μ) (nhds 0)

Theorem thm:PoissonApproximation(ii) (source lines 2126–2142): under (M) and (C), if n π_n → ∞, then N_n / (n π_n) → 1 in probability and N_n → ∞ in probability, where N_n = #{u ∈ 𝒯^n : G_{k_n}(𝒯^n_u) = 1}.

theorem PoissonDeclumping.Bridge.poissonApproximation_of_b3 {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hM : IsCutoff M) (hmic : Microscopic μ G k M) (hC : NonClustering μ G k M) (hb3 : (∃ (C : ℝ), ∀ᶠ (n : ℕ) in admissibleSizes μ, ↑n * markProb μ G k n ≤ C) → ∀ (f : ℕ → ℕ → ℝ), (∀ (n w : ℕ), |f n w| ≤ 1) → Filter.Tendsto (fun (n : ℕ) => errorB3 μ (G (k n)) (M n) n (f n)) (admissibleSizes μ) (nhds 0)) : ((∃ (C : ℝ), ∀ᶠ (n : ℕ) in admissibleSizes μ, ↑n * markProb μ G k n ≤ C) → Filter.Tendsto (fun (n : ℕ) => paperTVDist (markedCountLaw μ G k n) (ProbabilityTheory.poissonMeasure (↑n * markProb μ G k n).toNNReal)) (admissibleSizes μ) (nhds 0)) ∧ (Filter.Tendsto (fun (n : ℕ) => ↑n * markProb μ G k n) (admissibleSizes μ) Filter.atTop → (∀ (ε : ℝ), 0 < ε → Filter.Tendsto (fun (n : ℕ) => (PlaneTree.conditioned μ n).real {T : PlaneTree | ε < |↑(PlaneTree.markCount (G (k n)) T) / (↑n * markProb μ G k n) - 1|}) (admissibleSizes μ) (nhds 0)) ∧ ∀ (K : ℕ), Filter.Tendsto (fun (n : ℕ) => (PlaneTree.conditioned μ n).real {T : PlaneTree | PlaneTree.markCount (G (k n)) T ≤ K}) (admissibleSizes μ) (nhds 0))

Theorem thm:PoissonApproximation (source lines 305–329, proof 2092–2143) for one offspring law, conditional on Proposition prop:b3bis: the two conclusions of PoissonApproximationStatement for μ, G, k, given the toolkit, a cutoff M with (M) and (C), and the hypothesis hb3 (b_3 → 0 along admissible sizes whenever (n π_n) is bounded, for every family of test functions bounded by 1).

Theorem thm:PoissonApproximation2

theorem PoissonDeclumping.Bridge.poissonApproximation2_of_b3 {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hM : IsCutoff M) {B : Set ℕ} (hB0 : 0 < cB μ B) (hB1 : cB μ B < ⊤) (hS : StructuralMicroscopic μ a G k M) (hC : NonClustering μ (fun (j : ℕ) => PlaneTree.declumpedMark B (G j)) k M) (hb3 : (∃ (C : ℝ), ∀ᶠ (n : ℕ) in admissibleSizes μ, ↑n * markProb μ (fun (j : ℕ) => PlaneTree.declumpedMark B (G j)) k n ≤ C) → ∀ (f : ℕ → ℕ → ℝ), (∀ (n w : ℕ), |f n w| ≤ 1) → Filter.Tendsto (fun (n : ℕ) => errorB3 μ (PlaneTree.declumpedMark B (G (k n))) (M n) n (f n)) (admissibleSizes μ) (nhds 0)) : ((∃ (C : ℝ), ∀ᶠ (n : ℕ) in admissibleSizes μ, ↑n * markProb μ G k n ≤ C) → Filter.Tendsto (fun (n : ℕ) => paperTVDist (markedCountLaw μ (fun (j : ℕ) => PlaneTree.declumpedMark B (G j)) k n) (ProbabilityTheory.poissonMeasure ((cB μ B).toReal * (↑n * markProb μ G k n)).toNNReal)) (admissibleSizes μ) (nhds 0)) ∧ (Filter.Tendsto (fun (n : ℕ) => ↑n * markProb μ G k n) (admissibleSizes μ) Filter.atTop → ∀ (K : ℕ), Filter.Tendsto (fun (n : ℕ) => (PlaneTree.conditioned μ n).real {T : PlaneTree | PlaneTree.markCount (PlaneTree.declumpedMark B (G (k n))) T ≤ K}) (admissibleSizes μ) (nhds 0))

Theorem thm:PoissonApproximation2 (source lines 396–442, proof 2305–2330) for one offspring law, conditional on Proposition prop:b3bis for the declumped marks Ghat_k = declumpedMark B G_k: the two conclusions of PoissonApproximation2Statement. Proof: Lemma lem:root_declumping(iii) (microscopic_declumped) gives (M) for Ghat; with (C) for Ghat, Theorem thm:PoissonApproximation applies to Ghat. If (n π_n) is bounded, then so is (n π̂_n) and n π̂_n - c_B n π_n → 0 (Lemma lem:root_declumping(i)), and d_TV(Po(n π̂_n), Po(c_B n π_n)) ≤ |n π̂_n - c_B n π_n|; if n π_n → ∞, then n π̂_n → ∞ (Lemma lem:root_declumping(ii)) and the declumped count diverges in probability.

The paper's statements, conditional on Proposition prop:b3bis

def PoissonDeclumping.Bridge.ErrorB3Statement : Prop

Proposition prop:b3bis (P4.8, source lines 1860–1995) in the form used by the assembly: for every offspring law with the stable toolkit, every cutoff and marks with (M), if (n π_n) is bounded then b_3 → 0 along admissible sizes for every family of test functions bounded by 1. This is the export of the endpoint-smoothing package.

Equations

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

theorem PoissonDeclumping.Bridge.poissonApproximationStatement_of_b3 (hb3 : ErrorB3Statement) : PoissonApproximationStatement

Theorem thm:PoissonApproximation, the paper's statement, from Proposition prop:b3bis (ErrorB3Statement) and the stable toolkit derived from (H_α).

theorem PoissonDeclumping.Bridge.poissonApproximation2Statement_of_b3 (hb3 : ErrorB3Statement) : PoissonApproximation2Statement

Theorem thm:PoissonApproximation2, the paper's statement, from Proposition prop:b3bis (ErrorB3Statement, applied to the declumped marks) and the stable toolkit derived from (H_α).