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)

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

Definition 5.6.1 (Exponentiating a real by a natural number). Here we use the Mathlib definition coming from 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)

Analogue of Proposition 4.3.10(a)

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

Analogue of Proposition 4.3.10(a)

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

Analogue of Proposition 4.3.10(a)

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

Analogue of Proposition 4.3.10(b)

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

Analogue of Proposition 4.3.10(c)

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

Analogue of Proposition 4.3.10(c)

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

Analogue of Proposition 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

Analogue of Proposition 4.3.10(c)

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

Analogue of Proposition 4.3.10(d)

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

Definition 5.6.2 (Exponentiating a real by an integer). Here we use the Mathlib definition coming from 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)

Analogue of Proposition 4.3.12(a)

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

Analogue of Proposition 4.3.12(a)

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

Analogue of Proposition 4.3.12(a)

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

Analogue of Proposition 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

Analogue of Proposition 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

Analogue of Proposition 4.3.12(c)

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

Analogue of Proposition 4.3.12(d)

@[reducible, inline]

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

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

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

Lemma 5.6.5 (Existence of n^th roots)

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

Lemma 5.6.6 (ab) / Exercise 5.6.1

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

Lemma 5.6.6 (c) / Exercise 5.6.1

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

Lemma 5.6.6 (c) / Exercise 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

Lemma 5.6.6 (d) / Exercise 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

Lemma 5.6.6 (e) / Exercise 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

Lemma 5.6.6 (e) / Exercise 5.6.1

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

Lemma 5.6.6 (e) / Exercise 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

Lemma 5.6.6 (f) / Exercise 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)

Lemma 5.6.6 (f) / Exercise 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

Definition 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

Lemma 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_nonneg {x : Real} (hx : x > 0) (q : ℚ) : x ^ q > 0

Lemma 5.6.9(a) / Exercise 5.6.2

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

Lemma 5.6.9(b) / Exercise 5.6.2

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

Lemma 5.6.9(b) / Exercise 5.6.2

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

Lemma 5.6.9(c) / Exercise 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

Lemma 5.6.9(d) / Exercise 5.6.2

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

Lemma 5.6.9(e) / Exercise 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

Lemma 5.6.9(e) / Exercise 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

Lemma 5.6.9(f) / Exercise 5.6.2

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

Exercise 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

Exercise 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

Exercise 5.6.5