Transferring absence of fixed jumps through prefix densities

Restriction preserves the left limit at each positive prefix time. Absolute continuity of the weighted excursion measure transfers the fixed-time property.

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.leftLim_excursionRestrict (a t : NNReal) (ht : 0 < t) (hta : t ≤ a) (e : Excursion) : Function.leftLim ⇑(excursionRestrict a e) ⟨↑t, ⋯⟩ = Function.leftLim (↑e.path) t

Restricting an excursion preserves its left limit at positive prefix times.

theorem BGW.StableTrees.noFixedJumpUnit_of_prefix_density {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (b t : NNReal) (ht : 0 < t) (htb : t ≤ b) (hd : unitPrefix θ b = (ENNReal.ofReal (Scalar.stableDensity θ 0))⁻¹ • MeasureTheory.Measure.map (excursionRestrict b) (prefixDensityMeasure θ b)) : NoFixedJumpUnit θ t

A prefix density transfers absence of fixed jumps from the excursion measure.