English
Let f be integrable on [a,b] and measurable with a finite limit ca at a and cb at b along given filters; then the derivative of F at (a,b) equals the map (h,k) ↦ k cb − h ca.
Русский
Пусть f интегрируема на [a,b] и пределы ca, cb достигаются вдоль данных фильтров; производная F в (a,b) равна L(h,k)=k cb − h ca.
LaTeX
$$$dF_{(a,b)}(h,k) = k\,c_b - h\,c_a.$$$
Lean4
/-- **Fundamental theorem of calculus-1**: if `f : ℝ → E` is integrable on `a..b` and `f` is
continuous at `a` and `b`, then `fderiv` derivative of `(u, v) ↦ ∫ x in u..v, f x` at `(a, b)`
equals `(u, v) ↦ v • cb - u • ca`. -/
theorem fderiv_integral (hf : IntervalIntegrable f volume a b) (hmeas_a : StronglyMeasurableAtFilter f (𝓝 a))
(hmeas_b : StronglyMeasurableAtFilter f (𝓝 b)) (ha : ContinuousAt f a) (hb : ContinuousAt f b) :
fderiv ℝ (fun p : ℝ × ℝ => ∫ x in p.1..p.2, f x) (a, b) =
(snd ℝ ℝ ℝ).smulRight (f b) - (fst ℝ ℝ ℝ).smulRight (f a) :=
(integral_hasFDerivAt hf hmeas_a hmeas_b ha hb).fderiv
