English
For a Lipschitz function f: E → F and a countable set s of directions, there exists, almost everywhere, a linear functional L such that for all directions v in s, HasLineDerivAt Real f x v is witnessed by L v.
Русский
Для Lipschitz-функции f: E → F и счетного множества направлений существует почти всюду линейный функционал L, такой что для всех направлений v в s имеет место HasLineDerivAt Real f x v, задаваемое L v.
LaTeX
$$$\exists L, \forall v\in s, HasLineDerivAt( f, L v, x, v)$ a.e.$$
Lean4
/-- A real-valued function on a finite-dimensional space which is Lipschitz on a set is
differentiable almost everywere in this set. Superseded by
`LipschitzOnWith.ae_differentiableWithinAt_of_mem` which works for functions taking value in any
finite-dimensional space. -/
theorem ae_differentiableWithinAt_of_mem_of_real (hf : LipschitzOnWith C f s) :
∀ᵐ x ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x :=
by
obtain ⟨g, g_lip, hg⟩ : ∃ (g : E → ℝ), LipschitzWith C g ∧ EqOn f g s := hf.extend_real
filter_upwards [g_lip.ae_differentiableAt_of_real] with x hx xs
exact hx.differentiableWithinAt.congr hg (hg xs)
