Theorems · Theorem · real analysis

IntervalIntegrable.intervalIntegrable_slope

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

If f is interval integrable 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 246 from the axioms · uses propext, Classical.choice, Quot.sound