Аналіз I, Розділ 11.6: Ріманова інтегровність монотонних функцій

Я (прим. перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним підходом Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підправити", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Основні конструкції та результати цього розділу:

• Ріманова інтегровність монотонних функцій.

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

Твердження 11.6.1

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

Твердження 11.6.1

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

Наслідок 11.6.3 / Вправа 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

Твердження 11.6.4 (Ознака інтегрування)