Path and integral mixtures over every positive lifetime #
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.map_fromShapeLifetime_product
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
:
MeasureTheory.Measure.map (fromShapeLifetime θ) ((lifetimeLaw θ).prod ↑(unitExcursionLaw θ)) = excursionMeasure θ
Reconstructing the lifetime/shape product recovers the excursion measure.
theorem
BGW.StableTrees.lintegral_excursionMeasure_eq_mixture
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
{F : Excursion → ENNReal}
(hF : Measurable F)
:
Nonnegative mixture: ∫⁻ F dN = ∫⁻ u>0, (∫⁻ F dN_{(u)}) · density(u) du for measurable
F : Excursion → ℝ≥0∞.
theorem
BGW.StableTrees.excursionMeasure_eq_lifetime_mixture
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
{A : Set Excursion}
(hA : MeasurableSet A)
:
Path-only mixture: for measurable A,
N(A) = ∫⁻ u>0, (S_u)_* unitExcursionLaw (A) · (1/θ)/Γ(1-1/θ) u^{-1-1/θ} du.
theorem
BGW.StableTrees.setLIntegral_excursionMeasure_eq_mixture
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
{F : Excursion → ENNReal}
(hF : Measurable F)
(a : ℝ)
(ha : 0 ≤ a)
:
Restricted nonnegative mixture over long excursions {ζ > a}, a ≥ 0.
theorem
BGW.StableTrees.tailExcursionLaw_eq_mixture
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
{A : Set Excursion}
(hA : MeasurableSet A)
:
Mixture for the tail law: under N(· | ζ > 1) the lifetime has density
α u^{-1-α} on u > 1; for measurable A ⊆ Excursion.
theorem
BGW.StableTrees.tailLevyExcLaw_eq_mixture
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
(T : NNReal)
(hT : 0 < T)
{B : Set (Skorokhod.D ↑T ℝ)}
(hB : MeasurableSet B)
:
Tail path mixture (C28), every horizon T > 0 (zero continuation after u is built into
excursionRestrict): for measurable B ⊆ D T ℝ.