integral_hasStrictDerivAt_left — Mathlib

English

If f is integrable on [a,b] and f is continuous at a, then the map u ↦ ∫_{u}^{b} f(x) dx has a strict derivative at a equal to −f(a).

Русский

Если f интегрируема на [a,b] и непрерывна в a, то u ↦ ∫_{u}^{b} f(x) dx имеет строгую производную в a, равную −f(a).

LaTeX

$$$\\text{Deriv}_{a}^{-} \\left( u \\mapsto \\int_{u}^{b} f(x)dx \\right) = -f(a).$$$

Lean4

/-- **Fundamental theorem of calculus-1**, strict differentiability in the left endpoint.

If `f : ℝ → E` is integrable on `a..b` and `f` is continuous at `a`, then `u ↦ ∫ x in u..b, f x` has
derivative `-f a` at `a` in the sense of strict differentiability. -/
theorem integral_hasStrictDerivAt_left (hf : IntervalIntegrable f volume a b)
    (hmeas : StronglyMeasurableAtFilter f (𝓝 a)) (ha : ContinuousAt f a) :
    HasStrictDerivAt (fun u => ∫ x in u..b, f x) (-f a) a := by
  simpa only [← integral_symm] using (integral_hasStrictDerivAt_right hf.symm hmeas ha).fun_neg

Похожие утверждения