Analysis
11.7. A non-Riemann integrable function

Imports

import Mathlib.Tactic
import Mathlib.Topology.Instances.Irrational
import Analysis.Section_11_4

Analysis I, Section 11.7: A non-Riemann integrable function

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:

An example of a bounded function on a compact interval that is not Riemann integrable.

namespace Chapter11open BoundedInterval Chapter9

Proposition 11.7.1

theorem not_integrable : BddOn f_9_3_21 (Icc 0 1) ∧ ¬ IntegrableOn f_9_3_21 (Icc 0 1) := by⊢ BddOn f_9_3_21 ↑(Icc 0 1) ∧ ¬IntegrableOn f_9_3_21 (Icc 0 1)
  -- This proof is adapted from the structure of the original text.
  have hbdd: BddOn f_9_3_21 (Icc 0 1):= by⊢ BddOn f_9_3_21 ↑(Icc 0 1) ∧ ¬IntegrableOn f_9_3_21 (Icc 0 1)
    use 1h⊢ ∀ x ∈ ↑(Icc 0 1), |f_9_3_21 x| ≤ 1; intro x _hx:ℝa✝:x ∈ ↑(Icc 0 1)⊢ |f_9_3_21 x| ≤ 1; by_cases h: ∃ y:ℚ, y = xposx:ℝa✝:x ∈ ↑(Icc 0 1)h:∃ y, ↑y = x⊢ |f_9_3_21 x| ≤ 1negx:ℝa✝:x ∈ ↑(Icc 0 1)h:¬∃ y, ↑y = x⊢ |f_9_3_21 x| ≤ 1 <;>posx:ℝa✝:x ∈ ↑(Icc 0 1)h:∃ y, ↑y = x⊢ |f_9_3_21 x| ≤ 1negx:ℝa✝:x ∈ ↑(Icc 0 1)h:¬∃ y, ↑y = x⊢ |f_9_3_21 x| ≤ 1 simp [f_9_3_21, h]All goals completed! 🐙
  refine ⟨ hbdd, ?_ ⟩hbdd:BddOn f_9_3_21 ↑(Icc 0 1)⊢ ¬IntegrableOn f_9_3_21 (Icc 0 1)
  have hsup (P: Partition (Icc 0 1)) : ∀ J ∈ P.intervals, (sSup (f_9_3_21 '' (J:Set ℝ))) * |J|ₗ = |J|ₗ := by⊢ BddOn f_9_3_21 ↑(Icc 0 1) ∧ ¬IntegrableOn f_9_3_21 (Icc 0 1)
    intro J hJhbdd:BddOn f_9_3_21 ↑(Icc 0 1)P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervals⊢ sSup (f_9_3_21 '' ↑J) * J.length = J.length; by_cases hJ0: |J|ₗ = 0poshbdd:BddOn f_9_3_21 ↑(Icc 0 1)P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:J.length = 0⊢ sSup (f_9_3_21 '' ↑J) * J.length = J.lengthneghbdd:BddOn f_9_3_21 ↑(Icc 0 1)P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬J.length = 0⊢ sSup (f_9_3_21 '' ↑J) * J.length = J.length
    .poshbdd:BddOn f_9_3_21 ↑(Icc 0 1)P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:J.length = 0⊢ sSup (f_9_3_21 '' ↑J) * J.length = J.length simp [hJ0]All goals completed! 🐙
    have hJ0' := hJ0neghbdd:BddOn f_9_3_21 ↑(Icc 0 1)P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬J.length = 0hJ0':¬J.length = 0⊢ sSup (f_9_3_21 '' ↑J) * J.length = J.length
    rw [←length_of_subsingleton] at hJ0neghbdd:BddOn f_9_3_21 ↑(Icc 0 1)P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ sSup (f_9_3_21 '' ↑J) * J.length = J.length
    convert (one_mul _)h.e'_2.h.e'_5hbdd:BddOn f_9_3_21 ↑(Icc 0 1)P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ sSup (f_9_3_21 '' ↑J) = 1
    apply le_antisymmh.e'_2.h.e'_5.ahbdd:BddOn f_9_3_21 ↑(Icc 0 1)P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ sSup (f_9_3_21 '' ↑J) ≤ 1h.e'_2.h.e'_5.ahbdd:BddOn f_9_3_21 ↑(Icc 0 1)P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ 1 ≤ sSup (f_9_3_21 '' ↑J)
    .h.e'_2.h.e'_5.ahbdd:BddOn f_9_3_21 ↑(Icc 0 1)P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ sSup (f_9_3_21 '' ↑J) ≤ 1 apply csSup_leh.e'_2.h.e'_5.a.h₁hbdd:BddOn f_9_3_21 ↑(Icc 0 1)P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ (f_9_3_21 '' ↑J).Nonemptyh.e'_2.h.e'_5.a.h₂hbdd:BddOn f_9_3_21 ↑(Icc 0 1)P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ ∀ b ∈ f_9_3_21 '' ↑J, b ≤ 1
      .h.e'_2.h.e'_5.a.h₁hbdd:BddOn f_9_3_21 ↑(Icc 0 1)P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ (f_9_3_21 '' ↑J).Nonempty contrapose! hJ0h.e'_2.h.e'_5.a.h₁hbdd:BddOn f_9_3_21 ↑(Icc 0 1)P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0':¬J.length = 0hJ0:f_9_3_21 '' ↑J = ∅⊢ Subsingleton ↑↑J; simp_allAll goals completed! 🐙
      grindAll goals completed! 🐙
    apply le_csSup_of_le _ _ (show (1:ℝ) ≤ 1 by⊢ BddOn f_9_3_21 ↑(Icc 0 1) ∧ ¬IntegrableOn f_9_3_21 (Icc 0 1) norm_numAll goals completed! 🐙)
    .hbdd:BddOn f_9_3_21 ↑(Icc 0 1)P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ BddAbove (f_9_3_21 '' ↑J) rw [bddAbove_def]hbdd:BddOn f_9_3_21 ↑(Icc 0 1)P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ ∃ x, ∀ y ∈ f_9_3_21 '' ↑J, y ≤ x; use 1hhbdd:BddOn f_9_3_21 ↑(Icc 0 1)P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ ∀ y ∈ f_9_3_21 '' ↑J, y ≤ 1; grindAll goals completed! 🐙
    simp at hJ0'hbdd:BddOn f_9_3_21 ↑(Icc 0 1)P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':J.a < J.b⊢ 1 ∈ f_9_3_21 '' ↑J; choose z hz hz' using Dense.exists_between (Rat.denseRange_cast (𝕜 := ℝ)) hJ0'hbdd:BddOn f_9_3_21 ↑(Icc 0 1)P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':J.a < J.bz:ℝhz:z ∈ Set.range Rat.casthz':z ∈ Set.Ioo J.a J.b⊢ 1 ∈ f_9_3_21 '' ↑J
    simp at *P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0':J.a < J.bz:ℝhbdd:BddOn f_9_3_21 (Set.Icc 0 1)hJ0:(↑J).Nontrivialhz:∃ y, ↑y = zhz':J.a < z ∧ z < J.b⊢ ∃ y, ↑y ∈ ↑J; obtain ⟨ q, rfl ⟩ := hzP:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0':J.a < J.bhbdd:BddOn f_9_3_21 (Set.Icc 0 1)hJ0:(↑J).Nontrivialq:ℚhz':J.a < ↑q ∧ ↑q < J.b⊢ ∃ y, ↑y ∈ ↑J
    have hq_mem : (q:ℝ) ∈ (J:Set ℝ) := (subset_iff _ _).mp (Ioo_subset J) (byP:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0':J.a < J.bhbdd:BddOn f_9_3_21 (Set.Icc 0 1)hJ0:(↑J).Nontrivialq:ℚhz':J.a < ↑q ∧ ↑q < J.b⊢ ↑q ∈ ↑(Ioo J.a J.b) simp [hz']All goals completed! 🐙)
    exact ⟨q, hq_mem⟩All goals completed! 🐙
  have hupper (P: Partition (Icc 0 1)) : upper_riemann_sum f_9_3_21 P = 1 := by⊢ BddOn f_9_3_21 ↑(Icc 0 1) ∧ ¬IntegrableOn f_9_3_21 (Icc 0 1)
    simp [upper_riemann_sum]hbdd:BddOn f_9_3_21 ↑(Icc 0 1)hsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthP:Partition (Icc 0 1)⊢ ∑ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = 1
    calc
      _ = ∑ J ∈ P.intervals, |J|ₗ := byhbdd:BddOn f_9_3_21 ↑(Icc 0 1)hsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthP:Partition (Icc 0 1)⊢ ∑ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = ∑ J ∈ P.intervals, J.length apply Finset.sum_congr rflhbdd:BddOn f_9_3_21 ↑(Icc 0 1)hsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthP:Partition (Icc 0 1)⊢ ∀ x ∈ P.intervals, sSup (f_9_3_21 '' ↑x) * x.length = x.length; grindAll goals completed! 🐙
      _ = _ := byhbdd:BddOn f_9_3_21 ↑(Icc 0 1)hsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthP:Partition (Icc 0 1)⊢ ∑ J ∈ P.intervals, J.length = 1 simp [Partition.sum_of_length _ P]All goals completed! 🐙
  replace hupper : upper_integral f_9_3_21 (Icc 0 1) = 1 := by⊢ BddOn f_9_3_21 ↑(Icc 0 1) ∧ ¬IntegrableOn f_9_3_21 (Icc 0 1)
    simp [upper_integ_eq_inf_upper_sum hbdd, hupper]All goals completed! 🐙
  have hinf (P: Partition (Icc 0 1)) : ∀ J ∈ P.intervals, (sInf (f_9_3_21 '' (J:Set ℝ))) * |J|ₗ = 0 := by⊢ BddOn f_9_3_21 ↑(Icc 0 1) ∧ ¬IntegrableOn f_9_3_21 (Icc 0 1)
    intro J hJhbdd:BddOn f_9_3_21 ↑(Icc 0 1)hsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthhupper:upper_integral f_9_3_21 (Icc 0 1) = 1P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervals⊢ sInf (f_9_3_21 '' ↑J) * J.length = 0; by_cases hJ0: |J|ₗ = 0poshbdd:BddOn f_9_3_21 ↑(Icc 0 1)hsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthhupper:upper_integral f_9_3_21 (Icc 0 1) = 1P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:J.length = 0⊢ sInf (f_9_3_21 '' ↑J) * J.length = 0neghbdd:BddOn f_9_3_21 ↑(Icc 0 1)hsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthhupper:upper_integral f_9_3_21 (Icc 0 1) = 1P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬J.length = 0⊢ sInf (f_9_3_21 '' ↑J) * J.length = 0
    .poshbdd:BddOn f_9_3_21 ↑(Icc 0 1)hsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthhupper:upper_integral f_9_3_21 (Icc 0 1) = 1P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:J.length = 0⊢ sInf (f_9_3_21 '' ↑J) * J.length = 0 simp [hJ0]All goals completed! 🐙
    have hJ0' := hJ0neghbdd:BddOn f_9_3_21 ↑(Icc 0 1)hsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthhupper:upper_integral f_9_3_21 (Icc 0 1) = 1P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬J.length = 0hJ0':¬J.length = 0⊢ sInf (f_9_3_21 '' ↑J) * J.length = 0
    rw [←length_of_subsingleton] at hJ0neghbdd:BddOn f_9_3_21 ↑(Icc 0 1)hsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthhupper:upper_integral f_9_3_21 (Icc 0 1) = 1P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ sInf (f_9_3_21 '' ↑J) * J.length = 0
    convert (zero_mul _)h.e'_2.h.e'_5hbdd:BddOn f_9_3_21 ↑(Icc 0 1)hsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthhupper:upper_integral f_9_3_21 (Icc 0 1) = 1P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ sInf (f_9_3_21 '' ↑J) = 0
    apply le_antisymmh.e'_2.h.e'_5.ahbdd:BddOn f_9_3_21 ↑(Icc 0 1)hsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthhupper:upper_integral f_9_3_21 (Icc 0 1) = 1P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ sInf (f_9_3_21 '' ↑J) ≤ 0h.e'_2.h.e'_5.ahbdd:BddOn f_9_3_21 ↑(Icc 0 1)hsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthhupper:upper_integral f_9_3_21 (Icc 0 1) = 1P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ 0 ≤ sInf (f_9_3_21 '' ↑J)
    .h.e'_2.h.e'_5.ahbdd:BddOn f_9_3_21 ↑(Icc 0 1)hsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthhupper:upper_integral f_9_3_21 (Icc 0 1) = 1P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ sInf (f_9_3_21 '' ↑J) ≤ 0 apply csInf_le_of_le _ _ (show (0:ℝ) ≤ 0 by⊢ BddOn f_9_3_21 ↑(Icc 0 1) ∧ ¬IntegrableOn f_9_3_21 (Icc 0 1) norm_numAll goals completed! 🐙)
      .hbdd:BddOn f_9_3_21 ↑(Icc 0 1)hsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthhupper:upper_integral f_9_3_21 (Icc 0 1) = 1P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ BddBelow (f_9_3_21 '' ↑J) rw [bddBelow_def]hbdd:BddOn f_9_3_21 ↑(Icc 0 1)hsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthhupper:upper_integral f_9_3_21 (Icc 0 1) = 1P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ ∃ x, ∀ y ∈ f_9_3_21 '' ↑J, x ≤ y; use 0hhbdd:BddOn f_9_3_21 ↑(Icc 0 1)hsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthhupper:upper_integral f_9_3_21 (Icc 0 1) = 1P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ ∀ y ∈ f_9_3_21 '' ↑J, 0 ≤ y; grindAll goals completed! 🐙
      simp at hJ0'hbdd:BddOn f_9_3_21 ↑(Icc 0 1)hsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthhupper:upper_integral f_9_3_21 (Icc 0 1) = 1P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':J.a < J.b⊢ 0 ∈ f_9_3_21 '' ↑J
      choose z hz hz' using Dense.exists_between dense_irrational hJ0'hbdd:BddOn f_9_3_21 ↑(Icc 0 1)hsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthhupper:upper_integral f_9_3_21 (Icc 0 1) = 1P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':J.a < J.bz:ℝhz:z ∈ {x | Irrational x}hz':z ∈ Set.Ioo J.a J.b⊢ 0 ∈ f_9_3_21 '' ↑J
      simp at *hsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthhupper:upper_integral f_9_3_21 (Icc 0 1) = 1P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0':J.a < J.bz:ℝhz:Irrational zhbdd:BddOn f_9_3_21 (Set.Icc 0 1)hJ0:(↑J).Nontrivialhz':J.a < z ∧ z < J.b⊢ ∃ x ∈ ↑J, ∀ (x_1 : ℚ), ¬↑x_1 = x
      refine ⟨ z, (subset_iff _ _).mp (Ioo_subset J) (byhsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthhupper:upper_integral f_9_3_21 (Icc 0 1) = 1P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0':J.a < J.bz:ℝhz:Irrational zhbdd:BddOn f_9_3_21 (Set.Icc 0 1)hJ0:(↑J).Nontrivialhz':J.a < z ∧ z < J.b⊢ z ∈ ↑(Ioo J.a J.b) simp [hz']All goals completed! 🐙), ?_ ⟩
      intro qhsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthhupper:upper_integral f_9_3_21 (Icc 0 1) = 1P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0':J.a < J.bz:ℝhz:Irrational zhbdd:BddOn f_9_3_21 (Set.Icc 0 1)hJ0:(↑J).Nontrivialhz':J.a < z ∧ z < J.bq:ℚ⊢ ¬↑q = z; contrapose! hzhsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthhupper:upper_integral f_9_3_21 (Icc 0 1) = 1P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0':J.a < J.bz:ℝhbdd:BddOn f_9_3_21 (Set.Icc 0 1)hJ0:(↑J).Nontrivialhz':J.a < z ∧ z < J.bq:ℚhz:↑q = z⊢ ¬Irrational z; simp [←hz]All goals completed! 🐙
    apply le_csInfh.e'_2.h.e'_5.a.h₁hbdd:BddOn f_9_3_21 ↑(Icc 0 1)hsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthhupper:upper_integral f_9_3_21 (Icc 0 1) = 1P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ (f_9_3_21 '' ↑J).Nonemptyh.e'_2.h.e'_5.a.h₂hbdd:BddOn f_9_3_21 ↑(Icc 0 1)hsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthhupper:upper_integral f_9_3_21 (Icc 0 1) = 1P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ ∀ b ∈ f_9_3_21 '' ↑J, 0 ≤ b
    .h.e'_2.h.e'_5.a.h₁hbdd:BddOn f_9_3_21 ↑(Icc 0 1)hsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthhupper:upper_integral f_9_3_21 (Icc 0 1) = 1P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ (f_9_3_21 '' ↑J).Nonempty contrapose! hJ0h.e'_2.h.e'_5.a.h₁hbdd:BddOn f_9_3_21 ↑(Icc 0 1)hsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthhupper:upper_integral f_9_3_21 (Icc 0 1) = 1P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0':¬J.length = 0hJ0:f_9_3_21 '' ↑J = ∅⊢ Subsingleton ↑↑J; simp_allAll goals completed! 🐙
    grindAll goals completed! 🐙
  have hlower (P: Partition (Icc 0 1)) : lower_riemann_sum f_9_3_21 P = 0 := by⊢ BddOn f_9_3_21 ↑(Icc 0 1) ∧ ¬IntegrableOn f_9_3_21 (Icc 0 1)
    simp [lower_riemann_sum]hbdd:BddOn f_9_3_21 ↑(Icc 0 1)hsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthhupper:upper_integral f_9_3_21 (Icc 0 1) = 1hinf:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sInf (f_9_3_21 '' ↑J) * J.length = 0P:Partition (Icc 0 1)⊢ ∑ J ∈ P.intervals, sInf (f_9_3_21 '' ↑J) * J.length = 0; calc
      _ = ∑ J ∈ P.intervals, (0:ℝ) := byhbdd:BddOn f_9_3_21 ↑(Icc 0 1)hsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthhupper:upper_integral f_9_3_21 (Icc 0 1) = 1hinf:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sInf (f_9_3_21 '' ↑J) * J.length = 0P:Partition (Icc 0 1)⊢ ∑ J ∈ P.intervals, sInf (f_9_3_21 '' ↑J) * J.length = ∑ J ∈ P.intervals, 0 apply Finset.sum_congr rflhbdd:BddOn f_9_3_21 ↑(Icc 0 1)hsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthhupper:upper_integral f_9_3_21 (Icc 0 1) = 1hinf:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sInf (f_9_3_21 '' ↑J) * J.length = 0P:Partition (Icc 0 1)⊢ ∀ x ∈ P.intervals, sInf (f_9_3_21 '' ↑x) * x.length = 0; grindAll goals completed! 🐙
      _ = _ := byhbdd:BddOn f_9_3_21 ↑(Icc 0 1)hsup:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = J.lengthhupper:upper_integral f_9_3_21 (Icc 0 1) = 1hinf:∀ (P : Partition (Icc 0 1)), ∀ J ∈ P.intervals, sInf (f_9_3_21 '' ↑J) * J.length = 0P:Partition (Icc 0 1)⊢ ∑ J ∈ P.intervals, 0 = 0 simpAll goals completed! 🐙
  replace hlower : lower_integral f_9_3_21 (Icc 0 1) = 0 := by⊢ BddOn f_9_3_21 ↑(Icc 0 1) ∧ ¬IntegrableOn f_9_3_21 (Icc 0 1)
    simp [lower_integ_eq_sup_lower_sum hbdd, hlower]All goals completed! 🐙
  grindAll goals completed! 🐙

end Chapter11