From declumped Poisson counts to raw zero events

The probabilistic reduction in Lemma lem:declump_to_raw, source lines 2343–2399, for arbitrary laws on finite plane trees and arbitrary limit filters. This does not construct the conditioned Bienaymé law or prove its hypotheses.

The finite-measure sandwich also holds for nonmeasurable raw/root events, with Measure.real interpreted using the outer extension. Applications to the paper use measurable events (in particular, the discrete tree sigma algebra). The declumped count must be measurable when its distribution is pushed forward.

theorem PoissonDeclumping.PlaneTree.zero_probability_sandwich [MeasurableSpace PlaneTree] {B : Set ℕ} {G : PlaneTree → Prop} (μ : MeasureTheory.Measure PlaneTree) [MeasureTheory.IsFiniteMeasure μ] (hprop : PropagatesOutside B G) : 0 ≤ μ.real {T : PlaneTree | markCount (declumpedMark B G) T = 0} - μ.real {T : PlaneTree | markCount G T = 0} ∧ μ.real {T : PlaneTree | markCount (declumpedMark B G) T = 0} - μ.real {T : PlaneTree | markCount G T = 0} ≤ μ.real {T : PlaneTree | G T}

The difference of the zero-event probabilities is between zero and the root-mark probability, exactly as in the proof of Lemma lem:declump_to_raw.

theorem PoissonDeclumping.PlaneTree.abs_raw_zero_sub_declumped_zero_le [MeasurableSpace PlaneTree] {B : Set ℕ} {G : PlaneTree → Prop} (μ : MeasureTheory.Measure PlaneTree) [MeasureTheory.IsFiniteMeasure μ] (hprop : PropagatesOutside B G) : |μ.real {T : PlaneTree | markCount G T = 0} - μ.real {T : PlaneTree | markCount (declumpedMark B G) T = 0}| ≤ μ.real {T : PlaneTree | G T}

Absolute version of the zero-event sandwich.

theorem PoissonDeclumping.PlaneTree.raw_zero_poisson_error_le [MeasurableSpace PlaneTree] {B : Set ℕ} {G : PlaneTree → Prop} (μ : MeasureTheory.Measure PlaneTree) [MeasureTheory.IsProbabilityMeasure μ] (rate : NNReal) (hprop : PropagatesOutside B G) (hmeas : Measurable (markCount (declumpedMark B G))) : |μ.real {T : PlaneTree | markCount G T = 0} - Real.exp (-↑rate)| ≤ μ.real {T : PlaneTree | G T} + paperTVDist (MeasureTheory.Measure.map (markCount (declumpedMark B G)) μ) (ProbabilityTheory.poissonMeasure rate)

A finite-parameter error bound underlying Lemma lem:declump_to_raw. No boundedness assumption on the Poisson rate is needed.

theorem PoissonDeclumping.PlaneTree.declump_to_raw [MeasurableSpace PlaneTree] {ι : Type u_1} (l : Filter ι) (μ : ι → MeasureTheory.Measure PlaneTree) [∀ (i : ι), 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)

The abstract law-level reduction of Lemma lem:declump_to_raw.

An arbitrary filter permits subsequent use along admissible tree sizes. The conditioned Bienaymé law and the hypotheses for its application remain separate obligations; they are not supplied by this reduction.