A criterion for Assumption (M): Lemma lem:M

Source lines 1015–1049 (Lemma 3.3 and its proof), 227–233 (Assumption (M)), inventory L3.3, proof step P02. Notation: Ψ_m(x) = walkProb μ m x, 𝒯 ~ bienayme μ, 𝒯^n_{U_n} ~ uniformFringeLaw μ n.

Corollary cor:cyclicshift (Cyclic.uniformFringeLaw_real_eq) gives P(H(𝒯^n_{U_n})) = E[1_{H(𝒯)} R_n(|𝒯|)] with R_n(m) = Ψ_{n-m}(0) / Ψ_n(-1). The proof splits marked trees at the cutoff:

• small trees (|𝒯| ≤ m_n = o(n)): R_n(m) → 1 uniformly over compatible m (in the periodic case R_n(m) = 0 at incompatible m, correction F4). Compatibility is automatic: P(|𝒯| = m) > 0 → d ∣ m - 1 (dvd_sub_one_of_admissible, from LatticeLocal.support and Dwass), and 𝒯 has an admissible size almost surely (ae_admissible_vertexCount). Exports: eventually_abs_walkProb_div_sub_one_le (the ratio limit) and eventually_abs_uniformFringeLaw_real_sub_le (|P(H(𝒯^n_{U_n})) - P(H(𝒯))| ≤ ε P(H(𝒯)) uniformly over properties H forcing |T| ≤ m_n);
• large trees: R_n(m) ≤ Ψ_n(-1)⁻¹ ≤ a_n / c (uniformFringeLaw_real_le, exists_uniformFringeLaw_real_le_mul, from Ψ ≤ 1 and exists_lower_bound_neg_one).

microscopic_of_tail is Lemma lem:M without the hypothesis π_n > 0, which the proof does not need: at π_n = 0 both sides of the first half of (M) vanish and the conditional probability of the second half is 0 (cond of a null event, correction F13). microscopic_of_tail_of_eventually_pos is the statement with the source's hypothesis.

theorem PoissonDeclumping.Bridge.ae_admissible_vertexCount (μ : PMF ℕ) : ∀ᵐ (T : PlaneTree) ∂PlaneTree.bienayme μ, PlaneTree.Admissible μ T.vertexCount

𝒯 has an admissible size almost surely.

theorem PoissonDeclumping.Bridge.dvd_sub_one_of_admissible {μ : PMF ℕ} {a : ℕ → ℝ} {d : ℕ} {L : ℝ} (hloc : LatticeLocal μ a d L) {m : ℕ} (h : PlaneTree.Admissible μ m) : ↑d ∣ ↑m - 1

Compatibility of admissible sizes with the lattice: P(|𝒯| = m) > 0 → d ∣ m - 1.

theorem PoissonDeclumping.Bridge.eventually_abs_walkProb_div_sub_one_le {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {m : ℕ → ℕ} (hm : (fun (n : ℕ) => ↑(m n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in admissibleSizes μ, ∀ j ≤ m n, PlaneTree.Admissible μ j → |walkProb μ (↑n - ↑j) 0 / walkProb μ (↑n) (-1) - 1| ≤ ε

Uniform ratio limit over compatible sizes (TF5 with x = 0, y = -1, N n = n): for m_n = o(n) and ε > 0, eventually along admissible sizes, |Ψ_{n-j}(0) / Ψ_n(-1) - 1| ≤ ε for every admissible size j ≤ m_n. In the periodic case the restriction to admissible j is necessary (source lines 1033, 965, 1293).

theorem PoissonDeclumping.Bridge.integrable_bienayme_of_abs_le (μ : PMF ℕ) {f : PlaneTree → ℝ} (C : ℝ) (h : ∀ (T : PlaneTree), |f T| ≤ C) : MeasureTheory.Integrable f (PlaneTree.bienayme μ)

A bounded real function of a tree is bienayme μ-integrable.

theorem PoissonDeclumping.Bridge.uniformFringeLaw_real_le (μ : PMF ℕ) (n : ℕ) (H : PlaneTree → Prop) : (uniformFringeLaw μ n).real {T : PlaneTree | H T} ≤ (walkProb μ (↑n) (-1))⁻¹ * (PlaneTree.bienayme μ).real {T : PlaneTree | H T}

P(H(𝒯^n_{U_n})) ≤ Ψ_n(-1)⁻¹ P(H(𝒯)), for every n and every property H (from Corollary cor:cyclicshift and Ψ ≤ 1; this is the bound R_n(m) ≤ Ψ_n(-1)⁻¹ of source line 1034).

theorem PoissonDeclumping.Bridge.exists_uniformFringeLaw_real_le_mul {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), PlaneTree.Admissible μ n → ∀ (H : PlaneTree → Prop), (uniformFringeLaw μ n).real {T : PlaneTree | H T} ≤ C * a n * (PlaneTree.bienayme μ).real {T : PlaneTree | H T}

The large-tree bound of source line 1034 with a constant from the toolkit: at every admissible n and for every H, P(H(𝒯^n_{U_n})) ≤ C a_n P(H(𝒯)).

theorem PoissonDeclumping.Bridge.eventually_abs_uniformFringeLaw_real_sub_le {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {m : ℕ → ℕ} (hm : (fun (n : ℕ) => ↑(m n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in admissibleSizes μ, ∀ (H : PlaneTree → Prop), (∀ (T : PlaneTree), H T → T.vertexCount ≤ m n) → |(uniformFringeLaw μ n).real {T : PlaneTree | H T} - (PlaneTree.bienayme μ).real {T : PlaneTree | H T}| ≤ ε * (PlaneTree.bienayme μ).real {T : PlaneTree | H T}

Small fringe trees (source lines 1031–1034, 965, 1293; P02, first half): for m_n = o(n) and ε > 0, eventually along admissible sizes, uniformly over all properties H that force |T| ≤ m_n, |P(H(𝒯^n_{U_n})) - P(H(𝒯))| ≤ ε P(H(𝒯)).

theorem PoissonDeclumping.Bridge.measureReal_split_vertexCount (ν : MeasureTheory.Measure PlaneTree) [MeasureTheory.IsFiniteMeasure ν] (H : PlaneTree → Prop) (m : ℕ) : ν.real {T : PlaneTree | H T} = ν.real {T : PlaneTree | H T ∧ T.vertexCount ≤ m} + ν.real {T : PlaneTree | H T ∧ m < T.vertexCount}

Splitting a property of trees at a size cutoff m.

theorem PoissonDeclumping.Bridge.cond_real_apply_of_discrete (ν : MeasureTheory.Measure PlaneTree) (s t : Set PlaneTree) : ν[|s].real t = (ν.real s)⁻¹ * ν.real (s ∩ t)

ν(t | s) = ν(s)⁻¹ ν(s ∩ t) in ℝ (both sides vanish when ν(s) = 0).

theorem PoissonDeclumping.Bridge.microscopic_of_tail {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hM : IsCutoff M) (h : Filter.Tendsto (fun (n : ℕ) => a n * (PlaneTree.bienayme μ)[|{T : PlaneTree | G (k n) T}].real {T : PlaneTree | M n < T.vertexCount}) (admissibleSizes μ) (nhds 0)) : Microscopic μ G k M

Lemma lem:M (source lines 1015–1049), in a slightly stronger form: no positivity of π_n is needed. If a_n P(|𝒯| > M_n | G_{k_n}(𝒯) = 1) → 0 along admissible sizes, then Assumption (M) holds. At indices with π_n = 0 both sides of the first half vanish and the conditional probability in the second half is 0 (cond of a null event).

theorem PoissonDeclumping.Bridge.microscopic_of_tail_of_eventually_pos {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hM : IsCutoff M) (_hpos : ∀ᶠ (n : ℕ) in admissibleSizes μ, 0 < markProb μ G k n) (h : Filter.Tendsto (fun (n : ℕ) => a n * (PlaneTree.bienayme μ)[|{T : PlaneTree | G (k n) T}].real {T : PlaneTree | M n < T.vertexCount}) (admissibleSizes μ) (nhds 0)) : Microscopic μ G k M

Lemma lem:M exactly as stated in the source (line 1015–1026), with the hypothesis "π_n > 0 for all sufficiently large (admissible) n", which the proof does not need (see microscopic_of_tail).