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

noncomputable instance Real.instPow : Pow ℝ ℝ

@[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 exp (log x * y)

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Real.rpow_ofNat (x : ℝ) (n : ℕ) [n.AtLeastTwo] : x ^ OfNat.ofNat n = x ^ OfNat.ofNat n

@[simp]

theorem Real.rpow_neg_ofNat (x : ℝ) (n : ℕ) [n.AtLeastTwo] : x ^ (-OfNat.ofNat n) = x ^ (-OfNat.ofNat n)

@[simp]

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

@[simp]

theorem Real.exp_one_pow (n : ℕ) : exp 1 ^ n = 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

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 = exp (log x * y) * 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 exp (log x * y) * 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.pi_rpow_zero {α : Type u_1} (f : α → ℝ) : f ^ 0 = 1

@[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| ≤ exp (log x * y)

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

theorem Real.rpow_inv_log_le_exp_one {x : ℝ} : x ^ (log x)⁻¹ ≤ 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_eq_inv_rpow (x y : ℝ) : x ^ (-y) = x⁻¹ ^ y

See also rpow_neg for a version with (x ^ y)⁻¹ in the RHS.

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

See also rpow_neg_eq_inv_rpow for a version with x⁻¹ ^ y in the RHS.

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 * exp (↑Real.pi * I * y)

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

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

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

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

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

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

@[simp]

theorem Complex.norm_cpow_real (x : ℂ) (y : ℝ) : ‖x ^ ↑y‖ = ‖x‖ ^ y

@[simp]

theorem Complex.norm_cpow_inv_nat (x : ℂ) (n : ℕ) : ‖x ^ (↑n)⁻¹‖ = ‖x‖ ^ (↑n)⁻¹

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

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

theorem Complex.norm_ofReal_cpow_eventually_eq_atTop (c : ℂ) : (fun (t : ℝ) => ‖↑t ^ c‖) =ᶠ[Filter.atTop] fun (t : ℝ) => t ^ c.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 : 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 : 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_pow_comm {x : ℝ} (hx : 0 ≤ x) (y : ℝ) (n : ℕ) : (x ^ y) ^ n = (x ^ n) ^ y

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

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

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

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 : ℝ) : log (x ^ y) = y * log x

theorem Real.mul_log_eq_log_iff {x y z : ℝ} (hx : 0 < x) (hz : 0 < z) : y * log x = 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

@[deprecated Real.rpow_lt_rpow_of_neg (since := "2025-10-28")]

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

Alias of Real.rpow_lt_rpow_of_neg.

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

@[deprecated Real.rpow_le_rpow_of_nonpos (since := "2025-10-28")]

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

Alias of Real.rpow_le_rpow_of_nonpos.

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.rpow_max {x y p : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hp : 0 ≤ p) : max x y ^ p = max (x ^ p) (y ^ p)

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 ↔ log x ≤ z * log y

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

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

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

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

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

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

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

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

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

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

theorem Real.lt_zpow_of_log_lt {x y : ℝ} {n : ℤ} (hy : 0 < y) (h : log x < ↑n * 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 * log x ≤ log y

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

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

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

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

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

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

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

theorem Real.zpow_le_of_le_log {x y : ℝ} {n : ℤ} (hy : 0 < y) (h : log x ≤ ↑n * 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 * log x < log y

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

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

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

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

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

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

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

theorem Real.zpow_lt_of_lt_log {x y : ℝ} {n : ℤ} (hy : 0 < y) (h : log x < ↑n * 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) : |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 < ε) : 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 < ε) : 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_right_inj {x y z : ℝ} (hx₀ : 0 < x) (hx₁ : x ≠ 1) : x ^ y = x ^ z ↔ y = z

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 < ε) : ‖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 Complex.cpow_inv_two_re (x : ℂ) : (x ^ 2⁻¹).re = √((‖x‖ + x.re) / 2)

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

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

theorem Complex.abs_cpow_inv_two_im (x : ℂ) : |(x ^ 2⁻¹).im| = √((‖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_eq_pow {b : ℝ} {n : ℕ} (h : IsNat b n) (a : ℝ) : a ^ b = a ^ n

theorem Mathlib.Meta.NormNum.IsInt.rpow_eq_inv_pow {b : ℝ} {n : ℕ} (h : IsInt b (Int.negOfNat n)) (a : ℝ) : a ^ b = (a ^ n)⁻¹

@[deprecated Mathlib.Meta.NormNum.IsNat.rpow_eq_pow (since := "2025-10-21")]

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

@[deprecated Mathlib.Meta.NormNum.IsInt.rpow_eq_inv_pow (since := "2025-10-21")]

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

@[deprecated Mathlib.Meta.NormNum.IsNat.rpow_eq_pow (since := "2025-10-21")]

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

@[deprecated Mathlib.Meta.NormNum.IsInt.rpow_eq_inv_pow (since := "2025-10-21")]

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

@[deprecated Mathlib.Meta.NormNum.IsNat.rpow_eq_pow (since := "2025-10-21")]

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

@[deprecated Mathlib.Meta.NormNum.IsNat.rpow_eq_pow (since := "2025-10-21")]

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

@[deprecated Mathlib.Meta.NormNum.IsInt.rpow_eq_inv_pow (since := "2025-10-21")]

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

@[deprecated Mathlib.Meta.NormNum.IsInt.rpow_eq_inv_pow (since := "2025-10-21")]

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

theorem Mathlib.Meta.NormNum.IsNat.rpow_isNNRat {a 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

Given proofs

• that a is a natural number m
• that b is a nonnegative rational number n / d
• that r ^ d = m ^ n (written as r ^ d = k, m ^ n = l, k = l) prove that a ^ b = r.

theorem Mathlib.Meta.NormNum.IsNNRat.rpow_isNNRat (a 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.rpow_isRat_eq_inv_rpow (a b : ℝ) (n d : ℕ) (hb : IsRat b (Int.negOfNat n) d) : a ^ b = a⁻¹ ^ (↑n / ↑d)

def Mathlib.Meta.NormNum.proveIsNatRPowIsNNRat (a : Q(ℝ)) (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.evalRPow : NormNumExt

Evaluates expressions of the form a ^ b when a and b are both reals. Works if a, b, and a ^ b are in fact rational numbers, except for the case a < 0, b isn't integer.

TODO: simplify terms like (-a : ℝ) ^ (b / 3 : ℝ) and (-a : ℝ) ^ (b / 2 : ℝ) too, possibly after first considering changing the junk value.