Kolmogorov regularity of stable heights

The moment estimate supplies the vendored Kolmogorov condition on nonnegative time. A continuous modification agrees at every rational time on a common event, identifying it with the deterministic universal-sequence reconstruction.

theorem BGW.StableTrees.exists_height_isKolmogorovProcess {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {p : ℝ} (hp : 1 ≤ p) : ∃ (M : NNReal), ProbabilityTheory.IsKolmogorovProcess (fun (t : NNReal) (f : Skorokhod.DLoc) => height θ f t) (↑(stableLocalLaw θ)) p (p * (1 - 1 / θ)) M

The increment moment estimate gives the Kolmogorov condition with dimension one.

theorem BGW.StableTrees.exists_height_continuous_modification {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∃ (Y : NNReal → Skorokhod.DLoc → ℝ), (∀ (f : Skorokhod.DLoc), Continuous fun (t : NNReal) => Y t f) ∧ ∀ (t : NNReal), ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), Y t f = height θ f t

A sufficiently high moment gives a continuous modification on nonnegative time.

theorem BGW.StableTrees.ae_heightLoc_eq_modification {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (Y : NNReal → Skorokhod.DLoc → ℝ) (hY : ∀ (f : Skorokhod.DLoc), Continuous fun (t : NNReal) => Y t f) (hYeq : ∀ (t : NNReal), ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), Y t f = height θ f t) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), (∀ (t : NNReal), heightLoc θ f t = Y t f) ∧ ∀ (t : NNReal), IsRationalTime t → Y t f = heightUniv θ f t

A continuous modification is identified with rational reconstruction on one common event.

theorem BGW.StableTrees.ae_exists_continuous_height {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∃ (g : C(NNReal, ℝ)), ∀ (t : NNReal), IsRationalTime t → g t = heightUniv θ f t

Almost surely the rational heights (read along heightEps θ) extend continuously.

theorem BGW.StableTrees.ae_heightLoc_eq_height {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), heightLoc θ f t = height θ f t

Modification: for each fixed time, heightLoc agrees a.s. with H02's height.