Transform of attained weak ladder heights

Stopped restart gives the product formula for transforms of epoch heights. This retains zero height increments and does not require finite increment variance.

theorem BGW.StableTrees.DiscreteHeightApprox.weakEpochHeight_succ {ω : ℕ → ℕ} (hω : EpochsFinite ω) (i : ℕ) : weakEpochHeight ω (i + 1) = weakEpochHeight ω i + weakEpochHeight (epochRestart i ω) 1

Successive attained heights add the first height of the restarted sequence.

noncomputable def BGW.StableTrees.DiscreteHeightApprox.weakLadderPGF (μ : PMF ℕ) (s : ENNReal) : ENNReal

The nonnegative generating transform of the first weak ascending ladder height.

Equations

• BGW.StableTrees.DiscreteHeightApprox.weakLadderPGF μ s = ∫⁻ (ω : ℕ → ℕ), s ^ BGW.StableTrees.DiscreteHeightApprox.weakEpochHeight ω 1 ∂↑(BGW.StableTrees.DiscreteForest.offspringSeqLaw μ)

theorem BGW.StableTrees.DiscreteHeightApprox.lintegral_epochHeight (μ : PMF ℕ) (i : ℕ) (f : ℕ → ENNReal) : ∫⁻ (ω : ℕ → ℕ), f (weakEpochHeight ω i) ∂↑(DiscreteForest.offspringSeqLaw μ) = ∑' (h : ℕ), f h * ↑(DiscreteForest.offspringSeqLaw μ) {ω : ℕ → ℕ | weakEpochHeight ω i = h}

A nonnegative observable of one attained epoch height integrates against its discrete law.

theorem BGW.StableTrees.DiscreteHeightApprox.weakLadderPGF_eq_tsum (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (s : ENNReal) : weakLadderPGF μ s = ∑' (h : ℕ), s ^ h * μ.toMeasure (Set.Ici (h + 1))

The first ladder-height PGF has offspring tails as its coefficients.

theorem BGW.StableTrees.DiscreteHeightApprox.lintegral_epochHeight_pow (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (s : ENNReal) (i : ℕ) : ∫⁻ (ω : ℕ → ℕ), s ^ weakEpochHeight ω i ∂↑(DiscreteForest.offspringSeqLaw μ) = weakLadderPGF μ s ^ i

The transform of the ith attained height is the ith power of the first-height transform.