Some properties of the interval integral of fun x ↦ slope f x (x + c), given a constant c : ℝ

This file proves that:

• IntervalIntegrable.intervalIntegrable_slope: 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.
• MonotoneOn.intervalIntegrable_slope: 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.
• MonotoneOn.intervalIntegral_slope_le: If f is monotone on a..(b + c) where a ≤ b and 0 ≤ c, then the interval integral of fun x ↦ slope f x (x + c) on a..b is at most f (b + c) - f a.

Tags

interval integrable, interval integral, monotone, slope

theorem IntervalIntegrable.intervalIntegrable_slope {f : ℝ → ℝ} {a b c : ℝ} (hf : IntervalIntegrable f MeasureTheory.volume a (b + c)) (hab : a ≤ b) (hc : 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.

theorem MonotoneOn.intervalIntegrable_slope {f : ℝ → ℝ} {a b c : ℝ} (hf : MonotoneOn f (Set.Icc a (b + c))) (hab : a ≤ b) (hc : 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.

theorem MonotoneOn.intervalIntegral_slope_le {f : ℝ → ℝ} {a b c : ℝ} (hf : MonotoneOn f (Set.Icc a (b + c))) (hab : a ≤ b) (hc : 0 ≤ c) : ∫ (x : ℝ) in a..b, slope f x (x + c) ≤ f (b + c) - f a

If f is monotone on a..(b + c) where a ≤ b and 0 ≤ c, then the interval integral of fun x ↦ slope f x (x + c) on a..b is at most f (b + c) - f a.