Rate and null marks for first long excursions

The lifetime intensity has no atoms. Localizing the mean measure to bounded label windows transfers this fact simultaneously to every passage jump of a stable path.

Reference: J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.

noncomputable def BGW.StableTrees.longRate (θ : ℝ) : ℝ

The rate r_θ = 1/Γ(1-1/θ) = N(ζ > 1) = θ p₀.

Equations

• BGW.StableTrees.longRate θ = 1 / Real.Gamma (1 - 1 / θ)

noncomputable def BGW.StableTrees.firstLongLabelLaw (θ : ℝ) : MeasureTheory.Measure NNReal

The exponential law of rate r_θ on ℝ≥0 (the law of the first long label).

Equations

• BGW.StableTrees.firstLongLabelLaw θ = MeasureTheory.Measure.map Real.toNNReal (ProbabilityTheory.expMeasure (BGW.StableTrees.longRate θ))

theorem BGW.StableTrees.excursionMeasure_longMarks {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : (excursionMeasure θ) {e : Excursion | 1 < ↑e.lifetime} = ENNReal.ofReal (longRate θ)

N(ζ > 1) = r_θ, from the sealed lifetime tail.

theorem BGW.StableTrees.excursionMeasure_lifetime_singleton {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (u : NNReal) : (excursionMeasure θ) {e : Excursion | e.lifetime = u} = 0

No lifetime is charged by N (unified with lifetime 0, excluded by the carrier).

theorem BGW.StableTrees.ae_jumpExcursion_not_mem_of_null {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {A : Set Excursion} (hA : MeasurableSet A) (hnull : (excursionMeasure θ) A = 0) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ x ∈ passageJumpSet f, jumpExcursion x f ∉ A

A measurable null mark set contains none of the passage-jump marks, almost surely.

theorem BGW.StableTrees.ae_jump_lifetime_ne {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (a : NNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ x ∈ passageJumpSet f, passageTime x f - passageTimeMinus x f ≠ a

A.s. no excursion mark has a prescribed lifetime a: the set of excursions of lifetime a is N-null, and N-null mark sets carry no jump mark (ae_jumpExcursion_not_mem_of_null).

theorem BGW.StableTrees.ae_continuousAt_tailExcursion_path {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (T : NNReal) (hT : 0 < T) : ∀ᵐ (e : Excursion) ∂↑(tailExcursionLaw θ), ContinuousAt (↑e.path) T

No fixed jump of the selected mark at a positive cutoff.