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.

namespace Chapter11open BoundedInterval Chapter9

Definition 11.3.1 (Majorization of functions)

abbrev MajorizesOn (g f:ℝ → ℝ) (I: BoundedInterval) : Prop := ∀ x ∈ (I:Set ℝ), f x ≤ g x

abbrev MinorizesOn (g f:ℝ → ℝ) (I: BoundedInterval) : Prop := ∀ x ∈ (I:Set ℝ), g x ≤ f x

theorem MinorizesOn.iff (g f:ℝ → ℝ) (I: BoundedInterval) : MinorizesOn g f I ↔ MajorizesOn f g I := byg:ℝ → ℝf:ℝ → ℝI:BoundedInterval⊢ MinorizesOn g f I ↔ MajorizesOn f g I rflAll goals completed! 🐙

Definition 11.3.2 (Uppper and lower Riemann integrals )

noncomputable abbrev upper_integral (f:ℝ → ℝ) (I: BoundedInterval) : ℝ :=
  sInf ((PiecewiseConstantOn.integ ·I) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I})

noncomputable abbrev lower_integral (f:ℝ → ℝ) (I: BoundedInterval) : ℝ :=
  sSup ((PiecewiseConstantOn.integ ·I) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I})

theorem upper_integral_congr {f g:ℝ → ℝ} {I: BoundedInterval} (h: Set.EqOn f g I) :
  upper_integral f I = upper_integral g I := byf:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:Set.EqOn f g ↑I⊢ upper_integral f I = upper_integral g I
  simp [upper_integral]f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:Set.EqOn f g ↑I⊢ sInf ((fun x => PiecewiseConstantOn.integ x I) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}) =
  sInf ((fun x => PiecewiseConstantOn.integ x I) '' {g_1 | MajorizesOn g_1 g I ∧ PiecewiseConstantOn g_1 I}); congr! 2h.e'_3.h.e'_4f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:Set.EqOn f g ↑I⊢ {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I} = {g_1 | MajorizesOn g_1 g I ∧ PiecewiseConstantOn g_1 I}; exth.e'_3.h.e'_4.hf:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:Set.EqOn f g ↑Ix✝:ℝ → ℝ⊢ x✝ ∈ {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I} ↔ x✝ ∈ {g_1 | MajorizesOn g_1 g I ∧ PiecewiseConstantOn g_1 I}; simph.e'_3.h.e'_4.hf:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:Set.EqOn f g ↑Ix✝:ℝ → ℝ⊢ ∀ (x : Partition I), PiecewiseConstantWith x✝ x → (MajorizesOn x✝ f I ↔ MajorizesOn x✝ g I); grindAll goals completed! 🐙

theorem lower_integral_congr {f g:ℝ → ℝ} {I: BoundedInterval} (h: Set.EqOn f g I) :
  lower_integral f I = lower_integral g I := byf:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:Set.EqOn f g ↑I⊢ lower_integral f I = lower_integral g I
  simp [lower_integral]f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:Set.EqOn f g ↑I⊢ sSup ((fun x => PiecewiseConstantOn.integ x I) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}) =
  sSup ((fun x => PiecewiseConstantOn.integ x I) '' {g_1 | MinorizesOn g_1 g I ∧ PiecewiseConstantOn g_1 I}); congr! 2h.e'_3.h.e'_4f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:Set.EqOn f g ↑I⊢ {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I} = {g_1 | MinorizesOn g_1 g I ∧ PiecewiseConstantOn g_1 I}; exth.e'_3.h.e'_4.hf:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:Set.EqOn f g ↑Ix✝:ℝ → ℝ⊢ x✝ ∈ {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I} ↔ x✝ ∈ {g_1 | MinorizesOn g_1 g I ∧ PiecewiseConstantOn g_1 I}; simph.e'_3.h.e'_4.hf:ℝ → ℝg:ℝ → ℝI:BoundedIntervalh:Set.EqOn f g ↑Ix✝:ℝ → ℝ⊢ ∀ (x : Partition I), PiecewiseConstantWith x✝ x → (MinorizesOn x✝ f I ↔ MinorizesOn x✝ g I); grindAll goals completed! 🐙

lemma integral_bound_upper_of_bounded {f:ℝ → ℝ} {M:ℝ} {I: BoundedInterval} (h: ∀ x ∈ (I:Set ℝ), |f x| ≤ M) : M * |I|ₗ ∈ (PiecewiseConstantOn.integ ·I) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I} := byf:ℝ → ℝM:ℝI:BoundedIntervalh:∀ x ∈ ↑I, |f x| ≤ M⊢ M * I.length ∈ (fun x => PiecewiseConstantOn.integ x I) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}
  simpf:ℝ → ℝM:ℝI:BoundedIntervalh:∀ x ∈ ↑I, |f x| ≤ M⊢ ∃ x, (MajorizesOn x f I ∧ PiecewiseConstantOn x I) ∧ PiecewiseConstantOn.integ x I = M * I.length
  refine' ⟨ fun _ ↦ M , ⟨ ⟨ _, _ ⟩, PiecewiseConstantOn.integ_const _ _ ⟩ ⟩refine'_1f:ℝ → ℝM:ℝI:BoundedIntervalh:∀ x ∈ ↑I, |f x| ≤ M⊢ MajorizesOn (fun x => M) f Irefine'_2f:ℝ → ℝM:ℝI:BoundedIntervalh:∀ x ∈ ↑I, |f x| ≤ M⊢ PiecewiseConstantOn (fun x => M) I
  .refine'_1f:ℝ → ℝM:ℝI:BoundedIntervalh:∀ x ∈ ↑I, |f x| ≤ M⊢ MajorizesOn (fun x => M) f I grind [abs_le']All goals completed! 🐙
  apply (ConstantOn.of_const (c := M) _).piecewiseConstantOnf:ℝ → ℝM:ℝI:BoundedIntervalh:∀ x ∈ ↑I, |f x| ≤ M⊢ ∀ x ∈ ↑I, M = M; simpAll goals completed! 🐙

lemma integral_bound_lower_of_bounded {f:ℝ → ℝ} {M:ℝ} {I: BoundedInterval} (h: ∀ x ∈ (I:Set ℝ), |f x| ≤ M) : -M * |I|ₗ ∈ (PiecewiseConstantOn.integ ·I) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I} := byf:ℝ → ℝM:ℝI:BoundedIntervalh:∀ x ∈ ↑I, |f x| ≤ M⊢ -M * I.length ∈ (fun x => PiecewiseConstantOn.integ x I) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}
  simpf:ℝ → ℝM:ℝI:BoundedIntervalh:∀ x ∈ ↑I, |f x| ≤ M⊢ ∃ x, (MinorizesOn x f I ∧ PiecewiseConstantOn x I) ∧ PiecewiseConstantOn.integ x I = -(M * I.length)
  refine' ⟨ fun _ ↦ -M , ⟨ ⟨ _, _ ⟩, byf:ℝ → ℝM:ℝI:BoundedIntervalh:∀ x ∈ ↑I, |f x| ≤ M⊢ PiecewiseConstantOn.integ (fun x => -M) I = -(M * I.length) convert PiecewiseConstantOn.integ_const _ _ using 1h.e'_3f:ℝ → ℝM:ℝI:BoundedIntervalh:∀ x ∈ ↑I, |f x| ≤ M⊢ -(M * I.length) = -M * I.length; simpAll goals completed! 🐙 ⟩ ⟩
  .refine'_1f:ℝ → ℝM:ℝI:BoundedIntervalh:∀ x ∈ ↑I, |f x| ≤ M⊢ MinorizesOn (fun x => -M) f I grind [abs_le']All goals completed! 🐙
  exact (ConstantOn.of_const (c := -M) (byf:ℝ → ℝM:ℝI:BoundedIntervalh:∀ x ∈ ↑I, |f x| ≤ M⊢ ∀ x ∈ ↑I, -M = -M simpAll goals completed! 🐙)).piecewiseConstantOn

lemma integral_bound_upper_nonempty {f:ℝ → ℝ} {I: BoundedInterval} (h: BddOn f I) : ((PiecewiseConstantOn.integ ·I) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}).Nonempty :=
  ⟨ _, integral_bound_upper_of_bounded h.choose_spec ⟩

lemma integral_bound_lower_nonempty {f:ℝ → ℝ} {I: BoundedInterval} (h: BddOn f I) : ((PiecewiseConstantOn.integ ·I) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}).Nonempty :=
  ⟨ _, integral_bound_lower_of_bounded h.choose_spec ⟩

lemma integral_bound_lower_le_upper {f:ℝ → ℝ} {I: BoundedInterval} {a b:ℝ}
  (ha: a ∈ (PiecewiseConstantOn.integ ·I) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I})
  (hb: b ∈ (PiecewiseConstantOn.integ ·I) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I})
  : b ≤ a:= byf:ℝ → ℝI:BoundedIntervala:ℝ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
    obtain ⟨ g, ⟨ ⟨ hmaj, hgp⟩, rfl ⟩ ⟩ := haintro.intro.introf:ℝ → ℝI:BoundedIntervalb:ℝhb:b ∈ (fun x => PiecewiseConstantOn.integ x I) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}g:ℝ → ℝhmaj:MajorizesOn g f Ihgp:PiecewiseConstantOn g I⊢ b ≤ (fun x => PiecewiseConstantOn.integ x I) g
    obtain ⟨ h, ⟨ ⟨ hmin, hhp⟩, rfl ⟩ ⟩ := hbintro.intro.intro.intro.intro.introf:ℝ → ℝI:BoundedIntervalg:ℝ → ℝhmaj:MajorizesOn g f Ihgp:PiecewiseConstantOn g Ih:ℝ → ℝhmin:MinorizesOn h f Ihhp:PiecewiseConstantOn h I⊢ (fun x => PiecewiseConstantOn.integ x I) h ≤ (fun x => PiecewiseConstantOn.integ x I) g
    apply hhp.integ_mono _ hgpf:ℝ → ℝI:BoundedIntervalg:ℝ → ℝhmaj:MajorizesOn g f Ihgp:PiecewiseConstantOn g Ih:ℝ → ℝhmin:MinorizesOn h f Ihhp:PiecewiseConstantOn h I⊢ ∀ x ∈ I, h x ≤ g x; intro x hxf:ℝ → ℝI:BoundedIntervalg:ℝ → ℝhmaj:MajorizesOn g f Ihgp:PiecewiseConstantOn g Ih:ℝ → ℝhmin:MinorizesOn h f Ihhp:PiecewiseConstantOn h Ix:ℝhx:x ∈ I⊢ h x ≤ g x; linarith [hmin _ hx, hmaj _ hx]All goals completed! 🐙

lemma integral_bound_below {f:ℝ → ℝ} {I: BoundedInterval} (h: BddOn f I) :
  BddBelow ((PiecewiseConstantOn.integ ·I) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}) := byf:ℝ → ℝI:BoundedIntervalh:BddOn f ↑I⊢ BddBelow ((fun x => PiecewiseConstantOn.integ x I) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I})
    rw [bddBelow_def]f:ℝ → ℝI:BoundedIntervalh:BddOn f ↑I⊢ ∃ x, ∀ y ∈ (fun x => PiecewiseConstantOn.integ x I) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}, x ≤ y; use (integral_bound_lower_nonempty h).somehf:ℝ → ℝI:BoundedIntervalh:BddOn f ↑I⊢ ∀ y ∈ (fun x => PiecewiseConstantOn.integ x I) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}, ⋯.some ≤ y
    intro a hahf:ℝ → ℝI:BoundedIntervalh:BddOn f ↑Ia:ℝha:a ∈ (fun x => PiecewiseConstantOn.integ x I) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}⊢ ⋯.some ≤ a; exact integral_bound_lower_le_upper ha (integral_bound_lower_nonempty h).some_memAll goals completed! 🐙

lemma integral_bound_above {f:ℝ → ℝ} {I: BoundedInterval} (h: BddOn f I) :
  BddAbove ((PiecewiseConstantOn.integ ·I) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}) := byf:ℝ → ℝI:BoundedIntervalh:BddOn f ↑I⊢ BddAbove ((fun x => PiecewiseConstantOn.integ x I) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I})
    rw [bddAbove_def]f:ℝ → ℝI:BoundedIntervalh:BddOn f ↑I⊢ ∃ x, ∀ y ∈ (fun x => PiecewiseConstantOn.integ x I) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}, y ≤ x; use (integral_bound_upper_nonempty h).somehf:ℝ → ℝI:BoundedIntervalh:BddOn f ↑I⊢ ∀ y ∈ (fun x => PiecewiseConstantOn.integ x I) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}, y ≤ ⋯.some
    intro b hbhf:ℝ → ℝI:BoundedIntervalh:BddOn f ↑Ib:ℝhb:b ∈ (fun x => PiecewiseConstantOn.integ x I) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}⊢ b ≤ ⋯.some; exact integral_bound_lower_le_upper (integral_bound_upper_nonempty h).some_mem hbAll goals completed! 🐙

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

lemma le_lower_integral {f:ℝ → ℝ} {I: BoundedInterval} {M:ℝ} (h: ∀ x ∈ (I:Set ℝ), |f x| ≤ M) :
  -M * |I|ₗ ≤ lower_integral f I :=
  ConditionallyCompleteLattice.le_csSup _ _
    (integral_bound_above (BddOn.of_bounded h)) (integral_bound_lower_of_bounded h)

lemma lower_integral_le_upper {f:ℝ → ℝ} {I: BoundedInterval} (h: BddOn f I) :
  lower_integral f I ≤ upper_integral f I := byf:ℝ → ℝI:BoundedIntervalh:BddOn f ↑I⊢ lower_integral f I ≤ upper_integral f I
  apply ConditionallyCompleteLattice.csSup_le _ _ (integral_bound_lower_nonempty h) _f:ℝ → ℝI:BoundedIntervalh:BddOn f ↑I⊢ upper_integral f I ∈
  upperBounds ((fun x => PiecewiseConstantOn.integ x I) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I})
  rw [mem_upperBounds]f:ℝ → ℝI:BoundedIntervalh:BddOn f ↑I⊢ ∀ x ∈ (fun x => PiecewiseConstantOn.integ x I) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I},
  x ≤ upper_integral f I; introsf:ℝ → ℝI:BoundedIntervalh:BddOn f ↑Ix✝:ℝa✝:x✝ ∈ (fun x => PiecewiseConstantOn.integ x I) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}⊢ x✝ ≤ upper_integral f I
  apply ConditionallyCompleteLattice.le_csInf _ _ (integral_bound_upper_nonempty h) _f:ℝ → ℝI:BoundedIntervalh:BddOn f ↑Ix✝:ℝa✝:x✝ ∈ (fun x => PiecewiseConstantOn.integ x I) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}⊢ x✝ ∈ lowerBounds ((fun x => PiecewiseConstantOn.integ x I) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I})
  rw [mem_lowerBounds]f:ℝ → ℝI:BoundedIntervalh:BddOn f ↑Ix✝:ℝa✝:x✝ ∈ (fun x => PiecewiseConstantOn.integ x I) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}⊢ ∀ x ∈ (fun x => PiecewiseConstantOn.integ x I) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}, x✝ ≤ x
  solve_by_elim [integral_bound_lower_le_upper]All goals completed! 🐙

lemma upper_integral_le {f:ℝ → ℝ} {I: BoundedInterval} {M:ℝ} (h: ∀ x ∈ (I:Set ℝ), |f x| ≤ M) :
  upper_integral f I ≤ M * |I|ₗ :=
  ConditionallyCompleteLattice.csInf_le _ _
    (integral_bound_below (BddOn.of_bounded h)) (integral_bound_upper_of_bounded h)

lemma upper_integral_le_integ {f g:ℝ → ℝ} {I: BoundedInterval} (hf: BddOn f I)
  (hfg: MajorizesOn g f I) (hg: PiecewiseConstantOn g I) :
  upper_integral f I ≤ hg.integ' := byf:ℝ → ℝg:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑Ihfg:MajorizesOn g f Ihg:PiecewiseConstantOn g I⊢ upper_integral f I ≤ hg.integ'
  apply ConditionallyCompleteLattice.csInf_le _ _ (integral_bound_below hf) _f:ℝ → ℝg:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑Ihfg:MajorizesOn g f Ihg:PiecewiseConstantOn g I⊢ hg.integ' ∈ (fun x => PiecewiseConstantOn.integ x I) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}
  use ghf:ℝ → ℝg:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑Ihfg:MajorizesOn g f Ihg:PiecewiseConstantOn g I⊢ g ∈ {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I} ∧ (fun x => PiecewiseConstantOn.integ x I) g = hg.integ'; simpa [hg]All goals completed! 🐙

lemma integ_le_lower_integral {f h:ℝ → ℝ} {I: BoundedInterval} (hf: BddOn f I)
  (hfh: MinorizesOn h f I) (hg: PiecewiseConstantOn h I) :
  hg.integ' ≤ lower_integral f I := byf:ℝ → ℝh:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑Ihfh:MinorizesOn h f Ihg:PiecewiseConstantOn h I⊢ hg.integ' ≤ lower_integral f I
  apply ConditionallyCompleteLattice.le_csSup _ _ (integral_bound_above hf) _f:ℝ → ℝh:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑Ihfh:MinorizesOn h f Ihg:PiecewiseConstantOn h I⊢ hg.integ' ∈ (fun x => PiecewiseConstantOn.integ x I) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}
  use hhf:ℝ → ℝh:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑Ihfh:MinorizesOn h f Ihg:PiecewiseConstantOn h I⊢ h ∈ {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I} ∧ (fun x => PiecewiseConstantOn.integ x I) h = hg.integ'; simpa [hg]All goals completed! 🐙

lemma lt_of_gt_upper_integral {f:ℝ → ℝ} {I: BoundedInterval} (hf: BddOn f I)
  {X:ℝ} (hX: upper_integral f I < X ) :
  ∃ g, MajorizesOn g f I ∧ PiecewiseConstantOn g I ∧ PiecewiseConstantOn.integ g I < X := byf:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑IX:ℝhX:upper_integral f I < X⊢ ∃ g, MajorizesOn g f I ∧ PiecewiseConstantOn g I ∧ PiecewiseConstantOn.integ g I < X
  choose Y hY hYX using exists_lt_of_csInf_lt (integral_bound_upper_nonempty hf) hXf:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑IX:ℝhX:upper_integral f I < XY:ℝhY:Y ∈ (fun x => PiecewiseConstantOn.integ x I) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}hYX:Y < X⊢ ∃ g, MajorizesOn g f I ∧ PiecewiseConstantOn g I ∧ PiecewiseConstantOn.integ g I < X
  simp at hYf:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑IX:ℝhX:upper_integral f I < XY:ℝhYX:Y < XhY:∃ x, (MajorizesOn x f I ∧ PiecewiseConstantOn x I) ∧ PiecewiseConstantOn.integ x I = Y⊢ ∃ g, MajorizesOn g f I ∧ PiecewiseConstantOn g I ∧ PiecewiseConstantOn.integ g I < X; peel hYhf:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑IX:ℝhX:upper_integral f I < XY:ℝhYX:Y < XhY:∃ x, (MajorizesOn x f I ∧ PiecewiseConstantOn x I) ∧ PiecewiseConstantOn.integ x I = Yg✝:ℝ → ℝthis:(MajorizesOn g✝ f I ∧ PiecewiseConstantOn g✝ I) ∧ PiecewiseConstantOn.integ g✝ I = Y⊢ MajorizesOn g✝ f I ∧ PiecewiseConstantOn g✝ I ∧ PiecewiseConstantOn.integ g✝ I < X; simp_allhf:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑IX:ℝhX:upper_integral f I < XY:ℝhYX:Y < XhY:∃ x, (MajorizesOn x f I ∧ PiecewiseConstantOn x I) ∧ PiecewiseConstantOn.integ x I = Yg✝:ℝ → ℝthis:(MajorizesOn g✝ f I ∧ PiecewiseConstantOn g✝ I) ∧ PiecewiseConstantOn.integ g✝ I = Y⊢ MajorizesOn g✝ f I; tautoAll goals completed! 🐙

lemma gt_of_lt_lower_integral {f:ℝ → ℝ} {I: BoundedInterval} (hf: BddOn f I)
  {X:ℝ} (hX: X < lower_integral f I) :
  ∃ h, MinorizesOn h f I ∧ PiecewiseConstantOn h I ∧ X < PiecewiseConstantOn.integ h I := byf:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑IX:ℝhX:X < lower_integral f I⊢ ∃ h, MinorizesOn h f I ∧ PiecewiseConstantOn h I ∧ X < PiecewiseConstantOn.integ h I
  choose Y hY hYX using exists_lt_of_lt_csSup (integral_bound_lower_nonempty hf) hXf:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑IX:ℝhX:X < lower_integral f IY:ℝhY:Y ∈ (fun x => PiecewiseConstantOn.integ x I) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}hYX:X < Y⊢ ∃ h, MinorizesOn h f I ∧ PiecewiseConstantOn h I ∧ X < PiecewiseConstantOn.integ h I
  simp at hYf:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑IX:ℝhX:X < lower_integral f IY:ℝhYX:X < YhY:∃ x, (MinorizesOn x f I ∧ PiecewiseConstantOn x I) ∧ PiecewiseConstantOn.integ x I = Y⊢ ∃ h, MinorizesOn h f I ∧ PiecewiseConstantOn h I ∧ X < PiecewiseConstantOn.integ h I; peel hYhf:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑IX:ℝhX:X < lower_integral f IY:ℝhYX:X < YhY:∃ x, (MinorizesOn x f I ∧ PiecewiseConstantOn x I) ∧ PiecewiseConstantOn.integ x I = Yh✝:ℝ → ℝthis:(MinorizesOn h✝ f I ∧ PiecewiseConstantOn h✝ I) ∧ PiecewiseConstantOn.integ h✝ I = Y⊢ MinorizesOn h✝ f I ∧ PiecewiseConstantOn h✝ I ∧ X < PiecewiseConstantOn.integ h✝ I; simp_allhf:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑IX:ℝhX:X < lower_integral f IY:ℝhYX:X < YhY:∃ x, (MinorizesOn x f I ∧ PiecewiseConstantOn x I) ∧ PiecewiseConstantOn.integ x I = Yh✝:ℝ → ℝthis:(MinorizesOn h✝ f I ∧ PiecewiseConstantOn h✝ I) ∧ PiecewiseConstantOn.integ h✝ I = Y⊢ MinorizesOn h✝ f I; tautoAll goals completed! 🐙

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

noncomputable abbrev integ (f:ℝ → ℝ) (I: BoundedInterval) : ℝ := upper_integral f I

theorem integ_congr {f g:ℝ → ℝ} {I: BoundedInterval} (h: Set.EqOn f g I) :
  integ f I = integ g I := upper_integral_congr h

noncomputable abbrev IntegrableOn (f:ℝ → ℝ) (I: BoundedInterval) : Prop :=
  BddOn f I ∧ lower_integral f I = upper_integral f I

Lemma 11.3.7 / Exercise 11.3.3

theorem declaration uses 'sorry'integ_of_piecewise_const {f:ℝ → ℝ} {I: BoundedInterval} (hf: PiecewiseConstantOn f I) :
  IntegrableOn f I ∧ integ f I = hf.integ' := byf:ℝ → ℝI:BoundedIntervalhf:PiecewiseConstantOn f I⊢ IntegrableOn f I ∧ integ f I = hf.integ'
  sorryAll goals completed! 🐙

Remark 11.3.8

theorem integ_on_subsingleton {f:ℝ → ℝ} {I: BoundedInterval} (hI: |I|ₗ = 0) :
  IntegrableOn f I ∧ integ f I = 0 := byf:ℝ → ℝI:BoundedIntervalhI:I.length = 0⊢ IntegrableOn f I ∧ integ f I = 0
  observe : Subsingleton I.toSetf:ℝ → ℝI:BoundedIntervalhI:I.length = 0this:Subsingleton ↑↑I⊢ IntegrableOn f I ∧ integ f I = 0
  observe hconst : ConstantOn f If:ℝ → ℝI:BoundedIntervalhI:I.length = 0this:Subsingleton ↑↑Ihconst:ConstantOn f ↑I⊢ IntegrableOn f I ∧ integ f I = 0
  convert integ_of_piecewise_const hconst.piecewiseConstantOnh.e'_2.h.e'_3f:ℝ → ℝI:BoundedIntervalhI:I.length = 0this:Subsingleton ↑↑Ihconst:ConstantOn f ↑I⊢ 0 = ⋯.integ'
  simp [PiecewiseConstantOn.integ_const' hconst, hI]All goals completed! 🐙

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

noncomputable abbrev upper_riemann_sum (f:ℝ → ℝ) {I: BoundedInterval} (P: Partition I) : ℝ :=
  ∑ J ∈ P.intervals, (sSup (f '' (J:Set ℝ))) * |J|ₗ

noncomputable abbrev lower_riemann_sum (f:ℝ → ℝ) {I: BoundedInterval} (P: Partition I) : ℝ :=
  ∑ J ∈ P.intervals, (sInf (f '' (J:Set ℝ))) * |J|ₗ

Lemma 11.3.11 / Exercise 11.3.4

theorem declaration uses 'sorry'upper_riemann_sum_le {f g: ℝ → ℝ} {I:BoundedInterval} (P: Partition I)
  (hf: BddOn f I) (hgf: MajorizesOn g f I) (hg: PiecewiseConstantOn g I) :
  upper_riemann_sum f P ≤ integ g I := byf:ℝ → ℝg:ℝ → ℝI:BoundedIntervalP:Partition Ihf:BddOn f ↑Ihgf:MajorizesOn g f Ihg:PiecewiseConstantOn g I⊢ upper_riemann_sum f P ≤ integ g I
   sorryAll goals completed! 🐙

theorem declaration uses 'sorry'lower_riemann_sum_ge {f h: ℝ → ℝ} {I:BoundedInterval} (P: Partition I)
  (hf: BddOn f I) (hfh: MinorizesOn h f I) (hg: PiecewiseConstantOn h I) :
  integ h I ≤ lower_riemann_sum f P := byf:ℝ → ℝh:ℝ → ℝI:BoundedIntervalP:Partition Ihf:BddOn f ↑Ihfh:MinorizesOn h f Ihg:PiecewiseConstantOn h I⊢ integ h I ≤ lower_riemann_sum f P
   sorryAll goals completed! 🐙

Proposition 11.3.12 / Exercise 11.3.5

theorem declaration uses 'sorry'upper_integ_le_upper_sum {f:ℝ → ℝ} {I:BoundedInterval} (hf: BddOn f I)
  (P: Partition I): upper_integral f I ≤ upper_riemann_sum f P := byf:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑IP:Partition I⊢ upper_integral f I ≤ upper_riemann_sum f P
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'upper_integ_eq_inf_upper_sum {f:ℝ → ℝ} {I:BoundedInterval} (hf: BddOn f I) :
  upper_integral f I = sInf (.range (fun P : Partition I ↦ upper_riemann_sum f P)) := byf:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑I⊢ upper_integral f I = sInf (Set.range fun P => upper_riemann_sum f P)
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'lower_integ_ge_lower_sum {f:ℝ → ℝ} {I:BoundedInterval} (hf: BddOn f I)
  (P: Partition I): lower_riemann_sum f P ≤ lower_integral f I := byf:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑IP:Partition I⊢ lower_riemann_sum f P ≤ lower_integral f I
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'lower_integ_eq_sup_lower_sum {f:ℝ → ℝ} {I:BoundedInterval} (hf: BddOn f I) :
  lower_integral f I = sSup (.range (fun P : Partition I ↦ lower_riemann_sum f P)) := byf:ℝ → ℝI:BoundedIntervalhf:BddOn f ↑I⊢ lower_integral f I = sSup (Set.range fun P => lower_riemann_sum f P)
  sorryAll goals completed! 🐙

Exercise 11.3.1

theorem declaration uses 'sorry'MajorizesOn.trans {f g h: ℝ → ℝ} {I: BoundedInterval}
  (hfg: MajorizesOn f g I) (hgh: MajorizesOn g h I) : MajorizesOn f h I := byf:ℝ → ℝg:ℝ → ℝh:ℝ → ℝI:BoundedIntervalhfg:MajorizesOn f g Ihgh:MajorizesOn g h I⊢ MajorizesOn f h I
  sorryAll goals completed! 🐙

Exercise 11.3.1

theorem declaration uses 'sorry'MajorizesOn.anti_symm {f g: ℝ → ℝ} {I: BoundedInterval}:
  ∀ x ∈ (I:Set ℝ), f x = g x ↔ MajorizesOn f g I ∧ MajorizesOn g f I := byf:ℝ → ℝg:ℝ → ℝI:BoundedInterval⊢ ∀ x ∈ ↑I, f x = g x ↔ MajorizesOn f g I ∧ MajorizesOn g f I
  sorryAll goals completed! 🐙

Exercise 11.3.2

def declaration uses 'sorry'MajorizesOn.of_add : Decidable (∀ (f g h:ℝ → ℝ) (I:BoundedInterval) (hfg: MajorizesOn f g I),
 MajorizesOn (f+h) (g+h) I) := by⊢ Decidable (∀ (f g h : ℝ → ℝ) (I : BoundedInterval), MajorizesOn f g I → MajorizesOn (f + h) (g + h) I)
  -- the first line of this construction should be either `apply isTrue` or `apply isFalse`.
  sorryAll goals completed! 🐙

def declaration uses 'sorry'MajorizesOn.of_mul : Decidable (∀ (f g h:ℝ → ℝ) (I:BoundedInterval) (hfg: MajorizesOn f g I),
 MajorizesOn (f*h) (g*h) I) := by⊢ Decidable (∀ (f g h : ℝ → ℝ) (I : BoundedInterval), MajorizesOn f g I → MajorizesOn (f * h) (g * h) I)
  -- the first line of this construction should be either `apply isTrue` or `apply isFalse`.
  sorryAll goals completed! 🐙

def declaration uses 'sorry'MajorizesOn.of_smul : Decidable (∀ (f g:ℝ → ℝ) (c:ℝ) (I:BoundedInterval) (hfg: MajorizesOn f g I),
 MajorizesOn (c • f) (c • g) I) := by⊢ Decidable (∀ (f g : ℝ → ℝ) (c : ℝ) (I : BoundedInterval), MajorizesOn f g I → MajorizesOn (c • f) (c • g) I)
  -- the first line of this construction should be either `apply isTrue` or `apply isFalse`.
  sorryAll goals completed! 🐙

end Chapter11