Lemma lem:declump_to_raw for size-conditioned Bienaymé trees

Source lines 2343–2401. The abstract reduction PlaneTree.declump_to_raw assumes that every law in the family is a probability measure. Here we only require this eventually along the limit filter (declump_to_raw_of_eventually), and specialize to the family n ↦ 𝒯^n = conditioned μ n along the filter admissibleAtTop μ of large admissible sizes, where the conditioned laws are probability measures (conditioned_declump_to_raw). Measurability of counts is automatic for the discrete σ-algebra on finite plane trees.

theorem PoissonDeclumping.PlaneTree.declump_to_raw_of_eventually_of_measurable {mT : MeasurableSpace PlaneTree} {ι : Type u_1} (l : Filter ι) (μ : ι → MeasureTheory.Measure PlaneTree) (hμ : ∀ᶠ (i : ι) in l, MeasureTheory.IsProbabilityMeasure (μ i)) (B : Set ℕ) (G : ι → PlaneTree → Prop) (rate : ι → NNReal) (hprop : ∀ (i : ι), PropagatesOutside B (G i)) (hmeas : ∀ (i : ι), Measurable (markCount (declumpedMark B (G i)))) (hroot : Filter.Tendsto (fun (i : ι) => (μ i).real {T : PlaneTree | G i T}) l (nhds 0)) (htv : Filter.Tendsto (fun (i : ι) => paperTVDist (MeasureTheory.Measure.map (markCount (declumpedMark B (G i))) (μ i)) (ProbabilityTheory.poissonMeasure (rate i))) l (nhds 0)) : Filter.Tendsto (fun (i : ι) => (μ i).real {T : PlaneTree | markCount (G i) T = 0} - Real.exp (-↑(rate i))) l (nhds 0)

Lemma lem:declump_to_raw for laws that are only eventually probability measures, on an arbitrary measurable structure on trees (with measurable declumped counts).

theorem PoissonDeclumping.PlaneTree.declump_to_raw_of_eventually {ι : Type u_1} (l : Filter ι) (μ : ι → MeasureTheory.Measure PlaneTree) (hμ : ∀ᶠ (i : ι) in l, MeasureTheory.IsProbabilityMeasure (μ i)) (B : Set ℕ) (G : ι → PlaneTree → Prop) (rate : ι → NNReal) (hprop : ∀ (i : ι), PropagatesOutside B (G i)) (hroot : Filter.Tendsto (fun (i : ι) => (μ i).real {T : PlaneTree | G i T}) l (nhds 0)) (htv : Filter.Tendsto (fun (i : ι) => paperTVDist (MeasureTheory.Measure.map (markCount (declumpedMark B (G i))) (μ i)) (ProbabilityTheory.poissonMeasure (rate i))) l (nhds 0)) : Filter.Tendsto (fun (i : ι) => (μ i).real {T : PlaneTree | markCount (G i) T = 0} - Real.exp (-↑(rate i))) l (nhds 0)

Lemma lem:declump_to_raw for laws on finite plane trees (discrete σ-algebra) that are eventually probability measures along the filter l.

theorem PoissonDeclumping.PlaneTree.conditioned_declump_to_raw (μ : PMF ℕ) (B : Set ℕ) (G : ℕ → PlaneTree → Prop) (rate : ℕ → NNReal) (hprop : ∀ (n : ℕ), PropagatesOutside B (G n)) (hroot : Filter.Tendsto (fun (n : ℕ) => (conditioned μ n).real {T : PlaneTree | G n T}) (admissibleAtTop μ) (nhds 0)) (htv : Filter.Tendsto (fun (n : ℕ) => paperTVDist (MeasureTheory.Measure.map (markCount (declumpedMark B (G n))) (conditioned μ n)) (ProbabilityTheory.poissonMeasure (rate n))) (admissibleAtTop μ) (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => (conditioned μ n).real {T : PlaneTree | markCount (G n) T = 0} - Real.exp (-↑(rate n))) (admissibleAtTop μ) (nhds 0)

Lemma lem:declump_to_raw (source lines 2343–2357) for the size-conditioned Bienaymé trees 𝒯^n, as n → ∞ along admissible sizes: if the marks G_n (the paper's G_{k_n}) propagate to parents of degree outside B, 𝐏(G_n(𝒯^n)) → 0, and the declumped count N̂_n(𝒯^n) is close in total variation to Po(λ_n), then 𝐏(N_n(𝒯^n) = 0) - e^{-λ_n} → 0.

The size n itself is the index. The statement holds for every offspring law μ; for the paper's critical μ with μ_1 ≠ 1 the filter admissibleAtTop μ is proper (admissibleAtTop_neBot), so the limit statement is not vacuous.