English
On a convex set, if a Fréchet derivative behaves like a power of the distance to x0, then the increment from x0 is dominated by the next power, i.e., a higher-order little-o bound holds.
Русский
На выпуклом множестве, если производная Фреше ведёт себя как степень расстояния до x0, то приращение f(x)−f(x0) контролируется следующей степенью через малый o.
LaTeX
$$$Convex 𝕽 s \\Rightarrow x_0 ∈ s \\Rightarrow (∀ x ∈ s, HasFDerivWithinAt f (f'(x)) s x) \\Rightarrow f'(\\cdot) = o (‖\\cdot - x_0‖^n) \\\\Rightarrow f(\\cdot) - f(x_0) = o (‖\\cdot - x_0‖^{n+1})$$$
Lean4
/-- The mean value theorem on a convex set in dimension 1: if the derivative of a function is
bounded by `C`, then the function is `C`-Lipschitz. Version with `deriv`. -/
theorem norm_image_sub_le_of_norm_deriv_le {C : ℝ} (hf : ∀ x ∈ s, DifferentiableAt 𝕜 f x)
(bound : ∀ x ∈ s, ‖deriv f x‖ ≤ C) (hs : Convex ℝ s) (xs : x ∈ s) (ys : y ∈ s) : ‖f y - f x‖ ≤ C * ‖y - x‖ :=
hs.norm_image_sub_le_of_norm_hasDerivWithin_le (fun x hx => (hf x hx).hasDerivAt.hasDerivWithinAt) bound xs ys
