# mathlib3documentation

analysis.calculus.monotone

# Differentiability of monotone functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We show that a monotone function f : ℝ → ℝ is differentiable almost everywhere, in monotone.ae_differentiable_at. (We also give a version for a function monotone on a set, in monotone_on.ae_differentiable_within_at.)

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 vitali_family.ae_tendsto_rn_deriv. 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].

theorem tendsto_apply_add_mul_sq_div_sub {f : } {x a c d : } {l : filter } (hl : l {x}) (hf : filter.tendsto (λ (y : ), (f y - d) / (y - x)) l (nhds a)) (h' : filter.tendsto (λ (y : ), y + c * (y - x) ^ 2) l l) :
filter.tendsto (λ (y : ), (f (y + c * (y - x) ^ 2) - d) / (y - x)) l (nhds a)

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.

theorem monotone.ae_has_deriv_at {f : } (hf : monotone f) :

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

theorem monotone.ae_differentiable_at {f : } (hf : monotone f) :
∀ᵐ (x : ),

A monotone real function is differentiable Lebesgue-almost everywhere.

theorem monotone_on.ae_differentiable_within_at_of_mem {f : } {s : set } (hf : s) :
∀ᵐ (x : ), x s

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 monotone_on.ae_differentiable_within_at.

theorem monotone_on.ae_differentiable_within_at {f : } {s : set } (hf : s) (hs : measurable_set s) :

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 monotone_on.ae_differentiable_within_at_of_mem.