# Power function on ℝ#

We construct the power functions x ^ y, where x and y are real numbers.

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 arbitrary 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
• x.rpow y = (x ^ y).re
Instances For
noncomputable instance Real.instPow :
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 = if x = 0 then if y = 0 then 1 else 0 else Real.exp ( * y)
theorem Real.rpow_def_of_pos {x : } (hx : 0 < x) (y : ) :
x ^ y = Real.exp ( * y)
theorem Real.exp_mul (x : ) (y : ) :
Real.exp (x * y) = ^ y
@[simp]
theorem Real.rpow_intCast (x : ) (n : ) :
x ^ n = x ^ n
@[deprecated Real.rpow_intCast]
theorem Real.rpow_int_cast (x : ) (n : ) :
x ^ n = x ^ n

Alias of Real.rpow_intCast.

@[simp]
theorem Real.rpow_natCast (x : ) (n : ) :
x ^ n = x ^ n
@[deprecated Real.rpow_natCast]
theorem Real.rpow_nat_cast (x : ) (n : ) :
x ^ n = x ^ n

Alias of Real.rpow_natCast.

@[simp]
theorem Real.exp_one_rpow (x : ) :
^ x =
@[simp]
theorem Real.exp_one_pow (n : ) :
^ n = Real.exp n
theorem Real.rpow_eq_zero_iff_of_nonneg {x : } {y : } (hx : 0 x) :
x ^ y = 0 x = 0 y 0
@[simp]
theorem Real.rpow_eq_zero {x : } {y : } (hx : 0 x) (hy : y 0) :
x ^ y = 0 x = 0
@[simp]
theorem Real.rpow_ne_zero {x : } {y : } (hx : 0 x) (hy : y 0) :
x ^ y 0 x 0
theorem Real.rpow_def_of_neg {x : } (hx : x < 0) (y : ) :
x ^ y = Real.exp ( * y) * Real.cos ()
theorem Real.rpow_def_of_nonpos {x : } (hx : x 0) (y : ) :
x ^ y = if x = 0 then if y = 0 then 1 else 0 else Real.exp ( * y) * Real.cos ()
theorem Real.rpow_pos_of_pos {x : } (hx : 0 < x) (y : ) :
0 < x ^ y
@[simp]
theorem Real.rpow_zero (x : ) :
x ^ 0 = 1
theorem Real.rpow_zero_pos (x : ) :
0 < x ^ 0
@[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 {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| Real.exp ( * y)
theorem Real.norm_rpow_of_nonneg {x : } {y : } (hx_nonneg : 0 x) :
x ^ y = x ^ y
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_of_add_eq {w : } {x : } {y : } {z : } (hx : 0 x) (hw : w 0) (h : y + z = w) :
x ^ w = x ^ y * x ^ z

Variant of Real.rpow_add' that avoids having to prove y + z = w twice.

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 : ) :
a ^ xs, f x = xs, a ^ f x
theorem Real.rpow_sum_of_nonneg {ι : Type u_1} {a : } (ha : 0 a) {s : } {f : ι} (h : xs, 0 f x) :
a ^ xs, f x = xs, a ^ f x
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 HasCompactSupport.rpow_const {α : Type u_1} [] {f : α} (hf : ) {r : } (hr : r 0) :
HasCompactSupport fun (x : α) => f x ^ r

## Comparing real and complex powers #

theorem Complex.ofReal_cpow {x : } (hx : 0 x) (y : ) :
(x ^ y) = x ^ y
theorem Complex.ofReal_cpow_of_nonpos {x : } (hx : x 0) (y : ) :
x ^ y = (-x) ^ y * Complex.exp ()
theorem Complex.cpow_ofReal (x : ) (y : ) :
x ^ y = (Complex.abs x ^ y) * ((Real.cos (x.arg * y)) + (Real.sin (x.arg * y)) * Complex.I)
theorem Complex.cpow_ofReal_re (x : ) (y : ) :
(x ^ y).re = Complex.abs x ^ y * Real.cos (x.arg * y)
theorem Complex.cpow_ofReal_im (x : ) (y : ) :
(x ^ y).im = Complex.abs x ^ y * Real.sin (x.arg * y)
theorem Complex.abs_cpow_of_ne_zero {z : } (hz : z 0) (w : ) :
Complex.abs (z ^ w) = Complex.abs z ^ w.re / Real.exp (z.arg * w.im)
theorem Complex.abs_cpow_of_imp {z : } {w : } (h : z = 0w.re = 0w = 0) :
Complex.abs (z ^ w) = Complex.abs z ^ w.re / Real.exp (z.arg * w.im)
theorem Complex.abs_cpow_le (z : ) (w : ) :
Complex.abs (z ^ w) Complex.abs z ^ w.re / Real.exp (z.arg * w.im)
@[simp]
theorem Complex.abs_cpow_real (x : ) (y : ) :
Complex.abs (x ^ y) = Complex.abs x ^ y
@[simp]
theorem Complex.abs_cpow_inv_nat (x : ) (n : ) :
Complex.abs (x ^ (n)⁻¹) = Complex.abs x ^ (n)⁻¹
theorem Complex.abs_cpow_eq_rpow_re_of_pos {x : } (hx : 0 < x) (y : ) :
Complex.abs (x ^ y) = x ^ y.re
theorem Complex.abs_cpow_eq_rpow_re_of_nonneg {x : } (hx : 0 x) {y : } (hy : y.re 0) :
Complex.abs (x ^ y) = x ^ y.re
theorem Complex.norm_natCast_cpow_of_re_ne_zero (n : ) {s : } (hs : s.re 0) :
n ^ s = n ^ s.re
theorem Complex.norm_natCast_cpow_of_pos {n : } (hn : 0 < n) (s : ) :
n ^ s = n ^ s.re
theorem Complex.norm_natCast_cpow_pos_of_pos {n : } (hn : 0 < n) (s : ) :
0 < n ^ s
theorem Complex.cpow_mul_ofReal_nonneg {x : } (hx : 0 x) (y : ) (z : ) :
x ^ (y * z) = (x ^ y) ^ z

### Positivity extension #

Extension for the positivity tactic: exponentiation by a real number is positive (namely 1) when the exponent is zero. The other cases are done in evalRpow.

Instances For

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

Instances For

## Further algebraic properties of rpow#

theorem Real.rpow_mul {x : } (hx : 0 x) (y : ) (z : ) :
x ^ (y * z) = (x ^ y) ^ 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_int' {x : } {y : } (hx : 0 x) {n : } (h : y + n 0) :
x ^ (y + n) = x ^ y * x ^ n
theorem Real.rpow_add_nat' {x : } {y : } {n : } (hx : 0 x) (h : y + n 0) :
x ^ (y + n) = x ^ y * x ^ n
theorem Real.rpow_sub_int' {x : } {y : } (hx : 0 x) {n : } (h : y - n 0) :
x ^ (y - n) = x ^ y / x ^ n
theorem Real.rpow_sub_nat' {x : } {y : } {n : } (hx : 0 x) (h : y - n 0) :
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
theorem Real.rpow_add_one' {x : } {y : } (hx : 0 x) (h : y + 1 0) :
x ^ (y + 1) = x ^ y * x
theorem Real.rpow_one_add' {x : } {y : } (hx : 0 x) (h : 1 + y 0) :
x ^ (1 + y) = x * x ^ y
theorem Real.rpow_sub_one' {x : } {y : } (hx : 0 x) (h : y - 1 0) :
x ^ (y - 1) = x ^ y / x
theorem Real.rpow_one_sub' {x : } {y : } (hx : 0 x) (h : 1 - y 0) :
x ^ (1 - y) = x / x ^ y
@[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 : } (hx : 0 x) (hy : 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.mul_log_eq_log_iff {x : } {y : } {z : } (hx : 0 < x) (hz : 0 < z) :
y * = x ^ y = z
@[simp]
theorem Real.rpow_rpow_inv {x : } {y : } (hx : 0 x) (hy : y 0) :
(x ^ y) ^ y⁻¹ = x
@[simp]
theorem Real.rpow_inv_rpow {x : } {y : } (hx : 0 x) (hy : y 0) :
(x ^ y⁻¹) ^ y = x
theorem Real.pow_rpow_inv_natCast {x : } {n : } (hx : 0 x) (hn : n 0) :
(x ^ n) ^ (n)⁻¹ = x
theorem Real.rpow_inv_natCast_pow {x : } {n : } (hx : 0 x) (hn : n 0) :
(x ^ (n)⁻¹) ^ n = x
theorem Real.rpow_natCast_mul {x : } (hx : 0 x) (n : ) (z : ) :
x ^ (n * z) = (x ^ n) ^ z
theorem Real.rpow_mul_natCast {x : } (hx : 0 x) (y : ) (n : ) :
x ^ (y * n) = (x ^ y) ^ n
theorem Real.rpow_intCast_mul {x : } (hx : 0 x) (n : ) (z : ) :
x ^ (n * z) = (x ^ n) ^ z
theorem Real.rpow_mul_intCast {x : } (hx : 0 x) (y : ) (n : ) :
x ^ (y * n) = (x ^ y) ^ n

Note: lemmas about (∏ i ∈ s, f i ^ r) such as Real.finset_prod_rpow are proved in Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean instead.

## Order and monotonicity #

theorem Real.rpow_lt_rpow {x : } {y : } {z : } (hx : 0 x) (hxy : x < y) (hz : 0 < z) :
x ^ z < y ^ z
theorem Real.strictMonoOn_rpow_Ici_of_exponent_pos {r : } (hr : 0 < r) :
StrictMonoOn (fun (x : ) => x ^ r) ()
theorem Real.rpow_le_rpow {x : } {y : } {z : } (h : 0 x) (h₁ : x y) (h₂ : 0 z) :
x ^ z y ^ z
theorem Real.monotoneOn_rpow_Ici_of_exponent_nonneg {r : } (hr : 0 r) :
MonotoneOn (fun (x : ) => x ^ r) ()
theorem Real.rpow_lt_rpow_of_neg {x : } {y : } {z : } (hx : 0 < x) (hxy : x < y) (hz : z < 0) :
y ^ z < x ^ z
theorem Real.rpow_le_rpow_of_nonpos {x : } {y : } {z : } (hx : 0 < x) (hxy : x y) (hz : z 0) :
y ^ z x ^ 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.rpow_lt_rpow_iff_of_neg {x : } {y : } {z : } (hx : 0 < x) (hy : 0 < y) (hz : z < 0) :
x ^ z < y ^ z y < x
theorem Real.rpow_le_rpow_iff_of_neg {x : } {y : } {z : } (hx : 0 < x) (hy : 0 < y) (hz : z < 0) :
x ^ z y ^ z y x
theorem Real.le_rpow_inv_iff_of_pos {x : } {y : } {z : } (hx : 0 x) (hy : 0 y) (hz : 0 < z) :
x y ^ z⁻¹ x ^ z y
theorem Real.rpow_inv_le_iff_of_pos {x : } {y : } {z : } (hx : 0 x) (hy : 0 y) (hz : 0 < z) :
x ^ z⁻¹ y x y ^ z
theorem Real.lt_rpow_inv_iff_of_pos {x : } {y : } {z : } (hx : 0 x) (hy : 0 y) (hz : 0 < z) :
x < y ^ z⁻¹ x ^ z < y
theorem Real.rpow_inv_lt_iff_of_pos {x : } {y : } {z : } (hx : 0 x) (hy : 0 y) (hz : 0 < z) :
x ^ z⁻¹ < y x < y ^ z
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
theorem Real.rpow_lt_rpow_of_exponent_neg {x : } {y : } {z : } (hy : 0 < y) (hxy : y < x) (hz : z < 0) :
x ^ z < y ^ z
theorem Real.strictAntiOn_rpow_Ioi_of_exponent_neg {r : } (hr : r < 0) :
StrictAntiOn (fun (x : ) => x ^ r) ()
theorem Real.rpow_le_rpow_of_exponent_nonpos {z : } {x : } {y : } (hy : 0 < y) (hxy : y x) (hz : z 0) :
x ^ z y ^ z
theorem Real.antitoneOn_rpow_Ioi_of_exponent_nonpos {r : } (hr : r 0) :
AntitoneOn (fun (x : ) => x ^ r) ()
@[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.rpow_lt_one_iff' {x : } {y : } (hx : 0 x) (hy : 0 < y) :
x ^ y < 1 x < 1
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_injOn {x : } (hx : x 0) :
Set.InjOn (fun (y : ) => y ^ x) {y : | 0 y}
theorem Real.rpow_left_inj {x : } {y : } {z : } (hx : 0 x) (hy : 0 y) (hz : z 0) :
x ^ z = y ^ z x = y
theorem Real.rpow_inv_eq {x : } {y : } {z : } (hx : 0 x) (hy : 0 y) (hz : z 0) :
x ^ z⁻¹ = y x = y ^ z
theorem Real.eq_rpow_inv {x : } {y : } {z : } (hx : 0 x) (hy : 0 y) (hz : z 0) :
x = y ^ z⁻¹ x ^ z = 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.log_le_rpow_div {x : } {ε : } (hx : 0 x) (hε : 0 < ε) :
x ^ ε / ε

log x is bounded above by a multiple of every power of x with positive exponent.

theorem Real.log_natCast_le_rpow_div (n : ) {ε : } (hε : 0 < ε) :
Real.log n n ^ ε / ε

The (real) logarithm of a natural number n is bounded by a multiple of every power of n with positive exponent.

theorem Real.strictMono_rpow_of_base_gt_one {b : } (hb : 1 < b) :
StrictMono fun (x : ) => b ^ x
theorem Real.monotone_rpow_of_base_ge_one {b : } (hb : 1 b) :
Monotone fun (x : ) => b ^ x
theorem Real.strictAnti_rpow_of_base_lt_one {b : } (hb₀ : 0 < b) (hb₁ : b < 1) :
StrictAnti fun (x : ) => b ^ x
theorem Real.antitone_rpow_of_base_le_one {b : } (hb₀ : 0 < b) (hb₁ : b 1) :
Antitone fun (x : ) => b ^ x
theorem Complex.norm_prime_cpow_le_one_half (p : Nat.Primes) {s : } (hs : 1 < s.re) :
p ^ (-s) 1 / 2
theorem Complex.one_sub_prime_cpow_ne_zero {p : } (hp : ) {s : } (hs : 1 < s.re) :
1 - p ^ (-s) 0
theorem Complex.norm_natCast_cpow_le_norm_natCast_cpow_of_pos {n : } (hn : 0 < n) {w : } {z : } (h : w.re z.re) :
n ^ w n ^ z
theorem Complex.norm_natCast_cpow_le_norm_natCast_cpow_iff {n : } (hn : 1 < n) {w : } {z : } :
n ^ w n ^ z w.re z.re
theorem Complex.norm_log_natCast_le_rpow_div (n : ) {ε : } (hε : 0 < ε) :
n ^ ε / ε

## Square roots of reals #

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 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} [] (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 Complex.cpow_inv_two_re (x : ) :
(x ^ 2⁻¹).re = ((Complex.abs x + x.re) / 2)
theorem Complex.cpow_inv_two_im_eq_sqrt {x : } (hx : 0 x.im) :
(x ^ 2⁻¹).im = ((Complex.abs x - x.re) / 2)
theorem Complex.cpow_inv_two_im_eq_neg_sqrt {x : } (hx : x.im < 0) :
(x ^ 2⁻¹).im = -((Complex.abs x - x.re) / 2)
theorem Complex.abs_cpow_inv_two_im (x : ) :
|(x ^ 2⁻¹).im| = ((Complex.abs x - x.re) / 2)

## Tactic extensions for real powers #

theorem Mathlib.Meta.NormNum.isNat_rpow_pos {a : } {b : } {nb : } {ne : } (pb : ) (pe' : Mathlib.Meta.NormNum.IsNat (a ^ nb) ne) :
theorem Mathlib.Meta.NormNum.isNat_rpow_neg {a : } {b : } {nb : } {ne : } (pb : ) (pe' : Mathlib.Meta.NormNum.IsNat (a ^ ) ne) :
theorem Mathlib.Meta.NormNum.isInt_rpow_pos {a : } {b : } {nb : } {ne : } (pb : ) (pe' : Mathlib.Meta.NormNum.IsInt (a ^ nb) ()) :
theorem Mathlib.Meta.NormNum.isInt_rpow_neg {a : } {b : } {nb : } {ne : } (pb : ) (pe' : Mathlib.Meta.NormNum.IsInt (a ^ ) ()) :
theorem Mathlib.Meta.NormNum.isRat_rpow_pos {a : } {b : } {nb : } {num : } {den : } (pb : ) (pe' : Mathlib.Meta.NormNum.IsRat (a ^ nb) num den) :
theorem Mathlib.Meta.NormNum.isRat_rpow_neg {a : } {b : } {nb : } {num : } {den : } (pb : ) (pe' : Mathlib.Meta.NormNum.IsRat (a ^ ) num den) :

Evaluates expressions of the form a ^ b when a and b are both reals.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[deprecated Real.rpow_nonneg]
theorem rpow_nonneg_of_nonneg {x : } (hx : 0 x) (y : ) :
0 x ^ y

Alias of Real.rpow_nonneg.