The Itô excursion measure, defined as the mean mark measure on a unit time window. Its definition is independent of the measurable modification, and lifetime slabs have finite mass.

See Bertoin, Lévy Processes, Chapter IV.

The excursion measure N

noncomputable def BGW.StableTrees.excursionMeasure (θ : ℝ) : MeasureTheory.Measure Excursion

The excursion measure N A = ∫⁻ f, μ f ((0,1] × A) ∂P, P = stableLocalLaw θ, as the Measure.join of the law of f ↦ ((μ f) ↾ (0,1] × univ).map Prod.snd.

Equations

• One or more equations did not get rendered due to their size.

theorem BGW.StableTrees.excursionMeasure_apply {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {A : Set Excursion} (hA : MeasurableSet A) : (excursionMeasure θ) A = ∫⁻ (f : Skorokhod.DLoc), (excursionPointMeasure f) (Set.Ioc 0 1 ×ˢ A) ∂↑(stableLocalLaw θ)

Defining formula: N A = ∫⁻ f, μ f ((0,1] × A) ∂P.

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

Independence of the modification: for every measurable modification ξ, N A = ∫⁻ ξ ((0,1] × A) ∂P, which is markRate.

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

Finite lifetime slabs: N {ε < ζ} < ∞ for every ε > 0.

theorem BGW.StableTrees.sigmaFinite_excursionMeasure {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : MeasureTheory.SigmaFinite (excursionMeasure θ)

σ-finiteness of N (exhaustion by {1/(n+1) < ζ}; every lifetime is positive).