# Differentiability of monotone functions #

We show that a monotone function `f : ℝ → ℝ`

is differentiable almost everywhere, in
`Monotone.ae_differentiableAt`

. (We also give a version for a function monotone on a set, in
`MonotoneOn.ae_differentiableWithinAt`

.)

If the function `f`

is continuous, this follows directly from general differentiation of measure
theorems. Let `μ`

be the Stieltjes measure associated to `f`

. Then, almost everywhere,
`μ [x, y] / Leb [x, y]`

(resp. `μ [y, x] / Leb [y, x]`

) converges to the Radon-Nikodym derivative
of `μ`

with respect to Lebesgue when `y`

tends to `x`

in `(x, +∞)`

(resp. `(-∞, x)`

), by
`VitaliFamily.ae_tendsto_rnDeriv`

. As `μ [x, y] = f y - f x`

and `Leb [x, y] = y - x`

, this
gives differentiability right away.

When `f`

is only monotone, the same argument works up to small adjustments, as the associated
Stieltjes measure satisfies `μ [x, y] = f (y^+) - f (x^-)`

(the right and left limits of `f`

at `y`

and `x`

respectively). One argues that `f (x^-) = f x`

almost everywhere (in fact away from a
countable set), and moreover `f ((y - (y-x)^2)^+) ≤ f y ≤ f (y^+)`

. This is enough to deduce the
limit of `(f y - f x) / (y - x)`

by a lower and upper approximation argument from the known
behavior of `μ [x, y]`

.

If `(f y - f x) / (y - x)`

converges to a limit as `y`

tends to `x`

, then the same goes if
`y`

is shifted a little bit, i.e., `f (y + (y-x)^2) - f x) / (y - x)`

converges to the same limit.
This lemma contains a slightly more general version of this statement (where one considers
convergence along some subfilter, typically `𝓝[<] x`

or `𝓝[>] x`

) tailored to the application
to almost everywhere differentiability of monotone functions.

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

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

A monotone real function is differentiable Lebesgue-almost everywhere.

A real function which is monotone on a set is differentiable Lebesgue-almost everywhere on
this set. This version does not assume that `s`

is measurable. For a formulation with
`volume.restrict s`

assuming that `s`

is measurable, see `MonotoneOn.ae_differentiableWithinAt`

.

A real function which is monotone on a set is differentiable Lebesgue-almost everywhere on
this set. This version assumes that `s`

is measurable and uses `volume.restrict s`

.
For a formulation without measurability assumption,
see `MonotoneOn.ae_differentiableWithinAt_of_mem`

.