Ancestral concentration of the exploration measure

The Stieltjes measure is carried by ancestral times: outside that set the future infimum is locally constant. The fixed-horizon clock identity then bounds the heights seen by that measure. Fixed-time positivity also identifies the zero-height event.

theorem BGW.StableTrees.ae_exploration_ancestral_times (f : Skorokhod.DLoc) (hf : ∀ (r : NNReal), Function.leftLim (↑f) r ≤ ↑f r) (t : NNReal) : ∀ᵐ (s : ℝ) ∂(explorationStieltjes f t).measure.restrict (Set.Ioc 0 ↑t), Function.leftLim (↑f) s.toNNReal ≤ futureInf f t s.toNNReal

The exploration Stieltjes measure is carried by ancestral times, including endpoint atoms.

theorem BGW.StableTrees.ae_exploration_height_bounds {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ᵐ (s : ℝ) ∂(explorationStieltjes f t).measure.restrict (Set.Ioc 0 ↑t), 0 ≤ height θ f s.toNNReal ∧ height θ f s.toNNReal ≤ height θ f t ∧ heightRaw θ f s.toNNReal = ENNReal.ofReal (height θ f s.toNNReal)

At a fixed horizon, the Stieltjes measure sees finite ancestral heights below the endpoint.

theorem BGW.StableTrees.ae_exploration_above_height {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), (exploration θ f t) (Set.Ioi (height θ f t).toNNReal) = 0

Upper support bound (fixed t): a.s. ρ_t puts no mass above H_t (excludes the unbounded-support junk of topHeight).

theorem BGW.StableTrees.ae_height_pos_fixed {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), 0 < height θ f t

At each fixed positive time, the height is almost surely positive.

theorem BGW.StableTrees.futureInf_zero_eq_runningInf (f : Skorokhod.DLoc) (t : NNReal) : futureInf f t 0 = runningInfLoc f t

The future infimum from zero is the existing running infimum.

theorem BGW.StableTrees.ae_height_zero_iff {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), height θ f t = 0 ↔ ↑f t = futureInf f t 0

Height zero iff reflected zero (fixed t only): a.s. H_t = 0 ↔ X_t = I_t, i.e. ρ_t = 0. The all-t version needs ancestral local-time regularity (H03).