mathlib3 documentation

analysis.special_functions.pow.nnreal

Power function on ℝ≥0 and ℝ≥0∞ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We construct the power functions x ^ y where

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
source
@[protected, instance]
noncomputable def nnreal.real.has_pow  :
has_pow nnreal ℝ
Equations
source
@[simp]
theorem nnreal.rpow_eq_pow (x : nnreal) (y : ℝ) :
x.rpow y = x ^ y
source
@[simp, norm_cast]
theorem nnreal.coe_rpow (x : nnreal) (y : ℝ) :
↑(x ^ y) = ↑x ^ y
source
@[simp]
theorem nnreal.rpow_zero (x : nnreal) :
x ^ 0 = 1
source
@[simp]
theorem nnreal.rpow_eq_zero_iff {x : nnreal} {y : ℝ} :
x ^ y = 0 ↔ x = 0 ∧ y ≠ 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
@[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' (x : nnreal) {y z : ℝ} (h : y + z ≠ 0) :
x ^ (y + z) = x ^ y * x ^ z
source
theorem nnreal.rpow_mul (x : nnreal) (y z : ℝ) :
x ^ (y * z) = (x ^ y) ^ z
source
theorem nnreal.rpow_neg (x : nnreal) (y : ℝ) :
x ^ -y = (x ^ y)⁻¹
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' (x : nnreal) {y z : ℝ} (h : y - z ≠ 0) :
x ^ (y - z) = x ^ y / x ^ z
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) :
⇑nnreal.sqrt x = x ^ (1 / 2)
source
@[simp, norm_cast]
theorem nnreal.rpow_nat_cast (x : nnreal) (n : ℕ) :
x ^ ↑n = x ^ n
source
@[simp]
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
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_one_div_iff {x y : nnreal} {z : ℝ} (hz : 0 < z) :
x ≤ y ^ (1 / z) ↔ x ^ z ≤ y
source
theorem nnreal.rpow_one_div_le_iff {x y : nnreal} {z : ℝ} (hz : 0 < z) :
x ^ (1 / z) ≤ y ↔ x ≤ y ^ z
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 (λ (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 (λ (y : nnreal), y ^ x)
source
theorem nnreal.rpow_left_bijective {x : ℝ} (hx : x ≠ 0) :
function.bijective (λ (y : nnreal), y ^ x)
source
theorem nnreal.eq_rpow_one_div_iff {x y : nnreal} {z : ℝ} (hz : z ≠ 0) :
x = y ^ (1 / z) ↔ x ^ z = y
source
theorem nnreal.rpow_one_div_eq_iff {x y : nnreal} {z : ℝ} (hz : z ≠ 0) :
x ^ (1 / z) = y ↔ x = y ^ z
source
theorem nnreal.pow_nat_rpow_nat_inv (x : nnreal) {n : ℕ} (hn : n ≠ 0) :
(x ^ n) ^ (↑n)⁻¹ = x
source
theorem nnreal.rpow_nat_inv_pow_nat (x : nnreal) {n : ℕ} (hn : n ≠ 0) :
(x ^ (↑n)⁻¹) ^ n = x
source
theorem real.to_nnreal_rpow_of_nonneg {x y : ℝ} (hx : 0 ≤ x) :
(x ^ y).to_nnreal = x.to_nnreal ^ 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
source
@[protected, instance]
noncomputable def ennreal.real.has_pow  :
has_pow ennreal ℝ
Equations
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.top_rpow_def (y : ℝ) :
⊤ ^ y = ite (0 < y) ⊤ (ite (y = 0) 1 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 = ite (0 < y) 0 (ite (y = 0) 1 ⊤)
source
@[simp]
theorem ennreal.zero_rpow_mul_self (y : ℝ) :
0 ^ y * 0 ^ y = 0 ^ y
source
@[norm_cast]
theorem ennreal.coe_rpow_of_ne_zero {x : nnreal} (h : x ≠ 0) (y : ℝ) :
↑x ^ y = ↑(x ^ y)
source
@[norm_cast]
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 = ite (x = 0 ∧ y < 0) ⊤ ↑(x ^ y)
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
@[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_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_lt_top_of_nonneg {x : ennreal} {y : ℝ} (hy0 : 0 ≤ y) (h : 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_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, norm_cast]
theorem ennreal.rpow_nat_cast (x : ennreal) (n : ℕ) :
x ^ ↑n = x ^ n
source
@[simp]
theorem ennreal.rpow_two (x : ennreal) :
x ^ 2 = x ^ 2
source
theorem ennreal.mul_rpow_eq_ite (x y : ennreal) (z : ℝ) :
(x * y) ^ z = ite ((x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0) ∧ z < 0) ⊤ (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
@[norm_cast]
theorem ennreal.coe_mul_rpow (x y : nnreal) (z : ℝ) :
(↑x * ↑y) ^ z = ↑x ^ z * ↑y ^ z
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.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.strict_mono_rpow_of_pos {z : ℝ} (h : 0 < z) :
strict_mono (λ (x : ennreal), x ^ z)
source
theorem ennreal.monotone_rpow_of_nonneg {z : ℝ} (h : 0 ≤ z) :
monotone (λ (x : ennreal), x ^ z)
source
noncomputable def ennreal.order_iso_rpow (y : ℝ) (hy : 0 < y) :
ennreal ≃o ennreal

Bundles λ x : ℝ≥0∞, x ^ y into an order isomorphism when y : ℝ is positive, where the inverse is λ x : ℝ≥0∞, x ^ (1 / y).

Equations
source
@[simp]
theorem ennreal.order_iso_rpow_apply (y : ℝ) (hy : 0 < y) (x : ennreal) :
⇑(ennreal.order_iso_rpow y hy) x = x ^ y
source
theorem ennreal.order_iso_rpow_symm_apply (y : ℝ) (hy : 0 < y) :
(ennreal.order_iso_rpow y hy).symm = ennreal.order_iso_rpow (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.le_rpow_one_div_iff {x y : ennreal} {z : ℝ} (hz : 0 < z) :
x ≤ y ^ (1 / z) ↔ x ^ z ≤ y
source
theorem ennreal.lt_rpow_one_div_iff {x y : ennreal} {z : ℝ} (hz : 0 < z) :
x < y ^ (1 / z) ↔ x ^ z < y
source
theorem ennreal.rpow_one_div_le_iff {x y : ennreal} {z : ℝ} (hz : 0 < z) :
x ^ (1 / 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
theorem ennreal.to_nnreal_rpow (x : ennreal) (z : ℝ) :
x.to_nnreal ^ z = (x ^ z).to_nnreal
source
theorem ennreal.to_real_rpow (x : ennreal) (z : ℝ) :
x.to_real ^ z = (x ^ z).to_real
source
theorem ennreal.of_real_rpow_of_pos {x p : ℝ} (hx_pos : 0 < x) :
ennreal.of_real x ^ p = ennreal.of_real (x ^ p)
source
theorem ennreal.of_real_rpow_of_nonneg {x p : ℝ} (hx_nonneg : 0 ≤ x) (hp_nonneg : 0 ≤ p) :
ennreal.of_real x ^ p = ennreal.of_real (x ^ p)
source
theorem ennreal.rpow_left_injective {x : ℝ} (hx : x ≠ 0) :
function.injective (λ (y : ennreal), y ^ x)
source
theorem ennreal.rpow_left_surjective {x : ℝ} (hx : x ≠ 0) :
function.surjective (λ (y : ennreal), y ^ x)
source
theorem ennreal.rpow_left_bijective {x : ℝ} (hx : x ≠ 0) :
function.bijective (λ (y : ennreal), y ^ x)

Tactic extensions for powers on ℝ≥0 and ℝ≥0∞ #

source
theorem norm_num.nnrpow_pos (a : nnreal) (b : ℝ) (b' : ℕ) (c : nnreal) (hb : b = ↑b') (h : a ^ b' = c) :
a ^ b = c
source
theorem norm_num.nnrpow_neg (a : nnreal) (b : ℝ) (b' : ℕ) (c c' : nnreal) (hb : b = ↑b') (h : a ^ b' = c) (hc : c⁻¹ = c') :
a ^ -b = c'
source
theorem norm_num.ennrpow_pos (a : ennreal) (b : ℝ) (b' : ℕ) (c : ennreal) (hb : b = ↑b') (h : a ^ b' = c) :
a ^ b = c
source
theorem norm_num.ennrpow_neg (a : ennreal) (b : ℝ) (b' : ℕ) (c c' : ennreal) (hb : b = ↑b') (h : a ^ b' = c) (hc : c⁻¹ = c') :
a ^ -b = c'
source
meta def norm_num.prove_nnrpow  :
expr → expr → tactic (expr × expr)

Evaluate nnreal.rpow a b where a is a rational numeral and b is an integer.

source
meta def norm_num.prove_ennrpow  :
expr → expr → tactic (expr × expr)

Evaluate ennreal.rpow a b where a is a rational numeral and b is an integer.

source
meta def norm_num.eval_nnrpow_ennrpow  :
expr → tactic (expr × expr)

Evaluates expressions of the form rpow a b and a ^ b in the special case where b is an integer and a is a positive rational (so it's really just a rational power).

source
meta def tactic.positivity.prove_nnrpow (a b : expr) :
tactic tactic.positivity.strictness

Auxiliary definition for the positivity tactic to handle real powers of nonnegative reals.

source
meta def tactic.positivity.prove_ennrpow (a b : expr) :
tactic tactic.positivity.strictness

Auxiliary definition for the positivity tactic to handle real powers of extended nonnegative reals.

source
meta def tactic.positivity_nnrpow_ennrpow  :
expr → tactic tactic.positivity.strictness

Extension for the positivity tactic: exponentiation by a real number is nonnegative when the base is nonnegative and positive when the base is positive.