Аналіз I, Розділ 5.3: Побудова дійсних чисел

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

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

• Поняття формального границі послідовності Коші.
• Побудова типу дійсних чисел Chapter5.Real.
• Базові арифметичні операції та властивості.

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

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

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

class Chapter5.CauchySequenceextends Chapter5.Sequence : Type

Клас послідовностей Коші, що починаються з нуля

• 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

Послідовність, що починається з нуля і є Коші, можна розглядати як послідовність Коші.

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

Твердження 5.3.3 / Вправа 5.3.1

instance Chapter5.CauchySequence.instSetoid : Setoid CauchySequence

Твердження 5.3.3 / Вправа 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

Будь-яка стала послідовність є послідовністю Коші.

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

У Lean зручно присвоювати "порожнє" значення 0 для LIM a, коли a не є послідовністю Коші. Це вимагає класичної логіки, оскільки властивість бути послідовністю Коші не є обчислюваною або вирішуваною.

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

Визначення 5.3.1 (Дійсні числа)

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

Визначення 5.3.1 (Дійсні числа)

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

Лема 5.3.6 (Сума послідовностей Коші є послідовністю Коші.)

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

Лема 5.3.7 (Сума еквівалентних послідовностей є еквівалентною.)

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

Лема 5.3.7 (Сума еквівалентних послідовностей є еквівалентною)

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

Лема 5.3.7 (Сума еквівалентних послідовностей є еквівалентною)

noncomputable instance Chapter5.Real.add_inst : Add Real

Визначення 5.3.4 (Додавання дійсних чисел)

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)

Визначення 5.3.4 (Додавання дійсних чисел)

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

Твердження 5.3.10 (Добуток послідовностей Коші є послідовністю Коші)

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

Твердження 5.3.10 (Добуток еквівалентних послідовностей є еквівалентним) / Вправа 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 (Добуток еквівалентних послідовностей є еквівалентним) / Вправа 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 (Добуток еквівалентних послідовностей є еквівалентним) / Вправа 5.3.2

noncomputable instance Chapter5.Real.mul_inst : Mul Real

Визначення 5.3.9 (Добуток дійсних чисел)

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

Вправа 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 розподіляється щодо додавання

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

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

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 комутує з запереченням

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

Можливо, тут можна опустити гіпотезу про послідовність Коші.

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

noncomputable instance Chapter5.Real.addGroup_inst : AddGroup Real

Твердження 5.3.11 (закони алгебри)

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 розподіляється щодо віднімання

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

ratCast розподіляється щодо віднімання

noncomputable instance Chapter5.Real.instAddCommGroup : AddCommGroup Real

Твердження 5.3.11 (закони алгебри)

Equations

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

noncomputable instance Chapter5.Real.instCommMonoid : CommMonoid Real

Твердження 5.3.11 (закони алгебри)

Equations

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

noncomputable instance Chapter5.Real.instCommRing : CommRing Real

Твердження 5.3.11 (закони алгебри)

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

Визначення 5.3.12 (послідовності, обмежені від нуля). Послідовності індексуються так, щоб починатися з нуля, оскільки це зручніше для цілей Mathlib.

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

Лема 5.3.14

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

Цей результат не був явно зазначений у тексті, але потрібен у теорії. Це гарна вправа, тож я залишаю її як таку.

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

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

Лема 5.3.17 (Операція взяття оберненого числа визначена коректно)

noncomputable instance Chapter5.Real.instInv : Inv Real

Визначення 5.3.16 (Взяття оберненого числа дійсних чисел). Вимагає класичної логіки, оскільки потрібно присвоїти "сміттєве" значення оберненому 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

Стандартне визначення ділення

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

Вправа 5.3.4

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

Те саме, що Sequence.IsCauchy.harmonic, але з перенумерацією послідовності як a₀ = 1, a₁ = 1/2, ... Ця форма зручніша для майбутнього доведення Теореми 5.5.9.

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

Вправа 5.3.5