Unit excursion prefix density and absence of fixed jumps #
The prefix law at every interior horizon is the normalized Kendall-weighted excursion survival measure. In particular the unit law has no fixed jumps.
Main results #
unitPrefix: the law of the prefix of the unit excursion up to an interior time.levyExcLaw_prefix_density:unitPrefix θ ais the normalized Kendall-weighted excursion survival measure, pushed forward by the restriction to[0, a].lintegral_unitPrefix_eq: integral form of the prefix density for nonnegative measurable tests.levyExcLaw_noFixedJump: the unit law has no fixed jump at an interior time.exists_goodTimes_unit: a countable dense set of times without fixed jumps.prefix_density_ae_lifetime: the prefix density identity at almost every lifetime for a fixed nonnegative measurable 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.
T. Duquesne, Path decompositions for real Lévy processes, Ann. Inst. H. Poincaré Probab. Statist. 39 (2003), 339–370.
theorem
BGW.StableTrees.levyExcLaw_noFixedJump
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
(t : NNReal)
(ht : t ∈ Set.Ioo 0 1)
:
NoFixedJumpUnit θ t
The unit law has no jump at each deterministic interior time.
theorem
BGW.StableTrees.lintegral_prefix_density_mass
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
(a : NNReal)
(ha : a ∈ Set.Ioo 0 1)
:
∫⁻ (e : Excursion) in {e : Excursion | ↑a < ↑e.lifetime}, ENNReal.ofReal (qKernel θ (1 - ↑a) (↑e.path a)) ∂excursionMeasure θ = ENNReal.ofReal (Scalar.stableDensity θ 0)
The density side has mass equal to the stable density at zero.
theorem
BGW.StableTrees.levyExcLaw_prefix_density
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
(a : NNReal)
(ha : a ∈ Set.Ioo 0 1)
:
unitPrefix θ a = (ENNReal.ofReal (Scalar.stableDensity θ 0))⁻¹ • MeasureTheory.Measure.map (excursionRestrict a)
((excursionTail θ ↑a).withDensity fun (e : Excursion) => ENNReal.ofReal (qKernel θ (1 - ↑a) (↑e.path a)))
The law of a unit-excursion prefix is the normalized Kendall-weighted survival measure.
theorem
BGW.StableTrees.lintegral_unitPrefix_eq
{θ : ℝ}
(hθ : 1 < θ ∧ θ ≤ 2)
(a : NNReal)
(ha : a ∈ Set.Ioo 0 1)
(F : Skorokhod.D ↑a ℝ → ENNReal)
(hF : Measurable F)
:
∫⁻ (x : Skorokhod.D ↑a ℝ), F x ∂unitPrefix θ a = (ENNReal.ofReal (Scalar.stableDensity θ 0))⁻¹ * ∫⁻ (e : Excursion) in {e : Excursion | ↑a < ↑e.lifetime}, F (excursionRestrict a e) * ENNReal.ofReal (qKernel θ (1 - ↑a) (↑e.path a)) ∂excursionMeasure θ
Integral form of the prefix density for nonnegative measurable tests.