Deterministic comparison of raw and declumped occurrences

The two set inclusions in the proof of Lemma lem:declump_to_raw, source lines 2361–2389. No probability assumptions are required. Propagation is the paper's stated hypothesis, not a substitute for the conclusion.

theorem PoissonDeclumping.PlaneTree.declumped_count_pos_imp_raw_count_pos {B : Set ℕ} {G : PlaneTree → Prop} {T : PlaneTree} (h : 0 < markCount (declumpedMark B G) T) : 0 < markCount G T

A declumped occurrence contains a marked child and hence a raw occurrence.

theorem PoissonDeclumping.PlaneTree.raw_count_zero_imp_declumped_count_zero {B : Set ℕ} {G : PlaneTree → Prop} {T : PlaneTree} (h : markCount G T = 0) : markCount (declumpedMark B G) T = 0

Absence of raw occurrences implies absence of declumped occurrences.

theorem PoissonDeclumping.PlaneTree.marked_root_of_no_declumped {B : Set ℕ} {G : PlaneTree → Prop} {T : PlaneTree} (hprop : PropagatesOutside B G) (hraw : 0 < markCount G T) (hno : markCount (declumpedMark B G) T = 0) : G T

With no declumped occurrence, propagation carries any raw mark to the root. This is the deterministic core of Lemma lem:declump_to_raw.

theorem PoissonDeclumping.PlaneTree.raw_zero_subset_declumped_zero (B : Set ℕ) (G : PlaneTree → Prop) : {T : PlaneTree | markCount G T = 0} ⊆ {T : PlaneTree | markCount (declumpedMark B G) T = 0}

First event inclusion used in the probabilistic comparison.

theorem PoissonDeclumping.PlaneTree.declumped_zero_subset_raw_zero_union_root {B : Set ℕ} {G : PlaneTree → Prop} (hprop : PropagatesOutside B G) : {T : PlaneTree | markCount (declumpedMark B G) T = 0} ⊆ {T : PlaneTree | markCount G T = 0} ∪ {T : PlaneTree | G T}

The discrepancy between the two zero events requires a mark at the root.