Analysis I, Section 4.2

This file is a translation of Section 4.2 of Analysis I to Lean 4. All numbering refers to the original text.

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:

• Definition of the "Section 4.2" rationals, Section_4_2.Rat, as formal quotients a // b of integers a b:ℤ, up to equivalence. (This is a quotient of a scaffolding type Section_4_2.PreRat, which consists of formal quotients without any equivalence imposed.)

• Field operations and order on these rationals, as well as an embedding of ℕ and ℤ.

• Equivalence with the Mathlib rationals _root_.Rat (or ℚ), which we will use going forward.

Note: here (and in the sequel) we use Mathlib's natural numbers ℕ and integers ℤ rather than the Chapter 2 natural numbers and Section 4.1 integers.

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)

structure Section_4_2.PreRat : Type

• numerator : ℤ
• denominator : ℤ
• nonzero : self.denominator ≠ 0

instance Section_4_2.PreRat.instSetoid : Setoid PreRat

Exercise 4.2.1

Equations

• Section_4_2.PreRat.instSetoid = { r := fun (a b : Section_4_2.PreRat) => a.numerator * b.denominator = b.numerator * a.denominator, iseqv := Section_4_2.PreRat.instSetoid._proof_1 }

@[simp]

theorem Section_4_2.PreRat.eq (a b c d : ℤ) (hb : b ≠ 0) (hd : d ≠ 0) : { numerator := a, denominator := b, nonzero := hb } ≈ { numerator := c, denominator := d, nonzero := hd } ↔ a * d = c * b

@[reducible, inline]

abbrev Section_4_2.Rat : Type

Equations

• Section_4_2.Rat = Quotient Section_4_2.PreRat.instSetoid

@[reducible, inline]

abbrev Section_4_2.Rat.formalDiv (a b : ℤ) : Rat

We give division a "junk" value of 0//1 if the denominator is zero

Equations

• a // b = ⟦if h : b ≠ 0 then { numerator := a, denominator := b, nonzero := h } else { numerator := 0, denominator := 1, nonzero := Section_4_2.Rat.formalDiv._proof_1 }⟧

def Section_4_2.«term_//_» : Lean.TrailingParserDescr

Equations

• Section_4_2.«term_//_» = Lean.ParserDescr.trailingNode `Section_4_2.«term_//_» 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " // ") (Lean.ParserDescr.cat `term 101))

theorem Section_4_2.Rat.eq (a c : ℤ) {b d : ℤ} (hb : b ≠ 0) (hd : d ≠ 0) : a // b = c // d ↔ a * d = c * b

Definition 4.2.1 (Rationals)

theorem Section_4_2.Rat.eq_diff (n : Rat) : ∃ (a : ℤ) (b : ℤ), b ≠ 0 ∧ n = a // b

Definition 4.2.1 (Rationals)

instance Section_4_2.Rat.decidableEq : DecidableEq Rat

Decidability of equality. Hint: modify the proof of DecidableEq Int from the previous section. However, because formal division handles the case of zero denominator separately, it may be more convenient to avoid that operation and work directly with the Quotient API.

Equations

• Section_4_2.Rat.decidableEq = sorry

instance Section_4_2.Rat.add_inst : Add Rat

Lemma 4.2.3 (Addition well-defined)

Equations

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

theorem Section_4_2.Rat.add_eq (a c : ℤ) {b d : ℤ} (hb : b ≠ 0) (hd : d ≠ 0) : a // b + c // d = (a * d + b * c) // (b * d)

Definition 4.2.2 (Addition of rationals)

instance Section_4_2.Rat.mul_inst : Mul Rat

Lemma 4.2.3 (Multiplication well-defined)

Equations

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

theorem Section_4_2.Rat.mul_eq (a c : ℤ) {b d : ℤ} (hb : b ≠ 0) (hd : d ≠ 0) : a // b * c // d = (a * c) // (b * d)

Definition 4.2.2 (Multiplication of rationals)

instance Section_4_2.Rat.neg_inst : Neg Rat

Lemma 4.2.3 (Negation well-defined)

Equations

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

theorem Section_4_2.Rat.neg_eq (a : ℤ) {b : ℤ} (hb : b ≠ 0) : -a // b = (-a) // b

Definition 4.2.2 (Negation of rationals)

instance Section_4_2.Rat.instIntCast : IntCast Rat

Embedding the integers in the rationals

Equations

• Section_4_2.Rat.instIntCast = { intCast := fun (a : ℤ) => a // 1 }

instance Section_4_2.Rat.instNatCast : NatCast Rat

Equations

• Section_4_2.Rat.instNatCast = { natCast := fun (n : ℕ) => ↑n // 1 }

instance Section_4_2.Rat.instOfNat {n : ℕ} : OfNat Rat n

Equations

• Section_4_2.Rat.instOfNat = { ofNat := ↑n // 1 }

theorem Section_4_2.Rat.coe_Int_eq (a : ℤ) : ↑a = a // 1

theorem Section_4_2.Rat.coe_Nat_eq (n : ℕ) : ↑n = ↑n // 1

theorem Section_4_2.Rat.of_Nat_eq (n : ℕ) : OfNat.ofNat n = ↑(OfNat.ofNat n) // 1

theorem Section_4_2.Rat.natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1

natCast distributes over successor

theorem Section_4_2.Rat.intCast_add (a b : ℤ) : ↑a + ↑b = ↑(a + b)

intCast distributes over addition

theorem Section_4_2.Rat.intCast_mul (a b : ℤ) : ↑a * ↑b = ↑(a * b)

intCast distributes over multiplication

theorem Section_4_2.Rat.intCast_neg (a : ℤ) : -↑a = ↑(-a)

intCast commutes with negation

theorem Section_4_2.Rat.coe_Int_inj : Function.Injective fun (n : ℤ) => ↑n

instance Section_4_2.Rat.instInv : Inv Rat

Whereas the book leaves the inverse of 0 undefined, it is more convenient in Lean to assign a "junk" value to this inverse; we arbitrarily choose this junk value to be 0.

Equations

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

theorem Section_4_2.Rat.inv_eq (a : ℤ) {b : ℤ} (hb : b ≠ 0) : (a // b)⁻¹ = b // a

@[simp]

theorem Section_4_2.Rat.inv_zero : 0⁻¹ = 0

instance Section_4_2.Rat.addGroup_inst : AddGroup Rat

Proposition 4.2.4 (laws of algebra) / Exercise 4.2.3

Equations

• Section_4_2.Rat.addGroup_inst = AddGroup.ofLeftAxioms Section_4_2.Rat.addGroup_inst._proof_1 Section_4_2.Rat.addGroup_inst._proof_2 Section_4_2.Rat.addGroup_inst._proof_3

instance Section_4_2.Rat.instAddCommGroup : AddCommGroup Rat

Proposition 4.2.4 (laws of algebra) / Exercise 4.2.3

Equations

• Section_4_2.Rat.instAddCommGroup = { toAddGroup := Section_4_2.Rat.addGroup_inst, add_comm := Section_4_2.Rat.instAddCommGroup._proof_1 }

instance Section_4_2.Rat.instCommMonoid : CommMonoid Rat

Proposition 4.2.4 (laws of algebra) / Exercise 4.2.3

Equations

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

instance Section_4_2.Rat.instCommRing : CommRing Rat

Proposition 4.2.4 (laws of algebra) / Exercise 4.2.3

Equations

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

instance Section_4_2.Rat.instRatCast : RatCast Rat

Equations

• Section_4_2.Rat.instRatCast = { ratCast := fun (q : ℚ) => q.num // ↑q.den }

theorem Section_4_2.Rat.ratCast_inj : Function.Injective fun (n : ℚ) => ↑n

theorem Section_4_2.Rat.coe_Rat_eq (a : ℤ) {b : ℤ} (hb : b ≠ 0) : ↑(↑a / ↑b) = a // b

instance Section_4_2.Rat.instDivInvMonoid : DivInvMonoid Rat

Default definition of division

Equations

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

theorem Section_4_2.Rat.div_eq (q r : Rat) : q / r = q * r⁻¹

instance Section_4_2.Rat.instField : Field Rat

Proposition 4.2.4 (laws of algebra) / Exercise 4.2.3

Equations

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

def Section_4_2.Rat.coe_int_hom : ℤ →+* Rat

Equations

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

def Section_4_2.Rat.isPos (q : Rat) : Prop

Definition 4.2.6 (positivity)

Equations

• q.isPos = ∃ (a : ℤ) (b : ℤ), a > 0 ∧ b > 0 ∧ q = ↑a / ↑b

def Section_4_2.Rat.isNeg (q : Rat) : Prop

Definition 4.2.6 (negativity)

Equations

• q.isNeg = ∃ (r : Section_4_2.Rat), r.isPos ∧ q = -r

theorem Section_4_2.Rat.trichotomous (x : Rat) : x = 0 ∨ x.isPos ∨ x.isNeg

Lemma 4.2.7 (trichotomy of rationals) / Exercise 4.2.4

theorem Section_4_2.Rat.not_zero_and_pos (x : Rat) : ¬(x = 0 ∧ x.isPos)

Lemma 4.2.7 (trichotomy of rationals) / Exercise 4.2.4

theorem Section_4_2.Rat.not_zero_and_neg (x : Rat) : ¬(x = 0 ∧ x.isNeg)

Lemma 4.2.7 (trichotomy of rationals) / Exercise 4.2.4

theorem Section_4_2.Rat.not_pos_and_neg (x : Rat) : ¬(x.isPos ∧ x.isNeg)

Lemma 4.2.7 (trichotomy of rationals) / Exercise 4.2.4

instance Section_4_2.Rat.instLT : LT Rat

Definition 4.2.8 (Ordering of the rationals)

Equations

• Section_4_2.Rat.instLT = { lt := fun (x y : Section_4_2.Rat) => (x - y).isNeg }

instance Section_4_2.Rat.instLE : LE Rat

Definition 4.2.8 (Ordering of the rationals)

Equations

• Section_4_2.Rat.instLE = { le := fun (x y : Section_4_2.Rat) => x < y ∨ x = y }

theorem Section_4_2.Rat.lt_iff (x y : Rat) : x < y ↔ (x - y).isNeg

theorem Section_4_2.Rat.le_iff (x y : Rat) : x ≤ y ↔ x < y ∨ x = y

theorem Section_4_2.Rat.gt_iff (x y : Rat) : x > y ↔ (x - y).isPos

theorem Section_4_2.Rat.ge_iff (x y : Rat) : x ≥ y ↔ x > y ∨ x = y

theorem Section_4_2.Rat.trichotomous' (x y : Rat) : x > y ∨ x < y ∨ x = y

Proposition 4.2.9(a) (order trichotomy) / Exercise 4.2.5

theorem Section_4_2.Rat.not_gt_and_lt (x y : Rat) : ¬(x > y ∧ x < y)

Proposition 4.2.9(a) (order trichotomy) / Exercise 4.2.5

theorem Section_4_2.Rat.not_gt_and_eq (x y : Rat) : ¬(x > y ∧ x = y)

Proposition 4.2.9(a) (order trichotomy) / Exercise 4.2.5

theorem Section_4_2.Rat.not_lt_and_eq (x y : Rat) : ¬(x < y ∧ x = y)

Proposition 4.2.9(a) (order trichotomy) / Exercise 4.2.5

theorem Section_4_2.Rat.antisymm (x y : Rat) : x < y ↔ y > x

Proposition 4.2.9(b) (order is anti-symmetric) / Exercise 4.2.5

theorem Section_4_2.Rat.lt_trans {x y z : Rat} (hxy : x < y) (hyz : y < z) : x < z

Proposition 4.2.9(c) (order is transitive) / Exercise 4.2.5

theorem Section_4_2.Rat.add_lt_add_right {x y : Rat} (z : Rat) (hxy : x < y) : x + z < y + z

Proposition 4.2.9(d) (addition preserves order) / Exercise 4.2.5

theorem Section_4_2.Rat.mul_lt_mul_right {x y z : Rat} (hxy : x < y) (hz : z.isPos) : x * z < y * z

Proposition 4.2.9(e) (positive multiplication preserves order) / Exercise 4.2.5

instance Section_4_2.Rat.decidableRel : DecidableRel fun (x1 x2 : Rat) => x1 ≤ x2

(Not from textbook) Establish the decidability of this order.

Equations

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

instance Section_4_2.Rat.instLinearOrder : LinearOrder Rat

(Not from textbook) Rat has the structure of a linear ordering.

Equations

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

instance Section_4_2.Rat.instIsStrictOrderedRing : IsStrictOrderedRing Rat

(Not from textbook) Rat has the structure of a strict ordered ring.

theorem Section_4_2.Rat.mul_lt_mul_right_of_neg (x y z : Rat) (hxy : x < y) (hz : z.isNeg) : x * z > y * z

Exercise 4.2.6

@[reducible, inline]

abbrev Section_4_2.Rat.equivRat : Rat ≃ ℚ

Not in textbook: create an equivalence between Rat and ℚ. This requires some familiarity with the API for Mathlib's version of the rationals.

Equations

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

@[reducible, inline]

abbrev Section_4_2.Rat.equivRat_order : Rat ≃o ℚ

Not in textbook: equivalence preserves order

Equations

• Section_4_2.Rat.equivRat_order = { toEquiv := Section_4_2.Rat.equivRat, map_rel_iff' := @Section_4_2.Rat.equivRat_order._proof_1 }

@[reducible, inline]

abbrev Section_4_2.Rat.equivRat_ring : Rat ≃+* ℚ

Not in textbook: equivalence preserves ring operations

Equations

• Section_4_2.Rat.equivRat_ring = { toEquiv := Section_4_2.Rat.equivRat, map_mul' := Section_4_2.Rat.equivRat_ring._proof_1, map_add' := Section_4_2.Rat.equivRat_ring._proof_2 }

def Section_4_2.Rat.equivRat_ring_symm : ℚ ≃+* Rat

(Not from textbook) The textbook rationals are isomorphic (as a field) to the Mathlib rationals.

Equations

• Section_4_2.Rat.equivRat_ring_symm = Section_4_2.Rat.equivRat_ring.symm