Reversed clocks and ancestral windows

Measurable compact occupation functions transport uniform convergence to reversed prefixes. At every ancestral time of a fixed horizon, contact restart identifies the earlier height as the difference of two values of that clock. Endpoint jumps are retained explicitly.

theorem BGW.StableTrees.ae_reversed_clock_prefix {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {T : NNReal} (hT : 0 < T) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), (∀ u ≤ T, Filter.Tendsto (fun (k : ℕ) => supOccupation (supEps θ k) (reversedAt T f) u) Filter.atTop (nhds (supLocalTime θ (reversedAt T f) u))) ∧ (Continuous fun (u : ↑(Set.Iic T)) => supLocalTime θ (reversedAt T f) ↑u) ∧ (Monotone fun (u : ↑(Set.Iic T)) => supLocalTime θ (reversedAt T f) ↑u) ∧ supLocalTime θ (reversedAt T f) 0 = 0

The public occupation sequence has a continuous monotone clock on a reversed prefix.

theorem BGW.StableTrees.supRunning_reversedAt_window_left (f : Skorokhod.DLoc) {t s : NNReal} (hst : s ≤ t) (hf : ∀ (r : NNReal), Function.leftLim (↑f) r ≤ ↑f r) : supRunning (reversedAt t f) (t - s) = ↑f t - min (Function.leftLim (↑f) s) (futureInf f t s)

The reversed window supremum includes the original left-endpoint jump.

theorem BGW.StableTrees.supReflected_reversedAt_eq_zero_of_ancestor (f : Skorokhod.DLoc) {t s : NNReal} (hst : s ≤ t) (hf : ∀ (r : NNReal), Function.leftLim (↑f) r ≤ ↑f r) (hs : Function.leftLim (↑f) s ≤ futureInf f t s) : supReflected (reversedAt t f) (t - s) = 0

An ancestral time is a supremum contact in the reversed path.

theorem BGW.StableTrees.supOccupation_prefix_add_const {g h : Skorokhod.DLoc} {T : NNReal} {c : ℝ} (hp : ∀ u ≤ T, ↑g u = ↑h u + c) (ε : ℝ) : supOccupation ε g T = supOccupation ε h T

A constant spatial translation of a prefix preserves its occupation.

theorem BGW.StableTrees.supOccupation_reversedAt_shift (f : Skorokhod.DLoc) {t s : NNReal} (hst : s ≤ t) (ε : ℝ) : supOccupation ε (reversedAt s f) s = supOccupation ε (Skorokhod.DLoc.shift (t - s) (reversedAt t f)) s

Reversing at an earlier horizon is a translated prefix of the shifted reversal.

theorem BGW.StableTrees.height_ancestor_clock_identity (θ : ℝ) (f : Skorokhod.DLoc) {t s : NNReal} (hst : s ≤ t) (hf : ∀ (r : NNReal), Function.leftLim (↑f) r ≤ ↑f r) (hg0 : ↑(reversedAt t f) 0 = 0) (hs : Function.leftLim (↑f) s ≤ futureInf f t s) (hp : ∀ u ≤ t, Filter.Tendsto (fun (k : ℕ) => supOccupation (supEps θ k) (reversedAt t f) u) Filter.atTop (nhds (supLocalTime θ (reversedAt t f) u))) : Filter.Tendsto (fun (k : ℕ) => heightApprox (supEps θ k) f s) Filter.atTop (nhds (height θ f s)) ∧ height θ f s = supLocalTime θ (reversedAt t f) t - supLocalTime θ (reversedAt t f) (t - s)

At every ancestral time, a convergent reversed clock identifies the earlier height.

theorem BGW.StableTrees.ae_height_ancestor_fixed {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ s ≤ t, Function.leftLim (↑f) s ≤ futureInf f t s → Filter.Tendsto (fun (k : ℕ) => heightApprox (supEps θ k) f s) Filter.atTop (nhds (height θ f s)) ∧ 0 ≤ height θ f s ∧ heightRaw θ f s = ENNReal.ofReal (height θ f s) ∧ height θ f s = supLocalTime θ (reversedAt t f) t - supLocalTime θ (reversedAt t f) (t - s)

For a fixed horizon, all its ancestral times have finite identified height on one event.