Complete r-ary patterns, H_r(T) and the two-point leaf-height case

Source lines 458–473 (H_r, H_{r,k}), 827–833 (raw-count characterization of the maximum), 2453–2476 and 2625–2642 (inventory U07), 3031–3042 and 3274–3296 (inventory U09).

• U07: completeTree r k = H_{r,k} has internalCount = k and leafCount = 1 for r = 1, and internalCount = (r^k - 1)/(r - 1), leafCount = r^k for r ≥ 2 (internalCount_completeTree_one, internalCount_completeTree_of_two_le, leafCount_completeTree); the root occurrence probability is π_k = 𝐏(H_{r,k} ≺ 𝒯) = μ_1^k (r = 1) or μ_r^{(r^k-1)/(r-1)} (r ≥ 2) (bienayme_embeds_completeTree_one, bienayme_embeds_completeTree_of_two_le, and real forms), a specialization of U06 (bienayme_embeds_eq).
• H_r(T) = maxCompleteHeight r T (for r ≥ 1): the set {k : ∃ u, H_{r,k} ≺ T_u} contains 0, is downward closed and bounded by |T|, so H_r(T) ≥ k ↔ ∃ u, H_{r,k} ≺ T_u ↔ N_k(T) ≥ 1 (le_maxCompleteHeight_iff, le_maxCompleteHeight_iff_markCount_pos).
• U09, geometric half: if every vertex of T has outdegree 0 or κ (κ ≥ 1), then λ_∅(T) ≥ k ↔ H_{κ,k} ≺ T (le_rootLeafHeight_iff_embeds) and λ(T) = H_κ(T) (leafHeight_eq_maxCompleteHeight). If c = 1 - κμ_κ = 0, this holds almost surely for the Bienaymé tree and for the size-conditioned trees, and 𝐏(λ_∅(𝒯) ≥ k) = μ_κ^{(κ^k-1)/(κ-1)}.

@[simp]

theorem PoissonDeclumping.PlaneTree.completeTree_zero (r : ℕ) : completeTree r 0 = node []

theorem PoissonDeclumping.PlaneTree.completeTree_succ (r k : ℕ) : completeTree r (k + 1) = node (List.replicate r (completeTree r k))

U07: counts and root occurrence probability of H_{r,k}

theorem PoissonDeclumping.PlaneTree.leafCount_completeTree {r : ℕ} (hr : 1 ≤ r) (k : ℕ) : (completeTree r k).leafCount = r ^ k

H_{r,k} has r^k leaves (r ≥ 1).

theorem PoissonDeclumping.PlaneTree.internalCount_completeTree {r : ℕ} (hr : 1 ≤ r) (k : ℕ) : (completeTree r k).internalCount = ∑ j ∈ Finset.range k, r ^ j

H_{r,k} has 1 + r + ⋯ + r^{k-1} internal vertices (r ≥ 1).

theorem PoissonDeclumping.PlaneTree.internalCount_completeTree_one (k : ℕ) : (completeTree 1 k).internalCount = k

s_{1,k} = k.

theorem PoissonDeclumping.PlaneTree.internalCount_completeTree_of_two_le {r : ℕ} (hr : 2 ≤ r) (k : ℕ) : (completeTree r k).internalCount = (r ^ k - 1) / (r - 1)

s_{r,k} = (r^k - 1)/(r - 1) for r ≥ 2.

theorem PoissonDeclumping.PlaneTree.leafCount_completeTree_one (k : ℕ) : (completeTree 1 k).leafCount = 1

ℓ_{1,k} = 1.

theorem PoissonDeclumping.PlaneTree.patternWeight_completeTree (μ : PMF ℕ) {r : ℕ} (hr : 1 ≤ r) (k : ℕ) : patternWeight μ (completeTree r k) = μ r ^ (completeTree r k).internalCount

Every internal vertex of H_{r,k} has r children.

theorem PoissonDeclumping.PlaneTree.bienayme_embeds_completeTree {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) {r : ℕ} (hr : 1 ≤ r) (k : ℕ) : (bienayme μ) {T : PlaneTree | (completeTree r k).Embeds T} = μ r ^ (completeTree r k).internalCount

π_k = 𝐏(H_{r,k} ≺ 𝒯) = μ_r^{s_{r,k}} (source lines 2468–2476).

theorem PoissonDeclumping.PlaneTree.bienayme_embeds_completeTree_one {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (k : ℕ) : (bienayme μ) {T : PlaneTree | (completeTree 1 k).Embeds T} = μ 1 ^ k

U07, r = 1: π_k = μ_1^k.

theorem PoissonDeclumping.PlaneTree.bienayme_embeds_completeTree_of_two_le {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) {r : ℕ} (hr : 2 ≤ r) (k : ℕ) : (bienayme μ) {T : PlaneTree | (completeTree r k).Embeds T} = μ r ^ ((r ^ k - 1) / (r - 1))

U07, r ≥ 2: π_k = μ_r^{(r^k-1)/(r-1)}.

theorem PoissonDeclumping.PlaneTree.bienayme_real_embeds_completeTree_one {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (k : ℕ) : (bienayme μ).real {T : PlaneTree | (completeTree 1 k).Embeds T} = (μ 1).toReal ^ k

theorem PoissonDeclumping.PlaneTree.bienayme_real_embeds_completeTree_of_two_le {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) {r : ℕ} (hr : 2 ≤ r) (k : ℕ) : (bienayme μ).real {T : PlaneTree | (completeTree r k).Embeds T} = (μ r).toReal ^ ((r ^ k - 1) / (r - 1))

The maximal complete height H_r(T)

theorem PoissonDeclumping.PlaneTree.embeds_completeTree_succ_iff {r : ℕ} (hr : 1 ≤ r) (k : ℕ) (T : PlaneTree) : (completeTree r (k + 1)).Embeds T ↔ T.rootDegree = r ∧ ∀ U ∈ T.children, (completeTree r k).Embeds U

H_{r,k+1} ≺ T iff the root has exactly r children and H_{r,k} ≺ each of them.

theorem PoissonDeclumping.PlaneTree.embeds_completeTree_of_succ {r : ℕ} (hr : 1 ≤ r) {k : ℕ} {T : PlaneTree} (h : (completeTree r (k + 1)).Embeds T) : (completeTree r k).Embeds T

theorem PoissonDeclumping.PlaneTree.embeds_completeTree_mono {r : ℕ} (hr : 1 ≤ r) {k k' : ℕ} (hk : k ≤ k') {T : PlaneTree} (h : (completeTree r k').Embeds T) : (completeTree r k).Embeds T

H_{r,k'} ≺ T and k ≤ k' imply H_{r,k} ≺ T.

theorem PoissonDeclumping.PlaneTree.vertexCount_le_of_embeds {T' T : PlaneTree} (h : T'.Embeds T) : T'.vertexCount ≤ T.vertexCount

A pattern has at most as many vertices as the trees it embeds into.

theorem PoissonDeclumping.PlaneTree.succ_le_vertexCount_completeTree {r : ℕ} (hr : 1 ≤ r) (k : ℕ) : k + 1 ≤ (completeTree r k).vertexCount

theorem PoissonDeclumping.PlaneTree.zero_mem_setOf_embeds_completeTree (r : ℕ) (T : PlaneTree) : 0 ∈ {k : ℕ | ∃ U ∈ T.fringeTrees, (completeTree r k).Embeds U}

theorem PoissonDeclumping.PlaneTree.lt_vertexCount_of_embeds_completeTree {r : ℕ} (hr : 1 ≤ r) {T : PlaneTree} {k : ℕ} (hk : ∃ U ∈ T.fringeTrees, (completeTree r k).Embeds U) : k < T.vertexCount

theorem PoissonDeclumping.PlaneTree.exists_embeds_completeTree_of_le {r : ℕ} (hr : 1 ≤ r) {T : PlaneTree} {k k' : ℕ} (hkk : k ≤ k') (hk' : ∃ U ∈ T.fringeTrees, (completeTree r k').Embeds U) : ∃ U ∈ T.fringeTrees, (completeTree r k).Embeds U

theorem PoissonDeclumping.PlaneTree.le_maxCompleteHeight_iff {r : ℕ} (hr : 1 ≤ r) (T : PlaneTree) (k : ℕ) : k ≤ maxCompleteHeight r T ↔ ∃ U ∈ T.fringeTrees, (completeTree r k).Embeds U

H_r(T) ≥ k ↔ ∃ u ∈ T, H_{r,k} ≺ T_u, for r ≥ 1.

theorem PoissonDeclumping.PlaneTree.le_maxCompleteHeight_iff_markCount_pos {r : ℕ} (hr : 1 ≤ r) (T : PlaneTree) (k : ℕ) : k ≤ maxCompleteHeight r T ↔ 0 < markCount (fun (U : PlaneTree) => (completeTree r k).Embeds U) T

H_r(T) ≥ k ↔ N_k(T) = ∑_{u ∈ T} 1{H_{r,k} ≺ T_u} ≥ 1 (source lines 827–833).

theorem PoissonDeclumping.PlaneTree.exists_embeds_maxCompleteHeight {r : ℕ} (hr : 1 ≤ r) (T : PlaneTree) : ∃ U ∈ T.fringeTrees, (completeTree r (maxCompleteHeight r T)).Embeds U

The maximum H_r(T) is attained.

theorem PoissonDeclumping.PlaneTree.maxCompleteHeight_lt_vertexCount {r : ℕ} (hr : 1 ≤ r) (T : PlaneTree) : maxCompleteHeight r T < T.vertexCount

U09: outdegrees in {0, κ}

theorem PoissonDeclumping.PlaneTree.le_rootLeafHeight_iff_embeds {κ : ℕ} (hκ : 1 ≤ κ) {T : PlaneTree} (hT : ∀ V ∈ T.fringeTrees, V.rootDegree = 0 ∨ V.rootDegree = κ) (k : ℕ) : k ≤ T.rootLeafHeight ↔ (completeTree κ k).Embeds T

If every vertex of T has outdegree 0 or κ ≥ 1, then λ_∅(T) ≥ k ↔ H_{κ,k} ≺ T (source lines 3040–3042).

theorem PoissonDeclumping.PlaneTree.leafHeight_eq_maxCompleteHeight {κ : ℕ} (hκ : 1 ≤ κ) {T : PlaneTree} (hT : ∀ V ∈ T.fringeTrees, V.rootDegree = 0 ∨ V.rootDegree = κ) : T.leafHeight = maxCompleteHeight κ T

U09: if every vertex of T has outdegree 0 or κ ≥ 1, then λ(T) = H_κ(T) (source lines 3277–3280).

theorem PoissonDeclumping.PlaneTree.ae_rootDegree_mem_support (μ : PMF ℕ) : ∀ᵐ (T : PlaneTree) ∂bienayme μ, ∀ V ∈ T.fringeTrees, V.rootDegree ∈ μ.support

Almost surely every outdegree of a μ-Bienaymé tree lies in the support of μ.

theorem PoissonDeclumping.PlaneTree.ae_leafHeight_eq_maxCompleteHeight {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (hc0 : LeafHeight.cConst μ = 0) : ∀ᵐ (T : PlaneTree) ∂bienayme μ, T.leafHeight = maxCompleteHeight (LeafHeight.kappa μ) T

U09: if c = 1 - κμ_κ = 0 then almost surely λ(𝒯) = H_κ(𝒯).

theorem PoissonDeclumping.PlaneTree.ae_conditioned_leafHeight_eq_maxCompleteHeight {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (hc0 : LeafHeight.cConst μ = 0) (n : ℕ) : ∀ᵐ (T : PlaneTree) ∂conditioned μ n, T.leafHeight = maxCompleteHeight (LeafHeight.kappa μ) T

U09 for the size-conditioned tree: if c = 0 then λ(𝒯^n) = H_κ(𝒯^n) almost surely.

theorem PoissonDeclumping.PlaneTree.bienayme_le_rootLeafHeight_eq_embeds {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (hc0 : LeafHeight.cConst μ = 0) (k : ℕ) : (bienayme μ) {T : PlaneTree | k ≤ T.rootLeafHeight} = (bienayme μ) {T : PlaneTree | (completeTree (LeafHeight.kappa μ) k).Embeds T}

If c = 0: 𝐏(λ_∅(𝒯) ≥ k) = 𝐏(H_{κ,k} ≺ 𝒯).

theorem PoissonDeclumping.PlaneTree.bienayme_le_rootLeafHeight_of_cConst_eq_zero {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (hc0 : LeafHeight.cConst μ = 0) (k : ℕ) : (bienayme μ) {T : PlaneTree | k ≤ T.rootLeafHeight} = μ (LeafHeight.kappa μ) ^ ((LeafHeight.kappa μ ^ k - 1) / (LeafHeight.kappa μ - 1))

If c = 0: π_k = 𝐏(λ_∅(𝒯) ≥ k) = μ_κ^{(κ^k-1)/(κ-1)} (source line 3283).