Analysis I, Section 11.6: Riemann integrability of monotone functions #
I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.
Main constructions and results of this section:
- Riemann integrability of monotone functions.
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))
:
Proposition 11.6.4 (Integral test)