Compensation of discounted excursion occupation

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

theorem BGW.StableTrees.measurable_predictable_level : Measurable Prod.fst

The level coordinate is measurable for the stopped-past predictable sigma algebra.

theorem BGW.StableTrees.ae_passagePast_eq_passageTimeMinus {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (x : NNReal), passagePast x f = ↑(passageTimeMinus x f)

On the full-probability event of finite passages, the extended past agrees with its finite reading, simultaneously at all levels.

theorem BGW.StableTrees.measurable_excursionDiscount (q : ℝ) {G : ℝ → ENNReal} (hG : Measurable G) : Measurable (excursionDiscount q G)

The discounted excursion occupation functional is measurable in its excursion mark.

theorem BGW.StableTrees.lintegral_infimum_resolvent_factorization {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {q : ℝ} (hq : 0 < q) {F G : ℝ → ENNReal} (hF : Measurable F) (hG : Measurable G) : ∫⁻ (f : Skorokhod.DLoc), ∫⁻ (t : ℝ) in Set.Ici 0, ENNReal.ofReal (q * Real.exp (-q * t)) * F (localTime f t.toNNReal) * G (↑(reflectedFrom 0 f) t.toNNReal) ∂↑(stableLocalLaw θ) = (∫⁻ (f : Skorokhod.DLoc), ∫⁻ (x : NNReal), expNeg (ENNReal.ofReal q * passagePast x f) * F ↑x ∂lebNN ∂↑(stableLocalLaw θ)) * ∫⁻ (e : Excursion), excursionDiscount q G e ∂excursionMeasure θ

Compensation separates the infimum level from the reflected position in the exponentially discounted occupation integral.