# Documentation

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

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.

Instances For
noncomputable instance NNReal.instPowNNRealReal :
@[simp]
theorem NNReal.rpow_eq_pow (x : NNReal) (y : ) :
= x ^ y
@[simp]
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 : NNReal) (y : NNReal) (z : ) :
(x / y) ^ z = x ^ z / y ^ z
theorem NNReal.sqrt_eq_rpow (x : NNReal) :
= x ^ (1 / 2)
@[simp]
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 : NNReal} {y : NNReal} {z : } :
(x * y) ^ z = x ^ z * y ^ z
@[simp]
theorem NNReal.rpowMonoidHom_apply (r : ) :
∀ (x : NNReal), ↑() x = x ^ r

rpow as a MonoidHom

Instances For
theorem NNReal.list_prod_map_rpow (l : ) (r : ) :
List.prod (List.map (fun x => x ^ r) l) = ^ r

rpow variant of List.prod_map_pow for ℝ≥0

theorem NNReal.list_prod_map_rpow' {ι : Type u_1} (l : List ι) (f : ιNNReal) (r : ) :
List.prod (List.map (fun x => f x ^ r) l) = List.prod (List.map f l) ^ r
theorem NNReal.multiset_prod_map_rpow {ι : Type u_1} (s : ) (f : ιNNReal) (r : ) :
Multiset.prod (Multiset.map (fun x => f x ^ r) s) = ^ r

rpow version of Multiset.prod_map_pow for ℝ≥0.

theorem NNReal.finset_prod_rpow {ι : Type u_1} (s : ) (f : ιNNReal) (r : ) :
(Finset.prod s fun i => f i ^ r) = (Finset.prod s fun i => f i) ^ r

rpow version of Finset.prod_pow for ℝ≥0.

theorem Real.list_prod_map_rpow (l : ) (hl : ∀ (x : ), x l0 x) (r : ) :
List.prod (List.map (fun x => x ^ r) l) = ^ r

rpow version of List.prod_map_pow for Real.

theorem Real.list_prod_map_rpow' {ι : Type u_1} (l : List ι) (f : ι) (hl : ∀ (i : ι), i l0 f i) (r : ) :
List.prod (List.map (fun x => f x ^ r) l) = List.prod (List.map f l) ^ r
theorem Real.multiset_prod_map_rpow {ι : Type u_1} (s : ) (f : ι) (hs : ∀ (i : ι), i s0 f i) (r : ) :
Multiset.prod (Multiset.map (fun x => f x ^ r) s) = ^ r

rpow version of Multiset.prod_map_pow.

theorem Real.finset_prod_rpow {ι : Type u_1} (s : ) (f : ι) (hs : ∀ (i : ι), i s0 f i) (r : ) :
(Finset.prod s fun i => f i ^ r) = (Finset.prod s fun i => f i) ^ r

rpow version of Finset.prod_pow.

theorem NNReal.rpow_le_rpow {x : NNReal} {y : NNReal} {z : } (h₁ : x y) (h₂ : 0 z) :
x ^ z y ^ z
theorem NNReal.rpow_lt_rpow {x : NNReal} {y : NNReal} {z : } (h₁ : x < y) (h₂ : 0 < z) :
x ^ z < y ^ z
theorem NNReal.rpow_lt_rpow_iff {x : NNReal} {y : NNReal} {z : } (hz : 0 < z) :
x ^ z < y ^ z x < y
theorem NNReal.rpow_le_rpow_iff {x : NNReal} {y : NNReal} {z : } (hz : 0 < z) :
x ^ z y ^ z x y
theorem NNReal.le_rpow_one_div_iff {x : NNReal} {y : NNReal} {z : } (hz : 0 < z) :
x y ^ (1 / z) x ^ z y
theorem NNReal.rpow_one_div_le_iff {x : NNReal} {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 fun y => y ^ x
theorem NNReal.rpow_eq_rpow_iff {x : NNReal} {y : NNReal} {z : } (hz : z 0) :
x ^ z = y ^ z x = y
theorem NNReal.rpow_left_surjective {x : } (hx : x 0) :
Function.Surjective fun y => y ^ x
theorem NNReal.rpow_left_bijective {x : } (hx : x 0) :
Function.Bijective fun y => y ^ x
theorem NNReal.eq_rpow_one_div_iff {x : NNReal} {y : NNReal} {z : } (hz : z 0) :
x = y ^ (1 / z) x ^ z = y
theorem NNReal.rpow_one_div_eq_iff {x : NNReal} {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.toNNReal_rpow_of_nonneg {x : } {y : } (hx : 0 x) :
theorem NNReal.strictMono_rpow_of_pos {z : } (h : 0 < z) :
StrictMono fun x => x ^ z
theorem NNReal.monotone_rpow_of_nonneg {z : } (h : 0 z) :
Monotone fun x => x ^ z
@[simp]
theorem NNReal.orderIsoRpow_apply (y : ) (hy : 0 < y) (x : NNReal) :
↑() x = x ^ y
def NNReal.orderIsoRpow (y : ) (hy : 0 < y) :

Bundles fun x : ℝ≥0 => x ^ y into an order isomorphism when y : ℝ is positive, where the inverse is fun x : ℝ≥0 => x ^ (1 / y).

Instances For
theorem NNReal.orderIsoRpow_symm_eq (y : ) (hy : 0 < y) :
= NNReal.orderIsoRpow (1 / y) (_ : 0 < 1 / y)
noncomputable def ENNReal.rpow :
ENNReal

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

Instances For
noncomputable instance ENNReal.instPowENNRealReal :
@[simp]
theorem ENNReal.rpow_eq_pow (x : ENNReal) (y : ) :
= x ^ y
@[simp]
theorem ENNReal.rpow_zero {x : ENNReal} :
x ^ 0 = 1
theorem ENNReal.top_rpow_def (y : ) :
^ y = if 0 < y then else if y = 0 then 1 else 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 = if 0 < y then 0 else if y = 0 then 1 else
@[simp]
theorem ENNReal.zero_rpow_mul_self (y : ) :
0 ^ y * 0 ^ y = 0 ^ y
theorem ENNReal.coe_rpow_of_ne_zero {x : NNReal} (h : x 0) (y : ) :
x ^ y = ↑(x ^ y)
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 = if x = 0 y < 0 then else ↑(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_mul (x : ENNReal) (y : ) (z : ) :
x ^ (y * z) = (x ^ y) ^ z
@[simp]
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 : ENNReal) (y : ENNReal) (z : ) :
(x * y) ^ z = if (x = 0 y = x = y = 0) z < 0 then else x ^ z * y ^ z
theorem ENNReal.mul_rpow_of_ne_top {x : ENNReal} {y : ENNReal} (hx : x ) (hy : y ) (z : ) :
(x * y) ^ z = x ^ z * y ^ z
theorem ENNReal.coe_mul_rpow (x : NNReal) (y : NNReal) (z : ) :
(x * y) ^ z = x ^ z * y ^ z
theorem ENNReal.mul_rpow_of_ne_zero {x : ENNReal} {y : ENNReal} (hx : x 0) (hy : y 0) (z : ) :
(x * y) ^ z = x ^ z * y ^ z
theorem ENNReal.mul_rpow_of_nonneg (x : ENNReal) (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 : ENNReal) (y : ENNReal) {z : } (hz : 0 z) :
(x / y) ^ z = x ^ z / y ^ z
theorem ENNReal.strictMono_rpow_of_pos {z : } (h : 0 < z) :
StrictMono fun x => x ^ z
theorem ENNReal.monotone_rpow_of_nonneg {z : } (h : 0 z) :
Monotone fun x => x ^ z
@[simp]
theorem ENNReal.orderIsoRpow_apply (y : ) (hy : 0 < y) (x : ENNReal) :
↑() x = x ^ y
def ENNReal.orderIsoRpow (y : ) (hy : 0 < y) :

Bundles fun x : ℝ≥0∞ => x ^ y into an order isomorphism when y : ℝ is positive, where the inverse is fun x : ℝ≥0∞ => x ^ (1 / y).

Instances For
theorem ENNReal.orderIsoRpow_symm_apply (y : ) (hy : 0 < y) :
= ENNReal.orderIsoRpow (1 / y) (_ : 0 < 1 / y)
theorem ENNReal.rpow_le_rpow {x : ENNReal} {y : ENNReal} {z : } (h₁ : x y) (h₂ : 0 z) :
x ^ z y ^ z
theorem ENNReal.rpow_lt_rpow {x : ENNReal} {y : ENNReal} {z : } (h₁ : x < y) (h₂ : 0 < z) :
x ^ z < y ^ z
theorem ENNReal.rpow_le_rpow_iff {x : ENNReal} {y : ENNReal} {z : } (hz : 0 < z) :
x ^ z y ^ z x y
theorem ENNReal.rpow_lt_rpow_iff {x : ENNReal} {y : ENNReal} {z : } (hz : 0 < z) :
x ^ z < y ^ z x < y
theorem ENNReal.le_rpow_one_div_iff {x : ENNReal} {y : ENNReal} {z : } (hz : 0 < z) :
x y ^ (1 / z) x ^ z y
theorem ENNReal.lt_rpow_one_div_iff {x : ENNReal} {y : ENNReal} {z : } (hz : 0 < z) :
x < y ^ (1 / z) x ^ z < y
theorem ENNReal.rpow_one_div_le_iff {x : ENNReal} {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.ofReal_rpow_of_pos {x : } {p : } (hx_pos : 0 < x) :
theorem ENNReal.ofReal_rpow_of_nonneg {x : } {p : } (hx_nonneg : 0 x) (hp_nonneg : 0 p) :
theorem ENNReal.rpow_left_injective {x : } (hx : x 0) :
Function.Injective fun y => y ^ x
theorem ENNReal.rpow_left_surjective {x : } (hx : x 0) :
Function.Surjective fun y => y ^ x
theorem ENNReal.rpow_left_bijective {x : } (hx : x 0) :
Function.Bijective fun y => y ^ x