Theorems · Theorem · real analysis

MonotoneOn.intervalIntegrable_slope

∀ {f : ℝ → ℝ} {a b c : ℝ},
  MonotoneOn f (Set.Icc a (b + c)) →
    a ≤ b → 0 ≤ c → IntervalIntegrable (fun x => slope f x (x + c)) MeasureTheory.volume a b

If f is monotone on a..(b + c) where a ≤ b and 0 ≤ c, then fun x ↦ slope f x (x + c) is interval integrable on a..b.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope

Cited by

1 results in Mathlib

Foundations

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