Simultaneous positive heights of host excursion marks

The compact interior support bound keeps a generalized minimum strictly above the root. The minimum is ancestral to every sufficiently close later horizon.

theorem BGW.StableTrees.heightWindowInf_cut {g d : NNReal} {f : Skorokhod.DLoc} (hc : cutValid g d f) {a b : NNReal} (hab : a ≤ b) (hbd : b ≤ d - g) : heightWindowInf (g + a) (g + b) f = excursionWindowInf a b (excursionCut g d f) + ↑f g

Compact window infima commute with a valid excursion cut.

theorem BGW.StableTrees.heightLoc_pos_of_window (θ : ℝ) (f : Skorokhod.DLoc) (hf : ∀ (r : NNReal), Function.leftLim (↑f) r ≤ ↑f r) (hzero : ∀ (t s : NNReal), 0 < s → s < t → Function.leftLim (↑f) s ≤ futureInf f t s → height θ f s = 0 → futureInf f t s = futureInf f t 0) (hclock : ∀ (q : ℚ), 0 < ↑q → ∀ s ≤ (↑q).toNNReal, Function.leftLim (↑f) s ≤ futureInf f (↑q).toNNReal s → 0 ≤ height θ f s ∧ height θ f s = height θ f (↑q).toNNReal - supLocalTime θ (reversedAt (↑q).toNNReal f) ((↑q).toNNReal - s)) (hmod : ∀ (q : ℚ), heightLoc θ f (↑q).toNNReal = height θ f (↑q).toNNReal) {g a t : NNReal} (hga : g < a) (hat : a ≤ t) (hmin : ↑f g < heightWindowInf a t f) (hval : ↑f a < ↑f t) : 0 < heightLoc θ f t

A compact minimum above a previous level forces a positive continuous height.

theorem BGW.StableTrees.ae_jumpExcursion_height_pos {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ x ∈ passageJumpSet f, ∀ (t : NNReal), 0 < t → t < (jumpExcursion x f).lifetime → 0 < (excursionHeight θ (jumpExcursion x f)) t

Every host jump mark has strictly positive continuous height at every interior age.