mathlib documentation

analysis.special_functions.pow

Power function on , , ℝ≥0, and ennreal

We construct the power functions x ^ y where

We also prove basic properties of these functions.

def complex.cpow  :

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
@[instance]

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 ((x.log) * 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 : } :
x 00 ^ x = 0

@[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 : ) :
x 0x ^ (y + z) = (x ^ y) * x ^ z

theorem complex.cpow_mul {x y : } (z : ) :
-π < ((x.log) * y).im((x.log) * y).im πx ^ y * z = (x ^ y) ^ z

theorem complex.cpow_neg (x y : ) :
x ^ -y = (x ^ y)⁻¹

theorem complex.cpow_neg_one (x : ) :
x ^ -1 = x⁻¹

@[simp]
theorem complex.cpow_nat_cast (x : ) (n : ) :
x ^ n = x ^ n

@[simp]
theorem complex.cpow_int_cast (x : ) (n : ) :
x ^ n = x ^ n

theorem complex.cpow_nat_inv_pow (x : ) {n : } :
0 < n(x ^ (n)⁻¹) ^ n = x

def real.rpow  :

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
@[instance]

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

theorem real.rpow_eq_zero_iff_of_nonneg {x y : } :
0 x(x ^ y = 0 x = 0 y 0)

theorem real.rpow_def_of_neg {x : } (hx : x < 0) (y : ) :
x ^ y = (real.exp ((real.log x) * y)) * real.cos (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 * π))

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 : } :
x 00 ^ x = 0

@[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_le_abs_rpow (x y : ) :
abs (x ^ y) abs x ^ y

theorem complex.of_real_cpow {x : } (hx : 0 x) (y : ) :
(x ^ y) = x ^ y

@[simp]
theorem complex.abs_cpow_real (x : ) (y : ) :

@[simp]

theorem real.rpow_add {x : } (hx : 0 < x) (y z : ) :
x ^ (y + z) = (x ^ y) * x ^ z

theorem real.rpow_add' {x : } (hx : 0 x) {y z : } :
y + z 0x ^ (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_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 : } :
y - z 0x ^ (y - z) = x ^ y / x ^ z

@[simp]
theorem real.rpow_nat_cast (x : ) (n : ) :
x ^ n = x ^ n

@[simp]
theorem real.rpow_int_cast (x : ) (n : ) :
x ^ n = x ^ n

theorem real.rpow_neg_one (x : ) :
x ^ -1 = x⁻¹

theorem real.mul_rpow {x y z : } :
0 x0 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 : } :
0 xx < y0 < zx ^ z < y ^ z

theorem real.rpow_le_rpow {x y z : } :
0 xx y0 zx ^ z y ^ z

theorem real.rpow_lt_rpow_iff {x y z : } :
0 x0 y0 < z(x ^ z < y ^ z x < y)

theorem real.rpow_le_rpow_iff {x y z : } :
0 x0 y0 < z(x ^ z y ^ z x y)

theorem real.rpow_lt_rpow_of_exponent_lt {x y z : } :
1 < xy < zx ^ y < x ^ z

theorem real.rpow_le_rpow_of_exponent_le {x y z : } :
1 xy zx ^ y x ^ z

theorem real.rpow_lt_rpow_of_exponent_gt {x y z : } :
0 < xx < 1z < yx ^ y < x ^ z

theorem real.rpow_le_rpow_of_exponent_ge {x y z : } :
0 < xx 1z yx ^ y x ^ z

theorem real.rpow_lt_one {x z : } :
0 xx < 10 < zx ^ z < 1

theorem real.rpow_le_one {x z : } :
0 xx 10 zx ^ z 1

theorem real.rpow_lt_one_of_one_lt_of_neg {x z : } :
1 < xz < 0x ^ z < 1

theorem real.rpow_le_one_of_one_le_of_nonpos {x z : } :
1 xz 0x ^ z 1

theorem real.one_lt_rpow {x z : } :
1 < x0 < z1 < x ^ z

theorem real.one_le_rpow {x z : } :
1 x0 z1 x ^ z

theorem real.one_lt_rpow_of_pos_of_lt_one_of_neg {x z : } :
0 < xx < 1z < 01 < x ^ z

theorem real.one_le_rpow_of_pos_of_le_one_of_nonpos {x z : } :
0 < xx 1z 01 x ^ z

theorem real.rpow_lt_one_iff_of_pos {x y : } :
0 < x(x ^ y < 1 1 < x y < 0 x < 1 0 < y)

theorem real.rpow_lt_one_iff {x y : } :
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 : } :
0 < x(1 < x ^ y 1 < x 0 < y x < 1 y < 0)

theorem real.one_lt_rpow_iff {x y : } :
0 x(1 < x ^ y 1 < x 0 < y 0 < x x < 1 y < 0)

theorem real.rpow_le_one_iff_of_pos {x y : } :
0 < x(x ^ y 1 1 x y 0 x 1 0 y)

theorem real.pow_nat_rpow_nat_inv {x : } (hx : 0 x) {n : } :
0 < n(x ^ n) ^ (n)⁻¹ = x

theorem real.rpow_nat_inv_pow_nat {x : } (hx : 0 x) {n : } :
0 < n(x ^ (n)⁻¹) ^ n = x

theorem real.continuous_rpow_aux1  :
continuous (λ (p : {p // 0 < p.fst}), p.val.fst ^ p.val.snd)

theorem real.continuous_rpow_aux2  :
continuous (λ (p : {p // p.fst < 0}), p.val.fst ^ p.val.snd)

theorem real.continuous_at_rpow_of_ne_zero {x : } (hx : x 0) (y : ) :
continuous_at (λ (p : × ), p.fst ^ p.snd) (x, y)

theorem real.continuous_rpow_aux3  :
continuous (λ (p : {p // 0 < p.snd}), p.val.fst ^ p.val.snd)

theorem real.continuous_at_rpow_of_pos {y : } (hy : 0 < y) (x : ) :
continuous_at (λ (p : × ), p.fst ^ p.snd) (x, y)

theorem real.continuous_at_rpow {x y : } :
x 0 0 < ycontinuous_at (λ (p : × ), p.fst ^ p.snd) (x, y)

theorem real.continuous_rpow {α : Type u_1} [topological_space α] {f g : α → } :
(∀ (a : α), f a 0 0 < g a)continuous fcontinuous gcontinuous (λ (a : α), f a ^ g a)

real.rpow is continuous at all points except for the lower half of the y-axis. In other words, the function λp:ℝ×ℝ, p.1^p.2 is continuous at (x, y) if x ≠ 0 or y > 0.

Multiple forms of the claim is provided in the current section.

theorem real.continuous_rpow_of_ne_zero {α : Type u_1} [topological_space α] {f g : α → } :
(∀ (a : α), f a 0)continuous fcontinuous gcontinuous (λ (a : α), f a ^ g a)

theorem real.continuous_rpow_of_pos {α : Type u_1} [topological_space α] {f g : α → } :
(∀ (a : α), 0 < g a)continuous fcontinuous gcontinuous (λ (a : α), f a ^ g a)

theorem real.has_deriv_at_rpow_of_pos {x : } (h : 0 < x) (p : ) :
has_deriv_at (λ (x : ), x ^ p) (p * x ^ (p - 1)) x

theorem real.has_deriv_at_rpow_of_neg {x : } (h : x < 0) (p : ) :
has_deriv_at (λ (x : ), x ^ p) (p * x ^ (p - 1)) x

theorem real.has_deriv_at_rpow {x : } (h : x 0) (p : ) :
has_deriv_at (λ (x : ), x ^ p) (p * x ^ (p - 1)) x

theorem real.has_deriv_at_rpow_zero_of_one_le {p : } :
1 phas_deriv_at (λ (x : ), x ^ p) (p * 0 ^ (p - 1)) 0

theorem real.has_deriv_at_rpow_of_one_le (x : ) {p : } :
1 phas_deriv_at (λ (x : ), x ^ p) (p * x ^ (p - 1)) x

theorem real.sqrt_eq_rpow  :
real.sqrt = λ (x : ), x ^ (1 / 2)

theorem has_deriv_within_at.rpow {f : } {x f' : } {s : set } (p : ) :
has_deriv_within_at f f' s xf x 0has_deriv_within_at (λ (y : ), f y ^ p) ((f' * p) * f x ^ (p - 1)) s x

theorem has_deriv_at.rpow {f : } {x f' : } (p : ) :
has_deriv_at f f' xf x 0has_deriv_at (λ (y : ), f y ^ p) ((f' * p) * f x ^ (p - 1)) x

theorem differentiable_within_at.rpow {f : } {x : } {s : set } (p : ) :
differentiable_within_at f s xf x 0differentiable_within_at (λ (x : ), f x ^ p) s x

@[simp]
theorem differentiable_at.rpow {f : } {x : } (p : ) :
differentiable_at f xf x 0differentiable_at (λ (x : ), f x ^ p) x

theorem differentiable_on.rpow {f : } {s : set } (p : ) :
differentiable_on f s(∀ (x : ), x sf x 0)differentiable_on (λ (x : ), f x ^ p) s

@[simp]
theorem differentiable.rpow {f : } (p : ) :
differentiable f(∀ (x : ), f x 0)differentiable (λ (x : ), f x ^ p)

theorem deriv_within_rpow {f : } {x : } {s : set } (p : ) :
differentiable_within_at f s xf x 0unique_diff_within_at s xderiv_within (λ (x : ), f x ^ p) s x = ((deriv_within f s x) * p) * f x ^ (p - 1)

@[simp]
theorem deriv_rpow {f : } {x : } (p : ) :
differentiable_at f xf x 0deriv (λ (x : ), f x ^ p) x = ((deriv f x) * p) * f x ^ (p - 1)

theorem has_deriv_within_at.rpow_of_one_le {f : } {x f' : } {s : set } {p : } :
has_deriv_within_at f f' s x1 phas_deriv_within_at (λ (y : ), f y ^ p) ((f' * p) * f x ^ (p - 1)) s x

theorem has_deriv_at.rpow_of_one_le {f : } {x f' p : } :
has_deriv_at f f' x1 phas_deriv_at (λ (y : ), f y ^ p) ((f' * p) * f x ^ (p - 1)) x

theorem differentiable_within_at.rpow_of_one_le {f : } {x : } {s : set } {p : } :
differentiable_within_at f s x1 pdifferentiable_within_at (λ (x : ), f x ^ p) s x

@[simp]
theorem differentiable_at.rpow_of_one_le {f : } {x p : } :
differentiable_at f x1 pdifferentiable_at (λ (x : ), f x ^ p) x

theorem differentiable_on.rpow_of_one_le {f : } {s : set } {p : } :
differentiable_on f s1 pdifferentiable_on (λ (x : ), f x ^ p) s

@[simp]
theorem differentiable.rpow_of_one_le {f : } {p : } :
differentiable f1 pdifferentiable (λ (x : ), f x ^ p)

theorem deriv_within_rpow_of_one_le {f : } {x : } {s : set } {p : } :
differentiable_within_at f s x1 punique_diff_within_at s xderiv_within (λ (x : ), f x ^ p) s x = ((deriv_within f s x) * p) * f x ^ (p - 1)

@[simp]
theorem deriv_rpow_of_one_le {f : } {x p : } :
differentiable_at f x1 pderiv (λ (x : ), f x ^ p) x = ((deriv f x) * p) * f x ^ (p - 1)

theorem has_deriv_within_at.sqrt {f : } {x f' : } {s : set } :
has_deriv_within_at f f' s xf x 0has_deriv_within_at (λ (y : ), real.sqrt (f y)) (f' / 2 * real.sqrt (f x)) s x

theorem has_deriv_at.sqrt {f : } {x f' : } :
has_deriv_at f f' xf x 0has_deriv_at (λ (y : ), real.sqrt (f y)) (f' / 2 * real.sqrt (f x)) x

theorem differentiable_within_at.sqrt {f : } {x : } {s : set } :
differentiable_within_at f s xf x 0differentiable_within_at (λ (x : ), real.sqrt (f x)) s x

@[simp]
theorem differentiable_at.sqrt {f : } {x : } :
differentiable_at f xf x 0differentiable_at (λ (x : ), real.sqrt (f x)) x

theorem differentiable_on.sqrt {f : } {s : set } :
differentiable_on f s(∀ (x : ), x sf x 0)differentiable_on (λ (x : ), real.sqrt (f x)) s

@[simp]
theorem differentiable.sqrt {f : } :
differentiable f(∀ (x : ), f x 0)differentiable (λ (x : ), real.sqrt (f x))

theorem deriv_within_sqrt {f : } {x : } {s : set } :
differentiable_within_at f s xf x 0unique_diff_within_at s xderiv_within (λ (x : ), real.sqrt (f x)) s x = deriv_within f s x / 2 * real.sqrt (f x)

@[simp]
theorem deriv_sqrt {f : } {x : } :
differentiable_at f xf x 0deriv (λ (x : ), real.sqrt (f x)) x = deriv f x / 2 * real.sqrt (f x)

theorem tendsto_rpow_at_top {y : } :

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

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

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

theorem tendsto_rpow_div_mul_add (a b c : ) :
0 bfilter.tendsto (λ (x : ), x ^ (a / (b * x + c))) filter.at_top (𝓝 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 (𝓝 1)

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

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

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

def nnreal.rpow  :

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
@[simp]
theorem nnreal.rpow_eq_pow (x : ℝ≥0) (y : ) :
x.rpow y = x ^ y

@[simp]
theorem nnreal.coe_rpow (x : ℝ≥0) (y : ) :
(x ^ y) = x ^ y

@[simp]
theorem nnreal.rpow_zero (x : ℝ≥0) :
x ^ 0 = 1

@[simp]
theorem nnreal.rpow_eq_zero_iff {x : ℝ≥0} {y : } :
x ^ y = 0 x = 0 y 0

@[simp]
theorem nnreal.zero_rpow {x : } :
x 00 ^ x = 0

@[simp]
theorem nnreal.rpow_one (x : ℝ≥0) :
x ^ 1 = x

@[simp]
theorem nnreal.one_rpow (x : ) :
1 ^ x = 1

theorem nnreal.rpow_add {x : ℝ≥0} (hx : x 0) (y z : ) :
x ^ (y + z) = (x ^ y) * x ^ z

theorem nnreal.rpow_add' (x : ℝ≥0) {y z : } :
y + z 0x ^ (y + z) = (x ^ y) * x ^ z

theorem nnreal.rpow_mul (x : ℝ≥0) (y z : ) :
x ^ y * z = (x ^ y) ^ z

theorem nnreal.rpow_neg (x : ℝ≥0) (y : ) :
x ^ -y = (x ^ y)⁻¹

theorem nnreal.rpow_neg_one (x : ℝ≥0) :
x ^ -1 = x⁻¹

theorem nnreal.rpow_sub {x : ℝ≥0} (hx : x 0) (y z : ) :
x ^ (y - z) = x ^ y / x ^ z

theorem nnreal.rpow_sub' (x : ℝ≥0) {y z : } :
y - z 0x ^ (y - z) = x ^ y / x ^ z

theorem nnreal.inv_rpow (x : ℝ≥0) (y : ) :
x⁻¹ ^ y = (x ^ y)⁻¹

theorem nnreal.div_rpow (x y : ℝ≥0) (z : ) :
(x / y) ^ z = x ^ z / y ^ z

@[simp]
theorem nnreal.rpow_nat_cast (x : ℝ≥0) (n : ) :
x ^ n = x ^ n

theorem nnreal.mul_rpow {x y : ℝ≥0} {z : } :
(x * y) ^ z = (x ^ z) * y ^ z

theorem nnreal.rpow_le_rpow {x y : ℝ≥0} {z : } :
x y0 zx ^ z y ^ z

theorem nnreal.rpow_lt_rpow {x y : ℝ≥0} {z : } :
x < y0 < zx ^ z < y ^ z

theorem nnreal.rpow_lt_rpow_iff {x y : ℝ≥0} {z : } :
0 < z(x ^ z < y ^ z x < y)

theorem nnreal.rpow_le_rpow_iff {x y : ℝ≥0} {z : } :
0 < z(x ^ z y ^ z x y)

theorem nnreal.rpow_lt_rpow_of_exponent_lt {x : ℝ≥0} {y z : } :
1 < xy < zx ^ y < x ^ z

theorem nnreal.rpow_le_rpow_of_exponent_le {x : ℝ≥0} {y z : } :
1 xy zx ^ y x ^ z

theorem nnreal.rpow_lt_rpow_of_exponent_gt {x : ℝ≥0} {y z : } :
0 < xx < 1z < yx ^ y < x ^ z

theorem nnreal.rpow_le_rpow_of_exponent_ge {x : ℝ≥0} {y z : } :
0 < xx 1z yx ^ y x ^ z

theorem nnreal.rpow_lt_one {x : ℝ≥0} {z : } :
0 xx < 10 < zx ^ z < 1

theorem nnreal.rpow_le_one {x : ℝ≥0} {z : } :
x 10 zx ^ z 1

theorem nnreal.rpow_lt_one_of_one_lt_of_neg {x : ℝ≥0} {z : } :
1 < xz < 0x ^ z < 1

theorem nnreal.rpow_le_one_of_one_le_of_nonpos {x : ℝ≥0} {z : } :
1 xz 0x ^ z 1

theorem nnreal.one_lt_rpow {x : ℝ≥0} {z : } :
1 < x0 < z1 < x ^ z

theorem nnreal.one_le_rpow {x : ℝ≥0} {z : } :
1 x0 z1 x ^ z

theorem nnreal.one_lt_rpow_of_pos_of_lt_one_of_neg {x : ℝ≥0} {z : } :
0 < xx < 1z < 01 < x ^ z

theorem nnreal.one_le_rpow_of_pos_of_le_one_of_nonpos {x : ℝ≥0} {z : } :
0 < xx 1z 01 x ^ z

theorem nnreal.pow_nat_rpow_nat_inv (x : ℝ≥0) {n : } :
0 < n(x ^ n) ^ (n)⁻¹ = x

theorem nnreal.rpow_nat_inv_pow_nat (x : ℝ≥0) {n : } :
0 < n(x ^ (n)⁻¹) ^ n = x

theorem nnreal.continuous_at_rpow {x : ℝ≥0} {y : } :
x 0 0 < ycontinuous_at (λ (p : ℝ≥0 × ), p.fst ^ p.snd) (x, y)

theorem filter.tendsto.nnrpow {α : Type u_1} {f : filter α} {u : α → ℝ≥0} {v : α → } {x : ℝ≥0} {y : } :
filter.tendsto u f (𝓝 x)filter.tendsto v f (𝓝 y)x 0 0 < yfilter.tendsto (λ (a : α), u a ^ v a) f (𝓝 (x ^ y))

theorem nnreal.continuous_at_rpow_const {x : ℝ≥0} {y : } :
x 0 0 ycontinuous_at (λ (z : ℝ≥0), z ^ y) x

theorem nnreal.continuous_rpow_const {y : } :
0 ycontinuous (λ (x : ℝ≥0), x ^ y)

def ennreal.rpow  :

The real power function x^y on extended nonnegative reals, defined for x : ennreal 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
@[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 : } :
0 < y ^ y =

@[simp]
theorem ennreal.top_rpow_of_neg {y : } :
y < 0 ^ y = 0

@[simp]
theorem ennreal.zero_rpow_of_pos {y : } :
0 < y0 ^ y = 0

@[simp]
theorem ennreal.zero_rpow_of_neg {y : } :
y < 00 ^ y =

theorem ennreal.zero_rpow_def (y : ) :
0 ^ y = ite (0 < y) 0 (ite (y = 0) 1 )

theorem ennreal.coe_rpow_of_ne_zero {x : ℝ≥0} (h : x 0) (y : ) :
x ^ y = (x ^ y)

theorem ennreal.coe_rpow_of_nonneg (x : ℝ≥0) {y : } :
0 yx ^ y = (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_add {x : ennreal} (y z : ) :
x 0x x ^ (y + z) = (x ^ y) * x ^ z

theorem ennreal.rpow_neg (x : ennreal) (y : ) :
x ^ -y = (x ^ y)⁻¹

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]
theorem ennreal.rpow_nat_cast (x : ennreal) (n : ) :
x ^ n = x ^ n

theorem ennreal.coe_mul_rpow (x y : ℝ≥0) (z : ) :
((x) * y) ^ z = (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

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 : } :
0 z(x * y) ^ z = (x ^ z) * y ^ z

theorem ennreal.rpow_le_rpow {x y : ennreal} {z : } :
x y0 zx ^ z y ^ z

theorem ennreal.rpow_lt_rpow {x y : ennreal} {z : } :
x < y0 < zx ^ z < y ^ z

theorem ennreal.rpow_lt_rpow_of_exponent_lt {x : ennreal} {y z : } :
1 < xx y < zx ^ y < x ^ z

theorem ennreal.rpow_le_rpow_of_exponent_le {x : ennreal} {y z : } :
1 xy zx ^ y x ^ z

theorem ennreal.rpow_lt_rpow_of_exponent_gt {x : ennreal} {y z : } :
0 < xx < 1z < yx ^ y < x ^ z

theorem ennreal.rpow_le_rpow_of_exponent_ge {x : ennreal} {y z : } :
x 1z yx ^ y x ^ z

theorem ennreal.rpow_lt_one {x : ennreal} {z : } :
x < 10 < zx ^ z < 1

theorem ennreal.rpow_le_one {x : ennreal} {z : } :
x 10 zx ^ z 1

theorem ennreal.rpow_lt_one_of_one_lt_of_neg {x : ennreal} {z : } :
1 < xz < 0x ^ z < 1

theorem ennreal.rpow_le_one_of_one_le_of_neg {x : ennreal} {z : } :
1 xz < 0x ^ z 1

theorem ennreal.one_lt_rpow {x : ennreal} {z : } :
1 < x0 < z1 < x ^ z

theorem ennreal.one_le_rpow {x : ennreal} {z : } :
1 x0 < z1 x ^ z

theorem ennreal.one_lt_rpow_of_pos_of_lt_one_of_neg {x : ennreal} {z : } :
0 < xx < 1z < 01 < x ^ z

theorem ennreal.one_le_rpow_of_pos_of_le_one_of_neg {x : ennreal} {z : } :
0 < xx 1z < 01 x ^ z

theorem ennreal.to_real_rpow (x : ennreal) (z : ) :
x.to_real ^ z = (x ^ z).to_real