Theorem thm:max_lh: the maximum leaf-height

Source: statement lines 533–586, proof lines 3253–3387 (inventory T1.4, P24). Marks G_k(T) = 1{λ_∅(T) ≥ k}, raw counts N_k(T) = ∑_{v ∈ T} G_k(T_v) (markCount), declumped marks Ghat_k = RootDeclumping.lhDeclumpedMark μ k (degree set B = {j ≥ κ + 1}), π_k = P(λ_∅(𝒯) ≥ k), c = 1 - κ μ_κ (LeafHeight.cConst μ). The cutoff is M_n = max 1 ⌊n^{1-η}⌋₊ with η = (1 - 1/α)/2 ∈ (0, 1 - 1/α).

The final theorem takes Theorems thm:PoissonApproximation2 and thm:max_string (the paper's own results, proved elsewhere) as hypotheses of their reviewed statement types:

• maxLeafHeight_of_approx2_maxString : PoissonApproximation2Statement → MaxStringStatement → MaxLeafHeightStatement, and maxLeafHeight_of, the same with an (unused) extra hypothesis PoissonApproximationStatement.

The three cases are separate exports:

• maxLeafHeight_unary ((i), μ_1 > 0, source lines 3298–3326): C_μ = leafC μ; the levels h_n = ⌊k_n^* + t⌋ + 1 satisfy (S) (Applications.lem_S_lh, levels from ExtremesAnalysis.lh_unary_inputs), the declumped marks satisfy (C) (Applications.lem_C_lh), n π_{h_n} is bounded, so Theorem thm:PoissonApproximation2 gives the declumped Poisson approximation with parameter c_B n π_{h_n}, c_B = 1 - μ_1; the leaf-height marks propagate through parents of degree 1 (propagatesOutside_of_kappa_eq_one), the root mark vanishes (Bridge.conditioned_mark_tendsto_zero), and Lemma lem:declump_to_raw (PlaneTree.conditioned_declump_to_raw) transfers to P(N_{h_n}(𝒯^n) = 0) = P(λ(𝒯^n) ≤ ⌊k_n^* + t⌋).
• maxLeafHeight_superexp_of_cConst_pos ((ii), μ_1 = 0, c > 0, source lines 3328–3383): eq:threshold_lh is tendsto_conditioned_le_leafHeight_zero (first moment, Corollary cor:SM(ii), Markov) and tendsto_conditioned_le_leafHeight_one (Theorem thm:PoissonApproximation2, divergent part, and N̂_h ≥ 1 ⇒ N_h ≥ 1 ⇔ λ ≥ h); these are the two halves of Lemma lem:ineqs, proved here directly for the conditioned laws (probability measures only at admissible sizes). The levels and the thresholds are those of ExtremesAnalysis.lh_twoPoint_thresholds and ExtremesAnalysis.lh_interior_thresholds.
• maxLeafHeight_of_cConst_eq_zero ((ii), c = 0, source lines 3274–3296): λ = H_κ almost surely under 𝒯^n and k_n^{**} = t_n^{**} (ExtremesAnalysis.lh_center_eq_tStarStar), so the claim is Theorem thm:max_string(ii) with r = κ.

Departures

• The paper's case split at θ_n = 1/2 is replaced by the single lower level ExtremesAnalysis.twoPointLow k_n^{**} (J_n = [a_n, a_n + 2)), and integer levels are turned into natural mark indices by Int.toNat ({H ≤ m} = {(m+1).toNat ≤ H}ᶜ for every integer m), so negative floors and small n need no separate treatment.
• Theorem thm:PoissonApproximation is not needed: Theorem thm:PoissonApproximation2 (with Lemma lem:declump_to_raw in case (i)) covers both the bounded and the divergent regime.

theorem PoissonDeclumping.MaxLeafHeight.conditioned_real_markCount_pos_le (μ : PMF ℕ) (n : ℕ) (G : PlaneTree → Prop) : (PlaneTree.conditioned μ n).real {T : PlaneTree | 0 < PlaneTree.markCount G T} ≤ ∫ (T : PlaneTree), ↑(PlaneTree.markCount G T) ∂PlaneTree.conditioned μ n

Markov's inequality for a count under the conditioned law (any n): P(N(𝒯^n) ≥ 1) ≤ E[N(𝒯^n)].

theorem PoissonDeclumping.MaxLeafHeight.eventually_admissible_sizes (μ : PMF ℕ) : ∀ᶠ (n : ℕ) in admissibleSizes μ, PlaneTree.Admissible μ n

Along admissibleSizes μ, the sizes are eventually admissible.

theorem PoissonDeclumping.MaxLeafHeight.setOf_le_leafHeight_eq (h : ℕ) : {T : PlaneTree | h ≤ T.leafHeight} = {T : PlaneTree | 0 < PlaneTree.markCount (fun (U : PlaneTree) => h ≤ U.rootLeafHeight) T}

{λ(T) ≥ h} is the event that the raw leaf-height count is positive.

theorem PoissonDeclumping.MaxLeafHeight.tendsto_conditioned_le_leafHeight_zero {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {h M : ℕ → ℕ} (hM : IsCutoff M) (hS : StructuralMicroscopic μ a (fun (j : ℕ) (T : PlaneTree) => j ≤ T.rootLeafHeight) h M) (h0 : Filter.Tendsto (fun (n : ℕ) => ↑n * (PlaneTree.bienayme μ).real {T : PlaneTree | h n ≤ T.rootLeafHeight}) (admissibleSizes μ) (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => (PlaneTree.conditioned μ n).real {T : PlaneTree | h n ≤ T.leafHeight}) (admissibleSizes μ) (nhds 0)

Upper half of eq:threshold_lh (source lines 3343–3356): under (S) along the levels h_n, n π_{h_n} → 0 implies P(λ(𝒯^n) ≥ h_n) → 0 (Corollary cor:SM(ii) and the first half of Lemma lem:ineqs, i.e. Markov's inequality for N_{h_n}(𝒯^n)).

theorem PoissonDeclumping.MaxLeafHeight.tendsto_conditioned_le_leafHeight_one {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h2 : PoissonApproximation2Statement) (hD : StableDomain μ α a) (hcpos : 0 < LeafHeight.cConst μ) {h M : ℕ → ℕ} (hM : IsCutoff M) (hS : StructuralMicroscopic μ a (fun (j : ℕ) (T : PlaneTree) => j ≤ T.rootLeafHeight) h M) (hinf : Filter.Tendsto (fun (n : ℕ) => ↑n * (PlaneTree.bienayme μ).real {T : PlaneTree | h n ≤ T.rootLeafHeight}) (admissibleSizes μ) Filter.atTop) : Filter.Tendsto (fun (n : ℕ) => (PlaneTree.conditioned μ n).real {T : PlaneTree | h n ≤ T.leafHeight}) (admissibleSizes μ) (nhds 1)

Lower half of eq:threshold_lh (source lines 3343–3356): if c > 0, under (S) along the levels h_n, n π_{h_n} → ∞ implies P(λ(𝒯^n) ≥ h_n) → 1 (Theorem thm:PoissonApproximation2, divergent part, gives N̂_{h_n}(𝒯^n) → ∞ in probability, with (C) from Lemma lem:C_lh; then the second half of Lemma lem:ineqs, since N̂_h ≥ 1 ⇒ N_h ≥ 1 ⇔ λ ≥ h).

theorem PoissonDeclumping.MaxLeafHeight.tendsto_le_and_not_le {μ : PMF ℕ} {l : Filter ℕ} (hl : ∀ᶠ (n : ℕ) in l, PlaneTree.Admissible μ n) (H : PlaneTree → ℕ) {lo hi : ℕ → ℕ} (hlo : Filter.Tendsto (fun (n : ℕ) => (PlaneTree.conditioned μ n).real {T : PlaneTree | lo n ≤ H T}) l (nhds 1)) (hhi : Filter.Tendsto (fun (n : ℕ) => (PlaneTree.conditioned μ n).real {T : PlaneTree | hi n ≤ H T}) l (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => (PlaneTree.conditioned μ n).real {T : PlaneTree | lo n ≤ H T ∧ ¬hi n ≤ H T}) l (nhds 1)

Two thresholds give the localization on [lo, hi): if P(H(𝒯^n) ≥ lo_n) → 1 and P(H(𝒯^n) ≥ hi_n) → 0, then P(lo_n ≤ H(𝒯^n) < hi_n) → 1.

theorem PoissonDeclumping.MaxLeafHeight.propagatesOutside_of_kappa_eq_one {μ : PMF ℕ} (hκ : LeafHeight.kappa μ = 1) (k : ℕ) : PlaneTree.PropagatesOutside (RootDeclumping.lhDegrees μ) fun (T : PlaneTree) => k ≤ T.rootLeafHeight

Propagation for κ = 1 (source lines 3317–3319): with B = {j ≥ 2}, a vertex with a child U with λ_∅(U) ≥ k and degree outside B has degree one, hence λ_∅ ≥ k + 1 ≥ k.

theorem PoissonDeclumping.MaxLeafHeight.twoPointLocalization_congr {μ : PMF ℕ} {H H' : PlaneTree → ℕ} {x : ℕ → ℝ} (hH : ∀ (n : ℕ), ∀ᵐ (T : PlaneTree) ∂PlaneTree.conditioned μ n, H T = H' T) : TwoPointLocalization μ H x ↔ TwoPointLocalization μ H' x

Statistics that agree almost surely under every 𝒯^n have the same two-point localization.

theorem PoissonDeclumping.MaxLeafHeight.exists_eta {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) : ∃ (η : ℝ), (0 < η ∧ η < 1 - 1 / α) ∧ η < 1

An exponent η ∈ (0, 1 - 1/α) (namely η = (1 - 1/α)/2) for the cutoff M_n = max 1 ⌊n^{1-η}⌋₊ of the proof (source lines 3259–3261).

theorem PoissonDeclumping.MaxLeafHeight.isBigO_of_eventually_mul_le {l : Filter ℕ} (hl : l ≤ Filter.atTop) {p : ℕ → ℝ} (hp : ∀ (n : ℕ), 0 ≤ p n) {K : ℝ} (hK : ∀ᶠ (n : ℕ) in l, ↑n * p n ≤ K) : p =O[l] fun (n : ℕ) => 1 / ↑n

p_n = O(1/n) from an eventual bound on n p_n, for nonnegative p.

theorem PoissonDeclumping.MaxLeafHeight.maxLeafHeight_unary {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h2 : PoissonApproximation2Statement) (hD : StableDomain μ α a) (hpos : 0 < μ 1) : ∃ (C : ℝ), 0 < C ∧ Filter.Tendsto (fun (j : ℕ) => (PlaneTree.bienayme μ).real {T : PlaneTree | j ≤ T.rootLeafHeight} / (μ 1).toReal ^ j) Filter.atTop (nhds C) ∧ LatticeGumbel μ PlaneTree.leafHeight (μ 1).toReal fun (n : ℕ) => (Real.log ↑n + Real.log ((1 - (μ 1).toReal) * C)) / Real.log (1 / (μ 1).toReal)

Theorem thm:max_lh(i) (source lines 536–543, 562–566; proof 3298–3326): if μ_1 > 0, C_μ = lim P(λ_∅(𝒯) ≥ j)/μ_1^j > 0 exists, and with k_n^* = (log n + log((1 - μ_1) C_μ))/log(1/μ_1), for every real t, P(λ(𝒯^n) ≤ ⌊k_n^* + t⌋) - exp(-μ_1^{t + 1 - {k_n^* + t}}) → 0 along admissible sizes.

theorem PoissonDeclumping.MaxLeafHeight.maxLeafHeight_superexp_of_cConst_pos {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (h2 : PoissonApproximation2Statement) (hD : StableDomain μ α a) (h0 : μ 1 = 0) (hcpos : 0 < LeafHeight.cConst μ) {x : ℕ → ℝ} (hx : ∀ (n : ℕ), x n = Real.logb (↑(LeafHeight.kappa μ)) (Real.log ↑n) - Real.logb (↑(LeafHeight.kappa μ)) (Real.log (1 / LeafHeight.leafD μ))) : TwoPointLocalization μ PlaneTree.leafHeight x

Theorem thm:max_lh(ii), case c = 1 - κ μ_κ > 0 (source lines 545–558; proof 3328–3383): for μ_1 = 0 and k_n^{**} = log_κ log n - log_κ log(1/D_μ), P(λ(𝒯^n) ∈ J_n) → 1, and P(λ(𝒯^n) = ⌊k_n^{**}⌋) → 1 in the interior phase.

theorem PoissonDeclumping.MaxLeafHeight.maxLeafHeight_of_cConst_eq_zero {μ : PMF ℕ} (h3 : MaxStringStatement) (hμ : InStableDomain μ) (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (hc0 : LeafHeight.cConst μ = 0) {x : ℕ → ℝ} (hx : ∀ (n : ℕ), x n = Real.logb (↑(LeafHeight.kappa μ)) (Real.log ↑n) - Real.logb (↑(LeafHeight.kappa μ)) (Real.log (1 / LeafHeight.leafD μ))) : TwoPointLocalization μ PlaneTree.leafHeight x

Theorem thm:max_lh(ii), case c = 0 (source lines 3274–3296): the law is supported on {0, κ}, λ = H_κ almost surely and k_n^{**} = t_n^{**}, so this is Theorem thm:max_string(ii) with r = κ.

theorem PoissonDeclumping.MaxLeafHeight.maxLeafHeight_of_approx2_maxString (h2 : PoissonApproximation2Statement) (h3 : MaxStringStatement) : MaxLeafHeightStatement

Theorem thm:max_lh (source lines 533–586), from Theorems thm:PoissonApproximation2 and thm:max_string.

theorem PoissonDeclumping.MaxLeafHeight.maxLeafHeight_of (_h1 : PoissonApproximationStatement) (h2 : PoissonApproximation2Statement) (h3 : MaxStringStatement) : MaxLeafHeightStatement

Theorem thm:max_lh, from Theorems thm:PoissonApproximation2 and thm:max_string as hypotheses (the unconditional form is PoissonDeclumping.maxLeafHeight). Theorem thm:PoissonApproximation is not used (the proof goes through Theorem thm:PoissonApproximation2 and Theorem thm:max_string).