Removing the discount in occupation estimates

Fubini gives integration by parts for bounded measurable occupation kernels.

References

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

theorem BGW.StableTrees.integral_exp_mul_discountedPrimitive {k : ℝ → ℝ} {t : ℝ} (hk : MeasureTheory.IntegrableOn k (Set.Ioc 0 t) MeasureTheory.volume) : ∫ (s : ℝ) in Set.Ioc 0 t, Real.exp s * ∫ (u : ℝ) in Set.Ioc 0 s, Real.exp (-u) * k u = (Real.exp t * ∫ (u : ℝ) in Set.Ioc 0 t, Real.exp (-u) * k u) - ∫ (u : ℝ) in Set.Ioc 0 t, k u

Fubini integration by parts for a discounted primitive.

theorem BGW.StableTrees.abs_integral_le_of_discountedPrimitive_bound {k : ℝ → ℝ} {t H : ℝ} (ht : 0 ≤ t) (hk : MeasureTheory.IntegrableOn k (Set.Icc 0 t) MeasureTheory.volume) (hK : ∀ s ∈ Set.Icc 0 t, |∫ (u : ℝ) in Set.Ioc 0 s, Real.exp (-u) * k u| ≤ H) : |∫ (u : ℝ) in Set.Ioc 0 t, k u| ≤ 2 * Real.exp t * H

A bound on a discounted primitive controls its undiscounted integral.