theorem Chapter11.integ_of_monotone {a b : ℝ} {f : ℝ → ℝ} (hf : MonotoneOn f ↑(BoundedInterval.Icc a b)) : IntegrableOn f (BoundedInterval.Icc a b)

Proposition 11.6.1 (i)

theorem Chapter11.integ_of_antitone {a b : ℝ} {f : ℝ → ℝ} (hf : AntitoneOn f ↑(BoundedInterval.Icc a b)) : IntegrableOn f (BoundedInterval.Icc a b)

Proposition 11.6.1 (ii)

theorem Chapter11.integ_of_bdd_monotone {I : BoundedInterval} {f : ℝ → ℝ} (hbound : Chapter9.BddOn f ↑I) (hf : MonotoneOn f ↑I) : IntegrableOn f I

Corollary 11.6.3 (i) / Exercise 11.6.1

theorem Chapter11.integ_of_bdd_antitone {I : BoundedInterval} {f : ℝ → ℝ} (hbound : Chapter9.BddOn f ↑I) (hf : AntitoneOn f ↑I) : IntegrableOn f I

Corollary 11.6.3 (ii) / Exercise 11.6.1

theorem Chapter11.summable_iff_integ_of_antitone {f : ℝ → ℝ} (hnon : ∀ x ≥ 0, f x ≥ 0) (hf : AntitoneOn f (Set.Ici 0)) : (Summable fun (n : ℕ) => f ↑n) ↔ ∃ (M : ℝ), ∀ N ≥ 0, integ f (BoundedInterval.Icc 0 N) ≤ M

Proposition 11.6.4 (Integral test)