Аналіз I, Розділ 4.2: Раціональні числа

Цей файл є перекладом розділу 4.2 книги Analysis I на Lean 4. Уся нумерація відповідає оригінальному тексту.

Я (пр.перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним рішенням Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підбуцнути", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Основні побудови та результати цього розділу:

• Визначення раціональних чисел «Розділу 4.2» Section_4_2.Rat як формальних часток a // b цілих чисел a b : ℤ, з точністю до еквівалентності. (Це фактортип допоміжного типу Section_4_2.PreRat, який складається з формальних часток без накладеної еквівалентності.)

• Операції поля та порядок на цих раціональних числах, а також вкладення ℕ і ℤ.

• Еквівалентність із раціональними числами Mathlib _root_.Rat (або ℚ), які ми надалі використовуватимемо.

Примітка: тут (і надалі) ми використовуємо натуральні числа ℕ та цілі числа ℤ із Mathlib, а не натуральні числа розділу 2 та цілі числа розділу 4.1.

Підказки від попередніх користувачів

Користувачі супровідного матеріалу, які виконали вправи в цьому розділі, можуть надсилати свої поради майбутнім користувачам цього розділу як PRи.

• (Додайте підказку тут)

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

Ми надаємо діленню «сміттєве» значення 0//1, якщо знаменник дорівнює нулю

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

Визначення 4.2.1 (Раціональні числа)

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

Визначення 4.2.1 (Раціональні числа)

instance Section_4_2.Rat.decidableEq : DecidableEq Rat

Розв’язність рівності. Підказка: змініть доведення DecidableEq Int із попереднього розділу. Однак, оскільки формальне ділення окремо обробляє випадок нульового знаменника, може бути зручніше уникати цієї операції та працювати безпосередньо з API Quotient.

Equations

• Section_4_2.Rat.decidableEq = sorry

instance Section_4_2.Rat.add_inst : Add Rat

Лема 4.2.3 (Додавання коректно визначене)

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 (Додавання раціональних чисел)

instance Section_4_2.Rat.mul_inst : Mul Rat

Лема 4.2.3 (Множення коректно визначене)

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 (Множення раціональних чисел)

instance Section_4_2.Rat.neg_inst : Neg Rat

Лема 4.2.3 (Протилежний елемент коректно визначени)

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

Визначення 4.2.2 (Протилежний елемент раціональних чисел)

instance Section_4_2.Rat.instIntCast : IntCast Rat

Вкладення цілих чисел у раціональні числа

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 розподіляється на наступника

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

intCast розподіляється на додавання

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

intCast розподіляється на множення

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

intCast комутує з взяттям протилежного елемента

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

instance Section_4_2.Rat.instInv : Inv Rat

У той час як у книзі обернене число для 0 залишається невизначеним, у Lean зручніше призначити цьому оберненому числу «сміттєве» значення; ми довільно обираємо це сміттєве значення рівним 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

Твердження 4.2.4 (закони алгебри) / Вправа 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

Твердження 4.2.4 (закони алгебри) / Вправа 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

Твердження 4.2.4 (закони алгебри) / Вправа 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 (закони алгебри) / Вправа 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

Твердження 4.2.4 (закони алгебри) / Вправа 4.2.3

Equations

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

theorem Section_4_2.Rat.sub_eq (a b : Rat) : a - b = a + -b

Визначення віднімання

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

Визначення 4.2.6 (позитивність)

Equations

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

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

Визначення 4.2.6 (негативність)

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 (трихотомія раціональних чисел) / Вправа 4.2.4

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

Лема 4.2.7 (трихотомія раціональних чисел) / Вправа 4.2.4

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

Лема 4.2.7 (трихотомія раціональних чисел) / Вправа 4.2.4

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

Лема 4.2.7 (трихотомія раціональних чисел) / Вправа 4.2.4

instance Section_4_2.Rat.instLT : LT Rat

Визначення 4.2.8 (Порядок раціональних чисел)

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 (Порядок раціональних чисел)

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

Твердження 4.2.9(a) (трихотомія порядку) / Вправа 4.2.5

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

Твердження 4.2.9(a) (трихотомія порядку) / Вправа 4.2.5

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

Твердження 4.2.9(a) (трихотомія порядку) / Вправа 4.2.5

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

Твердження 4.2.9(a) (трихотомія порядку) / Вправа 4.2.5

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

Твердження 4.2.9(b) (порядок є антисиметричним) / Вправа 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) (порядок є транзитивним) / Вправа 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) (додавання зберігає порядок) / Вправа 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) (множення на додатне число зберігає порядок) / Вправа 4.2.5

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

(Не в підручнику) Встановіть розв’язність цього порядку.

Equations

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

instance Section_4_2.Rat.instLinearOrder : LinearOrder Rat

(Не в підручнику) Раціональні числа мають структуру лінійного порядку.

Equations

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

instance Section_4_2.Rat.instIsStrictOrderedRing : IsStrictOrderedRing Rat

(Не в підручнику) Раціональні числа мають структуру строго впорядкованого кільця.

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 ≃ ℚ

Не в підручнику: створіть еквівалентність між Rat та ℚ. Це вимагає певного знайомства з API для версії раціональних чисел у Mathlib.

Equations

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

@[reducible, inline]

abbrev Section_4_2.Rat.equivRat_order : Rat ≃o ℚ

Не в підручнику: еквівалентність зберігає порядок

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 ≃+* ℚ

Не в підручнику: еквівалентність зберігає операції кільця

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

(Не в підручнику) Раціональні числа з підручника ізоморфні (як поле) до раціональних чисел Mathlib.

Equations

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