integral_hasStrictDerivAt_right — Mathlib

English

If f is integrable on [a,b] and has a finite limit c at a, then the map H(u) = ∫_{u}^{b} f(x) dx has derivative −c at a.

Русский

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

LaTeX

$$$H(u) = \\int_{u}^{b} f(x)\\,dx,\\quad H'(a)= -c.$$$

Lean4

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

If `f : ℝ → E` is integrable on `a..b` and `f` is continuous at `b`, then `u ↦ ∫ x in a..u, f x` has
derivative `f b` at `b` in the sense of strict differentiability. -/
theorem integral_hasStrictDerivAt_right (hf : IntervalIntegrable f volume a b)
    (hmeas : StronglyMeasurableAtFilter f (𝓝 b)) (hb : ContinuousAt f b) :
    HasStrictDerivAt (fun u => ∫ x in a..u, f x) (f b) b :=
  integral_hasStrictDerivAt_of_tendsto_ae_right hf hmeas (hb.mono_left inf_le_left)

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