norm_image_sub_le_of_norm_fderivWithin_le

English

If f differentiable on a convex set, then f has a Lipschitz bound along lines inside the set.

Русский

Если f дифференцируема на выпуклом множестве, то вдоль прямых внутри множества существует линейное ограничение липшицивости.

LaTeX

$$$\forall x,y\in s, \|f(y)-f(x)\| ≤ K \|y-x\|$ for some K$$$

Lean4

/-- The mean value theorem on a convex set: if the derivative of a function within this set is
bounded by `C`, then the function is `C`-Lipschitz. Version with `fderivWithin`. -/
theorem norm_image_sub_le_of_norm_fderivWithin_le (hf : DifferentiableOn 𝕜 f s)
    (bound : ∀ x ∈ s, ‖fderivWithin 𝕜 f s 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_hasFDerivWithin_le (fun x hx => (hf x hx).hasFDerivWithinAt) bound xs ys

Похожие утверждения