Множення

Аналіз 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 "вручну" в наступних кількох розділах для педагогічних цілей.

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

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

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

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 (Множення натуральних чисел) Порівняйте із Mathlib-івської Chapter2.Nat.zero_mul (m : Nat) : 0 * m = 0Nat.zero_mul

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

Визначення 2.3.1 (Множення натуральних чисел) Порівняйте із Mathlib-івської Chapter2.Nat.succ_mul (n m : Nat) : n++ * m = n * m + mNat.succ_mul

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! 🐙

Порівняйте із Mathlib-овським Chapter2.Nat.one_mul (m : Nat) : 1 * m = mNat.one_mul

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. Порівняйте із Mathlib-івської Chapter2.Nat.mul_zero (n : Nat) : n * 0 = 0Nat.mul_zero

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

Ця лема буде корисною для доведення Леми 2.3.2. Порівняйте із Mathlib-івської Chapter2.Nat.mul_succ (n m : Nat) : n * m++ = n * m + nNat.mul_succ

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 Порівняйте із Mathlib-івської Chapter2.Nat.mul_comm (n m : Nat) : n * m = m * nNat.mul_comm

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

Порівняйте із Mathlib-овським Chapter2.Nat.mul_one (m : Nat) : m * 1 = mNat.mul_one

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. Порівняйте із Mathlib-овським Nat.mul_pos {n m : ℕ} (ha : n > 0) (hb : m > 0) : n * m > 0Nat.mul_pos

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.3 (Додатні натуральні числа не мають нульових дільників.) / Вправа 2.3.2. Порівняйте із Mathlib-овським Chapter2.Nat.mul_eq_zero (n m : Nat) : n * m = 0 ↔ n = 0 ∨ m = 0Nat.mul_eq_zero.

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

Твердження 2.3.4 (Дістрібутивність) Порівняйте із Mathlib-івської Chapter2.Nat.mul_add (a b c : Nat) : a * (b + c) = a * b + a * cNat.mul_add

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 (Дістрібутивність) Порівняйте із Mathlib-івської Chapter2.Nat.add_mul (a b c : Nat) : (a + b) * c = a * c + b * cNat.add_mul

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 Порівняйте із Mathlib-івської Chapter2.Nat.mul_assoc (a b c : Nat) : a * b * c = a * (b * c)Nat.mul_assoc

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 є комутативним півкільцем. Це дозволяє застосовувати такі тактики, як Unknown identifier `ring`ring, до натуральних чисел Розділу 2.

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

Ця ілюстрація тактики Unknown identifier `ring`ring не взята з підручника.

example (a b c d:ℕ) : (a+b)*1*(c+d) = d*b+a*c+c*b+a*d+0 := bya:ℕb:ℕc:ℕd:ℕ⊢ (a + b) * 1 * (c + d) = d * b + a * c + c * b + a * d + 0 ringAll goals completed! 🐙

Твердження 2.3.6 (Множення зберігає порядок) Порівняйте із Mathlib-івським Chapter2.Nat.mul_lt_mul_of_pos_right {a b c : Nat} (h : a < b) (hc : c.IsPos) : a * c < b * cNat.mul_lt_mul_of_pos_right

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
  choose d hdpos hd using ha:Natb:Natc:Nathc:c.IsPosd:Nathdpos:d.IsPoshd:b = a + d⊢ a * c < b * c
  replace hd := congr($hd * c)a:Natb:Natc:Nathc:c.IsPosd:Nathdpos:d.IsPoshd:?_mvar.4948 := id (congrArg (fun x => x * _fvar.4891) _fvar.4944)⊢ a * c < b * c
  rw [add_mul] at hda: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 hca:Natb:Natc:Nathc:c.IsPosd:Nathdpos:d.IsPoshd:b * c = a * c + d * chdcpos:Chapter2.Nat.IsPos (_fvar.4931 * _fvar.4891) := Chapter2.Nat.pos_mul_pos _fvar.4940 _fvar.4916⊢ a * c < b * c
  rw [lt_iff_add_pos]a:Natb:Natc:Nathc:c.IsPosd:Nathdpos:d.IsPoshd:b * c = a * c + d * chdcpos:Chapter2.Nat.IsPos (_fvar.4931 * _fvar.4891) := Chapter2.Nat.pos_mul_pos _fvar.4940 _fvar.4916⊢ ∃ 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 (Множення зберігає порядок) Порівняйте із Mathlib-івським Chapter2.Nat.mul_lt_mul_of_pos_left {a b c : Nat} (h : a < b) (hc : c.IsPos) : c * a < c * bNat.mul_lt_mul_of_pos_left

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 (Властивість скорочення) Порівняйте із Mathlib-овським Nat.mul_right_cancel {n m k : ℕ} (mp : 0 < m) (h : n * m = k * m) : n = kNat.mul_right_cancel

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:?_mvar.11884 := Chapter2.Nat.trichotomous _fvar.11877 _fvar.11878⊢ a = b
  obtain hlt | rfl | hgt := thisinla:Natb:Natc:Nath:a * c = b * chc:c.IsPoshlt:a < b⊢ a = binr.inla:Natc:Nathc:c.IsPosh:a * c = a * c⊢ a = ainr.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:?_mvar.11956 := Chapter2.Nat.mul_lt_mul_of_pos_right _fvar.11911 _fvar.11881⊢ a = b
    apply ne_of_lt at hltinla:Natb:Natc:Nath:a * c = b * chc:c.IsPoshlt:a * c ≠ b * c⊢ a = b
    contradictionAll goals completed! 🐙
  .inr.inla:Natc:Nathc:c.IsPosh:a * c = a * c⊢ a = a rflAll goals completed! 🐙
  replace hgt := mul_gt_mul_of_pos_right hgt hcinr.inra:Natb:Natc:Nath:a * c = b * chc:c.IsPoshgt:?_mvar.12001 := Chapter2.Nat.mul_gt_mul_of_pos_right _fvar.11939 _fvar.11881⊢ a = b
  apply ne_of_gt at hgtinr.inra:Natb:Natc:Nath:a * c = b * chc:c.IsPoshgt:a * c ≠ b * c⊢ a = b
  contradictionAll goals completed! 🐙

(Не в підручнику) Nat є впорядкованим півкільцем. Це дозволяє застосовувати такі тактики, як Unknown identifier `gcongr`gcongr, до натуральних чисел Розділу 2.

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! 🐙

Ця ілюстрація тактики Unknown identifier `gcongr`gcongr не взята з підручника.

example (a b c d:Nat) (hab: a ≤ b) : c*a*d ≤ c*b*d := bya:Natb:Natc:Natd:Nathab:a ≤ b⊢ c * a * d ≤ c * b * d
  gcongra0a:Natb:Natc:Natd:Nathab:a ≤ b⊢ 0 ≤ dh.a0a:Natb:Natc:Natd:Nathab:a ≤ b⊢ 0 ≤ c
  .a0a:Natb:Natc:Natd:Nathab:a ≤ b⊢ 0 ≤ d exact d.zero_leAll goals completed! 🐙
  exact c.zero_leAll goals completed! 🐙

Твердження 2.3.9 (Лема про ділення Евкліда) / Вправа 2.3.5 Порівняйте із Mathlib-івським Nat.mod_eq_iff {a b c : ℕ} : a % b = c ↔ b = 0 ∧ a = c ∨ c < b ∧ ∃ k, a = b * k + cNat.mod_eq_iff

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 (Піднесення до степеня для натуральних чисел) Порівняйте із Mathlib-івським Chapter2.Nat.pow_zero (m : Nat) : m ^ 0 = 1Nat.pow_zero

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

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

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

Визначення 2.3.11 (Піднесення до степеня для натуральних чисел) Порівняйте із Mathlib-івським Chapter2.Nat.pow_succ (m n : Nat) : m ^ n++ = m ^ n * mNat.pow_succ

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

Порівняйте із Mathlib-івським Chapter2.Nat.pow_one (m : Nat) : m ^ 1 = mNat.pow_one

@[simp]
theorem Nat.pow_one (m: Nat) : m ^ (1:Nat) = m := bym:Nat⊢ m ^ 1 = m
  rw [←zero_succ, pow_succ]m:Nat⊢ m ^ 0 * m = m; simpAll goals completed! 🐙

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