Theorems · Theorem · real analysis

intervalIntegral.sub_le_integral_of_hasDeriv_right_of_le_Ico

∀ {g' g φ : ℝ → ℝ} {a b : ℝ},
  a ≤ b →
    ContinuousOn g (Set.Icc a b) →
      (∀ x ∈ Set.Ico a b, HasDerivWithinAt g (g' x) (Set.Ioi x) x) →
        MeasureTheory.IntegrableOn φ (Set.Icc a b) MeasureTheory.volume →
          (∀ x ∈ Set.Ico a b, g' x ≤ φ x) → g b - g a ≤ ∫ (y : ℝ) in a..b, φ y

Hard part of FTC-2 for integrable derivatives, real-valued functions: one has g b - g a ≤ ∫ y in a..b, g' y when g' is integrable. Auxiliary lemma in the proof of integral_eq_sub_of_hasDeriv_right_of_le. We give the slightly more general version that g b - g a ≤ ∫ y in a..b, φ y when g' ≤ φ and φ is integrable (even if g' is not known to be integrable). Version assuming that g is differentiable on [a, b).

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Cited by

1 results in Mathlib

Foundations

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