mathlib documentation

analysis.special_functions.pow

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

We construct the power functions x ^ y where

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) (complex.exp (complex.log x * y))
theorem complex.cpow_def_of_ne_zero {x : } (hx : x 0) (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 < (complex.log x * y).im) (h₂ : (complex.log x * 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 zero_cpow_eq_nhds {b : } (hb : b 0) :
theorem cpow_eq_nhds {a b : } (ha : a 0) :
(λ (x : ), x.cpow b) =ᶠ[nhds a] λ (x : ), complex.exp (complex.log x * b)
theorem cpow_eq_nhds' {p : × } (hp_fst : p.fst 0) :
(λ (x : × ), x.fst ^ x.snd) =ᶠ[nhds p] λ (x : × ), complex.exp (complex.log x.fst * x.snd)
theorem continuous_at_const_cpow {a b : } (ha : a 0) :
theorem continuous_at_const_cpow' {a b : } (h : b 0) :
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 : filter.tendsto f l (nhds a)) (hg : filter.tendsto g l (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 : filter.tendsto f l (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} [topological_space α] {f g : α } {s : set α} {a : α} (hf : continuous_within_at f s a) (hg : continuous_within_at g s 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} [topological_space α] {f : α } {s : set α} {a : α} {b : } (hf : continuous_within_at f s a) (h : b 0 f a 0) :
continuous_within_at (λ (x : α), b ^ f x) s a
theorem continuous_at.cpow {α : Type u_1} [topological_space α] {f g : α } {a : α} (hf : continuous_at f a) (hg : continuous_at g 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} [topological_space α] {f : α } {a : α} {b : } (hf : continuous_at f a) (h : b 0 f a 0) :
continuous_at (λ (x : α), b ^ f x) a
theorem continuous_on.cpow {α : Type u_1} [topological_space α] {f g : α } {s : set α} (hf : continuous_on f s) (hg : continuous_on g 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} [topological_space α] {f : α } {s : set α} {b : } (hf : continuous_on f s) (h : b 0 (a : α), a s f a 0) :
continuous_on (λ (x : α), b ^ f x) s
theorem continuous.cpow {α : Type u_1} [topological_space α] {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} [topological_space α] {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} [topological_space α] {f : α } {s : set α} {b : } (hf : continuous_on f 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) (real.exp (real.log x * y))
theorem real.rpow_def_of_pos {x : } (hx : 0 < x) (y : ) :
x ^ y = real.exp (real.log x * y)
theorem real.exp_mul (x y : ) :
real.exp (x * y) = real.exp x ^ y
@[simp]
theorem real.exp_one_rpow (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 : ) :
theorem real.rpow_def_of_nonpos {x : } (hx : x 0) (y : ) :
x ^ y = ite (x = 0) (ite (y = 0) 1 0) (real.exp (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.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 : ) :
theorem complex.abs_cpow_of_ne_zero {z : } (hz : z 0) (w : ) :
theorem complex.abs_cpow_of_imp {z w : } (h : z = 0 w.re = 0 w = 0) :
theorem complex.is_Theta_exp_arg_mul_im {α : Type u_1} {l : filter α} {f g : α } (hl : filter.is_bounded_under has_le.le l (λ (x : α), |(g x).im|)) :
(λ (x : α), real.exp ((f x).arg * (g x).im)) =Θ[l] λ (x : α), 1
theorem complex.is_O_cpow_rpow {α : Type u_1} {l : filter α} {f g : α } (hl : filter.is_bounded_under has_le.le l (λ (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 : filter.is_bounded_under has_le.le l (λ (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 : ) :
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 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 * real.log x
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 real.log x z * real.log y
theorem real.le_rpow_of_log_le {x y z : } (hx : 0 x) (hy : 0 < y) (h : real.log x z * real.log y) :
x y ^ z
theorem real.lt_rpow_iff_log_lt {x y z : } (hx : 0 < x) (hy : 0 < y) :
x < y ^ z real.log x < z * real.log y
theorem real.lt_rpow_of_log_lt {x y z : } (hx : 0 x) (hy : 0 < y) (h : real.log x < z * real.log y) :
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) :
|real.log x * 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 : × ), real.exp (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 : × ), real.exp (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 : filter.tendsto f l (nhds x)) (hg : filter.tendsto g l (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 : filter.tendsto f l (nhds x)) (h : x 0 0 p) :
filter.tendsto (λ (a : α), f a ^ p) l (nhds (x ^ p))
theorem continuous_at.rpow {α : Type u_1} [topological_space α] {f g : α } {x : α} (hf : continuous_at f x) (hg : continuous_at g x) (h : f x 0 0 < g x) :
continuous_at (λ (t : α), f t ^ g t) x
theorem continuous_within_at.rpow {α : Type u_1} [topological_space α] {f g : α } {s : set α} {x : α} (hf : continuous_within_at f s x) (hg : continuous_within_at g s 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} [topological_space α] {f g : α } {s : set α} (hf : continuous_on f s) (hg : continuous_on g 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} [topological_space α] {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} [topological_space α] {f : α } {s : set α} {x : α} {p : } (hf : continuous_within_at f s x) (h : f x 0 0 p) :
continuous_within_at (λ (x : α), f x ^ p) s x
theorem continuous_at.rpow_const {α : Type u_1} [topological_space α] {f : α } {x : α} {p : } (hf : continuous_at f x) (h : f x 0 0 p) :
continuous_at (λ (x : α), f x ^ p) x
theorem continuous_on.rpow_const {α : Type u_1} [topological_space α] {f : α } {s : set α} {p : } (hf : continuous_on f s) (h : (x : α), x s f x 0 0 p) :
continuous_on (λ (x : α), f x ^ p) s
theorem continuous.rpow_const {α : Type u_1} [topological_space α] {f : α } {p : } (hf : continuous f) (h : (x : α), f x 0 0 p) :
continuous (λ (x : α), f x ^ p)
theorem real.sqrt_eq_rpow (x : ) :
real.sqrt x = x ^ (1 / 2)
theorem real.rpow_div_two_eq_sqrt {x : } (r : ) (hx : 0 x) :
x ^ (r / 2) = real.sqrt 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 * real.exp (-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 : asymptotics.is_O_with c l f 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 : ), real.exp (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 : ), real.exp (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 : ), real.exp (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 ^ 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 : ), real.log x ^ r) =o[filter.at_top] λ (x : ), x ^ s
theorem is_o_abs_log_rpow_rpow_nhds_zero {s : } (r : ) (hs : s < 0) :
(λ (x : ), |real.log x| ^ r) =o[nhds_within 0 (set.Ioi 0)] λ (x : ), x ^ s
theorem is_o_log_rpow_nhds_zero {r : } (hr : r < 0) :
real.log =o[nhds_within 0 (set.Ioi 0)] λ (x : ), x ^ r
theorem tendsto_log_div_rpow_nhds_zero {r : } (hr : r < 0) :
filter.tendsto (λ (x : ), real.log x / x ^ r) (nhds_within 0 (set.Ioi 0)) (nhds 0)
theorem tendsto_log_mul_rpow_nhds_zero {r : } (hr : 0 < r) :
filter.tendsto (λ (x : ), real.log x * x ^ r) (nhds_within 0 (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 complex.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 complex.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 complex.continuous_at_cpow_const for a version that assumes z ≠ 0 but makes no assumptions about w.

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) :
nnreal.sqrt x = 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 : nnreal × ), 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} [linear_ordered_field α] [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 : filter.tendsto u f (nhds x)) (hy : filter.tendsto v f (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) :
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 : filter.tendsto m f (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).

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

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.