Equivalence of reals

Аналіз I, Розділ 5, Епілог: Ізоморфізм із дійсними числами Mathlib

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

Відтепер Chapter5.Real : TypeChapter5.Real вважатиметься застарілим, і замість нього ми використовуватимемо стандартні дійсні числа ℝ : Typeℝ. Зокрема, для всіх наступних розділів слід використовувати повний API Mathlib для ℝ : Typeℝ замість API Chapter5.Real : TypeChapter5.Real.

Заповнення пропусків (sorries) тут потребує як API Chapter5.Real : TypeChapter5.Real, так і API Mathlib для стандартних дійсних чисел ℝ : Typeℝ. Таким чином, ці вправи є чудовою підготовкою до вищезгаданого переходу.

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

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

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

namespace Chapter5

@[ext]
structure DedekindCut where
  E : Set ℚ
  nonempty : E.Nonempty
  bounded : BddAbove E
  lower: IsLowerSet E
  nomax : ∀ q ∈ E, ∃ r ∈ E, r > q

theorem isLowerSet_iff (E: Set ℚ) : IsLowerSet E ↔ ∀ q r, r < q → q ∈ E → r ∈ E :=
  isLowerSet_iff_forall_lt

abbrev Real.toSet_Rat (x:Real) : Set ℚ := { q | (q:Real) < x }

lemma declaration uses 'sorry'Real.toSet_Rat_nonempty (x:Real) : x.toSet_Rat.Nonempty := byx:Real⊢ x.toSet_Rat.Nonempty sorryAll goals completed! 🐙

lemma declaration uses 'sorry'Real.toSet_Rat_bounded (x:Real) : BddAbove x.toSet_Rat := byx:Real⊢ BddAbove x.toSet_Rat sorryAll goals completed! 🐙

lemma declaration uses 'sorry'Real.toSet_Rat_lower (x:Real) : IsLowerSet x.toSet_Rat := byx:Real⊢ IsLowerSet x.toSet_Rat sorryAll goals completed! 🐙

lemma declaration uses 'sorry'Real.toSet_Rat_nomax {x:Real} : ∀ q ∈ x.toSet_Rat, ∃ r ∈ x.toSet_Rat, r > q := byx:Real⊢ ∀ q ∈ x.toSet_Rat, ∃ r ∈ x.toSet_Rat, r > q sorryAll goals completed! 🐙

abbrev Real.toCut (x:Real) : DedekindCut :=
 {
   E := x.toSet_Rat
   nonempty := x.toSet_Rat_nonempty
   bounded := x.toSet_Rat_bounded
   lower := x.toSet_Rat_lower
   nomax := x.toSet_Rat_nomax
 }

abbrev DedekindCut.toSet_Real (c: DedekindCut) : Set Real := (fun (q:ℚ) ↦ (q:Real)) '' c.E

lemma declaration uses 'sorry'DedekindCut.toSet_Real_nonempty (c: DedekindCut) : c.toSet_Real.Nonempty := byc:DedekindCut⊢ c.toSet_Real.Nonempty sorryAll goals completed! 🐙

lemma declaration uses 'sorry'DedekindCut.toSet_Real_bounded (c: DedekindCut) : BddAbove c.toSet_Real := byc:DedekindCut⊢ BddAbove c.toSet_Real sorryAll goals completed! 🐙

noncomputable abbrev DedekindCut.toReal (c: DedekindCut) : Real := sSup c.toSet_Real

lemma DedekindCut.toReal_isLUB (c: DedekindCut) : IsLUB c.toSet_Real c.toReal :=
  ExtendedReal.sSup_of_bounded c.toSet_Real_nonempty c.toSet_Real_bounded

noncomputable abbrev declaration uses 'sorry'declaration uses 'sorry'Real.equivCut : Real ≃ DedekindCut where
  toFun := toCut
  invFun := DedekindCut.toReal
  left_inv x := byx:Real⊢ x.toCut.toReal = x
    sorryAll goals completed! 🐙
  right_inv c := byc:DedekindCut⊢ c.toReal.toCut = c
    sorryAll goals completed! 🐙

end Chapter5

Тепер необхідно розробити аналогічні результати для дійсних чисел Mathlib.

abbrev Real.toSet_Rat (x:ℝ) : Set ℚ := { q | (q:ℝ) < x }

lemma declaration uses 'sorry'Real.toSet_Rat_nonempty (x:ℝ) : x.toSet_Rat.Nonempty := byx:ℝ⊢ x.toSet_Rat.Nonempty sorryAll goals completed! 🐙

lemma declaration uses 'sorry'Real.toSet_Rat_bounded (x:ℝ) : BddAbove x.toSet_Rat := byx:ℝ⊢ BddAbove x.toSet_Rat sorryAll goals completed! 🐙

lemma declaration uses 'sorry'Real.toSet_Rat_lower (x:ℝ) : IsLowerSet x.toSet_Rat := byx:ℝ⊢ IsLowerSet x.toSet_Rat sorryAll goals completed! 🐙

lemma declaration uses 'sorry'Real.toSet_Rat_nomax (x:ℝ) : ∀ q ∈ x.toSet_Rat, ∃ r ∈ x.toSet_Rat, r > q := byx:ℝ⊢ ∀ q ∈ x.toSet_Rat, ∃ r ∈ x.toSet_Rat, r > q sorryAll goals completed! 🐙

abbrev Real.toCut (x:ℝ) : Chapter5.DedekindCut :=
 {
   E := x.toSet_Rat
   nonempty := x.toSet_Rat_nonempty
   bounded := x.toSet_Rat_bounded
   lower := x.toSet_Rat_lower
   nomax := x.toSet_Rat_nomax
 }

namespace Chapter5abbrev DedekindCut.toSet_R (c: DedekindCut) : Set ℝ := (fun (q:ℚ) ↦ (q:ℝ)) '' c.E

lemma declaration uses 'sorry'DedekindCut.toSet_R_nonempty (c: DedekindCut) : c.toSet_R.Nonempty := byc:DedekindCut⊢ c.toSet_R.Nonempty sorryAll goals completed! 🐙

lemma declaration uses 'sorry'DedekindCut.toSet_R_bounded (c: DedekindCut) : BddAbove c.toSet_R := byc:DedekindCut⊢ BddAbove c.toSet_R sorryAll goals completed! 🐙

noncomputable abbrev DedekindCut.toR (c: DedekindCut) : ℝ := sSup c.toSet_R

lemma DedekindCut.toR_isLUB (c: DedekindCut) : IsLUB c.toSet_R c.toR :=
  isLUB_csSup c.toSet_R_nonempty c.toSet_R_bounded

end Chapter5

noncomputable abbrev declaration uses 'sorry'declaration uses 'sorry'Real.equivCut : ℝ ≃ Chapter5.DedekindCut where
  toFun := _root_.Real.toCut
  invFun := Chapter5.DedekindCut.toR
  left_inv x := byx:ℝ⊢ x.toCut.toR = x
    sorryAll goals completed! 🐙
  right_inv c := byc:Chapter5.DedekindCut⊢ c.toR.toCut = c
    sorryAll goals completed! 🐙

namespace Chapter5

Ізоморфізм між дійсними числами Розділу 5 та дійсними числами Mathlib.

noncomputable abbrev Real.equivR : Real ≃ ℝ := Real.equivCut.trans _root_.Real.equivCut.symm

lemma Real.equivR_iff (x : Real) (y : ℝ) : y = Real.equivR x ↔ y.toCut = x.toCut := byx:Realy:ℝ⊢ y = equivR x ↔ y.toCut = x.toCut
  simp only [equivR, Equiv.trans_apply, ←Equiv.apply_eq_iff_eq_symm_apply]x:Realy:ℝ⊢ _root_.Real.equivCut y = equivCut x ↔ y.toCut = x.toCut
  rflAll goals completed! 🐙

-- Щоб скористатися цим визначенням, нам знадобиться певний допоміжний апарат.
-----

-- Почнемо з того, що покажемо, як це працює для `ratCasts`
theorem declaration uses 'sorry'Real.equivR_ratCast {q: ℚ} : equivR q = (q: ℝ) := byq:ℚ⊢ equivR ↑q = ↑q
  sorryAll goals completed! 🐙

lemma Real.equivR_nat {n: ℕ} : equivR n = (n: ℝ) := equivR_ratCastlemma Real.equivR_int {n: ℤ} : equivR n = (n: ℝ) := equivR_ratCast

----

-- Далі ми хочемо налаштувати спосіб конвертації з Real `LIM` у ℝ `Real.mk`
-- Для цього нам знадобиться дещо:

-- Конвертація між поняттями послідовностей Коші
theorem declaration uses 'sorry'Sequence.IsCauchy.to_IsCauSeq {a: ℕ → ℚ} (ha: IsCauchy a) : IsCauSeq _root_.abs a := bya:ℕ → ℚha:(↑a).IsCauchy⊢ IsCauSeq _root_.abs a
  sorryAll goals completed! 🐙

-- Перетворення `IsCauchy` у `CauSeq`
abbrev Sequence.IsCauchy.CauSeq {a: ℕ → ℚ} : (ha: IsCauchy a) → CauSeq ℚ _root_.abs :=
  (⟨a, ·.to_IsCauSeq⟩)

-- Потім ми налаштовуємо перетворення з Sequence.Equiv у CauSeq.LimZero, оскільки
-- це є відношенням еквівалентності
example {a b: CauSeq ℚ abs} : a ≈ b ↔ CauSeq.LimZero (a - b) := bya:CauSeq ℚ absb:CauSeq ℚ abs⊢ a ≈ b ↔ (a - b).LimZero rflAll goals completed! 🐙

theorem declaration uses 'sorry'Sequence.Equiv.LimZero {a b: ℕ → ℚ} (ha: IsCauchy a) (hb: IsCauchy b) (h:Equiv a b)
  : CauSeq.LimZero (ha.CauSeq - hb.CauSeq) := bya:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchyh:Equiv a b⊢ (ha.CauSeq - hb.CauSeq).LimZero
    sorryAll goals completed! 🐙

-- Тепер ми можемо використовувати це для конвертації між різними функціями в Real.mk
theorem Real.mk_eq_mk {a b: ℕ → ℚ} (ha : Sequence.IsCauchy a) (hb : Sequence.IsCauchy b) (hab: Sequence.Equiv a b)
  : Real.mk ha.CauSeq = Real.mk hb.CauSeq := Real.mk_eq.mpr (hab.LimZero ha hb)

-- Обидва напрямки еквівалентності
theorem declaration uses 'sorry'Sequence.Equiv_iff_LimZero {a b: ℕ → ℚ} (ha: IsCauchy a) (hb: IsCauchy b)
  : Equiv a b ↔ CauSeq.LimZero (ha.CauSeq - hb.CauSeq) := bya:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchy⊢ Equiv a b ↔ (ha.CauSeq - hb.CauSeq).LimZero
    refine ⟨(·.LimZero ha hb), ?_⟩a:ℕ → ℚb:ℕ → ℚha:(↑a).IsCauchyhb:(↑b).IsCauchy⊢ (ha.CauSeq - hb.CauSeq).LimZero → Equiv a b
    sorryAll goals completed! 🐙

----
-- Ми створюємо кілька послідовностей Коші з корисними властивостями

-- Ми показуємо, що для будь-якої послідовності вона врешті-решт стане довільно близькою до свого LIM.
open Real in
theorem declaration uses 'sorry'Sequence.difference_approaches_zero {a: ℕ → ℚ} (ha: Sequence.IsCauchy a) :
  ∀ε > 0, ∃N, ∀n ≥ N, |LIM a - a n| ≤ (ε: ℚ) := bya:ℕ → ℚha:(↑a).IsCauchy⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, |LIM a - ↑(a n)| ≤ ↑ε
    sorryAll goals completed! 🐙

-- Існує послідовність Коші, яка повністю лежить вище свого LIM
theorem declaration uses 'sorry'Real.exists_equiv_above {a: ℕ → ℚ} (ha: Sequence.IsCauchy a)
  : ∃(b: ℕ → ℚ), Sequence.IsCauchy b ∧ Sequence.Equiv a b ∧ ∀n, LIM a ≤ b n := bya:ℕ → ℚha:(↑a).IsCauchy⊢ ∃ b, (↑b).IsCauchy ∧ Sequence.Equiv a b ∧ ∀ (n : ℕ), LIM a ≤ ↑(b n)
    sorryAll goals completed! 🐙

-- Існує послідовність Коші, яка повністю лежить нижче свого LIM
theorem declaration uses 'sorry'Real.exists_equiv_below {a: ℕ → ℚ} (ha: Sequence.IsCauchy a)
  : ∃(b: ℕ → ℚ), Sequence.IsCauchy b ∧ Sequence.Equiv a b ∧ ∀n, b n ≤ LIM a := bya:ℕ → ℚha:(↑a).IsCauchy⊢ ∃ b, (↑b).IsCauchy ∧ Sequence.Equiv a b ∧ ∀ (n : ℕ), ↑(b n) ≤ LIM a
    sorryAll goals completed! 🐙

Real.mk_le {f g : CauSeq ℚ abs} : Real.mk f ≤ Real.mk g ↔ f ≤ g

Real.mk_le_of_forall_le {f : CauSeq ℚ abs} {x : ℝ} (h : ∃ i, ∀ j ≥ i, ↑(↑f j) ≤ x) : Real.mk f ≤ x

Real.mk_const {x : ℚ} : Real.mk (CauSeq.const abs x) = ↑x

-- Перетворіть `Real` у `ℝ`, використовуючи послідовності Коші
-- ми можемо використовувати перетворення `Real.mk_eq`, щоб застосовувати різні послідовності для доведення різних частин
theorem declaration uses 'sorry'Real.equivR_eq' {a: ℕ → ℚ} (ha: Sequence.IsCauchy a)
  : (LIM a).equivR = Real.mk ha.CauSeq := bya:ℕ → ℚha:(↑a).IsCauchy⊢ equivR (LIM a) = Real.mk ha.CauSeq
    by_cases hq: ∃(q: ℚ), q = LIM apos._@._hyg.1523a:ℕ → ℚha:(↑a).IsCauchyhq:∃ q, ↑q = LIM a⊢ equivR (LIM a) = Real.mk ha.CauSeqneg._@._hyg.1523a:ℕ → ℚha:(↑a).IsCauchyhq:¬∃ q, ↑q = LIM a⊢ equivR (LIM a) = Real.mk ha.CauSeq
    ·pos._@._hyg.1523a:ℕ → ℚha:(↑a).IsCauchyhq:∃ q, ↑q = LIM a⊢ equivR (LIM a) = Real.mk ha.CauSeq sorryAll goals completed! 🐙
    show sSup (Rat.cast '' (LIM a).toSet_Rat) = _neg._@._hyg.1523a:ℕ → ℚha:(↑a).IsCauchyhq:¬∃ q, ↑q = LIM a⊢ sSup (Rat.cast '' (LIM a).toSet_Rat) = Real.mk ha.CauSeq
    refine IsLUB.csSup_eq ⟨?_, ?_⟩ (Set.Nonempty.image _ <| Real.toSet_Rat_nonempty _)neg.refine_1._@._hyg.1523a:ℕ → ℚha:(↑a).IsCauchyhq:¬∃ q, ↑q = LIM a⊢ Real.mk ha.CauSeq ∈ upperBounds (Rat.cast '' (LIM a).toSet_Rat)neg.refine_2._@._hyg.1523a:ℕ → ℚha:(↑a).IsCauchyhq:¬∃ q, ↑q = LIM a⊢ Real.mk ha.CauSeq ∈ lowerBounds (upperBounds (Rat.cast '' (LIM a).toSet_Rat))
    ·neg.refine_1._@._hyg.1523a:ℕ → ℚha:(↑a).IsCauchyhq:¬∃ q, ↑q = LIM a⊢ Real.mk ha.CauSeq ∈ upperBounds (Rat.cast '' (LIM a).toSet_Rat) -- покажіть, що `Real.mk ha.CauSeq` є верхньою межею
      intro _ hyneg.refine_1._@._hyg.1523a:ℕ → ℚha:(↑a).IsCauchyhq:¬∃ q, ↑q = LIM aa✝:ℝhy:a✝ ∈ Rat.cast '' (LIM a).toSet_Rat⊢ a✝ ≤ Real.mk ha.CauSeq
      obtain ⟨y, hy, h⟩ := Set.mem_image _ _ _ |>.mp hyneg.refine_1.intro.intro._@._hyg.1523a:ℕ → ℚha:(↑a).IsCauchyhq:¬∃ q, ↑q = LIM aa✝:ℝhy✝:a✝ ∈ Rat.cast '' (LIM a).toSet_Raty:ℚhy:y ∈ (LIM a).toSet_Rath:↑y = a✝⊢ a✝ ≤ Real.mk ha.CauSeq
      rw [← h, show (y: ℝ) = Real.mk (CauSeq.const _ y) from rfl]neg.refine_1.intro.intro._@._hyg.1523a:ℕ → ℚha:(↑a).IsCauchyhq:¬∃ q, ↑q = LIM aa✝:ℝhy✝:a✝ ∈ Rat.cast '' (LIM a).toSet_Raty:ℚhy:y ∈ (LIM a).toSet_Rath:↑y = a✝⊢ Real.mk (CauSeq.const _root_.abs y) ≤ Real.mk ha.CauSeq
      sorryAll goals completed! 🐙
    -- покажіть, що для будь-якої іншої верхньої межі `Real.mk ha.CauSeq` є меншим
    intro M hMneg.refine_2._@._hyg.1523a:ℕ → ℚha:(↑a).IsCauchyhq:¬∃ q, ↑q = LIM aM:ℝhM:M ∈ upperBounds (Rat.cast '' (LIM a).toSet_Rat)⊢ Real.mk ha.CauSeq ≤ M
    sorryAll goals completed! 🐙

lemma Real.equivR_eq (x: Real) : ∃(a : ℕ → ℚ) (ha: Sequence.IsCauchy a),
  x = LIM a ∧ x.equivR = Real.mk ha.CauSeq := byx:Real⊢ ∃ a, ∃ (ha : (↑a).IsCauchy), x = LIM a ∧ equivR x = Real.mk ha.CauSeq
    obtain ⟨a, ha, rfl⟩ := x.eq_limintro.introa:ℕ → ℚha:(↑a).IsCauchy⊢ ∃ a_1, ∃ (ha : (↑a_1).IsCauchy), LIM a = LIM a_1 ∧ equivR (LIM a) = Real.mk ha.CauSeq
    exact ⟨a, ha, rfl, equivR_eq' ha⟩All goals completed! 🐙

Ізоморфізм зберігає порядок та кільцеві операції

noncomputable abbrev declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Real.equivR_ordered_ring : Real ≃+*o ℝ where
  toEquiv := equivR
  map_add' := by⊢ ∀ (x y : Real), equivR.toFun (x + y) = equivR.toFun x + equivR.toFun y sorryAll goals completed! 🐙
  map_mul' := by⊢ ∀ (x y : Real), equivR.toFun (x * y) = equivR.toFun x * equivR.toFun y sorryAll goals completed! 🐙
  map_le_map_iff' := by⊢ ∀ {a b : Real}, equivR.toFun a ≤ equivR.toFun b ↔ a ≤ b sorryAll goals completed! 🐙

-- допоміжні твердження для конвертації властивостей між Real та ℝ
lemma Real.equivR_map_mul {x y : Real} : equivR (x * y) = equivR x * equivR y :=
  equivR_ordered_ring.map_mul _ _

lemma Real.equivR_map_inv {x: Real} : equivR (x⁻¹) = (equivR x)⁻¹ :=
  map_inv₀ equivR_ordered_ring _

theorem declaration uses 'sorry'Real.equivR_map_pos {x: Real} : 0 < x ↔ 0 < equivR x := byx:Real⊢ 0 < x ↔ 0 < equivR x sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Real.equivR_map_nonneg {x: Real} : 0 ≤ x ↔ 0 ≤ equivR x := byx:Real⊢ 0 ≤ x ↔ 0 ≤ equivR x sorryAll goals completed! 🐙

-- Доведення еквівалентності різних операцій піднесення до степеня
theorem declaration uses 'sorry'Real.pow_of_equivR (x:Real) (n:ℕ) : equivR (x^n) = (equivR x)^n := byx:Realn:ℕ⊢ equivR (x ^ n) = equivR x ^ n
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Real.zpow_of_equivR (x:Real) (n:ℤ) : equivR (x^n) = (equivR x)^n := byx:Realn:ℤ⊢ equivR (x ^ n) = equivR x ^ n
  sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Real.ratPow_of_equivR (x:Real) (q:ℚ) : equivR (x^q) = (equivR x)^(q:ℝ) := byx:Realq:ℚ⊢ equivR (x ^ q) = equivR x ^ ↑q
  sorryAll goals completed! 🐙

end Chapter5