Theorems · Theorem · measure theory

MeasureTheory.integral_Iic_of_hasDerivAt_of_tendsto

∀ {E : Type u_1} {f f' : ℝ → E} {a : ℝ} {m : E} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E],
  ContinuousWithinAt f (Set.Iic a) a →
    (∀ x ∈ Set.Iio a, HasDerivAt f (f' x) x) →
      MeasureTheory.IntegrableOn f' (Set.Iic a) MeasureTheory.volume →
        Filter.Tendsto f Filter.atBot (nhds m) → ∫ (x : ℝ) in Set.Iic a, f' x = f a - m

Fundamental theorem of calculus-2, on semi-infinite intervals (-∞, a). When a function has a limit m at -∞, and its derivative is integrable, then the integral of the derivative on (-∞, a) is f a - m. Version assuming differentiability on (-∞, a) and continuity at a⁻. Note that such a function always has a limit at minus infinity, see tendsto_limUnder_of_hasDerivAt_of_integrableOn_Iic.

Defined in

Mathlib.MeasureTheory.Integral.IntegralEqImproper

Cited by

3 results in Mathlib

Foundations

Depth 267 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace