English
If f is integrable on [a,b] and f tends to cb at b, then the one-variable function G(u) = ∫_{a}^{u} f(x) dx is strictly differentiable at u = b with derivative cb.
Русский
Если f интегрируема на [a,b] и имеет предел cb при x→b, то G(u)=∫_{a}^{u} f(x)dx строго дифференцируема в u=b, производная cb.
LaTeX
$$$G(u) = \\int_{a}^{u} f(x)\\,dx,\\quad G\\text{ strictly differentiable at } u=b\\ \\text{ with } G'(b)=c_b.$$$
Lean4
/-- **Fundamental theorem of calculus-1**, strict differentiability in the right endpoint.
If `f : ℝ → E` is integrable on `a..b` and `f x` has a finite limit `c` almost surely at `b`, then
`u ↦ ∫ x in a..u, f x` has derivative `c` at `b` in the sense of strict differentiability. -/
theorem integral_hasStrictDerivAt_of_tendsto_ae_right (hf : IntervalIntegrable f volume a b)
(hmeas : StronglyMeasurableAtFilter f (𝓝 b)) (hb : Tendsto f (𝓝 b ⊓ ae volume) (𝓝 c)) :
HasStrictDerivAt (fun u => ∫ x in a..u, f x) c b :=
.of_isLittleO <|
integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right hf hmeas hb continuousAt_snd continuousAt_fst
