Theorems · Theorem · measure theory

MeasureTheory.integral_eq_zero_of_hasDerivAt_of_integrable

∀ {E : Type u_1} {f f' : ℝ → E} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E],
  (∀ (x : ℝ), HasDerivAt f (f' x) x) →
    MeasureTheory.Integrable f' MeasureTheory.volume →
      MeasureTheory.Integrable f MeasureTheory.volume → ∫ (x : ℝ), f' x = 0

If a function and its derivative are integrable on the real line, then the integral of the derivative is zero.

Defined in

Mathlib.MeasureTheory.Integral.IntegralEqImproper

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace