mathlib docs: analysis.special

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

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 : ℂ} (h : 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 : ℂ) (hx : x ≠ 0) :

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

source

theorem complex.cpow_mul {x y : ℂ} (z : ℂ) (h₁ : -π < ((x.log) * y).im) (h₂ : ((x.log) * y).im ≤ π) :

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 : ℕ} (hn : 0 < n) :

(x ^ (↑n)⁻¹) ^ n = x

source

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

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 : ℝ} (hx : 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 * π)

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 * π))

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 : ℝ} (h : 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 : ℝ} (h : 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 : ℝ} (h : 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 : ℝ} (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.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.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

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

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.pow_nat_rpow_nat_inv {x : ℝ} (hx : 0 ≤ x) {n : ℕ} (hn : 0 < n) :

(x ^ n) ^ (↑n)⁻¹ = x

source

theorem real.rpow_nat_inv_pow_nat {x : ℝ} (hx : 0 ≤ x) {n : ℕ} (hn : 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 : ℝ} (h : 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 : α → ℝ} (h : ∀ (a : α), f a ≠ 0 ∨ 0 < g a) (hf : continuous f) (hg : 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 : α → ℝ} (h : ∀ (a : α), f a ≠ 0) (hf : continuous f) (hg : continuous g) :

continuous (λ (a : α), f a ^ g a)

source

theorem real.continuous_rpow_of_pos {α : Type u_1} [topological_space α] {f g : α → ℝ} (h : ∀ (a : α), 0 < g a) (hf : continuous f) (hg : 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 : ℝ} (h : 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 : ℝ} (h : 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 : ℝ) (hf : has_deriv_within_at f f' s x) (hx : 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 : ℝ) (hf : has_deriv_at f f' x) (hx : 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 : ℝ) (hf : differentiable_within_at ℝ f s x) (hx : f x ≠ 0) :

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

source

@[simp]

theorem differentiable_at.rpow {f : ℝ → ℝ} {x : ℝ} (p : ℝ) (hf : differentiable_at ℝ f x) (hx : f x ≠ 0) :

differentiable_at ℝ (λ (x : ℝ), f x ^ p) x

source

theorem differentiable_on.rpow {f : ℝ → ℝ} {s : set ℝ} (p : ℝ) (hf : differentiable_on ℝ f s) (hx : ∀ (x : ℝ), x ∈ s → f x ≠ 0) :

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

source

@[simp]

theorem differentiable.rpow {f : ℝ → ℝ} (p : ℝ) (hf : differentiable ℝ f) (hx : ∀ (x : ℝ), f x ≠ 0) :

differentiable ℝ (λ (x : ℝ), f x ^ p)

source

theorem deriv_within_rpow {f : ℝ → ℝ} {x : ℝ} {s : set ℝ} (p : ℝ) (hf : differentiable_within_at ℝ f s x) (hx : f x ≠ 0) (hxs : 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 : ℝ) (hf : differentiable_at ℝ f x) (hx : 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 : ℝ} (hf : has_deriv_within_at f f' s x) (hp : 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 : ℝ} (hf : has_deriv_at f f' x) (hp : 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 : ℝ} (hf : differentiable_within_at ℝ f s x) (hp : 1 ≤ p) :

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

source

@[simp]

theorem differentiable_at.rpow_of_one_le {f : ℝ → ℝ} {x p : ℝ} (hf : differentiable_at ℝ f x) (hp : 1 ≤ p) :

differentiable_at ℝ (λ (x : ℝ), f x ^ p) x

source

theorem differentiable_on.rpow_of_one_le {f : ℝ → ℝ} {s : set ℝ} {p : ℝ} (hf : differentiable_on ℝ f s) (hp : 1 ≤ p) :

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

source

@[simp]

theorem differentiable.rpow_of_one_le {f : ℝ → ℝ} {p : ℝ} (hf : differentiable ℝ f) (hp : 1 ≤ p) :

differentiable ℝ (λ (x : ℝ), f x ^ p)

source

theorem deriv_within_rpow_of_one_le {f : ℝ → ℝ} {x : ℝ} {s : set ℝ} {p : ℝ} (hf : differentiable_within_at ℝ f s x) (hp : 1 ≤ p) (hxs : 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 : ℝ} (hf : differentiable_at ℝ f x) (hp : 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 ℝ} (hf : has_deriv_within_at f f' s x) (hx : 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' : ℝ} (hf : has_deriv_at f f' x) (hx : 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 ℝ} (hf : differentiable_within_at ℝ f s x) (hx : f x ≠ 0) :

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

source

@[simp]

theorem differentiable_at.sqrt {f : ℝ → ℝ} {x : ℝ} (hf : differentiable_at ℝ f x) (hx : f x ≠ 0) :

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

source

theorem differentiable_on.sqrt {f : ℝ → ℝ} {s : set ℝ} (hf : differentiable_on ℝ f s) (hx : ∀ (x : ℝ), x ∈ s → f x ≠ 0) :

differentiable_on ℝ (λ (x : ℝ), real.sqrt (f x)) s

source

@[simp]

theorem differentiable.sqrt {f : ℝ → ℝ} (hf : differentiable ℝ f) (hx : ∀ (x : ℝ), f x ≠ 0) :

differentiable ℝ (λ (x : ℝ), real.sqrt (f x))

source

theorem deriv_within_sqrt {f : ℝ → ℝ} {x : ℝ} {s : set ℝ} (hf : differentiable_within_at ℝ f s x) (hx : f x ≠ 0) (hxs : 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 : ℝ} (hf : differentiable_at ℝ f x) (hx : f x ≠ 0) :

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

source

def nnreal.rpow (x : ℝ≥0) (y : ℝ) :

ℝ≥0

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 ℝ≥0 ℝ

Equations

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

source

@[simp]

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

x.rpow y = x ^ y

source

@[simp]

theorem nnreal.coe_rpow (x : ℝ≥0) (y : ℝ) :

↑(x ^ y) = ↑x ^ y

source

@[simp]

theorem nnreal.rpow_zero (x : ℝ≥0) :

x ^ 0 = 1

source

@[simp]

theorem nnreal.rpow_eq_zero_iff {x : ℝ≥0} {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 : ℝ≥0) :

x ^ 1 = x

source

@[simp]

theorem nnreal.one_rpow (x : ℝ) :

1 ^ x = 1

source

theorem nnreal.rpow_add {x : ℝ≥0} (hx : x ≠ 0) (y z : ℝ) :

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

source

theorem nnreal.rpow_add' (x : ℝ≥0) {y z : ℝ} (h : y + z ≠ 0) :

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

source

theorem nnreal.rpow_mul (x : ℝ≥0) (y z : ℝ) :

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

source

theorem nnreal.rpow_neg (x : ℝ≥0) (y : ℝ) :

x ^ -y = (x ^ y)⁻¹

source

theorem nnreal.rpow_neg_one (x : ℝ≥0) :

x ^ -1 = x⁻¹

source

theorem nnreal.rpow_sub {x : ℝ≥0} (hx : x ≠ 0) (y z : ℝ) :

x ^ (y - z) = x ^ y / x ^ z

source

theorem nnreal.rpow_sub' (x : ℝ≥0) {y z : ℝ} (h : y - z ≠ 0) :

x ^ (y - z) = x ^ y / x ^ z

source

theorem nnreal.inv_rpow (x : ℝ≥0) (y : ℝ) :

x⁻¹ ^ y = (x ^ y)⁻¹

source

theorem nnreal.div_rpow (x y : ℝ≥0) (z : ℝ) :

(x / y) ^ z = x ^ z / y ^ z

source

@[simp]

theorem nnreal.rpow_nat_cast (x : ℝ≥0) (n : ℕ) :

x ^ ↑n = x ^ n

source

theorem nnreal.mul_rpow {x y : ℝ≥0} {z : ℝ} :

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

source

theorem nnreal.rpow_le_rpow {x y : ℝ≥0} {z : ℝ} (h₁ : x ≤ y) (h₂ : 0 ≤ z) :

x ^ z ≤ y ^ z

source

theorem nnreal.rpow_lt_rpow {x y : ℝ≥0} {z : ℝ} (h₁ : x < y) (h₂ : 0 < z) :

x ^ z < y ^ z

source

theorem nnreal.rpow_lt_rpow_iff {x y : ℝ≥0} {z : ℝ} (hz : 0 < z) :

x ^ z < y ^ z ↔ x < y

source

theorem nnreal.rpow_le_rpow_iff {x y : ℝ≥0} {z : ℝ} (hz : 0 < z) :

x ^ z ≤ y ^ z ↔ x ≤ y

source

theorem nnreal.rpow_lt_rpow_of_exponent_lt {x : ℝ≥0} {y z : ℝ} (hx : 1 < x) (hyz : y < z) :

x ^ y < x ^ z

source

theorem nnreal.rpow_le_rpow_of_exponent_le {x : ℝ≥0} {y z : ℝ} (hx : 1 ≤ x) (hyz : y ≤ z) :

x ^ y ≤ x ^ z

source

theorem nnreal.rpow_lt_rpow_of_exponent_gt {x : ℝ≥0} {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 : ℝ≥0} {y z : ℝ} (hx0 : 0 < x) (hx1 : x ≤ 1) (hyz : z ≤ y) :

x ^ y ≤ x ^ z

source

theorem nnreal.rpow_lt_one {x : ℝ≥0} {z : ℝ} (hx : 0 ≤ x) (hx1 : x < 1) (hz : 0 < z) :

x ^ z < 1

source

theorem nnreal.rpow_le_one {x : ℝ≥0} {z : ℝ} (hx2 : x ≤ 1) (hz : 0 ≤ z) :

x ^ z ≤ 1

source

theorem nnreal.rpow_lt_one_of_one_lt_of_neg {x : ℝ≥0} {z : ℝ} (hx : 1 < x) (hz : z < 0) :

x ^ z < 1

source

theorem nnreal.rpow_le_one_of_one_le_of_nonpos {x : ℝ≥0} {z : ℝ} (hx : 1 ≤ x) (hz : z ≤ 0) :

x ^ z ≤ 1

source

theorem nnreal.one_lt_rpow {x : ℝ≥0} {z : ℝ} (hx : 1 < x) (hz : 0 < z) :

1 < x ^ z

source

theorem nnreal.one_le_rpow {x : ℝ≥0} {z : ℝ} (h : 1 ≤ x) (h₁ : 0 ≤ z) :

1 ≤ x ^ z

source

theorem nnreal.one_lt_rpow_of_pos_of_lt_one_of_neg {x : ℝ≥0} {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 : ℝ≥0} {z : ℝ} (hx1 : 0 < x) (hx2 : x ≤ 1) (hz : z ≤ 0) :

1 ≤ x ^ z

source

theorem nnreal.pow_nat_rpow_nat_inv (x : ℝ≥0) {n : ℕ} (hn : 0 < n) :

(x ^ n) ^ (↑n)⁻¹ = x

source

theorem nnreal.rpow_nat_inv_pow_nat (x : ℝ≥0) {n : ℕ} (hn : 0 < n) :

(x ^ (↑n)⁻¹) ^ n = x

source

theorem nnreal.continuous_at_rpow {x : ℝ≥0} {y : ℝ} (h : x ≠ 0 ∨ 0 < y) :

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

source

theorem filter.tendsto.nnrpow {α : Type u_1} {f : filter α} {u : α → ℝ≥0} {v : α → ℝ} {x : ℝ≥0} {y : ℝ} (hx : filter.tendsto u f (𝓝 x)) (hy : filter.tendsto v f (𝓝 y)) (h : x ≠ 0 ∨ 0 < y) :

filter.tendsto (λ (a : α), u a ^ v a) f (𝓝 (x ^ y))

source

theorem nnreal.continuous_at_rpow_const {x : ℝ≥0} {y : ℝ} (h : x ≠ 0 ∨ 0 ≤ y) :

continuous_at (λ (z : ℝ≥0), z ^ y) x

source

theorem nnreal.continuous_rpow_const {y : ℝ} (h : 0 ≤ y) :

continuous (λ (x : ℝ≥0), x ^ y)

source

def ennreal.rpow (a : ennreal) (a_1 : ℝ) :

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