Documentation

Mathlib.Analysis.Calculus.Monotone

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

theorem tendsto_apply_add_mul_sq_div_sub {f : } {x : } {a : } {c : } {d : } {l : Filter } (hl : l nhdsWithin x {x}) (hf : Filter.Tendsto (fun (y : ) => (f y - d) / (y - x)) l (nhds a)) (h' : Filter.Tendsto (fun (y : ) => y + c * (y - x) ^ 2) l l) :
Filter.Tendsto (fun (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.

theorem StieltjesFunction.ae_hasDerivAt (f : StieltjesFunction) :
∀ᵐ (x : ), HasDerivAt (↑f) (f.measure.rnDeriv MeasureTheory.volume x).toReal x

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_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.

theorem Monotone.ae_differentiableAt {f : } (hf : Monotone f) :
∀ᵐ (x : ), DifferentiableAt f x

A monotone real function is differentiable Lebesgue-almost everywhere.

theorem MonotoneOn.ae_differentiableWithinAt_of_mem {f : } {s : Set } (hf : MonotoneOn f s) :
∀ᵐ (x : ), x sDifferentiableWithinAt f s x

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.

theorem MonotoneOn.ae_differentiableWithinAt {f : } {s : Set } (hf : MonotoneOn f s) (hs : MeasurableSet s) :
∀ᵐ (x : ) ∂MeasureTheory.volume.restrict s, DifferentiableWithinAt f s x

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.