English
*Rademacher's theorem*: a Lipschitz function on a finite-dimensional domain is differentiable almost everywhere inside the domain.
Русский
Пусть f ограничена по Липшицу на конечномерном пространстве; тогда она дифференцируема почти всюду внутри области.
LaTeX
$$$\text{If } f: E\to F \text{ is Lipschitz on } s \text{ with respect to a measure } μ, \text{ then }\forall\text{ a.e. } x\in s,\ DifferentiableWithinAt(f,s,x).$$$
Lean4
/-- *Rademacher's theorem*: a function between finite-dimensional real vector spaces which is
Lipschitz on a set is differentiable almost everywere in this set. -/
theorem ae_differentiableWithinAt {f : E → F} (hf : LipschitzOnWith C f s) (hs : MeasurableSet s) :
∀ᵐ x ∂(μ.restrict s), DifferentiableWithinAt ℝ f s x :=
by
rw [ae_restrict_iff' hs]
exact hf.ae_differentiableWithinAt_of_mem
