Unit height scaling

Continuity reduces the all-age scaling equality to countably many rational evaluations, so the scaling events are jointly measurable. Fubini then supplies the version with a Lebesgue distributed positive scale. The raw fixed-scale identity and the unit continuous version determine a version of the scaled excursion, and the jointly measurable equality event gives the product formulation.

theorem BGW.StableTrees.measurableSet_excursionHeight_scale (θ : ℝ) : MeasurableSet {p : ↑(Set.Ioi 0) × Excursion | ∀ (t : NNReal), (excursionHeight θ (excursionScale θ p.1 p.2)) ((↑p.1).toNNReal * t) = ↑p.1 ^ (1 - 1 / θ) * (excursionHeight θ p.2) t}

The all-age scaling event is jointly Borel in the scale and excursion.

theorem BGW.StableTrees.ae_prod_excursionHeight_scale {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (p : ↑(Set.Ioi 0) × Excursion) ∂volIoi.prod (excursionMeasure θ), ∀ (t : NNReal), (excursionHeight θ (excursionScale θ p.1 p.2)) ((↑p.1).toNNReal * t) = ↑p.1 ^ (1 - 1 / θ) * (excursionHeight θ p.2) t

Scaling with a measurable parameter: (Lebesgue ⊗ N)-a.e. in (c, e).

theorem BGW.StableTrees.isExcursionHeightVersion_scale_of_ae (θ : ℝ) (c : ↑(Set.Ioi 0)) (e : Excursion) (g : C(NNReal, ℝ)) (hg : IsExcursionHeightVersion θ e g) (hr : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 ↑e.lifetime), heightUniv θ (excursionScale θ c e).path ((↑c).toNNReal * s.toNNReal) = ↑c ^ (1 - 1 / θ) * heightUniv θ e.path s.toNNReal) : IsExcursionHeightVersion θ (excursionScale θ c e) { toFun := fun (t : NNReal) => ↑c ^ (1 - 1 / θ) * g (t / (↑c).toNNReal), continuous_toFun := ⋯ }

Scaling a continuous version gives a version when the raw scaling identity holds a.e.

theorem BGW.StableTrees.ae_excursionHeight_scale_unit {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (c : ↑(Set.Ioi 0)) : ∀ᵐ (e : Excursion) ∂↑(unitExcursionLaw θ), ∀ (t : NNReal), (excursionHeight θ (excursionScale θ c e)) ((↑c).toNNReal * t) = ↑c ^ (1 - 1 / θ) * (excursionHeight θ e) t

Scaling under the unit law, for each fixed c > 0 (not implied by the N version: the unit law lives on the N-null set {ζ = 1}).

theorem BGW.StableTrees.ae_prod_excursionHeight_scale_unit {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (p : ↑(Set.Ioi 0) × Excursion) ∂volIoi.prod ↑(unitExcursionLaw θ), ∀ (t : NNReal), (excursionHeight θ (excursionScale θ p.1 p.2)) ((↑p.1).toNNReal * t) = ↑p.1 ^ (1 - 1 / θ) * (excursionHeight θ p.2) t

Scaling with a measurable parameter under the unit law: (Lebesgue ⊗ unit)-a.e. in (c, e) (a form J01's common-lifetime mixture can use).