Finite weighted clock integrals

Half-rate potentials justify conversion of the cumulative Tonelli identities to real integrals. All integrability assertions precede the corresponding real identities.

theorem BGW.StableTrees.integrable_of_lintegral_eq_ofReal {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f μ) (h0 : 0 ≤ᵐ[μ] f) {a : ℝ} (he : ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ = ENNReal.ofReal a) : MeasureTheory.Integrable f μ

A nonnegative measurable integral is determined by its finite extended integral.

Reference: Bertoin, Lévy Processes, Chapter VI.

theorem BGW.StableTrees.integral_exp_supOccupation_clock {q ε : ℝ} (hq : 0 < q) (hε : 0 < ε) (f : Skorokhod.DLoc) (hf : ↑f 0 = 0) : MeasureTheory.IntegrableOn (fun (t : ℝ) => Real.exp (-q * t)) (Set.Ioi 0) (pathStieltjes (supOccupation ε f)).measure ∧ ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-q * t) ∂(pathStieltjes (supOccupation ε f)).measure = supAuxOccupationTail q ε 0 f

The exponential Stieltjes potential of occupation is the ordinary discounted occupation.

Reference: Bertoin, Lévy Processes, Chapter VI.

theorem BGW.StableTrees.integral_supWeight_eq_cumulative {q lam : ℝ} (hq : 0 < q) (hlam : 0 ≤ lam) {f : Skorokhod.DLoc} (hf : ↑f 0 = 0) {m : NNReal → ℝ} (hm : Monotone m ∧ Continuous m) (hm0 : m 0 = 0) (hi : MeasureTheory.IntegrableOn (fun (t : ℝ) => Real.exp (-(q / 2) * t)) (Set.Ioi 0) (pathStieltjes m).measure) : MeasureTheory.IntegrableOn (fun (t : ℝ) => Real.exp (-q * t - lam * supRunning f t.toNNReal)) (Set.Ioi 0) (pathStieltjes m).measure ∧ ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-q * t - lam * supRunning f t.toNNReal) ∂(pathStieltjes m).measure = ∫ (s : ℝ) in Set.Ioi 0, m s.toNNReal ∂(supWeightStieltjes q lam ⋯ hlam f).measure

A finite half-rate clock potential makes the weighted clock and cumulative integrals integrable and identifies their real values.

Reference: Bertoin, Lévy Processes, Chapter VI.