English
A real-valued Lipschitz function on a finite dimensional space is differentiable almost everywhere.
Русский
Липшицева функция на конечномерном пространстве реальна дифференцируема почти всюду.
LaTeX
$$$\forall C:\; LipschitzWith C f \Rightarrow \ae x, DifferentiableAt Real f x$$$
Lean4
/-- A real function into a finite-dimensional real vector space which is Lipschitz on a set
is differentiable almost everywhere in this set. For the general Rademacher theorem assuming
that the source space is finite dimensional, see `LipschitzOnWith.ae_differentiableWithinAt`. -/
theorem ae_differentiableWithinAt_real {C : ℝ≥0} {f : ℝ → V} {s : Set ℝ} (h : LipschitzOnWith C f s)
(hs : MeasurableSet s) : ∀ᵐ x ∂volume.restrict s, DifferentiableWithinAt ℝ f s x :=
h.locallyBoundedVariationOn.ae_differentiableWithinAt hs