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

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

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 / 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

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

Proposition 11.6.4 (Integral test)