Theorems · Theorem · real analysis

intervalIntegral.integrableOn_deriv_right_of_nonneg

∀ {g' g : ℝ → ℝ} {a b : ℝ},
  ContinuousOn g (Set.Icc a b) →
    (∀ x ∈ Set.Ioo a b, HasDerivWithinAt g (g' x) (Set.Ioi x) x) →
      (∀ x ∈ Set.Ioo a b, 0 ≤ g' x) → MeasureTheory.IntegrableOn g' (Set.Ioc a b) MeasureTheory.volume

When the right derivative of a function is nonnegative, then it is automatically integrable.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Cited by

1 results in Mathlib

Foundations

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