Theorems · Theorem · real analysis

Monotone.ae_hasDerivAt

∀ {f : ℝ → ℝ} (hf : Monotone f),
  ∀ᵐ (x : ℝ), HasDerivAt f (hf.stieltjesFunction.measure.rnDeriv MeasureTheory.volume x).toReal x

A monotone function is almost everywhere differentiable, with derivative equal to the Radon-Nikodym derivative of the associated Stieltjes measure with respect to Lebesgue.

Defined in

Mathlib.Analysis.Calculus.Monotone

Cited by

1 results in Mathlib

Foundations

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