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

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

noncomputable instance Real.instPowReal : Pow ℝ ℝ

Equations

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

@[simp]

theorem Real.rpow_eq_pow (x : ℝ) (y : ℝ) : Real.rpow x 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.exp_one_rpow (x : ℝ) : Real.exp 1 ^ x = Real.exp x

theorem Real.rpow_eq_zero_iff_of_nonneg {x : ℝ} {y : ℝ} (hx : 0 ≤ x) : x ^ y = 0 ↔ x = 0 ∧ y ≠ 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_of_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.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_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 ^ Finset.sum s fun x => f x) = Finset.prod s fun x => a ^ f x

theorem Real.rpow_sum_of_nonneg {ι : Type u_1} {a : ℝ} (ha : 0 ≤ a) {s : Finset ι} {f : ι → ℝ} (h : ∀ (x : ι), x ∈ s → 0 ≤ f x) : (a ^ Finset.sum s fun x => f x) = Finset.prod s fun x => 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

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.abs_cpow_of_ne_zero {z : ℂ} (hz : z ≠ 0) (w : ℂ) : ↑Complex.abs (z ^ w) = ↑Complex.abs z ^ w.re / Real.exp (Complex.arg z * 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 (Complex.arg z * w.im)

theorem Complex.abs_cpow_le (z : ℂ) (w : ℂ) : ↑Complex.abs (z ^ w) ≤ ↑Complex.abs z ^ w.re / Real.exp (Complex.arg z * 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

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_int {x : ℝ} (hx : x ≠ 0) (y : ℝ) (n : ℤ) : x ^ (y + ↑n) = x ^ y * x ^ n

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

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

theorem Real.rpow_sub_nat {x : ℝ} (hx : x ≠ 0) (y : ℝ) (n : ℕ) : 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

@[simp]

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

@[simp]

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

@[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 : ℝ} (h : 0 ≤ x) (h₁ : 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

Note: lemmas about (∏ i in 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_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.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.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' {x : ℝ} {y : ℝ} {z : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) (hz : 0 ≤ z) (hyz : z ≤ y) : x ^ y ≤ x ^ z

theorem Real.rpow_left_injOn {x : ℝ} (hx : x ≠ 0) : Set.InjOn (fun y => y ^ x) {y | 0 ≤ 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_rpow_of_log_le {x : ℝ} {y : ℝ} {z : ℝ} (hx : 0 ≤ x) (hy : 0 < y) (h : Real.log x ≤ z * Real.log y) : x ≤ y ^ z

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_rpow_of_log_lt {x : ℝ} {y : ℝ} {z : ℝ} (hx : 0 ≤ x) (hy : 0 < y) (h : Real.log x < z * Real.log y) : x < y ^ z

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.pow_nat_rpow_nat_inv {x : ℝ} (hx : 0 ≤ x) {n : ℕ} (hn : n ≠ 0) : (x ^ n) ^ (↑n)⁻¹ = x

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

theorem Real.strictMono_rpow_of_base_gt_one {b : ℝ} (hb : 1 < b) : StrictMono (Real.rpow b)

theorem Real.monotone_rpow_of_base_ge_one {b : ℝ} (hb : 1 ≤ b) : Monotone (Real.rpow b)

theorem Real.strictAnti_rpow_of_base_lt_one {b : ℝ} (hb₀ : 0 < b) (hb₁ : b < 1) : StrictAnti (Real.rpow b)

theorem Real.antitone_rpow_of_base_le_one {b : ℝ} (hb₀ : 0 < b) (hb₁ : b ≤ 1) : Antitone (Real.rpow b)

Square roots of reals

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

theorem Real.rpow_div_two_eq_sqrt {x : ℝ} (r : ℝ) (hx : 0 ≤ x) : x ^ (r / 2) = Real.sqrt 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.

Tactic extensions for real powers

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.

Equations

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

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.

Equations

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