English
If differentiable on 𝕜 with bounded derivative norm by NNReal C, then LipschitzOnWith C f s holds for any s.
Русский
Если дифференцируемая функция имеет ограниченную норму производной, то on сфера Lipschitzness на C.
LaTeX
$$$$ \\text{LipschitzOnWith } C\, f\, s $$$$
Lean4
/-- Over the reals or the complexes, a continuously differentiable function is strictly
differentiable. -/
theorem hasStrictFDerivAt_of_hasFDerivAt_of_continuousAt (hder : ∀ᶠ y in 𝓝 x, HasFDerivAt f (f' y) y)
(hcont : ContinuousAt f' x) : HasStrictFDerivAt f (f' x) x := by
-- turn little-o definition of strict_fderiv into an epsilon-delta statement
rw [hasStrictFDerivAt_iff_isLittleO, isLittleO_iff]
refine fun c hc =>
Metric.eventually_nhds_iff_ball.mpr
?_
-- the correct ε is the modulus of continuity of f'
rcases Metric.mem_nhds_iff.mp (inter_mem hder (hcont <| ball_mem_nhds _ hc)) with ⟨ε, ε0, hε⟩
refine
⟨ε, ε0, ?_⟩
-- simplify formulas involving the product E × E
rintro ⟨a, b⟩ h
rw [← ball_prod_same, prodMk_mem_set_prod_eq] at h
have hf' : ∀ x' ∈ ball x ε, ‖f' x' - f' x‖ ≤ c := fun x' H' =>
by
rw [← dist_eq_norm]
exact
le_of_lt
(hε H').2
-- apply mean value theorem
letI : NormedSpace ℝ G := RestrictScalars.normedSpace ℝ 𝕜 G
refine (convex_ball _ _).norm_image_sub_le_of_norm_hasFDerivWithin_le' ?_ hf' h.2 h.1
exact fun y hy => (hε hy).1.hasFDerivWithinAt
