Analysis
5.6. Real exponentiation, part I

Imports

import Mathlib.Tactic
import Analysis.Section_5_5

Analysis 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 := rfl

lemma Real.pow_succ (x: Real) (n:ℕ) : x ^ (n+1) = (x ^ n) * x := rfl

lemma Real.pow_of_coe (q: ℚ) (n:ℕ) : (q:Real) ^ n = (q ^ n:ℚ) := byq:ℚn:ℕ⊢ ↑q ^ n = ↑(q ^ n) induction' n with n hnzeroq:ℚ⊢ ↑q ^ 0 = ↑(q ^ 0)succq:ℚn:ℕhn:↑q ^ n = ↑(q ^ n)⊢ ↑q ^ (n + 1) = ↑(q ^ (n + 1)) <;>zeroq:ℚ⊢ ↑q ^ 0 = ↑(q ^ 0)succq:ℚn:ℕhn:↑q ^ n = ↑(q ^ n)⊢ ↑q ^ (n + 1) = ↑(q ^ (n + 1)) simpAll goals completed! 🐙

Analogue of Proposition 4.3.10(a) (sum of exponents)

/- 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 declaration uses `sorry`Real.pow_add (x:Real) (m n:ℕ) : x^n * x^m = x^(n+m) := byx:Realm:ℕn:ℕ⊢ x ^ n * x ^ m = x ^ (n + m) sorryAll goals completed! 🐙

Analogue of Proposition 4.3.10(a) (product of exponents)

theorem declaration uses `sorry`Real.pow_mul (x:Real) (m n:ℕ) : (x^n)^m = x^(n*m) := byx:Realm:ℕn:ℕ⊢ (x ^ n) ^ m = x ^ (n * m) sorryAll goals completed! 🐙

Analogue of Proposition 4.3.10(a) (power of a product)

theorem declaration uses `sorry`Real.mul_pow (x y:Real) (n:ℕ) : (x*y)^n = x^n * y^n := byx:Realy:Realn:ℕ⊢ (x * y) ^ n = x ^ n * y ^ n sorryAll goals completed! 🐙

Analogue of Proposition 4.3.10(b)

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

Analogue of Proposition 4.3.10(c) (nonnegativity)

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

Analogue of Proposition 4.3.10(c) (positivity)

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

Analogue of Proposition 4.3.10(c) (monotone, non-strict)

theorem declaration uses `sorry`Real.pow_ge_pow (x y:Real) (n:ℕ) (hxy: x ≥ y) (hy: y ≥ 0) : x^n ≥ y^n := byx:Realy:Realn:ℕhxy:x ≥ yhy:y ≥ 0⊢ x ^ n ≥ y ^ n sorryAll goals completed! 🐙

Analogue of Proposition 4.3.10(c) (monotone, strict)

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

Analogue of Proposition 4.3.10(d)

theorem declaration uses `sorry`Real.pow_abs (x:Real) (n:ℕ) : |x|^n = |x^n| := byx:Realn:ℕ⊢ |x| ^ n = |x ^ n| sorryAll 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 := byx:Realn:ℕ⊢ x ^ ↑n = x ^ n rflAll goals completed! 🐙

@[simp]
lemma Real.zpow_zero (x: Real) : x ^ (0:ℤ) = 1 := byx:Real⊢ x ^ 0 = 1 rflAll goals completed! 🐙

lemma Real.zpow_neg {x:Real} (n:ℕ) : x^(-n:ℤ) = 1 / (x^n) := byx:Realn:ℕ⊢ x ^ (-↑n) = 1 / x ^ n simpAll goals completed! 🐙

Analogue of Proposition 4.3.12(a) (sum of exponents)

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

Analogue of Proposition 4.3.12(a) (product of exponents)

theorem declaration uses `sorry`Real.zpow_mul (x:Real) (n m:ℤ) : (x^n)^m = x^(n*m) := byx:Realn:ℤm:ℤ⊢ (x ^ n) ^ m = x ^ (n * m) sorryAll goals completed! 🐙

Analogue of Proposition 4.3.12(a) (power of a product)

theorem declaration uses `sorry`Real.mul_zpow (x y:Real) (n:ℤ) : (x*y)^n = x^n * y^n := byx:Realy:Realn:ℤ⊢ (x * y) ^ n = x ^ n * y ^ n sorryAll goals completed! 🐙

Analogue of Proposition 4.3.12(b) (positivity)

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

Analogue of Proposition 4.3.12(b) (monotone)

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

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

Analogue of Proposition 4.3.12(c)

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

Analogue of Proposition 4.3.12(d)

theorem declaration uses `sorry`Real.zpow_abs (x:Real) (n:ℤ) : |x|^n = |x^n| := byx:Realn:ℤ⊢ |x| ^ n = |x ^ n| sorryAll goals completed! 🐙

Definition 5.6.2. We permit "junk values" when x is negative or n vanishes.

noncomputable abbrev Real.root (x:Real) (n:ℕ) : Real := sSup { y:Real | y ≥ 0 ∧ y^n ≤ x }

noncomputable abbrev Real.sqrt (x:Real) := x.root 2

Lemma 5.6.5 (Existence of n^th roots)

theorem declaration uses `sorry`Real.rootset_nonempty {x:Real} (hx: x ≥ 0) (n:ℕ) (hn: n ≥ 1) : { y:Real | y ≥ 0 ∧ y^n ≤ x }.Nonempty := byx:Realhx:x ≥ 0n:ℕhn:n ≥ 1⊢ {y | y ≥ 0 ∧ y ^ n ≤ x}.Nonempty
  use 0hx:Realhx:x ≥ 0n:ℕhn:n ≥ 1⊢ 0 ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}
  sorryAll goals completed! 🐙

theorem declaration uses `sorry`Real.rootset_bddAbove {x:Real} (n:ℕ) (hn: n ≥ 1) : BddAbove { y:Real | y ≥ 0 ∧ y^n ≤ x } := byx:Realn:ℕhn:n ≥ 1⊢ BddAbove {y | y ≥ 0 ∧ y ^ n ≤ x}
  -- This proof is written to follow the structure of the original text.
  rw [_root_.bddAbove_def]x:Realn:ℕhn:n ≥ 1⊢ ∃ x_1, ∀ y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}, y ≤ x_1
  obtain h | h := le_or_gt x 1inlx:Realn:ℕhn:n ≥ 1h:x ≤ 1⊢ ∃ x_1, ∀ y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}, y ≤ x_1inrx:Realn:ℕhn:n ≥ 1h:1 < x⊢ ∃ x_1, ∀ y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}, y ≤ x_1
  .inlx:Realn:ℕhn:n ≥ 1h:x ≤ 1⊢ ∃ x_1, ∀ y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}, y ≤ x_1 use 1hx:Realn:ℕhn:n ≥ 1h:x ≤ 1⊢ ∀ y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}, y ≤ 1; intro y hyhx:Realn:ℕhn:n ≥ 1h:x ≤ 1y:Realhy:y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}⊢ y ≤ 1; simp at hyhx:Realn:ℕhn:n ≥ 1h:x ≤ 1y:Realhy:0 ≤ y ∧ y ^ n ≤ x⊢ y ≤ 1
    by_contra! hy'hx:Realn:ℕhn:n ≥ 1h:x ≤ 1y:Realhy:0 ≤ y ∧ y ^ n ≤ xhy':1 < y⊢ False
    replace hy' : 1 < y^n := byx:Realn:ℕhn:n ≥ 1⊢ BddAbove {y | y ≥ 0 ∧ y ^ n ≤ x}
      sorryAll goals completed! 🐙
    linarithAll goals completed! 🐙
  use xhx:Realn:ℕhn:n ≥ 1h:1 < x⊢ ∀ y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}, y ≤ x; intro y hyhx:Realn:ℕhn:n ≥ 1h:1 < xy:Realhy:y ∈ {y | y ≥ 0 ∧ y ^ n ≤ x}⊢ y ≤ x; simp at hyhx:Realn:ℕhn:n ≥ 1h:1 < xy:Realhy:0 ≤ y ∧ y ^ n ≤ x⊢ y ≤ x
  by_contra! hy'hx:Realn:ℕhn:n ≥ 1h:1 < xy:Realhy:0 ≤ y ∧ y ^ n ≤ xhy':x < y⊢ False
  replace hy' : x < y^n := byx:Realn:ℕhn:n ≥ 1⊢ BddAbove {y | y ≥ 0 ∧ y ^ n ≤ x}
    sorryAll goals completed! 🐙
  linarithAll goals completed! 🐙

Lemma 5.6.6 (ab) / Exercise 5.6.1

theorem declaration uses `sorry`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 := byx:Realy:Realhx:x ≥ 0hy:y ≥ 0n:ℕhn:n ≥ 1⊢ y = x.root n ↔ y ^ n = x sorryAll goals completed! 🐙

Lemma 5.6.6 (c) (nonnegativity) / Exercise 5.6.1

theorem declaration uses `sorry`Real.root_nonneg {x:Real} (hx: x ≥ 0) {n:ℕ} (hn: n ≥ 1) : x.root n ≥ 0 := byx:Realhx:x ≥ 0n:ℕhn:n ≥ 1⊢ x.root n ≥ 0 sorryAll goals completed! 🐙

Lemma 5.6.6 (c) (positivity) / Exercise 5.6.1

theorem declaration uses `sorry`Real.root_pos {x:Real} (hx: x ≥ 0) {n:ℕ} (hn: n ≥ 1) : x.root n > 0 ↔ x > 0 := byx:Realhx:x ≥ 0n:ℕhn:n ≥ 1⊢ x.root n > 0 ↔ x > 0 sorryAll goals completed! 🐙

theorem declaration uses `sorry`Real.pow_of_root {x:Real} (hx: x ≥ 0) {n:ℕ} (hn: n ≥ 1) :
  (x.root n)^n = x := byx:Realhx:x ≥ 0n:ℕhn:n ≥ 1⊢ x.root n ^ n = x sorryAll goals completed! 🐙

theorem declaration uses `sorry`Real.root_of_pow {x:Real} (hx: x ≥ 0) {n:ℕ} (hn: n ≥ 1) :
  (x^n).root n = x := byx:Realhx:x ≥ 0n:ℕhn:n ≥ 1⊢ (x ^ n).root n = x sorryAll goals completed! 🐙

Lemma 5.6.6 (d) / Exercise 5.6.1

theorem declaration uses `sorry`Real.root_mono {x y:Real} (hx: x ≥ 0) (hy: y ≥ 0) {n:ℕ} (hn: n ≥ 1) : x > y ↔ x.root n > y.root n := byx:Realy:Realhx:x ≥ 0hy:y ≥ 0n:ℕhn:n ≥ 1⊢ x > y ↔ x.root n > y.root n sorryAll goals completed! 🐙

Lemma 5.6.6 (e) (base greater than one) / Exercise 5.6.1

theorem declaration uses `sorry`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 := byx:Realhx:x > 1k:ℕl:ℕhkl:k > lhl:l ≥ 1⊢ x.root k < x.root l sorryAll goals completed! 🐙

Lemma 5.6.6 (e) (base less than one) / Exercise 5.6.1

theorem declaration uses `sorry`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 := byx:Realhx0:0 < xhx:x < 1k:ℕl:ℕhkl:k > lhl:l ≥ 1⊢ x.root k > x.root l sorryAll goals completed! 🐙

Lemma 5.6.6 (e) (base one) / Exercise 5.6.1

theorem declaration uses `sorry`Real.root_of_one {k: ℕ} (hk: k ≥ 1): (1:Real).root k = 1 := byk:ℕhk:k ≥ 1⊢ root 1 k = 1 sorryAll goals completed! 🐙

Lemma 5.6.6 (f) / Exercise 5.6.1

theorem declaration uses `sorry`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) := byx:Realy:Realhx:x ≥ 0hy:y ≥ 0n:ℕhn:n ≥ 1⊢ (x * y).root n = x.root n * y.root n sorryAll goals completed! 🐙

Lemma 5.6.6 (g) / Exercise 5.6.1

theorem declaration uses `sorry`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) := byx:Realhx:x ≥ 0n:ℕm:ℕhn:n ≥ 1hm:m ≥ 1⊢ (x.root n).root m = x.root (n * m) sorryAll goals completed! 🐙

              theorem declaration uses `sorry`Real.root_one {x:Real} (hx: x > 0): x.root 1 = x := byx:Realhx:x > 0⊢ x.root 1 = x sorryAll goals completed! 🐙theorem declaration uses `sorry`Real.pow_cancel {y z:Real} (hy: y > 0) (hz: z > 0) {n:ℕ} (hn: n ≥ 1)
  (h: y^n = z^n) : y = z := byy:Realz:Realhy:y > 0hz:z > 0n:ℕhn:n ≥ 1h:y ^ n = z ^ n⊢ y = z sorryAll goals completed! 🐙example : ¬(∀ (y:Real) (z:Real) (n:ℕ) (_: n ≥ 1) (_: y^n = z^n), y = z) := by⊢ ¬∀ (y z : Real), ∀ n ≥ 1, y ^ n = z ^ n → y = z
  simp⊢ ∃ x x_1 x_2, 1 ≤ x_2 ∧ x ^ x_2 = x_1 ^ x_2 ∧ ¬x = x_1; refine ⟨ (-3), 3, 2, ?_, ?_, ?_ ⟩refine_1⊢ 1 ≤ 2refine_2⊢ (-3) ^ 2 = 3 ^ 2refine_3⊢ ¬-3 = 3 <;>refine_1⊢ 1 ≤ 2refine_2⊢ (-3) ^ 2 = 3 ^ 2refine_3⊢ ¬-3 = 3 norm_numAll goals completed! 🐙

Definition 5.6.7

noncomputable abbrev Real.ratPow (x:Real) (q:ℚ) : Real := (x.root q.den)^(q.num)

noncomputable instance Real.instRatPow : Pow Real ℚ where
  pow x q := x.ratPow q

theorem Rat.eq_quot (q:ℚ) : ∃ a:ℤ, ∃ b:ℕ, b > 0 ∧ q = a / b := byq:ℚ⊢ ∃ a, ∃ b > 0, q = ↑a / ↑b
  use q.num, q.denhq:ℚ⊢ q.den > 0 ∧ q = ↑q.num / ↑q.den; have := q.den_nzhq:ℚthis:q.den ≠ 0⊢ q.den > 0 ∧ q = ↑q.num / ↑q.den
  refine ⟨ byq:ℚthis:q.den ≠ 0⊢ q.den > 0 omegaAll goals completed! 🐙, (Rat.num_div_den q).symm ⟩

Lemma 5.6.8

theorem declaration uses `sorry`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) := bya:ℤ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.
  wlog ha: a > 0 generalizing a b a' b'inra:ℤ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
  .inra:ℤ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 simp at hainra:ℤ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
    obtain ha | ha := le_iff_lt_or_eq.mp hainr.inla:ℤ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 ^ ainr.inra:ℤ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
    .inr.inla:ℤ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':ℚ) := bya:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a
        push_cast at *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'; ring_nf at *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')⁻¹); simp [hq]All goals completed! 🐙
      specialize this hb hb' hq (bya:ℤ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 linarithAll goals completed! 🐙)
      simpa [zpow_neg] using thisAll goals completed! 🐙
    have : a' = 0 := bya:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a sorryAll goals completed! 🐙
    simp_allAll goals completed! 🐙
  have : a' > 0 := bya:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a sorryAll goals completed! 🐙
  field_simp at hqx: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 byx:Realhx:x > 0a:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0ha:a > 0this:a' > 0hq:↑a * ↑b' = ↑b * ↑a'⊢ 0 ≤ a orderAll goals completed! 🐙
  lift a' to ℕ using byx:Realhx:x > 0a':ℤb:ℕb':ℕhb:b > 0hb':b' > 0this:a' > 0a:ℕha:↑a > 0hq:↑↑a * ↑b' = ↑b * ↑a'⊢ 0 ≤ a' orderAll goals completed! 🐙
  norm_cast at *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
  set y := x.root (a*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')⊢ x.root b' ^ a' = x.root b ^ a
  have h1 : y = (x.root b').root a := bya:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a rw [root_root, mul_comm]hxx: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 ≥ 0hnx: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' ≥ 1hmx: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 <;>hxx: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 ≥ 0hnx: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' ≥ 1hmx: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 linarithAll goals completed! 🐙
  have h2 : y = (x.root b).root a' := bya:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a rw [root_root, ←hq]hxx: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 ≥ 0hnx: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 ≥ 1hmx: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 <;>hxx: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 ≥ 0hnx: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 ≥ 1hmx: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 linarithAll goals completed! 🐙
  have h3 : y^a = x.root b' := bya:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a rw [h1]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'; apply pow_of_root (root_nonneg _ _)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 linarithAll goals completed! 🐙
  have h4 : y^a' = x.root b := bya:ℤa':ℤb:ℕb':ℕhb:b > 0hb':b' > 0hq:↑a / ↑b = ↑a' / ↑b'x:Realhx:x > 0⊢ x.root b' ^ a' = x.root b ^ a rw [h2]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; apply pow_of_root (root_nonneg _ _)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 linarithAll goals completed! 🐙
  rw [←h3, pow_mul, mul_comm, ←pow_mul, h4]All goals completed! 🐙

              theorem Real.ratPow_def {x:Real} (hx: x > 0) (a:ℤ) {b:ℕ} (hb: b > 0) : x^(a/b:ℚ) = (x.root b)^a := byx:Realhx:x > 0a:ℤb:ℕhb:b > 0⊢ x ^ (↑a / ↑b) = x.root b ^ a
  set q := (a/b:ℚ)x:Realhx:x > 0a:ℤb:ℕhb:b > 0q:ℚ := ↑a / ↑b⊢ x ^ q = x.root b ^ a
  convert pow_root_eq_pow_root hb _ _ hxconvert_4x:Realhx:x > 0a:ℤb:ℕhb:b > 0q:ℚ := ↑a / ↑b⊢ q.den > 0convert_5x:Realhx:x > 0a:ℤb:ℕhb:b > 0q:ℚ := ↑a / ↑b⊢ ↑a / ↑b = ↑q.num / ↑q.den
  .convert_4x:Realhx:x > 0a:ℤb:ℕhb:b > 0q:ℚ := ↑a / ↑b⊢ q.den > 0 have := q.den_nzconvert_4x:Realhx:x > 0a:ℤb:ℕhb:b > 0q:ℚ := ↑a / ↑bthis:q.den ≠ 0⊢ q.den > 0; omegaAll goals completed! 🐙
  rw [Rat.num_div_den q]All goals completed! 🐙theorem declaration uses `sorry`Real.ratPow_eq_root {x:Real} (hx: x > 0) {n:ℕ} (hn: n ≥ 1) : x^(1/n:ℚ) = x.root n := byx:Realhx:x > 0n:ℕhn:n ≥ 1⊢ x ^ (1 / ↑n) = x.root n sorryAll goals completed! 🐙theorem declaration uses `sorry`Real.ratPow_eq_pow {x:Real} (hx: x > 0) (n:ℤ) : x^(n:ℚ) = x^n := byx:Realhx:x > 0n:ℤ⊢ x ^ ↑n = x ^ n sorryAll goals completed! 🐙

Lemma 5.6.9(a) / Exercise 5.6.2

theorem declaration uses `sorry`Real.ratPow_pos {x:Real} (hx: x > 0) (q:ℚ) : x^q > 0 := byx:Realhx:x > 0q:ℚ⊢ x ^ q > 0
  sorryAll goals completed! 🐙

Lemma 5.6.9(b) (sum of exponents) / Exercise 5.6.2

theorem declaration uses `sorry`Real.ratPow_add {x:Real} (hx: x > 0) (q r:ℚ) : x^(q+r) = x^q * x^r := byx:Realhx:x > 0q:ℚr:ℚ⊢ x ^ (q + r) = x ^ q * x ^ r
  sorryAll goals completed! 🐙

Lemma 5.6.9(b) (product of exponents) / Exercise 5.6.2

theorem declaration uses `sorry`Real.ratPow_ratPow {x:Real} (hx: x > 0) (q r:ℚ) : (x^q)^r = x^(q*r) := byx:Realhx:x > 0q:ℚr:ℚ⊢ (x ^ q) ^ r = x ^ (q * r)
  sorryAll goals completed! 🐙

Lemma 5.6.9(c) / Exercise 5.6.2

theorem declaration uses `sorry`Real.ratPow_neg {x:Real} (hx: x > 0) (q:ℚ) : x^(-q) = 1 / x^q := byx:Realhx:x > 0q:ℚ⊢ x ^ (-q) = 1 / x ^ q
  sorryAll goals completed! 🐙

Lemma 5.6.9(d) / Exercise 5.6.2

theorem declaration uses `sorry`Real.ratPow_mono {x y:Real} (hx: x > 0) (hy: y > 0) {q:ℚ} (h: q > 0) : x > y ↔ x^q > y^q := byx:Realy:Realhx:x > 0hy:y > 0q:ℚh:q > 0⊢ x > y ↔ x ^ q > y ^ q
  sorryAll goals completed! 🐙

Lemma 5.6.9(e) (base greater than one) / Exercise 5.6.2

theorem declaration uses `sorry`Real.ratPow_mono_of_gt_one {x:Real} (hx: x > 1) {q r:ℚ} : x^q > x^r ↔ q > r := byx:Realhx:x > 1q:ℚr:ℚ⊢ x ^ q > x ^ r ↔ q > r
  sorryAll goals completed! 🐙

Lemma 5.6.9(e) (base less than one) / Exercise 5.6.2

theorem declaration uses `sorry`Real.ratPow_mono_of_lt_one {x:Real} (hx0: 0 < x) (hx: x < 1) {q r:ℚ} : x^q > x^r ↔ q < r := byx:Realhx0:0 < xhx:x < 1q:ℚr:ℚ⊢ x ^ q > x ^ r ↔ q < r
  sorryAll goals completed! 🐙

Lemma 5.6.9(f) / Exercise 5.6.2

theorem declaration uses `sorry`Real.ratPow_mul {x y:Real} (hx: x > 0) (hy: y > 0) (q:ℚ) : (x*y)^q = x^q * y^q := byx:Realy:Realhx:x > 0hy:y > 0q:ℚ⊢ (x * y) ^ q = x ^ q * y ^ q
  sorryAll goals completed! 🐙

Exercise 5.6.3

theorem declaration uses `sorry`Real.pow_even (x:Real) {n:ℕ} (hn: Even n) : x^n ≥ 0 := byx:Realn:ℕhn:Even n⊢ x ^ n ≥ 0 sorryAll goals completed! 🐙

Exercise 5.6.5 (a)

theorem declaration uses `sorry`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 := byx:Realy:Realhx:x > 0hy:y > 0q:ℚhq:q > 0⊢ max (x ^ q) (y ^ q) = max x y ^ q
  sorryAll goals completed! 🐙

Exercise 5.6.5 (b)

theorem declaration uses `sorry`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 := byx:Realy:Realhx:x > 0hy:y > 0q:ℚhq:q > 0⊢ min (x ^ q) (y ^ q) = min x y ^ q
  sorryAll 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