Determination of a joint walk and continuous-height law

Keeping the whole walk and observing the height at arbitrary finite sets of times determines the joint law. Projective uniqueness identifies the associated coordinate laws; the Borel sigma algebra of continuous paths is generated by evaluations.

def BGW.StableTrees.HeightTightness.heightPairEval (T : NNReal) {r : ℕ} (t : Fin r → ↑(Set.Icc 0 ↑T)) (p : Skorokhod.D ↑T ℝ × C(↑(Set.Icc 0 ↑T), ℝ)) : Skorokhod.D ↑T ℝ × (Fin r → ℝ)

Keep the whole walk and observe the height at finitely many deterministic times.

Equations

• BGW.StableTrees.HeightTightness.heightPairEval T t p = (p.1, fun (i : Fin r) => p.2 (t i))

theorem BGW.StableTrees.HeightTightness.continuous_heightPairEval (T : NNReal) {r : ℕ} (t : Fin r → ↑(Set.Icc 0 ↑T)) : Continuous (heightPairEval T t)

Finite height observation with the whole walk is continuous.

theorem BGW.StableTrees.HeightTightness.pairLaw_ext_of_height_observations {T : NNReal} {P Q : MeasureTheory.ProbabilityMeasure (Skorokhod.D ↑T ℝ × C(↑(Set.Icc 0 ↑T), ℝ))} (h : ∀ {r : ℕ} (t : Fin r → ↑(Set.Icc 0 ↑T)), P.map (heightPairEval T t) = Q.map (heightPairEval T t)) : P = Q

The whole walk together with all finite height observations determines the joint path law.