Bound on an Integral over a Half-Open Interval

This statement bounds the absolute value of a Lebesgue integral over a half-open interval.

Let f : ℝ → ℝ be measurable. Let B : ℝ satisfy |f(s)| ≤ B for every real s, and let a,b : ℝ satisfy a ≤ b. Then the integral of f over the interval (a,b] has absolute value at most B times the interval length:

The result provides the basic increment estimate for the drift integral of a bounded measurable function and can be reused to establish Lipschitz and continuity properties of cumulative integrals.

Formalization Note: The set integral is ∫ s in Set.Ioc a b, f s ∂volume, namely integration with respect to Lebesgue measure (volume) over the set (a,b]. The theorem states the bound under the explicit measurability, pointwise boundedness, and ordering hypotheses; integrability is not an additional premise.

Original Lean declaration header

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

theorem abs_setIntegral_Ioc_le {f : ℝ → ℝ} (hf : Measurable f) {B : ℝ}
    (hB : ∀ s, |f s| ≤ B) {a b : ℝ} (hab : a ≤ b) :
    |∫ s in Set.Ioc a b, f s ∂volume| ≤ B * (b - a)

Module navigation

Module: LevyStochCalc/Brownian/DriftIncrement.

Next: abs_setIntegral_Icc_sub_le.

Source excerpt, lines 58–60 · Frozen source 408915f.