Theorems · Theorem · real analysis

AbsolutelyContinuousOnInterval.ae_differentiableAt

∀ {f : ℝ → ℝ} {a b : ℝ}, AbsolutelyContinuousOnInterval f a b → ∀ᵐ (x : ℝ), x ∈ Set.uIcc a b → DifferentiableAt ℝ f x

If f is absolute continuous on uIcc a b, then f' exists a.e. on uIcc a b.

Defined in

Mathlib.MeasureTheory.Function.AbsolutelyContinuous

Cited by

2 results in Mathlib

Foundations

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