Absolute value and exponentiation

Аналіз I, Розділ 4.3: Абсолютні значення та піднесення до степеня

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

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

Базові властивості абсолютного значення та піднесення до степеня для раціональних чисел (тут ми використовуємо раціональні числа Mathlib ℚ : Typeℚ, а не раціональні числа розділу 4.2).

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

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

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

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

Це визначення потрібно зробити поза простором імен Розділу 4.3 з технічних причин.

def Rat.Close (ε : ℚ) (x y:ℚ) := |x-y| ≤ ε

namespace Section_4_3

Визначення 4.3.1 (Абсолютне значення)

abbrev abs (x:ℚ) : ℚ := if x > 0 then x else (if x < 0 then -x else 0)

theorem abs_of_pos {x: ℚ} (hx: 0 < x) : abs x = x := byx:ℚhx:0 < x⊢ abs x = x grindAll goals completed! 🐙

Визначення 4.3.1 (Абсолютне значення)

theorem abs_of_neg {x: ℚ} (hx: x < 0) : abs x = -x := byx:ℚhx:x < 0⊢ abs x = -x grindAll goals completed! 🐙

Визначення 4.3.1 (Абсолютне значення)

theorem abs_of_zero : abs 0 = 0 := rfl

(Не в підручнику) Це визначення абсолютного значення збігається з визначенням у Mathlib. Надалі ми використовуємо абсолютне значення Mathlib.

theorem declaration uses 'sorry'abs_eq_abs (x: ℚ) : abs x = |x| := byx:ℚ⊢ abs x = |x|
  sorryAll goals completed! 🐙

abbrev dist (x y : ℚ) := |x - y|

Визначення 4.2 (Відстань). Тут ми уникаємо поняття відстані з Mathlib, оскільки воно має дійсні значення.

theorem dist_eq (x y: ℚ) : dist x y = |x-y| := rfl

Твердження 4.3.3(a) / Вправа 4.3.1

theorem declaration uses 'sorry'abs_nonneg (x: ℚ) : |x| ≥ 0 := byx:ℚ⊢ |x| ≥ 0 sorryAll goals completed! 🐙

Твердження 4.3.3(a) / Вправа 4.3.1

theorem declaration uses 'sorry'abs_eq_zero_iff (x: ℚ) : |x| = 0 ↔ x = 0 := byx:ℚ⊢ |x| = 0 ↔ x = 0 sorryAll goals completed! 🐙

Твердження 4.3.3(b) / Вправа 4.3.1

theorem declaration uses 'sorry'abs_add (x y:ℚ) : |x + y| ≤ |x| + |y| := byx:ℚy:ℚ⊢ |x + y| ≤ |x| + |y| sorryAll goals completed! 🐙

Твердження 4.3.3(c) / Вправа 4.3.1

theorem declaration uses 'sorry'abs_le_iff (x y:ℚ) : -y ≤ x ∧ x ≤ y ↔ |x| ≤ y := byx:ℚy:ℚ⊢ -y ≤ x ∧ x ≤ y ↔ |x| ≤ y sorryAll goals completed! 🐙

Твердження 4.3.3(c) / Вправа 4.3.1

theorem declaration uses 'sorry'le_abs (x:ℚ) : -|x| ≤ x ∧ x ≤ |x| := byx:ℚ⊢ -|x| ≤ x ∧ x ≤ |x| sorryAll goals completed! 🐙

Твердження 4.3.3(d) / Вправа 4.3.1

theorem declaration uses 'sorry'abs_mul (x y:ℚ) : |x * y| = |x| * |y| := byx:ℚy:ℚ⊢ |x * y| = |x| * |y| sorryAll goals completed! 🐙

Твердження 4.3.3(d) / Вправа 4.3.1

theorem declaration uses 'sorry'abs_neg (x:ℚ) : |-x| = |x| := byx:ℚ⊢ |(-x)| = |x| sorryAll goals completed! 🐙

Твердження 4.3.3(e) / Вправа 4.3.1

theorem declaration uses 'sorry'dist_nonneg (x y:ℚ) : dist x y ≥ 0 := byx:ℚy:ℚ⊢ dist x y ≥ 0 sorryAll goals completed! 🐙

Твердження 4.3.3(e) / Вправа 4.3.1

theorem declaration uses 'sorry'dist_eq_zero_iff (x y:ℚ) : dist x y = 0 ↔ x = y := byx:ℚy:ℚ⊢ dist x y = 0 ↔ x = y
  sorryAll goals completed! 🐙

Твердження 4.3.3(f) / Вправа 4.3.1

theorem declaration uses 'sorry'dist_symm (x y:ℚ) : dist x y = dist y x := byx:ℚy:ℚ⊢ dist x y = dist y x sorryAll goals completed! 🐙

Твердження 4.3.3(f) / Вправа 4.3.1

theorem declaration uses 'sorry'dist_le (x y z:ℚ) : dist x z ≤ dist x y + dist y z := byx:ℚy:ℚz:ℚ⊢ dist x z ≤ dist x y + dist y z sorryAll goals completed! 🐙

Визначення 4.3.4 (ε-близькість). У тексті це поняття не визначене для ε, що дорівнює нулю або є від’ємним, але в Lean зручніше призначити в цьому випадку «сміттєве» визначення. Це також дозволяє деяке послаблення гіпотез у наступних лемах.

theorem close_iff (ε x y:ℚ): ε.Close x y ↔ |x - y| ≤ ε := byε:ℚx:ℚy:ℚ⊢ ε.Close x y ↔ |x - y| ≤ ε rflAll goals completed! 🐙

Приклади 4.3.6

declaration uses 'sorry'example : (0.1:ℚ).Close (0.99:ℚ) (1.01:ℚ) := by⊢ Rat.Close 0.1 0.99 1.01 sorryAll goals completed! 🐙

Приклади 4.3.6

declaration uses 'sorry'example : ¬ (0.01:ℚ).Close (0.99:ℚ) (1.01:ℚ) := by⊢ ¬Rat.Close 1e-2 0.99 1.01 sorryAll goals completed! 🐙

Приклади 4.3.6

declaration uses 'sorry'example (ε : ℚ) (hε : ε > 0) : ε.Close 2 2 := byε:ℚhε:ε > 0⊢ ε.Close 2 2 sorryAll goals completed! 🐙

theorem declaration uses 'sorry'close_refl (x:ℚ) : (0:ℚ).Close x x := byx:ℚ⊢ Rat.Close 0 x x sorryAll goals completed! 🐙

Твердження 4.3.7(a) / Вправа 4.3.2

theorem declaration uses 'sorry'eq_if_close (x y:ℚ) : x = y ↔ ∀ ε:ℚ, ε > 0 → ε.Close x y := byx:ℚy:ℚ⊢ x = y ↔ ∀ ε > 0, ε.Close x y sorryAll goals completed! 🐙

Твердження 4.3.7(b) / Вправа 4.3.2

theorem declaration uses 'sorry'close_symm (ε x y:ℚ) : ε.Close x y ↔ ε.Close y x := byε:ℚx:ℚy:ℚ⊢ ε.Close x y ↔ ε.Close y x sorryAll goals completed! 🐙

Твердження 4.3.7(c) / Вправа 4.3.2

theorem declaration uses 'sorry'close_trans {ε δ x y z:ℚ} (hxy: ε.Close x y) (hyz: δ.Close y z) :
    (ε + δ).Close x z := byε:ℚδ:ℚx:ℚy:ℚz:ℚhxy:ε.Close x yhyz:δ.Close y z⊢ (ε + δ).Close x z sorryAll goals completed! 🐙

Твердження 4.3.7(d) / Вправа 4.3.2

theorem declaration uses 'sorry'add_close {ε δ x y z w:ℚ} (hxy: ε.Close x y) (hzw: δ.Close z w) :
    (ε + δ).Close (x+z) (y+w) := byε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z w⊢ (ε + δ).Close (x + z) (y + w) sorryAll goals completed! 🐙

Твердження 4.3.7(d) / Вправа 4.3.2

theorem declaration uses 'sorry'sub_close {ε δ x y z w:ℚ} (hxy: ε.Close x y) (hzw: δ.Close z w) :
    (ε + δ).Close (x-z) (y-w) := byε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z w⊢ (ε + δ).Close (x - z) (y - w) sorryAll goals completed! 🐙

Твердження 4.3.7(e) / Вправа 4.3.2, трохи посилена

theorem declaration uses 'sorry'close_mono {ε ε' x y:ℚ} (hxy: ε.Close x y) (hε: ε' ≥  ε) :
    ε'.Close x y := byε:ℚε':ℚx:ℚy:ℚhxy:ε.Close x yhε:ε' ≥ ε⊢ ε'.Close x y sorryAll goals completed! 🐙

Твердження 4.3.7(f) / Вправа 4.3.2

theorem declaration uses 'sorry'close_between {ε x y z w:ℚ} (hxy: ε.Close x y) (hxz: ε.Close x z)
  (hbetween: (y ≤ w ∧ w ≤ z) ∨ (z ≤ w ∧ w ≤ y)) : ε.Close x w := byε:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhxz:ε.Close x zhbetween:y ≤ w ∧ w ≤ z ∨ z ≤ w ∧ w ≤ y⊢ ε.Close x w sorryAll goals completed! 🐙

Твердження 4.3.7(g) / Вправа 4.3.2

theorem declaration uses 'sorry'close_mul_right {ε x y z:ℚ} (hxy: ε.Close x y) :
    (ε*|z|).Close (x * z) (y * z) := byε:ℚx:ℚy:ℚz:ℚhxy:ε.Close x y⊢ (ε * |z|).Close (x * z) (y * z) sorryAll goals completed! 🐙

Твердження 4.3.7(h) / Вправа 4.3.2

theorem close_mul_mul {ε δ x y z w:ℚ} (hxy: ε.Close x y) (hzw: δ.Close z w) :
    (ε*|z|+δ*|x|+ε*δ).Close (x * z) (y * w) := byε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z w⊢ (ε * |z| + δ * |x| + ε * δ).Close (x * z) (y * w)
  -- Доведення написане так, щоб відповідати структурі оригінального тексту, хоча
  -- невід’ємність ε та δ є очевидною і не потребує явного зазначення в гіпотезах.
  have hε : ε ≥ 0 := le_trans (abs_nonneg _) hxyε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z whε:_fvar.6597 ≥ 0 := le_trans (abs_nonneg ?_mvar.6709) _fvar.6603⊢ (ε * |z| + δ * |x| + ε * δ).Close (x * z) (y * w)
  set a := y-xε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z whε:_fvar.6597 ≥ 0 := le_trans (abs_nonneg ?_mvar.6709) _fvar.6603a:ℚ := _fvar.6600 - _fvar.6599⊢ (ε * |z| + δ * |x| + ε * δ).Close (x * z) (y * w)
  have ha : y = x + a := byε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z w⊢ (ε * |z| + δ * |x| + ε * δ).Close (x * z) (y * w) grindAll goals completed! 🐙
  have haε: |a| ≤ ε := byε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z w⊢ (ε * |z| + δ * |x| + ε * δ).Close (x * z) (y * w) rwa [close_symm, close_iff]ε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:|y - x| ≤ εhzw:δ.Close z whε:ε ≥ 0a:ℚ := _fvar.6600 - _fvar.6599ha:y = x + a⊢ |a| ≤ ε at hxy
  set b := w-zε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z whε:_fvar.6597 ≥ 0 := le_trans (abs_nonneg ?_mvar.6709) _fvar.6603a:ℚ := _fvar.6600 - _fvar.6599ha:_fvar.6600 = _fvar.6599 + _fvar.6764 := ?_mvar.6923haε:|_fvar.6764| ≤ _fvar.6597 := ?_mvar.8623b:ℚ := _fvar.6602 - _fvar.6601⊢ (ε * |z| + δ * |x| + ε * δ).Close (x * z) (y * w)
  have hb : w = z + b := byε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z w⊢ (ε * |z| + δ * |x| + ε * δ).Close (x * z) (y * w) grindAll goals completed! 🐙
  have hbδ: |b| ≤ δ := byε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z w⊢ (ε * |z| + δ * |x| + ε * δ).Close (x * z) (y * w) rwa [close_symm, close_iff]ε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:|w - z| ≤ δhε:ε ≥ 0a:ℚ := _fvar.6600 - _fvar.6599ha:y = x + ahaε:|a| ≤ εb:ℚ := _fvar.6602 - _fvar.6601hb:w = z + b⊢ |b| ≤ δ at hzw
  have : y*w = x * z + a * z + x * b + a * b := byε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z w⊢ (ε * |z| + δ * |x| + ε * δ).Close (x * z) (y * w) grindAll goals completed! 🐙
  rw [close_symm, close_iff]ε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z whε:_fvar.6597 ≥ 0 := le_trans (abs_nonneg ?_mvar.6709) _fvar.6603a:ℚ := _fvar.6600 - _fvar.6599ha:_fvar.6600 = _fvar.6599 + _fvar.6764 := ?_mvar.6923haε:|_fvar.6764| ≤ _fvar.6597 := ?_mvar.8623b:ℚ := _fvar.6602 - _fvar.6601hb:_fvar.6602 = _fvar.6601 + _fvar.10741 := ?_mvar.10927hbδ:|_fvar.10741| ≤ _fvar.6598 := ?_mvar.12659this:_fvar.6600 * _fvar.6602 =
  _fvar.6599 * _fvar.6601 + _fvar.6764 * _fvar.6601 + _fvar.6599 * _fvar.10741 + _fvar.6764 * _fvar.10741 := 
  ?_mvar.14162⊢ |y * w - x * z| ≤ ε * |z| + δ * |x| + ε * δ
  calc
    _ = |a * z + b * x + a * b| := byε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z whε:_fvar.6597 ≥ 0 := le_trans (abs_nonneg (_fvar.6599 - _fvar.6600)) _fvar.6603a:ℚ := _fvar.6600 - _fvar.6599ha:_fvar.6600 = _fvar.6599 + _fvar.6764 := close_mul_mul._proof_1haε:|_fvar.6764| ≤ _fvar.6597 := 
  Eq.mp (congrArg (fun _a => _a) (propext (close_iff _fvar.6597 _fvar.6600 _fvar.6599)))
    (Eq.mp (congrArg (fun _a => _a) (propext (close_symm _fvar.6597 _fvar.6599 _fvar.6600))) _fvar.6603)b:ℚ := _fvar.6602 - _fvar.6601hb:_fvar.6602 = _fvar.6601 + _fvar.10741 := close_mul_mul._proof_2hbδ:|_fvar.10741| ≤ _fvar.6598 := 
  Eq.mp (congrArg (fun _a => _a) (propext (close_iff _fvar.6598 _fvar.6602 _fvar.6601)))
    (Eq.mp (congrArg (fun _a => _a) (propext (close_symm _fvar.6598 _fvar.6601 _fvar.6602))) _fvar.6604)this:_fvar.6600 * _fvar.6602 =
  _fvar.6599 * _fvar.6601 + _fvar.6764 * _fvar.6601 + _fvar.6599 * _fvar.10741 + _fvar.6764 * _fvar.10741 := 
  close_mul_mul._proof_3⊢ |y * w - x * z| = |a * z + b * x + a * b| grindAll goals completed! 🐙
    _ ≤ |a * z + b * x| + |a * b| := abs_add _ _
    _ ≤ |a * z| + |b * x| + |a * b| := byε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z whε:_fvar.6597 ≥ 0 := le_trans (abs_nonneg (_fvar.6599 - _fvar.6600)) _fvar.6603a:ℚ := _fvar.6600 - _fvar.6599ha:_fvar.6600 = _fvar.6599 + _fvar.6764 := close_mul_mul._proof_1haε:|_fvar.6764| ≤ _fvar.6597 := 
  Eq.mp (congrArg (fun _a => _a) (propext (close_iff _fvar.6597 _fvar.6600 _fvar.6599)))
    (Eq.mp (congrArg (fun _a => _a) (propext (close_symm _fvar.6597 _fvar.6599 _fvar.6600))) _fvar.6603)b:ℚ := _fvar.6602 - _fvar.6601hb:_fvar.6602 = _fvar.6601 + _fvar.10741 := close_mul_mul._proof_2hbδ:|_fvar.10741| ≤ _fvar.6598 := 
  Eq.mp (congrArg (fun _a => _a) (propext (close_iff _fvar.6598 _fvar.6602 _fvar.6601)))
    (Eq.mp (congrArg (fun _a => _a) (propext (close_symm _fvar.6598 _fvar.6601 _fvar.6602))) _fvar.6604)this:_fvar.6600 * _fvar.6602 =
  _fvar.6599 * _fvar.6601 + _fvar.6764 * _fvar.6601 + _fvar.6599 * _fvar.10741 + _fvar.6764 * _fvar.10741 := 
  close_mul_mul._proof_3⊢ |a * z + b * x| + |a * b| ≤ |a * z| + |b * x| + |a * b| grind [abs_add]All goals completed! 🐙
    _ = |a| * |z| + |b| * |x| + |a| * |b| := byε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z whε:_fvar.6597 ≥ 0 := le_trans (abs_nonneg (_fvar.6599 - _fvar.6600)) _fvar.6603a:ℚ := _fvar.6600 - _fvar.6599ha:_fvar.6600 = _fvar.6599 + _fvar.6764 := close_mul_mul._proof_1haε:|_fvar.6764| ≤ _fvar.6597 := 
  Eq.mp (congrArg (fun _a => _a) (propext (close_iff _fvar.6597 _fvar.6600 _fvar.6599)))
    (Eq.mp (congrArg (fun _a => _a) (propext (close_symm _fvar.6597 _fvar.6599 _fvar.6600))) _fvar.6603)b:ℚ := _fvar.6602 - _fvar.6601hb:_fvar.6602 = _fvar.6601 + _fvar.10741 := close_mul_mul._proof_2hbδ:|_fvar.10741| ≤ _fvar.6598 := 
  Eq.mp (congrArg (fun _a => _a) (propext (close_iff _fvar.6598 _fvar.6602 _fvar.6601)))
    (Eq.mp (congrArg (fun _a => _a) (propext (close_symm _fvar.6598 _fvar.6601 _fvar.6602))) _fvar.6604)this:_fvar.6600 * _fvar.6602 =
  _fvar.6599 * _fvar.6601 + _fvar.6764 * _fvar.6601 + _fvar.6599 * _fvar.10741 + _fvar.6764 * _fvar.10741 := 
  close_mul_mul._proof_3⊢ |a * z| + |b * x| + |a * b| = |a| * |z| + |b| * |x| + |a| * |b| grind [abs_mul]All goals completed! 🐙
    _ ≤ _ := byε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z whε:_fvar.6597 ≥ 0 := le_trans (abs_nonneg (_fvar.6599 - _fvar.6600)) _fvar.6603a:ℚ := _fvar.6600 - _fvar.6599ha:_fvar.6600 = _fvar.6599 + _fvar.6764 := close_mul_mul._proof_1haε:|_fvar.6764| ≤ _fvar.6597 := 
  Eq.mp (congrArg (fun _a => _a) (propext (close_iff _fvar.6597 _fvar.6600 _fvar.6599)))
    (Eq.mp (congrArg (fun _a => _a) (propext (close_symm _fvar.6597 _fvar.6599 _fvar.6600))) _fvar.6603)b:ℚ := _fvar.6602 - _fvar.6601hb:_fvar.6602 = _fvar.6601 + _fvar.10741 := close_mul_mul._proof_2hbδ:|_fvar.10741| ≤ _fvar.6598 := 
  Eq.mp (congrArg (fun _a => _a) (propext (close_iff _fvar.6598 _fvar.6602 _fvar.6601)))
    (Eq.mp (congrArg (fun _a => _a) (propext (close_symm _fvar.6598 _fvar.6601 _fvar.6602))) _fvar.6604)this:_fvar.6600 * _fvar.6602 =
  _fvar.6599 * _fvar.6601 + _fvar.6764 * _fvar.6601 + _fvar.6599 * _fvar.10741 + _fvar.6764 * _fvar.10741 := 
  close_mul_mul._proof_3⊢ |a| * |z| + |b| * |x| + |a| * |b| ≤ ε * |z| + δ * |x| + ε * δ gcongrAll goals completed! 🐙

Ця варіація Твердження 4.3.7(h) не містилася в підручнику, але може бути корисною у деяких наступних вправах.

theorem declaration uses 'sorry'close_mul_mul' {ε δ x y z w:ℚ} (hxy: ε.Close x y) (hzw: δ.Close z w) :
    (ε*|z|+δ*|y|).Close (x * z) (y * w) := byε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.Close x yhzw:δ.Close z w⊢ (ε * |z| + δ * |y|).Close (x * z) (y * w)
    sorryAll goals completed! 🐙

Визначення 4.3.9 (піднесення до степеня). Тут ми використовуємо визначення з Mathlib.

lemma pow_zero (x:ℚ) : x^0 = 1 := rfl

example : (0:ℚ)^0 = 1 := pow_zero 0

Визначення 4.3.9 (піднесення до степеня). Тут ми використовуємо визначення з Mathlib.

lemma pow_succ (x:ℚ) (n:ℕ) : x^(n+1) = x^n * x := _root_.pow_succ x n

Твердження 4.3.10(a) (Властивості піднесення до степеня, I) / Вправа 4.3.3

theorem declaration uses 'sorry'pow_add (x:ℚ) (m n:ℕ) : x^n * x^m = x^(n+m) := byx:ℚm:ℕn:ℕ⊢ x ^ n * x ^ m = x ^ (n + m) sorryAll goals completed! 🐙

Твердження 4.3.10(a) (Властивості піднесення до степеня, I) / Вправа 4.3.3

theorem declaration uses 'sorry'pow_mul (x:ℚ) (m n:ℕ) : (x^n)^m = x^(n*m) := byx:ℚm:ℕn:ℕ⊢ (x ^ n) ^ m = x ^ (n * m) sorryAll goals completed! 🐙

Твердження 4.3.10(a) (Властивості піднесення до степеня, I) / Вправа 4.3.3

theorem declaration uses 'sorry'mul_pow (x y:ℚ) (n:ℕ) : (x*y)^n = x^n * y^n := byx:ℚy:ℚn:ℕ⊢ (x * y) ^ n = x ^ n * y ^ n sorryAll goals completed! 🐙

Твердження 4.3.10(b) (Властивості піднесення до степеня, I) / Вправа 4.3.3

theorem declaration uses 'sorry'pow_eq_zero (x:ℚ) (n:ℕ) (hn : 0 < n) : x^n = 0 ↔ x = 0 := byx:ℚn:ℕhn:0 < n⊢ x ^ n = 0 ↔ x = 0 sorryAll goals completed! 🐙

Твердження 4.3.10(c) (Властивості піднесення до степеня, I) / Вправа 4.3.3

theorem declaration uses 'sorry'pow_nonneg {x:ℚ} (n:ℕ) (hx: x ≥ 0) : x^n ≥ 0 := byx:ℚn:ℕhx:x ≥ 0⊢ x ^ n ≥ 0 sorryAll goals completed! 🐙

Твердження 4.3.10(c) (Властивості піднесення до степеня, I) / Вправа 4.3.3

theorem declaration uses 'sorry'pow_pos {x:ℚ} (n:ℕ) (hx: x > 0) : x^n > 0 := byx:ℚn:ℕhx:x > 0⊢ x ^ n > 0 sorryAll goals completed! 🐙

Твердження 4.3.10(c) (Властивості піднесення до степеня, I) / Вправа 4.3.3

theorem declaration uses 'sorry'pow_ge_pow (x y:ℚ) (n:ℕ) (hxy: x ≥ y) (hy: y ≥ 0) : x^n ≥ y^n := byx:ℚy:ℚn:ℕhxy:x ≥ yhy:y ≥ 0⊢ x ^ n ≥ y ^ n sorryAll goals completed! 🐙

Твердження 4.3.10(c) (Властивості піднесення до степеня, I) / Вправа 4.3.3

theorem declaration uses 'sorry'pow_gt_pow (x y:ℚ) (n:ℕ) (hxy: x > y) (hy: y ≥ 0) (hn: n > 0) : x^n > y^n := byx:ℚy:ℚn:ℕhxy:x > yhy:y ≥ 0hn:n > 0⊢ x ^ n > y ^ n sorryAll goals completed! 🐙

Твердження 4.3.10(d) (Властивості піднесення до степеня, I) / Вправа 4.3.3

theorem declaration uses 'sorry'pow_abs (x:ℚ) (n:ℕ) : |x|^n = |x^n| := byx:ℚn:ℕ⊢ |x| ^ n = |x ^ n| sorryAll goals completed! 🐙

Визначення 4.3.11 (Піднесення до степеня з від’ємним показником). Тут ми використовуємо поняття піднесення до степеня з цілим показником із Mathlib.

theorem zpow_neg (x:ℚ) (n:ℕ) : x^(-(n:ℤ)) = 1/(x^n) := byx:ℚn:ℕ⊢ x ^ (-↑n) = 1 / x ^ n simpAll goals completed! 🐙

example (x:ℚ): x^(-3:ℤ) = 1/(x^3) := zpow_neg x 3

example (x:ℚ): x^(-3:ℤ) = 1/(x*x*x) := byx:ℚ⊢ x ^ (-3) = 1 / (x * x * x) convert zpow_neg x 3h.e'_3.h.e'_6x:ℚ⊢ x * x * x = x ^ 3; ringAll goals completed! 🐙

theorem pow_eq_zpow (x:ℚ) (n:ℕ): x^(n:ℤ) = x^n := zpow_natCast x n

Твердження 4.3.12(a) (Властивості піднесення до степеня, II) / Вправа 4.3.4

theorem declaration uses 'sorry'zpow_add (x:ℚ) (n m:ℤ) (hx: x ≠ 0): x^n * x^m = x^(n+m) := byx:ℚn:ℤm:ℤhx:x ≠ 0⊢ x ^ n * x ^ m = x ^ (n + m) sorryAll goals completed! 🐙

Твердження 4.3.12(a) (Властивості піднесення до степеня, II) / Вправа 4.3.4

theorem declaration uses 'sorry'zpow_mul (x:ℚ) (n m:ℤ) : (x^n)^m = x^(n*m) := byx:ℚn:ℤm:ℤ⊢ (x ^ n) ^ m = x ^ (n * m) sorryAll goals completed! 🐙

Твердження 4.3.12(a) (Властивості піднесення до степеня, II) / Вправа 4.3.4

theorem declaration uses 'sorry'mul_zpow (x y:ℚ) (n:ℤ) : (x*y)^n = x^n * y^n := byx:ℚy:ℚn:ℤ⊢ (x * y) ^ n = x ^ n * y ^ n sorryAll goals completed! 🐙

Твердження 4.3.12(b) (Властивості піднесення до степеня, II) / Вправа 4.3.4

theorem declaration uses 'sorry'zpow_pos {x:ℚ} (n:ℤ) (hx: x > 0) : x^n > 0 := byx:ℚn:ℤhx:x > 0⊢ x ^ n > 0 sorryAll goals completed! 🐙

Твердження 4.3.12(b) (Властивості піднесення до степеня, II) / Вправа 4.3.4

theorem declaration uses 'sorry'zpow_ge_zpow {x y:ℚ} {n:ℤ} (hxy: x ≥ y) (hy: y > 0) (hn: n > 0): x^n ≥ y^n := byx:ℚy:ℚn:ℤhxy:x ≥ yhy:y > 0hn:n > 0⊢ x ^ n ≥ y ^ n sorryAll goals completed! 🐙

theorem declaration uses 'sorry'zpow_ge_zpow_ofneg {x y:ℚ} {n:ℤ} (hxy: x ≥ y) (hy: y > 0) (hn: n < 0) : x^n ≤ y^n := byx:ℚy:ℚn:ℤhxy:x ≥ yhy:y > 0hn:n < 0⊢ x ^ n ≤ y ^ n
  sorryAll goals completed! 🐙

Твердження 4.3.12(c) (Властивості піднесення до степеня, II) / Вправа 4.3.4

theorem declaration uses 'sorry'zpow_inj {x y:ℚ} {n:ℤ} (hx: x > 0) (hy : y > 0) (hn: n ≠ 0) (hxy: x^n = y^n) : x = y := byx:ℚy:ℚn:ℤhx:x > 0hy:y > 0hn:n ≠ 0hxy:x ^ n = y ^ n⊢ x = y
  sorryAll goals completed! 🐙

Твердження 4.3.12(d) (Властивості піднесення до степеня, II) / Вправа 4.3.4

theorem declaration uses 'sorry'zpow_abs (x:ℚ) (n:ℤ) : |x|^n = |x^n| := byx:ℚn:ℤ⊢ |x| ^ n = |x ^ n| sorryAll goals completed! 🐙

Вправа 4.3.5

theorem declaration uses 'sorry'two_pow_geq (N:ℕ) : 2^N ≥ N := byN:ℕ⊢ 2 ^ N ≥ N sorryAll goals completed! 🐙