mathlib3documentation

analysis.special_functions.pow.real

Power function on ℝ#

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 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 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_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.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)
@[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) :

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, 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 *

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

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} [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.

Tactic extensions for real powers #

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

Evaluates expressions of the form rpow 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.

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