Imports
import Mathlib.Tactic
import Analysis.Section_5_5Analysis I, Section 5.6: Real exponentiation, part I
I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.
Main constructions and results of this section:
-
Exponentiating reals to natural numbers and integers.
-
nth roots.
-
Raising a real to a rational number.
Tips from past users
Users of the companion who have completed the exercises in this section are welcome to send their tips for future users in this section as PRs.
-
(Add tip here)
namespace Chapter5
Definition 5.6.1 (Exponentiating a real by a natural number). Here we use the
Mathlib definition coming from Monoid.
lemma Real.pow_zero (x: Real) : x ^ 0 = 1 := rfllemma Real.pow_succ (x: Real) (n:ℕ) : x ^ (n+1) = (x ^ n) * x := rfllemma Real.pow_of_coe (q: ℚ) (n:ℕ) : (q:Real) ^ n = (q ^ n:ℚ) := q:ℚn:ℕ⊢ ↑q ^ n = ↑(q ^ n) q:ℚ⊢ ↑q ^ 0 = ↑(q ^ 0)q:ℚn:ℕhn:↑q ^ n = ↑(q ^ n)⊢ ↑q ^ (n + 1) = ↑(q ^ (n + 1)) q:ℚ⊢ ↑q ^ 0 = ↑(q ^ 0)q:ℚn:ℕhn:↑q ^ n = ↑(q ^ n)⊢ ↑q ^ (n + 1) = ↑(q ^ (n + 1)) All goals completed! 🐙Analogue of Proposition 4.3.10(a)
/- The claims below can be handled easily by existing Mathlib API (as `Real` already is known
to be a `Field`), but the spirit of the exercises is to adapt the proofs of
Proposition 4.3.10 that you previously established. -/
theorem Real.pow_add (x:Real) (m n:ℕ) : x^n * x^m = x^(n+m) := x:Realm:ℕn:ℕ⊢ x ^ n * x ^ m = x ^ (n + m) All goals completed! 🐙Analogue of Proposition 4.3.10(a)
theorem Real.pow_mul (x:Real) (m n:ℕ) : (x^n)^m = x^(n*m) := x:Realm:ℕn:ℕ⊢ (x ^ n) ^ m = x ^ (n * m) All goals completed! 🐙Analogue of Proposition 4.3.10(a)
theorem Real.mul_pow (x y:Real) (n:ℕ) : (x*y)^n = x^n * y^n := x:Realy:Realn:ℕ⊢ (x * y) ^ n = x ^ n * y ^ n All goals completed! 🐙Analogue of Proposition 4.3.10(b)
theorem Real.pow_eq_zero (x:Real) (n:ℕ) (hn : 0 < n) : x^n = 0 ↔ x = 0 := x:Realn:ℕhn:0 < n⊢ x ^ n = 0 ↔ x = 0 All goals completed! 🐙Analogue of Proposition 4.3.10(c)
theorem Real.pow_nonneg {x:Real} (n:ℕ) (hx: x ≥ 0) : x^n ≥ 0 := x:Realn:ℕhx:x ≥ 0⊢ x ^ n ≥ 0 All goals completed! 🐙Analogue of Proposition 4.3.10(c)
theorem Real.pow_pos {x:Real} (n:ℕ) (hx: x > 0) : x^n > 0 := x:Realn:ℕhx:x > 0⊢ x ^ n > 0 All goals completed! 🐙Analogue of Proposition 4.3.10(c)
theorem Real.pow_ge_pow (x y:Real) (n:ℕ) (hxy: x ≥ y) (hy: y ≥ 0) : x^n ≥ y^n := x:Realy:Realn:ℕhxy:x ≥ yhy:y ≥ 0⊢ x ^ n ≥ y ^ n All goals completed! 🐙Analogue of Proposition 4.3.10(c)
theorem Real.pow_gt_pow (x y:Real) (n:ℕ) (hxy: x > y) (hy: y ≥ 0) (hn: n > 0) : x^n > y^n := x:Realy:Realn:ℕhxy:x > yhy:y ≥ 0hn:n > 0⊢ x ^ n > y ^ n All goals completed! 🐙Analogue of Proposition 4.3.10(d)
theorem Real.pow_abs (x:Real) (n:ℕ) : |x|^n = |x^n| := x:Realn:ℕ⊢ |x| ^ n = |x ^ n| All goals completed! 🐙
Definition 5.6.2 (Exponentiating a real by an integer). Here we use the Mathlib definition coming from DivInvMonoid.
lemma Real.pow_eq_pow (x: Real) (n:ℕ): x ^ (n:ℤ) = x ^ n := x:Realn:ℕ⊢ x ^ ↑n = x ^ n All goals completed! 🐙@[simp]
lemma Real.zpow_zero (x: Real) : x ^ (0:ℤ) = 1 := x:Real⊢ x ^ 0 = 1 All goals completed! 🐙lemma Real.zpow_neg {x:Real} (n:ℕ) : x^(-n:ℤ) = 1 / (x^n) := x:Realn:ℕ⊢ x ^ (-↑n) = 1 / x ^ n All goals completed! 🐙Analogue of Proposition 4.3.12(a)
theorem Real.zpow_add (x:Real) (n m:ℤ) (hx: x ≠ 0): x^n * x^m = x^(n+m) := x:Realn:ℤm:ℤhx:x ≠ 0⊢ x ^ n * x ^ m = x ^ (n + m) All goals completed! 🐙Analogue of Proposition 4.3.12(a)
theorem Real.zpow_mul (x:Real) (n m:ℤ) : (x^n)^m = x^(n*m) := x:Realn:ℤm:ℤ⊢ (x ^ n) ^ m = x ^ (n * m) All goals completed! 🐙Analogue of Proposition 4.3.12(a)
theorem Real.mul_zpow (x y:Real) (n:ℤ) : (x*y)^n = x^n * y^n := x:Realy:Realn:ℤ⊢ (x * y) ^ n = x ^ n * y ^ n All goals completed! 🐙Analogue of Proposition 4.3.12(b)
theorem Real.zpow_pos {x:Real} (n:ℤ) (hx: x > 0) : x^n > 0 := x:Realn:ℤhx:x > 0⊢ x ^ n > 0 All goals completed! 🐙Analogue of Proposition 4.3.12(b)
theorem Real.zpow_ge_zpow {x y:Real} {n:ℤ} (hxy: x ≥ y) (hy: y > 0) (hn: n > 0): x^n ≥ y^n := x:Realy:Realn:ℤhxy:x ≥ yhy:y > 0hn:n > 0⊢ x ^ n ≥ y ^ n All goals completed! 🐙theorem Real.zpow_ge_zpow_ofneg {x y:Real} {n:ℤ} (hxy: x ≥ y) (hy: y > 0) (hn: n < 0) : x^n ≤ y^n := x:Realy:Realn:ℤhxy:x ≥ yhy:y > 0hn:n < 0⊢ x ^ n ≤ y ^ n
All goals completed! 🐙Analogue of Proposition 4.3.12(c)
theorem Real.zpow_inj {x y:Real} {n:ℤ} (hx: x > 0) (hy : y > 0) (hn: n ≠ 0) (hxy: x^n = y^n) : x = y := x:Realy:Realn:ℤhx:x > 0hy:y > 0hn:n ≠ 0hxy:x ^ n = y ^ n⊢ x = y
All goals completed! 🐙Analogue of Proposition 4.3.12(d)
theorem Real.zpow_abs (x:Real) (n:ℤ) : |x|^n = |x^n| := x:Realn:ℤ⊢ |x| ^ n = |x ^ n| All goals completed! 🐙
Definition 5.6.2. We permit "junk values" when x is negative or n vanishes.
Lemma 5.6.5 (Existence of n^th roots)
theorem Real.rootset_nonempty {x:Real} (hx: x ≥ 0) (n:ℕ) (hn: n ≥ 1) : { y:Real | y ≥ 0 ∧ y^n ≤ x }.Nonempty := x:Realhx:x ≥ 0n:ℕhn:n ≥ 1⊢ {y | y ≥ 0 ∧ y ^ n ≤ x}.Nonempty
x:Realhx:x ≥ 0n:ℕhn:n ≥ 1⊢ 0 ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}
All goals completed! 🐙theorem Real.rootset_bddAbove {x:Real} (n:ℕ) (hn: n ≥ 1) : BddAbove { y:Real | y ≥ 0 ∧ y^n ≤ x } := x:Realn:ℕhn:n ≥ 1⊢ BddAbove {y | y ≥ 0 ∧ y ^ n ≤ x}
-- This proof is written to follow the structure of the original text.
x:Realn:ℕhn:n ≥ 1⊢ ∃ x_1, ∀ y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}, y ≤ x_1
x:Realn:ℕhn:n ≥ 1h:x ≤ 1⊢ ∃ x_1, ∀ y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}, y ≤ x_1x:Realn:ℕhn:n ≥ 1h:1 < x⊢ ∃ x_1, ∀ y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}, y ≤ x_1
x:Realn:ℕhn:n ≥ 1h:x ≤ 1⊢ ∃ x_1, ∀ y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}, y ≤ x_1 x:Realn:ℕhn:n ≥ 1h:x ≤ 1⊢ ∀ y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}, y ≤ 1; intro y x:Realn:ℕhn:n ≥ 1h:x ≤ 1y:Realhy:y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}⊢ y ≤ 1; x:Realn:ℕhn:n ≥ 1h:x ≤ 1y:Realhy:0 ≤ y ∧ y ^ n ≤ x⊢ y ≤ 1
x:Realn:ℕhn:n ≥ 1h:x ≤ 1y:Realhy:0 ≤ y ∧ y ^ n ≤ xhy':1 < y⊢ False
replace hy' : 1 < y^n := x:Realn:ℕhn:n ≥ 1⊢ BddAbove {y | y ≥ 0 ∧ y ^ n ≤ x}
All goals completed! 🐙
All goals completed! 🐙
x:Realn:ℕhn:n ≥ 1h:1 < x⊢ ∀ y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}, y ≤ x; intro y x:Realn:ℕhn:n ≥ 1h:1 < xy:Realhy:y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}⊢ y ≤ x; x:Realn:ℕhn:n ≥ 1h:1 < xy:Realhy:0 ≤ y ∧ y ^ n ≤ x⊢ y ≤ x
x:Realn:ℕhn:n ≥ 1h:1 < xy:Realhy:0 ≤ y ∧ y ^ n ≤ xhy':x < y⊢ False
replace hy' : x < y^n := x:Realn:ℕhn:n ≥ 1⊢ BddAbove {y | y ≥ 0 ∧ y ^ n ≤ x}
All goals completed! 🐙
All goals completed! 🐙Lemma 5.6.6 (ab) / Exercise 5.6.1
theorem 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 := x:Realy:Realhx:x ≥ 0hy:y ≥ 0n:ℕhn:n ≥ 1⊢ y = x.root n ↔ y ^ n = x All goals completed! 🐙Lemma 5.6.6 (c) / Exercise 5.6.1
theorem Real.root_nonneg {x:Real} (hx: x ≥ 0) {n:ℕ} (hn: n ≥ 1) : x.root n ≥ 0 := x:Realhx:x ≥ 0n:ℕhn:n ≥ 1⊢ x.root n ≥ 0 All goals completed! 🐙Lemma 5.6.6 (c) / Exercise 5.6.1
theorem Real.root_pos {x:Real} (hx: x ≥ 0) {n:ℕ} (hn: n ≥ 1) : x.root n > 0 ↔ x > 0 := x:Realhx:x ≥ 0n:ℕhn:n ≥ 1⊢ x.root n > 0 ↔ x > 0 All goals completed! 🐙theorem Real.pow_of_root {x:Real} (hx: x ≥ 0) {n:ℕ} (hn: n ≥ 1) :
(x.root n)^n = x := x:Realhx:x ≥ 0n:ℕhn:n ≥ 1⊢ x.root n ^ n = x All goals completed! 🐙theorem Real.root_of_pow {x:Real} (hx: x ≥ 0) {n:ℕ} (hn: n ≥ 1) :
(x^n).root n = x := x:Realhx:x ≥ 0n:ℕhn:n ≥ 1⊢ (x ^ n).root n = x All goals completed! 🐙Lemma 5.6.6 (d) / Exercise 5.6.1
theorem Real.root_mono {x y:Real} (hx: x ≥ 0) (hy: y ≥ 0) {n:ℕ} (hn: n ≥ 1) : x > y ↔ x.root n > y.root n := x:Realy:Realhx:x ≥ 0hy:y ≥ 0n:ℕhn:n ≥ 1⊢ x > y ↔ x.root n > y.root n All goals completed! 🐙Lemma 5.6.6 (e) / Exercise 5.6.1
theorem 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 := x:Realhx:x > 1k:ℕl:ℕhkl:k > lhl:l ≥ 1⊢ x.root k < x.root l All goals completed! 🐙Lemma 5.6.6 (e) / Exercise 5.6.1
theorem 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 := x:Realhx0:0 < xhx:x < 1k:ℕl:ℕhkl:k > lhl:l ≥ 1⊢ x.root k > x.root l All goals completed! 🐙Lemma 5.6.6 (e) / Exercise 5.6.1
theorem Real.root_of_one {k: ℕ} (hk: k ≥ 1): (1:Real).root k = 1 := k:ℕhk:k ≥ 1⊢ root 1 k = 1 All goals completed! 🐙Lemma 5.6.6 (f) / Exercise 5.6.1
theorem 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) := x:Realy:Realhx:x ≥ 0hy:y ≥ 0n:ℕhn:n ≥ 1⊢ (x * y).root n = x.root n * y.root n All goals completed! 🐙Lemma 5.6.6 (g) / Exercise 5.6.1
theorem 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) := x:Realhx:x ≥ 0n:ℕm:ℕhn:n ≥ 1hm:m ≥ 1⊢ (x.root n).root m = x.root (n * m) All goals completed! 🐙theorem Real.root_one {x:Real} (hx: x > 0): x.root 1 = x := x:Realhx:x > 0⊢ x.root 1 = x All goals completed! 🐙theorem Real.pow_cancel {y z:Real} (hy: y > 0) (hz: z > 0) {n:ℕ} (hn: n ≥ 1)
(h: y^n = z^n) : y = z := y:Realz:Realhy:y > 0hz:z > 0n:ℕhn:n ≥ 1h:y ^ n = z ^ n⊢ y = z All goals completed! 🐙example : ¬(∀ (y:Real) (z:Real) (n:ℕ) (_: n ≥ 1) (_: y^n = z^n), y = z) := ⊢ ¬∀ (y z : Real), ∀ n ≥ 1, y ^ n = z ^ n → y = z
⊢ ∃ x x_1 x_2, 1 ≤ x_2 ∧ x ^ x_2 = x_1 ^ x_2 ∧ ¬x = x_1; ⊢ 1 ≤ 2⊢ (-3) ^ 2 = 3 ^ 2⊢ ¬-3 = 3 ⊢ 1 ≤ 2⊢ (-3) ^ 2 = 3 ^ 2⊢ ¬-3 = 3 All goals completed! 🐙Definition 5.6.7
noncomputable instance Real.instRatPow : Pow Real ℚ where
pow x q := x.ratPow qtheorem Rat.eq_quot (q:ℚ) : ∃ a:ℤ, ∃ b:ℕ, b > 0 ∧ q = a / b := q:ℚ⊢ ∃ a, ∃ b > 0, q = ↑a / ↑b
q:ℚ⊢ q.den > 0 ∧ q = ↑q.num / ↑q.den; q:ℚthis:q.den ≠ 0⊢ q.den > 0 ∧ q = ↑q.num / ↑q.den
refine ⟨ q:ℚthis:q.den ≠ 0⊢ q.den > 0 All goals completed! 🐙, (Rat.num_div_den q).symm ⟩Lemma 5.6.8
theorem 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) := a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a
-- This proof is written to follow the structure of the original text.
a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0this:∀ {a a' : ℤ} {b b' : ℕ}, b > 0 → b' > 0 → ↑a / ↑b = ↑a' / ↑b' → a > 0 → x.root b' ^ a' = x.root b ^ aha:¬a > 0⊢ x.root b' ^ a' = x.root b ^ ax:Realhx:x > 0a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'ha:a > 0⊢ x.root b' ^ a' = x.root b ^ a
a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0this:∀ {a a' : ℤ} {b b' : ℕ}, b > 0 → b' > 0 → ↑a / ↑b = ↑a' / ↑b' → a > 0 → x.root b' ^ a' = x.root b ^ aha:¬a > 0⊢ x.root b' ^ a' = x.root b ^ a a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0this:∀ {a a' : ℤ} {b b' : ℕ}, b > 0 → b' > 0 → ↑a / ↑b = ↑a' / ↑b' → a > 0 → x.root b' ^ a' = x.root b ^ aha:a ≤ 0⊢ x.root b' ^ a' = x.root b ^ a
a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0this:∀ {a a' : ℤ} {b b' : ℕ}, b > 0 → b' > 0 → ↑a / ↑b = ↑a' / ↑b' → a > 0 → x.root b' ^ a' = x.root b ^ aha✝:a ≤ 0ha:a < 0⊢ x.root b' ^ a' = x.root b ^ aa:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0this:∀ {a a' : ℤ} {b b' : ℕ}, b > 0 → b' > 0 → ↑a / ↑b = ↑a' / ↑b' → a > 0 → x.root b' ^ a' = x.root b ^ aha✝:a ≤ 0ha:a = 0⊢ x.root b' ^ a' = x.root b ^ a
a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0this:∀ {a a' : ℤ} {b b' : ℕ}, b > 0 → b' > 0 → ↑a / ↑b = ↑a' / ↑b' → a > 0 → x.root b' ^ a' = x.root b ^ aha✝:a ≤ 0ha:a < 0⊢ x.root b' ^ a' = x.root b ^ a replace hq : ((-a:ℤ)/b:ℚ) = ((-a':ℤ)/b':ℚ) := a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a
a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0this:∀ {a a' : ℤ} {b b' : ℕ}, b > 0 → b' > 0 → ↑a / ↑b = ↑a' / ↑b' → a > 0 → x.root b' ^ a' = x.root b ^ aha✝:a ≤ 0ha:a < 0⊢ -↑a / ↑b = -↑a' / ↑b'; a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0x:Realhx:x > 0ha✝:a ≤ 0ha:a < 0this:∀ {a a' : ℤ} {b b' : ℕ}, b > 0 → b' > 0 → ↑a * (↑b)⁻¹ = ↑a' * (↑b')⁻¹ → a > 0 → x.root b' ^ a' = x.root b ^ ahq:↑a * (↑b)⁻¹ = ↑a' * (↑b')⁻¹⊢ -(↑a * (↑b)⁻¹) = -(↑a' * (↑b')⁻¹); All goals completed! 🐙
specialize this hb hb' hq (a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0x:Realhx:x > 0this:∀ {a a' : ℤ} {b b' : ℕ}, b > 0 → b' > 0 → ↑a / ↑b = ↑a' / ↑b' → a > 0 → x.root b' ^ a' = x.root b ^ aha✝:a ≤ 0ha:a < 0hq:↑(-a) / ↑b = ↑(-a') / ↑b'⊢ -a > 0 All goals completed! 🐙)
All goals completed! 🐙
have : a' = 0 := a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a All goals completed! 🐙
All goals completed! 🐙
have : a' > 0 := a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a All goals completed! 🐙
x:Realhx:x > 0a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0ha:a > 0this:a' > 0hq:↑a * ↑b' = ↑b * ↑a'⊢ x.root b' ^ a' = x.root b ^ a
lift a to ℕ using x:Realhx:x > 0a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0ha:a > 0this:a' > 0hq:↑a * ↑b' = ↑b * ↑a'⊢ 0 ≤ a All goals completed! 🐙
lift a' to ℕ using x:Realhx:x > 0a':ℤb:ℕb':ℕhb:b > 0hb':b' > 0this:a' > 0a:ℕha:↑a > 0hq:↑↑a * ↑b' = ↑b * ↑a'⊢ 0 ≤ a' All goals completed! 🐙
x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = b * a'⊢ x.root b' ^ a' = x.root b ^ a
x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = b * a'y:Real := x.root (a * b')⊢ x.root b' ^ a' = x.root b ^ a
have h1 : y = (x.root b').root a := a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = b * a'y:Real := x.root (a * b')⊢ x ≥ 0x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = b * a'y:Real := x.root (a * b')⊢ b' ≥ 1x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = b * a'y:Real := x.root (a * b')⊢ a ≥ 1 x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = b * a'y:Real := x.root (a * b')⊢ x ≥ 0x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = b * a'y:Real := x.root (a * b')⊢ b' ≥ 1x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = b * a'y:Real := x.root (a * b')⊢ a ≥ 1 All goals completed! 🐙
have h2 : y = (x.root b).root a' := a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = b * a'y:Real := x.root (a * b')h1:y = (x.root b').root a⊢ x ≥ 0x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = b * a'y:Real := x.root (a * b')h1:y = (x.root b').root a⊢ b ≥ 1x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = b * a'y:Real := x.root (a * b')h1:y = (x.root b').root a⊢ a' ≥ 1 x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = b * a'y:Real := x.root (a * b')h1:y = (x.root b').root a⊢ x ≥ 0x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = b * a'y:Real := x.root (a * b')h1:y = (x.root b').root a⊢ b ≥ 1x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = b * a'y:Real := x.root (a * b')h1:y = (x.root b').root a⊢ a' ≥ 1 All goals completed! 🐙
have h3 : y^a = x.root b' := a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = b * a'y:Real := x.root (a * b')h1:y = (x.root b').root ah2:y = (x.root b).root a'⊢ (x.root b').root a ^ a = x.root b'; x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = b * a'y:Real := x.root (a * b')h1:y = (x.root b').root ah2:y = (x.root b).root a'⊢ a ≥ 1x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = b * a'y:Real := x.root (a * b')h1:y = (x.root b').root ah2:y = (x.root b).root a'⊢ x ≥ 0x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = b * a'y:Real := x.root (a * b')h1:y = (x.root b').root ah2:y = (x.root b).root a'⊢ b' ≥ 1 x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = b * a'y:Real := x.root (a * b')h1:y = (x.root b').root ah2:y = (x.root b).root a'⊢ a ≥ 1x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = b * a'y:Real := x.root (a * b')h1:y = (x.root b').root ah2:y = (x.root b).root a'⊢ x ≥ 0x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = b * a'y:Real := x.root (a * b')h1:y = (x.root b').root ah2:y = (x.root b).root a'⊢ b' ≥ 1 All goals completed! 🐙
have h4 : y^a' = x.root b := a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = b * a'y:Real := x.root (a * b')h1:y = (x.root b').root ah2:y = (x.root b).root a'h3:y ^ a = x.root b'⊢ (x.root b).root a' ^ a' = x.root b; x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = b * a'y:Real := x.root (a * b')h1:y = (x.root b').root ah2:y = (x.root b).root a'h3:y ^ a = x.root b'⊢ a' ≥ 1x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = b * a'y:Real := x.root (a * b')h1:y = (x.root b').root ah2:y = (x.root b).root a'h3:y ^ a = x.root b'⊢ x ≥ 0x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = b * a'y:Real := x.root (a * b')h1:y = (x.root b').root ah2:y = (x.root b).root a'h3:y ^ a = x.root b'⊢ b ≥ 1 x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = b * a'y:Real := x.root (a * b')h1:y = (x.root b').root ah2:y = (x.root b).root a'h3:y ^ a = x.root b'⊢ a' ≥ 1x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = b * a'y:Real := x.root (a * b')h1:y = (x.root b').root ah2:y = (x.root b).root a'h3:y ^ a = x.root b'⊢ x ≥ 0x:Realb:ℕb':ℕhb:b > 0hb':b' > 0a:ℕa':ℕhx:x > 0ha:0 < athis:0 < a'hq:a * b' = b * a'y:Real := x.root (a * b')h1:y = (x.root b').root ah2:y = (x.root b).root a'h3:y ^ a = x.root b'⊢ b ≥ 1 All goals completed! 🐙
All goals completed! 🐙theorem Real.ratPow_def {x:Real} (hx: x > 0) (a:ℤ) {b:ℕ} (hb: b > 0) : x^(a/b:ℚ) = (x.root b)^a := x:Realhx:x > 0a:ℤb:ℕhb:b > 0⊢ x ^ (↑a / ↑b) = x.root b ^ a
x:Realhx:x > 0a:ℤb:ℕhb:b > 0q:ℚ := ↑a / ↑b⊢ x ^ q = x.root b ^ a
x:Realhx:x > 0a:ℤb:ℕhb:b > 0q:ℚ := ↑a / ↑b⊢ q.den > 0x:Realhx:x > 0a:ℤb:ℕhb:b > 0q:ℚ := ↑a / ↑b⊢ ↑a / ↑b = ↑q.num / ↑q.den
x:Realhx:x > 0a:ℤb:ℕhb:b > 0q:ℚ := ↑a / ↑b⊢ q.den > 0 x:Realhx:x > 0a:ℤb:ℕhb:b > 0q:ℚ := ↑a / ↑bthis:q.den ≠ 0⊢ q.den > 0; All goals completed! 🐙
All goals completed! 🐙theorem Real.ratPow_eq_root {x:Real} (hx: x > 0) {n:ℕ} (hn: n ≥ 1) : x^(1/n:ℚ) = x.root n := x:Realhx:x > 0n:ℕhn:n ≥ 1⊢ x ^ (1 / ↑n) = x.root n All goals completed! 🐙theorem Real.ratPow_eq_pow {x:Real} (hx: x > 0) (n:ℤ) : x^(n:ℚ) = x^n := x:Realhx:x > 0n:ℤ⊢ x ^ ↑n = x ^ n All goals completed! 🐙Lemma 5.6.9(a) / Exercise 5.6.2
theorem Real.ratPow_pos {x:Real} (hx: x > 0) (q:ℚ) : x^q > 0 := x:Realhx:x > 0q:ℚ⊢ x ^ q > 0
All goals completed! 🐙Lemma 5.6.9(b) / Exercise 5.6.2
theorem Real.ratPow_add {x:Real} (hx: x > 0) (q r:ℚ) : x^(q+r) = x^q * x^r := x:Realhx:x > 0q:ℚr:ℚ⊢ x ^ (q + r) = x ^ q * x ^ r
All goals completed! 🐙Lemma 5.6.9(b) / Exercise 5.6.2
theorem Real.ratPow_ratPow {x:Real} (hx: x > 0) (q r:ℚ) : (x^q)^r = x^(q*r) := x:Realhx:x > 0q:ℚr:ℚ⊢ (x ^ q) ^ r = x ^ (q * r)
All goals completed! 🐙Lemma 5.6.9(c) / Exercise 5.6.2
theorem Real.ratPow_neg {x:Real} (hx: x > 0) (q:ℚ) : x^(-q) = 1 / x^q := x:Realhx:x > 0q:ℚ⊢ x ^ (-q) = 1 / x ^ q
All goals completed! 🐙Lemma 5.6.9(d) / Exercise 5.6.2
theorem Real.ratPow_mono {x y:Real} (hx: x > 0) (hy: y > 0) {q:ℚ} (h: q > 0) : x > y ↔ x^q > y^q := x:Realy:Realhx:x > 0hy:y > 0q:ℚh:q > 0⊢ x > y ↔ x ^ q > y ^ q
All goals completed! 🐙Lemma 5.6.9(e) / Exercise 5.6.2
theorem Real.ratPow_mono_of_gt_one {x:Real} (hx: x > 1) {q r:ℚ} : x^q > x^r ↔ q > r := x:Realhx:x > 1q:ℚr:ℚ⊢ x ^ q > x ^ r ↔ q > r
All goals completed! 🐙Lemma 5.6.9(e) / Exercise 5.6.2
theorem Real.ratPow_mono_of_lt_one {x:Real} (hx0: 0 < x) (hx: x < 1) {q r:ℚ} : x^q > x^r ↔ q < r := x:Realhx0:0 < xhx:x < 1q:ℚr:ℚ⊢ x ^ q > x ^ r ↔ q < r
All goals completed! 🐙Lemma 5.6.9(f) / Exercise 5.6.2
theorem Real.ratPow_mul {x y:Real} (hx: x > 0) (hy: y > 0) (q:ℚ) : (x*y)^q = x^q * y^q := x:Realy:Realhx:x > 0hy:y > 0q:ℚ⊢ (x * y) ^ q = x ^ q * y ^ q
All goals completed! 🐙Exercise 5.6.3
theorem Real.pow_even (x:Real) {n:ℕ} (hn: Even n) : x^n ≥ 0 := x:Realn:ℕhn:Even n⊢ x ^ n ≥ 0 All goals completed! 🐙Exercise 5.6.5
theorem 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 := x:Realy:Realhx:x > 0hy:y > 0q:ℚhq:q > 0⊢ max (x ^ q) (y ^ q) = max x y ^ q
All goals completed! 🐙Exercise 5.6.5
theorem 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 := x:Realy:Realhx:x > 0hy:y > 0q:ℚhq:q > 0⊢ min (x ^ q) (y ^ q) = min x y ^ q
All goals completed! 🐙-- Final part of Exercise 5.6.5: state and prove versions of the above lemmas covering the case of negative q.
end Chapter5