English
Let f be measurable and integrable on [a,b]. Then for any s,t sets and suitable FTCFilteres, HasFDerivWithinAt holds with derivative L.
Русский
Пусть f измерима и интегрируема на [a,b]. Тогда для любых подходящих множеств s,t выполняется HasFDerivWithinAt с производной L.
LaTeX
$$$\\text{HasFDerivWithinAt}(F,L,s\\times t)\\;{(a,b)}$$$
Lean4
/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` has a finite
limit `c` almost surely as `x` tends to `b` from the right or from the left,
then `u ↦ ∫ x in a..u, f x` has right (resp., left) derivative `c` at `b`. -/
theorem integral_hasDerivWithinAt_of_tendsto_ae_right (hf : IntervalIntegrable f volume a b) {s t : Set ℝ}
[FTCFilter b (𝓝[s] b) (𝓝[t] b)] (hmeas : StronglyMeasurableAtFilter f (𝓝[t] b))
(hb : Tendsto f (𝓝[t] b ⊓ ae volume) (𝓝 c)) : HasDerivWithinAt (fun u => ∫ x in a..u, f x) c s b :=
.of_isLittleO <|
integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right hf hmeas hb
(tendsto_const_pure.mono_right FTCFilter.pure_le) tendsto_id
