English
Assume the same as above but with f(a) and f(b) being the endpoint values; then the derivative of F at (a,b) is the linear map (h,k) ↦ k f(b) − h f(a).
Русский
При тех же предпосылках пределы f в концах дают производную отображения F в точке (a,b): dF_{(a,b)}(h,k) = k f(b) − h f(a).
LaTeX
$$$F(u,v) = \\int_{u}^{v} f(x)\\,dx,\\quad F:\\mathbb{R}^{2}\\to E,$\n$F\\text{ строго дифференцируема в }(a,b)\\text{ и } dF_{(a,b)}(h,k) = k\,f(b) - h\,f(a).$$$
Lean4
/-- **Fundamental theorem of calculus-1**, strict differentiability in both endpoints.
If `f : ℝ → E` is integrable on `a..b` and `f` is continuous at `a` and `b`, then
`(u, v) ↦ ∫ x in u..v, f x` has derivative `(u, v) ↦ v • cb - u • ca` at `(a, b)` in the sense of
strict differentiability. -/
theorem integral_hasStrictFDerivAt (hf : IntervalIntegrable f volume a b) (hmeas_a : StronglyMeasurableAtFilter f (𝓝 a))
(hmeas_b : StronglyMeasurableAtFilter f (𝓝 b)) (ha : ContinuousAt f a) (hb : ContinuousAt f b) :
HasStrictFDerivAt (fun p : ℝ × ℝ => ∫ x in p.1..p.2, f x)
((snd ℝ ℝ ℝ).smulRight (f b) - (fst ℝ ℝ ℝ).smulRight (f a)) (a, b) :=
integral_hasStrictFDerivAt_of_tendsto_ae hf hmeas_a hmeas_b (ha.mono_left inf_le_left) (hb.mono_left inf_le_left)
