Signed lifetime density comparison

Two nonnegative prefix tests give the signed integral identity whenever the weighted test is integrable. The exceptional set depends on the fixed test.

References

• L. Chaumont, Excursion normalisée, méandre et pont pour les processus de Lévy stables, Bull. Sci. Math. 121 (1997), 377–403.

theorem BGW.StableTrees.prefix_density_ae_lifetime_integral {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (a : NNReal) (ha : 0 < a) (F : Skorokhod.D ↑a ℝ → ℝ) (hF : Measurable F) (hFb : ∃ (C : ℝ), ∀ (x : Skorokhod.D ↑a ℝ), |F x| ≤ C) : ∀ᵐ (u : ↑(Set.Ioi 0)) ∂volIoi.restrict {u : ↑(Set.Ioi 0) | ↑a < ↑u}, MeasureTheory.Integrable (fun (e : Excursion) => F (excursionRestrict a e) * qKernel θ (↑u - ↑a) (↑e.path a)) (excursionTail θ ↑a) → (lifetimeDensity θ ↑u).toReal * ∫ (e : Excursion), F (excursionRestrict a e) ∂excursionAt θ u = ∫ (e : Excursion), F (excursionRestrict a e) * qKernel θ (↑u - ↑a) (↑e.path a) ∂excursionTail θ ↑a

Signed integral comparison at almost every lifetime, whenever the weighted test is integrable.