Аналіз I, Розділ 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) : Prop

Визначення 11.3.1 (Majorization of functions)

Equations

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

@[reducible, inline]

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

Equations

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

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) : ℝ

Визначення 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})

@[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})

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

Лема 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) : ℝ

Визначення 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

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) : Prop

Equations

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

theorem Chapter11.integ_of_piecewise_const {f : ℝ → ℝ} {I : BoundedInterval} (hf : PiecewiseConstantOn f I) : IntegrableOn f I ∧ integ f I = hf.integ'

Лема 11.3.7 / Вправа 11.3.3

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

Ремарка 11.3.8

@[reducible, inline]

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

Визначення 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

@[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

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

Лема 11.3.11 / Вправа 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

Твердження 11.3.12 / Вправа 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

Вправа 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)

Вправа 11.3.1

def Chapter11.MajorizesOn.of_add : Decidable (∀ (f g h : ℝ → ℝ) (I : BoundedInterval), MajorizesOn f g I → MajorizesOn (f + h) (g + h) I)

Вправа 11.3.2

Equations

• Chapter11.MajorizesOn.of_add = sorry

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

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