Аналіз I, Розділ 5.6: Піднесення дійсних чисел до степеня, частина I

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

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

• Піднесення дійсних чисел до степеня натуральних та цілих чисел.
• Коріння n-го рівня.
• Піднесення дійсного числа до раціонального.

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

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

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

theorem Chapter5.Real.pow_zero (x : Real) : x ^ 0 = 1

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

theorem Chapter5.Real.pow_succ (x : Real) (n : ℕ) : x ^ (n + 1) = x ^ n * x

theorem Chapter5.Real.pow_of_coe (q : ℚ) (n : ℕ) : ↑q ^ n = ↑(q ^ n)

theorem Chapter5.Real.pow_add (x : Real) (m n : ℕ) : x ^ n * x ^ m = x ^ (n + m)

Аналог Твердження 4.3.10(a)

theorem Chapter5.Real.pow_mul (x : Real) (m n : ℕ) : (x ^ n) ^ m = x ^ (n * m)

Аналог Твердження 4.3.10(a)

theorem Chapter5.Real.mul_pow (x y : Real) (n : ℕ) : (x * y) ^ n = x ^ n * y ^ n

Аналог Твердження 4.3.10(a)

theorem Chapter5.Real.pow_eq_zero (x : Real) (n : ℕ) (hn : 0 < n) : x ^ n = 0 ↔ x = 0

Аналог Твердження 4.3.10(b)

theorem Chapter5.Real.pow_nonneg {x : Real} (n : ℕ) (hx : x ≥ 0) : x ^ n ≥ 0

Аналог Твердження 4.3.10(c)

theorem Chapter5.Real.pow_pos {x : Real} (n : ℕ) (hx : x > 0) : x ^ n > 0

Аналог Твердження 4.3.10(c)

theorem Chapter5.Real.pow_ge_pow (x y : Real) (n : ℕ) (hxy : x ≥ y) (hy : y ≥ 0) : x ^ n ≥ y ^ n

Аналог Твердження 4.3.10(c)

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

Аналог Твердження 4.3.10(c)

theorem Chapter5.Real.pow_abs (x : Real) (n : ℕ) : |x| ^ n = |x ^ n|

Аналог Твердження 4.3.10(d)

theorem Chapter5.Real.pow_eq_pow (x : Real) (n : ℕ) : x ^ ↑n = x ^ n

Визначення 5.6.2 (Піднесення дійсного числа до цілого степеня). Тут ми використовуємо визначення Mathlib, що походить від DivInvMonoid.

@[simp]

theorem Chapter5.Real.zpow_zero (x : Real) : x ^ 0 = 1

theorem Chapter5.Real.zpow_neg {x : Real} (n : ℕ) : x ^ (-↑n) = 1 / x ^ n

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

Аналог Твердження 4.3.12(a)

theorem Chapter5.Real.zpow_mul (x : Real) (n m : ℤ) : (x ^ n) ^ m = x ^ (n * m)

Аналог Твердження 4.3.12(a)

theorem Chapter5.Real.mul_zpow (x y : Real) (n : ℤ) : (x * y) ^ n = x ^ n * y ^ n

Аналог Твердження 4.3.12(a)

theorem Chapter5.Real.zpow_pos {x : Real} (n : ℤ) (hx : x > 0) : x ^ n > 0

Аналог Твердження 4.3.12(b)

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

Аналог Твердження 4.3.12(b)

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

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

Аналог Твердження 4.3.12(c)

theorem Chapter5.Real.zpow_abs (x : Real) (n : ℤ) : |x| ^ n = |x ^ n|

Аналог Твердження 4.3.12(d)

@[reducible, inline]

noncomputable abbrev Chapter5.Real.root (x : Real) (n : ℕ) : Real

Визначення 5.6.2. Ми допускаємо сміттєві значення, коли x є від’ємним або n дорівнює нулю.

Equations

• x.root n = sSup {y : Chapter5.Real | y ≥ 0 ∧ y ^ n ≤ x}

@[reducible, inline]

noncomputable abbrev Chapter5.Real.sqrt (x : Real) : Real

Equations

• x.sqrt = x.root 2

theorem Chapter5.Real.rootset_nonempty {x : Real} (hx : x ≥ 0) (n : ℕ) (hn : n ≥ 1) : {y : Real | y ≥ 0 ∧ y ^ n ≤ x}.Nonempty

Лема 5.6.5 (Існування коренів n-го степеня)

theorem Chapter5.Real.rootset_bddAbove {x : Real} (n : ℕ) (hn : n ≥ 1) : BddAbove {y : Real | y ≥ 0 ∧ y ^ n ≤ x}

theorem Chapter5.Real.eq_root_iff_pow_eq {x y : Real} (hx : x ≥ 0) (hy : y ≥ 0) {n : ℕ} (hn : n ≥ 1) : y = x.root n ↔ y ^ n = x

Лема 5.6.6 (ab) / Вправа 5.6.1

theorem Chapter5.Real.root_nonneg {x : Real} (hx : x ≥ 0) {n : ℕ} (hn : n ≥ 1) : x.root n ≥ 0

Лема 5.6.6 (c) / Вправа 5.6.1

theorem Chapter5.Real.root_pos {x : Real} (hx : x ≥ 0) {n : ℕ} (hn : n ≥ 1) : x.root n > 0 ↔ x > 0

Лема 5.6.6 (c) / Вправа 5.6.1

theorem Chapter5.Real.pow_of_root {x : Real} (hx : x ≥ 0) {n : ℕ} (hn : n ≥ 1) : x.root n ^ n = x

theorem Chapter5.Real.root_of_pow {x : Real} (hx : x ≥ 0) {n : ℕ} (hn : n ≥ 1) : (x ^ n).root n = x

theorem Chapter5.Real.root_mono {x y : Real} (hx : x ≥ 0) (hy : y ≥ 0) {n : ℕ} (hn : n ≥ 1) : x > y ↔ x.root n > y.root n

Лема 5.6.6 (d) / Вправа 5.6.1

theorem Chapter5.Real.root_mono_of_gt_one {x : Real} (hx : x > 1) {k l : ℕ} (hkl : k > l) (hl : l ≥ 1) : x.root k < x.root l

Лема 5.6.6 (e) / Вправа 5.6.1

theorem Chapter5.Real.root_mono_of_lt_one {x : Real} (hx0 : 0 < x) (hx : x < 1) {k l : ℕ} (hkl : k > l) (hl : l ≥ 1) : x.root k > x.root l

Лема 5.6.6 (e) / Вправа 5.6.1

theorem Chapter5.Real.root_of_one {k : ℕ} (hk : k ≥ 1) : root 1 k = 1

Лема 5.6.6 (e) / Вправа 5.6.1

theorem Chapter5.Real.root_mul {x y : Real} (hx : x ≥ 0) (hy : y ≥ 0) {n : ℕ} (hn : n ≥ 1) : (x * y).root n = x.root n * y.root n

Лема 5.6.6 (f) / Вправа 5.6.1

theorem Chapter5.Real.root_root {x : Real} (hx : x ≥ 0) {n m : ℕ} (hn : n ≥ 1) (hm : m ≥ 1) : (x.root n).root m = x.root (n * m)

Лема 5.6.6 (g) / Вправа 5.6.1

theorem Chapter5.Real.root_one {x : Real} (hx : x > 0) : x.root 1 = x

theorem Chapter5.Real.pow_cancel {y z : Real} (hy : y > 0) (hz : z > 0) {n : ℕ} (hn : n ≥ 1) (h : y ^ n = z ^ n) : y = z

@[reducible, inline]

noncomputable abbrev Chapter5.Real.ratPow (x : Real) (q : ℚ) : Real

Визначення 5.6.7

Equations

• x.ratPow q = x.root q.den ^ q.num

noncomputable instance Chapter5.Real.instRatPow : Pow Real ℚ

Equations

• Chapter5.Real.instRatPow = { pow := fun (x : Chapter5.Real) (q : ℚ) => x.ratPow q }

theorem Chapter5.Rat.eq_quot (q : ℚ) : ∃ (a : ℤ), ∃ b > 0, q = ↑a / ↑b

theorem Chapter5.Real.pow_root_eq_pow_root {a a' : ℤ} {b b' : ℕ} (hb : b > 0) (hb' : b' > 0) (hq : ↑a / ↑b = ↑a' / ↑b') {x : Real} (hx : x > 0) : x.root b' ^ a' = x.root b ^ a

Лема 5.6.8

theorem Chapter5.Real.ratPow_def {x : Real} (hx : x > 0) (a : ℤ) {b : ℕ} (hb : b > 0) : x ^ (↑a / ↑b) = x.root b ^ a

theorem Chapter5.Real.ratPow_eq_root {x : Real} (hx : x > 0) {n : ℕ} (hn : n ≥ 1) : x ^ (1 / ↑n) = x.root n

theorem Chapter5.Real.ratPow_eq_pow {x : Real} (hx : x > 0) (n : ℤ) : x ^ ↑n = x ^ n

theorem Chapter5.Real.ratPow_pos {x : Real} (hx : x > 0) (q : ℚ) : x ^ q > 0

Лема 5.6.9(a) / Вправа 5.6.2

theorem Chapter5.Real.ratPow_add {x : Real} (hx : x > 0) (q r : ℚ) : x ^ (q + r) = x ^ q * x ^ r

Лема 5.6.9(b) / Вправа 5.6.2

theorem Chapter5.Real.ratPow_ratPow {x : Real} (hx : x > 0) (q r : ℚ) : (x ^ q) ^ r = x ^ (q * r)

Лема 5.6.9(b) / Вправа 5.6.2

theorem Chapter5.Real.ratPow_neg {x : Real} (hx : x > 0) (q : ℚ) : x ^ (-q) = 1 / x ^ q

Лема 5.6.9(c) / Вправа 5.6.2

theorem Chapter5.Real.ratPow_mono {x y : Real} (hx : x > 0) (hy : y > 0) {q : ℚ} (h : q > 0) : x > y ↔ x ^ q > y ^ q

Лема 5.6.9(d) / Вправа 5.6.2

theorem Chapter5.Real.ratPow_mono_of_gt_one {x : Real} (hx : x > 1) {q r : ℚ} : x ^ q > x ^ r ↔ q > r

Лема 5.6.9(e) / Вправа 5.6.2

theorem Chapter5.Real.ratPow_mono_of_lt_one {x : Real} (hx0 : 0 < x) (hx : x < 1) {q r : ℚ} : x ^ q > x ^ r ↔ q < r

Лема 5.6.9(e) / Вправа 5.6.2

theorem Chapter5.Real.ratPow_mul {x y : Real} (hx : x > 0) (hy : y > 0) (q : ℚ) : (x * y) ^ q = x ^ q * y ^ q

Лема 5.6.9(f) / Вправа 5.6.2

theorem Chapter5.Real.pow_even (x : Real) {n : ℕ} (hn : Even n) : x ^ n ≥ 0

Вправа 5.6.3

theorem Chapter5.Real.max_ratPow {x y : Real} (hx : x > 0) (hy : y > 0) {q : ℚ} (hq : q > 0) : max (x ^ q) (y ^ q) = max x y ^ q

Вправа 5.6.5

theorem Chapter5.Real.min_ratPow {x y : Real} (hx : x > 0) (hy : y > 0) {q : ℚ} (hq : q > 0) : min (x ^ q) (y ^ q) = min x y ^ q

Вправа 5.6.5