Exact occupation mean in a weak ascending cycle

The nonnegative occupation series obtained by reversal agrees almost surely with the finite first-cycle count. Its integral is one at every integer gap, including zero. No second moment assumption is used for this normalization.

noncomputable def BGW.StableTrees.DiscreteHeightApprox.levelOccupation (y : ℕ) (ω : ℕ → ℕ) : ENNReal

Nonnegative pre-return occupation series at one integer gap.

Equations

• BGW.StableTrees.DiscreteHeightApprox.levelOccupation y ω = ∑' (n : ℕ), (BGW.StableTrees.DiscreteHeightApprox.negativeLevelEvent y n).indicator (fun (x : ℕ → ℕ) => 1) ω

theorem BGW.StableTrees.DiscreteHeightApprox.measurable_levelOccupation (y : ℕ) : Measurable (levelOccupation y)

The pre-return occupation series is measurable.

theorem BGW.StableTrees.DiscreteHeightApprox.lintegral_levelOccupation (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (y : ℕ) : ∫⁻ (ω : ℕ → ℕ), levelOccupation y ω ∂↑(DiscreteForest.offspringSeqLaw μ) = 1

The pre-return occupation series has nonnegative integral one.

theorem BGW.StableTrees.DiscreteHeightApprox.levelOccupation_eq_card {ω : ℕ → ℕ} (hω : EpochsFinite ω) (y : ℕ) : levelOccupation y ω = ↑{u ∈ Finset.Ico 0 (weakEpoch ω 1) | reflGap ω u = ↑y}.card

On finite paths, the occupation series is the finite first-cycle level count.

theorem BGW.StableTrees.DiscreteHeightApprox.clusterLevelMean (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (y : ℕ) : ∫ (ω : ℕ → ℕ), ↑{u ∈ Finset.Ico 0 (weakEpoch ω 1) | reflGap ω u = ↑y}.card ∂↑(DiscreteForest.offspringSeqLaw μ) = 1

Key normalization supplier (exact mean). In the first cycle [0, τ_1) the expected number of times at gap exactly y equals 1 for every y ∈ ℕ (duality with the strict descending ladder process, whose heights are 1 by downward skip-freeness).