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) (ENNReal.toReal (MeasureTheory.Measure.rnDeriv (StieltjesFunction.measure f) MeasureTheory.volume x)) 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 (ENNReal.toReal (MeasureTheory.Measure.rnDeriv (StieltjesFunction.measure (Monotone.stieltjesFunction hf)) MeasureTheory.volume x)) 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 ∈ s → DifferentiableWithinAt ℝ 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.Measure.restrict MeasureTheory.volume 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.