Power function on ℝ

We construct the power functions x ^ y, where x and y are real numbers.

noncomputable def Real.rpow (x y : ℝ) : ℝ

The real power function x ^ y, defined as the real part of the complex 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. For x < 0, the definition is somewhat arbitrary as it depends on the choice of a complex determination of the logarithm. With our conventions, it is equal to exp (y log x) cos (π y).

Equations

• x.rpow y = (↑x ^ ↑y).re

noncomputable instance Real.instPow : Pow ℝ ℝ

Equations

• Real.instPow = { pow := Real.rpow }

@[simp]

theorem Real.rpow_eq_pow (x y : ℝ) : x.rpow y = x ^ y

theorem Real.rpow_def (x y : ℝ) : x ^ y = (↑x ^ ↑y).re

theorem Real.rpow_def_of_nonneg {x : ℝ} (hx : 0 ≤ x) (y : ℝ) : x ^ y = if x = 0 then if y = 0 then 1 else 0 else Real.exp (Real.log x * y)

theorem Real.rpow_def_of_pos {x : ℝ} (hx : 0 < x) (y : ℝ) : x ^ y = Real.exp (Real.log x * y)

theorem Real.exp_mul (x y : ℝ) : Real.exp (x * y) = Real.exp x ^ y

@[simp]

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

@[deprecated Real.rpow_intCast]

theorem Real.rpow_int_cast (x : ℝ) (n : ℤ) : x ^ ↑n = x ^ n

Alias of Real.rpow_intCast.

@[simp]

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

@[deprecated Real.rpow_natCast]

theorem Real.rpow_nat_cast (x : ℝ) (n : ℕ) : x ^ ↑n = x ^ n

Alias of Real.rpow_natCast.

@[simp]

theorem Real.exp_one_rpow (x : ℝ) : Real.exp 1 ^ x = Real.exp x

@[simp]

theorem Real.exp_one_pow (n : ℕ) : Real.exp 1 ^ n = Real.exp ↑n

theorem Real.rpow_eq_zero_iff_of_nonneg {x y : ℝ} (hx : 0 ≤ x) : x ^ y = 0 ↔ x = 0 ∧ y ≠ 0

@[simp]

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

@[simp]

theorem Real.rpow_ne_zero {x y : ℝ} (hx : 0 ≤ x) (hy : y ≠ 0) : x ^ y ≠ 0 ↔ x ≠ 0

theorem Real.rpow_def_of_neg {x : ℝ} (hx : x < 0) (y : ℝ) : x ^ y = Real.exp (Real.log x * y) * Real.cos (y * Real.pi)

theorem Real.rpow_def_of_nonpos {x : ℝ} (hx : x ≤ 0) (y : ℝ) : x ^ y = if x = 0 then if y = 0 then 1 else 0 else Real.exp (Real.log x * y) * Real.cos (y * Real.pi)

theorem Real.rpow_pos_of_pos {x : ℝ} (hx : 0 < x) (y : ℝ) : 0 < x ^ y

@[simp]

theorem Real.rpow_zero (x : ℝ) : x ^ 0 = 1

theorem Real.rpow_zero_pos (x : ℝ) : 0 < x ^ 0

@[simp]

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

theorem Real.zero_rpow_eq_iff {x a : ℝ} : 0 ^ x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

theorem Real.eq_zero_rpow_iff {x a : ℝ} : a = 0 ^ x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

@[simp]

theorem Real.rpow_one (x : ℝ) : x ^ 1 = x

@[simp]

theorem Real.one_rpow (x : ℝ) : 1 ^ x = 1

theorem Real.zero_rpow_le_one (x : ℝ) : 0 ^ x ≤ 1

theorem Real.zero_rpow_nonneg (x : ℝ) : 0 ≤ 0 ^ x

theorem Real.rpow_nonneg {x : ℝ} (hx : 0 ≤ x) (y : ℝ) : 0 ≤ x ^ y

theorem Real.abs_rpow_of_nonneg {x y : ℝ} (hx_nonneg : 0 ≤ x) : |x ^ y| = |x| ^ y

theorem Real.abs_rpow_le_abs_rpow (x y : ℝ) : |x ^ y| ≤ |x| ^ y

theorem Real.abs_rpow_le_exp_log_mul (x y : ℝ) : |x ^ y| ≤ Real.exp (Real.log x * y)

theorem Real.rpow_inv_log {x : ℝ} (hx₀ : 0 < x) (hx₁ : x ≠ 1) : x ^ (Real.log x)⁻¹ = Real.exp 1

theorem Real.rpow_inv_log_le_exp_one {x : ℝ} : x ^ (Real.log x)⁻¹ ≤ Real.exp 1

See Real.rpow_inv_log for the equality when x ≠ 1 is strictly positive.

theorem Real.norm_rpow_of_nonneg {x y : ℝ} (hx_nonneg : 0 ≤ x) : ‖x ^ y‖ = ‖x‖ ^ y

theorem Real.rpow_add {x : ℝ} (hx : 0 < x) (y z : ℝ) : x ^ (y + z) = x ^ y * x ^ z

theorem Real.rpow_add' {x y z : ℝ} (hx : 0 ≤ x) (h : y + z ≠ 0) : x ^ (y + z) = x ^ y * x ^ z

theorem Real.rpow_of_add_eq {w x y z : ℝ} (hx : 0 ≤ x) (hw : w ≠ 0) (h : y + z = w) : x ^ w = x ^ y * x ^ z

Variant of Real.rpow_add' that avoids having to prove y + z = w twice.

theorem Real.rpow_add_of_nonneg {x y z : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : 0 ≤ z) : x ^ (y + z) = x ^ y * x ^ z

theorem Real.le_rpow_add {x : ℝ} (hx : 0 ≤ x) (y z : ℝ) : x ^ y * x ^ z ≤ x ^ (y + z)

For 0 ≤ x, the only problematic case in the equality x ^ y * x ^ z = x ^ (y + z) is for x = 0 and y + z = 0, where the right hand side is 1 while the left hand side can vanish. The inequality is always true, though, and given in this lemma.

theorem Real.rpow_sum_of_pos {ι : Type u_1} {a : ℝ} (ha : 0 < a) (f : ι → ℝ) (s : Finset ι) : a ^ ∑ x ∈ s, f x = ∏ x ∈ s, a ^ f x

theorem Real.rpow_sum_of_nonneg {ι : Type u_1} {a : ℝ} (ha : 0 ≤ a) {s : Finset ι} {f : ι → ℝ} (h : ∀ x ∈ s, 0 ≤ f x) : a ^ ∑ x ∈ s, f x = ∏ x ∈ s, a ^ f x

theorem Real.rpow_neg {x : ℝ} (hx : 0 ≤ x) (y : ℝ) : x ^ (-y) = (x ^ y)⁻¹

theorem Real.rpow_sub {x : ℝ} (hx : 0 < x) (y z : ℝ) : x ^ (y - z) = x ^ y / x ^ z

theorem Real.rpow_sub' {x : ℝ} (hx : 0 ≤ x) {y z : ℝ} (h : y - z ≠ 0) : x ^ (y - z) = x ^ y / x ^ z

theorem HasCompactSupport.rpow_const {α : Type u_1} [TopologicalSpace α] {f : α → ℝ} (hf : HasCompactSupport f) {r : ℝ} (hr : r ≠ 0) : HasCompactSupport fun (x : α) => f x ^ r

Comparing real and complex powers

theorem Complex.ofReal_cpow {x : ℝ} (hx : 0 ≤ x) (y : ℝ) : ↑(x ^ y) = ↑x ^ ↑y

theorem Complex.ofReal_cpow_of_nonpos {x : ℝ} (hx : x ≤ 0) (y : ℂ) : ↑x ^ y = (-↑x) ^ y * Complex.exp (↑Real.pi * Complex.I * y)

theorem Complex.cpow_ofReal (x : ℂ) (y : ℝ) : x ^ ↑y = ↑(Complex.abs x ^ y) * (↑(Real.cos (x.arg * y)) + ↑(Real.sin (x.arg * y)) * Complex.I)

theorem Complex.cpow_ofReal_re (x : ℂ) (y : ℝ) : (x ^ ↑y).re = Complex.abs x ^ y * Real.cos (x.arg * y)

theorem Complex.cpow_ofReal_im (x : ℂ) (y : ℝ) : (x ^ ↑y).im = Complex.abs x ^ y * Real.sin (x.arg * y)

theorem Complex.abs_cpow_of_ne_zero {z : ℂ} (hz : z ≠ 0) (w : ℂ) : Complex.abs (z ^ w) = Complex.abs z ^ w.re / Real.exp (z.arg * w.im)

theorem Complex.abs_cpow_of_imp {z w : ℂ} (h : z = 0 → w.re = 0 → w = 0) : Complex.abs (z ^ w) = Complex.abs z ^ w.re / Real.exp (z.arg * w.im)

theorem Complex.abs_cpow_le (z w : ℂ) : Complex.abs (z ^ w) ≤ Complex.abs z ^ w.re / Real.exp (z.arg * w.im)

@[simp]

theorem Complex.abs_cpow_real (x : ℂ) (y : ℝ) : Complex.abs (x ^ ↑y) = Complex.abs x ^ y

@[simp]

theorem Complex.abs_cpow_inv_nat (x : ℂ) (n : ℕ) : Complex.abs (x ^ (↑n)⁻¹) = Complex.abs x ^ (↑n)⁻¹

theorem Complex.abs_cpow_eq_rpow_re_of_pos {x : ℝ} (hx : 0 < x) (y : ℂ) : Complex.abs (↑x ^ y) = x ^ y.re

theorem Complex.abs_cpow_eq_rpow_re_of_nonneg {x : ℝ} (hx : 0 ≤ x) {y : ℂ} (hy : y.re ≠ 0) : Complex.abs (↑x ^ y) = x ^ y.re

theorem Complex.norm_natCast_cpow_of_re_ne_zero (n : ℕ) {s : ℂ} (hs : s.re ≠ 0) : ‖↑n ^ s‖ = ↑n ^ s.re

theorem Complex.norm_natCast_cpow_of_pos {n : ℕ} (hn : 0 < n) (s : ℂ) : ‖↑n ^ s‖ = ↑n ^ s.re

theorem Complex.norm_natCast_cpow_pos_of_pos {n : ℕ} (hn : 0 < n) (s : ℂ) : 0 < ‖↑n ^ s‖

theorem Complex.cpow_mul_ofReal_nonneg {x : ℝ} (hx : 0 ≤ x) (y : ℝ) (z : ℂ) : ↑x ^ (↑y * z) = ↑(x ^ y) ^ z

Positivity extension

def Mathlib.Meta.Positivity.evalRpowZero : Mathlib.Meta.Positivity.PositivityExt

Extension for the positivity tactic: exponentiation by a real number is positive (namely 1) when the exponent is zero. The other cases are done in evalRpow.

def Mathlib.Meta.Positivity.evalRpow : Mathlib.Meta.Positivity.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.

Further algebraic properties of rpow

theorem Real.rpow_mul {x : ℝ} (hx : 0 ≤ x) (y z : ℝ) : x ^ (y * z) = (x ^ y) ^ z

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

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

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

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

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

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

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

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

@[deprecated Real.rpow_add_intCast]

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

Alias of Real.rpow_add_intCast.

@[deprecated Real.rpow_add_natCast]

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

Alias of Real.rpow_add_natCast.

@[deprecated Real.rpow_sub_intCast]

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

Alias of Real.rpow_sub_intCast.

@[deprecated Real.rpow_sub_natCast]

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

Alias of Real.rpow_sub_natCast.

@[deprecated Real.rpow_add_intCast']

theorem Real.rpow_add_int' {x y : ℝ} (hx : 0 ≤ x) {n : ℤ} (h : y + ↑n ≠ 0) : x ^ (y + ↑n) = x ^ y * x ^ n

Alias of Real.rpow_add_intCast'.

@[deprecated Real.rpow_add_natCast']

theorem Real.rpow_add_nat' {x y : ℝ} {n : ℕ} (hx : 0 ≤ x) (h : y + ↑n ≠ 0) : x ^ (y + ↑n) = x ^ y * x ^ n

Alias of Real.rpow_add_natCast'.

@[deprecated Real.rpow_sub_intCast']

theorem Real.rpow_sub_int' {x y : ℝ} (hx : 0 ≤ x) {n : ℤ} (h : y - ↑n ≠ 0) : x ^ (y - ↑n) = x ^ y / x ^ n

Alias of Real.rpow_sub_intCast'.

@[deprecated Real.rpow_sub_natCast']

theorem Real.rpow_sub_nat' {x y : ℝ} {n : ℕ} (hx : 0 ≤ x) (h : y - ↑n ≠ 0) : x ^ (y - ↑n) = x ^ y / x ^ n

Alias of Real.rpow_sub_natCast'.

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

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

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

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

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

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

@[simp]

theorem Real.rpow_two (x : ℝ) : x ^ 2 = x ^ 2

theorem Real.rpow_neg_one (x : ℝ) : x ^ (-1) = x⁻¹

theorem Real.mul_rpow {x y z : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) : (x * y) ^ z = x ^ z * y ^ z

theorem Real.inv_rpow {x : ℝ} (hx : 0 ≤ x) (y : ℝ) : x⁻¹ ^ y = (x ^ y)⁻¹

theorem Real.div_rpow {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (z : ℝ) : (x / y) ^ z = x ^ z / y ^ z

theorem Real.log_rpow {x : ℝ} (hx : 0 < x) (y : ℝ) : Real.log (x ^ y) = y * Real.log x

theorem Real.mul_log_eq_log_iff {x y z : ℝ} (hx : 0 < x) (hz : 0 < z) : y * Real.log x = Real.log z ↔ x ^ y = z

@[simp]

theorem Real.rpow_rpow_inv {x y : ℝ} (hx : 0 ≤ x) (hy : y ≠ 0) : (x ^ y) ^ y⁻¹ = x

@[simp]

theorem Real.rpow_inv_rpow {x y : ℝ} (hx : 0 ≤ x) (hy : y ≠ 0) : (x ^ y⁻¹) ^ y = x

theorem Real.pow_rpow_inv_natCast {x : ℝ} {n : ℕ} (hx : 0 ≤ x) (hn : n ≠ 0) : (x ^ n) ^ (↑n)⁻¹ = x

theorem Real.rpow_inv_natCast_pow {x : ℝ} {n : ℕ} (hx : 0 ≤ x) (hn : n ≠ 0) : (x ^ (↑n)⁻¹) ^ n = x

theorem Real.rpow_natCast_mul {x : ℝ} (hx : 0 ≤ x) (n : ℕ) (z : ℝ) : x ^ (↑n * z) = (x ^ n) ^ z

theorem Real.rpow_mul_natCast {x : ℝ} (hx : 0 ≤ x) (y : ℝ) (n : ℕ) : x ^ (y * ↑n) = (x ^ y) ^ n

theorem Real.rpow_intCast_mul {x : ℝ} (hx : 0 ≤ x) (n : ℤ) (z : ℝ) : x ^ (↑n * z) = (x ^ n) ^ z

theorem Real.rpow_mul_intCast {x : ℝ} (hx : 0 ≤ x) (y : ℝ) (n : ℤ) : x ^ (y * ↑n) = (x ^ y) ^ n

Note: lemmas about (∏ i ∈ s, f i ^ r) such as Real.finset_prod_rpow are proved in Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean instead.

Order and monotonicity

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

theorem Real.strictMonoOn_rpow_Ici_of_exponent_pos {r : ℝ} (hr : 0 < r) : StrictMonoOn (fun (x : ℝ) => x ^ r) (Set.Ici 0)

theorem Real.rpow_le_rpow {x y z : ℝ} (h : 0 ≤ x) (h₁ : x ≤ y) (h₂ : 0 ≤ z) : x ^ z ≤ y ^ z

theorem Real.monotoneOn_rpow_Ici_of_exponent_nonneg {r : ℝ} (hr : 0 ≤ r) : MonotoneOn (fun (x : ℝ) => x ^ r) (Set.Ici 0)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Real.rpow_lt_rpow_of_exponent_lt {x y z : ℝ} (hx : 1 < x) (hyz : y < z) : x ^ y < x ^ z

theorem Real.rpow_le_rpow_of_exponent_le {x y z : ℝ} (hx : 1 ≤ x) (hyz : y ≤ z) : x ^ y ≤ x ^ z

theorem Real.rpow_lt_rpow_of_exponent_neg {x y z : ℝ} (hy : 0 < y) (hxy : y < x) (hz : z < 0) : x ^ z < y ^ z

theorem Real.strictAntiOn_rpow_Ioi_of_exponent_neg {r : ℝ} (hr : r < 0) : StrictAntiOn (fun (x : ℝ) => x ^ r) (Set.Ioi 0)

theorem Real.rpow_le_rpow_of_exponent_nonpos {z x y : ℝ} (hy : 0 < y) (hxy : y ≤ x) (hz : z ≤ 0) : x ^ z ≤ y ^ z

theorem Real.antitoneOn_rpow_Ioi_of_exponent_nonpos {r : ℝ} (hr : r ≤ 0) : AntitoneOn (fun (x : ℝ) => x ^ r) (Set.Ioi 0)

@[simp]

theorem Real.rpow_le_rpow_left_iff {x y z : ℝ} (hx : 1 < x) : x ^ y ≤ x ^ z ↔ y ≤ z

@[simp]

theorem Real.rpow_lt_rpow_left_iff {x y z : ℝ} (hx : 1 < x) : x ^ y < x ^ z ↔ y < z

theorem Real.rpow_lt_rpow_of_exponent_gt {x y z : ℝ} (hx0 : 0 < x) (hx1 : x < 1) (hyz : z < y) : x ^ y < x ^ z

theorem Real.rpow_le_rpow_of_exponent_ge {x y z : ℝ} (hx0 : 0 < x) (hx1 : x ≤ 1) (hyz : z ≤ y) : x ^ y ≤ x ^ z

@[simp]

theorem Real.rpow_le_rpow_left_iff_of_base_lt_one {x y z : ℝ} (hx0 : 0 < x) (hx1 : x < 1) : x ^ y ≤ x ^ z ↔ z ≤ y

@[simp]

theorem Real.rpow_lt_rpow_left_iff_of_base_lt_one {x y z : ℝ} (hx0 : 0 < x) (hx1 : x < 1) : x ^ y < x ^ z ↔ z < y

theorem Real.rpow_lt_one {x z : ℝ} (hx1 : 0 ≤ x) (hx2 : x < 1) (hz : 0 < z) : x ^ z < 1

theorem Real.rpow_le_one {x z : ℝ} (hx1 : 0 ≤ x) (hx2 : x ≤ 1) (hz : 0 ≤ z) : x ^ z ≤ 1

theorem Real.rpow_lt_one_of_one_lt_of_neg {x z : ℝ} (hx : 1 < x) (hz : z < 0) : x ^ z < 1

theorem Real.rpow_le_one_of_one_le_of_nonpos {x z : ℝ} (hx : 1 ≤ x) (hz : z ≤ 0) : x ^ z ≤ 1

theorem Real.one_lt_rpow {x z : ℝ} (hx : 1 < x) (hz : 0 < z) : 1 < x ^ z

theorem Real.one_le_rpow {x z : ℝ} (hx : 1 ≤ x) (hz : 0 ≤ z) : 1 ≤ x ^ z

theorem Real.one_lt_rpow_of_pos_of_lt_one_of_neg {x z : ℝ} (hx1 : 0 < x) (hx2 : x < 1) (hz : z < 0) : 1 < x ^ z

theorem Real.one_le_rpow_of_pos_of_le_one_of_nonpos {x z : ℝ} (hx1 : 0 < x) (hx2 : x ≤ 1) (hz : z ≤ 0) : 1 ≤ x ^ z

theorem Real.rpow_lt_one_iff_of_pos {x y : ℝ} (hx : 0 < x) : x ^ y < 1 ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y

theorem Real.rpow_lt_one_iff {x y : ℝ} (hx : 0 ≤ x) : x ^ y < 1 ↔ x = 0 ∧ y ≠ 0 ∨ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y

theorem Real.rpow_lt_one_iff' {x y : ℝ} (hx : 0 ≤ x) (hy : 0 < y) : x ^ y < 1 ↔ x < 1

theorem Real.one_lt_rpow_iff_of_pos {x y : ℝ} (hx : 0 < x) : 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ x < 1 ∧ y < 0

theorem Real.one_lt_rpow_iff {x y : ℝ} (hx : 0 ≤ x) : 1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ 0 < x ∧ x < 1 ∧ y < 0

theorem Real.rpow_le_rpow_of_exponent_ge_of_imp {x y z : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) (hyz : z ≤ y) (h : x = 0 → y = 0 → z = 0) : x ^ y ≤ x ^ z

This is a more general but less convenient version of rpow_le_rpow_of_exponent_ge. This version allows x = 0, so it explicitly forbids x = y = 0, z ≠ 0.

theorem Real.rpow_le_rpow_of_exponent_ge' {x y z : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) (hz : 0 ≤ z) (hyz : z ≤ y) : x ^ y ≤ x ^ z

This version of rpow_le_rpow_of_exponent_ge allows x = 0 but requires 0 ≤ z. See also rpow_le_rpow_of_exponent_ge_of_imp for the most general version.

theorem Real.self_le_rpow_of_le_one {x y : ℝ} (h₁ : 0 ≤ x) (h₂ : x ≤ 1) (h₃ : y ≤ 1) : x ≤ x ^ y

theorem Real.self_le_rpow_of_one_le {x y : ℝ} (h₁ : 1 ≤ x) (h₂ : 1 ≤ y) : x ≤ x ^ y

theorem Real.rpow_le_self_of_le_one {x y : ℝ} (h₁ : 0 ≤ x) (h₂ : x ≤ 1) (h₃ : 1 ≤ y) : x ^ y ≤ x

theorem Real.rpow_le_self_of_one_le {x y : ℝ} (h₁ : 1 ≤ x) (h₂ : y ≤ 1) : x ^ y ≤ x

theorem Real.self_lt_rpow_of_lt_one {x y : ℝ} (h₁ : 0 < x) (h₂ : x < 1) (h₃ : y < 1) : x < x ^ y

theorem Real.self_lt_rpow_of_one_lt {x y : ℝ} (h₁ : 1 < x) (h₂ : 1 < y) : x < x ^ y

theorem Real.rpow_lt_self_of_lt_one {x y : ℝ} (h₁ : 0 < x) (h₂ : x < 1) (h₃ : 1 < y) : x ^ y < x

theorem Real.rpow_lt_self_of_one_lt {x y : ℝ} (h₁ : 1 < x) (h₂ : y < 1) : x ^ y < x

theorem Real.rpow_left_injOn {x : ℝ} (hx : x ≠ 0) : Set.InjOn (fun (y : ℝ) => y ^ x) {y : ℝ | 0 ≤ y}

theorem Real.rpow_left_inj {x y z : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : z ≠ 0) : x ^ z = y ^ z ↔ x = y

theorem Real.rpow_inv_eq {x y z : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : z ≠ 0) : x ^ z⁻¹ = y ↔ x = y ^ z

theorem Real.eq_rpow_inv {x y z : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : z ≠ 0) : x = y ^ z⁻¹ ↔ x ^ z = y

theorem Real.le_rpow_iff_log_le {x y z : ℝ} (hx : 0 < x) (hy : 0 < y) : x ≤ y ^ z ↔ Real.log x ≤ z * Real.log y

theorem Real.le_pow_iff_log_le {x y : ℝ} {n : ℕ} (hx : 0 < x) (hy : 0 < y) : x ≤ y ^ n ↔ Real.log x ≤ ↑n * Real.log y

theorem Real.le_zpow_iff_log_le {x y : ℝ} {n : ℤ} (hx : 0 < x) (hy : 0 < y) : x ≤ y ^ n ↔ Real.log x ≤ ↑n * Real.log y

theorem Real.le_rpow_of_log_le {x y z : ℝ} (hy : 0 < y) (h : Real.log x ≤ z * Real.log y) : x ≤ y ^ z

theorem Real.le_pow_of_log_le {x y : ℝ} {n : ℕ} (hy : 0 < y) (h : Real.log x ≤ ↑n * Real.log y) : x ≤ y ^ n

theorem Real.le_zpow_of_log_le {x y : ℝ} {n : ℤ} (hy : 0 < y) (h : Real.log x ≤ ↑n * Real.log y) : x ≤ y ^ n

theorem Real.lt_rpow_iff_log_lt {x y z : ℝ} (hx : 0 < x) (hy : 0 < y) : x < y ^ z ↔ Real.log x < z * Real.log y

theorem Real.lt_pow_iff_log_lt {x y : ℝ} {n : ℕ} (hx : 0 < x) (hy : 0 < y) : x < y ^ n ↔ Real.log x < ↑n * Real.log y

theorem Real.lt_zpow_iff_log_lt {x y : ℝ} {n : ℤ} (hx : 0 < x) (hy : 0 < y) : x < y ^ n ↔ Real.log x < ↑n * Real.log y

theorem Real.lt_rpow_of_log_lt {x y z : ℝ} (hy : 0 < y) (h : Real.log x < z * Real.log y) : x < y ^ z

theorem Real.lt_pow_of_log_lt {x y : ℝ} {n : ℕ} (hy : 0 < y) (h : Real.log x < ↑n * Real.log y) : x < y ^ n

theorem Real.lt_zpow_of_log_lt {x y : ℝ} {n : ℤ} (hy : 0 < y) (h : Real.log x < ↑n * Real.log y) : x < y ^ n

theorem Real.rpow_le_iff_le_log {x y z : ℝ} (hx : 0 < x) (hy : 0 < y) : x ^ z ≤ y ↔ z * Real.log x ≤ Real.log y

theorem Real.pow_le_iff_le_log {x y : ℝ} {n : ℕ} (hx : 0 < x) (hy : 0 < y) : x ^ n ≤ y ↔ ↑n * Real.log x ≤ Real.log y

theorem Real.zpow_le_iff_le_log {x y : ℝ} {n : ℤ} (hx : 0 < x) (hy : 0 < y) : x ^ n ≤ y ↔ ↑n * Real.log x ≤ Real.log y

theorem Real.le_log_of_rpow_le {x y z : ℝ} (hx : 0 < x) (h : x ^ z ≤ y) : z * Real.log x ≤ Real.log y

theorem Real.le_log_of_pow_le {x y : ℝ} {n : ℕ} (hx : 0 < x) (h : x ^ n ≤ y) : ↑n * Real.log x ≤ Real.log y

theorem Real.le_log_of_zpow_le {x y : ℝ} {n : ℤ} (hx : 0 < x) (h : x ^ n ≤ y) : ↑n * Real.log x ≤ Real.log y

theorem Real.rpow_le_of_le_log {x y z : ℝ} (hy : 0 < y) (h : Real.log x ≤ z * Real.log y) : x ≤ y ^ z

theorem Real.pow_le_of_le_log {x y : ℝ} {n : ℕ} (hy : 0 < y) (h : Real.log x ≤ ↑n * Real.log y) : x ≤ y ^ n

theorem Real.zpow_le_of_le_log {x y : ℝ} {n : ℤ} (hy : 0 < y) (h : Real.log x ≤ ↑n * Real.log y) : x ≤ y ^ n

theorem Real.rpow_lt_iff_lt_log {x y z : ℝ} (hx : 0 < x) (hy : 0 < y) : x ^ z < y ↔ z * Real.log x < Real.log y

theorem Real.pow_lt_iff_lt_log {x y : ℝ} {n : ℕ} (hx : 0 < x) (hy : 0 < y) : x ^ n < y ↔ ↑n * Real.log x < Real.log y

theorem Real.zpow_lt_iff_lt_log {x y : ℝ} {n : ℤ} (hx : 0 < x) (hy : 0 < y) : x ^ n < y ↔ ↑n * Real.log x < Real.log y

theorem Real.lt_log_of_rpow_lt {x y z : ℝ} (hx : 0 < x) (h : x ^ z < y) : z * Real.log x < Real.log y

theorem Real.lt_log_of_pow_lt {x y : ℝ} {n : ℕ} (hx : 0 < x) (h : x ^ n < y) : ↑n * Real.log x < Real.log y

theorem Real.lt_log_of_zpow_lt {x y : ℝ} {n : ℤ} (hx : 0 < x) (h : x ^ n < y) : ↑n * Real.log x < Real.log y

theorem Real.rpow_lt_of_lt_log {x y z : ℝ} (hy : 0 < y) (h : Real.log x < z * Real.log y) : x < y ^ z

theorem Real.pow_lt_of_lt_log {x y : ℝ} {n : ℕ} (hy : 0 < y) (h : Real.log x < ↑n * Real.log y) : x < y ^ n

theorem Real.zpow_lt_of_lt_log {x y : ℝ} {n : ℤ} (hy : 0 < y) (h : Real.log x < ↑n * Real.log y) : x < y ^ n

theorem Real.rpow_le_one_iff_of_pos {x y : ℝ} (hx : 0 < x) : x ^ y ≤ 1 ↔ 1 ≤ x ∧ y ≤ 0 ∨ x ≤ 1 ∧ 0 ≤ y

theorem Real.abs_log_mul_self_rpow_lt (x t : ℝ) (h1 : 0 < x) (h2 : x ≤ 1) (ht : 0 < t) : |Real.log x * x ^ t| < 1 / t

Bound for |log x * x ^ t| in the interval (0, 1], for positive real t.

theorem Real.log_le_rpow_div {x ε : ℝ} (hx : 0 ≤ x) (hε : 0 < ε) : Real.log x ≤ x ^ ε / ε

log x is bounded above by a multiple of every power of x with positive exponent.

theorem Real.log_natCast_le_rpow_div (n : ℕ) {ε : ℝ} (hε : 0 < ε) : Real.log ↑n ≤ ↑n ^ ε / ε

The (real) logarithm of a natural number n is bounded by a multiple of every power of n with positive exponent.

theorem Real.strictMono_rpow_of_base_gt_one {b : ℝ} (hb : 1 < b) : StrictMono fun (x : ℝ) => b ^ x

theorem Real.monotone_rpow_of_base_ge_one {b : ℝ} (hb : 1 ≤ b) : Monotone fun (x : ℝ) => b ^ x

theorem Real.strictAnti_rpow_of_base_lt_one {b : ℝ} (hb₀ : 0 < b) (hb₁ : b < 1) : StrictAnti fun (x : ℝ) => b ^ x

theorem Real.antitone_rpow_of_base_le_one {b : ℝ} (hb₀ : 0 < b) (hb₁ : b ≤ 1) : Antitone fun (x : ℝ) => b ^ x

theorem Real.rpow_le_rpow_of_exponent_le_or_ge {x y z : ℝ} (h : 1 ≤ x ∧ y ≤ z ∨ 0 < x ∧ x ≤ 1 ∧ z ≤ y) : x ^ y ≤ x ^ z

Guessing rule for the bound tactic: when trying to prove x ^ y ≤ x ^ z, we can either assume 1 ≤ x or 0 < x ≤ 1.

theorem Complex.norm_prime_cpow_le_one_half (p : Nat.Primes) {s : ℂ} (hs : 1 < s.re) : ‖↑↑p ^ (-s)‖ ≤ 1 / 2

theorem Complex.one_sub_prime_cpow_ne_zero {p : ℕ} (hp : Nat.Prime p) {s : ℂ} (hs : 1 < s.re) : 1 - ↑p ^ (-s) ≠ 0

theorem Complex.norm_natCast_cpow_le_norm_natCast_cpow_of_pos {n : ℕ} (hn : 0 < n) {w z : ℂ} (h : w.re ≤ z.re) : ‖↑n ^ w‖ ≤ ‖↑n ^ z‖

theorem Complex.norm_natCast_cpow_le_norm_natCast_cpow_iff {n : ℕ} (hn : 1 < n) {w z : ℂ} : ‖↑n ^ w‖ ≤ ‖↑n ^ z‖ ↔ w.re ≤ z.re

theorem Complex.norm_log_natCast_le_rpow_div (n : ℕ) {ε : ℝ} (hε : 0 < ε) : ‖Complex.log ↑n‖ ≤ ↑n ^ ε / ε

Square roots of reals

theorem Real.sqrt_eq_rpow (x : ℝ) : √x = x ^ (1 / 2)

theorem Real.rpow_div_two_eq_sqrt {x : ℝ} (r : ℝ) (hx : 0 ≤ x) : x ^ (r / 2) = √x ^ r

theorem Real.exists_rat_pow_btwn_rat_aux {n : ℕ} (hn : n ≠ 0) (x y : ℝ) (h : x < y) (hy : 0 < y) : ∃ (q : ℚ), 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y

theorem Real.exists_rat_pow_btwn_rat {n : ℕ} (hn : n ≠ 0) {x y : ℚ} (h : x < y) (hy : 0 < y) : ∃ (q : ℚ), 0 < q ∧ x < q ^ n ∧ q ^ n < y

theorem Real.exists_rat_pow_btwn {n : ℕ} {α : Type u_1} [LinearOrderedField α] [Archimedean α] (hn : n ≠ 0) {x y : α} (h : x < y) (hy : 0 < y) : ∃ (q : ℚ), 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y

There is a rational power between any two positive elements of an archimedean ordered field.

theorem Complex.cpow_inv_two_re (x : ℂ) : (x ^ 2⁻¹).re = √((Complex.abs x + x.re) / 2)

theorem Complex.cpow_inv_two_im_eq_sqrt {x : ℂ} (hx : 0 ≤ x.im) : (x ^ 2⁻¹).im = √((Complex.abs x - x.re) / 2)

theorem Complex.cpow_inv_two_im_eq_neg_sqrt {x : ℂ} (hx : x.im < 0) : (x ^ 2⁻¹).im = -√((Complex.abs x - x.re) / 2)

theorem Complex.abs_cpow_inv_two_im (x : ℂ) : |(x ^ 2⁻¹).im| = √((Complex.abs x - x.re) / 2)

theorem Complex.inv_natCast_cpow_ofReal_pos {n : ℕ} (hn : n ≠ 0) (x : ℝ) : 0 < (↑n ^ ↑x)⁻¹

Tactic extensions for real powers

theorem Mathlib.Meta.NormNum.isNat_rpow_pos {a b : ℝ} {nb ne : ℕ} (pb : Mathlib.Meta.NormNum.IsNat b nb) (pe' : Mathlib.Meta.NormNum.IsNat (a ^ nb) ne) : Mathlib.Meta.NormNum.IsNat (a ^ b) ne

theorem Mathlib.Meta.NormNum.isNat_rpow_neg {a b : ℝ} {nb ne : ℕ} (pb : Mathlib.Meta.NormNum.IsInt b (Int.negOfNat nb)) (pe' : Mathlib.Meta.NormNum.IsNat (a ^ Int.negOfNat nb) ne) : Mathlib.Meta.NormNum.IsNat (a ^ b) ne

theorem Mathlib.Meta.NormNum.isInt_rpow_pos {a b : ℝ} {nb ne : ℕ} (pb : Mathlib.Meta.NormNum.IsNat b nb) (pe' : Mathlib.Meta.NormNum.IsInt (a ^ nb) (Int.negOfNat ne)) : Mathlib.Meta.NormNum.IsInt (a ^ b) (Int.negOfNat ne)

theorem Mathlib.Meta.NormNum.isInt_rpow_neg {a b : ℝ} {nb ne : ℕ} (pb : Mathlib.Meta.NormNum.IsInt b (Int.negOfNat nb)) (pe' : Mathlib.Meta.NormNum.IsInt (a ^ Int.negOfNat nb) (Int.negOfNat ne)) : Mathlib.Meta.NormNum.IsInt (a ^ b) (Int.negOfNat ne)

theorem Mathlib.Meta.NormNum.isRat_rpow_pos {a b : ℝ} {nb : ℕ} {num : ℤ} {den : ℕ} (pb : Mathlib.Meta.NormNum.IsNat b nb) (pe' : Mathlib.Meta.NormNum.IsRat (a ^ nb) num den) : Mathlib.Meta.NormNum.IsRat (a ^ b) num den

theorem Mathlib.Meta.NormNum.isRat_rpow_neg {a b : ℝ} {nb : ℕ} {num : ℤ} {den : ℕ} (pb : Mathlib.Meta.NormNum.IsInt b (Int.negOfNat nb)) (pe' : Mathlib.Meta.NormNum.IsRat (a ^ Int.negOfNat nb) num den) : Mathlib.Meta.NormNum.IsRat (a ^ b) num den

def Mathlib.Meta.NormNum.evalRPow : Mathlib.Meta.NormNum.NormNumExt

Evaluates expressions of the form a ^ b when a and b are both reals.

Equations

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