Fixed-time exploration support

The ladder-height transform excludes zero increments, yielding strict increase in level. Transport on countable dense prefix times and ancestral concentration identify gap-free exploration support with top equal to the height.

theorem BGW.StableTrees.ae_supLadderHeight_increment_pos {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {y z : NNReal} (hyz : y < z) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), supLadderHeight θ y f < supLadderHeight θ z f

Ladder height increments over a positive deterministic level interval are positive.

theorem BGW.StableTrees.ae_strictMono_supLadderHeight {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), StrictMono fun (z : NNReal) => supLadderHeight θ z f

The ascending ladder height is strictly increasing on all levels on one event.

theorem BGW.StableTrees.ae_supRunning_strict_of_clock_lt {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (s t : NNReal), supLocalTime θ f s < supLocalTime θ f t → supRunning f s < supRunning f t

Any increase of the supremum clock forces an increase of the running supremum.

theorem BGW.StableTrees.ae_reversed_clock_strict_countable {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {T : NNReal} (hT : 0 < T) (D : Set ↑(Set.Iic T)) (hD : D.Countable) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (u v : ↑D), supLocalTime θ (reversedAt T f) ↑↑u < supLocalTime θ (reversedAt T f) ↑↑v → supRunning (reversedAt T f) ↑↑u < supRunning (reversedAt T f) ↑↑v

Strict clock-to-supremum growth transports on any countable family of prefix times.

theorem BGW.StableTrees.ae_support_gapfree_fixed {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (h : NNReal), ↑h < height θ f t → ∀ (ε : ℝ), 0 < ε → 0 < (exploration θ f t) (Metric.ball h ε)

No gaps, fixed-time version (∀ t outside the a.e. binder; kept for reference).

theorem BGW.StableTrees.support_le_of_mass_above_zero {ρ : MeasureTheory.Measure NNReal} {R : NNReal} (hρ : ρ (Set.Ioi R) = 0) {h : NNReal} (hh : ∀ (ε : ℝ), 0 < ε → 0 < ρ (Metric.ball h ε)) : h ≤ R

A point of the support lies below any bound beyond which the measure has no mass.

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

Support reaches the height, fixed t: a.s. the top of the support of ρ_t is H_t.