deriv_integral_of_tendsto_ae_left

English

If f is interval-integrable on [a,b] with ca, cb limits and suitable measurability, then F(u,v) = ∫_{u}^{v} f(x) dx is differentiable with derivative dF_{(a,b)}(h,k) = k cb − h ca.

Русский

Если f интегрируема на [a,b] с пределами ca и cb и подходящей меримостью, то F избегает дифференцирования: dF_{(a,b)}(h,k)=k cb−h ca.

LaTeX

$$$dF_{(a,b)}(h,k)=k c_b - h c_a.$$$

Lean4

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

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