The cut-and-graft bound (Lemma lem:cut_graft)

Source lines 2512–2546 (statement) and 2557–2621 (proof); inventory L6.1, P18.

Let 𝓔 be an event on finite plane trees, (𝓠_m)_{m ∈ I} a finite family of events with 𝐏(𝒯 ∈ 𝓠_m) > 0, 𝓡 ⊆ 𝒜_ℓ and τ : 𝓡 → I such that (a) A[S'] ∈ 𝓔 for every A ∈ 𝓡 and S' ∈ 𝓠_{τ(A)}, and (b) whenever |T| ≥ ℓ+1, T ∈ 𝓔 and T_{u_{ℓ+1}(T)} ∈ 𝓔, one has Cut_ℓ(T) ∈ 𝓡 and T_{u_{ℓ+1}(T)} ∈ 𝓠_{τ(Cut_ℓ(T))}. Then 𝐏(|𝒯| ≥ ℓ+1, 𝒯 ∈ 𝓔, 𝒯_{u_{ℓ+1}(𝒯)} ∈ 𝓔) ≤ 𝐏(𝒯 ∈ 𝓔) max_{m ∈ I} 𝐏(𝒯 ∈ 𝓔 | 𝒯 ∈ 𝓠_m).

• PlaneTree.lem_cut_graft: the statement in ℝ≥0∞, with conditional probabilities given by ProbabilityTheory.cond and the maximum Finset.univ.sup' over a nonempty finite index type I (the paper writes max_{m ∈ I} without stating I ≠ ∅; all its applications have I = {0} or I = {0, …, k}).
• PlaneTree.lem_cut_graft_real: the same inequality between real probabilities, whose left-hand side is the paper's A_n(ℓ) set (cf. PoissonDeclumping.pairProb).
• PlaneTree.cut_graft_bound_aux: the core weighted estimate, for an arbitrary index type and a total selector, with any constant c such that 𝐏(𝓔 ∩ 𝓠_m) ≤ c 𝐏(𝓠_m).

The proof is the paper's: by the cut-and-graft factorization 𝐏(𝒯 = A[S]) = w(A) 𝐏(𝒯 = S), the left-hand side is at most ∑_{A ∈ 𝓡} w(A) 𝐏(𝓔 ∩ 𝓠_{τ(A)}), while uniqueness of the decomposition and (a) give ∑_{A ∈ 𝓡} w(A) 𝐏(𝓠_{τ(A)}) ≤ 𝐏(𝓔). (The paper groups the sum by m through W_m = ∑_{τ(A) = m} w(A); we sum over A directly.)

The inequality holds for every offspring law μ: criticality and μ_1 ≠ 1 (which make bienayme μ a probability measure) are not needed, so they are not assumed.

theorem PoissonDeclumping.PlaneTree.cut_graft_bound_aux (μ : PMF ℕ) (ℓ : ℕ) (E : Set PlaneTree) {I : Type u_1} (Q : I → Set PlaneTree) (R : Set MarkedTree) (hR : R ⊆ cutFamily ℓ) (τ : MarkedTree → I) (ha : ∀ A ∈ R, ∀ S ∈ Q (τ A), A.graft S ∈ E) (hb : ∀ (T : PlaneTree), ℓ + 1 ≤ T.vertexCount → T ∈ E → T.fringeAt ℓ ∈ E → cut ℓ T ∈ R ∧ T.fringeAt ℓ ∈ Q (τ (cut ℓ T))) (c : ENNReal) (hc : ∀ (m : I), (bienayme μ) (E ∩ Q m) ≤ c * (bienayme μ) (Q m)) : (bienayme μ) {T : PlaneTree | ℓ + 1 ≤ T.vertexCount ∧ T ∈ E ∧ T.fringeAt ℓ ∈ E} ≤ c * (bienayme μ) E

Core estimate of Lemma lem:cut_graft (total selector τ, arbitrary index type, and any constant c with 𝐏(𝓔 ∩ 𝓠_m) ≤ c 𝐏(𝓠_m) for all m).

theorem PoissonDeclumping.PlaneTree.setOf_pair_eq (ℓ : ℕ) (E : Set PlaneTree) : {T : PlaneTree | ℓ + 1 ≤ T.vertexCount ∧ T ∈ E ∧ ∃ U ∈ T.fringeTrees[ℓ]?, U ∈ E} = {T : PlaneTree | ℓ + 1 ≤ T.vertexCount ∧ T ∈ E ∧ T.fringeAt ℓ ∈ E}

The event {|T| ≥ ℓ+1, T ∈ 𝓔, T_{u_{ℓ+1}(T)} ∈ 𝓔} written with fringeTrees[ℓ]? (as in PoissonDeclumping.pairProb) or with fringeAt.

theorem PoissonDeclumping.PlaneTree.lem_cut_graft (μ : PMF ℕ) (ℓ : ℕ) (E : Set PlaneTree) {I : Type u_1} [Fintype I] [Nonempty I] (Q : I → Set PlaneTree) (hQ : ∀ (m : I), 0 < (bienayme μ) (Q m)) (R : Set MarkedTree) (hR : R ⊆ cutFamily ℓ) (τ : ↑R → I) (ha : ∀ (A : ↑R), ∀ S ∈ Q (τ A), (↑A).graft S ∈ E) (hb : ∀ (T : PlaneTree), ℓ + 1 ≤ T.vertexCount → T ∈ E → T.fringeAt ℓ ∈ E → ∃ (hA : cut ℓ T ∈ R), T.fringeAt ℓ ∈ Q (τ ⟨cut ℓ T, hA⟩)) : (bienayme μ) {T : PlaneTree | ℓ + 1 ≤ T.vertexCount ∧ T ∈ E ∧ ∃ U ∈ T.fringeTrees[ℓ]?, U ∈ E} ≤ (bienayme μ) E * Finset.univ.sup' ⋯ fun (m : I) => (bienayme μ)[E | Q m]

Lemma lem:cut_graft (cut-and-graft bound, source lines 2512–2546). Here ℓ is any natural number (the paper fixes ℓ ≥ 1), fringeAt T ℓ = T.fringeTrees[ℓ] is T_{u_{ℓ+1}(T)}, 𝒜_ℓ = cutFamily ℓ, A[S] = A.graft S, and the index type I is finite and nonempty. The bound holds for the Bienaymé measure of any offspring law.

theorem PoissonDeclumping.PlaneTree.lem_cut_graft_real (μ : PMF ℕ) (ℓ : ℕ) (E : Set PlaneTree) {I : Type u_1} [Fintype I] [Nonempty I] (Q : I → Set PlaneTree) (hQ : ∀ (m : I), 0 < (bienayme μ) (Q m)) (R : Set MarkedTree) (hR : R ⊆ cutFamily ℓ) (τ : ↑R → I) (ha : ∀ (A : ↑R), ∀ S ∈ Q (τ A), (↑A).graft S ∈ E) (hb : ∀ (T : PlaneTree), ℓ + 1 ≤ T.vertexCount → T ∈ E → T.fringeAt ℓ ∈ E → ∃ (hA : cut ℓ T ∈ R), T.fringeAt ℓ ∈ Q (τ ⟨cut ℓ T, hA⟩)) : (bienayme μ).real {T : PlaneTree | ℓ + 1 ≤ T.vertexCount ∧ T ∈ E ∧ ∃ U ∈ T.fringeTrees[ℓ]?, U ∈ E} ≤ (bienayme μ).real E * Finset.univ.sup' ⋯ fun (m : I) => (bienayme μ)[|Q m].real E

Lemma lem:cut_graft, real-valued form: the left-hand side is the paper's A_n(ℓ)-type probability 𝐏(|𝒯| ≥ ℓ+1, 𝒯 ∈ 𝓔, 𝒯_{u_{ℓ+1}(𝒯)} ∈ 𝓔).