Deterministic reconstruction of continuous heights

Rational evaluations determine a continuous height uniquely, including on a singleton horizon. Constant extension preserves the compact prefix literally.

def BGW.StableTrees.IsRationalTime (t : NNReal) : Prop

t is a rational time.

Equations

• BGW.StableTrees.IsRationalTime t = ∃ (q : ℚ), ↑q = ↑t

noncomputable def BGW.StableTrees.heightLoc (θ : ℝ) (f : Skorokhod.DLoc) : NNReal → ℝ

The continuous height process: the continuous function agreeing with heightUniv θ f at every rational time when one exists (it is then unique), the zero function otherwise.

Equations

• One or more equations did not get rendered due to their size.

theorem BGW.StableTrees.continuous_heightLoc (θ : ℝ) (f : Skorokhod.DLoc) : Continuous (heightLoc θ f)

Every path of heightLoc is continuous.

theorem BGW.StableTrees.dense_isRationalTime : Dense {t : NNReal | IsRationalTime t}

Rational nonnegative times are dense.

theorem BGW.StableTrees.heightLoc_eq_of_rational_agreement (θ : ℝ) (f : Skorokhod.DLoc) (g : C(NNReal, ℝ)) (hg : ∀ (t : NNReal), IsRationalTime t → g t = heightUniv θ f t) : heightLoc θ f = ⇑g

Continuous extensions of the same rational heights coincide.

theorem BGW.StableTrees.heightLoc_zero (θ : ℝ) (f : Skorokhod.DLoc) : heightLoc θ f 0 = 0

The continuous height starts at 0 for every path (height θ f 0 = 0 surely).

theorem BGW.StableTrees.heightLoc_nonneg (θ : ℝ) (f : Skorokhod.DLoc) (t : NNReal) : 0 ≤ heightLoc θ f t

The continuous height is nonnegative for every path.

noncomputable def BGW.StableTrees.extendConst (T : NNReal) (g : Skorokhod.D ↑T ℝ) : Skorokhod.DLoc

Extension of a path on [0,T] by its terminal value (the junk branch never occurs).

Equations

• BGW.StableTrees.extendConst T g = if h : IsCadlag fun (u : NNReal) => g (Set.projIcc 0 ↑T ⋯ ↑u) then ⟨fun (u : NNReal) => g (Set.projIcc 0 ↑T ⋯ ↑u), h⟩ else BGW.Skorokhod.DLoc.zero

noncomputable def BGW.StableTrees.heightPrefix (θ : ℝ) (T : NNReal) (g : Skorokhod.D ↑T ℝ) : C(↑(Set.Icc 0 ↑T), ℝ)

Prefix height map on [0,T]: the continuous function on [0,T] agreeing with heightUniv of extendConst T g at the rational times of [0,T] when one exists, 0 otherwise.

Equations

• One or more equations did not get rendered due to their size.

theorem BGW.StableTrees.isCadlag_extendConst_fun (T : NNReal) (g : Skorokhod.D ↑T ℝ) : IsCadlag fun (u : NNReal) => g (Set.projIcc 0 ↑T ⋯ ↑u)

Constant extension is càdlàg, including at the terminal time.

theorem BGW.StableTrees.restrict_extendConst (T : NNReal) (g : Skorokhod.D ↑T ℝ) : Skorokhod.DLoc.restrict T (extendConst T g) = g

Restricting constant extension gives the original path.

theorem BGW.StableTrees.measurable_extendConst (T : NNReal) : Measurable (extendConst T)

Constant extension is measurable for the evaluation sigma algebra.

theorem BGW.StableTrees.height_eq_of_restrict_eq (θ : ℝ) (T : NNReal) (f g : Skorokhod.DLoc) (hfg : Skorokhod.DLoc.restrict T f = Skorokhod.DLoc.restrict T g) (t : NNReal) (ht : t ≤ T) : height θ f t = height θ g t

Literal prefix locality of the raw height: height θ f t reads f only on [0,t].

theorem BGW.StableTrees.dense_prefix_rationals (T : NNReal) : Dense {t : ↑(Set.Icc 0 ↑T) | ∃ (q : ℚ), ↑q = ↑t}

Rational times are dense in a compact nonnegative interval.

theorem BGW.StableTrees.continuousMap_ext_rational (T : NNReal) (c d : C(↑(Set.Icc 0 ↑T), ℝ)) (h : ∀ (t : ↑(Set.Icc 0 ↑T)), (∃ (q : ℚ), ↑q = ↑t) → c t = d t) : c = d

Rational times in a compact nonnegative interval determine continuous functions.

theorem BGW.StableTrees.measurable_height_fixed (θ : ℝ) (t : NNReal) : Measurable fun (f : Skorokhod.DLoc) => height θ f t

The fixed-time height is measurable.

theorem BGW.StableTrees.heightPrefix_eq_of_rational_agreement (θ : ℝ) (T : NNReal) (f : Skorokhod.DLoc) (c : C(↑(Set.Icc 0 ↑T), ℝ)) (hc : ∀ (t : ↑(Set.Icc 0 ↑T)), IsRationalTime ⟨↑t, ⋯⟩ → c t = heightUniv θ f ⟨↑t, ⋯⟩) : heightPrefix θ T (Skorokhod.DLoc.restrict T f) = c

Deterministic reconstruction: a continuous function on [0,T] agreeing with heightUniv θ f at the rational times of [0,T] is the prefix height of f (no law involved; used by H04 under the excursion measures).