Аналіз I, Глава 2.3

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

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

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

Визначення множення та піднесення до степеня для натуральних чисел з "Розділу 2". Chapter2.Nat : TypeChapter2.Nat

Примітка: наприкінці цього розділу клас Chapter2.Nat : TypeChapter2.Nat буде замінено на користь стандартного класу Mathlib Nat : Type_root_.Nat, або ℕ : Typeℕ. Однак, ми пропрацюємо властивості Chapter2.Nat : TypeChapter2.Nat "вручну" в наступних кількох розділах для педагогічних цілей.

namespace Chapter2

Визначення 2.3.1 (Множення натуральних чисел)

abbrev Nat.mul (n m : Nat) : Nat := Nat.recurse (fun _ prod ↦ prod + m) 0 n

instance Nat.instMul : Mul Nat where
  mul := mul

Визначення 2.3.1 (Множення натуральних чисел)

theorem Nat.zero_mul (m: Nat) : 0 * m = 0 := recurse_zero (fun _ prod ↦ prod+m) _

Визначення 2.3.1 (Множення натуральних чисел)

theorem Nat.succ_mul (n m: Nat) : (n++) * m = n * m + m := recurse_succ (fun _ prod ↦ prod+m) _ _

theorem Nat.one_mul' (m: Nat) : 1 * m = 0 + m := bym:Nat⊢ 1 * m = 0 + m
  rw [←zero_succ, succ_mul, zero_mul]All goals completed! 🐙

theorem Nat.one_mul (m: Nat) : 1 * m = m := bym:Nat⊢ 1 * m = m
  rw [one_mul', zero_add]All goals completed! 🐙

theorem Nat.two_mul (m: Nat) : 2 * m = 0 + m + m := bym:Nat⊢ 2 * m = 0 + m + m
  rw [←one_succ, succ_mul, one_mul']All goals completed! 🐙

Ця лема буде корисною для доведення Леми 2.3.2.

lemma declaration uses 'sorry'Nat.mul_zero (n: Nat) : n * 0 = 0 := byn:Nat⊢ n * 0 = 0
  sorryAll goals completed! 🐙

Ця лема буде корисною для доведення Леми 2.3.2.

lemma declaration uses 'sorry'Nat.mul_succ (n m:Nat) : n * m++ = n * m + n := byn:Natm:Nat⊢ n * m++ = n * m + n
  sorryAll goals completed! 🐙

Лема 2.3.2 (Множення комутативне) / Вправа 2.3.1

lemma declaration uses 'sorry'Nat.mul_comm (n m: Nat) : n * m = m * n := byn:Natm:Nat⊢ n * m = m * n
  sorryAll goals completed! 🐙

theorem Nat.mul_one (m: Nat) : m * 1 = m := bym:Nat⊢ m * 1 = m
  rw [mul_comm, one_mul]All goals completed! 🐙

Лема 2.3.3 (Додатні натуральні числа не мають дільників на нуль) / Вправа 2.3.2

lemma declaration uses 'sorry'Nat.mul_eq_zero_iff (n m: Nat) : n * m = 0 ↔ n = 0 ∨ m = 0 := byn:Natm:Nat⊢ n * m = 0 ↔ n = 0 ∨ m = 0
  sorryAll goals completed! 🐙

lemma declaration uses 'sorry'Nat.pos_mul_pos {n m: Nat} (h₁: n.isPos) (h₂: m.isPos) : (n * m).isPos := byn:Natm:Nath₁:n.isPosh₂:m.isPos⊢ (n * m).isPos
  sorryAll goals completed! 🐙

Твердження 2.3.4 (Дістрібутивність)

theorem Nat.mul_add (a b c: Nat) : a * (b + c) = a * b + a * c := bya:Natb:Natc:Nat⊢ a * (b + c) = a * b + a * c
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  revert ca:Natb:Nat⊢ ∀ (c : Nat), a * (b + c) = a * b + a * c; apply inductionhbasea:Natb:Nat⊢ a * (b + 0) = a * b + a * 0hinda:Natb:Nat⊢ ∀ (n : Nat), a * (b + n) = a * b + a * n → a * (b + n++) = a * b + a * n++
  .hbasea:Natb:Nat⊢ a * (b + 0) = a * b + a * 0 rw [add_zero]hbasea:Natb:Nat⊢ a * b = a * b + a * 0
    rw [mul_zero, add_zero]All goals completed! 🐙
  intro c habchinda:Natb:Natc:Nathabc:a * (b + c) = a * b + a * c⊢ a * (b + c++) = a * b + a * c++
  rw [add_succ, mul_succ]hinda:Natb:Natc:Nathabc:a * (b + c) = a * b + a * c⊢ a * (b + c) + a = a * b + a * c++
  rw [mul_succ, ←add_assoc, ←habc]All goals completed! 🐙

Твердження 2.3.4 (Дістрібутивність)

theorem Nat.add_mul (a b c: Nat) : (a + b)*c = a*c + b*c := bya:Natb:Natc:Nat⊢ (a + b) * c = a * c + b * c
  simp only [mul_comm, mul_add]All goals completed! 🐙

Твердження 2.3.5 (Множення асоціативне) / Вправа 2.3.3

theorem declaration uses 'sorry'Nat.mul_assoc (a b c: Nat) : (a * b) * c = a * (b * c) := bya:Natb:Natc:Nat⊢ a * b * c = a * (b * c)
  sorryAll goals completed! 🐙

(Не із книги) Nat є комутативним півкільцем.

instance Nat.instCommSemiring : CommSemiring Nat where
  left_distrib := mul_add
  right_distrib := add_mul
  zero_mul := zero_mul
  mul_zero := mul_zero
  mul_assoc := mul_assoc
  one_mul := one_mul
  mul_one := mul_one
  mul_comm := mul_comm

Твердження 2.3.6 (Множення зберігає порядок)

theorem Nat.mul_lt_mul_of_pos_right {a b c: Nat} (h: a < b) (hc: c.isPos) : a * c < b * c := bya:Natb:Natc:Nath:a < bhc:c.isPos⊢ a * c < b * c
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  rw [lt_iff_add_pos] at ha:Natb:Natc:Nath:∃ d, d.isPos ∧ b = a + dhc:c.isPos⊢ a * c < b * c
  obtain ⟨ d, hdpos, hd ⟩ := hintro.introa:Natb:Natc:Nathc:c.isPosd:Nathdpos:d.isPoshd:b = a + d⊢ a * c < b * c
  apply_fun (· * c) at hdintro.introa:Natb:Natc:Nathc:c.isPosd:Nathdpos:d.isPoshd:b * c = (a + d) * c⊢ a * c < b * c
  rw [add_mul] at hdintro.introa:Natb:Natc:Nathc:c.isPosd:Nathdpos:d.isPoshd:b * c = a * c + d * c⊢ a * c < b * c
  have hdcpos : (d * c).isPos := pos_mul_pos hdpos hcintro.introa:Natb:Natc:Nathc:c.isPosd:Nathdpos:d.isPoshd:b * c = a * c + d * chdcpos:(d * c).isPos⊢ a * c < b * c
  rw [lt_iff_add_pos]intro.introa:Natb:Natc:Nathc:c.isPosd:Nathdpos:d.isPoshd:b * c = a * c + d * chdcpos:(d * c).isPos⊢ ∃ d, d.isPos ∧ b * c = a * c + d
  use d*cAll goals completed! 🐙

Твердження 2.3.6 (Множення зберігає порядок)

theorem Nat.mul_gt_mul_of_pos_right {a b c: Nat} (h: a > b) (hc: c.isPos) :
    a * c > b * c := mul_lt_mul_of_pos_right h hc

Твердження 2.3.6 (Множення зберігає порядок)

theorem Nat.mul_lt_mul_of_pos_left {a b c: Nat} (h: a < b) (hc: c.isPos) : c * a < c * b := bya:Natb:Natc:Nath:a < bhc:c.isPos⊢ c * a < c * b
  simp [mul_comm]a:Natb:Natc:Nath:a < bhc:c.isPos⊢ a * c < b * c
  exact mul_lt_mul_of_pos_right h hcAll goals completed! 🐙

Твердження 2.3.6 (Множення зберігає порядок)

theorem Nat.mul_gt_mul_of_pos_left {a b c: Nat} (h: a > b) (hc: c.isPos) :
    c * a > c * b := mul_lt_mul_of_pos_left h hc

Наслідок 2.3.7 (Властивість скорочення)

lemma Nat.mul_cancel_right {a b c: Nat} (h: a * c = b * c) (hc: c.isPos) : a = b := bya:Natb:Natc:Nath:a * c = b * chc:c.isPos⊢ a = b
  -- цей доказ написан так, щоб співпадати із структурою орігінального тексту.
  have := trichotomous a ba:Natb:Natc:Nath:a * c = b * chc:c.isPosthis:a < b ∨ a = b ∨ a > b⊢ a = b
  rcases this with hlt | heq | hgtinla:Natb:Natc:Nath:a * c = b * chc:c.isPoshlt:a < b⊢ a = binr.inla:Natb:Natc:Nath:a * c = b * chc:c.isPosheq:a = b⊢ a = binr.inra:Natb:Natc:Nath:a * c = b * chc:c.isPoshgt:a > b⊢ a = b
  .inla:Natb:Natc:Nath:a * c = b * chc:c.isPoshlt:a < b⊢ a = b replace hlt := mul_lt_mul_of_pos_right hlt hcinla:Natb:Natc:Nath:a * c = b * chc:c.isPoshlt:a * c < b * c⊢ a = b
    replace hlt := ne_of_lt _ _ hltinla:Natb:Natc:Nath:a * c = b * chc:c.isPoshlt:a * c ≠ b * c⊢ a = b
    contradictionAll goals completed! 🐙
  .inr.inla:Natb:Natc:Nath:a * c = b * chc:c.isPosheq:a = b⊢ a = b assumptionAll goals completed! 🐙
  replace hgt := mul_gt_mul_of_pos_right hgt hcinr.inra:Natb:Natc:Nath:a * c = b * chc:c.isPoshgt:a * c > b * c⊢ a = b
  replace hgt := ne_of_gt _ _ hgtinr.inra:Natb:Natc:Nath:a * c = b * chc:c.isPoshgt:a * c ≠ b * c⊢ a = b
  contradictionAll goals completed! 🐙

(Не із книги) Nat є впорядкованим півкільцем.

instance declaration uses 'sorry'Nat.isOrderedRing : IsOrderedRing Nat where
  zero_le_one := by⊢ 0 ≤ 1 sorryAll goals completed! 🐙
  mul_le_mul_of_nonneg_left := by⊢ ∀ (a b c : Nat), a ≤ b → 0 ≤ c → c * a ≤ c * b sorryAll goals completed! 🐙
  mul_le_mul_of_nonneg_right := by⊢ ∀ (a b c : Nat), a ≤ b → 0 ≤ c → a * c ≤ b * c sorryAll goals completed! 🐙

Твердження 2.3.9 (Лема про ділення Евкліда) / Вправа 2.3.5

theorem declaration uses 'sorry'Nat.exists_div_mod (n :Nat) {q: Nat} (hq: q.isPos) :
    ∃ m r: Nat, 0 ≤ r ∧ r < q ∧ n = m * q + r := byn:Natq:Nathq:q.isPos⊢ ∃ m r, 0 ≤ r ∧ r < q ∧ n = m * q + r
  sorryAll goals completed! 🐙

Визначення 2.3.11 (Піднесення до степеня для натуральних чисел)

abbrev Nat.pow (m n: Nat) : Nat := Nat.recurse (fun _ prod ↦ prod * m) 1 n

instance Nat.instPow : HomogeneousPow Nat where
  pow := Nat.pow

Визначення 2.3.11 (Піднесення до степеня для натуральних чисел)

theorem Nat.pow_zero (m: Nat) : m ^ (0:Nat) = 1 := recurse_zero (fun _ prod ↦ prod * m) _

Визначення 2.3.11 (Піднесення до степеня для натуральних чисел)

theorem Nat.zero_pow_zero : (0:Nat) ^ 0 = 1 := recurse_zero (fun _ prod ↦ prod * 0) _

Визначення 2.3.11 (Піднесення до степеня для натуральних чисел)

theorem Nat.pow_succ (m n: Nat) : (m:Nat) ^ n++ = m^n * m :=
  recurse_succ (fun _ prod ↦ prod * m) _ _

Вправа 2.3.4

theorem declaration uses 'sorry'Nat.sq_add_eq (a b: Nat) :
    (a + b) ^ (2 : Nat) = a ^ (2 : Nat) + 2 * a * b + b ^ (2 : Nat) := bya:Natb:Nat⊢ (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2
  sorryAll goals completed! 🐙

end Chapter2