norm_image_sub_le_of_norm_fderiv_le'

English

A bound on the difference $f(y)-f(x)-φ(y-x)$ in terms of a bound on the derivative within a convex set, expressed with a prime variant.

Русский

Пределы на разность $f(y)-f(x)-φ(y-x)$ в терминах ограниченности производной внутри выпуклого множества, выражение варианта.

LaTeX

$$$\forall x,y\in s:\ ‖f(y)-f(x)-φ(y-x)‖ ≤ C\,‖y-x‖.$$$

Lean4

/-- Variant of the mean value inequality on a convex set. Version with `fderiv`. -/
theorem norm_image_sub_le_of_norm_fderiv_le' (hf : ∀ x ∈ s, DifferentiableAt 𝕜 f x)
    (bound : ∀ x ∈ s, ‖fderiv 𝕜 f x - φ‖ ≤ C) (hs : Convex ℝ s) (xs : x ∈ s) (ys : y ∈ s) :
    ‖f y - f x - φ (y - x)‖ ≤ C * ‖y - x‖ :=
  hs.norm_image_sub_le_of_norm_hasFDerivWithin_le' (fun x hx => (hf x hx).hasFDerivAt.hasFDerivWithinAt) bound xs ys

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