Theorems · Theorem · real analysis

absolutelyContinuousOnInterval_iff

∀ {X : Type u_1} [inst : PseudoMetricSpace X] (f : ℝ → X) (a b : ℝ),
  AbsolutelyContinuousOnInterval f a b ↔
    ∀ ε > 0,
      ∃ δ > 0,
        ∀ E ∈ AbsolutelyContinuousOnInterval.disjWithin a b,
          ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < δ →
            ∑ i ∈ Finset.range E.1, dist (f (E.2 i).1) (f (E.2 i).2) < ε

The traditional ε-δ definition of absolutely continuous: A function f is absolutely continuous on uIcc a b if for any ε > 0, there is δ > 0 such that for any finite disjoint collection of intervals uIoc (a i) (b i) for i < n where a i, b i are all in uIcc a b for i < n, if ∑ i ∈ range n, dist (a i) (b i) < δ, then ∑ i ∈ range n, dist (f (a i)) (f (b i)) < ε.

Defined in

Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Cited by

2 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpace