English
Let f: R → E be integrable on [a,b] and suppose f is left- or right-continuous at a. Then the map F: R → E given by F(u) = ∫ from x = u to b of f(x) dx has left (resp. right) derivative at a equal to −f(a).
Русский
Пусть f: ℝ → E интегрируема на [a,b] и при a слева или справа непрерывна; тогда функция F(u) = ∫_{u}^{b} f(x) dx имеет слева (или справа) производную в точке a равную −f(a).
LaTeX
$$$F(u)=\\int_{u}^{b} f(x)\\,dx\\quad\\Rightarrow\\quad F'(a^-)=-f(a) \\quad(\\text{или }F'(a^+)= -f(a)\\text{ в зависимости от стороны непрерывности at }a).$$
Lean4
/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` is continuous
from the left or from the right at `a`, then `u ↦ ∫ x in u..b, f x` has left (resp., right)
derivative `-f a` at `a`. -/
theorem integral_hasDerivWithinAt_left (hf : IntervalIntegrable f volume a b) {s t : Set ℝ}
[FTCFilter a (𝓝[s] a) (𝓝[t] a)] (hmeas : StronglyMeasurableAtFilter f (𝓝[t] a)) (ha : ContinuousWithinAt f t a) :
HasDerivWithinAt (fun u => ∫ x in u..b, f x) (-f a) s a :=
integral_hasDerivWithinAt_of_tendsto_ae_left hf hmeas (ha.mono_left inf_le_left)
