English
If f has a right derivative f'(x) on [a,b] and f' is integrable on [a,b], then ∫ f' = f(b) − f(a).
Русский
Если f имеет правую производную на [a,b] и f' интегрируемо на [a,b], то интеграл от f' равен разности концов: f(b)−f(a).
LaTeX
$$$\\int_{a}^{b} f'(y)\\,dy = f(b)-f(a)$$$
Lean4
/-- Fundamental theorem of calculus-2: If `f : ℝ → E` is continuous on `[a, b]` and
has a right derivative at `f' x` for all `x` in `[a, b)`, and `f'` is integrable on `[a, b]` then
`∫ y in a..b, f' y` equals `f b - f a`. -/
theorem integral_eq_sub_of_hasDeriv_right (hcont : ContinuousOn f (uIcc a b))
(hderiv : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x)
(hint : IntervalIntegrable f' volume a b) : ∫ y in a..b, f' y = f b - f a :=
by
rcases le_total a b with hab | hab
· simp only [uIcc_of_le, min_eq_left, max_eq_right, hab] at hcont hderiv hint
apply integral_eq_sub_of_hasDeriv_right_of_le hab hcont hderiv hint
· simp only [uIcc_of_ge, min_eq_right, max_eq_left, hab] at hcont hderiv
rw [integral_symm, integral_eq_sub_of_hasDeriv_right_of_le hab hcont hderiv hint.symm, neg_sub]
