Theorems · Theorem · real analysis

norm_sub_le_mul_volume_of_norm_lineDeriv_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 : ℝ},
  ContinuousOn f (segment ℝ a b) →
    (∀ t ∈ Set.Ioo 0 1, LineDifferentiableAt ℝ f ((AffineMap.lineMap a b) t) (b - a)) →
      (∀ᵐ (t : ℝ), t ∈ Set.Ioo 0 1 → ‖lineDeriv ℝ f ((AffineMap.lineMap a b) t) (b - a)‖ ≤ C) →
        ‖f b - f a‖ ≤
          C * MeasureTheory.volume.real {t | t ∈ Set.Ioo 0 1 ∧ lineDeriv ℝ f ((AffineMap.lineMap a b) t) (b - a) ≠ 0}

Consider a function f : E → F continuous on a segment [a, b] and line differentiable in the direction b - a at all points of the open segment (a, b). If ‖∂_{b - a} f‖ ≤ C at a.e. all points of the open segment, then ‖f b - f a‖ ≤ C * volume s, where s is the set of points t ∈ Ioo 0 1 such that f has nonzero line derivative in the direction b - a at lineMap a b t.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace