norm_image_sub_le_of_norm_fderivWithin_le'

English

A variant of the mean value bound on a convex set when the derivative within s is close to φ, yielding the same inequality as above.

Русский

Вариант неравенства среднего значения на выпуклом множестве при наличии $f' - φ$ малого отклонения внутри $s$, дающий неравенство аналогично предыдущему.

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 `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 - φ (y - x)‖ ≤ C * ‖y - x‖ :=
  hs.norm_image_sub_le_of_norm_hasFDerivWithin_le' (fun x hx => (hf x hx).hasFDerivWithinAt) bound xs ys

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