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.

noncomputable instance NNReal.instPowReal : Pow NNReal ℝ

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

theorem NNReal.rpow_zero_pos (x : NNReal) : 0 < x ^ 0

@[simp]

theorem NNReal.rpow_eq_zero_iff {x : NNReal} {y : ℝ} : x ^ y = 0 ↔ x = 0 ∧ y ≠ 0

theorem NNReal.rpow_eq_zero {x : NNReal} {y : ℝ} (hy : y ≠ 0) : x ^ y = 0 ↔ x = 0

@[simp]

theorem NNReal.zero_rpow {x : ℝ} (h : x ≠ 0) : 0 ^ x = 0

@[simp]

theorem NNReal.rpow_one (x : NNReal) : x ^ 1 = x

theorem NNReal.rpow_neg (x : NNReal) (y : ℝ) : x ^ (-y) = (x ^ y)⁻¹

@[simp]

theorem NNReal.rpow_natCast (x : NNReal) (n : ℕ) : x ^ ↑n = x ^ n

@[simp]

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

@[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' {y z : ℝ} (h : y + z ≠ 0) (x : NNReal) : x ^ (y + z) = x ^ y * x ^ z

theorem NNReal.rpow_add_intCast {x : NNReal} (hx : x ≠ 0) (y : ℝ) (n : ℤ) : x ^ (y + ↑n) = x ^ y * x ^ n

theorem NNReal.rpow_add_natCast {x : NNReal} (hx : x ≠ 0) (y : ℝ) (n : ℕ) : x ^ (y + ↑n) = x ^ y * x ^ n

theorem NNReal.rpow_sub_intCast {x : NNReal} (hx : x ≠ 0) (y : ℝ) (n : ℕ) : x ^ (y - ↑n) = x ^ y / x ^ n

theorem NNReal.rpow_sub_natCast {x : NNReal} (hx : x ≠ 0) (y : ℝ) (n : ℕ) : x ^ (y - ↑n) = x ^ y / x ^ n

theorem NNReal.rpow_add_intCast' {y : ℝ} {n : ℤ} (h : y + ↑n ≠ 0) (x : NNReal) : x ^ (y + ↑n) = x ^ y * x ^ n

theorem NNReal.rpow_add_natCast' {y : ℝ} {n : ℕ} (h : y + ↑n ≠ 0) (x : NNReal) : x ^ (y + ↑n) = x ^ y * x ^ n

theorem NNReal.rpow_sub_intCast' {y : ℝ} {n : ℤ} (h : y - ↑n ≠ 0) (x : NNReal) : x ^ (y - ↑n) = x ^ y / x ^ n

theorem NNReal.rpow_sub_natCast' {y : ℝ} {n : ℕ} (h : y - ↑n ≠ 0) (x : NNReal) : x ^ (y - ↑n) = x ^ y / x ^ n

theorem NNReal.rpow_add_one {x : NNReal} (hx : x ≠ 0) (y : ℝ) : x ^ (y + 1) = x ^ y * x

theorem NNReal.rpow_sub_one {x : NNReal} (hx : x ≠ 0) (y : ℝ) : x ^ (y - 1) = x ^ y / x

theorem NNReal.rpow_add_one' {y : ℝ} (h : y + 1 ≠ 0) (x : NNReal) : x ^ (y + 1) = x ^ y * x

theorem NNReal.rpow_one_add' {y : ℝ} (h : 1 + y ≠ 0) (x : NNReal) : x ^ (1 + y) = x * x ^ y

theorem NNReal.rpow_add_of_nonneg (x : NNReal) {y z : ℝ} (hy : 0 ≤ y) (hz : 0 ≤ z) : 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_natCast_mul (x : NNReal) (n : ℕ) (z : ℝ) : x ^ (↑n * z) = (x ^ n) ^ z

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

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

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

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' {y z : ℝ} (h : y - z ≠ 0) (x : NNReal) : x ^ (y - z) = x ^ y / x ^ z

theorem NNReal.rpow_sub_one' {y : ℝ} (h : y - 1 ≠ 0) (x : NNReal) : x ^ (y - 1) = x ^ y / x

theorem NNReal.rpow_one_sub' {y : ℝ} (h : 1 - y ≠ 0) (x : NNReal) : x ^ (1 - y) = x / x ^ y

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) : sqrt x = x ^ (1 / 2)

@[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 y : NNReal} {z : ℝ} : (x * y) ^ z = x ^ z * y ^ z

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

rpow as a MonoidHom

@[simp]

theorem NNReal.rpowMonoidHom_apply (r : ℝ) (x✝ : NNReal) : (rpowMonoidHom r) x✝ = x✝ ^ r

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 : ℝ) : ∏ i ∈ s, f i ^ r = (∏ i ∈ s, 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 : ℝ) : ∏ i ∈ s, f i ^ r = (∏ i ∈ s, f i) ^ r

rpow version of Finset.prod_pow.

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_inv_iff {x y : NNReal} {z : ℝ} (hz : 0 < z) : x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y

theorem NNReal.rpow_inv_le_iff {x y : NNReal} {z : ℝ} (hz : 0 < z) : x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z

theorem NNReal.lt_rpow_inv_iff {x y : NNReal} {z : ℝ} (hz : 0 < z) : x < y ^ z⁻¹ ↔ x ^ z < y

theorem NNReal.rpow_inv_lt_iff {x y : NNReal} {z : ℝ} (hz : 0 < z) : x ^ z⁻¹ < y ↔ x < y ^ z

theorem NNReal.rpow_lt_rpow_of_neg {x : NNReal} {z : ℝ} {y : NNReal} (hx : 0 < x) (hxy : x < y) (hz : z < 0) : y ^ z < x ^ z

theorem NNReal.rpow_le_rpow_of_nonpos {x : NNReal} {z : ℝ} {y : NNReal} (hx : 0 < x) (hxy : x ≤ y) (hz : z ≤ 0) : y ^ z ≤ x ^ z

theorem NNReal.rpow_lt_rpow_iff_of_neg {x : NNReal} {z : ℝ} {y : NNReal} (hx : 0 < x) (hy : 0 < y) (hz : z < 0) : x ^ z < y ^ z ↔ y < x

theorem NNReal.rpow_le_rpow_iff_of_neg {x : NNReal} {z : ℝ} {y : NNReal} (hx : 0 < x) (hy : 0 < y) (hz : z < 0) : x ^ z ≤ y ^ z ↔ y ≤ x

theorem NNReal.le_rpow_inv_iff_of_pos {z : ℝ} {y : NNReal} (hy : 0 ≤ y) (hz : 0 < z) (x : NNReal) : x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y

theorem NNReal.rpow_inv_le_iff_of_pos {z : ℝ} {y : NNReal} (hy : 0 ≤ y) (hz : 0 < z) (x : NNReal) : x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z

theorem NNReal.lt_rpow_inv_iff_of_pos {z : ℝ} {y : NNReal} (hy : 0 ≤ y) (hz : 0 < z) (x : NNReal) : x < y ^ z⁻¹ ↔ x ^ z < y

theorem NNReal.rpow_inv_lt_iff_of_pos {z : ℝ} {y : NNReal} (hy : 0 ≤ y) (hz : 0 < z) (x : NNReal) : x ^ z⁻¹ < y ↔ x < y ^ z

theorem NNReal.le_rpow_inv_iff_of_neg {x : NNReal} {z : ℝ} {y : NNReal} (hx : 0 < x) (hy : 0 < y) (hz : z < 0) : x ≤ y ^ z⁻¹ ↔ y ≤ x ^ z

theorem NNReal.lt_rpow_inv_iff_of_neg {x : NNReal} {z : ℝ} {y : NNReal} (hx : 0 < x) (hy : 0 < y) (hz : z < 0) : x < y ^ z⁻¹ ↔ y < x ^ z

theorem NNReal.rpow_inv_lt_iff_of_neg {x : NNReal} {z : ℝ} {y : NNReal} (hx : 0 < x) (hy : 0 < y) (hz : z < 0) : x ^ z⁻¹ < y ↔ y ^ z < x

theorem NNReal.rpow_inv_le_iff_of_neg {x : NNReal} {z : ℝ} {y : NNReal} (hx : 0 < x) (hy : 0 < y) (hz : z < 0) : x ^ z⁻¹ ≤ y ↔ y ^ z ≤ x

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 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_inv_iff {x y : NNReal} {z : ℝ} (hz : z ≠ 0) : x = y ^ z⁻¹ ↔ x ^ z = y

theorem NNReal.rpow_inv_eq_iff {x y : NNReal} {z : ℝ} (hz : z ≠ 0) : x ^ 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

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

@[simp]

theorem NNReal.orderIsoRpow_apply (y : ℝ) (hy : 0 < y) (x : NNReal) : (orderIsoRpow y hy) x = x ^ y

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

theorem Real.nnnorm_rpow_of_nonneg {x y : ℝ} (hx : 0 ≤ x) : ‖x ^ y‖₊ = ‖x‖₊ ^ 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).

noncomputable instance ENNReal.instPowReal : Pow ENNReal ℝ

@[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.rpow_zero_pos (x : ENNReal) : 0 < x ^ 0

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)

theorem ENNReal.rpow_ofNNReal {M : NNReal} {P : ℝ} (hP : 0 ≤ P) : ↑M ^ P = ↑(M ^ P)

@[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_ne_top_of_nonneg' {y : ℝ} {x : ENNReal} (hx : 0 < x) (hx' : x ≠ ⊤) : x ^ y ≠ ⊤

theorem ENNReal.rpow_lt_top_of_nonneg {x : ENNReal} {y : ℝ} (hy0 : 0 ≤ y) (h : x ≠ ⊤) : x ^ y < ⊤

theorem ENNReal.rpow_ne_top_of_ne_zero {x : ENNReal} {y : ℝ} (hx : x ≠ 0) (hx' : 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_add_of_nonneg {x : ENNReal} (y z : ℝ) (hy : 0 ≤ y) (hz : 0 ≤ z) : x ^ (y + z) = x ^ y * x ^ z

theorem ENNReal.rpow_add_of_add_pos {x : ENNReal} (hx : x ≠ ⊤) (y z : ℝ) (hyz : 0 < y + z) : 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 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 y : ENNReal} (hx : x ≠ ⊤) (hy : y ≠ ⊤) (z : ℝ) : (x * y) ^ z = x ^ z * y ^ z

theorem ENNReal.coe_mul_rpow (x y : NNReal) (z : ℝ) : (↑x * ↑y) ^ z = ↑x ^ z * ↑y ^ z

theorem ENNReal.prod_coe_rpow {ι : Type u_1} (s : Finset ι) (f : ι → NNReal) (r : ℝ) : ∏ i ∈ s, ↑(f i) ^ r = ↑(∏ i ∈ s, f i) ^ r

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

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

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

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

@[simp]

theorem ENNReal.orderIsoRpow_apply (y : ℝ) (hy : 0 < y) (x : ENNReal) : (orderIsoRpow y hy) x = x ^ y

theorem ENNReal.orderIsoRpow_symm_apply (y : ℝ) (hy : 0 < y) : (orderIsoRpow y hy).symm = orderIsoRpow (1 / 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.max_rpow {x y : ENNReal} {p : ℝ} (hp : 0 ≤ p) : max x y ^ p = max (x ^ p) (y ^ p)

theorem ENNReal.le_rpow_inv_iff {x y : ENNReal} {z : ℝ} (hz : 0 < z) : x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y

theorem ENNReal.rpow_inv_lt_iff {x y : ENNReal} {z : ℝ} (hz : 0 < z) : x ^ z⁻¹ < y ↔ x < y ^ z

theorem ENNReal.lt_rpow_inv_iff {x y : ENNReal} {z : ℝ} (hz : 0 < z) : x < y ^ z⁻¹ ↔ x ^ z < y

theorem ENNReal.rpow_inv_le_iff {x y : ENNReal} {z : ℝ} (hz : 0 < z) : x ^ 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

@[simp]

theorem ENNReal.toNNReal_rpow (x : ENNReal) (z : ℝ) : (x ^ z).toNNReal = x.toNNReal ^ z

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

theorem Real.enorm_rpow_of_nonneg {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) : ‖x ^ y‖ₑ = ‖x‖ₑ ^ y

theorem ENNReal.add_rpow_le_two_rpow_mul_rpow_add_rpow {p : ℝ} (a b : ENNReal) (hp : 0 ≤ p) : (a + b) ^ p ≤ 2 ^ p * (a ^ p + b ^ p)

Positivity extension

def Mathlib.Meta.Positivity.evalNNRealRpow : PositivityExt

Extension for the positivity tactic: exponentiation by a real number is nonnegative when the base is nonnegative and positive when the base is positive. This is the NNReal analogue of evalRpow for Real.

def Mathlib.Meta.Positivity.evalENNRealRpow : PositivityExt

Extension for the positivity tactic: exponentiation by a real number is nonnegative when the base is nonnegative and positive when the base is positive. This is the ENNReal analogue of evalRpow for Real.

NormNum extension for NNReal powers

theorem Mathlib.Meta.NormNum.IsNat.nnreal_rpow_eq_nnreal_pow {b : ℝ} {n : ℕ} (h : IsNat b n) (a : NNReal) : a ^ b = a ^ n

theorem Mathlib.Meta.NormNum.IsInt.nnreal_rpow_eq_inv_nnreal_pow {b : ℝ} {n : ℕ} (h : IsInt b (Int.negOfNat n)) (a : NNReal) : a ^ b = (a ^ n)⁻¹

theorem Mathlib.Meta.NormNum.IsNat.nnreal_rpow_isNNRat {a : NNReal} {b : ℝ} {m n d r : ℕ} (ha : IsNat a m) (hb : IsNNRat b n d) (k : ℕ) (hr : r ^ d = k) (l : ℕ) (hm : m ^ n = l) (hkl : k = l) : IsNat (a ^ b) r

theorem Mathlib.Meta.NormNum.IsNNRat.nnreal_rpow_isNNRat (a : NNReal) (b : ℝ) (na da : ℕ) (ha : IsNNRat a na da) (nr dr : ℕ) (hnum : IsNat (↑na ^ b) nr) (hden : IsNat (↑da ^ b) dr) : IsNNRat (a ^ b) nr dr

theorem Mathlib.Meta.NormNum.nnreal_rpow_isRat_eq_inv_nnreal_rpow (a : NNReal) (b : ℝ) (n d : ℕ) (hb : IsRat b (Int.negOfNat n) d) : a ^ b = a⁻¹ ^ (↑n / ↑d)

def Mathlib.Meta.NormNum.proveIsNatNNRealRPowIsNNRat (a : Q(NNReal)) (na : Q(ℕ)) (pa : Q(IsNat «$a» «$na»)) (b : Q(ℝ)) (nb db : Q(ℕ)) (pb : Q(IsNNRat «$b» «$nb» «$db»)) : Lean.MetaM (ℕ × (r : Q(ℕ)) × Q(IsNat («$a» ^ «$b») «$r»))

Given proofs

• that a is a natural number na;
• that b is a nonnegative rational number nb / db; returns a tuple of
• a natural number r (result);
• the same number, as an expression;
• a proof that a ^ b = r.

Fails if na is not a dbth power of a natural number.

def Mathlib.Meta.NormNum.evalNNRealRPow : NormNumExt

Evaluates expressions of the form a ^ b when a : ℝ≥0 and b : ℝ. Works if a, b, and a ^ b are in fact rational numbers.