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

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

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

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

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

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

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

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

def Rat.Close (ε x y : ℚ) : Prop

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

Equations

• ε.Close x y = (|x - y| ≤ ε)

@[reducible, inline]

abbrev Section_4_3.abs (x : ℚ) : ℚ

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

Equations

• Section_4_3.abs x = if x > 0 then x else if x < 0 then -x else 0

theorem Section_4_3.abs_of_pos {x : ℚ} (hx : 0 < x) : abs x = x

theorem Section_4_3.abs_of_neg {x : ℚ} (hx : x < 0) : abs x = -x

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

theorem Section_4_3.abs_of_zero : abs 0 = 0

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

theorem Section_4_3.abs_eq_abs (x : ℚ) : abs x = |x|

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

@[reducible, inline]

abbrev Section_4_3.dist (x y : ℚ) : ℚ

Equations

• Section_4_3.dist x y = |x - y|

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

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

theorem Section_4_3.abs_nonneg (x : ℚ) : |x| ≥ 0

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

theorem Section_4_3.abs_eq_zero_iff (x : ℚ) : |x| = 0 ↔ x = 0

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

theorem Section_4_3.abs_add (x y : ℚ) : |x + y| ≤ |x| + |y|

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

theorem Section_4_3.abs_le_iff (x y : ℚ) : -y ≤ x ∧ x ≤ y ↔ |x| ≤ y

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

theorem Section_4_3.le_abs (x : ℚ) : -|x| ≤ x ∧ x ≤ |x|

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

theorem Section_4_3.abs_mul (x y : ℚ) : |x * y| = |x| * |y|

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

theorem Section_4_3.abs_neg (x : ℚ) : |(-x)| = |x|

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

theorem Section_4_3.dist_nonneg (x y : ℚ) : dist x y ≥ 0

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

theorem Section_4_3.dist_eq_zero_iff (x y : ℚ) : dist x y = 0 ↔ x = y

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

theorem Section_4_3.dist_symm (x y : ℚ) : dist x y = dist y x

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

theorem Section_4_3.dist_le (x y z : ℚ) : dist x z ≤ dist x y + dist y z

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

theorem Section_4_3.close_iff (ε x y : ℚ) : ε.Close x y ↔ |x - y| ≤ ε

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

theorem Section_4_3.close_refl (x : ℚ) : Rat.Close 0 x x

theorem Section_4_3.eq_if_close (x y : ℚ) : x = y ↔ ∀ ε > 0, ε.Close x y

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

theorem Section_4_3.close_symm (ε x y : ℚ) : ε.Close x y ↔ ε.Close y x

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

theorem Section_4_3.close_trans {ε δ x y z : ℚ} (hxy : ε.Close x y) (hyz : δ.Close y z) : (ε + δ).Close x z

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

theorem Section_4_3.add_close {ε δ x y z w : ℚ} (hxy : ε.Close x y) (hzw : δ.Close z w) : (ε + δ).Close (x + z) (y + w)

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

theorem Section_4_3.sub_close {ε δ x y z w : ℚ} (hxy : ε.Close x y) (hzw : δ.Close z w) : (ε + δ).Close (x - z) (y - w)

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

theorem Section_4_3.close_mono {ε ε' x y : ℚ} (hxy : ε.Close x y) (hε : ε' ≥ ε) : ε'.Close x y

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

theorem Section_4_3.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

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

theorem Section_4_3.close_mul_right {ε x y z : ℚ} (hxy : ε.Close x y) : (ε * |z|).Close (x * z) (y * z)

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

theorem Section_4_3.close_mul_mul {ε δ x y z w : ℚ} (hxy : ε.Close x y) (hzw : δ.Close z w) : (ε * |z| + δ * |x| + ε * δ).Close (x * z) (y * w)

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

theorem Section_4_3.close_mul_mul' {ε δ x y z w : ℚ} (hxy : ε.Close x y) (hzw : δ.Close z w) : (ε * |z| + δ * |y|).Close (x * z) (y * w)

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

theorem Section_4_3.pow_zero (x : ℚ) : x ^ 0 = 1

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

theorem Section_4_3.pow_succ (x : ℚ) (n : ℕ) : x ^ (n + 1) = x ^ n * x

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

theorem Section_4_3.pow_add (x : ℚ) (m n : ℕ) : x ^ n * x ^ m = x ^ (n + m)

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

theorem Section_4_3.pow_mul (x : ℚ) (m n : ℕ) : (x ^ n) ^ m = x ^ (n * m)

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

theorem Section_4_3.mul_pow (x y : ℚ) (n : ℕ) : (x * y) ^ n = x ^ n * y ^ n

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

theorem Section_4_3.pow_eq_zero (x : ℚ) (n : ℕ) (hn : 0 < n) : x ^ n = 0 ↔ x = 0

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

theorem Section_4_3.pow_nonneg {x : ℚ} (n : ℕ) (hx : x ≥ 0) : x ^ n ≥ 0

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

theorem Section_4_3.pow_pos {x : ℚ} (n : ℕ) (hx : x > 0) : x ^ n > 0

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

theorem Section_4_3.pow_ge_pow (x y : ℚ) (n : ℕ) (hxy : x ≥ y) (hy : y ≥ 0) : x ^ n ≥ y ^ n

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

theorem Section_4_3.pow_gt_pow (x y : ℚ) (n : ℕ) (hxy : x > y) (hy : y ≥ 0) (hn : n > 0) : x ^ n > y ^ n

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

theorem Section_4_3.pow_abs (x : ℚ) (n : ℕ) : |x| ^ n = |x ^ n|

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

theorem Section_4_3.zpow_neg (x : ℚ) (n : ℕ) : x ^ (-↑n) = 1 / x ^ n

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

theorem Section_4_3.pow_eq_zpow (x : ℚ) (n : ℕ) : x ^ ↑n = x ^ n

theorem Section_4_3.zpow_add (x : ℚ) (n m : ℤ) (hx : x ≠ 0) : x ^ n * x ^ m = x ^ (n + m)

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

theorem Section_4_3.zpow_mul (x : ℚ) (n m : ℤ) : (x ^ n) ^ m = x ^ (n * m)

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

theorem Section_4_3.mul_zpow (x y : ℚ) (n : ℤ) : (x * y) ^ n = x ^ n * y ^ n

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

theorem Section_4_3.zpow_pos {x : ℚ} (n : ℤ) (hx : x > 0) : x ^ n > 0

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

theorem Section_4_3.zpow_ge_zpow {x y : ℚ} {n : ℤ} (hxy : x ≥ y) (hy : y > 0) (hn : n > 0) : x ^ n ≥ y ^ n

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

theorem Section_4_3.zpow_ge_zpow_ofneg {x y : ℚ} {n : ℤ} (hxy : x ≥ y) (hy : y > 0) (hn : n < 0) : x ^ n ≤ y ^ n

theorem Section_4_3.zpow_inj {x y : ℚ} {n : ℤ} (hx : x > 0) (hy : y > 0) (hn : n ≠ 0) (hxy : x ^ n = y ^ n) : x = y

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

theorem Section_4_3.zpow_abs (x : ℚ) (n : ℤ) : |x| ^ n = |x ^ n|

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

theorem Section_4_3.two_pow_geq (N : ℕ) : 2 ^ N ≥ N

Вправа 4.3.5