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

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

Instances For

source
noncomputable instance NNReal.instPowReal :
Pow NNReal ℝ
Equations

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

source
@[simp]
theorem NNReal.rpow_eq_pow (x : NNReal) (y : ℝ) :
x.rpow y = x ^ y
source
@[simp]
theorem NNReal.coe_rpow (x : NNReal) (y : ℝ) :
↑(x ^ y) = ↑x ^ y
source
@[simp]
theorem NNReal.rpow_zero (x : NNReal) :
x ^ 0 = 1
source
theorem NNReal.rpow_zero_pos (x : NNReal) :
0 < x ^ 0
source
@[simp]
theorem NNReal.rpow_eq_zero_iff {x : NNReal} {y : ℝ} :
x ^ y = 0 ↔ x = 0 ∧ y ≠ 0
source
theorem NNReal.rpow_eq_zero {x : NNReal} {y : ℝ} (hy : y ≠ 0) :
x ^ y = 0 ↔ x = 0
source
@[simp]
theorem NNReal.zero_rpow {x : ℝ} (h : x ≠ 0) :
0 ^ x = 0
source
@[simp]
theorem NNReal.rpow_one (x : NNReal) :
x ^ 1 = x
source
theorem NNReal.rpow_neg (x : NNReal) (y : ℝ) :
x ^ (-y) = (x ^ y)⁻¹
source
@[simp]
theorem NNReal.rpow_natCast (x : NNReal) (n : ℕ) :
x ^ ↑n = x ^ n
source
@[simp]
theorem NNReal.rpow_intCast (x : NNReal) (n : ℤ) :
x ^ ↑n = x ^ n
source
@[simp]
theorem NNReal.one_rpow (x : ℝ) :
1 ^ x = 1
source
theorem NNReal.rpow_add {x : NNReal} (hx : x ≠ 0) (y z : ℝ) :
x ^ (y + z) = x ^ y * x ^ z
source
theorem NNReal.rpow_add' {y z : ℝ} (h : y + z ≠ 0) (x : NNReal) :
x ^ (y + z) = x ^ y * x ^ z
source
theorem NNReal.rpow_add_intCast {x : NNReal} (hx : x ≠ 0) (y : ℝ) (n : ℤ) :
x ^ (y + ↑n) = x ^ y * x ^ n
source
theorem NNReal.rpow_add_natCast {x : NNReal} (hx : x ≠ 0) (y : ℝ) (n : ℕ) :
x ^ (y + ↑n) = x ^ y * x ^ n
source
theorem NNReal.rpow_sub_intCast {x : NNReal} (hx : x ≠ 0) (y : ℝ) (n : ℕ) :
x ^ (y - ↑n) = x ^ y / x ^ n
source
theorem NNReal.rpow_sub_natCast {x : NNReal} (hx : x ≠ 0) (y : ℝ) (n : ℕ) :
x ^ (y - ↑n) = x ^ y / x ^ n
source
theorem NNReal.rpow_add_intCast' {y : ℝ} {n : ℤ} (h : y + ↑n ≠ 0) (x : NNReal) :
x ^ (y + ↑n) = x ^ y * x ^ n
source
theorem NNReal.rpow_add_natCast' {y : ℝ} {n : ℕ} (h : y + ↑n ≠ 0) (x : NNReal) :
x ^ (y + ↑n) = x ^ y * x ^ n
source
theorem NNReal.rpow_sub_intCast' {y : ℝ} {n : ℤ} (h : y - ↑n ≠ 0) (x : NNReal) :
x ^ (y - ↑n) = x ^ y / x ^ n
source
theorem NNReal.rpow_sub_natCast' {y : ℝ} {n : ℕ} (h : y - ↑n ≠ 0) (x : NNReal) :
x ^ (y - ↑n) = x ^ y / x ^ n
source
theorem NNReal.rpow_add_one {x : NNReal} (hx : x ≠ 0) (y : ℝ) :
x ^ (y + 1) = x ^ y * x
source
theorem NNReal.rpow_sub_one {x : NNReal} (hx : x ≠ 0) (y : ℝ) :
x ^ (y - 1) = x ^ y / x
source
theorem NNReal.rpow_add_one' {y : ℝ} (h : y + 1 ≠ 0) (x : NNReal) :
x ^ (y + 1) = x ^ y * x
source
theorem NNReal.rpow_one_add' {y : ℝ} (h : 1 + y ≠ 0) (x : NNReal) :
x ^ (1 + y) = x * x ^ y
source
theorem NNReal.rpow_add_of_nonneg (x : NNReal) {y z : ℝ} (hy : 0 ≤ y) (hz : 0 ≤ z) :
x ^ (y + z) = x ^ y * x ^ z
source
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.

source
theorem NNReal.rpow_mul (x : NNReal) (y z : ℝ) :
x ^ (y * z) = (x ^ y) ^ z
source
theorem NNReal.rpow_natCast_mul (x : NNReal) (n : ℕ) (z : ℝ) :
x ^ (↑n * z) = (x ^ n) ^ z
source
theorem NNReal.rpow_mul_natCast (x : NNReal) (y : ℝ) (n : ℕ) :
x ^ (y * ↑n) = (x ^ y) ^ n
source
theorem NNReal.rpow_intCast_mul (x : NNReal) (n : ℤ) (z : ℝ) :
x ^ (↑n * z) = (x ^ n) ^ z
source
theorem NNReal.rpow_mul_intCast (x : NNReal) (y : ℝ) (n : ℤ) :
x ^ (y * ↑n) = (x ^ y) ^ n
source
theorem NNReal.rpow_neg_one (x : NNReal) :
x ^ (-1) = x⁻¹
source
theorem NNReal.rpow_sub {x : NNReal} (hx : x ≠ 0) (y z : ℝ) :
x ^ (y - z) = x ^ y / x ^ z
source
theorem NNReal.rpow_sub' {y z : ℝ} (h : y - z ≠ 0) (x : NNReal) :
x ^ (y - z) = x ^ y / x ^ z
source
theorem NNReal.rpow_sub_one' {y : ℝ} (h : y - 1 ≠ 0) (x : NNReal) :
x ^ (y - 1) = x ^ y / x
source
theorem NNReal.rpow_one_sub' {y : ℝ} (h : 1 - y ≠ 0) (x : NNReal) :
x ^ (1 - y) = x / x ^ y
source
theorem NNReal.rpow_inv_rpow_self {y : ℝ} (hy : y ≠ 0) (x : NNReal) :
(x ^ y) ^ (1 / y) = x
source
theorem NNReal.rpow_self_rpow_inv {y : ℝ} (hy : y ≠ 0) (x : NNReal) :
(x ^ (1 / y)) ^ y = x
source
theorem NNReal.inv_rpow (x : NNReal) (y : ℝ) :
x⁻¹ ^ y = (x ^ y)⁻¹
source
theorem NNReal.div_rpow (x y : NNReal) (z : ℝ) :
(x / y) ^ z = x ^ z / y ^ z
source
theorem NNReal.sqrt_eq_rpow (x : NNReal) :
sqrt x = x ^ (1 / 2)
source
@[simp]
theorem NNReal.rpow_ofNat (x : NNReal) (n : ℕ) [n.AtLeastTwo] :
x ^ OfNat.ofNat n = x ^ OfNat.ofNat n
source
theorem NNReal.rpow_two (x : NNReal) :
x ^ 2 = x ^ 2
source
theorem NNReal.mul_rpow {x y : NNReal} {z : ℝ} :
(x * y) ^ z = x ^ z * y ^ z
source
def NNReal.rpowMonoidHom (r : ℝ) :
NNReal →* NNReal

`rpow` as a `MonoidHom`

Equations

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

Instances For

source
@[simp]
theorem NNReal.rpowMonoidHom_apply (r : ℝ) (x✝ : NNReal) :
(rpowMonoidHom r) x✝ = x✝ ^ r
source
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`

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

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

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

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

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

source
theorem NNReal.rpow_le_rpow {x y : NNReal} {z : ℝ} (h₁ : x ≤ y) (h₂ : 0 ≤ z) :
x ^ z ≤ y ^ z
source
theorem NNReal.rpow_lt_rpow {x y : NNReal} {z : ℝ} (h₁ : x < y) (h₂ : 0 < z) :
x ^ z < y ^ z
source
theorem NNReal.rpow_lt_rpow_iff {x y : NNReal} {z : ℝ} (hz : 0 < z) :
x ^ z < y ^ z ↔ x < y
source
theorem NNReal.rpow_le_rpow_iff {x y : NNReal} {z : ℝ} (hz : 0 < z) :
x ^ z ≤ y ^ z ↔ x ≤ y
source
theorem NNReal.le_rpow_inv_iff {x y : NNReal} {z : ℝ} (hz : 0 < z) :
x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y
source
theorem NNReal.rpow_inv_le_iff {x y : NNReal} {z : ℝ} (hz : 0 < z) :
x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z
source
theorem NNReal.lt_rpow_inv_iff {x y : NNReal} {z : ℝ} (hz : 0 < z) :
x < y ^ z⁻¹ ↔ x ^ z < y
source
theorem NNReal.rpow_inv_lt_iff {x y : NNReal} {z : ℝ} (hz : 0 < z) :
x ^ z⁻¹ < y ↔ x < y ^ z
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
theorem NNReal.rpow_lt_rpow_of_exponent_lt {x : NNReal} {y z : ℝ} (hx : 1 < x) (hyz : y < z) :
x ^ y < x ^ z
source
theorem NNReal.rpow_le_rpow_of_exponent_le {x : NNReal} {y z : ℝ} (hx : 1 ≤ x) (hyz : y ≤ z) :
x ^ y ≤ x ^ z
source
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
source
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
source
theorem NNReal.rpow_pos {p : ℝ} {x : NNReal} (hx_pos : 0 < x) :
0 < x ^ p
source
theorem NNReal.rpow_lt_one {x : NNReal} {z : ℝ} (hx1 : x < 1) (hz : 0 < z) :
x ^ z < 1
source
theorem NNReal.rpow_le_one {x : NNReal} {z : ℝ} (hx2 : x ≤ 1) (hz : 0 ≤ z) :
x ^ z ≤ 1
source
theorem NNReal.rpow_lt_one_of_one_lt_of_neg {x : NNReal} {z : ℝ} (hx : 1 < x) (hz : z < 0) :
x ^ z < 1
source
theorem NNReal.rpow_le_one_of_one_le_of_nonpos {x : NNReal} {z : ℝ} (hx : 1 ≤ x) (hz : z ≤ 0) :
x ^ z ≤ 1
source
theorem NNReal.one_lt_rpow {x : NNReal} {z : ℝ} (hx : 1 < x) (hz : 0 < z) :
1 < x ^ z
source
theorem NNReal.one_le_rpow {x : NNReal} {z : ℝ} (h : 1 ≤ x) (h₁ : 0 ≤ z) :
1 ≤ x ^ z
source
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
source
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
source
theorem NNReal.rpow_le_self_of_le_one {x : NNReal} {z : ℝ} (hx : x ≤ 1) (h_one_le : 1 ≤ z) :
x ^ z ≤ x
source
theorem NNReal.rpow_left_injective {x : ℝ} (hx : x ≠ 0) :
Function.Injective fun (y : NNReal) => y ^ x
source
theorem NNReal.rpow_eq_rpow_iff {x y : NNReal} {z : ℝ} (hz : z ≠ 0) :
x ^ z = y ^ z ↔ x = y
source
theorem NNReal.rpow_left_surjective {x : ℝ} (hx : x ≠ 0) :
Function.Surjective fun (y : NNReal) => y ^ x
source
theorem NNReal.rpow_left_bijective {x : ℝ} (hx : x ≠ 0) :
Function.Bijective fun (y : NNReal) => y ^ x
source
theorem NNReal.eq_rpow_inv_iff {x y : NNReal} {z : ℝ} (hz : z ≠ 0) :
x = y ^ z⁻¹ ↔ x ^ z = y
source
theorem NNReal.rpow_inv_eq_iff {x y : NNReal} {z : ℝ} (hz : z ≠ 0) :
x ^ z⁻¹ = y ↔ x = y ^ z
source
@[simp]
theorem NNReal.rpow_rpow_inv {y : ℝ} (hy : y ≠ 0) (x : NNReal) :
(x ^ y) ^ y⁻¹ = x
source
@[simp]
theorem NNReal.rpow_inv_rpow {y : ℝ} (hy : y ≠ 0) (x : NNReal) :
(x ^ y⁻¹) ^ y = x
source
theorem NNReal.pow_rpow_inv_natCast (x : NNReal) {n : ℕ} (hn : n ≠ 0) :
(x ^ n) ^ (↑n)⁻¹ = x
source
theorem NNReal.rpow_inv_natCast_pow (x : NNReal) {n : ℕ} (hn : n ≠ 0) :
(x ^ (↑n)⁻¹) ^ n = x
source
theorem Real.toNNReal_rpow_of_nonneg {x y : ℝ} (hx : 0 ≤ x) :
(x ^ y).toNNReal = x.toNNReal ^ y
source
theorem NNReal.strictMono_rpow_of_pos {z : ℝ} (h : 0 < z) :
StrictMono fun (x : NNReal) => x ^ z
source
theorem NNReal.monotone_rpow_of_nonneg {z : ℝ} (h : 0 ≤ z) :
Monotone fun (x : NNReal) => x ^ z
source
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)) ⋯

Instances For

source
@[simp]
theorem NNReal.orderIsoRpow_apply (y : ℝ) (hy : 0 < y) (x : NNReal) :
(orderIsoRpow y hy) x = x ^ y
source
theorem NNReal.orderIsoRpow_symm_eq (y : ℝ) (hy : 0 < y) :
(orderIsoRpow y hy).symm = orderIsoRpow (1 / y) ⋯
source
theorem Real.nnnorm_rpow_of_nonneg {x y : ℝ} (hx : 0 ≤ x) :
‖x ^ y‖₊ = ‖x‖₊ ^ y
source
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

Instances For

source
noncomputable instance ENNReal.instPowReal :
Pow ENNReal ℝ
Equations

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

source
@[simp]
theorem ENNReal.rpow_eq_pow (x : ENNReal) (y : ℝ) :
x.rpow y = x ^ y
source
@[simp]
theorem ENNReal.rpow_zero {x : ENNReal} :
x ^ 0 = 1
source
theorem ENNReal.rpow_zero_pos (x : ENNReal) :
0 < x ^ 0
source
theorem ENNReal.top_rpow_def (y : ℝ) :
⊤ ^ y = if 0 < y then ⊤ else if y = 0 then 1 else 0
source
@[simp]
theorem ENNReal.top_rpow_of_pos {y : ℝ} (h : 0 < y) :
⊤ ^ y = ⊤
source
@[simp]
theorem ENNReal.top_rpow_of_neg {y : ℝ} (h : y < 0) :
⊤ ^ y = 0
source
@[simp]
theorem ENNReal.zero_rpow_of_pos {y : ℝ} (h : 0 < y) :
0 ^ y = 0
source
@[simp]
theorem ENNReal.zero_rpow_of_neg {y : ℝ} (h : y < 0) :
0 ^ y = ⊤
source
theorem ENNReal.zero_rpow_def (y : ℝ) :
0 ^ y = if 0 < y then 0 else if y = 0 then 1 else ⊤
source
@[simp]
theorem ENNReal.zero_rpow_mul_self (y : ℝ) :
0 ^ y * 0 ^ y = 0 ^ y
source
theorem ENNReal.coe_rpow_of_ne_zero {x : NNReal} (h : x ≠ 0) (y : ℝ) :
↑(x ^ y) = ↑x ^ y
source
theorem ENNReal.coe_rpow_of_nonneg (x : NNReal) {y : ℝ} (h : 0 ≤ y) :
↑(x ^ y) = ↑x ^ y
source
theorem ENNReal.coe_rpow_def (x : NNReal) (y : ℝ) :
↑x ^ y = if x = 0 ∧ y < 0 then ⊤ else ↑(x ^ y)
source
theorem ENNReal.rpow_ofNNReal {M : NNReal} {P : ℝ} (hP : 0 ≤ P) :
↑M ^ P = ↑(M ^ P)
source
@[simp]
theorem ENNReal.rpow_one (x : ENNReal) :
x ^ 1 = x
source
@[simp]
theorem ENNReal.one_rpow (x : ℝ) :
1 ^ x = 1
source
@[simp]
theorem ENNReal.rpow_eq_zero_iff {x : ENNReal} {y : ℝ} :
x ^ y = 0 ↔ x = 0 ∧ 0 < y ∨ x = ⊤ ∧ y < 0
source
theorem ENNReal.rpow_eq_zero_iff_of_pos {x : ENNReal} {y : ℝ} (hy : 0 < y) :
x ^ y = 0 ↔ x = 0
source
@[simp]
theorem ENNReal.rpow_eq_top_iff {x : ENNReal} {y : ℝ} :
x ^ y = ⊤ ↔ x = 0 ∧ y < 0 ∨ x = ⊤ ∧ 0 < y
source
theorem ENNReal.rpow_eq_top_iff_of_pos {x : ENNReal} {y : ℝ} (hy : 0 < y) :
x ^ y = ⊤ ↔ x = ⊤
source
theorem ENNReal.rpow_lt_top_iff_of_pos {x : ENNReal} {y : ℝ} (hy : 0 < y) :
x ^ y < ⊤ ↔ x < ⊤
source
theorem ENNReal.rpow_eq_top_of_nonneg (x : ENNReal) {y : ℝ} (hy0 : 0 ≤ y) :
x ^ y = ⊤ → x = ⊤
source
theorem ENNReal.rpow_ne_top_of_nonneg {x : ENNReal} {y : ℝ} (hy0 : 0 ≤ y) (h : x ≠ ⊤) :
x ^ y ≠ ⊤
source
theorem ENNReal.rpow_ne_top_of_nonneg' {y : ℝ} {x : ENNReal} (hx : 0 < x) (hx' : x ≠ ⊤) :
x ^ y ≠ ⊤
source
theorem ENNReal.rpow_lt_top_of_nonneg {x : ENNReal} {y : ℝ} (hy0 : 0 ≤ y) (h : x ≠ ⊤) :
x ^ y < ⊤
source
theorem ENNReal.rpow_ne_top_of_ne_zero {x : ENNReal} {y : ℝ} (hx : x ≠ 0) (hx' : x ≠ ⊤) :
x ^ y ≠ ⊤
source
theorem ENNReal.rpow_add {x : ENNReal} (y z : ℝ) (hx : x ≠ 0) (h'x : x ≠ ⊤) :
x ^ (y + z) = x ^ y * x ^ z
source
theorem ENNReal.rpow_add_of_nonneg {x : ENNReal} (y z : ℝ) (hy : 0 ≤ y) (hz : 0 ≤ z) :
x ^ (y + z) = x ^ y * x ^ z
source
theorem ENNReal.rpow_add_of_add_pos {x : ENNReal} (hx : x ≠ ⊤) (y z : ℝ) (hyz : 0 < y + z) :
x ^ (y + z) = x ^ y * x ^ z
source
theorem ENNReal.rpow_neg (x : ENNReal) (y : ℝ) :
x ^ (-y) = (x ^ y)⁻¹
source
theorem ENNReal.rpow_sub {x : ENNReal} (y z : ℝ) (hx : x ≠ 0) (h'x : x ≠ ⊤) :
x ^ (y - z) = x ^ y / x ^ z
source
theorem ENNReal.rpow_neg_one (x : ENNReal) :
x ^ (-1) = x⁻¹
source
theorem ENNReal.rpow_mul (x : ENNReal) (y z : ℝ) :
x ^ (y * z) = (x ^ y) ^ z
source
@[simp]
theorem ENNReal.rpow_natCast (x : ENNReal) (n : ℕ) :
x ^ ↑n = x ^ n
source
@[simp]
theorem ENNReal.rpow_ofNat (x : ENNReal) (n : ℕ) [n.AtLeastTwo] :
x ^ OfNat.ofNat n = x ^ OfNat.ofNat n
source
@[simp]
theorem ENNReal.rpow_intCast (x : ENNReal) (n : ℤ) :
x ^ ↑n = x ^ n
source
theorem ENNReal.rpow_two (x : ENNReal) :
x ^ 2 = x ^ 2
source
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
source
theorem ENNReal.mul_rpow_of_ne_top {x y : ENNReal} (hx : x ≠ ⊤) (hy : y ≠ ⊤) (z : ℝ) :
(x * y) ^ z = x ^ z * y ^ z
source
theorem ENNReal.coe_mul_rpow (x y : NNReal) (z : ℝ) :
(↑x * ↑y) ^ z = ↑x ^ z * ↑y ^ z
source
theorem ENNReal.prod_coe_rpow {ι : Type u_1} (s : Finset ι) (f : ι → NNReal) (r : ℝ) :
∏ i ∈ s, ↑(f i) ^ r = ↑(∏ i ∈ s, f i) ^ r
source
theorem ENNReal.mul_rpow_of_ne_zero {x y : ENNReal} (hx : x ≠ 0) (hy : y ≠ 0) (z : ℝ) :
(x * y) ^ z = x ^ z * y ^ z
source
theorem ENNReal.mul_rpow_of_nonneg (x y : ENNReal) {z : ℝ} (hz : 0 ≤ z) :
(x * y) ^ z = x ^ z * y ^ z
source
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
source
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
source
theorem ENNReal.inv_rpow (x : ENNReal) (y : ℝ) :
x⁻¹ ^ y = (x ^ y)⁻¹
source
theorem ENNReal.div_rpow_of_nonneg (x y : ENNReal) {z : ℝ} (hz : 0 ≤ z) :
(x / y) ^ z = x ^ z / y ^ z
source
theorem ENNReal.strictMono_rpow_of_pos {z : ℝ} (h : 0 < z) :
StrictMono fun (x : ENNReal) => x ^ z
source
theorem ENNReal.monotone_rpow_of_nonneg {z : ℝ} (h : 0 ≤ z) :
Monotone fun (x : ENNReal) => x ^ z
source
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)) ⋯

Instances For

source
@[simp]
theorem ENNReal.orderIsoRpow_apply (y : ℝ) (hy : 0 < y) (x : ENNReal) :
(orderIsoRpow y hy) x = x ^ y
source
theorem ENNReal.orderIsoRpow_symm_apply (y : ℝ) (hy : 0 < y) :
(orderIsoRpow y hy).symm = orderIsoRpow (1 / y) ⋯
source
theorem ENNReal.rpow_le_rpow {x y : ENNReal} {z : ℝ} (h₁ : x ≤ y) (h₂ : 0 ≤ z) :
x ^ z ≤ y ^ z
source
theorem ENNReal.rpow_lt_rpow {x y : ENNReal} {z : ℝ} (h₁ : x < y) (h₂ : 0 < z) :
x ^ z < y ^ z
source
theorem ENNReal.rpow_le_rpow_iff {x y : ENNReal} {z : ℝ} (hz : 0 < z) :
x ^ z ≤ y ^ z ↔ x ≤ y
source
theorem ENNReal.rpow_lt_rpow_iff {x y : ENNReal} {z : ℝ} (hz : 0 < z) :
x ^ z < y ^ z ↔ x < y
source
theorem ENNReal.max_rpow {x y : ENNReal} {p : ℝ} (hp : 0 ≤ p) :
max x y ^ p = max (x ^ p) (y ^ p)
source
theorem ENNReal.le_rpow_inv_iff {x y : ENNReal} {z : ℝ} (hz : 0 < z) :
x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y
source
theorem ENNReal.rpow_inv_lt_iff {x y : ENNReal} {z : ℝ} (hz : 0 < z) :
x ^ z⁻¹ < y ↔ x < y ^ z
source
theorem ENNReal.lt_rpow_inv_iff {x y : ENNReal} {z : ℝ} (hz : 0 < z) :
x < y ^ z⁻¹ ↔ x ^ z < y
source
theorem ENNReal.rpow_inv_le_iff {x y : ENNReal} {z : ℝ} (hz : 0 < z) :
x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z
source
theorem ENNReal.rpow_lt_rpow_of_exponent_lt {x : ENNReal} {y z : ℝ} (hx : 1 < x) (hx' : x ≠ ⊤) (hyz : y < z) :
x ^ y < x ^ z
source
theorem ENNReal.rpow_le_rpow_of_exponent_le {x : ENNReal} {y z : ℝ} (hx : 1 ≤ x) (hyz : y ≤ z) :
x ^ y ≤ x ^ z
source
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
source
theorem ENNReal.rpow_le_rpow_of_exponent_ge {x : ENNReal} {y z : ℝ} (hx1 : x ≤ 1) (hyz : z ≤ y) :
x ^ y ≤ x ^ z
source
theorem ENNReal.rpow_le_self_of_le_one {x : ENNReal} {z : ℝ} (hx : x ≤ 1) (h_one_le : 1 ≤ z) :
x ^ z ≤ x
source
theorem ENNReal.le_rpow_self_of_one_le {x : ENNReal} {z : ℝ} (hx : 1 ≤ x) (h_one_le : 1 ≤ z) :
x ≤ x ^ z
source
theorem ENNReal.rpow_pos_of_nonneg {p : ℝ} {x : ENNReal} (hx_pos : 0 < x) (hp_nonneg : 0 ≤ p) :
0 < x ^ p
source
theorem ENNReal.rpow_pos {p : ℝ} {x : ENNReal} (hx_pos : 0 < x) (hx_ne_top : x ≠ ⊤) :
0 < x ^ p
source
theorem ENNReal.rpow_lt_one {x : ENNReal} {z : ℝ} (hx : x < 1) (hz : 0 < z) :
x ^ z < 1
source
theorem ENNReal.rpow_le_one {x : ENNReal} {z : ℝ} (hx : x ≤ 1) (hz : 0 ≤ z) :
x ^ z ≤ 1
source
theorem ENNReal.rpow_lt_one_of_one_lt_of_neg {x : ENNReal} {z : ℝ} (hx : 1 < x) (hz : z < 0) :
x ^ z < 1
source
theorem ENNReal.rpow_le_one_of_one_le_of_neg {x : ENNReal} {z : ℝ} (hx : 1 ≤ x) (hz : z < 0) :
x ^ z ≤ 1
source
theorem ENNReal.one_lt_rpow {x : ENNReal} {z : ℝ} (hx : 1 < x) (hz : 0 < z) :
1 < x ^ z
source
theorem ENNReal.one_le_rpow {x : ENNReal} {z : ℝ} (hx : 1 ≤ x) (hz : 0 < z) :
1 ≤ x ^ z
source
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
source
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
source
@[simp]
theorem ENNReal.toNNReal_rpow (x : ENNReal) (z : ℝ) :
(x ^ z).toNNReal = x.toNNReal ^ z
source
theorem ENNReal.toReal_rpow (x : ENNReal) (z : ℝ) :
x.toReal ^ z = (x ^ z).toReal
source
theorem ENNReal.ofReal_rpow_of_pos {x p : ℝ} (hx_pos : 0 < x) :
ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
source
theorem ENNReal.ofReal_rpow_of_nonneg {x p : ℝ} (hx_nonneg : 0 ≤ x) (hp_nonneg : 0 ≤ p) :
ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
source
@[simp]
theorem ENNReal.rpow_rpow_inv {y : ℝ} (hy : y ≠ 0) (x : ENNReal) :
(x ^ y) ^ y⁻¹ = x
source
@[simp]
theorem ENNReal.rpow_inv_rpow {y : ℝ} (hy : y ≠ 0) (x : ENNReal) :
(x ^ y⁻¹) ^ y = x
source
theorem ENNReal.pow_rpow_inv_natCast {n : ℕ} (hn : n ≠ 0) (x : ENNReal) :
(x ^ n) ^ (↑n)⁻¹ = x
source
theorem ENNReal.rpow_inv_natCast_pow {n : ℕ} (hn : n ≠ 0) (x : ENNReal) :
(x ^ (↑n)⁻¹) ^ n = x
source
theorem ENNReal.rpow_natCast_mul (x : ENNReal) (n : ℕ) (z : ℝ) :
x ^ (↑n * z) = (x ^ n) ^ z
source
theorem ENNReal.rpow_mul_natCast (x : ENNReal) (y : ℝ) (n : ℕ) :
x ^ (y * ↑n) = (x ^ y) ^ n
source
theorem ENNReal.rpow_intCast_mul (x : ENNReal) (n : ℤ) (z : ℝ) :
x ^ (↑n * z) = (x ^ n) ^ z
source
theorem ENNReal.rpow_mul_intCast (x : ENNReal) (y : ℝ) (n : ℤ) :
x ^ (y * ↑n) = (x ^ y) ^ n
source
theorem ENNReal.rpow_left_injective {x : ℝ} (hx : x ≠ 0) :
Function.Injective fun (y : ENNReal) => y ^ x
source
theorem ENNReal.rpow_left_surjective {x : ℝ} (hx : x ≠ 0) :
Function.Surjective fun (y : ENNReal) => y ^ x
source
theorem ENNReal.rpow_left_bijective {x : ℝ} (hx : x ≠ 0) :
Function.Bijective fun (y : ENNReal) => y ^ x
source
theorem Real.enorm_rpow_of_nonneg {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) :
‖x ^ y‖ₑ = ‖x‖ₑ ^ y
source
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 #

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

Instances For

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

Instances For