mathlib documentation

analysis.special_functions.pow

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

We construct the power functions x ^ y where

We also prove basic properties of these functions.

source
noncomputable def complex.cpow (x y : ℂ) :
ℂ

The complex power function x^y, given by x^y = exp(y log x) (where log is the principal determination of the logarithm), unless x = 0 where one sets 0^0 = 1 and 0^y = 0 for y ≠ 0.

Equations
source
@[protected, instance]
noncomputable def complex.has_pow  :
has_pow ℂ ℂ
Equations
source
@[simp]
theorem complex.cpow_eq_pow (x y : ℂ) :
x.cpow y = x ^ y
source
theorem complex.cpow_def (x y : ℂ) :
x ^ y = ite (x = 0) (ite (y = 0) 1 0) (cexp (complex.log x * y))
source
theorem complex.cpow_def_of_ne_zero {x : ℂ} (hx : x ≠ 0) (y : ℂ) :
x ^ y = cexp (complex.log x * y)
source
@[simp]
theorem complex.cpow_zero (x : ℂ) :
x ^ 0 = 1
source
@[simp]
theorem complex.cpow_eq_zero_iff (x y : ℂ) :
x ^ y = 0 ↔ x = 0 ∧ y ≠ 0
source
@[simp]
theorem complex.zero_cpow {x : ℂ} (h : x ≠ 0) :
0 ^ x = 0
source
theorem complex.zero_cpow_eq_iff {x a : ℂ} :
0 ^ x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
source
theorem complex.eq_zero_cpow_iff {x a : ℂ} :
a = 0 ^ x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
source
@[simp]
theorem complex.cpow_one (x : ℂ) :
x ^ 1 = x
source
@[simp]
theorem complex.one_cpow (x : ℂ) :
1 ^ x = 1
source
theorem complex.cpow_add {x : ℂ} (y z : ℂ) (hx : x ≠ 0) :
x ^ (y + z) = x ^ y * x ^ z
source
theorem complex.cpow_mul {x y : ℂ} (z : ℂ) (h₁ : -real.pi < (complex.log x * y).im) (h₂ : (complex.log x * y).im ≤ real.pi) :
x ^ (y * z) = (x ^ y) ^ z
source
theorem complex.cpow_neg (x y : ℂ) :
x ^ -y = (x ^ y)⁻¹
source
theorem complex.cpow_sub {x : ℂ} (y z : ℂ) (hx : x ≠ 0) :
x ^ (y - z) = x ^ y / x ^ z
source
theorem complex.cpow_neg_one (x : ℂ) :
x ^ -1 = x⁻¹
source
@[simp, norm_cast]
theorem complex.cpow_nat_cast (x : ℂ) (n : ℕ) :
x ^ ↑n = x ^ n
source
@[simp]
theorem complex.cpow_two (x : ℂ) :
x ^ 2 = x ^ 2
source
@[simp, norm_cast]
theorem complex.cpow_int_cast (x : ℂ) (n : ℤ) :
x ^ ↑n = x ^ n
source
theorem complex.cpow_nat_inv_pow (x : ℂ) {n : ℕ} (hn : n ≠ 0) :
(x ^ (↑n)⁻¹) ^ n = x
source
theorem complex.mul_cpow_of_real_nonneg {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (r : ℂ) :
(↑a * ↑b) ^ r = ↑a ^ r * ↑b ^ r
source
theorem zero_cpow_eq_nhds {b : ℂ} (hb : b ≠ 0) :
(λ (x : ℂ), 0 ^ x) =ᶠ[nhds b] 0
source
theorem cpow_eq_nhds {a b : ℂ} (ha : a ≠ 0) :
(λ (x : ℂ), x ^ b) =ᶠ[nhds a] λ (x : ℂ), cexp (complex.log x * b)
source
theorem cpow_eq_nhds' {p : ℂ × ℂ} (hp_fst : p.fst ≠ 0) :
(λ (x : ℂ × ℂ), x.fst ^ x.snd) =ᶠ[nhds p] λ (x : ℂ × ℂ), cexp (complex.log x.fst * x.snd)
source
theorem continuous_at_const_cpow {a b : ℂ} (ha : a ≠ 0) :
continuous_at (λ (x : ℂ), a ^ x) b
source
theorem continuous_at_const_cpow' {a b : ℂ} (h : b ≠ 0) :
continuous_at (λ (x : ℂ), a ^ x) b
source
theorem continuous_at_cpow {p : ℂ × ℂ} (hp_fst : 0 < p.fst.re ∨ p.fst.im ≠ 0) :
continuous_at (λ (x : ℂ × ℂ), x.fst ^ x.snd) p

The function z ^ w is continuous in (z, w) provided that z does not belong to the interval (-∞, 0] on the real line. See also complex.continuous_at_cpow_zero_of_re_pos for a version that works for z = 0 but assumes 0 < re w.

source
theorem continuous_at_cpow_const {a b : ℂ} (ha : 0 < a.re ∨ a.im ≠ 0) :
continuous_at (λ (x : ℂ), x.cpow b) a
source
theorem filter.tendsto.cpow {α : Type u_1} {l : filter α} {f g : α → ℂ} {a b : ℂ} (hf : filter.tendsto f l (nhds a)) (hg : filter.tendsto g l (nhds b)) (ha : 0 < a.re ∨ a.im ≠ 0) :
filter.tendsto (λ (x : α), f x ^ g x) l (nhds (a ^ b))
source
theorem filter.tendsto.const_cpow {α : Type u_1} {l : filter α} {f : α → ℂ} {a b : ℂ} (hf : filter.tendsto f l (nhds b)) (h : a ≠ 0 ∨ b ≠ 0) :
filter.tendsto (λ (x : α), a ^ f x) l (nhds (a ^ b))
source
theorem continuous_within_at.cpow {α : Type u_1} [topological_space α] {f g : α → ℂ} {s : set α} {a : α} (hf : continuous_within_at f s a) (hg : continuous_within_at g s a) (h0 : 0 < (f a).re ∨ (f a).im ≠ 0) :
continuous_within_at (λ (x : α), f x ^ g x) s a
source
theorem continuous_within_at.const_cpow {α : Type u_1} [topological_space α] {f : α → ℂ} {s : set α} {a : α} {b : ℂ} (hf : continuous_within_at f s a) (h : b ≠ 0 ∨ f a ≠ 0) :
continuous_within_at (λ (x : α), b ^ f x) s a
source
theorem continuous_at.cpow {α : Type u_1} [topological_space α] {f g : α → ℂ} {a : α} (hf : continuous_at f a) (hg : continuous_at g a) (h0 : 0 < (f a).re ∨ (f a).im ≠ 0) :
continuous_at (λ (x : α), f x ^ g x) a
source
theorem continuous_at.const_cpow {α : Type u_1} [topological_space α] {f : α → ℂ} {a : α} {b : ℂ} (hf : continuous_at f a) (h : b ≠ 0 ∨ f a ≠ 0) :
continuous_at (λ (x : α), b ^ f x) a
source
theorem continuous_on.cpow {α : Type u_1} [topological_space α] {f g : α → ℂ} {s : set α} (hf : continuous_on f s) (hg : continuous_on g s) (h0 : ∀ (a : α), a ∈ s → 0 < (f a).re ∨ (f a).im ≠ 0) :
continuous_on (λ (x : α), f x ^ g x) s
source
theorem continuous_on.const_cpow {α : Type u_1} [topological_space α] {f : α → ℂ} {s : set α} {b : ℂ} (hf : continuous_on f s) (h : b ≠ 0 ∨ ∀ (a : α), a ∈ s → f a ≠ 0) :
continuous_on (λ (x : α), b ^ f x) s
source
theorem continuous.cpow {α : Type u_1} [topological_space α] {f g : α → ℂ} (hf : continuous f) (hg : continuous g) (h0 : ∀ (a : α), 0 < (f a).re ∨ (f a).im ≠ 0) :
continuous (λ (x : α), f x ^ g x)
source
theorem continuous.const_cpow {α : Type u_1} [topological_space α] {f : α → ℂ} {b : ℂ} (hf : continuous f) (h : b ≠ 0 ∨ ∀ (a : α), f a ≠ 0) :
continuous (λ (x : α), b ^ f x)
source
theorem continuous_on.cpow_const {α : Type u_1} [topological_space α] {f : α → ℂ} {s : set α} {b : ℂ} (hf : continuous_on f s) (h : ∀ (a : α), a ∈ s → 0 < (f a).re ∨ (f a).im ≠ 0) :
continuous_on (λ (x : α), f x ^ b) s
source
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
source
@[protected, instance]
noncomputable def real.has_pow  :
has_pow ℝ ℝ
Equations
source
@[simp]
theorem real.rpow_eq_pow (x y : ℝ) :
x.rpow y = x ^ y
source
theorem real.rpow_def (x y : ℝ) :
x ^ y = (↑x ^ ↑y).re
source
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))
source
theorem real.rpow_def_of_pos {x : ℝ} (hx : 0 < x) (y : ℝ) :
x ^ y = rexp (real.log x * y)
source
theorem real.exp_mul (x y : ℝ) :
rexp (x * y) = rexp x ^ y
source
@[simp]
theorem real.exp_one_rpow (x : ℝ) :
rexp 1 ^ x = rexp x
source
theorem real.rpow_eq_zero_iff_of_nonneg {x y : ℝ} (hx : 0 ≤ x) :
x ^ y = 0 ↔ x = 0 ∧ y ≠ 0
source
theorem real.rpow_def_of_neg {x : ℝ} (hx : x < 0) (y : ℝ) :
x ^ y = rexp (real.log x * y) * real.cos (y * real.pi)
source
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))
source
theorem real.rpow_pos_of_pos {x : ℝ} (hx : 0 < x) (y : ℝ) :
0 < x ^ y
source
@[simp]
theorem real.rpow_zero (x : ℝ) :
x ^ 0 = 1
source
@[simp]
theorem real.zero_rpow {x : ℝ} (h : x ≠ 0) :
0 ^ x = 0
source
theorem real.zero_rpow_eq_iff {x a : ℝ} :
0 ^ x = a ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
source
theorem real.eq_zero_rpow_iff {x a : ℝ} :
a = 0 ^ x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
source
@[simp]
theorem real.rpow_one (x : ℝ) :
x ^ 1 = x
source
@[simp]
theorem real.one_rpow (x : ℝ) :
1 ^ x = 1
source
theorem real.zero_rpow_le_one (x : ℝ) :
0 ^ x ≤ 1
source
theorem real.zero_rpow_nonneg (x : ℝ) :
0 ≤ 0 ^ x
source
theorem real.rpow_nonneg_of_nonneg {x : ℝ} (hx : 0 ≤ x) (y : ℝ) :
0 ≤ x ^ y
source
theorem real.abs_rpow_of_nonneg {x y : ℝ} (hx_nonneg : 0 ≤ x) :
|x ^ y| = |x| ^ y
source
theorem real.abs_rpow_le_abs_rpow (x y : ℝ) :
|x ^ y| ≤ |x| ^ y
source
theorem real.abs_rpow_le_exp_log_mul (x y : ℝ) :
|x ^ y| ≤ rexp (real.log x * y)
source
theorem real.norm_rpow_of_nonneg {x y : ℝ} (hx_nonneg : 0 ≤ x) :
‖x ^ y‖ = ‖x‖ ^ y
source
theorem complex.of_real_cpow {x : ℝ} (hx : 0 ≤ x) (y : ℝ) :
↑(x ^ y) = ↑x ^ ↑y
source
theorem complex.of_real_cpow_of_nonpos {x : ℝ} (hx : x ≤ 0) (y : ℂ) :
↑x ^ y = (-↑x) ^ y * cexp (↑real.pi * complex.I * y)
source
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)
source
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)
source
theorem complex.abs_cpow_le (z w : ℂ) :
⇑complex.abs (z ^ w) ≤ ⇑complex.abs z ^ w.re / rexp (z.arg * w.im)
source
theorem complex.is_Theta_exp_arg_mul_im {α : Type u_1} {l : filter α} {f g : α → ℂ} (hl : filter.is_bounded_under has_le.le l (λ (x : α), |(g x).im|)) :
(λ (x : α), rexp ((f x).arg * (g x).im)) =Θ[l] λ (x : α), 1
source
theorem complex.is_O_cpow_rpow {α : Type u_1} {l : filter α} {f g : α → ℂ} (hl : filter.is_bounded_under has_le.le l (λ (x : α), |(g x).im|)) :
(λ (x : α), f x ^ g x) =O[l] λ (x : α), ⇑complex.abs (f x) ^ (g x).re
source
theorem complex.is_Theta_cpow_rpow {α : Type u_1} {l : filter α} {f g : α → ℂ} (hl_im : filter.is_bounded_under has_le.le l (λ (x : α), |(g x).im|)) (hl : ∀ᶠ (x : α) in l, f x = 0 → (g x).re = 0 → g x = 0) :
(λ (x : α), f x ^ g x) =Θ[l] λ (x : α), ⇑complex.abs (f x) ^ (g x).re
source
theorem complex.is_Theta_cpow_const_rpow {α : Type u_1} {l : filter α} {f : α → ℂ} {b : ℂ} (hl : b.re = 0 → b ≠ 0 → (∀ᶠ (x : α) in l, f x ≠ 0)) :
(λ (x : α), f x ^ b) =Θ[l] λ (x : α), ⇑complex.abs (f x) ^ b.re
source
@[simp]
theorem complex.abs_cpow_real (x : ℂ) (y : ℝ) :
⇑complex.abs (x ^ ↑y) = ⇑complex.abs x ^ y
source
@[simp]
theorem complex.abs_cpow_inv_nat (x : ℂ) (n : ℕ) :
⇑complex.abs (x ^ (↑n)⁻¹) = ⇑complex.abs x ^ (↑n)⁻¹
source
theorem complex.abs_cpow_eq_rpow_re_of_pos {x : ℝ} (hx : 0 < x) (y : ℂ) :
⇑complex.abs (↑x ^ y) = x ^ y.re
source
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
source
theorem complex.inv_cpow_eq_ite (x n : ℂ) :
x⁻¹ ^ n = ite (x.arg = real.pi) (⇑(star_ring_end ℂ) (x ^ ⇑(star_ring_end ℂ) n)⁻¹) (x ^ n)⁻¹
source
theorem complex.inv_cpow (x n : ℂ) (hx : x.arg ≠ real.pi) :
x⁻¹ ^ n = (x ^ n)⁻¹
source
theorem complex.inv_cpow_eq_ite' (x n : ℂ) :
(x ^ n)⁻¹ = ite (x.arg = real.pi) (⇑(star_ring_end ℂ) (x⁻¹ ^ ⇑(star_ring_end ℂ) n)) (x⁻¹ ^ n)

complex.inv_cpow_eq_ite with the ite on the other side.

source
theorem complex.conj_cpow_eq_ite (x n : ℂ) :
⇑(star_ring_end ℂ) x ^ n = ite (x.arg = real.pi) (x ^ n) (⇑(star_ring_end ℂ) (x ^ ⇑(star_ring_end ℂ) n))
source
theorem complex.conj_cpow (x n : ℂ) (hx : x.arg ≠ real.pi) :
⇑(star_ring_end ℂ) x ^ n = ⇑(star_ring_end ℂ) (x ^ ⇑(star_ring_end ℂ) n)
source
theorem complex.cpow_conj (x n : ℂ) (hx : x.arg ≠ real.pi) :
x ^ ⇑(star_ring_end ℂ) n = ⇑(star_ring_end ℂ) (⇑(star_ring_end ℂ) x ^ n)
source
theorem real.rpow_add {x : ℝ} (hx : 0 < x) (y z : ℝ) :
x ^ (y + z) = x ^ y * x ^ z
source
theorem real.rpow_add' {x y z : ℝ} (hx : 0 ≤ x) (h : y + z ≠ 0) :
x ^ (y + z) = x ^ y * x ^ z
source
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
source
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.

source
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)
source
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)
source
theorem real.rpow_mul {x : ℝ} (hx : 0 ≤ x) (y z : ℝ) :
x ^ (y * z) = (x ^ y) ^ z
source
theorem real.rpow_neg {x : ℝ} (hx : 0 ≤ x) (y : ℝ) :
x ^ -y = (x ^ y)⁻¹
source
theorem real.rpow_sub {x : ℝ} (hx : 0 < x) (y z : ℝ) :
x ^ (y - z) = x ^ y / x ^ z
source
theorem real.rpow_sub' {x : ℝ} (hx : 0 ≤ x) {y z : ℝ} (h : y - z ≠ 0) :
x ^ (y - z) = x ^ y / x ^ z
source
theorem real.rpow_add_int {x : ℝ} (hx : x ≠ 0) (y : ℝ) (n : ℤ) :
x ^ (y + ↑n) = x ^ y * x ^ n
source
theorem real.rpow_add_nat {x : ℝ} (hx : x ≠ 0) (y : ℝ) (n : ℕ) :
x ^ (y + ↑n) = x ^ y * x ^ n
source
theorem real.rpow_sub_int {x : ℝ} (hx : x ≠ 0) (y : ℝ) (n : ℤ) :
x ^ (y - ↑n) = x ^ y / x ^ n
source
theorem real.rpow_sub_nat {x : ℝ} (hx : x ≠ 0) (y : ℝ) (n : ℕ) :
x ^ (y - ↑n) = x ^ y / x ^ n
source
theorem real.rpow_add_one {x : ℝ} (hx : x ≠ 0) (y : ℝ) :
x ^ (y + 1) = x ^ y * x
source
theorem real.rpow_sub_one {x : ℝ} (hx : x ≠ 0) (y : ℝ) :
x ^ (y - 1) = x ^ y / x
source
@[simp, norm_cast]
theorem real.rpow_int_cast (x : ℝ) (n : ℤ) :
x ^ ↑n = x ^ n
source
@[simp, norm_cast]
theorem real.rpow_nat_cast (x : ℝ) (n : ℕ) :
x ^ ↑n = x ^ n
source
@[simp]
theorem real.rpow_two (x : ℝ) :
x ^ 2 = x ^ 2
source
theorem real.rpow_neg_one (x : ℝ) :
x ^ -1 = x⁻¹
source
theorem real.mul_rpow {x y z : ℝ} (h : 0 ≤ x) (h₁ : 0 ≤ y) :
(x * y) ^ z = x ^ z * y ^ z
source
theorem real.inv_rpow {x : ℝ} (hx : 0 ≤ x) (y : ℝ) :
x⁻¹ ^ y = (x ^ y)⁻¹
source
theorem real.div_rpow {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (z : ℝ) :
(x / y) ^ z = x ^ z / y ^ z
source
theorem real.log_rpow {x : ℝ} (hx : 0 < x) (y : ℝ) :
real.log (x ^ y) = y * real.log x
source
theorem real.rpow_lt_rpow {x y z : ℝ} (hx : 0 ≤ x) (hxy : x < y) (hz : 0 < z) :
x ^ z < y ^ z
source
theorem real.rpow_le_rpow {x y z : ℝ} (h : 0 ≤ x) (h₁ : x ≤ y) (h₂ : 0 ≤ z) :
x ^ z ≤ y ^ z
source
theorem real.rpow_lt_rpow_iff {x y z : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : 0 < z) :
x ^ z < y ^ z ↔ x < y
source
theorem real.rpow_le_rpow_iff {x y z : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : 0 < z) :
x ^ z ≤ y ^ z ↔ x ≤ y
source
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
source
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
source
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
source
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
source
theorem real.rpow_lt_rpow_of_exponent_lt {x y z : ℝ} (hx : 1 < x) (hyz : y < z) :
x ^ y < x ^ z
source
theorem real.rpow_le_rpow_of_exponent_le {x y z : ℝ} (hx : 1 ≤ x) (hyz : y ≤ z) :
x ^ y ≤ x ^ z
source
@[simp]
theorem real.rpow_le_rpow_left_iff {x y z : ℝ} (hx : 1 < x) :
x ^ y ≤ x ^ z ↔ y ≤ z
source
@[simp]
theorem real.rpow_lt_rpow_left_iff {x y z : ℝ} (hx : 1 < x) :
x ^ y < x ^ z ↔ y < z
source
theorem real.rpow_lt_rpow_of_exponent_gt {x y z : ℝ} (hx0 : 0 < x) (hx1 : x < 1) (hyz : z < y) :
x ^ y < x ^ z
source
theorem real.rpow_le_rpow_of_exponent_ge {x y z : ℝ} (hx0 : 0 < x) (hx1 : x ≤ 1) (hyz : z ≤ y) :
x ^ y ≤ x ^ z
source
@[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
source
@[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
source
theorem real.rpow_lt_one {x z : ℝ} (hx1 : 0 ≤ x) (hx2 : x < 1) (hz : 0 < z) :
x ^ z < 1
source
theorem real.rpow_le_one {x z : ℝ} (hx1 : 0 ≤ x) (hx2 : x ≤ 1) (hz : 0 ≤ z) :
x ^ z ≤ 1
source
theorem real.rpow_lt_one_of_one_lt_of_neg {x z : ℝ} (hx : 1 < x) (hz : z < 0) :
x ^ z < 1
source
theorem real.rpow_le_one_of_one_le_of_nonpos {x z : ℝ} (hx : 1 ≤ x) (hz : z ≤ 0) :
x ^ z ≤ 1
source
theorem real.one_lt_rpow {x z : ℝ} (hx : 1 < x) (hz : 0 < z) :
1 < x ^ z
source
theorem real.one_le_rpow {x z : ℝ} (hx : 1 ≤ x) (hz : 0 ≤ z) :
1 ≤ x ^ z
source
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
source
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
source
theorem real.rpow_lt_one_iff_of_pos {x y : ℝ} (hx : 0 < x) :
x ^ y < 1 ↔ 1 < x ∧ y < 0 ∨ x < 1 ∧ 0 < y
source
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
source
theorem real.one_lt_rpow_iff_of_pos {x y : ℝ} (hx : 0 < x) :
1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ x < 1 ∧ y < 0
source
theorem real.one_lt_rpow_iff {x y : ℝ} (hx : 0 ≤ x) :
1 < x ^ y ↔ 1 < x ∧ 0 < y ∨ 0 < x ∧ x < 1 ∧ y < 0
source
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
source
theorem real.rpow_left_inj_on {x : ℝ} (hx : x ≠ 0) :
set.inj_on (λ (y : ℝ), y ^ x) {y : ℝ | 0 ≤ y}
source
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
source
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
source
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
source
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
source
theorem real.rpow_le_one_iff_of_pos {x y : ℝ} (hx : 0 < x) :
x ^ y ≤ 1 ↔ 1 ≤ x ∧ y ≤ 0 ∨ x ≤ 1 ∧ 0 ≤ y
source
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.

source
theorem real.pow_nat_rpow_nat_inv {x : ℝ} (hx : 0 ≤ x) {n : ℕ} (hn : n ≠ 0) :
(x ^ n) ^ (↑n)⁻¹ = x
source
theorem real.rpow_nat_inv_pow_nat {x : ℝ} (hx : 0 ≤ x) {n : ℕ} (hn : n ≠ 0) :
(x ^ (↑n)⁻¹) ^ n = x
source
theorem real.continuous_at_const_rpow {a b : ℝ} (h : a ≠ 0) :
continuous_at a.rpow b
source
theorem real.continuous_at_const_rpow' {a b : ℝ} (h : b ≠ 0) :
continuous_at a.rpow b
source
theorem real.rpow_eq_nhds_of_neg {p : ℝ × ℝ} (hp_fst : p.fst < 0) :
(λ (x : ℝ × ℝ), x.fst ^ x.snd) =ᶠ[nhds p] λ (x : ℝ × ℝ), rexp (real.log x.fst * x.snd) * real.cos (x.snd * real.pi)
source
theorem real.rpow_eq_nhds_of_pos {p : ℝ × ℝ} (hp_fst : 0 < p.fst) :
(λ (x : ℝ × ℝ), x.fst ^ x.snd) =ᶠ[nhds p] λ (x : ℝ × ℝ), rexp (real.log x.fst * x.snd)
source
theorem real.continuous_at_rpow_of_ne (p : ℝ × ℝ) (hp : p.fst ≠ 0) :
continuous_at (λ (p : ℝ × ℝ), p.fst ^ p.snd) p
source
theorem real.continuous_at_rpow_of_pos (p : ℝ × ℝ) (hp : 0 < p.snd) :
continuous_at (λ (p : ℝ × ℝ), p.fst ^ p.snd) p
source
theorem real.continuous_at_rpow (p : ℝ × ℝ) (h : p.fst ≠ 0 ∨ 0 < p.snd) :
continuous_at (λ (p : ℝ × ℝ), p.fst ^ p.snd) p
source
theorem real.continuous_at_rpow_const (x q : ℝ) (h : x ≠ 0 ∨ 0 < q) :
continuous_at (λ (x : ℝ), x ^ q) x
source
theorem filter.tendsto.rpow {α : Type u_1} {l : filter α} {f g : α → ℝ} {x y : ℝ} (hf : filter.tendsto f l (nhds x)) (hg : filter.tendsto g l (nhds y)) (h : x ≠ 0 ∨ 0 < y) :
filter.tendsto (λ (t : α), f t ^ g t) l (nhds (x ^ y))
source
theorem filter.tendsto.rpow_const {α : Type u_1} {l : filter α} {f : α → ℝ} {x p : ℝ} (hf : filter.tendsto f l (nhds x)) (h : x ≠ 0 ∨ 0 ≤ p) :
filter.tendsto (λ (a : α), f a ^ p) l (nhds (x ^ p))
source
theorem continuous_at.rpow {α : Type u_1} [topological_space α] {f g : α → ℝ} {x : α} (hf : continuous_at f x) (hg : continuous_at g x) (h : f x ≠ 0 ∨ 0 < g x) :
continuous_at (λ (t : α), f t ^ g t) x
source
theorem continuous_within_at.rpow {α : Type u_1} [topological_space α] {f g : α → ℝ} {s : set α} {x : α} (hf : continuous_within_at f s x) (hg : continuous_within_at g s x) (h : f x ≠ 0 ∨ 0 < g x) :
continuous_within_at (λ (t : α), f t ^ g t) s x
source
theorem continuous_on.rpow {α : Type u_1} [topological_space α] {f g : α → ℝ} {s : set α} (hf : continuous_on f s) (hg : continuous_on g s) (h : ∀ (x : α), x ∈ s → f x ≠ 0 ∨ 0 < g x) :
continuous_on (λ (t : α), f t ^ g t) s
source
theorem continuous.rpow {α : Type u_1} [topological_space α] {f g : α → ℝ} (hf : continuous f) (hg : continuous g) (h : ∀ (x : α), f x ≠ 0 ∨ 0 < g x) :
continuous (λ (x : α), f x ^ g x)
source
theorem continuous_within_at.rpow_const {α : Type u_1} [topological_space α] {f : α → ℝ} {s : set α} {x : α} {p : ℝ} (hf : continuous_within_at f s x) (h : f x ≠ 0 ∨ 0 ≤ p) :
continuous_within_at (λ (x : α), f x ^ p) s x
source
theorem continuous_at.rpow_const {α : Type u_1} [topological_space α] {f : α → ℝ} {x : α} {p : ℝ} (hf : continuous_at f x) (h : f x ≠ 0 ∨ 0 ≤ p) :
continuous_at (λ (x : α), f x ^ p) x
source
theorem continuous_on.rpow_const {α : Type u_1} [topological_space α] {f : α → ℝ} {s : set α} {p : ℝ} (hf : continuous_on f s) (h : ∀ (x : α), x ∈ s → f x ≠ 0 ∨ 0 ≤ p) :
continuous_on (λ (x : α), f x ^ p) s
source
theorem continuous.rpow_const {α : Type u_1} [topological_space α] {f : α → ℝ} {p : ℝ} (hf : continuous f) (h : ∀ (x : α), f x ≠ 0 ∨ 0 ≤ p) :
continuous (λ (x : α), f x ^ p)
source
theorem real.sqrt_eq_rpow (x : ℝ) :
√ x = x ^ (1 / 2)
source
theorem real.rpow_div_two_eq_sqrt {x : ℝ} (r : ℝ) (hx : 0 ≤ x) :
x ^ (r / 2) = √ x ^ r
source
theorem tendsto_rpow_at_top {y : ℝ} (hy : 0 < y) :
filter.tendsto (λ (x : ℝ), x ^ y) filter.at_top filter.at_top

The function x ^ y tends to +∞ at +∞ for any positive real y.

source
theorem tendsto_rpow_neg_at_top {y : ℝ} (hy : 0 < y) :
filter.tendsto (λ (x : ℝ), x ^ -y) filter.at_top (nhds 0)

The function x ^ (-y) tends to 0 at +∞ for any positive real y.

source
theorem tendsto_rpow_div_mul_add (a b c : ℝ) (hb : 0 ≠ b) :
filter.tendsto (λ (x : ℝ), x ^ (a / (b * x + c))) filter.at_top (nhds 1)

The function x ^ (a / (b * x + c)) tends to 1 at +∞, for any real numbers a, b, and c such that b is nonzero.

source
theorem tendsto_rpow_div  :
filter.tendsto (λ (x : ℝ), x ^ (1 / x)) filter.at_top (nhds 1)

The function x ^ (1 / x) tends to 1 at +∞.

source
theorem tendsto_rpow_neg_div  :
filter.tendsto (λ (x : ℝ), x ^ ((-1) / x)) filter.at_top (nhds 1)

The function x ^ (-1 / x) tends to 1 at +∞.

source
theorem tendsto_exp_div_rpow_at_top (s : ℝ) :
filter.tendsto (λ (x : ℝ), rexp x / x ^ s) filter.at_top filter.at_top

The function exp(x) / x ^ s tends to +∞ at +∞, for any real number s.

source
theorem tendsto_exp_mul_div_rpow_at_top (s b : ℝ) (hb : 0 < b) :
filter.tendsto (λ (x : ℝ), rexp (b * x) / x ^ s) filter.at_top filter.at_top

The function exp (b * x) / x ^ s tends to +∞ at +∞, for any real s and b > 0.

source
theorem tendsto_rpow_mul_exp_neg_mul_at_top_nhds_0 (s b : ℝ) (hb : 0 < b) :
filter.tendsto (λ (x : ℝ), x ^ s * rexp (-b * x)) filter.at_top (nhds 0)

The function x ^ s * exp (-b * x) tends to 0 at +∞, for any real s and b > 0.

source
theorem asymptotics.is_O_with.rpow {α : Type u_1} {r c : ℝ} {l : filter α} {f g : α → ℝ} (h : asymptotics.is_O_with c l f g) (hc : 0 ≤ c) (hr : 0 ≤ r) (hg : 0 ≤ᶠ[l] g) :
asymptotics.is_O_with (c ^ r) l (λ (x : α), f x ^ r) (λ (x : α), g x ^ r)
source
theorem asymptotics.is_O.rpow {α : Type u_1} {r : ℝ} {l : filter α} {f g : α → ℝ} (hr : 0 ≤ r) (hg : 0 ≤ᶠ[l] g) (h : f =O[l] g) :
(λ (x : α), f x ^ r) =O[l] λ (x : α), g x ^ r
source
theorem asymptotics.is_o.rpow {α : Type u_1} {r : ℝ} {l : filter α} {f g : α → ℝ} (hr : 0 < r) (hg : 0 ≤ᶠ[l] g) (h : f =o[l] g) :
(λ (x : α), f x ^ r) =o[l] λ (x : α), g x ^ r
source
theorem is_o_rpow_exp_pos_mul_at_top (s : ℝ) {b : ℝ} (hb : 0 < b) :
(λ (x : ℝ), x ^ s) =o[filter.at_top] λ (x : ℝ), rexp (b * x)

x ^ s = o(exp(b * x)) as x → ∞ for any real s and positive b.

source
theorem is_o_zpow_exp_pos_mul_at_top (k : ℤ) {b : ℝ} (hb : 0 < b) :
(λ (x : ℝ), x ^ k) =o[filter.at_top] λ (x : ℝ), rexp (b * x)

x ^ k = o(exp(b * x)) as x → ∞ for any integer k and positive b.

source
theorem is_o_pow_exp_pos_mul_at_top (k : ℕ) {b : ℝ} (hb : 0 < b) :
(λ (x : ℝ), x ^ k) =o[filter.at_top] λ (x : ℝ), rexp (b * x)

x ^ k = o(exp(b * x)) as x → ∞ for any natural k and positive b.

source
theorem is_o_rpow_exp_at_top (s : ℝ) :
(λ (x : ℝ), x ^ s) =o[filter.at_top] rexp

x ^ s = o(exp x) as x → ∞ for any real s.

source
theorem is_o_log_rpow_at_top {r : ℝ} (hr : 0 < r) :
real.log =o[filter.at_top] λ (x : ℝ), x ^ r
source
theorem is_o_log_rpow_rpow_at_top {s : ℝ} (r : ℝ) (hs : 0 < s) :
(λ (x : ℝ), real.log x ^ r) =o[filter.at_top] λ (x : ℝ), x ^ s
source
theorem is_o_abs_log_rpow_rpow_nhds_zero {s : ℝ} (r : ℝ) (hs : s < 0) :
(λ (x : ℝ), |real.log x| ^ r) =o[nhds_within 0 (set.Ioi 0)] λ (x : ℝ), x ^ s
source
theorem is_o_log_rpow_nhds_zero {r : ℝ} (hr : r < 0) :
real.log =o[nhds_within 0 (set.Ioi 0)] λ (x : ℝ), x ^ r
source
theorem tendsto_log_div_rpow_nhds_zero {r : ℝ} (hr : r < 0) :
filter.tendsto (λ (x : ℝ), real.log x / x ^ r) (nhds_within 0 (set.Ioi 0)) (nhds 0)
source
theorem tendsto_log_mul_rpow_nhds_zero {r : ℝ} (hr : 0 < r) :
filter.tendsto (λ (x : ℝ), real.log x * x ^ r) (nhds_within 0 (set.Ioi 0)) (nhds 0)
source
theorem complex.continuous_at_cpow_zero_of_re_pos {z : ℂ} (hz : 0 < z.re) :
continuous_at (λ (x : ℂ × ℂ), x.fst ^ x.snd) (0, z)

See also continuous_at_cpow and complex.continuous_at_cpow_of_re_pos.

source
theorem complex.continuous_at_cpow_of_re_pos {p : ℂ × ℂ} (h₁ : 0 ≤ p.fst.re ∨ p.fst.im ≠ 0) (h₂ : 0 < p.snd.re) :
continuous_at (λ (x : ℂ × ℂ), x.fst ^ x.snd) p

See also continuous_at_cpow for a version that assumes p.1 ≠ 0 but makes no assumptions about p.2.

source
theorem complex.continuous_at_cpow_const_of_re_pos {z w : ℂ} (hz : 0 ≤ z.re ∨ z.im ≠ 0) (hw : 0 < w.re) :
continuous_at (λ (x : ℂ), x ^ w) z

See also continuous_at_cpow_const for a version that assumes z ≠ 0 but makes no assumptions about w.

source
theorem complex.continuous_at_of_real_cpow (x : ℝ) (y : ℂ) (h : 0 < y.re ∨ x ≠ 0) :
continuous_at (λ (p : ℝ × ℂ), ↑(p.fst) ^ p.snd) (x, y)

Continuity of (x, y) ↦ x ^ y as a function on ℝ × ℂ.

source
theorem complex.continuous_at_of_real_cpow_const (x : ℝ) (y : ℂ) (h : 0 < y.re ∨ x ≠ 0) :
continuous_at (λ (a : ℝ), ↑a ^ y) x
source
theorem complex.continuous_of_real_cpow_const {y : ℂ} (hs : 0 < y.re) :
continuous (λ (x : ℝ), ↑x ^ y)
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 nnreal.continuous_at_rpow {x : nnreal} {y : ℝ} (h : x ≠ 0 ∨ 0 < y) :
continuous_at (λ (p : nnreal × ℝ), p.fst ^ p.snd) (x, y)
source
theorem real.to_nnreal_rpow_of_nonneg {x y : ℝ} (hx : 0 ≤ x) :
(x ^ y).to_nnreal = x.to_nnreal ^ y
source
theorem nnreal.eventually_pow_one_div_le (x : nnreal) {y : nnreal} (hy : 1 < y) :
∀ᶠ (n : ℕ) in filter.at_top, x ^ (1 / ↑n) ≤ y
source
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
source
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
source
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.

source
theorem filter.tendsto.nnrpow {α : Type u_1} {f : filter α} {u : α → nnreal} {v : α → ℝ} {x : nnreal} {y : ℝ} (hx : filter.tendsto u f (nhds x)) (hy : filter.tendsto v f (nhds y)) (h : x ≠ 0 ∨ 0 < y) :
filter.tendsto (λ (a : α), u a ^ v a) f (nhds (x ^ y))
source
theorem nnreal.continuous_at_rpow_const {x : nnreal} {y : ℝ} (h : x ≠ 0 ∨ 0 ≤ y) :
continuous_at (λ (z : nnreal), z ^ y) x
source
theorem nnreal.continuous_rpow_const {y : ℝ} (h : 0 ≤ y) :
continuous (λ (x : nnreal), x ^ y)
source
theorem nnreal.tendsto_rpow_at_top {y : ℝ} (hy : 0 < y) :
filter.tendsto (λ (x : nnreal), x ^ y) filter.at_top filter.at_top
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)
source
theorem ennreal.tendsto_rpow_at_top {y : ℝ} (hy : 0 < y) :
filter.tendsto (λ (x : ennreal), x ^ y) (nhds ⊤) (nhds ⊤)
source
theorem ennreal.eventually_pow_one_div_le {x : ennreal} (hx : x ≠ ⊤) {y : ennreal} (hy : 1 < y) :
∀ᶠ (n : ℕ) in filter.at_top, x ^ (1 / ↑n) ≤ y
source
@[continuity]
theorem ennreal.continuous_rpow_const {y : ℝ} :
continuous (λ (a : ennreal), a ^ y)
source
theorem ennreal.tendsto_const_mul_rpow_nhds_zero_of_pos {c : ennreal} (hc : c ≠ ⊤) {y : ℝ} (hy : 0 < y) :
filter.tendsto (λ (x : ennreal), c * x ^ y) (nhds 0) (nhds 0)
source
theorem filter.tendsto.ennrpow_const {α : Type u_1} {f : filter α} {m : α → ennreal} {a : ennreal} (r : ℝ) (hm : filter.tendsto m f (nhds a)) :
filter.tendsto (λ (x : α), m x ^ r) f (nhds (a ^ r))
source
theorem norm_num.rpow_pos (a b : ℝ) (b' : ℕ) (c : ℝ) (hb : ↑b' = b) (h : a ^ b' = c) :
a ^ b = c
source
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'
source
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.)

source
meta def norm_num.prove_rpow' (pos neg zero : name) (α β one a b : expr) :
tactic (expr × expr)

Generalized version of prove_cpow, prove_nnrpow, prove_ennrpow.

source
theorem norm_num.cpow_pos (a b : ℂ) (b' : ℕ) (c : ℂ) (hb : b = ↑b') (h : a ^ b' = c) :
a ^ b = c
source
theorem norm_num.cpow_neg (a b : ℂ) (b' : ℕ) (c c' : ℂ) (hb : b = ↑b') (h : a ^ b' = c) (hc : c⁻¹ = c') :
a ^ -b = c'
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_cpow  :
expr → expr → tactic (expr × expr)

Evaluate complex.cpow a b where a is a rational numeral and b is an integer.

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_rpow_cpow  :
expr → tactic (expr × expr)

Evaluates expressions of the form rpow a b, cpow 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_rpow (a b : expr) :
tactic tactic.positivity.strictness

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

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