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 : ℝ) : NNReal

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

• NNReal.rpow x y = { val := ↑x ^ y, property := (_ : 0 ≤ ↑x ^ y) }

noncomputable instance NNReal.instPowNNRealReal : Pow NNReal ℝ

Equations

• NNReal.instPowNNRealReal = { pow := NNReal.rpow }

@[simp]

theorem NNReal.rpow_eq_pow (x : NNReal) (y : ℝ) : NNReal.rpow x 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) : ↑NNReal.sqrt x = 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), ↑(NNReal.rpowMonoidHom r) x = x ^ r

def NNReal.rpowMonoidHom (r : ℝ) : NNReal →* NNReal

rpow as a MonoidHom

Equations

• NNReal.rpowMonoidHom r = { toOneHom := { toFun := fun x => x ^ r, map_one' := (_ : 1 ^ r = 1) }, map_mul' := (_ : ∀ (_x _y : NNReal), (_x * _y) ^ r = _x ^ r * _y ^ r) }

theorem NNReal.list_prod_map_rpow (l : List NNReal) (r : ℝ) : List.prod (List.map (fun x => x ^ r) l) = List.prod 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 : Multiset ι) (f : ι → NNReal) (r : ℝ) : Multiset.prod (Multiset.map (fun x => f x ^ r) s) = Multiset.prod (Multiset.map f s) ^ r

rpow version of Multiset.prod_map_pow for ℝ≥0.

theorem NNReal.finset_prod_rpow {ι : Type u_1} (s : Finset ι) (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 : List ℝ) (hl : ∀ (x : ℝ), x ∈ l → 0 ≤ x) (r : ℝ) : List.prod (List.map (fun x => x ^ r) l) = List.prod 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 ∈ l → 0 ≤ 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 : Multiset ι) (f : ι → ℝ) (hs : ∀ (i : ι), i ∈ s → 0 ≤ f i) (r : ℝ) : Multiset.prod (Multiset.map (fun x => f x ^ r) s) = Multiset.prod (Multiset.map f s) ^ r

rpow version of Multiset.prod_map_pow.

theorem Real.finset_prod_rpow {ι : Type u_1} (s : Finset ι) (f : ι → ℝ) (hs : ∀ (i : ι), i ∈ s → 0 ≤ 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) : Real.toNNReal (x ^ y) = Real.toNNReal x ^ y

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) : ↑(NNReal.orderIsoRpow y hy) x = x ^ y

def NNReal.orderIsoRpow (y : ℝ) (hy : 0 < y) : NNReal ≃o NNReal

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

Equations

• One or more equations did not get rendered due to their size.

theorem NNReal.orderIsoRpow_symm_eq (y : ℝ) (hy : 0 < y) : OrderIso.symm (NNReal.orderIsoRpow y hy) = NNReal.orderIsoRpow (1 / y) (_ : 0 < 1 / y)

noncomputable def ENNReal.rpow : ENNReal → ℝ → 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).

Equations

• ENNReal.rpow x x = match x, x with | some x, y => if x = 0 ∧ y < 0 then ⊤ else ↑(x ^ y) | none, y => if 0 < y then ⊤ else if y = 0 then 1 else 0

noncomputable instance ENNReal.instPowENNRealReal : Pow ENNReal ℝ

Equations

• ENNReal.instPowENNRealReal = { pow := ENNReal.rpow }

@[simp]

theorem ENNReal.rpow_eq_pow (x : ENNReal) (y : ℝ) : ENNReal.rpow x 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) : ⊤ ^ 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_neg_one (x : ENNReal) : x ^ (-1) = x⁻¹

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) : ↑(ENNReal.orderIsoRpow y hy) x = x ^ y

def ENNReal.orderIsoRpow (y : ℝ) (hy : 0 < y) : ENNReal ≃o ENNReal

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

Equations

• One or more equations did not get rendered due to their size.

theorem ENNReal.orderIsoRpow_symm_apply (y : ℝ) (hy : 0 < y) : OrderIso.symm (ENNReal.orderIsoRpow y hy) = 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.toNNReal_rpow (x : ENNReal) (z : ℝ) : ENNReal.toNNReal x ^ z = ENNReal.toNNReal (x ^ z)

theorem ENNReal.toReal_rpow (x : ENNReal) (z : ℝ) : ENNReal.toReal x ^ z = ENNReal.toReal (x ^ z)

theorem ENNReal.ofReal_rpow_of_pos {x : ℝ} {p : ℝ} (hx_pos : 0 < x) : ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

theorem ENNReal.ofReal_rpow_of_nonneg {x : ℝ} {p : ℝ} (hx_nonneg : 0 ≤ x) (hp_nonneg : 0 ≤ p) : ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ 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