Support of ancestral exploration measures

Future-infimum Stieltjes measures agree strictly before an ancestor. Clock order separates the earlier and later heights, transporting the fixed-horizon support bounds to every ancestor. Rational horizons give one event for ancestral support tops. The final window identity records the deterministic source truncation needed for exploration restart.

theorem BGW.StableTrees.futureInf_eq_before_ancestor (f : Skorokhod.DLoc) {u s q : NNReal} (hus : u < s) (hsq : s ≤ q) (ha : Function.leftLim (↑f) s ≤ futureInf f q s) : futureInf f q u = futureInf f s u

Before an ancestral time, the two future-infimum functions coincide.

theorem BGW.StableTrees.explorationStieltjes_restrict_before_ancestor (f : Skorokhod.DLoc) {s q : NNReal} (hs : 0 < s) (hsq : s ≤ q) (ha : Function.leftLim (↑f) s ≤ futureInf f q s) : (explorationStieltjes f s).measure.restrict (Set.Ioo 0 ↑s) = (explorationStieltjes f q).measure.restrict (Set.Ioo 0 ↑s)

The exploration source before an ancestor does not depend on the later horizon.

theorem BGW.StableTrees.exploration_apply_before_ancestor (θ : ℝ) (f : Skorokhod.DLoc) {s q : NNReal} (hs : 0 < s) (hsq : s ≤ q) (ha : Function.leftLim (↑f) s ≤ futureInf f q s) {B : Set NNReal} (hB : MeasurableSet B) (hn : (height θ f s).toNNReal ∉ B) : (exploration θ f s) B = ((explorationStieltjes f q).measure.restrict (Set.Ioo 0 ↑s)) ((fun (x : ℝ) => (height θ f x.toNNReal).toNNReal) ⁻¹' B)

Away from its terminal height, an ancestral exploration uses the earlier source window.

theorem BGW.StableTrees.ae_exploration_support_ancestors_fixed {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : NNReal} (hq : 0 < q) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ s ≤ q, Function.leftLim (↑f) s ≤ futureInf f q s → (exploration θ f s) (Set.Ioi (height θ f s).toNNReal) = 0 ∧ ∀ (h : NNReal), ↑h < height θ f s → ∀ (ε : ℝ), 0 < ε → 0 < (exploration θ f s) (Metric.ball h ε)

At a fixed horizon, every ancestor has an upper support bound and no gaps below its height.

theorem BGW.StableTrees.topHeight_eq_of_support_bounds {ρ : MeasureTheory.Measure NNReal} {H : ℝ} (hfinite : 0 ≤ H) (habove : ρ (Set.Ioi H.toNNReal) = 0) (hgap : ∀ (h : NNReal), ↑h < H → ∀ (ε : ℝ), 0 < ε → 0 < ρ (Metric.ball h ε)) : ↑(topHeight ρ) = H

An upper support bound and positivity below a nonnegative level identify its support top.

theorem BGW.StableTrees.ae_topHeight_ancestral {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (t s : NNReal), s < t ∧ Function.leftLim (↑f) s ≤ futureInf f t s ∨ s = t ∧ Function.leftLim (↑f) t < ↑f t → ↑(topHeight (exploration θ f s)) = height θ f s

Ancestral top identification: a.s., for every t and ancestral s (same antecedent as ae_heightApprox_ancestral), the top of the support of ρ_s is H_s.

theorem BGW.StableTrees.futureInf_restart_window (f : Skorokhod.DLoc) (t r : NNReal) {s : NNReal} (hst : s ≤ t) : futureInf f (t + r) s = min (futureInf f t s) (↑f t + futureInf (Skorokhod.DLoc.shift t f) r 0)

Future infima across a deterministic restart split into the old and fresh windows.