f' is interval integrable for certain classes of functions f

This file proves that:

• MonotoneOn.intervalIntegrable_deriv: If f is monotone on a..b, then f' is interval integrable on a..b.
• MonotoneOn.intervalIntegral_deriv_mem_uIcc: If f is monotone on a..b, then the integral of f' on a..b is in uIcc 0 (f b - f a).
• BoundedVariationOn.intervalIntegrable_deriv: If f has bounded variation on a..b, then f' is interval integrable on a..b.
• AbsolutelyContinuousOnInterval.intervalIntegrable_deriv: If f is absolutely continuous on a..b, then f' is interval integrable on a..b.

Tags

interval integrable, monotone, bounded variation, absolutely continuous

theorem MonotoneOn.exists_tendsto_deriv_liminf_lintegral_enorm_le {f : ℝ → ℝ} {a b : ℝ} (hab : a ≤ b) (hf : MonotoneOn f (Set.Icc a b)) : ∃ (G : ℕ → ℝ → ℝ), (∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict (Set.Icc a b), Filter.Tendsto (fun (n : ℕ) => G n x) Filter.atTop (nhds (deriv f x))) ∧ (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (G n) (MeasureTheory.volume.restrict (Set.Icc a b))) ∧ Filter.liminf (fun (n : ℕ) => ∫⁻ (x : ℝ) in Set.Icc a b, ‖G n x‖ₑ) Filter.atTop ≤ ENNReal.ofReal (f b - f a)

If f is monotone on [a, b], then f' is the limit of G n a.e. on [a, b], where each G n is AEStronglyMeasurable and the liminf of the lower Lebesgue integral of ‖G n ·‖ₑ is at most f b - f a.

theorem MonotoneOn.intervalIntegrable_deriv {f : ℝ → ℝ} {a b : ℝ} (hf : MonotoneOn f (Set.uIcc a b)) : IntervalIntegrable (deriv f) MeasureTheory.volume a b

If f is monotone on a..b, then f' is interval integrable on a..b.

theorem MonotoneOn.intervalIntegral_deriv_mem_uIcc {f : ℝ → ℝ} {a b : ℝ} (hf : MonotoneOn f (Set.uIcc a b)) : ∫ (x : ℝ) in a..b, deriv f x ∈ Set.uIcc 0 (f b - f a)

If f is monotone on a..b, then f' is interval integrable on a..b and the integral of f' on a..b is in between 0 and f b - f a.

theorem BoundedVariationOn.intervalIntegrable_deriv {f : ℝ → ℝ} {a b : ℝ} (hf : BoundedVariationOn f (Set.uIcc a b)) : IntervalIntegrable (deriv f) MeasureTheory.volume a b

If f has bounded variation on uIcc a b, then f' is interval integrable on a..b.

theorem AbsolutelyContinuousOnInterval.intervalIntegrable_deriv {f : ℝ → ℝ} {a b : ℝ} (hf : AbsolutelyContinuousOnInterval f a b) : IntervalIntegrable (deriv f) MeasureTheory.volume a b

If f is absolutely continuous on uIcc a b, then f' is interval integrable on a..b.