integral_derivWithin_Icc_of_contDiffOn_Icc

English

If f is C^1 on the union-interval uIcc(a,b), then ∫_a^b deriv f = f(b) - f(a).

Русский

Если f C^1 на uIcc(a,b), то интеграл производной равен f(b)-f(a).

LaTeX

$$$ContDiffOn \\mathbb{R} 1 f (uIcc(a,b)) \\Rightarrow \\int_a^b deriv f = f(b) - f(a)$$$

Lean4

/-- Fundamental theorem of calculus-2: If `f : ℝ → E` is `C^1` on `[a, b]`,
then `∫ y in a..b, derivWithin f (Icc a b) y` equals `f b - f a`. -/
theorem integral_derivWithin_Icc_of_contDiffOn_Icc (h : ContDiffOn ℝ 1 f (Icc a b)) (hab : a ≤ b) :
    ∫ x in a..b, derivWithin f (Icc a b) x = f b - f a :=
  by
  rw [← integral_deriv_of_contDiffOn_Icc h hab]
  rw [integral_of_le hab, integral_of_le hab]
  apply MeasureTheory.integral_congr_ae
  rw [← restrict_Ioo_eq_restrict_Ioc]
  filter_upwards [self_mem_ae_restrict measurableSet_Ioo] with x hx
  exact derivWithin_of_mem_nhds (Icc_mem_nhds hx.1 hx.2)

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