Tail estimates for cumulative clock integrals

Tail domination of the weight measure transfers, by Tonelli, to integrals of a nondecreasing clock. A half-rate discount makes the estimates uniform at large times.

theorem BGW.StableTrees.lintegral_clock_le_of_tail_le {m : NNReal → ℝ} (hm : Monotone m ∧ Continuous m) (hm0 : m 0 = 0) (ν : MeasureTheory.Measure ℝ) [MeasureTheory.SFinite ν] (v : ℝ → ENNReal) (C : ENNReal) (hv : Measurable v) (hν : ∀ (t : ℝ), 0 < t → ν (Set.Ioi t) ≤ C * v t) : ∫⁻ (s : ℝ) in Set.Ioi 0, ENNReal.ofReal (m s.toNNReal) ∂ν ≤ C * ∫⁻ (t : ℝ) in Set.Ioi 0, v t ∂(pathStieltjes m).measure

A bound on weight tails controls the cumulative clock integral.

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

theorem BGW.StableTrees.lintegral_clock_tail_le {m : NNReal → ℝ} (hm : Monotone m ∧ Continuous m) (hm0 : m 0 = 0) (ν : MeasureTheory.Measure ℝ) [MeasureTheory.SFinite ν] {q : ℝ} (hq : 0 < q) (hν : ∀ (t : ℝ), 0 ≤ t → ν (Set.Ioi t) ≤ ENNReal.ofReal (Real.exp (-q * t))) (T : NNReal) : ∫⁻ (s : ℝ) in Set.Ioi ↑T, ENNReal.ofReal (m s.toNNReal) ∂ν ≤ ENNReal.ofReal (Real.exp (-(q / 2) * ↑T)) * ∫⁻ (t : ℝ) in Set.Ioi 0, ENNReal.ofReal (Real.exp (-(q / 2) * t)) ∂(pathStieltjes m).measure

Cumulative mass beyond T is bounded by the half-rate clock potential times exp(-q T / 2). This uses only domination of tails, allowing atoms in the weight measure.

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

theorem BGW.StableTrees.integrable_clock_and_integral_tail_le {m : NNReal → ℝ} (hm : Monotone m ∧ Continuous m) (hm0 : m 0 = 0) (ν : MeasureTheory.Measure ℝ) [MeasureTheory.SFinite ν] {q : ℝ} (hq : 0 < q) (hν : ∀ (t : ℝ), 0 ≤ t → ν (Set.Ioi t) ≤ ENNReal.ofReal (Real.exp (-q * t))) (hi : MeasureTheory.IntegrableOn (fun (t : ℝ) => Real.exp (-(q / 2) * t)) (Set.Ioi 0) (pathStieltjes m).measure) : MeasureTheory.IntegrableOn (fun (s : ℝ) => m s.toNNReal) (Set.Ioi 0) ν ∧ ∀ (T : NNReal), ∫ (s : ℝ) in Set.Ioi ↑T, m s.toNNReal ∂ν ≤ Real.exp (-(q / 2) * ↑T) * ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-(q / 2) * t) ∂(pathStieltjes m).measure

A finite half-rate clock potential gives integrability of the cumulative clock against any measure with the stated tail bound, together with a real tail estimate.

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

theorem BGW.StableTrees.abs_integral_clock_sub_le {m n : NNReal → ℝ} (hm : Monotone m ∧ Continuous m) (hm0 : m 0 = 0) (hn : Monotone n ∧ Continuous n) (hn0 : n 0 = 0) (ν : MeasureTheory.Measure ℝ) [MeasureTheory.SFinite ν] {q : ℝ} (hq : 0 < q) (hν : ∀ (t : ℝ), 0 ≤ t → ν (Set.Ioi t) ≤ ENNReal.ofReal (Real.exp (-q * t))) (hmi : MeasureTheory.IntegrableOn (fun (t : ℝ) => Real.exp (-(q / 2) * t)) (Set.Ioi 0) (pathStieltjes m).measure) (hni : MeasureTheory.IntegrableOn (fun (t : ℝ) => Real.exp (-(q / 2) * t)) (Set.Ioi 0) (pathStieltjes n).measure) (T : NNReal) {E : ℝ} (hE : 0 ≤ E) (he : ∀ t ≤ T, |m t - n t| ≤ E) : |∫ (s : ℝ) in Set.Ioi 0, m s.toNNReal ∂ν - ∫ (s : ℝ) in Set.Ioi 0, n s.toNNReal ∂ν| ≤ E + Real.exp (-(q / 2) * ↑T) * (∫ (t : ℝ) in Set.Ioi 0, Real.exp (-(q / 2) * t) ∂(pathStieltjes m).measure + ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-(q / 2) * t) ∂(pathStieltjes n).measure)

The difference of two cumulative integrals is controlled on a compact interval by uniform clock error, and outside it by the two half-rate potentials.

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