Prefix densities at almost every lifetime #
The remaining-lifetime identity and Kendall's density give the prefix/lifetime joint integral. Comparing it with the lifetime mixture proves the density identity for each fixed nonnegative measurable prefix test.
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.prefix_lifetime_lintegral
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
(a : NNReal)
(ha : 0 < a)
(F : Skorokhod.D ↑a ℝ → ENNReal)
(hF : Measurable F)
(g : ℝ → ENNReal)
(hg : Measurable g)
:
∫⁻ (e : Excursion) in {e : Excursion | ↑a < ↑e.lifetime}, F (excursionRestrict a e) * g ↑e.lifetime ∂excursionMeasure θ = ∫⁻ (u : ℝ) in Set.Ioi ↑a, g u * ∫⁻ (e : Excursion) in {e : Excursion | ↑a < ↑e.lifetime}, F (excursionRestrict a e) * ENNReal.ofReal (qKernel θ (u - ↑a) (↑e.path a)) ∂excursionMeasure θ
The remaining-lifetime law expressed as a density in the full lifetime.
theorem
BGW.StableTrees.prefix_density_ae_lifetime
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
(a : NNReal)
(ha : 0 < a)
(F : Skorokhod.D ↑a ℝ → ENNReal)
(hF : Measurable F)
:
∀ᵐ (u : ↑(Set.Ioi 0)) ∂volIoi.restrict {u : ↑(Set.Ioi 0) | ↑a < ↑u}, lifetimeDensity θ ↑u * ∫⁻ (e : Excursion), F (excursionRestrict a e) ∂excursionAt θ u = ∫⁻ (e : Excursion) in {e : Excursion | ↑a < ↑e.lifetime}, F (excursionRestrict a e) * ENNReal.ofReal (qKernel θ (↑u - ↑a) (↑e.path a)) ∂excursionMeasure θ
The density identity for each fixed nonnegative measurable prefix test.