English
Let f be interval-integrable on [a,b], and measurable with respect to la, lb; then HasFDerivWithinAt of F with derivative L holds within s × t around (a,b).
Русский
Пусть f интегрируемо на [a,b], и относится к фильтрам la, lb; тогда HasFDerivWithinAt F с производной L выполняется внутри s × t около (a,b).
LaTeX
$$$\\text{HasFDerivWithinAt}(F, L, s \\timesˢ t, (a,b)).$$$
Lean4
/-- **Fundamental theorem of calculus-1**: 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)`. -/
theorem integral_hasFDerivAt (hf : IntervalIntegrable f volume a b) (hmeas_a : StronglyMeasurableAtFilter f (𝓝 a))
(hmeas_b : StronglyMeasurableAtFilter f (𝓝 b)) (ha : ContinuousAt f a) (hb : ContinuousAt f b) :
HasFDerivAt (fun p : ℝ × ℝ => ∫ x in p.1..p.2, f x) ((snd ℝ ℝ ℝ).smulRight (f b) - (fst ℝ ℝ ℝ).smulRight (f a))
(a, b) :=
(integral_hasStrictFDerivAt hf hmeas_a hmeas_b ha hb).hasFDerivAt
