Agreement of continuous and universal heights at almost every host time

Fubini on countably many bounded windows puts the a.e.-age identities on a single host event. Literal prefix locality then identifies both reconstructions at every horizon on that event.

theorem BGW.StableTrees.ae_heightLoc_eq_heightUniv_ae {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), heightLoc θ f s.toNNReal = heightUniv θ f s.toNNReal

A.e.-time identity on the host: almost surely, the continuous height equals the universal raw height at Lebesgue-almost every time.

theorem BGW.StableTrees.isPrefixHeightVersion_restrict_of_ae (θ : ℝ) (f : Skorokhod.DLoc) (hf : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), heightLoc θ f s.toNNReal = heightUniv θ f s.toNNReal) (T : NNReal) : IsPrefixHeightVersion θ T (Skorokhod.DLoc.restrict T f) { toFun := fun (t : ↑(Set.Icc 0 ↑T)) => heightLoc θ f ⟨↑t, ⋯⟩, continuous_toFun := ⋯ }

An a.e.-time host agreement gives a version on each compact prefix.

theorem BGW.StableTrees.ae_heightPrefixAE_eq_heightPrefix {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (T : NNReal), heightPrefixAE θ T (Skorokhod.DLoc.restrict T f) = heightPrefix θ T (Skorokhod.DLoc.restrict T f)

Under the stable law, the a.e.-time prefix map and H03's rational-time prefix map agree on the restricted path, simultaneously for all horizons.