mathlibdocumentation

analysis.special_functions.pow

Power function on `ℂ`, `ℝ`, `ℝ≥0`, and `ℝ≥0∞`#

We construct the power functions `x ^ y` where

• `x` and `y` are complex numbers,
• or `x` and `y` are real numbers,
• or `x` is a nonnegative real number and `y` is a real number;
• or `x` is a number from `[0, +∞]` (a.k.a. `ℝ≥0∞`) and `y` is a real number.

We also prove basic properties of these functions.

noncomputable def complex.cpow (x y : ) :

The complex power function `x^y`, given by `x^y = exp(y log x)` (where `log` is the principal determination of the logarithm), unless `x = 0` where one sets `0^0 = 1` and `0^y = 0` for `y ≠ 0`.

Equations
@[protected, instance]
noncomputable def complex.has_pow  :
Equations
@[simp]
theorem complex.cpow_eq_pow (x y : ) :
x.cpow y = x ^ y
theorem complex.cpow_def (x y : ) :
x ^ y = ite (x = 0) (ite (y = 0) 1 0) (cexp * y))
theorem complex.cpow_def_of_ne_zero {x : } (hx : x 0) (y : ) :
x ^ y = cexp * y)
@[simp]
theorem complex.cpow_zero (x : ) :
x ^ 0 = 1
@[simp]
theorem complex.cpow_eq_zero_iff (x y : ) :
x ^ y = 0 x = 0 y 0
@[simp]
theorem complex.zero_cpow {x : } (h : x 0) :
0 ^ x = 0
theorem complex.zero_cpow_eq_iff {x a : } :
0 ^ x = a x 0 a = 0 x = 0 a = 1
theorem complex.eq_zero_cpow_iff {x a : } :
a = 0 ^ x x 0 a = 0 x = 0 a = 1
@[simp]
theorem complex.cpow_one (x : ) :
x ^ 1 = x
@[simp]
theorem complex.one_cpow (x : ) :
1 ^ x = 1
theorem complex.cpow_add {x : } (y z : ) (hx : x 0) :
x ^ (y + z) = x ^ y * x ^ z
theorem complex.cpow_mul {x y : } (z : ) (h₁ : -real.pi < * y).im) (h₂ : * y).im real.pi) :
x ^ (y * z) = (x ^ y) ^ z
theorem complex.cpow_neg (x y : ) :
x ^ -y = (x ^ y)⁻¹
theorem complex.cpow_sub {x : } (y z : ) (hx : x 0) :
x ^ (y - z) = x ^ y / x ^ z
theorem complex.cpow_neg_one (x : ) :
x ^ -1 = x⁻¹
@[simp, norm_cast]
theorem complex.cpow_nat_cast (x : ) (n : ) :
x ^ n = x ^ n
@[simp]
theorem complex.cpow_two (x : ) :
x ^ 2 = x ^ 2
@[simp, norm_cast]
theorem complex.cpow_int_cast (x : ) (n : ) :
x ^ n = x ^ n
theorem complex.cpow_nat_inv_pow (x : ) {n : } (hn : n 0) :
(x ^ (n)⁻¹) ^ n = x
theorem complex.mul_cpow_of_real_nonneg {a b : } (ha : 0 a) (hb : 0 b) (r : ) :
(a * b) ^ r = a ^ r * b ^ r
theorem zero_cpow_eq_nhds {b : } (hb : b 0) :
(λ (x : ), 0 ^ x) =ᶠ[nhds b] 0
theorem cpow_eq_nhds {a b : } (ha : a 0) :
(λ (x : ), x ^ b) =ᶠ[nhds a] λ (x : ), cexp * b)
theorem cpow_eq_nhds' {p : × } (hp_fst : p.fst 0) :
(λ (x : × ), x.fst ^ x.snd) =ᶠ[nhds p] λ (x : × ), cexp * x.snd)
theorem continuous_at_const_cpow {a b : } (ha : a 0) :
continuous_at (λ (x : ), a ^ x) b
theorem continuous_at_const_cpow' {a b : } (h : b 0) :
continuous_at (λ (x : ), a ^ x) b
theorem continuous_at_cpow {p : × } (hp_fst : 0 < p.fst.re p.fst.im 0) :
continuous_at (λ (x : × ), x.fst ^ x.snd) p

The function `z ^ w` is continuous in `(z, w)` provided that `z` does not belong to the interval `(-∞, 0]` on the real line. See also `complex.continuous_at_cpow_zero_of_re_pos` for a version that works for `z = 0` but assumes `0 < re w`.

theorem continuous_at_cpow_const {a b : } (ha : 0 < a.re a.im 0) :
continuous_at (λ (x : ), x.cpow b) a
theorem filter.tendsto.cpow {α : Type u_1} {l : filter α} {f g : α } {a b : } (hf : (nhds a)) (hg : (nhds b)) (ha : 0 < a.re a.im 0) :
filter.tendsto (λ (x : α), f x ^ g x) l (nhds (a ^ b))
theorem filter.tendsto.const_cpow {α : Type u_1} {l : filter α} {f : α } {a b : } (hf : (nhds b)) (h : a 0 b 0) :
filter.tendsto (λ (x : α), a ^ f x) l (nhds (a ^ b))
theorem continuous_within_at.cpow {α : Type u_1} {f g : α } {s : set α} {a : α} (hf : a) (hg : a) (h0 : 0 < (f a).re (f a).im 0) :
continuous_within_at (λ (x : α), f x ^ g x) s a
theorem continuous_within_at.const_cpow {α : Type u_1} {f : α } {s : set α} {a : α} {b : } (hf : a) (h : b 0 f a 0) :
continuous_within_at (λ (x : α), b ^ f x) s a
theorem continuous_at.cpow {α : Type u_1} {f g : α } {a : α} (hf : a) (hg : a) (h0 : 0 < (f a).re (f a).im 0) :
continuous_at (λ (x : α), f x ^ g x) a
theorem continuous_at.const_cpow {α : Type u_1} {f : α } {a : α} {b : } (hf : a) (h : b 0 f a 0) :
continuous_at (λ (x : α), b ^ f x) a
theorem continuous_on.cpow {α : Type u_1} {f g : α } {s : set α} (hf : s) (hg : s) (h0 : (a : α), a s 0 < (f a).re (f a).im 0) :
continuous_on (λ (x : α), f x ^ g x) s
theorem continuous_on.const_cpow {α : Type u_1} {f : α } {s : set α} {b : } (hf : s) (h : b 0 (a : α), a s f a 0) :
continuous_on (λ (x : α), b ^ f x) s
theorem continuous.cpow {α : Type u_1} {f g : α } (hf : continuous f) (hg : continuous g) (h0 : (a : α), 0 < (f a).re (f a).im 0) :
continuous (λ (x : α), f x ^ g x)
theorem continuous.const_cpow {α : Type u_1} {f : α } {b : } (hf : continuous f) (h : b 0 (a : α), f a 0) :
continuous (λ (x : α), b ^ f x)
theorem continuous_on.cpow_const {α : Type u_1} {f : α } {s : set α} {b : } (hf : s) (h : (a : α), a s 0 < (f a).re (f a).im 0) :
continuous_on (λ (x : α), f x ^ b) s
noncomputable def real.rpow (x y : ) :

The real power function `x^y`, defined as the real part of the complex power function. For `x > 0`, it is equal to `exp(y log x)`. For `x = 0`, one sets `0^0=1` and `0^y=0` for `y ≠ 0`. For `x < 0`, the definition is somewhat arbitary as it depends on the choice of a complex determination of the logarithm. With our conventions, it is equal to `exp (y log x) cos (πy)`.

Equations
@[protected, instance]
noncomputable def real.has_pow  :
Equations
@[simp]
theorem real.rpow_eq_pow (x y : ) :
x.rpow y = x ^ y
theorem real.rpow_def (x y : ) :
x ^ y = (x ^ y).re
theorem real.rpow_def_of_nonneg {x : } (hx : 0 x) (y : ) :
x ^ y = ite (x = 0) (ite (y = 0) 1 0) (rexp (real.log x * y))
theorem real.rpow_def_of_pos {x : } (hx : 0 < x) (y : ) :
x ^ y = rexp (real.log x * y)
theorem real.exp_mul (x y : ) :
rexp (x * y) = rexp x ^ y
@[simp]
theorem real.exp_one_rpow (x : ) :
rexp 1 ^ x = rexp x
theorem real.rpow_eq_zero_iff_of_nonneg {x y : } (hx : 0 x) :
x ^ y = 0 x = 0 y 0
theorem real.rpow_def_of_neg {x : } (hx : x < 0) (y : ) :
x ^ y = rexp (real.log x * y) * real.cos (y * real.pi)
theorem real.rpow_def_of_nonpos {x : } (hx : x 0) (y : ) :
x ^ y = ite (x = 0) (ite (y = 0) 1 0) (rexp (real.log x * y) * real.cos (y * real.pi))
theorem real.rpow_pos_of_pos {x : } (hx : 0 < x) (y : ) :
0 < x ^ y
@[simp]
theorem real.rpow_zero (x : ) :
x ^ 0 = 1
@[simp]
theorem real.zero_rpow {x : } (h : x 0) :
0 ^ x = 0
theorem real.zero_rpow_eq_iff {x a : } :
0 ^ x = a x 0 a = 0 x = 0 a = 1
theorem real.eq_zero_rpow_iff {x a : } :
a = 0 ^ x x 0 a = 0 x = 0 a = 1
@[simp]
theorem real.rpow_one (x : ) :
x ^ 1 = x
@[simp]
theorem real.one_rpow (x : ) :
1 ^ x = 1
theorem real.zero_rpow_le_one (x : ) :
0 ^ x 1
theorem real.zero_rpow_nonneg (x : ) :
0 0 ^ x
theorem real.rpow_nonneg_of_nonneg {x : } (hx : 0 x) (y : ) :
0 x ^ y
theorem real.abs_rpow_of_nonneg {x y : } (hx_nonneg : 0 x) :
|x ^ y| = |x| ^ y
theorem real.abs_rpow_le_abs_rpow (x y : ) :
|x ^ y| |x| ^ y
theorem real.abs_rpow_le_exp_log_mul (x y : ) :
|x ^ y| rexp (real.log x * y)
theorem real.norm_rpow_of_nonneg {x y : } (hx_nonneg : 0 x) :
x ^ y = x ^ y
theorem complex.of_real_cpow {x : } (hx : 0 x) (y : ) :
(x ^ y) = x ^ y
theorem complex.of_real_cpow_of_nonpos {x : } (hx : x 0) (y : ) :
x ^ y = (-x) ^ y * cexp * y)
theorem complex.abs_cpow_of_ne_zero {z : } (hz : z 0) (w : ) :
complex.abs (z ^ w) = ^ w.re / rexp (z.arg * w.im)
theorem complex.abs_cpow_of_imp {z w : } (h : z = 0 w.re = 0 w = 0) :
complex.abs (z ^ w) = ^ w.re / rexp (z.arg * w.im)
theorem complex.abs_cpow_le (z w : ) :
complex.abs (z ^ w) ^ w.re / rexp (z.arg * w.im)
theorem complex.is_Theta_exp_arg_mul_im {α : Type u_1} {l : filter α} {f g : α } (hl : (λ (x : α), |(g x).im|)) :
(λ (x : α), rexp ((f x).arg * (g x).im)) =Θ[l] λ (x : α), 1
theorem complex.is_O_cpow_rpow {α : Type u_1} {l : filter α} {f g : α } (hl : (λ (x : α), |(g x).im|)) :
(λ (x : α), f x ^ g x) =O[l] λ (x : α), complex.abs (f x) ^ (g x).re
theorem complex.is_Theta_cpow_rpow {α : Type u_1} {l : filter α} {f g : α } (hl_im : (λ (x : α), |(g x).im|)) (hl : ∀ᶠ (x : α) in l, f x = 0 (g x).re = 0 g x = 0) :
(λ (x : α), f x ^ g x) =Θ[l] λ (x : α), complex.abs (f x) ^ (g x).re
theorem complex.is_Theta_cpow_const_rpow {α : Type u_1} {l : filter α} {f : α } {b : } (hl : b.re = 0 b 0 (∀ᶠ (x : α) in l, f x 0)) :
(λ (x : α), f x ^ b) =Θ[l] λ (x : α), complex.abs (f x) ^ b.re
@[simp]
theorem complex.abs_cpow_real (x : ) (y : ) :
@[simp]
theorem complex.abs_cpow_inv_nat (x : ) (n : ) :
theorem complex.abs_cpow_eq_rpow_re_of_pos {x : } (hx : 0 < x) (y : ) :
theorem complex.abs_cpow_eq_rpow_re_of_nonneg {x : } (hx : 0 x) {y : } (hy : y.re 0) :
theorem complex.inv_cpow_eq_ite (x n : ) :
x⁻¹ ^ n = ite (x.arg = real.pi) ( (x ^ n)⁻¹) (x ^ n)⁻¹
theorem complex.inv_cpow (x n : ) (hx : x.arg real.pi) :
x⁻¹ ^ n = (x ^ n)⁻¹
theorem complex.inv_cpow_eq_ite' (x n : ) :
(x ^ n)⁻¹ = ite (x.arg = real.pi) ( (x⁻¹ ^ n)) (x⁻¹ ^ n)

`complex.inv_cpow_eq_ite` with the `ite` on the other side.

theorem complex.conj_cpow_eq_ite (x n : ) :
x ^ n = ite (x.arg = real.pi) (x ^ n) ( (x ^ n))
theorem complex.conj_cpow (x n : ) (hx : x.arg real.pi) :
x ^ n = (x ^ n)
theorem complex.cpow_conj (x n : ) (hx : x.arg real.pi) :
x ^ n = ( x ^ n)
theorem real.rpow_add {x : } (hx : 0 < x) (y z : ) :
x ^ (y + z) = x ^ y * x ^ z
theorem real.rpow_add' {x y z : } (hx : 0 x) (h : y + z 0) :
x ^ (y + z) = x ^ y * x ^ z
theorem real.rpow_add_of_nonneg {x y z : } (hx : 0 x) (hy : 0 y) (hz : 0 z) :
x ^ (y + z) = x ^ y * x ^ z
theorem real.le_rpow_add {x : } (hx : 0 x) (y z : ) :
x ^ y * x ^ z x ^ (y + z)

For `0 ≤ x`, the only problematic case in the equality `x ^ y * x ^ z = x ^ (y + z)` is for `x = 0` and `y + z = 0`, where the right hand side is `1` while the left hand side can vanish. The inequality is always true, though, and given in this lemma.

theorem real.rpow_sum_of_pos {ι : Type u_1} {a : } (ha : 0 < a) (f : ι ) (s : finset ι) :
a ^ s.sum (λ (x : ι), f x) = s.prod (λ (x : ι), a ^ f x)
theorem real.rpow_sum_of_nonneg {ι : Type u_1} {a : } (ha : 0 a) {s : finset ι} {f : ι } (h : (x : ι), x s 0 f x) :
a ^ s.sum (λ (x : ι), f x) = s.prod (λ (x : ι), a ^ f x)
theorem real.rpow_mul {x : } (hx : 0 x) (y z : ) :
x ^ (y * z) = (x ^ y) ^ z
theorem real.rpow_neg {x : } (hx : 0 x) (y : ) :
x ^ -y = (x ^ y)⁻¹
theorem real.rpow_sub {x : } (hx : 0 < x) (y z : ) :
x ^ (y - z) = x ^ y / x ^ z
theorem real.rpow_sub' {x : } (hx : 0 x) {y z : } (h : y - z 0) :
x ^ (y - z) = x ^ y / x ^ z
theorem real.rpow_add_int {x : } (hx : x 0) (y : ) (n : ) :
x ^ (y + n) = x ^ y * x ^ n
theorem real.rpow_add_nat {x : } (hx : x 0) (y : ) (n : ) :
x ^ (y + n) = x ^ y * x ^ n
theorem real.rpow_sub_int {x : } (hx : x 0) (y : ) (n : ) :
x ^ (y - n) = x ^ y / x ^ n
theorem real.rpow_sub_nat {x : } (hx : x 0) (y : ) (n : ) :
x ^ (y - n) = x ^ y / x ^ n
theorem real.rpow_add_one {x : } (hx : x 0) (y : ) :
x ^ (y + 1) = x ^ y * x
theorem real.rpow_sub_one {x : } (hx : x 0) (y : ) :
x ^ (y - 1) = x ^ y / x
@[simp, norm_cast]
theorem real.rpow_int_cast (x : ) (n : ) :
x ^ n = x ^ n
@[simp, norm_cast]
theorem real.rpow_nat_cast (x : ) (n : ) :
x ^ n = x ^ n
@[simp]
theorem real.rpow_two (x : ) :
x ^ 2 = x ^ 2
theorem real.rpow_neg_one (x : ) :
x ^ -1 = x⁻¹
theorem real.mul_rpow {x y z : } (h : 0 x) (h₁ : 0 y) :
(x * y) ^ z = x ^ z * y ^ z
theorem real.inv_rpow {x : } (hx : 0 x) (y : ) :
x⁻¹ ^ y = (x ^ y)⁻¹
theorem real.div_rpow {x y : } (hx : 0 x) (hy : 0 y) (z : ) :
(x / y) ^ z = x ^ z / y ^ z
theorem real.log_rpow {x : } (hx : 0 < x) (y : ) :
real.log (x ^ y) = y *
theorem real.rpow_lt_rpow {x y z : } (hx : 0 x) (hxy : x < y) (hz : 0 < z) :
x ^ z < y ^ z
theorem real.rpow_le_rpow {x y z : } (h : 0 x) (h₁ : x y) (h₂ : 0 z) :
x ^ z y ^ z
theorem real.rpow_lt_rpow_iff {x y z : } (hx : 0 x) (hy : 0 y) (hz : 0 < z) :
x ^ z < y ^ z x < y
theorem real.rpow_le_rpow_iff {x y z : } (hx : 0 x) (hy : 0 y) (hz : 0 < z) :
x ^ z y ^ z x y
theorem real.le_rpow_inv_iff_of_neg {x y z : } (hx : 0 < x) (hy : 0 < y) (hz : z < 0) :
x y ^ z⁻¹ y x ^ z
theorem real.lt_rpow_inv_iff_of_neg {x y z : } (hx : 0 < x) (hy : 0 < y) (hz : z < 0) :
x < y ^ z⁻¹ y < x ^ z
theorem real.rpow_inv_lt_iff_of_neg {x y z : } (hx : 0 < x) (hy : 0 < y) (hz : z < 0) :
x ^ z⁻¹ < y y ^ z < x
theorem real.rpow_inv_le_iff_of_neg {x y z : } (hx : 0 < x) (hy : 0 < y) (hz : z < 0) :
x ^ z⁻¹ y y ^ z x
theorem real.rpow_lt_rpow_of_exponent_lt {x y z : } (hx : 1 < x) (hyz : y < z) :
x ^ y < x ^ z
theorem real.rpow_le_rpow_of_exponent_le {x y z : } (hx : 1 x) (hyz : y z) :
x ^ y x ^ z
@[simp]
theorem real.rpow_le_rpow_left_iff {x y z : } (hx : 1 < x) :
x ^ y x ^ z y z
@[simp]
theorem real.rpow_lt_rpow_left_iff {x y z : } (hx : 1 < x) :
x ^ y < x ^ z y < z
theorem real.rpow_lt_rpow_of_exponent_gt {x y z : } (hx0 : 0 < x) (hx1 : x < 1) (hyz : z < y) :
x ^ y < x ^ z
theorem real.rpow_le_rpow_of_exponent_ge {x y z : } (hx0 : 0 < x) (hx1 : x 1) (hyz : z y) :
x ^ y x ^ z
@[simp]
theorem real.rpow_le_rpow_left_iff_of_base_lt_one {x y z : } (hx0 : 0 < x) (hx1 : x < 1) :
x ^ y x ^ z z y
@[simp]
theorem real.rpow_lt_rpow_left_iff_of_base_lt_one {x y z : } (hx0 : 0 < x) (hx1 : x < 1) :
x ^ y < x ^ z z < y
theorem real.rpow_lt_one {x z : } (hx1 : 0 x) (hx2 : x < 1) (hz : 0 < z) :
x ^ z < 1
theorem real.rpow_le_one {x z : } (hx1 : 0 x) (hx2 : x 1) (hz : 0 z) :
x ^ z 1
theorem real.rpow_lt_one_of_one_lt_of_neg {x z : } (hx : 1 < x) (hz : z < 0) :
x ^ z < 1
theorem real.rpow_le_one_of_one_le_of_nonpos {x z : } (hx : 1 x) (hz : z 0) :
x ^ z 1
theorem real.one_lt_rpow {x z : } (hx : 1 < x) (hz : 0 < z) :
1 < x ^ z
theorem real.one_le_rpow {x z : } (hx : 1 x) (hz : 0 z) :
1 x ^ z
theorem real.one_lt_rpow_of_pos_of_lt_one_of_neg {x z : } (hx1 : 0 < x) (hx2 : x < 1) (hz : z < 0) :
1 < x ^ z
theorem real.one_le_rpow_of_pos_of_le_one_of_nonpos {x z : } (hx1 : 0 < x) (hx2 : x 1) (hz : z 0) :
1 x ^ z
theorem real.rpow_lt_one_iff_of_pos {x y : } (hx : 0 < x) :
x ^ y < 1 1 < x y < 0 x < 1 0 < y
theorem real.rpow_lt_one_iff {x y : } (hx : 0 x) :
x ^ y < 1 x = 0 y 0 1 < x y < 0 x < 1 0 < y
theorem real.one_lt_rpow_iff_of_pos {x y : } (hx : 0 < x) :
1 < x ^ y 1 < x 0 < y x < 1 y < 0
theorem real.one_lt_rpow_iff {x y : } (hx : 0 x) :
1 < x ^ y 1 < x 0 < y 0 < x x < 1 y < 0
theorem real.rpow_le_rpow_of_exponent_ge' {x y z : } (hx0 : 0 x) (hx1 : x 1) (hz : 0 z) (hyz : z y) :
x ^ y x ^ z
theorem real.rpow_left_inj_on {x : } (hx : x 0) :
set.inj_on (λ (y : ), y ^ x) {y : | 0 y}
theorem real.le_rpow_iff_log_le {x y z : } (hx : 0 < x) (hy : 0 < y) :
x y ^ z z *
theorem real.le_rpow_of_log_le {x y z : } (hx : 0 x) (hy : 0 < y) (h : z * ) :
x y ^ z
theorem real.lt_rpow_iff_log_lt {x y z : } (hx : 0 < x) (hy : 0 < y) :
x < y ^ z < z *
theorem real.lt_rpow_of_log_lt {x y z : } (hx : 0 x) (hy : 0 < y) (h : < z * ) :
x < y ^ z
theorem real.rpow_le_one_iff_of_pos {x y : } (hx : 0 < x) :
x ^ y 1 1 x y 0 x 1 0 y
theorem real.abs_log_mul_self_rpow_lt (x t : ) (h1 : 0 < x) (h2 : x 1) (ht : 0 < t) :
| * x ^ t| < 1 / t

Bound for `|log x * x ^ t|` in the interval `(0, 1]`, for positive real `t`.

theorem real.pow_nat_rpow_nat_inv {x : } (hx : 0 x) {n : } (hn : n 0) :
(x ^ n) ^ (n)⁻¹ = x
theorem real.rpow_nat_inv_pow_nat {x : } (hx : 0 x) {n : } (hn : n 0) :
(x ^ (n)⁻¹) ^ n = x
theorem real.continuous_at_const_rpow {a b : } (h : a 0) :
theorem real.continuous_at_const_rpow' {a b : } (h : b 0) :
theorem real.rpow_eq_nhds_of_neg {p : × } (hp_fst : p.fst < 0) :
(λ (x : × ), x.fst ^ x.snd) =ᶠ[nhds p] λ (x : × ), rexp (real.log x.fst * x.snd) * real.cos (x.snd * real.pi)
theorem real.rpow_eq_nhds_of_pos {p : × } (hp_fst : 0 < p.fst) :
(λ (x : × ), x.fst ^ x.snd) =ᶠ[nhds p] λ (x : × ), rexp (real.log x.fst * x.snd)
theorem real.continuous_at_rpow_of_ne (p : × ) (hp : p.fst 0) :
continuous_at (λ (p : × ), p.fst ^ p.snd) p
theorem real.continuous_at_rpow_of_pos (p : × ) (hp : 0 < p.snd) :
continuous_at (λ (p : × ), p.fst ^ p.snd) p
theorem real.continuous_at_rpow (p : × ) (h : p.fst 0 0 < p.snd) :
continuous_at (λ (p : × ), p.fst ^ p.snd) p
theorem real.continuous_at_rpow_const (x q : ) (h : x 0 0 < q) :
continuous_at (λ (x : ), x ^ q) x
theorem filter.tendsto.rpow {α : Type u_1} {l : filter α} {f g : α } {x y : } (hf : (nhds x)) (hg : (nhds y)) (h : x 0 0 < y) :
filter.tendsto (λ (t : α), f t ^ g t) l (nhds (x ^ y))
theorem filter.tendsto.rpow_const {α : Type u_1} {l : filter α} {f : α } {x p : } (hf : (nhds x)) (h : x 0 0 p) :
filter.tendsto (λ (a : α), f a ^ p) l (nhds (x ^ p))
theorem continuous_at.rpow {α : Type u_1} {f g : α } {x : α} (hf : x) (hg : x) (h : f x 0 0 < g x) :
continuous_at (λ (t : α), f t ^ g t) x
theorem continuous_within_at.rpow {α : Type u_1} {f g : α } {s : set α} {x : α} (hf : x) (hg : x) (h : f x 0 0 < g x) :
continuous_within_at (λ (t : α), f t ^ g t) s x
theorem continuous_on.rpow {α : Type u_1} {f g : α } {s : set α} (hf : s) (hg : s) (h : (x : α), x s f x 0 0 < g x) :
continuous_on (λ (t : α), f t ^ g t) s
theorem continuous.rpow {α : Type u_1} {f g : α } (hf : continuous f) (hg : continuous g) (h : (x : α), f x 0 0 < g x) :
continuous (λ (x : α), f x ^ g x)
theorem continuous_within_at.rpow_const {α : Type u_1} {f : α } {s : set α} {x : α} {p : } (hf : x) (h : f x 0 0 p) :
continuous_within_at (λ (x : α), f x ^ p) s x
theorem continuous_at.rpow_const {α : Type u_1} {f : α } {x : α} {p : } (hf : x) (h : f x 0 0 p) :
continuous_at (λ (x : α), f x ^ p) x
theorem continuous_on.rpow_const {α : Type u_1} {f : α } {s : set α} {p : } (hf : s) (h : (x : α), x s f x 0 0 p) :
continuous_on (λ (x : α), f x ^ p) s
theorem continuous.rpow_const {α : Type u_1} {f : α } {p : } (hf : continuous f) (h : (x : α), f x 0 0 p) :
continuous (λ (x : α), f x ^ p)
theorem real.sqrt_eq_rpow (x : ) :
x = x ^ (1 / 2)
theorem real.rpow_div_two_eq_sqrt {x : } (r : ) (hx : 0 x) :
x ^ (r / 2) = x ^ r
theorem tendsto_rpow_at_top {y : } (hy : 0 < y) :

The function `x ^ y` tends to `+∞` at `+∞` for any positive real `y`.

theorem tendsto_rpow_neg_at_top {y : } (hy : 0 < y) :
filter.tendsto (λ (x : ), x ^ -y) filter.at_top (nhds 0)

The function `x ^ (-y)` tends to `0` at `+∞` for any positive real `y`.

theorem tendsto_rpow_div_mul_add (a b c : ) (hb : 0 b) :
filter.tendsto (λ (x : ), x ^ (a / (b * x + c))) filter.at_top (nhds 1)

The function `x ^ (a / (b * x + c))` tends to `1` at `+∞`, for any real numbers `a`, `b`, and `c` such that `b` is nonzero.

theorem tendsto_rpow_div  :
filter.tendsto (λ (x : ), x ^ (1 / x)) filter.at_top (nhds 1)

The function `x ^ (1 / x)` tends to `1` at `+∞`.

theorem tendsto_rpow_neg_div  :
filter.tendsto (λ (x : ), x ^ ((-1) / x)) filter.at_top (nhds 1)

The function `x ^ (-1 / x)` tends to `1` at `+∞`.

The function `exp(x) / x ^ s` tends to `+∞` at `+∞`, for any real number `s`.

theorem tendsto_exp_mul_div_rpow_at_top (s b : ) (hb : 0 < b) :

The function `exp (b * x) / x ^ s` tends to `+∞` at `+∞`, for any real `s` and `b > 0`.

theorem tendsto_rpow_mul_exp_neg_mul_at_top_nhds_0 (s b : ) (hb : 0 < b) :
filter.tendsto (λ (x : ), x ^ s * rexp (-b * x)) filter.at_top (nhds 0)

The function `x ^ s * exp (-b * x)` tends to `0` at `+∞`, for any real `s` and `b > 0`.

theorem asymptotics.is_O_with.rpow {α : Type u_1} {r c : } {l : filter α} {f g : α } (h : g) (hc : 0 c) (hr : 0 r) (hg : 0 ≤ᶠ[l] g) :
asymptotics.is_O_with (c ^ r) l (λ (x : α), f x ^ r) (λ (x : α), g x ^ r)
theorem asymptotics.is_O.rpow {α : Type u_1} {r : } {l : filter α} {f g : α } (hr : 0 r) (hg : 0 ≤ᶠ[l] g) (h : f =O[l] g) :
(λ (x : α), f x ^ r) =O[l] λ (x : α), g x ^ r
theorem asymptotics.is_o.rpow {α : Type u_1} {r : } {l : filter α} {f g : α } (hr : 0 < r) (hg : 0 ≤ᶠ[l] g) (h : f =o[l] g) :
(λ (x : α), f x ^ r) =o[l] λ (x : α), g x ^ r
theorem is_o_rpow_exp_pos_mul_at_top (s : ) {b : } (hb : 0 < b) :
(λ (x : ), x ^ s) =o[filter.at_top] λ (x : ), rexp (b * x)

`x ^ s = o(exp(b * x))` as `x → ∞` for any real `s` and positive `b`.

theorem is_o_zpow_exp_pos_mul_at_top (k : ) {b : } (hb : 0 < b) :
(λ (x : ), x ^ k) =o[filter.at_top] λ (x : ), rexp (b * x)

`x ^ k = o(exp(b * x))` as `x → ∞` for any integer `k` and positive `b`.

theorem is_o_pow_exp_pos_mul_at_top (k : ) {b : } (hb : 0 < b) :
(λ (x : ), x ^ k) =o[filter.at_top] λ (x : ), rexp (b * x)

`x ^ k = o(exp(b * x))` as `x → ∞` for any natural `k` and positive `b`.

theorem is_o_rpow_exp_at_top (s : ) :
(λ (x : ), x ^ s) =o[filter.at_top] rexp

`x ^ s = o(exp x)` as `x → ∞` for any real `s`.

theorem is_o_log_rpow_at_top {r : } (hr : 0 < r) :
theorem is_o_log_rpow_rpow_at_top {s : } (r : ) (hs : 0 < s) :
(λ (x : ), ^ r) =o[filter.at_top] λ (x : ), x ^ s
theorem is_o_abs_log_rpow_rpow_nhds_zero {s : } (r : ) (hs : s < 0) :
(λ (x : ), ^ r) =o[ (set.Ioi 0)] λ (x : ), x ^ s
theorem is_o_log_rpow_nhds_zero {r : } (hr : r < 0) :
real.log =o[ (set.Ioi 0)] λ (x : ), x ^ r
theorem tendsto_log_div_rpow_nhds_zero {r : } (hr : r < 0) :
filter.tendsto (λ (x : ), / x ^ r) (set.Ioi 0)) (nhds 0)
theorem tendsto_log_mul_rpow_nhds_zero {r : } (hr : 0 < r) :
filter.tendsto (λ (x : ), * x ^ r) (set.Ioi 0)) (nhds 0)
theorem complex.continuous_at_cpow_zero_of_re_pos {z : } (hz : 0 < z.re) :
continuous_at (λ (x : × ), x.fst ^ x.snd) (0, z)

See also `continuous_at_cpow` and `complex.continuous_at_cpow_of_re_pos`.

theorem complex.continuous_at_cpow_of_re_pos {p : × } (h₁ : 0 p.fst.re p.fst.im 0) (h₂ : 0 < p.snd.re) :
continuous_at (λ (x : × ), x.fst ^ x.snd) p

See also `continuous_at_cpow` for a version that assumes `p.1 ≠ 0` but makes no assumptions about `p.2`.

theorem complex.continuous_at_cpow_const_of_re_pos {z w : } (hz : 0 z.re z.im 0) (hw : 0 < w.re) :
continuous_at (λ (x : ), x ^ w) z

See also `continuous_at_cpow_const` for a version that assumes `z ≠ 0` but makes no assumptions about `w`.

theorem complex.continuous_at_of_real_cpow (x : ) (y : ) (h : 0 < y.re x 0) :
continuous_at (λ (p : × ), (p.fst) ^ p.snd) (x, y)

Continuity of `(x, y) ↦ x ^ y` as a function on `ℝ × ℂ`.

theorem complex.continuous_at_of_real_cpow_const (x : ) (y : ) (h : 0 < y.re x 0) :
continuous_at (λ (a : ), a ^ y) x
theorem complex.continuous_of_real_cpow_const {y : } (hs : 0 < y.re) :
continuous (λ (x : ), x ^ y)
noncomputable def nnreal.rpow (x : nnreal) (y : ) :

The nonnegative real power function `x^y`, defined for `x : ℝ≥0` and `y : ℝ` as the restriction of the real power function. For `x > 0`, it is equal to `exp (y log x)`. For `x = 0`, one sets `0 ^ 0 = 1` and `0 ^ y = 0` for `y ≠ 0`.

Equations
@[protected, instance]
noncomputable def nnreal.real.has_pow  :
Equations
@[simp]
theorem nnreal.rpow_eq_pow (x : nnreal) (y : ) :
x.rpow y = x ^ y
@[simp, norm_cast]
theorem nnreal.coe_rpow (x : nnreal) (y : ) :
(x ^ y) = x ^ y
@[simp]
theorem nnreal.rpow_zero (x : nnreal) :
x ^ 0 = 1
@[simp]
theorem nnreal.rpow_eq_zero_iff {x : nnreal} {y : } :
x ^ y = 0 x = 0 y 0
@[simp]
theorem nnreal.zero_rpow {x : } (h : x 0) :
0 ^ x = 0
@[simp]
theorem nnreal.rpow_one (x : nnreal) :
x ^ 1 = x
@[simp]
theorem nnreal.one_rpow (x : ) :
1 ^ x = 1
theorem nnreal.rpow_add {x : nnreal} (hx : x 0) (y z : ) :
x ^ (y + z) = x ^ y * x ^ z
theorem nnreal.rpow_add' (x : nnreal) {y z : } (h : y + z 0) :
x ^ (y + z) = x ^ y * x ^ z
theorem nnreal.rpow_mul (x : nnreal) (y z : ) :
x ^ (y * z) = (x ^ y) ^ z
theorem nnreal.rpow_neg (x : nnreal) (y : ) :
x ^ -y = (x ^ y)⁻¹
theorem nnreal.rpow_neg_one (x : nnreal) :
x ^ -1 = x⁻¹
theorem nnreal.rpow_sub {x : nnreal} (hx : x 0) (y z : ) :
x ^ (y - z) = x ^ y / x ^ z
theorem nnreal.rpow_sub' (x : nnreal) {y z : } (h : y - z 0) :
x ^ (y - z) = x ^ y / x ^ z
theorem nnreal.rpow_inv_rpow_self {y : } (hy : y 0) (x : nnreal) :
(x ^ y) ^ (1 / y) = x
theorem nnreal.rpow_self_rpow_inv {y : } (hy : y 0) (x : nnreal) :
(x ^ (1 / y)) ^ y = x
theorem nnreal.inv_rpow (x : nnreal) (y : ) :
x⁻¹ ^ y = (x ^ y)⁻¹
theorem nnreal.div_rpow (x y : nnreal) (z : ) :
(x / y) ^ z = x ^ z / y ^ z
theorem nnreal.sqrt_eq_rpow (x : nnreal) :
= x ^ (1 / 2)
@[simp, norm_cast]
theorem nnreal.rpow_nat_cast (x : nnreal) (n : ) :
x ^ n = x ^ n
@[simp]
theorem nnreal.rpow_two (x : nnreal) :
x ^ 2 = x ^ 2
theorem nnreal.mul_rpow {x y : nnreal} {z : } :
(x * y) ^ z = x ^ z * y ^ z
theorem nnreal.rpow_le_rpow {x y : nnreal} {z : } (h₁ : x y) (h₂ : 0 z) :
x ^ z y ^ z
theorem nnreal.rpow_lt_rpow {x y : nnreal} {z : } (h₁ : x < y) (h₂ : 0 < z) :
x ^ z < y ^ z
theorem nnreal.rpow_lt_rpow_iff {x y : nnreal} {z : } (hz : 0 < z) :
x ^ z < y ^ z x < y
theorem nnreal.rpow_le_rpow_iff {x y : nnreal} {z : } (hz : 0 < z) :
x ^ z y ^ z x y
theorem nnreal.le_rpow_one_div_iff {x y : nnreal} {z : } (hz : 0 < z) :
x y ^ (1 / z) x ^ z y
theorem nnreal.rpow_one_div_le_iff {x y : nnreal} {z : } (hz : 0 < z) :
x ^ (1 / z) y x y ^ z
theorem nnreal.rpow_lt_rpow_of_exponent_lt {x : nnreal} {y z : } (hx : 1 < x) (hyz : y < z) :
x ^ y < x ^ z
theorem nnreal.rpow_le_rpow_of_exponent_le {x : nnreal} {y z : } (hx : 1 x) (hyz : y z) :
x ^ y x ^ z
theorem nnreal.rpow_lt_rpow_of_exponent_gt {x : nnreal} {y z : } (hx0 : 0 < x) (hx1 : x < 1) (hyz : z < y) :
x ^ y < x ^ z
theorem nnreal.rpow_le_rpow_of_exponent_ge {x : nnreal} {y z : } (hx0 : 0 < x) (hx1 : x 1) (hyz : z y) :
x ^ y x ^ z
theorem nnreal.rpow_pos {p : } {x : nnreal} (hx_pos : 0 < x) :
0 < x ^ p
theorem nnreal.rpow_lt_one {x : nnreal} {z : } (hx1 : x < 1) (hz : 0 < z) :
x ^ z < 1
theorem nnreal.rpow_le_one {x : nnreal} {z : } (hx2 : x 1) (hz : 0 z) :
x ^ z 1
theorem nnreal.rpow_lt_one_of_one_lt_of_neg {x : nnreal} {z : } (hx : 1 < x) (hz : z < 0) :
x ^ z < 1
theorem nnreal.rpow_le_one_of_one_le_of_nonpos {x : nnreal} {z : } (hx : 1 x) (hz : z 0) :
x ^ z 1
theorem nnreal.one_lt_rpow {x : nnreal} {z : } (hx : 1 < x) (hz : 0 < z) :
1 < x ^ z
theorem nnreal.one_le_rpow {x : nnreal} {z : } (h : 1 x) (h₁ : 0 z) :
1 x ^ z
theorem nnreal.one_lt_rpow_of_pos_of_lt_one_of_neg {x : nnreal} {z : } (hx1 : 0 < x) (hx2 : x < 1) (hz : z < 0) :
1 < x ^ z
theorem nnreal.one_le_rpow_of_pos_of_le_one_of_nonpos {x : nnreal} {z : } (hx1 : 0 < x) (hx2 : x 1) (hz : z 0) :
1 x ^ z
theorem nnreal.rpow_le_self_of_le_one {x : nnreal} {z : } (hx : x 1) (h_one_le : 1 z) :
x ^ z x
theorem nnreal.rpow_left_injective {x : } (hx : x 0) :
function.injective (λ (y : nnreal), y ^ x)
theorem nnreal.rpow_eq_rpow_iff {x y : nnreal} {z : } (hz : z 0) :
x ^ z = y ^ z x = y
theorem nnreal.rpow_left_surjective {x : } (hx : x 0) :
function.surjective (λ (y : nnreal), y ^ x)
theorem nnreal.rpow_left_bijective {x : } (hx : x 0) :
function.bijective (λ (y : nnreal), y ^ x)
theorem nnreal.eq_rpow_one_div_iff {x y : nnreal} {z : } (hz : z 0) :
x = y ^ (1 / z) x ^ z = y
theorem nnreal.rpow_one_div_eq_iff {x y : nnreal} {z : } (hz : z 0) :
x ^ (1 / z) = y x = y ^ z
theorem nnreal.pow_nat_rpow_nat_inv (x : nnreal) {n : } (hn : n 0) :
(x ^ n) ^ (n)⁻¹ = x
theorem nnreal.rpow_nat_inv_pow_nat (x : nnreal) {n : } (hn : n 0) :
(x ^ (n)⁻¹) ^ n = x
theorem nnreal.continuous_at_rpow {x : nnreal} {y : } (h : x 0 0 < y) :
continuous_at (λ (p : , p.fst ^ p.snd) (x, y)
theorem real.to_nnreal_rpow_of_nonneg {x y : } (hx : 0 x) :
(x ^ y).to_nnreal = x.to_nnreal ^ y
theorem nnreal.eventually_pow_one_div_le (x : nnreal) {y : nnreal} (hy : 1 < y) :
∀ᶠ (n : ) in filter.at_top, x ^ (1 / n) y
theorem real.exists_rat_pow_btwn_rat_aux {n : } (hn : n 0) (x y : ) (h : x < y) (hy : 0 < y) :
(q : ), 0 < q x < q ^ n q ^ n < y
theorem real.exists_rat_pow_btwn_rat {n : } (hn : n 0) {x y : } (h : x < y) (hy : 0 < y) :
(q : ), 0 < q x < q ^ n q ^ n < y
theorem real.exists_rat_pow_btwn {n : } {α : Type u_1} [archimedean α] (hn : n 0) {x y : α} (h : x < y) (hy : 0 < y) :
(q : ), 0 < q x < q ^ n q ^ n < y

There is a rational power between any two positive elements of an archimedean ordered field.

theorem filter.tendsto.nnrpow {α : Type u_1} {f : filter α} {u : α nnreal} {v : α } {x : nnreal} {y : } (hx : (nhds x)) (hy : (nhds y)) (h : x 0 0 < y) :
filter.tendsto (λ (a : α), u a ^ v a) f (nhds (x ^ y))
theorem nnreal.continuous_at_rpow_const {x : nnreal} {y : } (h : x 0 0 y) :
continuous_at (λ (z : nnreal), z ^ y) x
theorem nnreal.continuous_rpow_const {y : } (h : 0 y) :
continuous (λ (x : nnreal), x ^ y)
noncomputable def ennreal.rpow  :

The real power function `x^y` on extended nonnegative reals, defined for `x : ℝ≥0∞` and `y : ℝ` as the restriction of the real power function if `0 < x < ⊤`, and with the natural values for `0` and `⊤` (i.e., `0 ^ x = 0` for `x > 0`, `1` for `x = 0` and `⊤` for `x < 0`, and `⊤ ^ x = 1 / 0 ^ x`).

Equations
@[protected, instance]
noncomputable def ennreal.real.has_pow  :
Equations
@[simp]
theorem ennreal.rpow_eq_pow (x : ennreal) (y : ) :
x.rpow y = x ^ y
@[simp]
theorem ennreal.rpow_zero {x : ennreal} :
x ^ 0 = 1
theorem ennreal.top_rpow_def (y : ) :
^ y = ite (0 < y) (ite (y = 0) 1 0)
@[simp]
theorem ennreal.top_rpow_of_pos {y : } (h : 0 < y) :
@[simp]
theorem ennreal.top_rpow_of_neg {y : } (h : y < 0) :
^ y = 0
@[simp]
theorem ennreal.zero_rpow_of_pos {y : } (h : 0 < y) :
0 ^ y = 0
@[simp]
theorem ennreal.zero_rpow_of_neg {y : } (h : y < 0) :
0 ^ y =
theorem ennreal.zero_rpow_def (y : ) :
0 ^ y = ite (0 < y) 0 (ite (y = 0) 1 )
@[simp]
theorem ennreal.zero_rpow_mul_self (y : ) :
0 ^ y * 0 ^ y = 0 ^ y
@[norm_cast]
theorem ennreal.coe_rpow_of_ne_zero {x : nnreal} (h : x 0) (y : ) :
x ^ y = (x ^ y)
@[norm_cast]
theorem ennreal.coe_rpow_of_nonneg (x : nnreal) {y : } (h : 0 y) :
x ^ y = (x ^ y)
theorem ennreal.coe_rpow_def (x : nnreal) (y : ) :
x ^ y = ite (x = 0 y < 0) (x ^ y)
@[simp]
theorem ennreal.rpow_one (x : ennreal) :
x ^ 1 = x
@[simp]
theorem ennreal.one_rpow (x : ) :
1 ^ x = 1
@[simp]
theorem ennreal.rpow_eq_zero_iff {x : ennreal} {y : } :
x ^ y = 0 x = 0 0 < y x = y < 0
@[simp]
theorem ennreal.rpow_eq_top_iff {x : ennreal} {y : } :
x ^ y = x = 0 y < 0 x = 0 < y
theorem ennreal.rpow_eq_top_iff_of_pos {x : ennreal} {y : } (hy : 0 < y) :
x ^ y = x =
theorem ennreal.rpow_eq_top_of_nonneg (x : ennreal) {y : } (hy0 : 0 y) :
x ^ y = x =
theorem ennreal.rpow_ne_top_of_nonneg {x : ennreal} {y : } (hy0 : 0 y) (h : x ) :
x ^ y
theorem ennreal.rpow_lt_top_of_nonneg {x : ennreal} {y : } (hy0 : 0 y) (h : x ) :
x ^ y <
theorem ennreal.rpow_add {x : ennreal} (y z : ) (hx : x 0) (h'x : x ) :
x ^ (y + z) = x ^ y * x ^ z
theorem ennreal.rpow_neg (x : ennreal) (y : ) :
x ^ -y = (x ^ y)⁻¹
theorem ennreal.rpow_sub {x : ennreal} (y z : ) (hx : x 0) (h'x : x ) :
x ^ (y - z) = x ^ y / x ^ z
theorem ennreal.rpow_neg_one (x : ennreal) :
x ^ -1 = x⁻¹
theorem ennreal.rpow_mul (x : ennreal) (y z : ) :
x ^ (y * z) = (x ^ y) ^ z
@[simp, norm_cast]
theorem ennreal.rpow_nat_cast (x : ennreal) (n : ) :
x ^ n = x ^ n
@[simp]
theorem ennreal.rpow_two (x : ennreal) :
x ^ 2 = x ^ 2
theorem ennreal.mul_rpow_eq_ite (x y : ennreal) (z : ) :
(x * y) ^ z = ite ((x = 0 y = x = y = 0) z < 0) (x ^ z * y ^ z)
theorem ennreal.mul_rpow_of_ne_top {x y : ennreal} (hx : x ) (hy : y ) (z : ) :
(x * y) ^ z = x ^ z * y ^ z
@[norm_cast]
theorem ennreal.coe_mul_rpow (x y : nnreal) (z : ) :
(x * y) ^ z = x ^ z * y ^ z
theorem ennreal.mul_rpow_of_ne_zero {x y : ennreal} (hx : x 0) (hy : y 0) (z : ) :
(x * y) ^ z = x ^ z * y ^ z
theorem ennreal.mul_rpow_of_nonneg (x y : ennreal) {z : } (hz : 0 z) :
(x * y) ^ z = x ^ z * y ^ z
theorem ennreal.inv_rpow (x : ennreal) (y : ) :
x⁻¹ ^ y = (x ^ y)⁻¹
theorem ennreal.div_rpow_of_nonneg (x y : ennreal) {z : } (hz : 0 z) :
(x / y) ^ z = x ^ z / y ^ z
theorem ennreal.strict_mono_rpow_of_pos {z : } (h : 0 < z) :
strict_mono (λ (x : ennreal), x ^ z)
theorem ennreal.monotone_rpow_of_nonneg {z : } (h : 0 z) :
monotone (λ (x : ennreal), x ^ z)
noncomputable def ennreal.order_iso_rpow (y : ) (hy : 0 < y) :

Bundles `λ x : ℝ≥0∞, x ^ y` into an order isomorphism when `y : ℝ` is positive, where the inverse is `λ x : ℝ≥0∞, x ^ (1 / y)`.

Equations
@[simp]
theorem ennreal.order_iso_rpow_apply (y : ) (hy : 0 < y) (x : ennreal) :
hy) x = x ^ y
theorem ennreal.order_iso_rpow_symm_apply (y : ) (hy : 0 < y) :
theorem ennreal.rpow_le_rpow {x y : ennreal} {z : } (h₁ : x y) (h₂ : 0 z) :
x ^ z y ^ z
theorem ennreal.rpow_lt_rpow {x y : ennreal} {z : } (h₁ : x < y) (h₂ : 0 < z) :
x ^ z < y ^ z
theorem ennreal.rpow_le_rpow_iff {x y : ennreal} {z : } (hz : 0 < z) :
x ^ z y ^ z x y
theorem ennreal.rpow_lt_rpow_iff {x y : ennreal} {z : } (hz : 0 < z) :
x ^ z < y ^ z x < y
theorem ennreal.le_rpow_one_div_iff {x y : ennreal} {z : } (hz : 0 < z) :
x y ^ (1 / z) x ^ z y
theorem ennreal.lt_rpow_one_div_iff {x y : ennreal} {z : } (hz : 0 < z) :
x < y ^ (1 / z) x ^ z < y
theorem ennreal.rpow_one_div_le_iff {x y : ennreal} {z : } (hz : 0 < z) :
x ^ (1 / z) y x y ^ z
theorem ennreal.rpow_lt_rpow_of_exponent_lt {x : ennreal} {y z : } (hx : 1 < x) (hx' : x ) (hyz : y < z) :
x ^ y < x ^ z
theorem ennreal.rpow_le_rpow_of_exponent_le {x : ennreal} {y z : } (hx : 1 x) (hyz : y z) :
x ^ y x ^ z
theorem ennreal.rpow_lt_rpow_of_exponent_gt {x : ennreal} {y z : } (hx0 : 0 < x) (hx1 : x < 1) (hyz : z < y) :
x ^ y < x ^ z
theorem ennreal.rpow_le_rpow_of_exponent_ge {x : ennreal} {y z : } (hx1 : x 1) (hyz : z y) :
x ^ y x ^ z
theorem ennreal.rpow_le_self_of_le_one {x : ennreal} {z : } (hx : x 1) (h_one_le : 1 z) :
x ^ z x
theorem ennreal.le_rpow_self_of_one_le {x : ennreal} {z : } (hx : 1 x) (h_one_le : 1 z) :
x x ^ z
theorem ennreal.rpow_pos_of_nonneg {p : } {x : ennreal} (hx_pos : 0 < x) (hp_nonneg : 0 p) :
0 < x ^ p
theorem ennreal.rpow_pos {p : } {x : ennreal} (hx_pos : 0 < x) (hx_ne_top : x ) :
0 < x ^ p
theorem ennreal.rpow_lt_one {x : ennreal} {z : } (hx : x < 1) (hz : 0 < z) :
x ^ z < 1
theorem ennreal.rpow_le_one {x : ennreal} {z : } (hx : x 1) (hz : 0 z) :
x ^ z 1
theorem ennreal.rpow_lt_one_of_one_lt_of_neg {x : ennreal} {z : } (hx : 1 < x) (hz : z < 0) :
x ^ z < 1
theorem ennreal.rpow_le_one_of_one_le_of_neg {x : ennreal} {z : } (hx : 1 x) (hz : z < 0) :
x ^ z 1
theorem ennreal.one_lt_rpow {x : ennreal} {z : } (hx : 1 < x) (hz : 0 < z) :
1 < x ^ z
theorem ennreal.one_le_rpow {x : ennreal} {z : } (hx : 1 x) (hz : 0 < z) :
1 x ^ z
theorem ennreal.one_lt_rpow_of_pos_of_lt_one_of_neg {x : ennreal} {z : } (hx1 : 0 < x) (hx2 : x < 1) (hz : z < 0) :
1 < x ^ z
theorem ennreal.one_le_rpow_of_pos_of_le_one_of_neg {x : ennreal} {z : } (hx1 : 0 < x) (hx2 : x 1) (hz : z < 0) :
1 x ^ z
theorem ennreal.to_nnreal_rpow (x : ennreal) (z : ) :
x.to_nnreal ^ z = (x ^ z).to_nnreal
theorem ennreal.to_real_rpow (x : ennreal) (z : ) :
x.to_real ^ z = (x ^ z).to_real
theorem ennreal.of_real_rpow_of_pos {x p : } (hx_pos : 0 < x) :
theorem ennreal.of_real_rpow_of_nonneg {x p : } (hx_nonneg : 0 x) (hp_nonneg : 0 p) :
theorem ennreal.rpow_left_injective {x : } (hx : x 0) :
function.injective (λ (y : ennreal), y ^ x)
theorem ennreal.rpow_left_surjective {x : } (hx : x 0) :
function.surjective (λ (y : ennreal), y ^ x)
theorem ennreal.rpow_left_bijective {x : } (hx : x 0) :
function.bijective (λ (y : ennreal), y ^ x)
theorem ennreal.tendsto_rpow_at_top {y : } (hy : 0 < y) :
filter.tendsto (λ (x : ennreal), x ^ y) (nhds ) (nhds )
theorem ennreal.eventually_pow_one_div_le {x : ennreal} (hx : x ) {y : ennreal} (hy : 1 < y) :
∀ᶠ (n : ) in filter.at_top, x ^ (1 / n) y
@[continuity]
theorem ennreal.continuous_rpow_const {y : } :
continuous (λ (a : ennreal), a ^ y)
theorem ennreal.tendsto_const_mul_rpow_nhds_zero_of_pos {c : ennreal} (hc : c ) {y : } (hy : 0 < y) :
filter.tendsto (λ (x : ennreal), c * x ^ y) (nhds 0) (nhds 0)
theorem filter.tendsto.ennrpow_const {α : Type u_1} {f : filter α} {m : α ennreal} {a : ennreal} (r : ) (hm : (nhds a)) :
filter.tendsto (λ (x : α), m x ^ r) f (nhds (a ^ r))
theorem norm_num.rpow_pos (a b : ) (b' : ) (c : ) (hb : b' = b) (h : a ^ b' = c) :
a ^ b = c
theorem norm_num.rpow_neg (a b : ) (b' : ) (c c' : ) (a0 : 0 a) (hb : b' = b) (h : a ^ b' = c) (hc : c⁻¹ = c') :
a ^ -b = c'
meta def norm_num.prove_rpow (a b : expr) :

Evaluate `real.rpow a b` where `a` is a rational numeral and `b` is an integer. (This cannot go via the generalized version `prove_rpow'` because `rpow_pos` has a side condition; we do not attempt to evaluate `a ^ b` where `a` and `b` are both negative because it comes out to some garbage.)

meta def norm_num.prove_rpow' (pos neg zero : name) (α β one a b : expr) :

Generalized version of `prove_cpow`, `prove_nnrpow`, `prove_ennrpow`.

theorem norm_num.cpow_pos (a b : ) (b' : ) (c : ) (hb : b = b') (h : a ^ b' = c) :
a ^ b = c
theorem norm_num.cpow_neg (a b : ) (b' : ) (c c' : ) (hb : b = b') (h : a ^ b' = c) (hc : c⁻¹ = c') :
a ^ -b = c'
theorem norm_num.nnrpow_pos (a : nnreal) (b : ) (b' : ) (c : nnreal) (hb : b = b') (h : a ^ b' = c) :
a ^ b = c
theorem norm_num.nnrpow_neg (a : nnreal) (b : ) (b' : ) (c c' : nnreal) (hb : b = b') (h : a ^ b' = c) (hc : c⁻¹ = c') :
a ^ -b = c'
theorem norm_num.ennrpow_pos (a : ennreal) (b : ) (b' : ) (c : ennreal) (hb : b = b') (h : a ^ b' = c) :
a ^ b = c
theorem norm_num.ennrpow_neg (a : ennreal) (b : ) (b' : ) (c c' : ennreal) (hb : b = b') (h : a ^ b' = c) (hc : c⁻¹ = c') :
a ^ -b = c'

Evaluate `complex.cpow a b` where `a` is a rational numeral and `b` is an integer.

Evaluate `nnreal.rpow a b` where `a` is a rational numeral and `b` is an integer.

Evaluate `ennreal.rpow a b` where `a` is a rational numeral and `b` is an integer.

Evaluates expressions of the form `rpow a b`, `cpow a b` and `a ^ b` in the special case where `b` is an integer and `a` is a positive rational (so it's really just a rational power).

meta def tactic.positivity.prove_rpow (a b : expr) :

Auxiliary definition for the `positivity` tactic to handle real powers of reals.

meta def tactic.positivity.prove_nnrpow (a b : expr) :

Auxiliary definition for the `positivity` tactic to handle real powers of nonnegative reals.

Auxiliary definition for the `positivity` tactic to handle real powers of extended nonnegative reals.

Extension for the `positivity` tactic: exponentiation by a real number is nonnegative when the base is nonnegative and positive when the base is positive.