Lipschitz Bound for Window Integrals

Let $f:\mathbb R\to\mathbb R$ be measurable, let $B\ge0$, and assume $|f(s)|\le B$ for every $s\in\mathbb R$. For all $t,t'\in\mathbb R$, the Lebesgue integrals over the intervals $[0,t']$ and $[0,t]$ satisfy

The convention for negative endpoints is inherited from the set integrals over $[0,t]$. This is the deterministic Lipschitz estimate for drift increments.

Original Lean declaration header

Within namespace LevyStochCalc. Shown in its original module context. Proof omitted.

theorem abs_setIntegral_Icc_sub_le {f : ℝ → ℝ} (hf : Measurable f) {B : ℝ} (hB0 : 0 ≤ B)
    (hB : ∀ s, |f s| ≤ B) (t t' : ℝ) :
    |(∫ s in Set.Icc (0 : ℝ) t', f s ∂volume) - ∫ s in Set.Icc (0 : ℝ) t, f s ∂volume|
      ≤ B * |t' - t|

Module navigation

Module: LevyStochCalc/Brownian/DriftIncrement.

Supporting theorems: abs_setIntegral_Ioc_le.

Previous: abs_setIntegral_Ioc_le.

Source excerpt, lines 93–96 · Frozen source 408915f.