integral_hasDerivAt_of_tendsto_ae_right

English

If f is integrable on [a,b] with limits ca, cb, then fderiv of the map F(u,v) = ∫_u^v f(x) dx equals the linear map L(h,k) = k cb − h ca.

Русский

Если f интегрируема на [a,b] с пределами ca, cb, то fderiv от F(u,v) равна линейному отображению L(h,k) = k cb − h ca.

LaTeX

$$$fderiv\\,F_{(a,b)}(h,k)=k\\,c_b - h\\,c_a.$$$

Lean4

/-- **Fundamental theorem of calculus-1**: if `f : ℝ → E` is integrable on `a..b` and `f x` has a
finite limit `c` almost surely at `b`, then `u ↦ ∫ x in a..u, f x` has derivative `c` at `b`. -/
theorem integral_hasDerivAt_of_tendsto_ae_right (hf : IntervalIntegrable f volume a b)
    (hmeas : StronglyMeasurableAtFilter f (𝓝 b)) (hb : Tendsto f (𝓝 b ⊓ ae volume) (𝓝 c)) :
    HasDerivAt (fun u => ∫ x in a..u, f x) c b :=
  (integral_hasStrictDerivAt_of_tendsto_ae_right hf hmeas hb).hasDerivAt

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