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, ⋯⟩

@[implicit_reducible]

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

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

theorem NNReal.zero_rpow_def (y : ℝ) : 0 ^ y = if y = 0 then 1 else 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

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

rpow as a MonoidHom

Equations

• NNReal.rpowMonoidHom r = { toFun := fun (x : NNReal) => x ^ r, map_one' := ⋯, map_mul' := ⋯ }

@[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.rpow_right_inj {x : NNReal} {y z : ℝ} (hx₀ : x ≠ 0) (hx₁ : x ≠ 1) : x ^ y = x ^ z ↔ y = z

theorem NNReal.rpow_eq_rpow_right_iff {x : NNReal} {y z : ℝ} : x ^ y = x ^ z ↔ y = z ∨ x = 1 ∨ x = 0 ∧ (y = 0 ↔ z = 0)

@[simp]

theorem NNReal.rpow_eq_left_iff {x : NNReal} {y : ℝ} : x ^ y = x ↔ x = 1 ∨ y = 1 ∨ x = 0 ∧ y ≠ 0

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

@[simp]

theorem NNReal.rpow_rpow_inv_eq_iff {x : NNReal} {y : ℝ} : (x ^ y) ^ y⁻¹ = x ↔ y ≠ 0 ∨ x = 1

@[simp]

theorem NNReal.rpow_inv_rpow_eq_iff {x : NNReal} {y : ℝ} : (x ^ y⁻¹) ^ y = x ↔ y ≠ 0 ∨ x = 1

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

noncomputable 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)) ⋯

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

Equations

• ENNReal.rpow (some x_2) x✝ = if x_2 = 0 ∧ x✝ < 0 then ⊤ else ↑(x_2 ^ x✝)
• ENNReal.rpow none x✝ = if 0 < x✝ then ⊤ else if x✝ = 0 then 1 else 0

@[implicit_reducible]

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

noncomputable 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)) ⋯

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

@[simp]

theorem ENNReal.rpow_rpow_inv_eq_iff {x : ENNReal} {y : ℝ} : (x ^ y) ^ y⁻¹ = x ↔ y ≠ 0 ∨ x = 1

@[simp]

theorem ENNReal.rpow_inv_rpow_eq_iff {x : ENNReal} {y : ℝ} : (x ^ y⁻¹) ^ y = x ↔ y ≠ 0 ∨ x = 1

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.

Equations

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

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.

Equations

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

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.

Equations

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