ae_differentiableWithinAt_of_mem_real

English

A real-valued Lipschitz function on a set is differentiable almost everywhere in that set.

Русский

Липшицева функция в рамках нескольких измерений направлена на дифференцируемость почти всюду на множестве.

LaTeX

$$$\forall C:\; LipschitzOnWith C f s \Rightarrow \ae x\in volume.restrict s, DifferentiableWithinAt Real f s 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_of_mem`.
-/
theorem ae_differentiableWithinAt_of_mem_real {C : ℝ≥0} {f : ℝ → V} {s : Set ℝ} (h : LipschitzOnWith C f s) :
    ∀ᵐ x, x ∈ s → DifferentiableWithinAt ℝ f s x :=
  h.locallyBoundedVariationOn.ae_differentiableWithinAt_of_mem

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