Analysis I, Section 11.5: Riemann integrability of continuous 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 uniformly continuous functions.
• Riemann integrability of bounded continuous functions.

theorem Chapter11.integ_of_uniform_cts {I : BoundedInterval} {f : ℝ → ℝ} (hf : UniformContinuousOn f ↑I) : IntegrableOn f I

Theorem 11.5.1

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

Corollary 11.5.2

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

Proposition 11.5.3

@[reducible, inline]

abbrev Chapter11.PiecewiseContinuousOn (f : ℝ → ℝ) (I : BoundedInterval) : Prop

Definition 11.5.4

Equations

• Chapter11.PiecewiseContinuousOn f I = ∃ (P : Chapter11.Partition I), ∀ J ∈ P.intervals, ContinuousOn f ↑J

@[reducible, inline]

noncomputable abbrev Chapter11.f_11_5_5 : ℝ → ℝ

Example 11.5.5

Equations

• Chapter11.f_11_5_5 x = if x < 2 then x ^ 2 else if x = 2 then 7 else x ^ 3

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

Proposition 11.5.6 / Exercise 11.5.1

theorem Chapter11.integ_zero {a b : ℝ} (hab : a ≤ b) (f : ℝ → ℝ) (hf : ContinuousOn f ↑(BoundedInterval.Icc a b)) (hnonneg : MajorizesOn f (fun (x : ℝ) => 0) (BoundedInterval.Icc a b)) (hinteg : integ f (BoundedInterval.Icc a b) = 0) (x : ℝ) : x ∈ BoundedInterval.Icc a b → f x = 0

Exercise 11.5.2