integral_hasDerivAt_of_tendsto_ae_left

English

Let f be integrable on [a,b]. If f has a finite limit c at a, then the derivative of u ↦ ∫_{u}^{b} f(x) dx at a equals −c.

Русский

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

LaTeX

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

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 `a`, then `u ↦ ∫ x in u..b, f x` has derivative `-c` at `a`. -/
theorem integral_hasDerivAt_of_tendsto_ae_left (hf : IntervalIntegrable f volume a b)
    (hmeas : StronglyMeasurableAtFilter f (𝓝 a)) (ha : Tendsto f (𝓝 a ⊓ ae volume) (𝓝 c)) :
    HasDerivAt (fun u => ∫ x in u..b, f x) (-c) a :=
  (integral_hasStrictDerivAt_of_tendsto_ae_left hf hmeas ha).hasDerivAt

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