Theorems · Definition · real analysis

AbsolutelyContinuousOnInterval

{X : Type u_1} → [PseudoMetricSpace X] → (ℝ → X) → ℝ → ℝ → Prop

AbsolutelyContinuousOnInterval f a b: A function f is absolutely continuous on uIcc a b if the function which (intuitively) maps uIoc (a i) (b i), i < n to ∑ i ∈ Finset.range n, dist (f (a i)) (f (b i)) tendsto 𝓝 0 wrt totalLengthFilter restricted to disjWithin a b. This is equivalent to the traditional ε-δ definition: 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

31 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpace