Theorems · Theorem · real analysis

norm_sub_le_mul_volume_of_norm_deriv_le_of_le

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b C : ℝ},
  a ≤ b →
    ContinuousOn f (Set.Icc a b) →
      DifferentiableOn ℝ f (Set.Ioo a b) →
        (∀ᵐ (t : ℝ), t ∈ Set.Ioo a b → ‖deriv f t‖ ≤ C) →
          ‖f b - f a‖ ≤ C * MeasureTheory.volume.real {x | x ∈ Set.Ioo a b ∧ deriv f x ≠ 0}

Let f : ℝ → E be a function which is continuous on [a, b] and is differentiable on (a, b). Suppose that ‖f' t‖ ≤ C for a.e. t ∈ (a, b). Then the distance between f a and f b is at most C times the measure of x ∈ (a, b) such that f' x ≠ 0. This lemma is useful, if f is known to have zero derivative at most points of [a, b].

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace