Documentation

@[implicit_reducible]

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

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

Instances For

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

Instances For

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

Instances For

@[implicit_reducible]

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

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

Instances For

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

Instances For

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.

Instances For

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)