Theorems · Theorem · real analysis

norm_sub_le_mul_volume_of_norm_fderiv_le

∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f : E → F} {a b : E} {C : ℝ} {s : Set E},
  IsOpen s →
    DiffContOnCl ℝ f s →
      openSegment ℝ a b ⊆ s →
        (∀ x ∈ s, ‖fderiv ℝ f x‖ ≤ C) →
          ‖f b - f a‖ ≤
            C * ‖b - a‖ * MeasureTheory.volume.real {t | t ∈ Set.Ioo 0 1 ∧ fderiv ℝ f ((AffineMap.lineMap a b) t) ≠ 0}

Let f : E → F be a function differentiable on a set s and continuous on its closure. Let a, b be two points such that the open segment connecting a to b is a subset of s. If ‖Df‖ ≤ C everywhere on s then ‖f b - f a‖ ≤ C * volume u, where u is the set of points t ∈ Ioo 0 1 such that f has nonzero derivative at lineMap a b t.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace