English
Let f be interval-integrable on [a,b] with limits ca, cb as x→a,b (ae). Then the map F(u,v) = ∫_{u}^{v} f(x) dx has a Frechet derivative at (a,b) given by the linear map (h,k) ↦ k cb − h ca.
Русский
Пусть f интегрируема на [a,b] и стремится к ca, cb при x→a,b (ae). Тогда F(u,v)=∫_{u}^{v} f(x) dx имеет Фреше- производную в (a,b) равную L(h,k)=k cb − h ca.
LaTeX
$$$F(u,v)=\\int_{u}^{v} f(x)\\,dx,\\quad dF_{(a,b)}(h,k)=k\,c_b - h\,c_a.$$$
Lean4
/-- **Fundamental theorem of calculus-1**, strict differentiability in the left endpoint.
If `f : ℝ → E` is integrable on `a..b` and `f x` has a finite limit `c` almost surely at `a`, then
`u ↦ ∫ x in u..b, f x` has derivative `-c` at `a` in the sense of strict differentiability. -/
theorem integral_hasStrictDerivAt_of_tendsto_ae_left (hf : IntervalIntegrable f volume a b)
(hmeas : StronglyMeasurableAtFilter f (𝓝 a)) (ha : Tendsto f (𝓝 a ⊓ ae volume) (𝓝 c)) :
HasStrictDerivAt (fun u => ∫ x in u..b, f x) (-c) a := by
simpa only [← integral_symm] using (integral_hasStrictDerivAt_of_tendsto_ae_right hf.symm hmeas ha).fun_neg
