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

• x.rpow y = ⟨↑x ^ y, ⋯⟩

noncomputable instance NNReal.instPowReal : Pow NNReal ℝ

Equations

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

@[simp]

theorem NNReal.rpow_eq_pow (x : NNReal) (y : ℝ) : x.rpow 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_of_add_eq {w : ℝ} {y : ℝ} {z : ℝ} (x : NNReal) (hw : w ≠ 0) (h : y + z = w) : x ^ w = x ^ y * x ^ z

Variant of NNReal.rpow_add' that avoids having to prove y + z = w twice.

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_natCast (x : NNReal) (n : ℕ) : x ^ ↑n = x ^ n

@[simp]

theorem NNReal.rpow_ofNat (x : NNReal) (n : ℕ) [n.AtLeastTwo] : x ^ OfNat.ofNat n = x ^ OfNat.ofNat n

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 = { toFun := fun (x : NNReal) => x ^ r, map_one' := ⋯, map_mul' := ⋯ }

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

theorem NNReal.multiset_prod_map_rpow {ι : Type u_1} (s : Multiset ι) (f : ι → NNReal) (r : ℝ) : (Multiset.map (fun (x : ι) => f x ^ r) s).prod = (Multiset.map f s).prod ^ r

rpow version of Multiset.prod_map_pow for ℝ≥0.

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

rpow version of Finset.prod_pow for ℝ≥0.

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

rpow version of List.prod_map_pow for Real.

theorem Real.list_prod_map_rpow' {ι : Type u_1} (l : List ι) (f : ι → ℝ) (hl : ∀ i ∈ l, 0 ≤ f i) (r : ℝ) : (List.map (fun (x : ι) => f x ^ r) l).prod = (List.map f l).prod ^ r

theorem Real.multiset_prod_map_rpow {ι : Type u_1} (s : Multiset ι) (f : ι → ℝ) (hs : ∀ i ∈ s, 0 ≤ f i) (r : ℝ) : (Multiset.map (fun (x : ι) => f x ^ r) s).prod = (Multiset.map f s).prod ^ r

rpow version of Multiset.prod_map_pow.

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

theorem NNReal.rpow_left_bijective {x : ℝ} (hx : x ≠ 0) : Function.Bijective fun (y : NNReal) => 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

@[simp]

theorem NNReal.rpow_rpow_inv {y : ℝ} (hy : y ≠ 0) (x : NNReal) : (x ^ y) ^ y⁻¹ = x

@[simp]

theorem NNReal.rpow_inv_rpow {y : ℝ} (hy : y ≠ 0) (x : NNReal) : (x ^ y⁻¹) ^ y = x

theorem NNReal.pow_rpow_inv_natCast (x : NNReal) {n : ℕ} (hn : n ≠ 0) : (x ^ n) ^ (↑n)⁻¹ = x

theorem NNReal.rpow_inv_natCast_pow (x : NNReal) {n : ℕ} (hn : n ≠ 0) : (x ^ (↑n)⁻¹) ^ n = x

theorem Real.toNNReal_rpow_of_nonneg {x : ℝ} {y : ℝ} (hx : 0 ≤ x) : (x ^ y).toNNReal = x.toNNReal ^ y

theorem NNReal.strictMono_rpow_of_pos {z : ℝ} (h : 0 < z) : StrictMono fun (x : NNReal) => x ^ z

theorem NNReal.monotone_rpow_of_nonneg {z : ℝ} (h : 0 ≤ z) : Monotone fun (x : NNReal) => 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

• NNReal.orderIsoRpow y hy = StrictMono.orderIsoOfRightInverse (fun (x : NNReal) => x ^ y) ⋯ (fun (x : NNReal) => x ^ (1 / y)) ⋯

theorem NNReal.orderIsoRpow_symm_eq (y : ℝ) (hy : 0 < y) : (NNReal.orderIsoRpow y hy).symm = NNReal.orderIsoRpow (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

• x✝.rpow 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.instPowReal : Pow ENNReal ℝ

Equations

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

@[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 = 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

theorem ENNReal.rpow_eq_zero_iff_of_pos {x : ENNReal} {y : ℝ} (hy : 0 < y) : x ^ y = 0 ↔ x = 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_lt_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_natCast (x : ENNReal) (n : ℕ) : x ^ ↑n = x ^ n

@[simp]

theorem ENNReal.rpow_ofNat (x : ENNReal) (n : ℕ) [n.AtLeastTwo] : x ^ OfNat.ofNat n = x ^ OfNat.ofNat n

@[simp]

theorem ENNReal.rpow_intCast (x : ENNReal) (n : ℤ) : x ^ ↑n = x ^ n

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.prod_coe_rpow {ι : Type u_1} (s : Finset ι) (f : ι → NNReal) (r : ℝ) : (s.prod fun (i : ι) => ↑(f i) ^ r) = ↑(s.prod fun (i : ι) => f i) ^ r

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.prod_rpow_of_ne_top {ι : Type u_1} {s : Finset ι} {f : ι → ENNReal} (hf : ∀ i ∈ s, f i ≠ ⊤) (r : ℝ) : (s.prod fun (i : ι) => f i ^ r) = (s.prod fun (i : ι) => f i) ^ r

theorem ENNReal.prod_rpow_of_nonneg {ι : Type u_1} {s : Finset ι} {f : ι → ENNReal} {r : ℝ} (hr : 0 ≤ r) : (s.prod fun (i : ι) => f i ^ r) = (s.prod fun (i : ι) => f i) ^ r

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 : ENNReal) => x ^ z

theorem ENNReal.monotone_rpow_of_nonneg {z : ℝ} (h : 0 ≤ z) : Monotone fun (x : ENNReal) => 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

• ENNReal.orderIsoRpow y hy = StrictMono.orderIsoOfRightInverse (fun (x : ENNReal) => x ^ y) ⋯ (fun (x : ENNReal) => x ^ (1 / y)) ⋯

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

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

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)

@[simp]

theorem ENNReal.rpow_rpow_inv {y : ℝ} (hy : y ≠ 0) (x : ENNReal) : (x ^ y) ^ y⁻¹ = x

@[simp]

theorem ENNReal.rpow_inv_rpow {y : ℝ} (hy : y ≠ 0) (x : ENNReal) : (x ^ y⁻¹) ^ y = x

theorem ENNReal.pow_rpow_inv_natCast {n : ℕ} (hn : n ≠ 0) (x : ENNReal) : (x ^ n) ^ (↑n)⁻¹ = x

theorem ENNReal.rpow_inv_natCast_pow {n : ℕ} (hn : n ≠ 0) (x : ENNReal) : (x ^ (↑n)⁻¹) ^ n = x

theorem ENNReal.rpow_natCast_mul (x : ENNReal) (n : ℕ) (z : ℝ) : x ^ (↑n * z) = (x ^ n) ^ z

theorem ENNReal.rpow_mul_natCast (x : ENNReal) (y : ℝ) (n : ℕ) : x ^ (y * ↑n) = (x ^ y) ^ n

theorem ENNReal.rpow_intCast_mul (x : ENNReal) (n : ℤ) (z : ℝ) : x ^ (↑n * z) = (x ^ n) ^ z

theorem ENNReal.rpow_mul_intCast (x : ENNReal) (y : ℝ) (n : ℤ) : x ^ (y * ↑n) = (x ^ y) ^ n

theorem ENNReal.rpow_left_injective {x : ℝ} (hx : x ≠ 0) : Function.Injective fun (y : ENNReal) => y ^ x

theorem ENNReal.rpow_left_surjective {x : ℝ} (hx : x ≠ 0) : Function.Surjective fun (y : ENNReal) => y ^ x

theorem ENNReal.rpow_left_bijective {x : ℝ} (hx : x ≠ 0) : Function.Bijective fun (y : ENNReal) => y ^ x