Normalized excursion laws and their lifetime-indexed scaling family

References

• L. Chaumont, Excursion normalisée, méandre et pont pour les processus de Lévy stables, Bull. Sci. Math. 121 (1997), 377–403.

Definitions

noncomputable def BGW.StableTrees.excursionTail (θ a : ℝ) : MeasureTheory.Measure Excursion

The tail N ↾ {ζ > a} of the excursion measure.

Equations

• BGW.StableTrees.excursionTail θ a = (BGW.StableTrees.excursionMeasure θ).restrict {e : BGW.StableTrees.Excursion | a < ↑e.lifetime}

noncomputable def BGW.StableTrees.unitExcursionMeasure (θ : ℝ) : MeasureTheory.Measure Excursion

Explicit normalized unit measure: Γ(1-1/θ) • (normalizeExc θ)_* (N ↾ {ζ > 1}). The coefficient is N(ζ > 1)⁻¹; this is a normalized restriction, not a conditioning on {ζ = 1}.

Equations

• BGW.StableTrees.unitExcursionMeasure θ = ENNReal.ofReal (Real.Gamma (1 - 1 / θ)) • MeasureTheory.Measure.map (BGW.StableTrees.normalizeExc θ) (BGW.StableTrees.excursionTail θ 1)

noncomputable def BGW.StableTrees.tailExcursionMeasure (θ : ℝ) : MeasureTheory.Measure Excursion

The tail law N(· | ζ > 1) = Γ(1-1/θ) • N ↾ {ζ > 1} as a plain measure.

Equations

• BGW.StableTrees.tailExcursionMeasure θ = ENNReal.ofReal (Real.Gamma (1 - 1 / θ)) • BGW.StableTrees.excursionTail θ 1

noncomputable def BGW.StableTrees.toProbOrJunk (μ : MeasureTheory.Measure Excursion) : MeasureTheory.ProbabilityMeasure Excursion

Probability-measure packaging with a junk dirac junkExcursion branch.

Equations

• BGW.StableTrees.toProbOrJunk μ = if h : MeasureTheory.IsProbabilityMeasure μ then ⟨μ, h⟩ else ⟨MeasureTheory.Measure.dirac BGW.StableTrees.junkExcursion, BGW.StableTrees.toProbOrJunk._proof_1⟩

noncomputable def BGW.StableTrees.unitExcursionLaw (θ : ℝ) : MeasureTheory.ProbabilityMeasure Excursion

Unit excursion law; agrees with unitExcursionMeasure for 1 < θ ≤ 2. Outside that range it is only a totalized probability measure.

Equations

• BGW.StableTrees.unitExcursionLaw θ = BGW.StableTrees.toProbOrJunk (BGW.StableTrees.unitExcursionMeasure θ)

noncomputable def BGW.StableTrees.tailExcursionLaw (θ : ℝ) : MeasureTheory.ProbabilityMeasure Excursion

Law of the excursion under N(· | ζ > 1); agrees with tailExcursionMeasure for 1 < θ ≤ 2. Outside that range it is only a totalized probability measure.

Equations

• BGW.StableTrees.tailExcursionLaw θ = BGW.StableTrees.toProbOrJunk (BGW.StableTrees.tailExcursionMeasure θ)

noncomputable def BGW.StableTrees.levyExcLaw (θ : ℝ) : MeasureTheory.ProbabilityMeasure (Skorokhod.D 1 ℝ)

Unit-lifetime excursion as a path on [0,1].

Equations

• BGW.StableTrees.levyExcLaw θ = (BGW.StableTrees.unitExcursionLaw θ).map (BGW.StableTrees.excursionRestrict 1)

noncomputable def BGW.StableTrees.tailLevyExcLaw (θ : ℝ) (T : NNReal) : MeasureTheory.ProbabilityMeasure (Skorokhod.D ↑T ℝ)

Whole excursion under N(· | ζ > 1), restricted to [0,T].

Equations

• BGW.StableTrees.tailLevyExcLaw θ T = (BGW.StableTrees.tailExcursionLaw θ).map (BGW.StableTrees.excursionRestrict T)

noncomputable def BGW.StableTrees.excursionAt (θ : ℝ) (u : ↑(Set.Ioi 0)) : MeasureTheory.Measure Excursion

The scaled unit excursion (S_u)_* unitExcursionLaw, u > 0: the measure N_{(u)} of excursions of lifetime u.

Equations

• BGW.StableTrees.excursionAt θ u = MeasureTheory.Measure.map (BGW.StableTrees.excursionScale θ u) ↑(BGW.StableTrees.unitExcursionLaw θ)

noncomputable def BGW.StableTrees.lifetimeDensity (θ u : ℝ) : ENNReal

The lifetime density (1/θ)/Γ(1-1/θ) · u^{-1-1/θ}.

Equations

• BGW.StableTrees.lifetimeDensity θ u = ENNReal.ofReal (1 / θ / Real.Gamma (1 - 1 / θ) * u ^ (-1 - 1 / θ))

theorem BGW.StableTrees.measurable_lifetimeDensity (θ : ℝ) : Measurable fun (u : ↑(Set.Ioi 0)) => lifetimeDensity θ ↑u

The excursion lifetime density is measurable on the positive half-line.

noncomputable def BGW.StableTrees.volIoi : MeasureTheory.Measure ↑(Set.Ioi 0)

Lebesgue measure on Set.Ioi 0 (comap of volume).

Equations

• BGW.StableTrees.volIoi = MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume

theorem BGW.StableTrees.sigmaFinite_volIoi : MeasureTheory.SigmaFinite volIoi

Lebesgue measure restricted to the positive half-line is sigma-finite.

noncomputable def BGW.StableTrees.lifetimeLaw (θ : ℝ) : MeasureTheory.Measure ↑(Set.Ioi 0)

The Lévy measure ζ_* N on Set.Ioi 0.

Equations

• BGW.StableTrees.lifetimeLaw θ = BGW.StableTrees.volIoi.withDensity fun (u : ↑(Set.Ioi 0)) => BGW.StableTrees.lifetimeDensity θ ↑u

theorem BGW.StableTrees.excursionMeasure_lifetime_gt_one {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : (excursionMeasure θ) {e : Excursion | 1 < ↑e.lifetime} = ENNReal.ofReal (1 / Real.Gamma (1 - 1 / θ))

Mass of the unit tail: N(ζ > 1) = 1/Γ(1-1/θ) = θ d_θ(0).

theorem BGW.StableTrees.excursionMeasure_lifetime_gt_one_eq_density {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : (excursionMeasure θ) {e : Excursion | 1 < ↑e.lifetime} = ENNReal.ofReal (θ * Scalar.stableDensity θ 0)

The same mass through the stable density at 0.

theorem BGW.StableTrees.isProbabilityMeasure_tailExcursionMeasure {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : MeasureTheory.IsProbabilityMeasure (tailExcursionMeasure θ)

The tail measure is a probability measure.

theorem BGW.StableTrees.isProbabilityMeasure_unitExcursionMeasure {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : MeasureTheory.IsProbabilityMeasure (unitExcursionMeasure θ)

The unnormalized unit measure is a probability measure.

theorem BGW.StableTrees.coe_unitExcursionLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ↑(unitExcursionLaw θ) = unitExcursionMeasure θ

Unfolding: the law is the explicit normalized restriction.

theorem BGW.StableTrees.coe_tailExcursionLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ↑(tailExcursionLaw θ) = tailExcursionMeasure θ

Unfolding for the tail law.

theorem BGW.StableTrees.ae_lifetime_unitExcursionLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (e : Excursion) ∂↑(unitExcursionLaw θ), e.lifetime = 1

Unit excursions have lifetime one almost surely (indeed surely on the support).

theorem BGW.StableTrees.isProbabilityMeasure_excursionAt (θ : ℝ) (u : ↑(Set.Ioi 0)) : MeasureTheory.IsProbabilityMeasure (excursionAt θ u)

Each excursionAt θ u is a probability measure (for every θ).

theorem BGW.StableTrees.measurable_excursionAt_apply (θ : ℝ) {A : Set Excursion} (hA : MeasurableSet A) : Measurable fun (u : ↑(Set.Ioi 0)) => (excursionAt θ u) A

Measurability of u ↦ N_{(u)}(A).

theorem BGW.StableTrees.ae_lifetime_excursionAt {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (u : ↑(Set.Ioi 0)) : ∀ᵐ (e : Excursion) ∂excursionAt θ u, ↑e.lifetime = ↑u

N_{(u)}-almost every excursion has lifetime u.

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

Exact scaling of the family at every lifetime: (S_c)_* N_{(u)} = N_{(cu)}.

theorem BGW.StableTrees.excursionAt_one (θ : ℝ) : excursionAt θ ⟨1, ⋯⟩ = ↑(unitExcursionLaw θ)

The family at lifetime one is the unit law.