ae_differentiableAt_real — Mathlib

English

A real Lipschitz function on a finite-dimensional domain is differentiable almost everywhere.

Русский

Липшицева функция на конечномерном домене дифференцируема почти повсюду.

LaTeX

$$$\forall C\; f:\mathbb{R} \to V,\ LipschitzWith C f \Rightarrow \ae x, DifferentiableAt Real f x$$$

Lean4

/-- A real Lipschitz function into a finite-dimensional real vector space is differentiable
almost everywhere. For the general Rademacher theorem assuming
that the source space is finite dimensional, see `LipschitzWith.ae_differentiableAt`. -/
theorem ae_differentiableAt_real {C : ℝ≥0} {f : ℝ → V} (h : LipschitzWith C f) : ∀ᵐ x, DifferentiableAt ℝ f x :=
  (h.locallyBoundedVariationOn univ).ae_differentiableAt

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