Analysis I, Section 11.4: Basic properties of the Riemann integral

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:

• Basic properties of the Riemann integral.

theorem Chapter11.IntegrableOn.add {I : BoundedInterval} {f g : ℝ → ℝ} (hf : IntegrableOn f I) (hg : IntegrableOn g I) : IntegrableOn (f + g) I ∧ integ (f + g) I = integ f I + integ g I

Theorem 11.4.1(a) / Exercise 11.4.1

theorem Chapter11.IntegrableOn.smul {I : BoundedInterval} (c : ℝ) {f : ℝ → ℝ} (hf : IntegrableOn f I) : IntegrableOn (c • f) I ∧ integ (c • f) I = c * integ f I

Theorem 11.4.1(b) / Exercise 11.4.1

theorem Chapter11.IntegrableOn.neg {I : BoundedInterval} {f : ℝ → ℝ} (hf : IntegrableOn f I) : IntegrableOn (-f) I ∧ integ (-f) I = -integ f I

theorem Chapter11.IntegrableOn.sub {I : BoundedInterval} {f g : ℝ → ℝ} (hf : IntegrableOn f I) (hg : IntegrableOn g I) : IntegrableOn (f - g) I ∧ integ (f - g) I = integ f I - integ g I

Theorem 11.4.1(c) / Exercise 11.4.1

theorem Chapter11.IntegrableOn.nonneg {I : BoundedInterval} {f : ℝ → ℝ} (hf : IntegrableOn f I) (hf_nonneg : ∀ x ∈ I, 0 ≤ f x) : 0 ≤ integ f I

Theorem 11.4.1(d) / Exercise 11.4.1

theorem Chapter11.IntegrableOn.mono {I : BoundedInterval} {f g : ℝ → ℝ} (hf : IntegrableOn f I) (hg : IntegrableOn g I) (h : MajorizesOn g f I) : integ f I ≤ integ g I

Theorem 11.4.1(e) / Exercise 11.4.1

theorem Chapter11.IntegrableOn.const (c : ℝ) (I : BoundedInterval) : IntegrableOn (fun (x : ℝ) => c) I ∧ integ (fun (x : ℝ) => c) I = c * I.length

Theorem 11.4.1(f) / Exercise 11.4.1

theorem Chapter11.IntegrableOn.const' {I : BoundedInterval} {f : ℝ → ℝ} (hf : ConstantOn f ↑I) : IntegrableOn f I ∧ integ f I = constant_value_on f ↑I * I.length

Theorem 11.4.1(f) / Exercise 11.4.1

theorem Chapter11.IntegrableOn.of_extend {I J : BoundedInterval} (hIJ : I ⊆ J) {f : ℝ → ℝ} (h : IntegrableOn f I) : IntegrableOn (fun (x : ℝ) => if x ∈ I then f x else 0) J

Theorem 11.4.1 (g) / Exercise 11.4.1

theorem Chapter11.IntegrableOn.of_extend' {I J : BoundedInterval} (hIJ : I ⊆ J) {f : ℝ → ℝ} (h : IntegrableOn f I) : integ (fun (x : ℝ) => if x ∈ I then f x else 0) J = integ f I

Theorem 11.4.1 (g) / Exercise 11.4.1

theorem Chapter11.IntegrableOn.join {I J K : BoundedInterval} (hIJK : K.joins I J) {f : ℝ → ℝ} (h : IntegrableOn f K) : IntegrableOn f I ∧ IntegrableOn f J ∧ integ f K = integ f I + integ f J

Theorem 11.4.1 (h) (Laws of integration) / Exercise 11.4.1

theorem Chapter11.IntegrableOn.mono' {I J : BoundedInterval} (hIJ : J ⊆ I) {f : ℝ → ℝ} (h : IntegrableOn f I) : IntegrableOn f J

A variant of Theorem 11.4.1(h) that will be useful in later sections.

theorem Chapter11.IntegrableOn.eq {I J : BoundedInterval} (hIJ : J ⊆ I) (ha : J.a = I.a) (hb : J.b = I.b) {f : ℝ → ℝ} (h : IntegrableOn f I) : integ f J = integ f I

A further variant of Theorem 11.4.1(h) that will be useful in later sections.

theorem Chapter11.nonneg_of_le_const_mul_eps {x C : ℝ} (h : ∀ ε > 0, x ≤ C * ε) : x ≤ 0

A handy little lemma for "epsilon of room" type arguments

theorem Chapter11.IntegrableOn.max {I : BoundedInterval} {f g : ℝ → ℝ} (hf : IntegrableOn f I) (hg : IntegrableOn g I) : IntegrableOn (f ⊔ g) I

Theorem 11.4.3 (Max and min preserve integrability)

theorem Chapter11.IntegrableOn.min {I : BoundedInterval} {f g : ℝ → ℝ} (hf : IntegrableOn f I) (hg : IntegrableOn g I) : IntegrableOn (f ⊓ g) I

Theorem 11.4.5 / Exercise 11.4.3. The objective here is to create a shorter proof than the one above.

theorem Chapter11.IntegrableOn.abs {I : BoundedInterval} {f : ℝ → ℝ} (hf : IntegrableOn f I) : IntegrableOn |f| I

Corollary 11.4.4

theorem Chapter11.integ_of_mul_nonneg {I : BoundedInterval} {f g : ℝ → ℝ} (hf : IntegrableOn f I) (hg : IntegrableOn g I) (hf_nonneg : MajorizesOn f 0 I) (hg_nonneg : MajorizesOn g 0 I) : IntegrableOn (f * g) I

Theorem 11.4.5 (Products preserve Riemann integrability). It is convenient to first establish the non-negative case.

theorem Chapter11.integ_of_mul {I : BoundedInterval} {f g : ℝ → ℝ} (hf : IntegrableOn f I) (hg : IntegrableOn g I) : IntegrableOn (f * g) I

theorem Chapter11.IntegrableOn.split {I : BoundedInterval} {f : ℝ → ℝ} (hf : IntegrableOn f I) (P : Partition I) : integ f I = ∑ J ∈ P.intervals, integ f J

Exercise 11.4.2