ae_differentiableAt — Mathlib

English

The norm is differentiable almost everywhere in a finite-dimensional real normed space.

Русский

Норма имеет почти везде дифференцируемость в конечномерном вещественном пространстве.

LaTeX

$$$\\text{ae\\_differentiableAt\\_norm}$$$

Lean4

/-- *Rademacher's theorem*: a Lipschitz function between finite-dimensional real vector spaces is
differentiable almost everywhere. -/
theorem ae_differentiableAt {f : E → F} (h : LipschitzWith C f) : ∀ᵐ x ∂μ, DifferentiableAt ℝ f x :=
  by
  rw [← lipschitzOnWith_univ] at h
  simpa [differentiableWithinAt_univ] using h.ae_differentiableWithinAt_of_mem

Похожие утверждения