Lifetime and normalized shape form a product under the excursion measure #
References #
- L. Chaumont, Excursion normalisée, méandre et pont pour les processus de Lévy stables, Bull. Sci. Math. 121 (1997), 377–403.
theorem
BGW.StableTrees.normalize_tail_independent_of_threshold
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
(a : ℝ)
(ha : 0 < a)
:
((excursionMeasure θ) {e : Excursion | a < ↑e.lifetime})⁻¹ • MeasureTheory.Measure.map (normalizeExc θ) (excursionTail θ a) = ↑(unitExcursionLaw θ)
Threshold independence: for every a > 0, the normalized restriction of N to
{ζ > a}, pushed by normalizeExc, is the unit law.
theorem
BGW.StableTrees.shapeLifetime_map_of_scaling
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
(ν : MeasureTheory.Measure Excursion)
(hν : ∀ (c : ↑(Set.Ioi 0)), MeasureTheory.Measure.map (excursionScale θ c) ν = ENNReal.ofReal (↑c ^ (1 / θ)) • ν)
(hfin : ν {e : Excursion | 1 < ↑e.lifetime} < ⊤)
:
MeasureTheory.Measure.map (shapeLifetime θ) ν = ENNReal.ofReal (Real.Gamma (1 - 1 / θ)) • (lifetimeLaw θ).prod (MeasureTheory.Measure.map (normalizeExc θ) (ν.restrict {e : Excursion | 1 < ↑e.lifetime}))
Uniqueness of scaling-consistent families: a measure ν with
(S_c)_* ν = c^{1/θ} • ν for all c > 0 and ν {ζ > 1} < ∞ is determined by its unit shape
measure (normalizeExc)_* (ν ↾ {ζ > 1}): (ζ, normalizeExc)_* ν = Γ(1-1/θ) • lifetimeLaw ⊗ (normalizeExc)_* (ν ↾ {ζ > 1}).
theorem
BGW.StableTrees.shapeLifetime_map_excursionMeasure
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
:
MeasureTheory.Measure.map (shapeLifetime θ) (excursionMeasure θ) = (lifetimeLaw θ).prod ↑(unitExcursionLaw θ)
Joint identity: (ζ, normalizeExc)_* N = lifetimeLaw ⊗ unitExcursionLaw.
theorem
BGW.StableTrees.shapeLifetime_map_excursionTail
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
(a : ℝ)
(ha : 0 < a)
:
MeasureTheory.Measure.map (shapeLifetime θ) (excursionTail θ a) = ((lifetimeLaw θ).restrict {u : ↑(Set.Ioi 0) | a < ↑u}).prod ↑(unitExcursionLaw θ)
Joint identity on tail rectangles: for a > 0,
(ζ, normalizeExc)_* (N ↾ {ζ > a}) = (lifetime law ↾ {u > a}) ⊗ unitExcursionLaw.
theorem
BGW.StableTrees.excursionMeasure_unique_of_scaling
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
(ν : MeasureTheory.Measure Excursion)
(hν : ∀ (c : ↑(Set.Ioi 0)), MeasureTheory.Measure.map (excursionScale θ c) ν = ENNReal.ofReal (↑c ^ (1 / θ)) • ν)
(hfin : ν {e : Excursion | 1 < ↑e.lifetime} < ⊤)
(hshape :
MeasureTheory.Measure.map (normalizeExc θ) (ν.restrict {e : Excursion | 1 < ↑e.lifetime}) = MeasureTheory.Measure.map (normalizeExc θ) (excursionTail θ 1))
:
Characterization of N: a scaling-consistent ν with ν {ζ > 1} < ∞ and the same
unit shape measure as N equals N.