English
A Lipschitz function on a finite-dimensional space is almost everywhere line-differentiable in the sense of line derivatives in almost every direction.
Русский
Липшицова функция на конечномерном пространстве почти везде линейно дифференцируема вдоль направлений.
LaTeX
$$$\\text{ae\_lineDifferentiableAt} \\subseteq \\text{LineDifferentiableAt}$$$
Lean4
/-- A function on a finite-dimensional space which is Lipschitz on a set and taking values in a
product space 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_pi {ι : Type*} [Fintype ι] {f : E → ι → ℝ} {s : Set E}
(hf : LipschitzOnWith C f s) : ∀ᵐ x ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x :=
by
have A : ∀ i : ι, LipschitzWith 1 (fun x : ι → ℝ ↦ x i) := fun i => LipschitzWith.eval i
have : ∀ i : ι, ∀ᵐ x ∂μ, x ∈ s → DifferentiableWithinAt ℝ (fun x : E ↦ f x i) s x := fun i ↦
by
apply ae_differentiableWithinAt_of_mem_of_real
exact LipschitzWith.comp_lipschitzOnWith (A i) hf
filter_upwards [ae_all_iff.2 this] with x hx xs
exact differentiableWithinAt_pi.2 (fun i ↦ hx i xs)
