Pre-return duality and finiteness of weak ascending epochs

Negative prefixes are expressed without a totalized hitting time, and finite reversal identifies their level occupations with first downward passages. Duality thus computes occupation before the first return without assuming its finiteness. Factoring the final independent step and summing offspring tails gives return mass one, since the offspring mean is one. Shift invariance then gives all weak epochs.

def BGW.StableTrees.DiscreteHeightApprox.NegativePrefix (ω : ℕ → ℕ) (n : ℕ) : Prop

Strict negativity at positive times through n, before the first weak return.

Equations

• BGW.StableTrees.DiscreteHeightApprox.NegativePrefix ω n = ∀ (u : ℕ), 1 ≤ u → u ≤ n → BGW.StableTrees.DiscreteForest.walk ω u < 0

def BGW.StableTrees.DiscreteHeightApprox.negativeLevelEvent (y n : ℕ) : Set (ℕ → ℕ)

Occupation of gap y at time n before any weak ascending return.

Equations

• BGW.StableTrees.DiscreteHeightApprox.negativeLevelEvent y n = {ω : ℕ → ℕ | BGW.StableTrees.DiscreteForest.walk ω n = -↑y ∧ BGW.StableTrees.DiscreteHeightApprox.NegativePrefix ω n}

theorem BGW.StableTrees.DiscreteHeightApprox.measurableSet_negativeLevelEvent (y n : ℕ) : MeasurableSet (negativeLevelEvent y n)

Negative level occupations are measurable finite-prefix events.

theorem BGW.StableTrees.DiscreteHeightApprox.tsum_negativeLevelEvent_mass (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (y : ℕ) : ∑' (n : ℕ), ↑(DiscreteForest.offspringSeqLaw μ) (negativeLevelEvent y n) = 1

The expected pre-return occupation of each integer gap is exactly one, expressed as a nonnegative series without presupposing return finiteness.

theorem BGW.StableTrees.DiscreteHeightApprox.preStopped_negativeLevelEvent (y n : ℕ) : DiscreteForest.PreStopped (fun (x : ℕ → ℕ) => ↑n) (negativeLevelEvent y n)

A negative-level event is determined by the offspring prefix before its time.

theorem BGW.StableTrees.DiscreteHeightApprox.tsum_offspring_tails (μ : PMF ℕ) (hc : IsCritical μ) : ∑' (y : ℕ), μ.toMeasure (Set.Ici (y + 1)) = 1

The sum of offspring upper tails is exactly the offspring mean.

theorem BGW.StableTrees.DiscreteHeightApprox.ae_hasWeakReturn (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) : ∀ᵐ (ω : ℕ → ℕ) ∂↑(DiscreteForest.offspringSeqLaw μ), ∃ (u : ℕ), 0 < u ∧ 0 ≤ DiscreteForest.walk ω u

A critical nondegenerate walk has a positive-time weak upward return almost surely.

theorem BGW.StableTrees.DiscreteHeightApprox.ae_epochsFinite (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) : ∀ᵐ (ω : ℕ → ℕ) ∂↑(DiscreteForest.offspringSeqLaw μ), EpochsFinite ω

Critical nondegenerate walks oscillate: all weak epochs are a.s. finite.