mathlib docs: analysis.special

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

x.cpow y = ite (x = 0) (ite (y = 0) 1 0) (complex.exp (x.log * y))

source

@[instance]

def complex.has_pow :

has_pow ℂ ℂ

Equations

complex.has_pow = {pow := complex.cpow}

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) (complex.exp (x.log * 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 : ℂ} :

x ≠ 0 → 0 ^ x = 0

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 : ℂ) :

x ≠ 0 → x ^ (y + z) = x ^ y * x ^ z

source

theorem complex.cpow_mul {x y : ℂ} (z : ℂ) :

-real.pi < (x.log * y).im → (x.log * 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_neg_one (x : ℂ) :

x ^ -1 = x⁻¹

source

@[simp]

theorem complex.cpow_nat_cast (x : ℂ) (n : ℕ) :

x ^ ↑n = x ^ n

source

@[simp]

theorem complex.cpow_int_cast (x : ℂ) (n : ℤ) :

x ^ ↑n = x ^ n

source

theorem complex.cpow_nat_inv_pow (x : ℂ) {n : ℕ} :

0 < n → (x ^ (↑n)⁻¹) ^ n = x

source

def real.rpow :

ℝ → ℝ → ℝ

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

source

@[instance]

def real.has_pow :

has_pow ℝ ℝ

Equations

real.has_pow = {pow := real.rpow}

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) (real.exp (real.log x * y))

source

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

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

source

theorem real.rpow_eq_zero_iff_of_nonneg {x y : ℝ} :

0 ≤ x → (x ^ y = 0 ↔ x = 0 ∧ y ≠ 0)

source

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

x ^ y = real.exp (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) (real.exp (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

theorem real.abs_rpow_le_abs_rpow (x y : ℝ) :

abs (x ^ y) ≤ abs x ^ y

source

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

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

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

@[simp]

theorem real.rpow_zero (x : ℝ) :

x ^ 0 = 1

source

@[simp]

theorem real.zero_rpow {x : ℝ} :

x ≠ 0 → 0 ^ x = 0

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.rpow_add {x : ℝ} (hx : 0 < x) (y z : ℝ) :

x ^ (y + z) = x ^ y * x ^ z

source

theorem real.rpow_add' {x : ℝ} (hx : 0 ≤ x) {y z : ℝ} :

y + z ≠ 0 → 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_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 : ℝ} :

y - z ≠ 0 → x ^ (y - z) = x ^ y / x ^ z

source

@[simp]

theorem real.rpow_nat_cast (x : ℝ) (n : ℕ) :

x ^ ↑n = x ^ n

source

@[simp]

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

x ^ ↑n = x ^ n

source

theorem real.rpow_neg_one (x : ℝ) :

x ^ -1 = x⁻¹

source

theorem real.mul_rpow {x y z : ℝ} :

0 ≤ x → 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.rpow_lt_rpow {x y z : ℝ} :

0 ≤ x → x < y → 0 < z → x ^ z < y ^ z

source

theorem real.rpow_le_rpow {x y z : ℝ} :

0 ≤ x → x ≤ y → 0 ≤ z → x ^ z ≤ y ^ z

source

theorem real.rpow_lt_rpow_iff {x y z : ℝ} :

0 ≤ x → 0 ≤ y → 0 < z → (x ^ z < y ^ z ↔ x < y)

source

theorem real.rpow_le_rpow_iff {x y z : ℝ} :

0 ≤ x → 0 ≤ y → 0 < z → (x ^ z ≤ y ^ z ↔ x ≤ y)

source

theorem real.rpow_lt_rpow_of_exponent_lt {x y z : ℝ} :

1 < x → y < z → x ^ y < x ^ z

source

theorem real.rpow_le_rpow_of_exponent_le {x y z : ℝ} :

1 ≤ x → y ≤ z → x ^ y ≤ x ^ z

source

theorem real.rpow_lt_rpow_of_exponent_gt {x y z : ℝ} :

0 < x → x < 1 → z < y → x ^ y < x ^ z

source

theorem real.rpow_le_rpow_of_exponent_ge {x y z : ℝ} :

0 < x → x ≤ 1 → z ≤ y → x ^ y ≤ x ^ z

source

theorem real.rpow_lt_one {x z : ℝ} :

0 ≤ x → x < 1 → 0 < z → x ^ z < 1

source

theorem real.rpow_le_one {x z : ℝ} :

0 ≤ x → x ≤ 1 → 0 ≤ z → x ^ z ≤ 1

source

theorem real.rpow_lt_one_of_one_lt_of_neg {x z : ℝ} :

1 < x → z < 0 → x ^ z < 1

source

theorem real.rpow_le_one_of_one_le_of_nonpos {x z : ℝ} :

1 ≤ x → z ≤ 0 → x ^ z ≤ 1

source

theorem real.one_lt_rpow {x z : ℝ} :

1 < x → 0 < z → 1 < x ^ z

source

theorem real.one_le_rpow {x z : ℝ} :

1 ≤ x → 0 ≤ z → 1 ≤ x ^ z

source

theorem real.one_lt_rpow_of_pos_of_lt_one_of_neg {x z : ℝ} :

0 < x → x < 1 → z < 0 → 1 < x ^ z

source

theorem real.one_le_rpow_of_pos_of_le_one_of_nonpos {x z : ℝ} :

0 < x → x ≤ 1 → z ≤ 0 → 1 ≤ x ^ z

source

theorem real.pow_nat_rpow_nat_inv {x : ℝ} (hx : 0 ≤ x) {n : ℕ} :

0 < n → (x ^ n) ^ (↑n)⁻¹ = x

source

theorem real.rpow_nat_inv_pow_nat {x : ℝ} (hx : 0 ≤ x) {n : ℕ} :

0 < n → (x ^ (↑n)⁻¹) ^ n = x

source

theorem real.continuous_rpow_aux1 :

continuous (λ (p : {p // 0 < p.fst}), p.val.fst ^ p.val.snd)

source

theorem real.continuous_rpow_aux2 :

continuous (λ (p : {p // p.fst < 0}), p.val.fst ^ p.val.snd)

source

theorem real.continuous_at_rpow_of_ne_zero {x : ℝ} (hx : x ≠ 0) (y : ℝ) :

continuous_at (λ (p : ℝ × ℝ), p.fst ^ p.snd) (x, y)

source

theorem real.continuous_rpow_aux3 :

continuous (λ (p : {p // 0 < p.snd}), p.val.fst ^ p.val.snd)

source

theorem real.continuous_at_rpow_of_pos {y : ℝ} (hy : 0 < y) (x : ℝ) :

continuous_at (λ (p : ℝ × ℝ), p.fst ^ p.snd) (x, y)

source

theorem real.continuous_at_rpow {x y : ℝ} :

x ≠ 0 ∨ 0 < y → continuous_at (λ (p : ℝ × ℝ), p.fst ^ p.snd) (x, y)

source

theorem real.continuous_rpow {α : Type u_1} [topological_space α] {f g : α → ℝ} :

(∀ (a : α), f a ≠ 0 ∨ 0 < g a) → continuous f → continuous g → continuous (λ (a : α), f a ^ g a)

real.rpow is continuous at all points except for the lower half of the y-axis. In other words, the function λp:ℝ×ℝ, p.1^p.2 is continuous at (x, y) if x ≠ 0 or y > 0.

Multiple forms of the claim is provided in the current section.

source

theorem real.continuous_rpow_of_ne_zero {α : Type u_1} [topological_space α] {f g : α → ℝ} :

(∀ (a : α), f a ≠ 0) → continuous f → continuous g → continuous (λ (a : α), f a ^ g a)

source

theorem real.continuous_rpow_of_pos {α : Type u_1} [topological_space α] {f g : α → ℝ} :

(∀ (a : α), 0 < g a) → continuous f → continuous g → continuous (λ (a : α), f a ^ g a)

source

theorem real.has_deriv_at_rpow_of_pos {x : ℝ} (h : 0 < x) (p : ℝ) :

has_deriv_at (λ (x : ℝ), x ^ p) (p * x ^ (p - 1)) x

source

theorem real.has_deriv_at_rpow_of_neg {x : ℝ} (h : x < 0) (p : ℝ) :

has_deriv_at (λ (x : ℝ), x ^ p) (p * x ^ (p - 1)) x

source

theorem real.has_deriv_at_rpow {x : ℝ} (h : x ≠ 0) (p : ℝ) :

has_deriv_at (λ (x : ℝ), x ^ p) (p * x ^ (p - 1)) x

source

theorem real.has_deriv_at_rpow_zero_of_one_le {p : ℝ} :

1 ≤ p → has_deriv_at (λ (x : ℝ), x ^ p) (p * 0 ^ (p - 1)) 0

source

theorem real.has_deriv_at_rpow_of_one_le (x : ℝ) {p : ℝ} :

1 ≤ p → has_deriv_at (λ (x : ℝ), x ^ p) (p * x ^ (p - 1)) x

source

theorem real.sqrt_eq_rpow :

real.sqrt = λ (x : ℝ), x ^ (1 / 2)

source

theorem real.continuous_sqrt :

continuous real.sqrt

source

theorem has_deriv_within_at.rpow {f : ℝ → ℝ} {x f' : ℝ} {s : set ℝ} (p : ℝ) :

has_deriv_within_at f f' s x → f x ≠ 0 → has_deriv_within_at (λ (y : ℝ), f y ^ p) (f' * p * f x ^ (p - 1)) s x

source

theorem has_deriv_at.rpow {f : ℝ → ℝ} {x f' : ℝ} (p : ℝ) :

has_deriv_at f f' x → f x ≠ 0 → has_deriv_at (λ (y : ℝ), f y ^ p) (f' * p * f x ^ (p - 1)) x

source

theorem differentiable_within_at.rpow {f : ℝ → ℝ} {x : ℝ} {s : set ℝ} (p : ℝ) :

differentiable_within_at ℝ f s x → f x ≠ 0 → differentiable_within_at ℝ (λ (x : ℝ), f x ^ p) s x

source

@[simp]

theorem differentiable_at.rpow {f : ℝ → ℝ} {x : ℝ} (p : ℝ) :

differentiable_at ℝ f x → f x ≠ 0 → differentiable_at ℝ (λ (x : ℝ), f x ^ p) x

source

theorem differentiable_on.rpow {f : ℝ → ℝ} {s : set ℝ} (p : ℝ) :

differentiable_on ℝ f s → (∀ (x : ℝ), x ∈ s → f x ≠ 0) → differentiable_on ℝ (λ (x : ℝ), f x ^ p) s

source

@[simp]

theorem differentiable.rpow {f : ℝ → ℝ} (p : ℝ) :

differentiable ℝ f → (∀ (x : ℝ), f x ≠ 0) → differentiable ℝ (λ (x : ℝ), f x ^ p)

source

theorem deriv_within_rpow {f : ℝ → ℝ} {x : ℝ} {s : set ℝ} (p : ℝ) :

differentiable_within_at ℝ f s x → f x ≠ 0 → unique_diff_within_at ℝ s x → deriv_within (λ (x : ℝ), f x ^ p) s x = deriv_within f s x * p * f x ^ (p - 1)

source

@[simp]

theorem deriv_rpow {f : ℝ → ℝ} {x : ℝ} (p : ℝ) :

differentiable_at ℝ f x → f x ≠ 0 → deriv (λ (x : ℝ), f x ^ p) x = deriv f x * p * f x ^ (p - 1)

source

theorem has_deriv_within_at.rpow_of_one_le {f : ℝ → ℝ} {x f' : ℝ} {s : set ℝ} {p : ℝ} :

has_deriv_within_at f f' s x → 1 ≤ p → has_deriv_within_at (λ (y : ℝ), f y ^ p) (f' * p * f x ^ (p - 1)) s x

source

theorem has_deriv_at.rpow_of_one_le {f : ℝ → ℝ} {x f' p : ℝ} :

has_deriv_at f f' x → 1 ≤ p → has_deriv_at (λ (y : ℝ), f y ^ p) (f' * p * f x ^ (p - 1)) x

source

theorem differentiable_within_at.rpow_of_one_le {f : ℝ → ℝ} {x : ℝ} {s : set ℝ} {p : ℝ} :

differentiable_within_at ℝ f s x → 1 ≤ p → differentiable_within_at ℝ (λ (x : ℝ), f x ^ p) s x

source

@[simp]

theorem differentiable_at.rpow_of_one_le {f : ℝ → ℝ} {x p : ℝ} :

differentiable_at ℝ f x → 1 ≤ p → differentiable_at ℝ (λ (x : ℝ), f x ^ p) x

source

theorem differentiable_on.rpow_of_one_le {f : ℝ → ℝ} {s : set ℝ} {p : ℝ} :

differentiable_on ℝ f s → 1 ≤ p → differentiable_on ℝ (λ (x : ℝ), f x ^ p) s

source

@[simp]

theorem differentiable.rpow_of_one_le {f : ℝ → ℝ} {p : ℝ} :

differentiable ℝ f → 1 ≤ p → differentiable ℝ (λ (x : ℝ), f x ^ p)

source

theorem deriv_within_rpow_of_one_le {f : ℝ → ℝ} {x : ℝ} {s : set ℝ} {p : ℝ} :

differentiable_within_at ℝ f s x → 1 ≤ p → unique_diff_within_at ℝ s x → deriv_within (λ (x : ℝ), f x ^ p) s x = deriv_within f s x * p * f x ^ (p - 1)

source

@[simp]

theorem deriv_rpow_of_one_le {f : ℝ → ℝ} {x p : ℝ} :

differentiable_at ℝ f x → 1 ≤ p → deriv (λ (x : ℝ), f x ^ p) x = deriv f x * p * f x ^ (p - 1)

source

theorem has_deriv_within_at.sqrt {f : ℝ → ℝ} {x f' : ℝ} {s : set ℝ} :

has_deriv_within_at f f' s x → f x ≠ 0 → has_deriv_within_at (λ (y : ℝ), real.sqrt (f y)) (f' / (2 * real.sqrt (f x))) s x

source

theorem has_deriv_at.sqrt {f : ℝ → ℝ} {x f' : ℝ} :

has_deriv_at f f' x → f x ≠ 0 → has_deriv_at (λ (y : ℝ), real.sqrt (f y)) (f' / (2 * real.sqrt (f x))) x

source

theorem differentiable_within_at.sqrt {f : ℝ → ℝ} {x : ℝ} {s : set ℝ} :

differentiable_within_at ℝ f s x → f x ≠ 0 → differentiable_within_at ℝ (λ (x : ℝ), real.sqrt (f x)) s x

source

@[simp]

theorem differentiable_at.sqrt {f : ℝ → ℝ} {x : ℝ} :

differentiable_at ℝ f x → f x ≠ 0 → differentiable_at ℝ (λ (x : ℝ), real.sqrt (f x)) x

source

theorem differentiable_on.sqrt {f : ℝ → ℝ} {s : set ℝ} :

differentiable_on ℝ f s → (∀ (x : ℝ), x ∈ s → f x ≠ 0) → differentiable_on ℝ (λ (x : ℝ), real.sqrt (f x)) s

source

@[simp]

theorem differentiable.sqrt {f : ℝ → ℝ} :

differentiable ℝ f → (∀ (x : ℝ), f x ≠ 0) → differentiable ℝ (λ (x : ℝ), real.sqrt (f x))

source

theorem deriv_within_sqrt {f : ℝ → ℝ} {x : ℝ} {s : set ℝ} :

differentiable_within_at ℝ f s x → f x ≠ 0 → unique_diff_within_at ℝ s x → deriv_within (λ (x : ℝ), real.sqrt (f x)) s x = deriv_within f s x / (2 * real.sqrt (f x))

source

@[simp]

theorem deriv_sqrt {f : ℝ → ℝ} {x : ℝ} :

differentiable_at ℝ f x → f x ≠ 0 → deriv (λ (x : ℝ), real.sqrt (f x)) x = deriv f x / (2 * real.sqrt (f x))

source

def nnreal.rpow :

nnreal → ℝ → 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

x.rpow y = ⟨↑x ^ y, _⟩

source

@[instance]

def nnreal.has_pow :

has_pow nnreal ℝ

Equations

nnreal.has_pow = {pow := nnreal.rpow}

source

@[simp]

theorem nnreal.rpow_eq_pow (x : nnreal) (y : ℝ) :

x.rpow y = x ^ y

source

@[simp]

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 : ℝ} :

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 : ℝ} :

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 : ℝ} :

y - z ≠ 0 → x ^ (y - z) = x ^ y / x ^ z

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

@[simp]

theorem nnreal.rpow_nat_cast (x : nnreal) (n : ℕ) :

x ^ ↑n = x ^ n

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 : ℝ} :

x ≤ y → 0 ≤ z → x ^ z ≤ y ^ z

source

theorem nnreal.rpow_lt_rpow {x y : nnreal} {z : ℝ} :

x < y → 0 < z → x ^ z < y ^ z

source

theorem nnreal.rpow_lt_rpow_iff {x y : nnreal} {z : ℝ} :

0 < z → (x ^ z < y ^ z ↔ x < y)

source

theorem nnreal.rpow_le_rpow_iff {x y : nnreal} {z : ℝ} :

0 < z → (x ^ z ≤ y ^ z ↔ x ≤ y)

source

theorem nnreal.rpow_lt_rpow_of_exponent_lt {x : nnreal} {y z : ℝ} :

1 < x → y < z → x ^ y < x ^ z

source

theorem nnreal.rpow_le_rpow_of_exponent_le {x : nnreal} {y z : ℝ} :

1 ≤ x → y ≤ z → x ^ y ≤ x ^ z

source

theorem nnreal.rpow_lt_rpow_of_exponent_gt {x : nnreal} {y z : ℝ} :

0 < x → x < 1 → z < y → x ^ y < x ^ z

source

theorem nnreal.rpow_le_rpow_of_exponent_ge {x : nnreal} {y z : ℝ} :

0 < x → x ≤ 1 → z ≤ y → x ^ y ≤ x ^ z

source

theorem nnreal.rpow_lt_one {x : nnreal} {z : ℝ} :

0 ≤ x → x < 1 → 0 < z → x ^ z < 1

source

theorem nnreal.rpow_le_one {x : nnreal} {z : ℝ} :

x ≤ 1 → 0 ≤ z → x ^ z ≤ 1

source

theorem nnreal.rpow_lt_one_of_one_lt_of_neg {x : nnreal} {z : ℝ} :

1 < x → z < 0 → x ^ z < 1

source

theorem nnreal.rpow_le_one_of_one_le_of_nonpos {x : nnreal} {z : ℝ} :

1 ≤ x → z ≤ 0 → x ^ z ≤ 1

source

theorem nnreal.one_lt_rpow {x : nnreal} {z : ℝ} :

1 < x → 0 < z → 1 < x ^ z

source

theorem nnreal.one_le_rpow {x : nnreal} {z : ℝ} :

1 ≤ x → 0 ≤ z → 1 ≤ x ^ z

source

theorem nnreal.one_lt_rpow_of_pos_of_lt_one_of_neg {x : nnreal} {z : ℝ} :

0 < x → x < 1 → z < 0 → 1 < x ^ z

source

theorem nnreal.one_le_rpow_of_pos_of_le_one_of_nonpos {x : nnreal} {z : ℝ} :

0 < x → x ≤ 1 → z ≤ 0 → 1 ≤ x ^ z

source

theorem nnreal.pow_nat_rpow_nat_inv (x : nnreal) {n : ℕ} :

0 < n → (x ^ n) ^ (↑n)⁻¹ = x

source

theorem nnreal.rpow_nat_inv_pow_nat (x : nnreal) {n : ℕ} :

0 < n → (x ^ (↑n)⁻¹) ^ n = x

source

theorem nnreal.continuous_at_rpow {x : nnreal} {y : ℝ} :

x ≠ 0 ∨ 0 < y → continuous_at (λ (p : nnreal × ℝ), p.fst ^ p.snd) (x, y)

source

theorem filter.tendsto.nnrpow {α : Type u_1} {f : filter α} {u : α → nnreal} {v : α → ℝ} {x : nnreal} {y : ℝ} :

filter.tendsto u f (nhds x) → filter.tendsto v f (nhds y) → x ≠ 0 ∨ 0 < y → filter.tendsto (λ (a : α), u a ^ v a) f (nhds (x ^ y))

source

def ennreal.rpow :

ennreal → ℝ → ennreal

The real power function x^y on extended nonnegative reals, defined for x : ennreal 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).