mathlib3documentation

analysis.special_functions.pow.nnreal

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

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 is a nonnegative real number and y is a real number;
• x is a number from [0, +∞] (a.k.a. ℝ≥0∞) and y is a real number.

We also prove basic properties of these functions.

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) :
= 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 real.to_nnreal_rpow_of_nonneg {x y : } (hx : 0 x) :
(x ^ y).to_nnreal = x.to_nnreal ^ 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) :
hy) x = x ^ y
theorem ennreal.order_iso_rpow_symm_apply (y : ) (hy : 0 < y) :
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)

Tactic extensions for powers on ℝ≥0 and ℝ≥0∞#

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 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 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_nnrpow (a b : expr) :

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.