Cumulative Tonelli formula for decreasing weights

Writing a decreasing weight as the tail of a measure exchanges the clock measure and its continuous cumulative function. No differentiation of the weight is required.

theorem BGW.StableTrees.lintegral_tail_eq_lintegral_cumulative (μ ν : MeasureTheory.Measure ℝ) [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] (a : ℝ) : ∫⁻ (t : ℝ) in Set.Ioi a, ν (Set.Ioi t) ∂μ = ∫⁻ (s : ℝ) in Set.Ioi a, μ (Set.Ioo a s) ∂ν

Tonelli exchanges a tail weight and the open-interval cumulative mass.

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

theorem BGW.StableTrees.pathStieltjes_lintegral_tail {m : NNReal → ℝ} (hm : Monotone m ∧ Continuous m) (hm0 : m 0 = 0) (ν : MeasureTheory.Measure ℝ) [MeasureTheory.SFinite ν] : ∫⁻ (t : ℝ) in Set.Ioi 0, ν (Set.Ioi t) ∂(pathStieltjes m).measure = ∫⁻ (s : ℝ) in Set.Ioi 0, ENNReal.ofReal (m s.toNNReal) ∂ν

A continuous clock integrates a decreasing weight through its cumulative values.

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

theorem BGW.StableTrees.pathStieltjes_lintegral_decreasing {m : NNReal → ℝ} (hm : Monotone m ∧ Continuous m) (hm0 : m 0 = 0) (g : StieltjesFunction ℝ) {l : ℝ} (hg : Filter.Tendsto (↑g) Filter.atTop (nhds l)) : ∫⁻ (t : ℝ) in Set.Ioi 0, ENNReal.ofReal (l - ↑g t) ∂(pathStieltjes m).measure = ∫⁻ (s : ℝ) in Set.Ioi 0, ENNReal.ofReal (m s.toNNReal) ∂g.measure

A Stieltjes function with finite limit supplies a decreasing tail weight.

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