English
If segment convex and ω continuous on s, then HasFDerivWithinAt for the segment-integral equals ω(a).
Русский
Если сегмент выпуклый и ω непрерывна на s, то HasFDerivWithinAt для сегментного интеграла равна ω(a).
LaTeX
$$$\\text{HasFDerivWithinAt}(\\int_{\\text{segment } a..·} ω(x)dx, ω(a), s, a)$$$
Lean4
/-- **Fundamental theorem of calculus, part 2**. This version assumes that `f` is continuous on the
interval and is differentiable off a countable set `s`.
See also `intervalIntegral.integral_eq_sub_of_hasDeriv_right` for a version that
only assumes right differentiability of `f`.
-/
theorem integral_eq_of_hasDerivAt_off_countable [CompleteSpace E] (f f' : ℝ → E) {a b : ℝ} {s : Set ℝ}
(hs : s.Countable) (Hc : ContinuousOn f [[a, b]]) (Hd : ∀ x ∈ Ioo (min a b) (max a b) \ s, HasDerivAt f (f' x) x)
(Hi : IntervalIntegrable f' volume a b) : ∫ x in a..b, f' x = f b - f a :=
by
rcases le_total a b with hab | hab
· simp only [uIcc_of_le hab, min_eq_left hab, max_eq_right hab] at *
exact integral_eq_of_hasDerivAt_off_countable_of_le f f' hab hs Hc Hd Hi
· simp only [uIcc_of_ge hab, min_eq_right hab, max_eq_left hab] at *
rw [intervalIntegral.integral_symm, neg_eq_iff_eq_neg, neg_sub]
exact integral_eq_of_hasDerivAt_off_countable_of_le f f' hab hs Hc Hd Hi.symm
