Analysis I, Section 5.3: The construction of the real numbers

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:

• Notion of a formal limit of a Cauchy sequence.
• Construction of a real number type Chapter5.Real.
• Basic arithmetic operations and properties.

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)

class Chapter5.CauchySequenceextends Chapter5.Sequence : Type

A class of Cauchy sequences that start at zero

• n₀ : ℤ
• seq : ℤ → ℚ
• vanish (n : ℤ) : n < self.n₀ → self.seq n = 0
• zero : self.n₀ = 0
• cauchy : self.IsCauchy

theorem Chapter5.CauchySequence.ext_iff {x y : CauchySequence} : x = y ↔ x.n₀ = y.n₀ ∧ x.seq = y.seq

theorem Chapter5.CauchySequence.ext {x y : CauchySequence} (n₀ : x.n₀ = y.n₀) (seq : x.seq = y.seq) : x = y

theorem Chapter5.CauchySequence.ext' {a b : CauchySequence} (h : a.seq = b.seq) : a = b

@[reducible, inline]

abbrev Chapter5.CauchySequence.mk' {a : ℕ → ℚ} (ha : (↑a).IsCauchy) : CauchySequence

A sequence starting at zero that is Cauchy, can be viewed as a Cauchy sequence.

Equations

• Chapter5.CauchySequence.mk' ha = { n₀ := 0, seq := (↑a).seq, vanish := ⋯, zero := Chapter5.CauchySequence.mk'._proof_2, cauchy := ha }

@[simp]

theorem Chapter5.CauchySequence.coe_eq {a : ℕ → ℚ} (ha : (↑a).IsCauchy) : (mk' ha).toSequence = ↑a

instance Chapter5.CauchySequence.instCoeFun : CoeFun CauchySequence fun (x : CauchySequence) => ℕ → ℚ

Equations

• Chapter5.CauchySequence.instCoeFun = { coe := fun (a : Chapter5.CauchySequence) (n : ℕ) => a.seq ↑n }

@[simp]

theorem Chapter5.CauchySequence.coe_to_sequence (a : CauchySequence) : (↑fun (n : ℕ) => a.seq ↑n) = a.toSequence

@[simp]

theorem Chapter5.CauchySequence.coe_coe {a : ℕ → ℚ} (ha : (↑a).IsCauchy) : (fun (n : ℕ) => (mk' ha).seq ↑n) = a

theorem Chapter5.Sequence.equiv_trans {a b c : ℕ → ℚ} (hab : Equiv a b) (hbc : Equiv b c) : Equiv a c

Proposition 5.3.3 / Exercise 5.3.1

instance Chapter5.CauchySequence.instSetoid : Setoid CauchySequence

Proposition 5.3.3 / Exercise 5.3.1

Equations

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

theorem Chapter5.CauchySequence.equiv_iff (a b : CauchySequence) : a ≈ b ↔ Sequence.Equiv (fun (n : ℕ) => a.seq ↑n) fun (n : ℕ) => b.seq ↑n

theorem Chapter5.Sequence.IsCauchy.const (a : ℚ) : (↑fun (x : ℕ) => a).IsCauchy

Every constant sequence is Cauchy

instance Chapter5.CauchySequence.instZero : Zero CauchySequence

Equations

• Chapter5.CauchySequence.instZero = { zero := Chapter5.CauchySequence.mk' Chapter5.CauchySequence.instZero._proof_1 }

@[reducible, inline]

abbrev Chapter5.Real : Type

Equations

• Chapter5.Real = Quotient Chapter5.CauchySequence.instSetoid

@[reducible, inline]

noncomputable abbrev Chapter5.LIM (a : ℕ → ℚ) : Real

It is convenient in Lean to assign the "dummy" value of 0 to LIM a when a is not Cauchy. This requires Classical logic, because the property of being Cauchy is not computable or decidable.

Equations

• Chapter5.LIM a = ⟦if h : (↑a).IsCauchy then Chapter5.CauchySequence.mk' h else 0⟧

theorem Chapter5.LIM_def {a : ℕ → ℚ} (ha : (↑a).IsCauchy) : LIM a = ⟦CauchySequence.mk' ha⟧

theorem Chapter5.Real.eq_lim (x : Real) : ∃ (a : ℕ → ℚ), (↑a).IsCauchy ∧ x = LIM a

Definition 5.3.1 (Real numbers)

theorem Chapter5.Real.LIM_eq_LIM {a b : ℕ → ℚ} (ha : (↑a).IsCauchy) (hb : (↑b).IsCauchy) : LIM a = LIM b ↔ Sequence.Equiv a b

Definition 5.3.1 (Real numbers)

theorem Chapter5.Sequence.IsCauchy.add {a b : ℕ → ℚ} (ha : (↑a).IsCauchy) (hb : (↑b).IsCauchy) : (↑(a + b)).IsCauchy

Lemma 5.3.6 (Sum of Cauchy sequences is Cauchy)

theorem Chapter5.Sequence.add_equiv_left {a a' : ℕ → ℚ} (b : ℕ → ℚ) (haa' : Equiv a a') : Equiv (a + b) (a' + b)

Lemma 5.3.7 (Sum of equivalent sequences is equivalent)

theorem Chapter5.Sequence.add_equiv_right {b b' : ℕ → ℚ} (a : ℕ → ℚ) (hbb' : Equiv b b') : Equiv (a + b) (a + b')

Lemma 5.3.7 (Sum of equivalent sequences is equivalent)

theorem Chapter5.Sequence.add_equiv {a b a' b' : ℕ → ℚ} (haa' : Equiv a a') (hbb' : Equiv b b') : Equiv (a + b) (a' + b')

Lemma 5.3.7 (Sum of equivalent sequences is equivalent)

noncomputable instance Chapter5.Real.add_inst : Add Real

Definition 5.3.4 (Addition of reals)

Equations

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

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

Definition 5.3.4 (Addition of reals)

theorem Chapter5.Sequence.IsCauchy.mul {a b : ℕ → ℚ} (ha : (↑a).IsCauchy) (hb : (↑b).IsCauchy) : (↑(a * b)).IsCauchy

Proposition 5.3.10 (Product of Cauchy sequences is Cauchy)

theorem Chapter5.Sequence.mul_equiv_left {a a' : ℕ → ℚ} (b : ℕ → ℚ) (hb : (↑b).IsCauchy) (haa' : Equiv a a') : Equiv (a * b) (a' * b)

Proposition 5.3.10 (Product of equivalent sequences is equivalent) / Exercise 5.3.2

theorem Chapter5.Sequence.mul_equiv_right {b b' : ℕ → ℚ} (a : ℕ → ℚ) (ha : (↑a).IsCauchy) (hbb' : Equiv b b') : Equiv (a * b) (a * b')

Proposition 5.3.10 (Product of equivalent sequences is equivalent) / Exercise 5.3.2

theorem Chapter5.Sequence.mul_equiv {a b a' b' : ℕ → ℚ} (ha : (↑a).IsCauchy) (hb' : (↑b').IsCauchy) (haa' : Equiv a a') (hbb' : Equiv b b') : Equiv (a * b) (a' * b')

Proposition 5.3.10 (Product of equivalent sequences is equivalent) / Exercise 5.3.2

noncomputable instance Chapter5.Real.mul_inst : Mul Real

Definition 5.3.9 (Product of reals)

Equations

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

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

instance Chapter5.Real.instRatCast : RatCast Real

Equations

• Chapter5.Real.instRatCast = { ratCast := fun (q : ℚ) => ⟦Chapter5.CauchySequence.mk' ⋯⟧ }

theorem Chapter5.Real.ratCast_def (q : ℚ) : ↑q = LIM fun (x : ℕ) => q

@[simp]

theorem Chapter5.Real.ratCast_inj (q r : ℚ) : ↑q = ↑r ↔ q = r

Exercise 5.3.3

instance Chapter5.Real.instOfNat {n : ℕ} : OfNat Real n

Equations

• Chapter5.Real.instOfNat = { ofNat := ↑↑n }

instance Chapter5.Real.instNatCast : NatCast Real

Equations

• Chapter5.Real.instNatCast = { natCast := fun (n : ℕ) => ↑↑n }

@[simp]

theorem Chapter5.Real.LIM.zero : (LIM fun (x : ℕ) => 0) = 0

instance Chapter5.Real.instIntCast : IntCast Real

Equations

• Chapter5.Real.instIntCast = { intCast := fun (n : ℤ) => ↑↑n }

theorem Chapter5.Real.ratCast_add (a b : ℚ) : ↑a + ↑b = ↑(a + b)

ratCast distributes over addition

theorem Chapter5.Real.ratCast_mul (a b : ℚ) : ↑a * ↑b = ↑(a * b)

ratCast distributes over multiplication

noncomputable instance Chapter5.Real.instNeg : Neg Real

Equations

• Chapter5.Real.instNeg = { neg := fun (x : Chapter5.Real) => ↑(-1) * x }

theorem Chapter5.Real.neg_ratCast (a : ℚ) : -↑a = ↑(-a)

ratCast commutes with negation

theorem Chapter5.Real.neg_LIM (a : ℕ → ℚ) (ha : (↑a).IsCauchy) : -LIM a = LIM (-a)

It may be possible to omit the Cauchy sequence hypothesis here.

theorem Chapter5.Real.IsCauchy.neg (a : ℕ → ℚ) (ha : (↑a).IsCauchy) : (↑(-a)).IsCauchy

noncomputable instance Chapter5.Real.addGroup_inst : AddGroup Real

Proposition 5.3.11 (laws of algebra)

Equations

• Chapter5.Real.addGroup_inst = AddGroup.ofLeftAxioms Chapter5.Real.addGroup_inst._proof_1 Chapter5.Real.addGroup_inst._proof_2 Chapter5.Real.addGroup_inst._proof_3

theorem Chapter5.Real.sub_eq_add_neg (x y : Real) : x - y = x + -y

theorem Chapter5.Sequence.IsCauchy.sub {a b : ℕ → ℚ} (ha : (↑a).IsCauchy) (hb : (↑b).IsCauchy) : (↑(a - b)).IsCauchy

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

LIM distributes over subtraction

theorem Chapter5.Real.ratCast_sub (a b : ℚ) : ↑a - ↑b = ↑(a - b)

ratCast distributes over subtraction

noncomputable instance Chapter5.Real.instAddCommGroup : AddCommGroup Real

Proposition 5.3.11 (laws of algebra)

Equations

• Chapter5.Real.instAddCommGroup = { toAddGroup := Chapter5.Real.addGroup_inst, add_comm := Chapter5.Real.instAddCommGroup._proof_1 }

noncomputable instance Chapter5.Real.instCommMonoid : CommMonoid Real

Proposition 5.3.11 (laws of algebra)

Equations

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

noncomputable instance Chapter5.Real.instCommRing : CommRing Real

Proposition 5.3.11 (laws of algebra)

Equations

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

@[reducible, inline]

abbrev Chapter5.Real.ratCast_hom : ℚ →+* Real

Equations

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

@[reducible, inline]

abbrev Chapter5.BoundedAwayZero (a : ℕ → ℚ) : Prop

Definition 5.3.12 (sequences bounded away from zero). Sequences are indexed to start from zero as this is more convenient for Mathlib purposes.

Equations

• Chapter5.BoundedAwayZero a = ∃ c > 0, ∀ (n : ℕ), |a n| ≥ c

theorem Chapter5.bounded_away_zero_def (a : ℕ → ℚ) : BoundedAwayZero a ↔ ∃ c > 0, ∀ (n : ℕ), |a n| ≥ c

theorem Chapter5.Real.boundedAwayZero_of_nonzero {x : Real} (hx : x ≠ 0) : ∃ (a : ℕ → ℚ), (↑a).IsCauchy ∧ BoundedAwayZero a ∧ x = LIM a

Lemma 5.3.14

theorem Chapter5.Real.lim_of_boundedAwayZero {a : ℕ → ℚ} (ha : BoundedAwayZero a) (ha_cauchy : (↑a).IsCauchy) : LIM a ≠ 0

This result was not explicitly stated in the text, but is needed in the theory. It's a good exercise, so I'm setting it as such.

theorem Chapter5.Real.nonzero_of_boundedAwayZero {a : ℕ → ℚ} (ha : BoundedAwayZero a) (n : ℕ) : a n ≠ 0

theorem Chapter5.Real.inv_isCauchy_of_boundedAwayZero {a : ℕ → ℚ} (ha : BoundedAwayZero a) (ha_cauchy : (↑a).IsCauchy) : (↑a⁻¹).IsCauchy

Lemma 5.3.15

theorem Chapter5.Real.inv_of_equiv {a b : ℕ → ℚ} (ha : BoundedAwayZero a) (ha_cauchy : (↑a).IsCauchy) (hb : BoundedAwayZero b) (hb_cauchy : (↑b).IsCauchy) (hlim : LIM a = LIM b) : LIM a⁻¹ = LIM b⁻¹

Lemma 5.3.17 (Reciprocation is well-defined)

noncomputable instance Chapter5.Real.instInv : Inv Real

Definition 5.3.16 (Reciprocation of real numbers). Requires classical logic because we need to assign a "junk" value to the inverse of 0.

Equations

• Chapter5.Real.instInv = { inv := fun (x : Chapter5.Real) => if h : x ≠ 0 then Chapter5.LIM ⋯.choose⁻¹ else 0 }

theorem Chapter5.Real.inv_def {a : ℕ → ℚ} (h : BoundedAwayZero a) (hc : (↑a).IsCauchy) : (LIM a)⁻¹ = LIM a⁻¹

@[simp]

theorem Chapter5.Real.inv_zero : 0⁻¹ = 0

theorem Chapter5.Real.self_mul_inv {x : Real} (hx : x ≠ 0) : x * x⁻¹ = 1

theorem Chapter5.Real.inv_mul_self {x : Real} (hx : x ≠ 0) : x⁻¹ * x = 1

theorem Chapter5.BoundedAwayZero.const {q : ℚ} (hq : q ≠ 0) : BoundedAwayZero fun (x : ℕ) => q

theorem Chapter5.Real.inv_ratCast (q : ℚ) : (↑q)⁻¹ = ↑q⁻¹

noncomputable instance Chapter5.Real.instDivInvMonoid : DivInvMonoid Real

Default definition of division

Equations

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

theorem Chapter5.Real.div_eq (x y : Real) : x / y = x * y⁻¹

noncomputable instance Chapter5.Real.instField : Field Real

Equations

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

theorem Chapter5.Real.mul_right_cancel₀ {x y z : Real} (hz : z ≠ 0) (h : x * z = y * z) : x = y

theorem Chapter5.Real.mul_right_nocancel : ¬∀ (x y z : Real), z = 0 → x * z = y * z → x = y

theorem Chapter5.Real.IsBounded.equiv {a b : ℕ → ℚ} (ha : (↑a).IsBounded) (hab : Sequence.Equiv a b) : (↑b).IsBounded

Exercise 5.3.4

theorem Chapter5.Sequence.IsCauchy.harmonic' : (↑fun (n : ℕ) => 1 / (↑n + 1)).IsCauchy

Same as Sequence.IsCauchy.harmonic but reindexing the sequence as a₀ = 1, a₁ = 1/2, ... This form is more convenient for the upcoming proof of Theorem 5.5.9.

theorem Chapter5.Real.LIM.harmonic : (LIM fun (n : ℕ) => 1 / (↑n + 1)) = 0

Exercise 5.3.5