Аналіз I, Глава 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

Вправа 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

Визначення 4.2.1 (Rationals)

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

Визначення 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

Лема 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)

Визначення 4.2.2 (Addition of rationals)

instance Section_4_2.Rat.mul_inst : Mul Rat

Лема 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)

Визначення 4.2.2 (Multiplication of rationals)

instance Section_4_2.Rat.neg_inst : Neg Rat

Лема 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

Визначення 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

Твердження 4.2.4 (laws of algebra) / Вправа 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

Твердження 4.2.4 (laws of algebra) / Вправа 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

Твердження 4.2.4 (laws of algebra) / Вправа 4.2.3

Equations

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

instance Section_4_2.Rat.instCommRing : CommRing Rat

Твердження 4.2.4 (laws of algebra) / Вправа 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

Твердження 4.2.4 (laws of algebra) / Вправа 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

(Не із книги) 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

Визначення 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

Визначення 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

Лема 4.2.7 (trichotomy of rationals) / Вправа 4.2.4

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

Лема 4.2.7 (trichotomy of rationals) / Вправа 4.2.4

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

Лема 4.2.7 (trichotomy of rationals) / Вправа 4.2.4

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

Лема 4.2.7 (trichotomy of rationals) / Вправа 4.2.4

instance Section_4_2.Rat.instLT : LT Rat

Визначення 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

Визначення 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

Твердження 4.2.9(a) (order trichotomy) / Вправа 4.2.5

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

Твердження 4.2.9(a) (order trichotomy) / Вправа 4.2.5

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

Твердження 4.2.9(a) (order trichotomy) / Вправа 4.2.5

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

Твердження 4.2.9(a) (order trichotomy) / Вправа 4.2.5

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

Твердження 4.2.9(b) (order is anti-symmetric) / Вправа 4.2.5

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

Твердження 4.2.9(c) (order is transitive) / Вправа 4.2.5

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

Твердження 4.2.9(d) (addition preserves order) / Вправа 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

Твердження 4.2.9(e) (positive multiplication preserves order) / Вправа 4.2.5

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

(Не із книги) 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

(Не із книги) 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

(Не із книги) 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

Вправа 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_78 }

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