Itô’s excursion family indexed by lifetime

The scaled unit laws have exact lifetimes and satisfy the stable scaling group law. Restricting the lifetime mixtures to measurable lifetime sets identifies a competing family almost everywhere; a countable generating algebra removes the exceptional lifetime, and scaling proves uniqueness at every positive lifetime.

theorem BGW.StableTrees.measure_lifetime_excursionAt {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (a : ↑(Set.Ioi 0)) : (excursionAt θ a) {e : Excursion | ↑e.lifetime = ↑a} = 1

C22, exact lifetime. For every a > 0, N_(a) assigns mass one to {ζ = a}.

theorem BGW.StableTrees.excursionAt_scaling (θ : ℝ) (c a : ↑(Set.Ioi 0)) : MeasureTheory.Measure.map (excursionScale θ c) (excursionAt θ a) = excursionAt θ ⟨↑c * ↑a, ⋯⟩

C22, scaling. (S^(λ))_* N_(a) = N_(λa) for every λ,a > 0.

theorem BGW.StableTrees.excursionAt_unique {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (ν : ↑(Set.Ioi 0) → MeasureTheory.Measure Excursion) (hprob : ∀ (a : ↑(Set.Ioi 0)), (ν a) Set.univ = 1) (hlife : ∀ (a : ↑(Set.Ioi 0)), (ν a) {e : Excursion | ↑e.lifetime = ↑a} = 1) (hscale : ∀ (c a : ↑(Set.Ioi 0)), MeasureTheory.Measure.map (excursionScale θ c) (ν a) = ν ⟨↑c * ↑a, ⋯⟩) (hmeas : ∀ (A : Set Excursion), MeasurableSet A → Measurable fun (a : ↑(Set.Ioi 0)) => (ν a) A) (hmix : ∀ (A : Set Excursion), MeasurableSet A → (excursionMeasure θ) A = ∫⁻ (a : ↑(Set.Ioi 0)), (ν a) A * lifetimeDensity θ ↑a ∂volIoi) (a : ↑(Set.Ioi 0)) : ν a = excursionAt θ a

C22, uniqueness of the Itô family. A measurable probability family with exact lifetime support, the stable scaling law and the lifetime mixture of N is excursionAt θ.