Documentation

Analysis.Section_11_3

Analysis I, Section 11.3: Upper and lower Riemann integrals #

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:

The upper and lower Riemann integral; the Riemann integral.
Upper and lower Riemann sums.

@[reducible, inline]

abbrev Chapter11.MajorizesOn (g f : ℝ → ℝ) (I : BoundedInterval) :

Definition 11.3.1 (Majorization of functions)

Equations

Chapter11.MajorizesOn g f I = ∀ x ∈ ↑I, f x ≤ g x

Instances For

@[reducible, inline]

abbrev Chapter11.MinorizesOn (g f : ℝ → ℝ) (I : BoundedInterval) :

Equations

Chapter11.MinorizesOn g f I = ∀ x ∈ ↑I, g x ≤ f x

Instances For

theorem Chapter11.MinorizesOn.iff (g f : ℝ → ℝ) (I : BoundedInterval) :

MinorizesOn g f I ↔ MajorizesOn f g I

@[reducible, inline]

noncomputable abbrev Chapter11.upper_integral (f : ℝ → ℝ) (I : BoundedInterval) :

Definition 11.3.2 (Uppper and lower Riemann integrals )

Equations

Chapter11.upper_integral f I = sInf ((fun (x : ℝ → ℝ) => Chapter11.PiecewiseConstantOn.integ x I) '' {g : ℝ → ℝ | Chapter11.MajorizesOn g f I ∧ Chapter11.PiecewiseConstantOn g I})

Instances For

@[reducible, inline]

noncomputable abbrev Chapter11.lower_integral (f : ℝ → ℝ) (I : BoundedInterval) :

Equations

Chapter11.lower_integral f I = sSup ((fun (x : ℝ → ℝ) => Chapter11.PiecewiseConstantOn.integ x I) '' {g : ℝ → ℝ | Chapter11.MinorizesOn g f I ∧ Chapter11.PiecewiseConstantOn g I})

Instances For

theorem Chapter11.upper_integral_congr {f g : ℝ → ℝ} {I : BoundedInterval} (h : Set.EqOn f g ↑I) :

upper_integral f I = upper_integral g I

theorem Chapter11.lower_integral_congr {f g : ℝ → ℝ} {I : BoundedInterval} (h : Set.EqOn f g ↑I) :

lower_integral f I = lower_integral g I

theorem Chapter11.integral_bound_upper_of_bounded {f : ℝ → ℝ} {M : ℝ} {I : BoundedInterval} (h : ∀ x ∈ ↑I, |f x| ≤ M) :

M * I.length ∈ (fun (x : ℝ → ℝ) => PiecewiseConstantOn.integ x I) '' {g : ℝ → ℝ | MajorizesOn g f I ∧ PiecewiseConstantOn g I}

theorem Chapter11.integral_bound_lower_of_bounded {f : ℝ → ℝ} {M : ℝ} {I : BoundedInterval} (h : ∀ x ∈ ↑I, |f x| ≤ M) :

-M * I.length ∈ (fun (x : ℝ → ℝ) => PiecewiseConstantOn.integ x I) '' {g : ℝ → ℝ | MinorizesOn g f I ∧ PiecewiseConstantOn g I}

theorem Chapter11.integral_bound_upper_nonempty {f : ℝ → ℝ} {I : BoundedInterval} (h : Chapter9.BddOn f ↑I) :

((fun (x : ℝ → ℝ) => PiecewiseConstantOn.integ x I) '' {g : ℝ → ℝ | MajorizesOn g f I ∧ PiecewiseConstantOn g I}).Nonempty

theorem Chapter11.integral_bound_lower_nonempty {f : ℝ → ℝ} {I : BoundedInterval} (h : Chapter9.BddOn f ↑I) :

((fun (x : ℝ → ℝ) => PiecewiseConstantOn.integ x I) '' {g : ℝ → ℝ | MinorizesOn g f I ∧ PiecewiseConstantOn g I}).Nonempty

theorem Chapter11.integral_bound_lower_le_upper {f : ℝ → ℝ} {I : BoundedInterval} {a b : ℝ} (ha : a ∈ (fun (x : ℝ → ℝ) => PiecewiseConstantOn.integ x I) '' {g : ℝ → ℝ | MajorizesOn g f I ∧ PiecewiseConstantOn g I}) (hb : b ∈ (fun (x : ℝ → ℝ) => PiecewiseConstantOn.integ x I) '' {g : ℝ → ℝ | MinorizesOn g f I ∧ PiecewiseConstantOn g I}) :

b ≤ a

theorem Chapter11.integral_bound_below {f : ℝ → ℝ} {I : BoundedInterval} (h : Chapter9.BddOn f ↑I) :

BddBelow ((fun (x : ℝ → ℝ) => PiecewiseConstantOn.integ x I) '' {g : ℝ → ℝ | MajorizesOn g f I ∧ PiecewiseConstantOn g I})

theorem Chapter11.integral_bound_above {f : ℝ → ℝ} {I : BoundedInterval} (h : Chapter9.BddOn f ↑I) :

BddAbove ((fun (x : ℝ → ℝ) => PiecewiseConstantOn.integ x I) '' {g : ℝ → ℝ | MinorizesOn g f I ∧ PiecewiseConstantOn g I})

theorem Chapter11.le_lower_integral {f : ℝ → ℝ} {I : BoundedInterval} {M : ℝ} (h : ∀ x ∈ ↑I, |f x| ≤ M) :

-M * I.length ≤ lower_integral f I

Lemma 11.3.3. The proof has been reorganized somewhat from the textbook.

theorem Chapter11.lower_integral_le_upper {f : ℝ → ℝ} {I : BoundedInterval} (h : Chapter9.BddOn f ↑I) :

lower_integral f I ≤ upper_integral f I

theorem Chapter11.upper_integral_le {f : ℝ → ℝ} {I : BoundedInterval} {M : ℝ} (h : ∀ x ∈ ↑I, |f x| ≤ M) :

upper_integral f I ≤ M * I.length

theorem Chapter11.upper_integral_le_integ {f g : ℝ → ℝ} {I : BoundedInterval} (hf : Chapter9.BddOn f ↑I) (hfg : MajorizesOn g f I) (hg : PiecewiseConstantOn g I) :

upper_integral f I ≤ hg.integ'

theorem Chapter11.integ_le_lower_integral {f h : ℝ → ℝ} {I : BoundedInterval} (hf : Chapter9.BddOn f ↑I) (hfh : MinorizesOn h f I) (hg : PiecewiseConstantOn h I) :

hg.integ' ≤ lower_integral f I

theorem Chapter11.lt_of_gt_upper_integral {f : ℝ → ℝ} {I : BoundedInterval} (hf : Chapter9.BddOn f ↑I) {X : ℝ} (hX : upper_integral f I < X) :

∃ (g : ℝ → ℝ), MajorizesOn g f I ∧ PiecewiseConstantOn g I ∧ PiecewiseConstantOn.integ g I < X

theorem Chapter11.gt_of_lt_lower_integral {f : ℝ → ℝ} {I : BoundedInterval} (hf : Chapter9.BddOn f ↑I) {X : ℝ} (hX : X < lower_integral f I) :

∃ (h : ℝ → ℝ), MinorizesOn h f I ∧ PiecewiseConstantOn h I ∧ X < PiecewiseConstantOn.integ h I

@[reducible, inline]

noncomputable abbrev Chapter11.integ (f : ℝ → ℝ) (I : BoundedInterval) :

Definition 11.3.4 (Riemann integral) As we permit junk values, the simplest definition for the Riemann integral is the upper integral.

Equations

Chapter11.integ f I = Chapter11.upper_integral f I

Instances For

theorem Chapter11.integ_congr {f g : ℝ → ℝ} {I : BoundedInterval} (h : Set.EqOn f g ↑I) :

integ f I = integ g I

@[reducible, inline]

noncomputable abbrev Chapter11.IntegrableOn (f : ℝ → ℝ) (I : BoundedInterval) :

Equations

Chapter11.IntegrableOn f I = (Chapter9.BddOn f ↑I ∧ Chapter11.lower_integral f I = Chapter11.upper_integral f I)

Instances For

theorem Chapter11.integ_of_piecewise_const {f : ℝ → ℝ} {I : BoundedInterval} (hf : PiecewiseConstantOn f I) :

IntegrableOn f I ∧ integ f I = hf.integ'

Lemma 11.3.7 / Exercise 11.3.3

theorem Chapter11.integ_on_subsingleton {f : ℝ → ℝ} {I : BoundedInterval} (hI : I.length = 0) :

IntegrableOn f I ∧ integ f I = 0

Remark 11.3.8

@[reducible, inline]

noncomputable abbrev Chapter11.upper_riemann_sum (f : ℝ → ℝ) {I : BoundedInterval} (P : Partition I) :

Definition 11.3.9 (Riemann sums). The restriction to positive length J is not needed thanks to various junk value conventions.

Equations

Chapter11.upper_riemann_sum f P = ∑ J ∈ P.intervals, sSup (f '' ↑J) * J.length

Instances For

@[reducible, inline]

noncomputable abbrev Chapter11.lower_riemann_sum (f : ℝ → ℝ) {I : BoundedInterval} (P : Partition I) :

Equations

Chapter11.lower_riemann_sum f P = ∑ J ∈ P.intervals, sInf (f '' ↑J) * J.length

Instances For

theorem Chapter11.upper_riemann_sum_le {f g : ℝ → ℝ} {I : BoundedInterval} (P : Partition I) (hf : Chapter9.BddOn f ↑I) (hgf : MajorizesOn g f I) (hg : PiecewiseConstantOn g I) :

upper_riemann_sum f P ≤ integ g I

Lemma 11.3.11 / Exercise 11.3.4

theorem Chapter11.lower_riemann_sum_ge {f h : ℝ → ℝ} {I : BoundedInterval} (P : Partition I) (hf : Chapter9.BddOn f ↑I) (hfh : MinorizesOn h f I) (hg : PiecewiseConstantOn h I) :

integ h I ≤ lower_riemann_sum f P

theorem Chapter11.upper_integ_le_upper_sum {f : ℝ → ℝ} {I : BoundedInterval} (hf : Chapter9.BddOn f ↑I) (P : Partition I) :

upper_integral f I ≤ upper_riemann_sum f P

Proposition 11.3.12 / Exercise 11.3.5

theorem Chapter11.upper_integ_eq_inf_upper_sum {f : ℝ → ℝ} {I : BoundedInterval} (hf : Chapter9.BddOn f ↑I) :

upper_integral f I = sInf (Set.range fun (P : Partition I) => upper_riemann_sum f P)

theorem Chapter11.lower_integ_ge_lower_sum {f : ℝ → ℝ} {I : BoundedInterval} (hf : Chapter9.BddOn f ↑I) (P : Partition I) :

lower_riemann_sum f P ≤ lower_integral f I

theorem Chapter11.lower_integ_eq_sup_lower_sum {f : ℝ → ℝ} {I : BoundedInterval} (hf : Chapter9.BddOn f ↑I) :

lower_integral f I = sSup (Set.range fun (P : Partition I) => lower_riemann_sum f P)

theorem Chapter11.MajorizesOn.trans {f g h : ℝ → ℝ} {I : BoundedInterval} (hfg : MajorizesOn f g I) (hgh : MajorizesOn g h I) :

MajorizesOn f h I

Exercise 11.3.1

theorem Chapter11.MajorizesOn.anti_symm {f g : ℝ → ℝ} {I : BoundedInterval} (x : ℝ) :

x ∈ ↑I → (f x = g x ↔ MajorizesOn f g I ∧ MajorizesOn g f I)

Exercise 11.3.1

def Chapter11.MajorizesOn.of_add :

Decidable (∀ (f g h : ℝ → ℝ) (I : BoundedInterval), MajorizesOn f g I → MajorizesOn (f + h) (g + h) I)

Exercise 11.3.2

Equations

Chapter11.MajorizesOn.of_add = sorry

Instances For

def Chapter11.MajorizesOn.of_mul :

Decidable (∀ (f g h : ℝ → ℝ) (I : BoundedInterval), MajorizesOn f g I → MajorizesOn (f * h) (g * h) I)

Equations

Chapter11.MajorizesOn.of_mul = sorry

Instances For

def Chapter11.MajorizesOn.of_smul :

Decidable (∀ (f g : ℝ → ℝ) (c : ℝ) (I : BoundedInterval), MajorizesOn f g I → MajorizesOn (c • f) (c • g) I)

Equations

Chapter11.MajorizesOn.of_smul = sorry

Instances For