Theorems · Theorem · real analysis

exists_dist_slope_lt_pairwiseDisjoint_hasSum

∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {f f' : ℝ → F} {d b η : ℝ},
  d ≤ b →
    (∀ᵐ (x : ℝ), x ∈ Set.Ioo d b → HasDerivAt f (f' x) x) →
      0 < η →
        ∃ u,
          (∀ z ∈ u, (d < z.1 ∧ z.1 < z.2 ∧ z.2 < b) ∧ dist (slope f z.1 z.2) (f' z.1) < η) ∧
            (u.PairwiseDisjoint fun z => Set.Icc z.1 z.2) ∧ HasSum (fun z => (↑z).2 - (↑z).1) (b - d)

If f has derivative f' a.e. on [d, b] and η is positive, then there is a collection of pairwise disjoint closed subintervals of [a, b] of total length b - a where the slope of f on each subinterval [x, y] differs from f' x by at most η.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace