Documentation

Analysis.Section_5_5

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

@[implicit_reducible]

instance Chapter5.ExtendedReal.inst_Top :

Top ExtendedReal

Mathlib prefers ⊤ to denote the +∞ element.

Equations

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

@[implicit_reducible]

instance Chapter5.ExtendedReal.inst_Bot :

Bot ExtendedReal

Mathlib prefers ⊥ to denote the -∞ element.

Equations

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

@[implicit_reducible]

instance Chapter5.ExtendedReal.coe_real :

Coe Real ExtendedReal

Equations

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

@[implicit_reducible]

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 of empty set).

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

Definition 5.5.10 (Supremum of unbounded set).

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 of bounded set).

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

@[implicit_reducible]

noncomputable instance Chapter5.Real.inst_SupSet :

Equations

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

@[implicit_reducible]

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)