Continuous excursion heights from almost every age

Versions agree with the universal height at Lebesgue-almost every interior age. Continuity and the prescribed boundary values make versions unique, even when the prefix horizon is zero.

def BGW.StableTrees.IsExcursionHeightVersion (θ : ℝ) (e : Excursion) (g : C(NNReal, ℝ)) : Prop

g is an a.e.-age height version of the excursion e: it vanishes at time 0 and at and after the lifetime, and agrees with heightUniv θ e.path at Lebesgue-almost every age of (0, ζ(e)).

Equations

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

noncomputable def BGW.StableTrees.excursionHeight (θ : ℝ) (e : Excursion) : C(NNReal, ℝ)

The excursion height: the a.e.-age height version of e when one exists (it is then unique), the zero function otherwise.

Equations

• BGW.StableTrees.excursionHeight θ e = if h : ∃ (g : C(NNReal, ℝ)), BGW.StableTrees.IsExcursionHeightVersion θ e g then Classical.choose h else 0

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

c is an a.e.-time prefix height version of g : D T ℝ: it vanishes at time 0 and agrees with heightUniv θ (extendConst T g) at Lebesgue-almost every time of (0, T).

Equations

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

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

A.e.-time prefix height map on [0,T]: the a.e.-time prefix height version of g when one exists (it is then unique), 0 otherwise.

Equations

• BGW.StableTrees.heightPrefixAE θ T g = if h : ∃ (c : C(↑(Set.Icc 0 ↑T), ℝ)), BGW.StableTrees.IsPrefixHeightVersion θ T g c then Classical.choose h else 0

theorem BGW.StableTrees.IsExcursionHeightVersion.unique {θ : ℝ} {e : Excursion} {g h : C(NNReal, ℝ)} (hg : IsExcursionHeightVersion θ e g) (hh : IsExcursionHeightVersion θ e h) : g = h

A.e.-age versions of one excursion coincide.

theorem BGW.StableTrees.excursionHeight_eq_of_isExcursionHeightVersion (θ : ℝ) (e : Excursion) (g : C(NNReal, ℝ)) (hg : IsExcursionHeightVersion θ e g) : excursionHeight θ e = g

Deterministic characterization: an a.e.-age height version is the excursion height.

theorem BGW.StableTrees.isExcursionHeightVersion_excursionHeight (θ : ℝ) (e : Excursion) (h : ∃ (g : C(NNReal, ℝ)), IsExcursionHeightVersion θ e g) : IsExcursionHeightVersion θ e (excursionHeight θ e)

On the non-junk branch the excursion height is itself a version.

theorem BGW.StableTrees.excursionHeight_zero (θ : ℝ) (e : Excursion) : (excursionHeight θ e) 0 = 0

The excursion height starts at 0, for every excursion.

theorem BGW.StableTrees.excursionHeight_eq_zero_of_lifetime_le (θ : ℝ) (e : Excursion) {t : NNReal} (ht : e.lifetime ≤ t) : (excursionHeight θ e) t = 0

The excursion height vanishes at and after the lifetime, for every excursion.

theorem BGW.StableTrees.IsExcursionHeightVersion.nonneg {θ : ℝ} {e : Excursion} {g : C(NNReal, ℝ)} (hg : IsExcursionHeightVersion θ e g) (t : NNReal) : 0 ≤ g t

Every a.e.-age version is nonnegative, by uniqueness applied to its positive part.

theorem BGW.StableTrees.excursionHeight_nonneg (θ : ℝ) (e : Excursion) (t : NNReal) : 0 ≤ (excursionHeight θ e) t

The excursion height is nonnegative, for every excursion.

theorem BGW.StableTrees.IsPrefixHeightVersion.unique {θ : ℝ} {T : NNReal} {g : Skorokhod.D ↑T ℝ} {c d : C(↑(Set.Icc 0 ↑T), ℝ)} (hc : IsPrefixHeightVersion θ T g c) (hd : IsPrefixHeightVersion θ T g d) : c = d

A.e.-time versions on a compact horizon coincide, including at horizon zero.

theorem BGW.StableTrees.heightPrefixAE_eq_of_isPrefixHeightVersion (θ : ℝ) (T : NNReal) (g : Skorokhod.D ↑T ℝ) (c : C(↑(Set.Icc 0 ↑T), ℝ)) (hc : IsPrefixHeightVersion θ T g c) : heightPrefixAE θ T g = c

Deterministic characterization of the prefix map: an a.e.-time prefix height version is the value of heightPrefixAE.

theorem BGW.StableTrees.heightPrefixAE_excursionRestrict_of_exists (θ : ℝ) (e : Excursion) (he : ∃ (g : C(NNReal, ℝ)), IsExcursionHeightVersion θ e g) {a : NNReal} (ha : a < e.lifetime) (t : ↑(Set.Icc 0 ↑a)) : (heightPrefixAE θ a (excursionRestrict a e)) t = (excursionHeight θ e) ⟨↑t, ⋯⟩

Deterministic graph identity: on the non-junk branch, for every horizon a < ζ(e), the prefix map applied to the restricted excursion is the excursion height on [0,a].