Theorems · Theorem · measure theory

MeasureTheory.integral_Ioi_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.Ici a) a →
    (∀ x ∈ Set.Ioi a, HasDerivAt f (f' x) x) →
      MeasureTheory.IntegrableOn f' (Set.Ioi a) MeasureTheory.volume →
        Filter.Tendsto f Filter.atTop (nhds m) → ∫ (x : ℝ) in Set.Ioi a, f' x = m - f a

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

Defined in

Mathlib.MeasureTheory.Integral.IntegralEqImproper

Cited by

5 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace