Simultaneous interior positivity

Positivity on every compact interior rational window is a Borel event in the compact-open continuous-map space. Compensation transfers host positivity to the excursion measure; the shape/lifetime law and fixed-scale unit scaling transfer it to the unit law.

theorem BGW.StableTrees.measurableSet_excursionHeight_pos (θ : ℝ) : MeasurableSet {e : Excursion | ∀ (t : NNReal), 0 < t → t < e.lifetime → 0 < (excursionHeight θ e) t}

Strict positivity at every interior age is a Borel event of the excursion.

theorem BGW.StableTrees.ae_excursionHeight_pos {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (e : Excursion) ∂excursionMeasure θ, ∀ (t : NNReal), 0 < t → t < e.lifetime → 0 < (excursionHeight θ e) t

Positivity inside, simultaneously for all times of (0, ζ), under N.

theorem BGW.StableTrees.ae_excursionHeight_pos_unit {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (e : Excursion) ∂↑(unitExcursionLaw θ), ∀ (t : NNReal), 0 < t → t < e.lifetime → 0 < (excursionHeight θ e) t

Positivity inside, simultaneously for all times of (0, ζ), under the unit law.