Leaf-heights of plane trees and the root leaf-height law

Source lines 814–833 and 2911–2930. The leaf-height λ_v(T) of a vertex is the distance from v to its closest leaf descendant; we define the root leaf-height λ_∅(T) recursively (a leaf has 0; otherwise one plus the minimum over the children) and the leaf-height λ(T) = max_{v ∈ T} λ_v(T), where λ_v(T) = λ_∅(T_v) for the fringe subtree T_v.

• PlaneTree.le_leafHeight_iff_markCount_pos: λ(T) ≥ k iff the raw count ∑_{v ∈ T} 1{λ_∅(T_v) ≥ k} is positive (inventory U04, source lines 827–829).
• LeafHeight.bienayme_real_le_rootLeafHeight: for a critical μ with μ_1 ≠ 1, P(λ_∅(𝒯) ≥ k) is the analytic sequence π_k (π_0 = 1, π_{k+1} = g(π_k)), by the branching property (inventory U10, source lines 2922–2930, 2956–2957); and P(λ_∅(𝒯) = k) = ℓ_k.
• Lemma lem:ell_asymp and the identification of C_μ, D_μ (U03), restated for the tree law.

@[simp]

theorem PoissonDeclumping.PlaneTree.rootLeafHeight_leaf : (node []).rootLeafHeight = 0

theorem PoissonDeclumping.PlaneTree.succ_le_rootLeafHeight_iff (k : ℕ) (T : PlaneTree) : k + 1 ≤ T.rootLeafHeight ↔ T.children ≠ [] ∧ ∀ U ∈ T.children, k ≤ U.rootLeafHeight

λ_∅(T) ≥ k + 1 iff the root has at least one child and every child has root leaf-height at least k.

theorem PoissonDeclumping.PlaneTree.rootLeafHeight_eq_zero_iff (T : PlaneTree) : T.rootLeafHeight = 0 ↔ T.children = []

λ_∅(T) = 0 iff T is a leaf.

theorem PoissonDeclumping.PlaneTree.le_leafHeight_iff (k : ℕ) (T : PlaneTree) : k ≤ T.leafHeight ↔ ∃ U ∈ T.fringeTrees, k ≤ U.rootLeafHeight

λ(T) ≥ k iff some vertex v has λ_∅(T_v) ≥ k.

theorem PoissonDeclumping.PlaneTree.le_leafHeight_iff_markCount_pos (k : ℕ) (T : PlaneTree) : k ≤ T.leafHeight ↔ 0 < markCount (fun (U : PlaneTree) => k ≤ U.rootLeafHeight) T

U04 for the leaf-height: λ(T) ≥ k iff the raw marked count ∑_{v ∈ T} 1{λ_∅(T_v) ≥ k} is positive (source lines 827–829).

theorem PoissonDeclumping.PlaneTree.rootLeafHeight_le_leafHeight (T : PlaneTree) : T.rootLeafHeight ≤ T.leafHeight

theorem PoissonDeclumping.LeafHeight.bienayme_real_le_rootLeafHeight {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (k : ℕ) : (PlaneTree.bienayme μ).real {T : PlaneTree | k ≤ T.rootLeafHeight} = piSeq μ k

U10: for a critical μ with μ_1 ≠ 1, P(λ_∅(𝒯) ≥ k) = π_k, where π_0 = 1 and π_{k+1} = g(π_k), g(x) = ∑_{j ≥ 1} μ_j x^j.

theorem PoissonDeclumping.LeafHeight.bienayme_real_rootLeafHeight_eq {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (k : ℕ) : (PlaneTree.bienayme μ).real {T : PlaneTree | T.rootLeafHeight = k} = ellSeq μ k

P(λ_∅(𝒯) = k) = ℓ_k = π_k - π_{k+1} (source line 3009).

theorem PoissonDeclumping.LeafHeight.bienayme_real_le_rootLeafHeight_eq_piSeq {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) : (fun (k : ℕ) => (PlaneTree.bienayme μ).real {T : PlaneTree | k ≤ T.rootLeafHeight}) = piSeq μ

P(λ_∅(𝒯) ≥ k) as a function of k is π.

theorem PoissonDeclumping.LeafHeight.lem_ell_asymp_i_tree {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (hpos : 0 < μ 1) : 0 < leafC μ ∧ Filter.Tendsto (fun (k : ℕ) => (PlaneTree.bienayme μ).real {T : PlaneTree | k ≤ T.rootLeafHeight} / (μ 1).toReal ^ k) Filter.atTop (nhds (leafC μ)) ∧ Asymptotics.IsEquivalent Filter.atTop (fun (k : ℕ) => (PlaneTree.bienayme μ).real {T : PlaneTree | k ≤ T.rootLeafHeight}) fun (k : ℕ) => leafC μ * (μ 1).toReal ^ k

Lemma lem:ell_asymp(i) for the tree law: if μ_1 > 0, P(λ_∅(𝒯) ≥ k) ∼ C_μ μ_1^k with C_μ = lim P(λ_∅(𝒯) ≥ k)/μ_1^k > 0.

theorem PoissonDeclumping.LeafHeight.lem_ell_asymp_ii_tree {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (h0 : μ 1 = 0) : kappa μ = sInf {j : ℕ | 2 ≤ j ∧ 0 < μ j} ∧ 0 < leafD μ ∧ leafD μ < 1 ∧ Filter.Tendsto (fun (k : ℕ) => (PlaneTree.bienayme μ).real {T : PlaneTree | k ≤ T.rootLeafHeight} ^ (1 / ↑(kappa μ) ^ k)) Filter.atTop (nhds (leafD μ)) ∧ Asymptotics.IsEquivalent Filter.atTop (fun (k : ℕ) => (PlaneTree.bienayme μ).real {T : PlaneTree | k ≤ T.rootLeafHeight}) fun (k : ℕ) => (μ (kappa μ)).toReal ^ (-1 / (↑(kappa μ) - 1)) * leafD μ ^ kappa μ ^ k

Lemma lem:ell_asymp(ii) for the tree law: if μ_1 = 0 and κ = min{j ≥ 2 : μ_j > 0}, P(λ_∅(𝒯) ≥ k) ∼ μ_κ^{-1/(κ-1)} D_μ^{κ^k} with D_μ = lim P(λ_∅(𝒯) ≥ k)^{1/κ^k} ∈ (0, 1).