English
A real function monotone on a set is differentiable almost everywhere on that set (no measurability assumed).
Русский
Функция монотонна на множестве; дифференцируема почти всюду на этом множестве без предположения измеримости.
LaTeX
$$$$ \text{ae differentiable within}$$$$
Lean4
/-- 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 ae_differentiableWithinAt_of_mem {f : ℝ → ℝ} {s : Set ℝ} (hf : MonotoneOn f s) :
∀ᵐ x, x ∈ s → DifferentiableWithinAt ℝ f s x := by
/- We use a global monotone extension of `f`, and argue that this extension is differentiable
almost everywhere. Such an extension need not exist (think of `1/x` on `(0, +∞)`), but it exists
if one restricts first the function to a compact interval `[a, b]`. -/
apply ae_of_mem_of_ae_of_mem_inter_Ioo
intro a b as bs _
obtain ⟨g, hg, gf⟩ : ∃ g : ℝ → ℝ, Monotone g ∧ EqOn f g (s ∩ Icc a b) :=
(hf.mono inter_subset_left).exists_monotone_extension
(hf.map_bddBelow inter_subset_left ⟨a, fun x hx => hx.2.1, as⟩)
(hf.map_bddAbove inter_subset_left ⟨b, fun x hx => hx.2.2, bs⟩)
filter_upwards [hg.ae_differentiableAt] with x hx
intro h'x
apply hx.differentiableWithinAt.congr_of_eventuallyEq _ (gf ⟨h'x.1, h'x.2.1.le, h'x.2.2.le⟩)
have : Ioo a b ∈ 𝓝[s] x := nhdsWithin_le_nhds (Ioo_mem_nhds h'x.2.1 h'x.2.2)
filter_upwards [self_mem_nhdsWithin, this] with y hy h'y
exact gf ⟨hy, h'y.1.le, h'y.2.le⟩
