Theorems · Theorem · real analysis

norm_sub_le_integral_of_norm_deriv_le_of_le

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {B : ℝ → ℝ},
  a ≤ b →
    ContinuousOn f (Set.Icc a b) →
      DifferentiableOn ℝ f (Set.Ioo a b) →
        (∀ᵐ (t : ℝ), t ∈ Set.Ioo a b → ‖deriv f t‖ ≤ B t) →
          IntervalIntegrable B MeasureTheory.volume a b → ‖f b - f a‖ ≤ ∫ (t : ℝ) in a..b, B t

Displacement is at most the integral of an upper estimate on the speed. Let f : ℝ → E be a function which is continuous on a closed interval [a, b] and is differentiable on the open interval (a, b). If B t is an integrable upper estimate on ‖f' t‖, a < t < b, then ‖f b - f a‖ ≤ ∫ t in a..b, B t.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Cited by

1 results in Mathlib

Foundations

Depth 267 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace