English
If F is Lipschitz on a set and takes values in a product space, then the differentiation property extends componentwise to the product, i.e., differentiability almost everywhere in each coordinate implies differentiability in the product sense.
Русский
Если функция Lipschitz на множестве и принимает значения в произведённом пространстве, то дифференцируемость компонентно переносится на произведение.
LaTeX
$$$\\text{ae\_differentiableWithinAt\_pi}$$$
Lean4
/-- A real-valued function on a finite-dimensional space which is Lipschitz is
differentiable almost everywere. Superseded by
`LipschitzWith.ae_differentiableAt` which works for functions taking value in any
finite-dimensional space. -/
theorem ae_differentiableAt_of_real (hf : LipschitzWith C f) : ∀ᵐ x ∂μ, DifferentiableAt ℝ f x :=
by
obtain ⟨s, s_count, s_dense⟩ : ∃ (s : Set E), s.Countable ∧ Dense s := TopologicalSpace.exists_countable_dense E
have hs : sphere 0 1 ⊆ closure s := by rw [s_dense.closure_eq]; exact subset_univ _
filter_upwards [hf.ae_exists_fderiv_of_countable s_count]
rintro x ⟨L, hL⟩
exact (hf.hasFDerivAt_of_hasLineDerivAt_of_closure hs hL).differentiableAt
