The root leaf-height recursion

Section 7 of the paper (source lines 2911–2958). For an offspring law μ, put g(x) = ∑_{j ≥ 1} μ_j x^j = G_μ(x) - μ_0 and define π_0 = 1, π_{k+1} = g(π_k). For the Bienaymé tree, π_k = P(λ_∅(𝒯) ≥ k) (this identification is proved separately); here π_k is the purely analytic sequence (inventory item U10).

The paper sets π_k = 1 for k ≤ 0; this convention is encoded by piSeqZ, indexed by ℤ.

We also define κ = min{j ≥ 1 : μ_j > 0} (source lines 2913 and 3031) and prove the basic two-sided bound μ_κ x^κ ≤ g(x) ≤ μ_κ x^κ + x^{κ+1} on [0, 1], together with g(x) ≤ (1 - μ_0) x. For a critical μ with μ_1 ≠ 1, these give that π_k is positive, strictly decreasing and tends to zero (item (a) of the analysis of Lemma lem:ell_asymp).

noncomputable def PoissonDeclumping.LeafHeight.mass (μ : PMF ℕ) (j : ℕ) : ℝ

The real offspring mass μ_j.

Equations

• PoissonDeclumping.LeafHeight.mass μ j = (μ j).toReal

noncomputable def PoissonDeclumping.LeafHeight.g (μ : PMF ℕ) (x : ℝ) : ℝ

The function g(x) = ∑_{j ≥ 1} μ_j x^j of the proof of Lemma lem:ell_asymp.

Equations

• PoissonDeclumping.LeafHeight.g μ x = ∑' (j : ℕ), PoissonDeclumping.LeafHeight.mass μ (j + 1) * x ^ (j + 1)

noncomputable def PoissonDeclumping.LeafHeight.piSeq (μ : PMF ℕ) : ℕ → ℝ

The sequence π_0 = 1, π_{k+1} = g(π_k). For a Bienaymé tree it is the tail P(λ_∅(𝒯) ≥ k) of the root leaf-height.

Equations

• PoissonDeclumping.LeafHeight.piSeq μ 0 = 1
• PoissonDeclumping.LeafHeight.piSeq μ k.succ = PoissonDeclumping.LeafHeight.g μ (PoissonDeclumping.LeafHeight.piSeq μ k)

noncomputable def PoissonDeclumping.LeafHeight.piSeqZ (μ : PMF ℕ) (k : ℤ) : ℝ

The paper's convention π_k = 1 for k ≤ 0, as an integer-indexed sequence.

Equations

• PoissonDeclumping.LeafHeight.piSeqZ μ k = PoissonDeclumping.LeafHeight.piSeq μ k.toNat

noncomputable def PoissonDeclumping.LeafHeight.ellSeq (μ : PMF ℕ) (k : ℕ) : ℝ

ℓ_k = π_k - π_{k+1}, which is P(λ_∅(𝒯) = k) for a Bienaymé tree.

Equations

• PoissonDeclumping.LeafHeight.ellSeq μ k = PoissonDeclumping.LeafHeight.piSeq μ k - PoissonDeclumping.LeafHeight.piSeq μ (k + 1)

noncomputable def PoissonDeclumping.LeafHeight.kappa (μ : PMF ℕ) : ℕ

κ = min{j ≥ 1 : μ_j > 0} (source lines 2913, 3031).

Equations

• PoissonDeclumping.LeafHeight.kappa μ = sInf {j : ℕ | 1 ≤ j ∧ 0 < μ j}

@[simp]

theorem PoissonDeclumping.LeafHeight.piSeq_zero {μ : PMF ℕ} : piSeq μ 0 = 1

theorem PoissonDeclumping.LeafHeight.piSeq_succ {μ : PMF ℕ} (k : ℕ) : piSeq μ (k + 1) = g μ (piSeq μ k)

theorem PoissonDeclumping.LeafHeight.piSeqZ_natCast {μ : PMF ℕ} (k : ℕ) : piSeqZ μ ↑k = piSeq μ k

theorem PoissonDeclumping.LeafHeight.piSeqZ_of_nonpos {μ : PMF ℕ} {k : ℤ} (hk : k ≤ 0) : piSeqZ μ k = 1

Real masses

theorem PoissonDeclumping.LeafHeight.mass_nonneg {μ : PMF ℕ} (j : ℕ) : 0 ≤ mass μ j

theorem PoissonDeclumping.LeafHeight.mass_le_one {μ : PMF ℕ} (j : ℕ) : mass μ j ≤ 1

theorem PoissonDeclumping.LeafHeight.mass_pos_iff {μ : PMF ℕ} (j : ℕ) : 0 < mass μ j ↔ 0 < μ j

theorem PoissonDeclumping.LeafHeight.hasSum_mass {μ : PMF ℕ} : HasSum (mass μ) 1

theorem PoissonDeclumping.LeafHeight.summable_mass {μ : PMF ℕ} : Summable (mass μ)

theorem PoissonDeclumping.LeafHeight.tsum_mass {μ : PMF ℕ} : ∑' (j : ℕ), mass μ j = 1

theorem PoissonDeclumping.LeafHeight.hasSum_mean {μ : PMF ℕ} (hc : IsCritical μ) : HasSum (fun (j : ℕ) => ↑j * mass μ j) 1

The mean of μ, in real numbers, for a critical law.

theorem PoissonDeclumping.LeafHeight.exists_two_le_pos {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) : ∃ (j : ℕ), 2 ≤ j ∧ 0 < μ j

A critical law with μ_1 ≠ 1 charges some j ≥ 2.

theorem PoissonDeclumping.LeafHeight.mass_zero_pos {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) : 0 < mass μ 0

A critical law with μ_1 ≠ 1 has μ_0 > 0.

theorem PoissonDeclumping.LeafHeight.mass_zero_le_one {μ : PMF ℕ} : mass μ 0 ≤ 1

The index κ

theorem PoissonDeclumping.LeafHeight.kappa_mem {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) : 1 ≤ kappa μ ∧ 0 < μ (kappa μ)

theorem PoissonDeclumping.LeafHeight.one_le_kappa {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) : 1 ≤ kappa μ

theorem PoissonDeclumping.LeafHeight.mass_kappa_pos {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) : 0 < mass μ (kappa μ)

theorem PoissonDeclumping.LeafHeight.mass_eq_zero_of_lt_kappa {μ : PMF ℕ} {j : ℕ} (hj : 1 ≤ j) (hjk : j < kappa μ) : mass μ j = 0

theorem PoissonDeclumping.LeafHeight.kappa_eq_one {μ : PMF ℕ} (hpos : 0 < μ 1) : kappa μ = 1

theorem PoissonDeclumping.LeafHeight.two_le_kappa {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (h0 : μ 1 = 0) : 2 ≤ kappa μ

theorem PoissonDeclumping.LeafHeight.kappa_eq_sInf_two {μ : PMF ℕ} (h0 : μ 1 = 0) : kappa μ = sInf {j : ℕ | 2 ≤ j ∧ 0 < μ j}

When μ_1 = 0, κ is the index min{j ≥ 2 : μ_j > 0} of Theorem thm:max_lh(ii).

Bounds on g

theorem PoissonDeclumping.LeafHeight.summable_g {μ : PMF ℕ} {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : Summable fun (j : ℕ) => mass μ (j + 1) * x ^ (j + 1)

theorem PoissonDeclumping.LeafHeight.g_nonneg {μ : PMF ℕ} {x : ℝ} (hx0 : 0 ≤ x) : 0 ≤ g μ x

theorem PoissonDeclumping.LeafHeight.g_eq_pgf_sub {μ : PMF ℕ} {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : g μ x = ∑' (j : ℕ), mass μ j * x ^ j - mass μ 0

g = G_μ - μ_0 on [0, 1], where G_μ is the generating function of μ.

theorem PoissonDeclumping.LeafHeight.tsum_mass_succ {μ : PMF ℕ} : ∑' (j : ℕ), mass μ (j + 1) = 1 - mass μ 0

theorem PoissonDeclumping.LeafHeight.g_le_mul {μ : PMF ℕ} {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : g μ x ≤ (1 - mass μ 0) * x

g(x) ≤ (1 - μ_0) x on [0, 1].

theorem PoissonDeclumping.LeafHeight.mass_mul_pow_le_g {μ : PMF ℕ} {x : ℝ} {m : ℕ} (hm : 1 ≤ m) (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : mass μ m * x ^ m ≤ g μ x

Each term gives a lower bound: μ_m x^m ≤ g(x) for m ≥ 1 and x ∈ [0, 1].

theorem PoissonDeclumping.LeafHeight.g_le_mass_mul_pow_add {μ : PMF ℕ} {x : ℝ} {m : ℕ} (hm : 1 ≤ m) (hzero : ∀ (j : ℕ), 1 ≤ j → j < m → mass μ j = 0) (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : g μ x ≤ mass μ m * x ^ m + x ^ (m + 1)

Upper bound: if μ_j = 0 for 1 ≤ j < m, then g(x) ≤ μ_m x^m + x^{m+1} on [0, 1].

theorem PoissonDeclumping.LeafHeight.g_bounds {μ : PMF ℕ} {x : ℝ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : mass μ (kappa μ) * x ^ kappa μ ≤ g μ x ∧ g μ x ≤ mass μ (kappa μ) * x ^ kappa μ + x ^ (kappa μ + 1)

The two-sided bound μ_κ x^κ ≤ g(x) ≤ μ_κ x^κ + x^{κ+1} on [0, 1].

Item (a): positivity, strict decrease and convergence to zero

theorem PoissonDeclumping.LeafHeight.piSeq_pos_le_one {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (k : ℕ) : 0 < piSeq μ k ∧ piSeq μ k ≤ 1

theorem PoissonDeclumping.LeafHeight.piSeq_pos {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (k : ℕ) : 0 < piSeq μ k

theorem PoissonDeclumping.LeafHeight.piSeq_le_one {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (k : ℕ) : piSeq μ k ≤ 1

theorem PoissonDeclumping.LeafHeight.piSeq_succ_le_mul {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (k : ℕ) : piSeq μ (k + 1) ≤ (1 - mass μ 0) * piSeq μ k

theorem PoissonDeclumping.LeafHeight.piSeq_succ_lt {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (k : ℕ) : piSeq μ (k + 1) < piSeq μ k

theorem PoissonDeclumping.LeafHeight.strictAnti_piSeq {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) : StrictAnti (piSeq μ)

π_k is strictly decreasing.

theorem PoissonDeclumping.LeafHeight.antitone_piSeq {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) : Antitone (piSeq μ)

theorem PoissonDeclumping.LeafHeight.piSeq_le_pow {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (k : ℕ) : piSeq μ k ≤ (1 - mass μ 0) ^ k

theorem PoissonDeclumping.LeafHeight.tendsto_piSeq_zero {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) : Filter.Tendsto (piSeq μ) Filter.atTop (nhds 0)

π_k → 0 (extinction of the critical non-degenerate process).

theorem PoissonDeclumping.LeafHeight.ellSeq_pos {μ : PMF ℕ} (hc : IsCritical μ) (h1 : μ 1 ≠ 1) (k : ℕ) : 0 < ellSeq μ k