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.Int, as formal differences 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 differences 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.

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_3 }⟧

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.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 {b : ℤ} (a : ℤ) (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.add_of_int (a b : ℤ) : ↑a + ↑b = ↑(a + b)

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

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

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 {b : ℤ} (a : ℤ) (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_8 Section_4_2.Rat.addGroup_inst._proof_9 Section_4_2.Rat.addGroup_inst._proof_10

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_11 }

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.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.equiv_rat : ℚ ≃+* Rat

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

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 z : 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).isPos

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) The order is decidable. This exercise is only recommended for Lean experts. Alternatively, one can establish this fact in classical logic via classical; exact Classical.decRel _

Equations

• Section_4_2.Rat.decidableRel = sorry

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_72 }

@[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_73, map_add' := Section_4_2.Rat.equivRat_ring._proof_74 }