Documentation

BGW.StableTrees.DiscreteHeightApproxLadderPGF

The weak ladder-height PGF identity #

The centered one-step Laplace expansion from SurvivalExpansion supplies the normalized offspring PGF gap at exponential arguments, retaining the index-two infinite-variance case. The offspring-tail coefficients satisfy a one-step difference identity. Summing it against powers gives (1-s) φ(s) = 1-g(s), with the atom at zero retained.

source
noncomputable def BGW.StableTrees.DiscreteHeightApprox.offspringPGFReal (μ : PMF ℕ) (s : ℝ) :
ℝ

Real-variable offspring PGF (internal interface for the Laplace bridge).

Equations
Instances For
    source
    theorem BGW.StableTrees.DiscreteHeightApprox.norming_offspringPGF_gap {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {lam : ℝ} (hlam : 0 < lam) :
    Filter.Tendsto (fun (n : ℕ) => ↑n * (offspringPGFReal μ (Real.exp (-lam / B n)) - Real.exp (-lam / B n))) Filter.atTop (nhds (lam ^ θ))

    Laplace bridge from StableDomain (finding 3): a real proof obligation.

    source
    theorem BGW.StableTrees.DiscreteHeightApprox.weakLadderPGF_le_one (μ : PMF ℕ) {s : ENNReal} (hs : s ≤ 1) :
    weakLadderPGF μ s ≤ 1

    The ladder PGF is at most one at arguments in the unit interval.

    source
    theorem BGW.StableTrees.DiscreteHeightApprox.weakLadderPGF_identity (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) {s : ℝ} (hs0 : 0 ≤ s) (hs1 : s ≤ 1) :
    offspringPGFReal μ s + (1 - s) * (weakLadderPGF μ (ENNReal.ofReal s)).toReal = 1

    The first ladder PGF has the exact offspring generating-function identity.

    source
    theorem BGW.StableTrees.DiscreteHeightApprox.one_sub_weakLadderPGF (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) {s : ℝ} (hs0 : 0 ≤ s) (hs1 : s < 1) :
    1 - (weakLadderPGF μ (ENNReal.ofReal s)).toReal = (offspringPGFReal μ s - s) / (1 - s)

    The complement of the ladder PGF equals the offspring PGF gap divided by 1-s.

    source
    theorem BGW.StableTrees.DiscreteHeightApprox.weakLadderPGF_lt_one (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) {s : ℝ} (hs0 : 0 ≤ s) (hs1 : s < 1) :
    weakLadderPGF μ (ENNReal.ofReal s) < 1

    The ladder PGF is strictly less than one below one, for a nondegenerate critical law.