# Documentation

Mathlib.Analysis.SpecialFunctions.Pow.Real

# 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).

Instances For
noncomputable instance Real.instPowReal :
@[simp]
theorem Real.rpow_eq_pow (x : ) (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.exp_one_rpow (x : ) :
^ 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 = 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_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| 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_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 ^ Finset.sum s fun x => f x) = Finset.prod s fun x => a ^ f x
theorem Real.rpow_sum_of_nonneg {ι : Type u_1} {a : } (ha : 0 a) {s : } {f : ι} (h : ∀ (x : ι), x s0 f x) :
(a ^ Finset.sum s fun x => f x) = Finset.prod s fun x => 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

## 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.abs_cpow_of_ne_zero {z : } (hz : z 0) (w : ) :
Complex.abs (z ^ w) = ^ w.re / Real.exp ( * w.im)
theorem Complex.abs_cpow_of_imp {z : } {w : } (h : z = 0w.re = 0w = 0) :
Complex.abs (z ^ w) = ^ w.re / Real.exp ( * w.im)
theorem Complex.abs_cpow_le (z : ) (w : ) :
Complex.abs (z ^ w) ^ w.re / Real.exp ( * w.im)
@[simp]
theorem Complex.abs_cpow_real (x : ) (y : ) :
Complex.abs (x ^ y) = ^ y
@[simp]
theorem Complex.abs_cpow_inv_nat (x : ) (n : ) :
Complex.abs (x ^ (n)⁻¹) = ^ (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

## 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_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]
theorem Real.rpow_int_cast (x : ) (n : ) :
x ^ n = x ^ n
@[simp]
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.mul_log_eq_log_iff {x : } {y : } {z : } (hx : 0 < x) (hz : 0 < z) :
y * = x ^ y = z

Note: lemmas about (∏ i in 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_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
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.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.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.strictAnti_rpow_of_base_lt_one {b : } (hb₀ : 0 < b) (hb₁ : b < 1) :
theorem Real.antitone_rpow_of_base_le_one {b : } (hb₀ : 0 < b) (hb₁ : b 1) :

## Square roots of reals #

theorem Real.sqrt_eq_rpow (x : ) :
= x ^ (1 / 2)
theorem Real.rpow_div_two_eq_sqrt {x : } (r : ) (hx : 0 x) :
x ^ (r / 2) = ^ 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.

## Tactic extensions for real powers #

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