Regenerated height crossings and their iid durations

Crossing times are built by restarting the offspring sequence at each previous crossing. These are measurable, almost surely finite stopping times. Finite gap histories are pre-stopped events, so stopped iid restart proves independence and identifies every gap law with the first height-upcrossing law.

theorem BGW.StableTrees.HeightTightness.measurable_heightUpcrossingStop (q : ℕ) : Measurable (heightUpcrossingStop q)

First-upcrossing times are measurable, including their infinite value.

noncomputable def BGW.StableTrees.HeightTightness.nextHeightUpcrossing (q : ℕ) (N : (ℕ → ℕ) → ℕ∞) (ω : ℕ → ℕ) : ℕ∞

Advance a stopping time to the next upcrossing of the regenerated height.

Equations

• BGW.StableTrees.HeightTightness.nextHeightUpcrossing q N ω = N ω + BGW.StableTrees.HeightTightness.heightUpcrossingStop q (BGW.StableTrees.DiscreteForest.shiftSeq (N ω).toNat ω)

theorem BGW.StableTrees.HeightTightness.isSeqStoppingTime_nextHeightUpcrossing (q : ℕ) {N : (ℕ → ℕ) → ℕ∞} (hN : DiscreteForest.IsSeqStoppingTime N) : DiscreteForest.IsSeqStoppingTime (nextHeightUpcrossing q N)

Advancing to a regenerated height upcrossing preserves the stopping-time property.

theorem BGW.StableTrees.HeightTightness.map_stoppedShift_offspringSeqLaw (μ : PMF ℕ) {N : (ℕ → ℕ) → ℕ∞} (hNm : Measurable N) (hN : DiscreteForest.IsSeqStoppingTime N) (hfin : ∀ᵐ (ω : ℕ → ℕ) ∂↑(DiscreteForest.offspringSeqLaw μ), N ω ≠ ⊤) : MeasureTheory.Measure.map (fun (ω : ℕ → ℕ) => DiscreteForest.shiftSeq (N ω).toNat ω) ↑(DiscreteForest.offspringSeqLaw μ) = ↑(DiscreteForest.offspringSeqLaw μ)

Restarting the offspring sequence at a finite stopping time preserves its law.

theorem BGW.StableTrees.HeightTightness.measurable_nextHeightUpcrossing (q : ℕ) {N : (ℕ → ℕ) → ℕ∞} (hN : Measurable N) : Measurable (nextHeightUpcrossing q N)

Advancing to a regenerated upcrossing preserves measurability.

theorem BGW.StableTrees.HeightTightness.ae_nextHeightUpcrossing_ne_top (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (q : ℕ) {N : (ℕ → ℕ) → ℕ∞} (hNm : Measurable N) (hN : DiscreteForest.IsSeqStoppingTime N) (hfin : ∀ᵐ (ω : ℕ → ℕ) ∂↑(DiscreteForest.offspringSeqLaw μ), N ω ≠ ⊤) : ∀ᵐ (ω : ℕ → ℕ) ∂↑(DiscreteForest.offspringSeqLaw μ), nextHeightUpcrossing q N ω ≠ ⊤

Advancing an almost surely finite stopping time to a height upcrossing remains finite.

noncomputable def BGW.StableTrees.HeightTightness.heightRegenerationStop (q : ℕ) : ℕ → (ℕ → ℕ) → ℕ∞

Successive integer stopping times of regenerated height upcrossings.

Equations

• BGW.StableTrees.HeightTightness.heightRegenerationStop q 0 = fun (x : ℕ → ℕ) => 0
• BGW.StableTrees.HeightTightness.heightRegenerationStop q j.succ = BGW.StableTrees.HeightTightness.nextHeightUpcrossing q (BGW.StableTrees.HeightTightness.heightRegenerationStop q j)

theorem BGW.StableTrees.HeightTightness.isSeqStoppingTime_heightRegenerationStop (q j : ℕ) : DiscreteForest.IsSeqStoppingTime (heightRegenerationStop q j)

Every regenerated crossing time is a stopping time of the offspring filtration.

theorem BGW.StableTrees.HeightTightness.measurable_heightRegenerationStop (q j : ℕ) : Measurable (heightRegenerationStop q j)

Every regenerated crossing time is measurable.

theorem BGW.StableTrees.HeightTightness.ae_heightRegenerationStop_ne_top (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (q j : ℕ) : ∀ᵐ (ω : ℕ → ℕ) ∂↑(DiscreteForest.offspringSeqLaw μ), heightRegenerationStop q j ω ≠ ⊤

Every regenerated crossing time is almost surely finite.

theorem BGW.StableTrees.HeightTightness.monotone_heightRegenerationStop (q : ℕ) (ω : ℕ → ℕ) : Monotone fun (j : ℕ) => heightRegenerationStop q j ω

Crossing times increase with the number of regenerated upcrossings.

noncomputable def BGW.StableTrees.HeightTightness.heightRegenerationGap (q j : ℕ) (ω : ℕ → ℕ) : ℕ

The integer duration of a regenerated height crossing, read on finite crossing times.

Equations

• One or more equations did not get rendered due to their size.

theorem BGW.StableTrees.HeightTightness.measurable_heightRegenerationGap (q j : ℕ) : Measurable (heightRegenerationGap q j)

Every regenerated crossing duration is measurable.

theorem BGW.StableTrees.HeightTightness.heightRegenerationGap_history_factor (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (q i : ℕ) (S : Finset ℕ) (hS : ∀ j ∈ S, j < i) (A : ℕ → Set ℕ) {C : Set ℕ} (hC : MeasurableSet C) : ↑(DiscreteForest.offspringSeqLaw μ) ({ω : ℕ → ℕ | ∀ j ∈ S, heightRegenerationGap q j ω ∈ A j} ∩ {ω : ℕ → ℕ | heightRegenerationGap q i ω ∈ C}) = ↑(DiscreteForest.offspringSeqLaw μ) {ω : ℕ → ℕ | ∀ j ∈ S, heightRegenerationGap q j ω ∈ A j} * ↑(DiscreteForest.offspringSeqLaw μ) {ω : ℕ → ℕ | (heightUpcrossingStop q ω).toNat ∈ C}

Restart factors each regenerated crossing duration from all preceding finite gap histories.

theorem BGW.StableTrees.HeightTightness.map_heightRegenerationGap (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (q i : ℕ) : MeasureTheory.Measure.map (heightRegenerationGap q i) ↑(DiscreteForest.offspringSeqLaw μ) = MeasureTheory.Measure.map (fun (ω : ℕ → ℕ) => (heightUpcrossingStop q ω).toNat) ↑(DiscreteForest.offspringSeqLaw μ)

Every regenerated duration has the law of the first height upcrossing.

theorem BGW.StableTrees.HeightTightness.iIndepFun_heightRegenerationGap (μ : PMF ℕ) (hc : IsCritical μ) (hne : μ 1 ≠ 1) (q : ℕ) : ProbabilityTheory.iIndepFun (fun (j : ℕ) => heightRegenerationGap q j) ↑(DiscreteForest.offspringSeqLaw μ)

Durations between successive regenerated height crossings are independent.