Laws of shifted offspring sequences

Coordinate shifts preserve the iid offspring law, and the real increments have the canonical iid real-walk law. Stopping times of the coordinate filtration and their pre-stopped events are also defined here.

theorem BGW.StableTrees.DiscreteForest.map_shiftSeq_offspringSeqLaw (μ : PMF ℕ) (m : ℕ) : MeasureTheory.Measure.map (shiftSeq m) ↑(offspringSeqLaw μ) = ↑(offspringSeqLaw μ)

The iid sequence law is shift invariant.

theorem BGW.StableTrees.DiscreteForest.map_offspringSeqLaw_realIncrements (μ : PMF ℕ) : MeasureTheory.Measure.map (fun (ω : ℕ → ℕ) (i : ℕ) => ↑↑(ω i) - 1) ↑(offspringSeqLaw μ) = ↑(Probability.RealWalk.iidLaw (realOffspringStepLaw μ))

The walk (ω i - 1)_i of offspringSeqLaw μ is the iid real walk with step law realOffspringStepLaw μ.

def BGW.StableTrees.DiscreteForest.PreStopped (N : (ℕ → ℕ) → ℕ∞) (E : Set (ℕ → ℕ)) : Prop

E is determined, on {N = n}, by the first n coordinates, and so is {N = n}: the pre-N events of an ℕ∞-valued stopping time N of the coordinate filtration.

Equations

• BGW.StableTrees.DiscreteForest.PreStopped N E = ∀ (n : ℕ) (ω ω' : ℕ → ℕ), N ω = ↑n → (∀ i < n, ω i = ω' i) → N ω' = ↑n ∧ (ω ∈ E ↔ ω' ∈ E)

def BGW.StableTrees.DiscreteForest.IsSeqStoppingTime (N : (ℕ → ℕ) → ℕ∞) : Prop

A stopping time of the coordinate filtration with values in ℕ∞.

Equations

• BGW.StableTrees.DiscreteForest.IsSeqStoppingTime N = BGW.StableTrees.DiscreteForest.PreStopped N Set.univ