ae_differentiableWithinAt_real — Mathlib

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

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