English
If f is C^1 on [a,b], then ∫_a^b deriv f = f(b) - f(a).
Русский
Если f имеет непрерывную производную на [a,b], то интеграл от производной равен разности f(b) - f(a).
LaTeX
$$$\\int_a^b \\mathrm{deriv}\n f = f(b) - f(a)$ under ContDiffOn assumptions.$$
Lean4
/-- Fundamental theorem of calculus-2: If `f : ℝ → E` is `C^1` on `[a, b]`,
then `∫ y in a..b, deriv f y` equals `f b - f a`. -/
theorem integral_deriv_of_contDiffOn_Icc (h : ContDiffOn ℝ 1 f (Icc a b)) (hab : a ≤ b) :
∫ x in a..b, deriv f x = f b - f a := by
rcases hab.eq_or_lt with rfl | h'ab
· simp
apply integral_eq_sub_of_hasDerivAt_of_le hab h.continuousOn
· intro x hx
apply DifferentiableAt.hasDerivAt
apply ((h x ⟨hx.1.le, hx.2.le⟩).differentiableWithinAt le_rfl).differentiableAt
exact Icc_mem_nhds hx.1 hx.2
· have := (h.derivWithin (m := 0) (uniqueDiffOn_Icc h'ab) (by simp)).continuousOn
apply (this.intervalIntegrable_of_Icc (μ := volume) hab).congr_ae
simp only [hab, uIoc_of_le]
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)
