English
If s is convex and f,g: E→G are differentiable with derivatives bounded by C on s, then f is C-Lipschitz on s; that is, for all x,y in s, ‖f(y)−f(x)‖ ≤ C‖y−x‖.
Русский
Если s выпукло и функции f,g: E→G дифференцируемы с производными, ограниченными сверху на s величиной C, то f ограничено ляпшицевской константой C на s: для всех x,y∈s выполняется ‖f(y)−f(x)‖ ≤ C‖y−x‖.
LaTeX
$$$\text{If } s \text{ is convex } f,g: E\to G,\HasFDerivWithinAt \,f\, (f' x)\ sx, \text{ and } bound:\; \|f' x\| \le C \text{ for all } x\in s, \text{ then } \|f(y)-f(x)\| \le C \|y-x\| \text{ for all } x,y\in s.$$$
Lean4
/-- The mean value theorem on a convex set: if the derivative of a function is bounded by `C`, then
the function is `C`-Lipschitz. Version with `HasFDerivWithinAt`. -/
theorem norm_image_sub_le_of_norm_hasFDerivWithin_le (hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x)
(bound : ∀ x ∈ s, ‖f' x‖ ≤ C) (hs : Convex ℝ s) (xs : x ∈ s) (ys : y ∈ s) : ‖f y - f x‖ ≤ C * ‖y - x‖ :=
by
letI : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
letI : NormedSpace ℝ G := RestrictScalars.normedSpace ℝ 𝕜 G
set g := (AffineMap.lineMap x y : ℝ → E)
have segm : MapsTo g (Icc 0 1 : Set ℝ) s := hs.mapsTo_lineMap xs ys
have hD : ∀ t ∈ Icc (0 : ℝ) 1, HasDerivWithinAt (f ∘ g) (f' (g t) (y - x)) (Icc 0 1) t := fun t ht => by
simpa using ((hf (g t) (segm ht)).restrictScalars ℝ).comp_hasDerivWithinAt _ AffineMap.hasDerivWithinAt_lineMap segm
have bound : ∀ t ∈ Ico (0 : ℝ) 1, ‖f' (g t) (y - x)‖ ≤ C * ‖y - x‖ := fun t ht =>
le_of_opNorm_le _ (bound _ <| segm <| Ico_subset_Icc_self ht) _
simpa [g] using norm_image_sub_le_of_norm_deriv_le_segment_01' hD bound
