Documentation

Analysis.Section_5_5

Analysis I, Section 5.5: The least upper bound property #

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:

Upper bound and least upper bound on the real line

Tips from past users #

Users of the companion who have completed the exercises in this section are welcome to send their tips for future users in this section as PRs.

(Add tip here)

theorem Chapter5.Real.upperBound_def (E : Set Real) (M : Real) :

M ∈ upperBounds E ↔ ∀ x ∈ E, x ≤ M

Definition 5.5.1 (upper bounds). Here we use the upperBounds set defined in Mathlib.

theorem Chapter5.Real.lowerBound_def (E : Set Real) (M : Real) :

M ∈ lowerBounds E ↔ ∀ x ∈ E, x ≥ M

theorem Chapter5.Real.Icc_def (x y : Real) :

Set.Icc x y = {z : Real | x ≤ z ∧ z ≤ y}

API for Example 5.5.2

theorem Chapter5.Real.mem_Icc (x y z : Real) :

z ∈ Set.Icc x y ↔ x ≤ z ∧ z ≤ y

API for Example 5.5.2

theorem Chapter5.Real.Ioi_def (x : Real) :

Set.Ioi x = {z : Real | z > x}

API for Example 5.5.3

theorem Chapter5.Real.upperBound_upper {M M' : Real} (h : M ≤ M') {E : Set Real} (hb : M ∈ upperBounds E) :

M' ∈ upperBounds E

theorem Chapter5.Real.isLUB_def (E : Set Real) (M : Real) :

IsLUB E M ↔ M ∈ upperBounds E ∧ ∀ M' ∈ upperBounds E, M' ≥ M

Definition 5.5.5 (least upper bound). Here we use the isLUB predicate defined in Mathlib.

theorem Chapter5.Real.isGLB_def (E : Set Real) (M : Real) :

IsGLB E M ↔ M ∈ lowerBounds E ∧ ∀ M' ∈ lowerBounds E, M' ≤ M

theorem Chapter5.Real.LUB_unique {E : Set Real} {M M' : Real} (h1 : IsLUB E M) (h2 : IsLUB E M') :

M = M'

Proposition 5.5.8 (Uniqueness of least upper bound)

theorem Chapter5.Real.bddAbove_def (E : Set Real) :

BddAbove E ↔ ∃ (M : Real), M ∈ upperBounds E

definition of "bounded above", using Mathlib notation

theorem Chapter5.Real.bddBelow_def (E : Set Real) :

BddBelow E ↔ ∃ (M : Real), M ∈ lowerBounds E

theorem Chapter5.Real.upperBound_between {E : Set Real} {n : ℕ} {L K : ℤ} (hLK : L < K) (hK : ↑K * ↑(1 / (↑n + 1)) ∈ upperBounds E) (hL : ↑L * ↑(1 / (↑n + 1)) ∉ upperBounds E) :

∃ (m : ℤ), L < m ∧ m ≤ K ∧ ↑m * ↑(1 / (↑n + 1)) ∈ upperBounds E ∧ (↑m - 1) * ↑(1 / (↑n + 1)) ∉ upperBounds E

Exercise 5.5.2

theorem Chapter5.Real.upperBound_discrete_unique {E : Set Real} {n : ℕ} {m m' : ℤ} (hm1 : ↑(↑m / (↑n + 1)) ∈ upperBounds E) (hm2 : ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E) (hm'1 : ↑(↑m' / (↑n + 1)) ∈ upperBounds E) (hm'2 : ↑(↑m' / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E) :

m = m'

Exercise 5.5.3

theorem Chapter5.Sequence.IsCauchy.abs {a : ℕ → ℚ} (ha : (↑a).IsCauchy) :

(↑|a|).IsCauchy

Lemmas that can be helpful for proving 5.5.4

theorem Chapter5.Real.LIM.abs_eq {a b : ℕ → ℚ} (ha : (↑a).IsCauchy) (hb : (↑b).IsCauchy) (h : LIM a = LIM b) :

LIM |a| = LIM |b|

theorem Chapter5.Real.LIM.abs_eq_pos {a : ℕ → ℚ} (h : LIM a > 0) (ha : (↑a).IsCauchy) :

LIM a = LIM |a|

theorem Chapter5.Real.LIM_abs {a : ℕ → ℚ} (ha : (↑a).IsCauchy) :

|LIM a| = LIM |a|

theorem Chapter5.Real.LIM_of_le' {x : Real} {a : ℕ → ℚ} (hcauchy : (↑a).IsCauchy) (h : ∃ (N : ℕ), ∀ n ≥ N, ↑(a n) ≤ x) :

theorem Chapter5.Real.LIM_of_Cauchy {q : ℕ → ℚ} (hq : ∀ (M n : ℕ), n ≥ M → ∀ n' ≥ M, |q n - q n'| ≤ 1 / (↑M + 1)) :

(↑q).IsCauchy ∧ ∀ (M : ℕ), |↑(q M) - LIM q| ≤ 1 / (↑M + 1)

Exercise 5.5.4

theorem Chapter5.Real.LUB_claim1 (n : ℕ) {E : Set Real} (hE : E.Nonempty) (hbound : BddAbove E) :

∃! m : ℤ , ↑(↑m / (↑n + 1)) ∈ upperBounds E ∧ ↑(↑m / (↑n + 1) - 1 / (↑n + 1)) ∉ upperBounds E

The sequence m₁, m₂, … is well-defined. This proof uses a different indexing convention than the text

theorem Chapter5.Real.LUB_claim2 {E : Set Real} (N : ℕ) {a b : ℕ → ℚ} (hb : ∀ (n : ℕ), b n = 1 / (↑n + 1)) (hm1 : ∀ (n : ℕ), ↑(a n) ∈ upperBounds E) (hm2 : ∀ (n : ℕ), ↑((a - b) n) ∉ upperBounds E) (n : ℕ) :

n ≥ N → ∀ n' ≥ N, |a n - a n'| ≤ 1 / (↑N + 1)

theorem Chapter5.Real.LUB_exist {E : Set Real} (hE : E.Nonempty) (hbound : BddAbove E) :

∃ (S : Real), IsLUB E S

Theorem 5.5.9 (Existence of least upper bound)

inductive Chapter5.ExtendedReal :

A bare-bones extended real class to define supremum.

neg_infty : ExtendedReal
real (x : Real) : ExtendedReal
infty : ExtendedReal

Instances For

instance Chapter5.ExtendedReal.inst_Top :

Top ExtendedReal

Mathlib prefers ⊤ to denote the +∞ element.

Equations

Chapter5.ExtendedReal.inst_Top = { top := Chapter5.ExtendedReal.infty }

instance Chapter5.ExtendedReal.inst_Bot :

Bot ExtendedReal

Mathlib prefers ⊥ to denote the -∞ element.

Equations

Chapter5.ExtendedReal.inst_Bot = { bot := Chapter5.ExtendedReal.infty }

instance Chapter5.ExtendedReal.coe_real :

Coe Real ExtendedReal

Equations

Chapter5.ExtendedReal.coe_real = { coe := fun (x : Chapter5.Real) => Chapter5.ExtendedReal.real x }

instance Chapter5.ExtendedReal.real_coe :

Coe ExtendedReal Real

Equations

One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Chapter5.ExtendedReal.IsFinite (X : ExtendedReal) :

Equations

Instances For

theorem Chapter5.ExtendedReal.finite_eq_coe {X : ExtendedReal} (hX : X.IsFinite) :

X = real (match X with | neg_infty => 0 | real x => x | infty => 0)

@[reducible, inline]

noncomputable abbrev Chapter5.ExtendedReal.sup (E : Set Real) :

Definition 5.5.10 (Supremum)

Equations

Chapter5.ExtendedReal.sup E = if h1 : E.Nonempty then if h2 : BddAbove E then Chapter5.ExtendedReal.real ⋯.choose else ⊤ else ⊥

Instances For

theorem Chapter5.ExtendedReal.sup_of_empty :

Definition 5.5.10 (Supremum)

theorem Chapter5.ExtendedReal.sup_of_unbounded {E : Set Real} (hb : ¬BddAbove E) :

Definition 5.5.10 (Supremum)

theorem Chapter5.ExtendedReal.sup_of_bounded {E : Set Real} (hnon : E.Nonempty) (hb : BddAbove E) :

IsLUB E (match sup E with | neg_infty => 0 | real x => x | infty => 0)

Definition 5.5.10 (Supremum)

theorem Chapter5.ExtendedReal.sup_of_bounded_finite {E : Set Real} (hnon : E.Nonempty) (hb : BddAbove E) :

(sup E).IsFinite

theorem Chapter5.Real.exist_sqrt_two :

∃ (x : Real), x ^ 2 = 2

Proposition 5.5.12

theorem Chapter5.Real.exist_irrational :

∃ (x : Real), ¬∃ (q : ℚ), x = ↑q

Remark 5.5.13

theorem Chapter5.Real.mem_neg (E : Set Real) (x : Real) :

x ∈ -E ↔ -x ∈ E

Helper lemma for Exercise 5.5.1.

theorem Chapter5.Real.inf_neg {E : Set Real} {M : Real} (h : IsLUB E M) :

IsGLB (-E) (-M)

Exercise 5.5.1

theorem Chapter5.Real.GLB_exist {E : Set Real} (hE : E.Nonempty) (hbound : BddBelow E) :

∃ (S : Real), IsGLB E S

@[reducible, inline]

noncomputable abbrev Chapter5.ExtendedReal.inf (E : Set Real) :

Equations

Chapter5.ExtendedReal.inf E = if h1 : E.Nonempty then if h2 : BddBelow E then Chapter5.ExtendedReal.real ⋯.choose else ⊥ else ⊤

Instances For

theorem Chapter5.ExtendedReal.inf_of_empty :

theorem Chapter5.ExtendedReal.inf_of_unbounded {E : Set Real} (hb : ¬BddBelow E) :

theorem Chapter5.ExtendedReal.inf_of_bounded {E : Set Real} (hnon : E.Nonempty) (hb : BddBelow E) :

IsGLB E (match inf E with | neg_infty => 0 | real x => x | infty => 0)

theorem Chapter5.ExtendedReal.inf_of_bounded_finite {E : Set Real} (hnon : E.Nonempty) (hb : BddBelow E) :

(inf E).IsFinite

theorem Chapter5.Real.irrat_between {x y : Real} (hxy : x < y) :

∃ (z : Real), x < z ∧ z < y ∧ ¬∃ (q : ℚ), z = ↑q

Exercise 5.5.5

noncomputable instance Chapter5.Real.inst_SupSet :

Equations

One or more equations did not get rendered due to their size.

noncomputable instance Chapter5.Real.inst_conditionallyCompleteLattice :

ConditionallyCompleteLattice Real

Use the sSup operation to build a conditionally complete lattice structure on Real

Equations

Chapter5.Real.inst_conditionallyCompleteLattice = conditionallyCompleteLatticeOfLatticeOfsSup Chapter5.Real ⋯

theorem Chapter5.ExtendedReal.sSup_of_bounded {E : Set Real} (hnon : E.Nonempty) (hb : BddAbove E) :

IsLUB E (sSup E)