First-order consequences of Theorem thm:max_lh (inventory U03)

Source lines 574–581: Theorem thm:max_lh implies λ(𝒯^n)/log n → 1/log(1/μ_1) in probability if μ_1 > 0, and λ(𝒯^n)/log_κ log n → 1 in probability if μ_1 = 0, κ = min{i ≥ 2 : μ_i > 0}. "In probability" is stated as P(|λ(𝒯^n)/ℓ_n - ℓ| > ε) → 0 for every ε > 0, along admissible sizes.

• tendsto_div_log_of_latticeGumbel: any lattice-modulated Gumbel limit (LatticeGumbel) with centering (log n + c)/log(1/q), 0 < q < 1, gives H(𝒯^n)/log n → 1/log(1/q);
• tendsto_div_logb_of_twoPoint: any two-point localization (TwoPointLocalization) with centering log_κ log n - c, κ ≥ 2, gives H(𝒯^n)/log_κ log n → 1;
• leafHeight_div_log_tendsto, leafHeight_div_logb_log_tendsto: the two consequences, derived from MaxLeafHeightStatement itself (so they hold as soon as Theorem thm:max_lh does, e.g. through MaxLeafHeight.maxLeafHeight_of).

theorem PoissonDeclumping.MaxLeafHeight.tendsto_log_natCast_admissible (μ : PMF ℕ) : Filter.Tendsto (fun (n : ℕ) => Real.log ↑n) (admissibleSizes μ) Filter.atTop

log n → ∞ along admissible sizes.

theorem PoissonDeclumping.MaxLeafHeight.tendsto_div_log_of_latticeGumbel {μ : PMF ℕ} {H : PlaneTree → ℕ} {q c : ℝ} (hq0 : 0 < q) (hq1 : q < 1) (hG : LatticeGumbel μ H q fun (n : ℕ) => (Real.log ↑n + c) / Real.log (1 / q)) {ε : ℝ} (hε : 0 < ε) : Filter.Tendsto (fun (n : ℕ) => (PlaneTree.conditioned μ n).real {T : PlaneTree | ε < |↑(H T) / Real.log ↑n - 1 / Real.log (1 / q)|}) (admissibleSizes μ) (nhds 0)

First-order consequence of a lattice-modulated Gumbel limit with centering x_n = (log n + c)/log(1/q): H(𝒯^n)/log n → 1/log(1/q) in probability.

theorem PoissonDeclumping.MaxLeafHeight.tendsto_div_logb_of_twoPoint {μ : PMF ℕ} {H : PlaneTree → ℕ} {κ : ℕ} (hκ : 2 ≤ κ) {c : ℝ} (hTP : TwoPointLocalization μ H fun (n : ℕ) => Real.logb (↑κ) (Real.log ↑n) - c) {ε : ℝ} (hε : 0 < ε) : Filter.Tendsto (fun (n : ℕ) => (PlaneTree.conditioned μ n).real {T : PlaneTree | ε < |↑(H T) / Real.logb (↑κ) (Real.log ↑n) - 1|}) (admissibleSizes μ) (nhds 0)

First-order consequence of the two-point localization with centering x_n = log_κ log n - c, κ ≥ 2: H(𝒯^n)/log_κ log n → 1 in probability.

theorem PoissonDeclumping.MaxLeafHeight.leafHeight_div_log_tendsto {μ : PMF ℕ} (h : MaxLeafHeightStatement) (hμ : InStableDomain μ) (hpos : 0 < μ 1) {ε : ℝ} (hε : 0 < ε) : Filter.Tendsto (fun (n : ℕ) => (PlaneTree.conditioned μ n).real {T : PlaneTree | ε < |↑T.leafHeight / Real.log ↑n - 1 / Real.log (1 / (μ 1).toReal)|}) (admissibleSizes μ) (nhds 0)

U03, first-order consequence of Theorem thm:max_lh(i) (source lines 574–577): if μ_1 > 0, then λ(𝒯^n)/log n → 1/log(1/μ_1) in probability (along admissible sizes).

theorem PoissonDeclumping.MaxLeafHeight.leafHeight_div_logb_log_tendsto {μ : PMF ℕ} (h : MaxLeafHeightStatement) (hμ : InStableDomain μ) (h0 : μ 1 = 0) {ε : ℝ} (hε : 0 < ε) : Filter.Tendsto (fun (n : ℕ) => (PlaneTree.conditioned μ n).real {T : PlaneTree | ε < |↑T.leafHeight / Real.logb (↑(sInf {i : ℕ | 2 ≤ i ∧ 0 < μ i})) (Real.log ↑n) - 1|}) (admissibleSizes μ) (nhds 0)

U03, first-order consequence of Theorem thm:max_lh(ii) (source lines 574–578): if μ_1 = 0 and κ = min{i ≥ 2 : μ_i > 0}, then λ(𝒯^n)/log_κ log n → 1 in probability (along admissible sizes).