English
The norm is differentiable almost everywhere in a finite-dimensional real normed space.
Русский
Норма дифференцируема почти везде в конечномерном вещественном нормированном пространстве.
LaTeX
$$$\\text{ae\\_differentiableAt\\_norm}$$$
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_of_mem {f : E → F} (hf : LipschitzOnWith C f s) :
∀ᵐ x ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x :=
by
have A := (Basis.ofVectorSpace ℝ F).equivFun.toContinuousLinearEquiv
suffices H : ∀ᵐ x ∂μ, x ∈ s → DifferentiableWithinAt ℝ (A ∘ f) s x
by
filter_upwards [H] with x hx xs
have : f = (A.symm ∘ A) ∘ f := by simp only [ContinuousLinearEquiv.symm_comp_self, Function.id_comp]
rw [this]
exact A.symm.differentiableAt.comp_differentiableWithinAt x (hx xs)
apply ae_differentiableWithinAt_of_mem_pi
exact A.lipschitz.comp_lipschitzOnWith hf
