Finite measures on surviving excursion age windows

The product of Lebesgue measure and the excursion measure is restricted to survival. Its mass is finite because the lifetime tail has exponent -1 / θ > -1 at zero.

noncomputable def BGW.StableTrees.heightExcursionAgeMeasure (θ : ℝ) (S : NNReal) : MeasureTheory.Measure (ℝ × Excursion)

The surviving excursion age window, with the survival restriction on the product measure.

Equations

• One or more equations did not get rendered due to their size.

theorem BGW.StableTrees.measurableSet_heightExcursionAge_survival : MeasurableSet {p : ℝ × Excursion | p.1.toNNReal < p.2.lifetime}

Joint measurability of the survival event.

theorem BGW.StableTrees.lintegral_excursion_lifetime_tail_lt_top {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (S : NNReal) : ∫⁻ (s : ℝ) in Set.Ioo 0 ↑S, (excursionMeasure θ) {e : Excursion | s.toNNReal < e.lifetime} < ⊤

The lifetime tail is integrable on each bounded interval starting at zero.

theorem BGW.StableTrees.isFiniteMeasure_heightExcursionAgeMeasure {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (S : NNReal) : MeasureTheory.IsFiniteMeasure (heightExcursionAgeMeasure θ S)

Survival-restricted product age windows have finite mass.