norm_image_sub_le_of_norm_deriv_le_segment'

English

For a function f with right-derivative data on [a,b], the bound on the norm of the difference f(x)−f(a) is controlled by the bound on the derivative times (x−a).

Русский

Для функции f с данными правой производной на [a,b] ограничение нормы разности f(x)−f(a) задается произведением границы производной на (x−a).

LaTeX

$$$\displaystyle \|f(x) - f(a)\| \le C\,(x-a)\quad\text{for } x\in[a,b]$$$

Lean4

/-- A function on `[a, b]` with the norm of the derivative within `[a, b]`
bounded by `C` satisfies `‖f x - f a‖ ≤ C * (x - a)`, `HasDerivWithinAt`
version. -/
theorem norm_image_sub_le_of_norm_deriv_le_segment' {f' : ℝ → E} {C : ℝ}
    (hf : ∀ x ∈ Icc a b, HasDerivWithinAt f (f' x) (Icc a b) x) (bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ C) :
    ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ C * (x - a) :=
  by
  refine
    norm_image_sub_le_of_norm_deriv_right_le_segment (fun x hx => (hf x hx).continuousWithinAt) (fun x hx => ?_) bound
  exact (hf x <| Ico_subset_Icc_self hx).mono_of_mem_nhdsWithin (Icc_mem_nhdsGE_of_mem hx)

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