Restart at discrete stopping times

Pre-stopped events have measurable slices determined by finitely many coordinates. Independence of each slice from the remaining coordinates gives stopped restart.

theorem BGW.StableTrees.DiscreteForest.stoppedRestart (μ : PMF ℕ) (N : (ℕ → ℕ) → ℕ∞) (hN : IsSeqStoppingTime N) (hfin : ∀ᵐ (ω : ℕ → ℕ) ∂↑(offspringSeqLaw μ), N ω ≠ ⊤) {E : Set (ℕ → ℕ)} (hE : PreStopped N E) {A : Set (ℕ → ℕ)} (hA : MeasurableSet A) : ↑(offspringSeqLaw μ) (E ∩ {ω : ℕ → ℕ | ∃ (n : ℕ), N ω = ↑n ∧ shiftSeq n ω ∈ A}) = ↑(offspringSeqLaw μ) E * ↑(offspringSeqLaw μ) A

(Stopped iid restart, finite guard) For an a.s. finite stopping time N, a pre-N event E and a measurable A, the restarted sequence shiftSeq N ω is independent of E and has the law P. Consequence of the product law (item 2 of the plan).

theorem BGW.StableTrees.DiscreteForest.stoppedRestart_height (μ : PMF ℕ) (N : (ℕ → ℕ) → ℕ∞) (hN : IsSeqStoppingTime N) (hfin : ∀ᵐ (ω : ℕ → ℕ) ∂↑(offspringSeqLaw μ), N ω ≠ ⊤) {E : Set (ℕ → ℕ)} (hE : PreStopped N E) {A : Set (ℕ → ℤ)} (hA : MeasurableSet A) : ↑(offspringSeqLaw μ) (E ∩ {ω : ℕ → ℕ | ∃ (n : ℕ), N ω = ↑n ∧ (fun (k : ℕ) => shiftedHeight ω n k) ∈ A}) = ↑(offspringSeqLaw μ) E * ↑(offspringSeqLaw μ) {ω : ℕ → ℕ | (fun (k : ℕ) => ↑(forestHeight ω k)) ∈ A}

(Regeneration of the height at a stopping time) For N a.s. finite stopping time and E pre-N, the height seen from N is independent of E and has the law of the height.