Identification at every positive real age

A surviving-age window supplies a good deterministic age. Dilation of its finite survival measure transports the full-filter approximation limit to each prescribed positive age.

theorem BGW.StableTrees.measurable_excursion_heightApprox (ε : ℝ) (t : NNReal) : Measurable fun (e : Excursion) => heightApprox ε e.path t

Fixed-age excursion occupation approximations are measurable.

theorem BGW.StableTrees.exists_age_heightApprox_tendstoInMeasure_excursionHeight {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∃ (t : NNReal), 0 < t ∧ MeasureTheory.TendstoInMeasure ((excursionMeasure θ).restrict {e : Excursion | t < e.lifetime}) (fun (ε : ℝ) (e : Excursion) => heightApprox ε e.path t) (nhdsWithin 0 (Set.Ioi 0)) fun (e : Excursion) => (excursionHeight θ e) t

At least one deterministic positive age identifies the continuous excursion height.

theorem BGW.StableTrees.map_excursionScale_survival {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (c : ↑(Set.Ioi 0)) (t : NNReal) : MeasureTheory.Measure.map (excursionScale θ c) ((excursionMeasure θ).restrict {e : Excursion | t < e.lifetime}) = ENNReal.ofReal (↑c ^ (1 / θ)) • (excursionMeasure θ).restrict {e : Excursion | (↑c).toNNReal * t < e.lifetime}

Scaling carries a survival restriction to the scaled restriction, with the usual mass factor.

theorem BGW.StableTrees.heightApprox_tendstoInMeasure_excursionHeight_dilate {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (c : ↑(Set.Ioi 0)) (t : NNReal) (ht : 0 < t) (hgood : MeasureTheory.TendstoInMeasure ((excursionMeasure θ).restrict {e : Excursion | t < e.lifetime}) (fun (ε : ℝ) (e : Excursion) => heightApprox ε e.path t) (nhdsWithin 0 (Set.Ioi 0)) fun (e : Excursion) => (excursionHeight θ e) t) : MeasureTheory.TendstoInMeasure ((excursionMeasure θ).restrict {e : Excursion | (↑c).toNNReal * t < e.lifetime}) (fun (ε : ℝ) (e : Excursion) => heightApprox ε e.path ((↑c).toNNReal * t)) (nhdsWithin 0 (Set.Ioi 0)) fun (e : Excursion) => (excursionHeight θ e) ((↑c).toNNReal * t)

Good ages for full-filter continuous-height identification are preserved by dilation.

theorem BGW.StableTrees.heightApprox_tendstoInMeasure_excursionHeight {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) (ht : 0 < t) : MeasureTheory.TendstoInMeasure ((excursionMeasure θ).restrict {e : Excursion | t < e.lifetime}) (fun (ε : ℝ) (e : Excursion) => heightApprox ε e.path t) (nhdsWithin 0 (Set.Ioi 0)) fun (e : Excursion) => (excursionHeight θ e) t

Identification under N: for each fixed age t > 0, on {t < ζ} the approximations converge in N-measure to the excursion height.