Splitting occupation integrals over infimum excursions

The zero set has zero Lebesgue measure, so an occupation integral can be split over passage-jump intervals. The local-time coordinate is constant on each such interval.

Reference: J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapters IV and VI.

theorem BGW.StableTrees.ae_localTime_on_passage_interval {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ x ∈ passageJumpSet f, ∀ (t : NNReal), passageTimeMinus x f ≤ t → t ≤ passageTime x f → localTime f t = ↑x

On each passage-jump interval the infimum local time equals the jump label.

theorem BGW.StableTrees.ae_lintegral_split_passage_intervals {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (H : ℝ → ℝ → ℝ → ENNReal) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∫⁻ (t : ℝ) in Set.Ici 0, H t (localTime f t.toNNReal) (↑(reflectedFrom 0 f) t.toNNReal) = ∫⁻ (p : NNReal × Excursion), ∫⁻ (t : ℝ) in Set.Ioo ↑(passageTimeMinus p.1 f) ↑(passageTime p.1 f), H t (↑p.1) (↑(reflectedFrom 0 f) t.toNNReal) ∂excursionPointMeasure f

Split an occupation integral into the passage-jump intervals, recording the local-time label as the first coordinate of the excursion point measure.