Extended discounted cumulative-integral formula

Tonelli proves the Laplace formula before any finiteness assertion. In particular no convergence of Stieltjes measures and no recurrence assumption are needed.

References

• J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.

theorem BGW.StableTrees.lintegral_exp_eq_lintegral_cumulative (μ : MeasureTheory.Measure ℝ) [MeasureTheory.SFinite μ] {q : ℝ} (hq : 0 < q) (s : ℝ) : ∫⁻ (t : ℝ) in Set.Ioi s, ENNReal.ofReal (Real.exp (-q * t)) ∂μ = ENNReal.ofReal q * ∫⁻ (u : ℝ) in Set.Ioi s, ENNReal.ofReal (Real.exp (-q * u)) * μ (Set.Ioc s u)

Tonelli's discounted cumulative-integral formula, valid even when both sides are infinite.

theorem BGW.StableTrees.pathStieltjes_lintegral_exp {m : NNReal → ℝ} (hm : Monotone m ∧ Continuous m) {q : ℝ} (hq : 0 < q) (s : NNReal) : ∫⁻ (t : ℝ) in Set.Ioi ↑s, ENNReal.ofReal (Real.exp (-q * t)) ∂(pathStieltjes m).measure = ENNReal.ofReal q * ∫⁻ (t : ℝ) in Set.Ioi ↑s, ENNReal.ofReal (Real.exp (-q * t)) * ENNReal.ofReal (m t.toNNReal - m s)

The extended Stieltjes Laplace formula needs no integrability or boundary hypothesis.

theorem BGW.StableTrees.lintegral_exp_mul_eq_primitive {k : ℝ → ℝ} (hk : Measurable k) (hk0 : ∀ (t : ℝ), 0 ≤ k t) {q : ℝ} (hq : 0 < q) (s : ℝ) (hloc : ∀ (t : ℝ), MeasureTheory.IntegrableOn k (Set.Ioc s t) MeasureTheory.volume) : ∫⁻ (t : ℝ) in Set.Ioi s, ENNReal.ofReal (Real.exp (-q * t) * k t) = ENNReal.ofReal q * ∫⁻ (t : ℝ) in Set.Ioi s, ENNReal.ofReal (Real.exp (-q * t)) * ENNReal.ofReal (∫ (u : ℝ) in Set.Ioc s t, k u)

The same Tonelli identity for a nonnegative time kernel and its ordinary primitive.

theorem BGW.StableTrees.measurable_integral_Ioc (k : ℝ → ℝ) (hk : Measurable k) (s : ℝ) : Measurable fun (t : ℝ) => ∫ (u : ℝ) in Set.Ioc s t, k u

A measurable kernel has a measurable primitive with a moving upper endpoint.

theorem BGW.StableTrees.integral_exp_mul_eq_primitive {k : ℝ → ℝ} (hk : Measurable k) (hk0 : ∀ (t : ℝ), 0 ≤ k t) {q : ℝ} (hq : 0 < q) (s : ℝ) (hloc : ∀ (t : ℝ), MeasureTheory.IntegrableOn k (Set.Ioc s t) MeasureTheory.volume) (hi : MeasureTheory.IntegrableOn (fun (t : ℝ) => Real.exp (-q * t) * k t) (Set.Ioi s) MeasureTheory.volume) : MeasureTheory.IntegrableOn (fun (t : ℝ) => Real.exp (-q * t) * ∫ (u : ℝ) in Set.Ioc s t, k u) (Set.Ioi s) MeasureTheory.volume ∧ ∫ (t : ℝ) in Set.Ioi s, Real.exp (-q * t) * k t = q * ∫ (t : ℝ) in Set.Ioi s, Real.exp (-q * t) * ∫ (u : ℝ) in Set.Ioc s t, k u

A finite discounted kernel integral makes the discounted primitive integrable, and converts the extended Tonelli formula into the ordinary real integral identity.