English
For a Lipschitz function f, almost everywhere there exists a Frechet derivative, and there is a line-derivative-to-FDeriv bridge that yields HasFDerivAt almost everywhere.
Русский
Для Lipschitz-функции f почти везде существует Фреше-дериватив; существует связь между линейной производной и Фреше-деривативом, дающая HasFDerivAt почти повсеместно.
LaTeX
$$$\\text{ae\_differentiableAt}(f) = \\text{ae\_differentiableWithinAt}(f)$ a.e. implies HasFDerivAt a.e.$$
Lean4
theorem ae_lineDifferentiableAt (hf : LipschitzWith C f) (v : E) : ∀ᵐ p ∂μ, LineDifferentiableAt ℝ f p v :=
by
let L : ℝ →L[ℝ] E := ContinuousLinearMap.smulRight (1 : ℝ →L[ℝ] ℝ) v
suffices A : ∀ p, ∀ᵐ (t : ℝ) ∂volume, LineDifferentiableAt ℝ f (p + t • v) v from
ae_mem_of_ae_add_linearMap_mem L.toLinearMap volume μ (measurableSet_lineDifferentiableAt hf.continuous) A
intro p
have : ∀ᵐ (s : ℝ), DifferentiableAt ℝ (fun t ↦ f (p + t • v)) s :=
(hf.comp ((LipschitzWith.const p).add L.lipschitz)).ae_differentiableAt_real
filter_upwards [this] with s hs
have h's : DifferentiableAt ℝ (fun t ↦ f (p + t • v)) (s + 0) := by simpa using hs
have : DifferentiableAt ℝ (fun t ↦ s + t) 0 := differentiableAt_id.const_add _
simp only [LineDifferentiableAt]
convert h's.comp 0 this with _ t
simp only [add_assoc, Function.comp_apply, add_smul]
