norm_image_sub_le_of_norm_deriv_le_segment_01'

English

On the unit interval, if the derivative is bounded by C in norm, then the difference f(1)−f(0) has norm at most C.

Русский

На единичном отрезке, если производная ограничена по норме C, то разность f(1)−f(0) имеет норму не более C.

LaTeX

$$$\displaystyle \|f(1) - f(0)\| \le C$$$

Lean4

/-- A function on `[0, 1]` with the norm of the derivative within `[0, 1]`
bounded by `C` satisfies `‖f 1 - f 0‖ ≤ C`, `HasDerivWithinAt`
version. -/
theorem norm_image_sub_le_of_norm_deriv_le_segment_01' {f' : ℝ → E} {C : ℝ}
    (hf : ∀ x ∈ Icc (0 : ℝ) 1, HasDerivWithinAt f (f' x) (Icc (0 : ℝ) 1) x) (bound : ∀ x ∈ Ico (0 : ℝ) 1, ‖f' x‖ ≤ C) :
    ‖f 1 - f 0‖ ≤ C := by
  simpa only [sub_zero, mul_one] using
    norm_image_sub_le_of_norm_deriv_le_segment' hf bound 1 (right_mem_Icc.2 zero_le_one)

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