Interior ancestors and positive continuous heights

A compact window minimum supplies an ancestor. A strict gap above the root excludes zero ancestral height. The reversed clock bounds nearby rational-horizon heights from below.

noncomputable def BGW.StableTrees.heightWindowInf (a b : NNReal) (f : Skorokhod.DLoc) : ℝ

The infimum of a local path on a compact window.

Equations

• BGW.StableTrees.heightWindowInf a b f = (⨅ (s : ↑(Set.Icc 0 ↑(b - a))), (BGW.Skorokhod.DLoc.restrict (b - a) (BGW.Skorokhod.DLoc.shift a f)) s) + ↑f a

theorem BGW.StableTrees.heightWindowInf_le_eval (f : Skorokhod.DLoc) {a b v : NNReal} (hav : a ≤ v) (hvb : v ≤ b) : heightWindowInf a b f ≤ ↑f v

A compact window infimum bounds each value in the window.

theorem BGW.StableTrees.exists_heightWindow_ancestor (f : Skorokhod.DLoc) (hf : ∀ (r : NNReal), Function.leftLim (↑f) r ≤ ↑f r) {a b : NNReal} (hab : a ≤ b) : ∃ (s : NNReal), a ≤ s ∧ s ≤ b ∧ Function.leftLim (↑f) s ≤ heightWindowInf a b f

A generalized minimum gives an ancestral contact in a compact window.

theorem BGW.StableTrees.heightLoc_pos_of_ancestor_window (θ : ℝ) (f : Skorokhod.DLoc) (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) {s t b : NNReal} (hs : 0 < s) (hst : s ≤ t) (htb : t < b) (ha : ∀ r ∈ Set.Ioo t b, Function.leftLim (↑f) s ≤ futureInf f r s ∧ futureInf f r 0 < futureInf f r s) : 0 < heightLoc θ f t

The rational clock formulas exclude a zero continuous height above a positive ancestor.