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) (sum of exponents)

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

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

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

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

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) (nonnegativity)

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

Analogue of Proposition 4.3.10(c) (positivity)

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) (monotone, non-strict)

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) (monotone, strict)

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) (sum of exponents)

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

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

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

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

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

Analogue of Proposition 4.3.12(b) (positivity)

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) (monotone)

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) (nonnegativity) / 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) (positivity) / 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) (base greater than one) / 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) (base less than one) / Exercise 5.6.1

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

Lemma 5.6.6 (e) (base one) / 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 (g) / 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

@[implicit_reducible]

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_pos {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) (sum of exponents) / 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) (product of exponents) / 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) (base greater than one) / 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) (base less than one) / 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 (a)

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 (b)