mathlib3 documentation

analysis.special_functions.pow.real

Power function on `ℝ` #

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 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 arbitary 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

@[protected, instance]

noncomputable def real.has_pow :

has_pow ℝ ℝ

Equations

real.has_pow = {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 = ite (x = 0) (ite (y = 0) 1 0) (rexp (real.log x * y))

theorem real.rpow_def_of_pos {x : ℝ} (hx : 0 < x) (y : ℝ) :

x ^ y = rexp (real.log x * y)

theorem real.exp_mul (x y : ℝ) :

rexp (x * y) = rexp x ^ y

@[simp]

theorem real.exp_one_rpow (x : ℝ) :

rexp 1 ^ x = rexp 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 = rexp (real.log x * y) * real.cos (y * real.pi)

theorem real.rpow_def_of_nonpos {x : ℝ} (hx : x ≤ 0) (y : ℝ) :

x ^ y = ite (x = 0) (ite (y = 0) 1 0) (rexp (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

@[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| ≤ rexp (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 ^ s.sum (λ (x : ι), f x) = s.prod (λ (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 ^ s.sum (λ (x : ι), f x) = s.prod (λ (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.of_real_cpow {x : ℝ} (hx : 0 ≤ x) (y : ℝ) :

↑(x ^ y) = ↑x ^ ↑y

theorem complex.of_real_cpow_of_nonpos {x : ℝ} (hx : x ≤ 0) (y : ℂ) :

↑x ^ y = (-↑x) ^ y * cexp (↑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 / rexp (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 / rexp (z.arg * w.im)

theorem complex.abs_cpow_le (z w : ℂ) :

⇑complex.abs (z ^ w) ≤ ⇑complex.abs z ^ w.re / rexp (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

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, norm_cast]

theorem real.rpow_int_cast (x : ℝ) (n : ℤ) :

x ^ ↑n = x ^ n

@[simp, norm_cast]

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

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.rpow_le_rpow {x y z : ℝ} (h : 0 ≤ x) (h₁ : x ≤ y) (h₂ : 0 ≤ z) :

x ^ z ≤ y ^ 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.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

@[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_inj_on {x : ℝ} (hx : x ≠ 0) :

set.inj_on (λ (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

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} [linear_ordered_field α] [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 #

theorem norm_num.rpow_pos (a b : ℝ) (b' : ℕ) (c : ℝ) (hb : ↑b' = b) (h : a ^ b' = c) :

a ^ b = c

theorem norm_num.rpow_neg (a b : ℝ) (b' : ℕ) (c c' : ℝ) (a0 : 0 ≤ a) (hb : ↑b' = b) (h : a ^ b' = c) (hc : c⁻¹ = c') :

a ^ -b = c'

meta def norm_num.prove_rpow (a b : expr) :

tactic (expr × expr)

Evaluate real.rpow a b where a is a rational numeral and b is an integer. (This cannot go via the generalized version prove_rpow' because rpow_pos has a side condition; we do not attempt to evaluate a ^ b where a and b are both negative because it comes out to some garbage.)

meta def norm_num.eval_rpow :

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

meta def tactic.positivity.prove_rpow (a b : expr) :

tactic tactic.positivity.strictness

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

meta def tactic.positivity_rpow :

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.