English
Let f be interval-integrable on [a,b] and measurable with respect to chosen filters so that f tends to ca, cb along la, lb; then HasFDerivWithinAt of F with derivative L(h,k) as above holds within s × t around (a,b).
Русский
Пусть f интегрируемо на [a,b] и пределы ca, cb достигаются вдоль заданных фильтров la, lb; тогда HasFDerivWithinAt F с производной L в окрестности (a,b верна внутри s × t.
LaTeX
$$$F(u,v)=\\int_{u}^{v} f(x)dx,\\ HasFDerivWithinAt F (s \\times t) \\bigl(L\\bigr) (a,b).$$$
Lean4
/-- **Fundamental theorem of calculus-1**: if `f : ℝ → E` is integrable on `a..b` and `f x` has
finite limits `ca` and `cb` almost surely as `x` tends to `a` and `b`, respectively, then
`(u, v) ↦ ∫ x in u..v, f x` has derivative `(u, v) ↦ v • cb - u • ca` at `(a, b)`. -/
theorem integral_hasFDerivAt_of_tendsto_ae (hf : IntervalIntegrable f volume a b)
(hmeas_a : StronglyMeasurableAtFilter f (𝓝 a)) (hmeas_b : StronglyMeasurableAtFilter f (𝓝 b))
(ha : Tendsto f (𝓝 a ⊓ ae volume) (𝓝 ca)) (hb : Tendsto f (𝓝 b ⊓ ae volume) (𝓝 cb)) :
HasFDerivAt (fun p : ℝ × ℝ => ∫ x in p.1..p.2, f x) ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (a, b) :=
(integral_hasStrictFDerivAt_of_tendsto_ae hf hmeas_a hmeas_b ha hb).hasFDerivAt
