Consequences of Assumption (S): Lemma lem:consequenceM and Corollary cor:SM

Work package WP3 of the bridge plan. Source lines 1182–1251 (Lemma 3.6, proof step P04) and 1256–1365 (Corollary 3.7, proof step P05). Notation: 𝒯 ~ bienayme μ, P_k = P(· | G_k(𝒯) = 1) (cond), Ψ_m(x) = walkProb μ m x, supWalk μ m = sup_x Ψ_m(x).

The decomposition of Assumption (S)

A decomposition ρ (Skeleton) is a law of (𝒯, C, 𝒯^{(1)}, …, 𝒯^{(L)}) with first marginal P_k, conditionally i.i.d. trees given (C, L) and |𝒯| = C + ∑ |𝒯^{(i)}|. lintegral_skeleton is the resulting forest formula E[h(C, L, ∑ |𝒯^{(i)}|)] = ∑_{c, ℓ} P(C = c, L = ℓ) ∑_q P(|𝒢_ℓ| = q) h(c, ℓ, q), and lintegral_skeleton_le compares with E[L]; the empty forest ℓ = 0 needs no special treatment there.

Main statements

• consequenceM_tail (Lemma lem:consequenceM, first assertion): P_{k_n}(|𝒯| > M_n/4) → 0.
• consequenceM_weighted (second assertion, numerator form, correction F3): for every ε > 0, eventually, uniformly over a time shift j ≤ 1 and an endpoint selector e, a_n E_{k_n}[Ψ_{n-j-|𝒯|}(e(𝒯)) 1{|𝒯| > M_n/4}] ≤ ε; consequenceM_weighted_sup is the sup_x form and consequenceM_weighted_div the paper's form (division by Ψ_n(-1)). The paper's step "Ψ_{n-c}(-1) ∼ Ψ_n(-1) uniformly for c ≤ M_n/8" fails in the periodic case (Ψ_{n-c}(-1) = 0 when d ∤ c); the proof instead applies the numerator forest estimate forest_weighted_tail_sup_le at time N = n - j - c ≥ n/2 and uses a_n ≤ C a_N.
• microscopic_of_large: Assumption (M) from o(π_n) bounds on large marked trees, before and after bridge weighting (the assembly of source lines 1286–1311).
• microscopic_of_structural (Corollary cor:SM(i)): (S) implies (M), same cutoff.
• integral_markCount_isEquivalent (Corollary cor:SM(ii)): E[#{u ∈ 𝒯^n : G_{k_n}(𝒯^n_u) = 1}] ∼ n π_n.
• conditioned_mark_tendsto_zero (Corollary cor:SM(iii)): π_n = O(1/n) implies P(G_{k_n}(𝒯^n) = 1) → 0.

Null marks (π_n = 0, where (S) gives no decomposition) are handled by cond of a null event being 0 (correction F13).

Forests of i.i.d. trees: sums over tuples and lists

theorem PoissonDeclumping.Bridge.tsum_prod_weight_mul (μ : PMF ℕ) (L : ℕ) (H : ℕ → ENNReal) : ∑' (f : Fin L → PlaneTree), (∏ i : Fin L, PlaneTree.weight μ (f i)) * H (∑ i : Fin L, (f i).vertexCount) = ∑' (q : ℕ), PlaneTree.forestSizeWeight μ L q * H q

∑_{(t_1..t_L)} ∏ w(t_i) H(∑ |t_i|) = ∑_q P(|𝒢_L| = q) H(q).

theorem PoissonDeclumping.Bridge.tsum_list_prod_weight_mul (μ : PMF ℕ) (Φ : ℕ → ℕ → ENNReal) : ∑' (ts : List PlaneTree), (List.map (PlaneTree.weight μ) ts).prod * Φ ts.length (List.map PlaneTree.vertexCount ts).sum = ∑' (L : ℕ) (q : ℕ), PlaneTree.forestSizeWeight μ L q * Φ L q

Lists of trees grouped by length: ∑_{ts} ∏ w(t_i) Φ(|ts|, ∑ |t_i|) = ∑_L ∑_q P(|𝒢_L| = q) Φ(L, q).

Integrals over a decomposition ρ

theorem PoissonDeclumping.Bridge.lintegral_core_length (ρ : MeasureTheory.Measure (PlaneTree × ℕ × List PlaneTree)) (g : ℕ → ℕ → ENNReal) : ∫⁻ (ω : PlaneTree × ℕ × List PlaneTree), g ω.2.1 ω.2.2.length ∂ρ = ∑' (c : ℕ) (L : ℕ), ρ {ω : PlaneTree × ℕ × List PlaneTree | ω.2.1 = c ∧ ω.2.2.length = L} * g c L

Integrating a function of (C, L) against any measure on PlaneTree × ℕ × List PlaneTree.

theorem PoissonDeclumping.Bridge.lintegral_skeleton {μ : PMF ℕ} {G : PlaneTree → Prop} {ρ : MeasureTheory.Measure (PlaneTree × ℕ × List PlaneTree)} (hρ : Skeleton μ G ρ) (h : ℕ → ℕ → ℕ → ENNReal) : ∫⁻ (ω : PlaneTree × ℕ × List PlaneTree), h ω.2.1 ω.2.2.length (List.map PlaneTree.vertexCount ω.2.2).sum ∂ρ = ∑' (c : ℕ) (L : ℕ), ρ {ω : PlaneTree × ℕ × List PlaneTree | ω.2.1 = c ∧ ω.2.2.length = L} * ∑' (q : ℕ), PlaneTree.forestSizeWeight μ L q * h c L q

The conditional forest structure of a decomposition (Assumption (S), source lines 1196–1202): for every h(c, ℓ, q), E[h(C, L, ∑_{i ≤ L} |𝒯^{(i)}|)] = ∑_{c, ℓ} P(C = c, L = ℓ) ∑_q P(|𝒢_ℓ| = q) h(c, ℓ, q).

theorem PoissonDeclumping.Bridge.lintegral_skeleton_le {μ : PMF ℕ} {G : PlaneTree → Prop} {ρ : MeasureTheory.Measure (PlaneTree × ℕ × List PlaneTree)} (hρ : Skeleton μ G ρ) (h : ℕ → ℕ → ℕ → ENNReal) (K : ENNReal) (hK : ∀ (c L : ℕ), ∑' (q : ℕ), PlaneTree.forestSizeWeight μ L q * h c L q ≤ K * ↑L) : ∫⁻ (ω : PlaneTree × ℕ × List PlaneTree), h ω.2.1 ω.2.2.length (List.map PlaneTree.vertexCount ω.2.2).sum ∂ρ ≤ K * ∫⁻ (ω : PlaneTree × ℕ × List PlaneTree), ↑ω.2.2.length ∂ρ

Comparison: if ∑_q P(|𝒢_ℓ| = q) h(c, ℓ, q) ≤ K ℓ for all c, ℓ, then E[h(C, L, ∑ |𝒯^{(i)}|)] ≤ K E[L] (the empty forest ℓ = 0 contributes only through the hypothesis at ℓ = 0).

theorem PoissonDeclumping.Bridge.lintegral_cond_vertexCount {μ : PMF ℕ} {G : PlaneTree → Prop} {ρ : MeasureTheory.Measure (PlaneTree × ℕ × List PlaneTree)} (hρ : Skeleton μ G ρ) (ψ : ℕ → ENNReal) : ∫⁻ (T : PlaneTree), ψ T.vertexCount ∂(PlaneTree.bienayme μ)[|{T : PlaneTree | G T}] = ∫⁻ (ω : PlaneTree × ℕ × List PlaneTree), ψ (ω.2.1 + (List.map PlaneTree.vertexCount ω.2.2).sum) ∂ρ

Under a decomposition, a function of the size of the marked tree integrates as a function of C + ∑_{i ≤ L} |𝒯^{(i)}| (source line 1198).

Core estimates for one decomposition

theorem PoissonDeclumping.Bridge.exists_comparison {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) : ∃ (C : ℝ), 0 < C ∧ (∀ (M : ℕ), 8 ≤ M → a M ≤ C * a (M / 8)) ∧ ∀ (n N : ℕ), 1 ≤ N → n ≤ 2 * N → a n ≤ C * a N

a_M ≤ C a_{⌊M/8⌋} and a_n ≤ C a_N for n ≤ 2N (regular variation).

theorem PoissonDeclumping.Bridge.cond_vertexCount_gt_le {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (G : PlaneTree → Prop) (ρ : MeasureTheory.Measure (PlaneTree × ℕ × List PlaneTree)), Skeleton μ G ρ → ∀ (M : ℕ), 8 ≤ M → (PlaneTree.bienayme μ)[{T : PlaneTree | ↑M / 4 < ↑T.vertexCount} | {T : PlaneTree | G T}] ≤ ρ {ω : PlaneTree × ℕ × List PlaneTree | 1 / 8 * ↑M < ↑ω.2.1} + ENNReal.ofReal (C / a M) * ∫⁻ (ω : PlaneTree × ℕ × List PlaneTree), ↑ω.2.2.length ∂ρ

Unweighted core estimate (proof of lem:consequenceM, source lines 1208–1224): for a decomposition ρ of P(· | G(𝒯) = 1) and M ≥ 8, P(|𝒯| > M/4 | G(𝒯) = 1) ≤ P(C > M/8) + (C' / a_M) E[L].

theorem PoissonDeclumping.Bridge.lintegral_cond_supWalk_le {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (G : PlaneTree → Prop) (ρ : MeasureTheory.Measure (PlaneTree × ℕ × List PlaneTree)), Skeleton μ G ρ → ∀ (M n j : ℕ), 8 ≤ M → j ≤ 1 → 2 * M ≤ n → ∫⁻ (T : PlaneTree), ENNReal.ofReal ({T : PlaneTree | ↑M / 4 < ↑T.vertexCount}.indicator (fun (T : PlaneTree) => supWalk μ (↑n - ↑j - ↑T.vertexCount)) T) ∂(PlaneTree.bienayme μ)[|{T : PlaneTree | G T}] ≤ ρ {ω : PlaneTree × ℕ × List PlaneTree | 1 / 8 * ↑M < ↑ω.2.1} + ENNReal.ofReal (C / (a M * a n)) * ∫⁻ (ω : PlaneTree × ℕ × List PlaneTree), ↑ω.2.2.length ∂ρ

Bridge-weighted core estimate (proof of lem:consequenceM, source lines 1226–1250, in numerator form, correction F3): for a decomposition ρ of P(· | G(𝒯) = 1), M ≥ 8, n ≥ 2M and a time shift j ≤ 1, E[sup_x Ψ_{n-j-|𝒯|}(x) 1{|𝒯| > M/4} | G(𝒯) = 1] ≤ P(C > M/8) + C' E[L] / (a_M a_n). On {C ≤ M/8} the forest has more than M/8 vertices and the forest estimate is applied at time N = n - j - C ≥ n/2 (no ratio Ψ_{n-c}(-1)/Ψ_n(-1) is used).

Lemma lem:consequenceM

theorem PoissonDeclumping.Bridge.tendsto_zero_of_forall_eventually_le {ι : Type u_1} {l : Filter ι} {f : ι → ℝ} (h0 : ∀ (i : ι), 0 ≤ f i) (h : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (i : ι) in l, f i ≤ ε) : Filter.Tendsto f l (nhds 0)

A nonnegative function that is eventually below every ε > 0 tends to 0.

theorem PoissonDeclumping.Bridge.toReal_le_add_of_le_add_div {X P E : ENNReal} {K A δ : ℝ} (hK : 0 ≤ K) (hA : 0 < A) (hδ : 0 ≤ δ) (hP : P ≠ ⊤) (hX : X ≤ P + ENNReal.ofReal (K / A) * E) (hE : E / ENNReal.ofReal A ≤ ENNReal.ofReal δ) : X.toReal ≤ P.toReal + K * δ

Turning a bound X ≤ P + (K / A) E with E / A ≤ δ into X ≤ P + K δ in ℝ.

theorem PoissonDeclumping.Bridge.eventually_cutoff_facts {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {M : ℕ → ℕ} (hM : IsCutoff M) : ∀ᶠ (n : ℕ) in admissibleSizes μ, 8 ≤ M n ∧ 2 * M n ≤ n ∧ 1 ≤ a n

Eventual facts on a cutoff along admissible sizes: M_n ≥ 8, 2 M_n ≤ n, a_n ≥ 1.

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

Lemma lem:consequenceM, first assertion (source lines 1182–1224, P04): under Assumption (S), P(|𝒯| > M_n/4 | G_{k_n}(𝒯) = 1) → 0 along admissible sizes.

theorem PoissonDeclumping.Bridge.consequenceM_weighted_sup {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hM : IsCutoff M) (hS : StructuralMicroscopic μ a G k M) (ε : ℝ) : 0 < ε → ∀ᶠ (n : ℕ) in admissibleSizes μ, ∀ j ≤ 1, a n * ∫ (T : PlaneTree), {T : PlaneTree | ↑(M n) / 4 < ↑T.vertexCount}.indicator (fun (T : PlaneTree) => supWalk μ (↑n - ↑j - ↑T.vertexCount)) T ∂(PlaneTree.bienayme μ)[|{T : PlaneTree | G (k n) T}] ≤ ε

Lemma lem:consequenceM, second assertion, sup_x form (source lines 1226–1250): under Assumption (S), uniformly in a time shift j ≤ 1, a_n E[sup_x Ψ_{n-j-|𝒯|}(x) 1{|𝒯| > M_n/4} | G_{k_n}(𝒯) = 1] → 0 along admissible sizes.

theorem PoissonDeclumping.Bridge.consequenceM_weighted {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hM : IsCutoff M) (hS : StructuralMicroscopic μ a G k M) (ε : ℝ) : 0 < ε → ∀ᶠ (n : ℕ) in admissibleSizes μ, ∀ j ≤ 1, ∀ (e : PlaneTree → ℤ), a n * ∫ (T : PlaneTree), {T : PlaneTree | ↑(M n) / 4 < ↑T.vertexCount}.indicator (fun (T : PlaneTree) => walkProb μ (↑n - ↑j - ↑T.vertexCount) (e T)) T ∂(PlaneTree.bienayme μ)[|{T : PlaneTree | G (k n) T}] ≤ ε

Lemma lem:consequenceM, second assertion, numerator form (source lines 1226–1250; plan WP3.3, correction F3): under Assumption (S), for every ε > 0, eventually along admissible sizes, for every time shift j ≤ 1 and every endpoint selector e, a_n E[Ψ_{n-j-|𝒯|}(e(𝒯)) 1{|𝒯| > M_n/4} | G_{k_n}(𝒯) = 1] ≤ ε. Dividing by Ψ_n(-1) ≥ c / a_n gives the paper's form at j = 0.

theorem PoissonDeclumping.Bridge.consequenceM_weighted_div {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hM : IsCutoff M) (hS : StructuralMicroscopic μ a G k M) : Filter.Tendsto (fun (n : ℕ) => ∫ (T : PlaneTree), {T : PlaneTree | ↑(M n) / 4 < ↑T.vertexCount}.indicator (fun (T : PlaneTree) => supWalk μ (↑n - ↑T.vertexCount) / walkProb μ (↑n) (-1)) T ∂(PlaneTree.bienayme μ)[|{T : PlaneTree | G (k n) T}]) (admissibleSizes μ) (nhds 0)

Lemma lem:consequenceM, second assertion, the paper's form (source line 1189, eq:record): under Assumption (S), E[sup_x Ψ_{n-|𝒯|}(x) / Ψ_n(-1) 1{|𝒯| > M_n/4} | G_{k_n}(𝒯) = 1] → 0 along admissible sizes (at admissible n, Ψ_n(-1) ≥ c / a_n > 0).

Corollary cor:SM

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

ν(s ∩ t) = ν(s) ν(t | s) in ℝ, for a finite measure on plane trees.

theorem PoissonDeclumping.Bridge.integral_indicator_eq_mul_integral_cond (ν : MeasureTheory.Measure PlaneTree) [MeasureTheory.IsFiniteMeasure ν] (s : Set PlaneTree) (f : PlaneTree → ℝ) : ∫ (T : PlaneTree), s.indicator f T ∂ν = ν.real s * ∫ (T : PlaneTree), f T ∂ν[|s]

∫ 1_s f dν = ν(s) ∫ f dν(· | s) in ℝ, for a finite measure on plane trees.

theorem PoissonDeclumping.Bridge.microscopic_of_large {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hM : IsCutoff M) (h1 : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in admissibleSizes μ, (PlaneTree.bienayme μ).real {T : PlaneTree | G (k n) T ∧ M n < T.vertexCount} ≤ ε * markProb μ G k n) (h2 : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in admissibleSizes μ, a n * ∫ (T : PlaneTree), {T : PlaneTree | G (k n) T ∧ M n < T.vertexCount}.indicator (fun (T : PlaneTree) => walkProb μ (↑n - ↑T.vertexCount) 0) T ∂PlaneTree.bienayme μ ≤ ε * markProb μ G k n) : Microscopic μ G k M

Assembly of Assumption (M) from bounds on large marked trees (the argument of source lines 1286–1311, in numerator form): if P(G_{k_n}(𝒯), |𝒯| > M_n) = o(π_n) and a_n E[1{G_{k_n}(𝒯), |𝒯| > M_n} Ψ_{n-|𝒯|}(0)] = o(π_n) along admissible sizes, then (M) holds. Small trees are handled by the uniform ratio limit (eventually_abs_uniformFringeLaw_real_sub_le), large ones by Corollary cor:cyclicshift and Ψ_n(-1) ≥ c / a_n.

theorem PoissonDeclumping.Bridge.microscopic_of_structural {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hM : IsCutoff M) (hS : StructuralMicroscopic μ a G k M) : Microscopic μ G k M

Corollary cor:SM(i) (source lines 1256–1311, P05): Assumption (S) implies Assumption (M) along (k_n) with respect to the same cutoff (M_n).

theorem PoissonDeclumping.Bridge.integral_markCount_isEquivalent {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hM : IsCutoff M) (hS : StructuralMicroscopic μ a G k M) : Asymptotics.IsEquivalent (admissibleSizes μ) (fun (n : ℕ) => ∫ (T : PlaneTree), ↑(PlaneTree.markCount (G (k n)) T) ∂PlaneTree.conditioned μ n) fun (n : ℕ) => ↑n * markProb μ G k n

Corollary cor:SM(ii) (source lines 1305–1311): under Assumption (S), E[#{u ∈ 𝒯^n : G_{k_n}(𝒯^n_u) = 1}] ∼ n π_n along admissible sizes.

theorem PoissonDeclumping.Bridge.cond_vertexCount_eq_le {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) : ∃ (K : ℝ), 0 ≤ K ∧ ∀ (G : PlaneTree → Prop) (ρ : MeasureTheory.Measure (PlaneTree × ℕ × List PlaneTree)), Skeleton μ G ρ → ∀ (n : ℕ), 1 ≤ n → (PlaneTree.bienayme μ)[{T : PlaneTree | T.vertexCount = n} | {T : PlaneTree | G T}] ≤ ρ {ω : PlaneTree × ℕ × List PlaneTree | ↑n / 2 < ↑ω.2.1} + ENNReal.ofReal (K / (↑n * a n)) * ∫⁻ (ω : PlaneTree × ℕ × List PlaneTree), ↑ω.2.2.length ∂ρ

Local core estimate (proof of cor:SM(iii), source lines 1330–1353): for a decomposition ρ of P(· | G(𝒯) = 1) and n ≥ 1, P(|𝒯| = n | G(𝒯) = 1) ≤ P(C > n/2) + K E[L] / (n a_n). On {C ≤ n/2} the forest must have exactly n - C ≥ n/2 vertices, and P(|𝒢_ℓ| = n - c) ≤ C ℓ / ((n - c) a_{n-c}); the empty forest contributes nothing since n - c ≥ 1.

theorem PoissonDeclumping.Bridge.conditioned_mark_tendsto_zero {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {G : ℕ → PlaneTree → Prop} {k M : ℕ → ℕ} (hM : IsCutoff M) (hS : StructuralMicroscopic μ a G k M) (hO : markProb μ G k =O[admissibleSizes μ] fun (n : ℕ) => 1 / ↑n) : Filter.Tendsto (fun (n : ℕ) => (PlaneTree.conditioned μ n).real {T : PlaneTree | G (k n) T}) (admissibleSizes μ) (nhds 0)

Corollary cor:SM(iii) (source lines 1258–1260, 1313–1364): under Assumption (S), if π_n = O(1/n) along admissible sizes, then the root of 𝒯^n is marked with vanishing probability, P(G_{k_n}(𝒯^n) = 1) → 0. The proof writes P(G_{k_n}(𝒯^n) = 1) = π_n P_{k_n}(|𝒯| = n) / P(|𝒯| = n), uses P(|𝒯| = n) ≥ c / (n a_n) (tree_size_asymp) and the local core estimate cond_vertexCount_eq_le; null marks (π_n = 0) and empty forests are covered (correction F13).