Window intensities of the excursion process, including mark sets of infinite intensity.

See Bertoin, Lévy Processes, Chapter IV.

noncomputable def BGW.StableTrees.lebNN : MeasureTheory.Measure NNReal

Lebesgue measure on ℝ≥0 (flagged: Mathlib has no MeasureSpace ℝ≥0; this is the pullback of volume on ℝ under the coercion, so lebNN (Ioc a b) = b - a).

Equations

• BGW.StableTrees.lebNN = MeasureTheory.Measure.comap NNReal.toReal MeasureTheory.volume

theorem BGW.StableTrees.lebNN_Ioc (a b : NNReal) : lebNN (Set.Ioc a b) = ↑(b - a)

Lebesgue measure of an interval.

def BGW.StableTrees.excursionLifetimeSlab (n : ℕ) : Set Excursion

The increasing lifetime exhaustion used to extend finite-rate formulas.

Equations

• BGW.StableTrees.excursionLifetimeSlab n = {e : BGW.StableTrees.Excursion | 1 / (↑n + 1) < e.lifetime}

theorem BGW.StableTrees.measurableSet_excursionLifetimeSlab (n : ℕ) : MeasurableSet (excursionLifetimeSlab n)

Lifetime slabs are measurable.

theorem BGW.StableTrees.monotone_excursionLifetimeSlab : Monotone excursionLifetimeSlab

Lifetime slabs increase with their index.

theorem BGW.StableTrees.iUnion_excursionLifetimeSlab : ⋃ (n : ℕ), excursionLifetimeSlab n = Set.univ

Every excursion belongs to a lifetime slab.

theorem BGW.StableTrees.lintegral_windowMark_eq {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {ξ : Skorokhod.DLoc → MeasureTheory.Measure (NNReal × Excursion)} (hξ : Measurable ξ) (hae : ξ =ᵐ[↑(stableLocalLaw θ)] excursionPointMeasure) {a b : NNReal} (hab : a ≤ b) {A : Set Excursion} (hA : MeasurableSet A) : ∫⁻ (f : Skorokhod.DLoc), (ξ f) (Set.Ioc a b ×ˢ A) ∂↑(stableLocalLaw θ) = ↑(b - a) * (excursionMeasure θ) A

Mean measure of windows: for a measurable modification ξ, a ≤ b and measurable A (finite or infinite rate), E ξ((a,b] × A) = (b - a) N(A).