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

source

theorem tendsto_apply_add_mul_sq_div_sub {f : ℝ → ℝ} {x a c d : ℝ} {l : filter ℝ} (hl : l ≤ nhds_within x {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.

source

theorem stieltjes_function.ae_has_deriv_at (f : stieltjes_function) :

∀ᵐ (x : ℝ), has_deriv_at ⇑f (f.measure.rn_deriv measure_theory.measure_space.volume x).to_real 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.

source

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

∀ᵐ (x : ℝ), has_deriv_at f (hf.stieltjes_function.measure.rn_deriv measure_theory.measure_space.volume x).to_real 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.

source

theorem monotone.ae_differentiable_at {f : ℝ → ℝ} (hf : monotone f) :

∀ᵐ (x : ℝ), differentiable_at ℝ f x

A monotone real function is differentiable Lebesgue-almost everywhere.

source

theorem monotone_on.ae_differentiable_within_at_of_mem {f : ℝ → ℝ} {s : set ℝ} (hf : monotone_on f s) :

∀ᵐ (x : ℝ), x ∈ s → differentiable_within_at ℝ 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 monotone_on.ae_differentiable_within_at.

source

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

∀ᵐ (x : ℝ) ∂measure_theory.measure_space.volume.restrict s, differentiable_within_at ℝ 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 monotone_on.ae_differentiable_within_at_of_mem.