enorm_sub_le_lintegral_derivWithin_Icc_of_contDiffOn_Icc

English

If f is C^1 on Icc(a,b) and a ≤ b, then ||f(b) − f(a)|| ≤ ∫_a^b ||deriv f(x)|| dx, where deriv f is the derivative on the interval.

Русский

Если f ∈ C^1 на Icc(a,b) и a ≤ b, то ||f(b) − f(a)|| ≤ ∫_a^b ||f'(x)|| dx.

LaTeX

$$$\\|f(b) - f(a)\\| \\le \\int_{a}^{b} \\|f'(x)\\| \\, dx$$$

Lean4

theorem enorm_sub_le_lintegral_derivWithin_Icc_of_contDiffOn_Icc (h : ContDiffOn ℝ 1 f (Icc a b)) (hab : a ≤ b) :
    ‖f b - f a‖ₑ ≤ ∫⁻ x in Icc a b, ‖derivWithin f (Icc a b) x‖ₑ :=
  by
  apply (enorm_sub_le_lintegral_deriv_of_contDiffOn_Icc h hab).trans_eq
  apply lintegral_congr_ae
  rw [← restrict_Ioo_eq_restrict_Icc]
  filter_upwards [self_mem_ae_restrict measurableSet_Ioo] with x hx
  rw [derivWithin_of_mem_nhds (Icc_mem_nhds hx.1 hx.2)]

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