# Continuity of power functions #

This file contains lemmas about continuity of the power functions on `ℂ`, `ℝ`, `ℝ≥0`, and `ℝ≥0∞`.

## Continuity for complex powers #

source
theorem zero_cpow_eq_nhds {b : ℂ} (hb : b ≠ 0) :
(fun (x : ℂ) => 0 ^ x) =ᶠ[nhds b] 0
source
theorem cpow_eq_nhds {a b : ℂ} (ha : a ≠ 0) :
(fun (x : ℂ) => x ^ b) =ᶠ[nhds a] fun (x : ℂ) => Complex.exp (Complex.log x * b)
source
theorem cpow_eq_nhds' {p : ℂ × ℂ} (hp_fst : p.1 ≠ 0) :
(fun (x : ℂ × ℂ) => x.1 ^ x.2) =ᶠ[nhds p] fun (x : ℂ × ℂ) => Complex.exp (Complex.log x.1 * x.2)
source
theorem continuousAt_const_cpow {a b : ℂ} (ha : a ≠ 0) :
ContinuousAt (fun (x : ℂ) => a ^ x) b
source
theorem continuousAt_const_cpow' {a b : ℂ} (h : b ≠ 0) :
ContinuousAt (fun (x : ℂ) => a ^ x) b
source
theorem continuousAt_cpow {p : ℂ × ℂ} (hp_fst : p.1 ∈ Complex.slitPlane) :
ContinuousAt (fun (x : ℂ × ℂ) => x.1 ^ x.2) 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.continuousAt_cpow_zero_of_re_pos` for a version that works for `z = 0` but assumes `0 < re w`.

source
theorem continuousAt_cpow_const {a b : ℂ} (ha : a ∈ Complex.slitPlane) :
ContinuousAt (fun (x : ℂ) => x ^ b) a
source
theorem Filter.Tendsto.cpow {α : Type u_1} {l : Filter α} {f g : α → ℂ} {a b : ℂ} (hf : Tendsto f l (nhds a)) (hg : Tendsto g l (nhds b)) (ha : a ∈ Complex.slitPlane) :
Tendsto (fun (x : α) => f x ^ g x) l (nhds (a ^ b))
source
theorem Filter.Tendsto.const_cpow {α : Type u_1} {l : Filter α} {f : α → ℂ} {a b : ℂ} (hf : Tendsto f l (nhds b)) (h : a ≠ 0 ∨ b ≠ 0) :
Tendsto (fun (x : α) => a ^ f x) l (nhds (a ^ b))
source
theorem ContinuousWithinAt.cpow {α : Type u_1} [TopologicalSpace α] {f g : α → ℂ} {s : Set α} {a : α} (hf : ContinuousWithinAt f s a) (hg : ContinuousWithinAt g s a) (h0 : f a ∈ Complex.slitPlane) :
ContinuousWithinAt (fun (x : α) => f x ^ g x) s a
source
theorem ContinuousWithinAt.const_cpow {α : Type u_1} [TopologicalSpace α] {f : α → ℂ} {s : Set α} {a : α} {b : ℂ} (hf : ContinuousWithinAt f s a) (h : b ≠ 0 ∨ f a ≠ 0) :
ContinuousWithinAt (fun (x : α) => b ^ f x) s a
source
theorem ContinuousAt.cpow {α : Type u_1} [TopologicalSpace α] {f g : α → ℂ} {a : α} (hf : ContinuousAt f a) (hg : ContinuousAt g a) (h0 : f a ∈ Complex.slitPlane) :
ContinuousAt (fun (x : α) => f x ^ g x) a
source
theorem ContinuousAt.const_cpow {α : Type u_1} [TopologicalSpace α] {f : α → ℂ} {a : α} {b : ℂ} (hf : ContinuousAt f a) (h : b ≠ 0 ∨ f a ≠ 0) :
ContinuousAt (fun (x : α) => b ^ f x) a
source
theorem ContinuousOn.cpow {α : Type u_1} [TopologicalSpace α] {f g : α → ℂ} {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) (h0 : ∀ a ∈ s, f a ∈ Complex.slitPlane) :
ContinuousOn (fun (x : α) => f x ^ g x) s
source
theorem ContinuousOn.const_cpow {α : Type u_1} [TopologicalSpace α] {f : α → ℂ} {s : Set α} {b : ℂ} (hf : ContinuousOn f s) (h : b ≠ 0 ∨ ∀ a ∈ s, f a ≠ 0) :
ContinuousOn (fun (x : α) => b ^ f x) s
source
theorem Continuous.cpow {α : Type u_1} [TopologicalSpace α] {f g : α → ℂ} (hf : Continuous f) (hg : Continuous g) (h0 : ∀ (a : α), f a ∈ Complex.slitPlane) :
Continuous fun (x : α) => f x ^ g x
source
theorem Continuous.const_cpow {α : Type u_1} [TopologicalSpace α] {f : α → ℂ} {b : ℂ} (hf : Continuous f) (h : b ≠ 0 ∨ ∀ (a : α), f a ≠ 0) :
Continuous fun (x : α) => b ^ f x
source
theorem ContinuousOn.cpow_const {α : Type u_1} [TopologicalSpace α] {f : α → ℂ} {s : Set α} {b : ℂ} (hf : ContinuousOn f s) (h : ∀ a ∈ s, f a ∈ Complex.slitPlane) :
ContinuousOn (fun (x : α) => f x ^ b) s
source
theorem continuous_const_cpow (z : ℂ) [NeZero z] :
Continuous fun (s : ℂ) => z ^ s

## Continuity for real powers #

source
theorem Real.continuousAt_const_rpow {a b : ℝ} (h : a ≠ 0) :
ContinuousAt (fun (x : ℝ) => a ^ x) b
source
theorem Real.continuousAt_const_rpow' {a b : ℝ} (h : b ≠ 0) :
ContinuousAt (fun (x : ℝ) => a ^ x) b
source
theorem Real.rpow_eq_nhds_of_neg {p : ℝ × ℝ} (hp_fst : p.1 < 0) :
(fun (x : ℝ × ℝ) => x.1 ^ x.2) =ᶠ[nhds p] fun (x : ℝ × ℝ) => exp (log x.1 * x.2) * cos (x.2 * Real.pi)
source
theorem Real.rpow_eq_nhds_of_pos {p : ℝ × ℝ} (hp_fst : 0 < p.1) :
(fun (x : ℝ × ℝ) => x.1 ^ x.2) =ᶠ[nhds p] fun (x : ℝ × ℝ) => exp (log x.1 * x.2)
source
theorem Real.continuousAt_rpow_of_ne (p : ℝ × ℝ) (hp : p.1 ≠ 0) :
ContinuousAt (fun (p : ℝ × ℝ) => p.1 ^ p.2) p
source
theorem Real.continuousAt_rpow_of_pos (p : ℝ × ℝ) (hp : 0 < p.2) :
ContinuousAt (fun (p : ℝ × ℝ) => p.1 ^ p.2) p
source
theorem Real.continuousAt_rpow (p : ℝ × ℝ) (h : p.1 ≠ 0 ∨ 0 < p.2) :
ContinuousAt (fun (p : ℝ × ℝ) => p.1 ^ p.2) p
source
theorem Real.continuousAt_rpow_const (x q : ℝ) (h : x ≠ 0 ∨ 0 ≤ q) :
ContinuousAt (fun (x : ℝ) => x ^ q) x
source
theorem Real.continuous_rpow_const {q : ℝ} (h : 0 ≤ q) :
Continuous fun (x : ℝ) => x ^ q
source
theorem Real.continuous_const_rpow {a : ℝ} (h : a ≠ 0) :
Continuous fun (x : ℝ) => a ^ x
source
theorem Filter.Tendsto.rpow {α : Type u_1} {l : Filter α} {f g : α → ℝ} {x y : ℝ} (hf : Tendsto f l (nhds x)) (hg : Tendsto g l (nhds y)) (h : x ≠ 0 ∨ 0 < y) :
Tendsto (fun (t : α) => f t ^ g t) l (nhds (x ^ y))
source
theorem Filter.Tendsto.rpow_const {α : Type u_1} {l : Filter α} {f : α → ℝ} {x p : ℝ} (hf : Tendsto f l (nhds x)) (h : x ≠ 0 ∨ 0 ≤ p) :
Tendsto (fun (a : α) => f a ^ p) l (nhds (x ^ p))
source
theorem ContinuousAt.rpow {α : Type u_1} [TopologicalSpace α] {f g : α → ℝ} {x : α} (hf : ContinuousAt f x) (hg : ContinuousAt g x) (h : f x ≠ 0 ∨ 0 < g x) :
ContinuousAt (fun (t : α) => f t ^ g t) x
source
theorem ContinuousWithinAt.rpow {α : Type u_1} [TopologicalSpace α] {f g : α → ℝ} {s : Set α} {x : α} (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) (h : f x ≠ 0 ∨ 0 < g x) :
ContinuousWithinAt (fun (t : α) => f t ^ g t) s x
source
theorem ContinuousOn.rpow {α : Type u_1} [TopologicalSpace α] {f g : α → ℝ} {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) (h : ∀ x ∈ s, f x ≠ 0 ∨ 0 < g x) :
ContinuousOn (fun (t : α) => f t ^ g t) s
source
theorem Continuous.rpow {α : Type u_1} [TopologicalSpace α] {f g : α → ℝ} (hf : Continuous f) (hg : Continuous g) (h : ∀ (x : α), f x ≠ 0 ∨ 0 < g x) :
Continuous fun (x : α) => f x ^ g x
source
theorem ContinuousWithinAt.rpow_const {α : Type u_1} [TopologicalSpace α] {f : α → ℝ} {s : Set α} {x : α} {p : ℝ} (hf : ContinuousWithinAt f s x) (h : f x ≠ 0 ∨ 0 ≤ p) :
ContinuousWithinAt (fun (x : α) => f x ^ p) s x
source
theorem ContinuousAt.rpow_const {α : Type u_1} [TopologicalSpace α] {f : α → ℝ} {x : α} {p : ℝ} (hf : ContinuousAt f x) (h : f x ≠ 0 ∨ 0 ≤ p) :
ContinuousAt (fun (x : α) => f x ^ p) x
source
theorem ContinuousOn.rpow_const {α : Type u_1} [TopologicalSpace α] {f : α → ℝ} {s : Set α} {p : ℝ} (hf : ContinuousOn f s) (h : ∀ x ∈ s, f x ≠ 0 ∨ 0 ≤ p) :
ContinuousOn (fun (x : α) => f x ^ p) s
source
theorem Continuous.rpow_const {α : Type u_1} [TopologicalSpace α] {f : α → ℝ} {p : ℝ} (hf : Continuous f) (h : ∀ (x : α), f x ≠ 0 ∨ 0 ≤ p) :
Continuous fun (x : α) => f x ^ p

## Continuity results for `cpow`, part II #

These results involve relating real and complex powers, so cannot be done higher up.

source
theorem Complex.continuousAt_cpow_zero_of_re_pos {z : ℂ} (hz : 0 < z.re) :
ContinuousAt (fun (x : ℂ × ℂ) => x.1 ^ x.2) (0, z)

See also `continuousAt_cpow` and `Complex.continuousAt_cpow_of_re_pos`.

source
theorem Complex.continuousAt_cpow_of_re_pos {p : ℂ × ℂ} (h₁ : 0 ≤ p.1.re ∨ p.1.im ≠ 0) (h₂ : 0 < p.2.re) :
ContinuousAt (fun (x : ℂ × ℂ) => x.1 ^ x.2) p

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

source
theorem Complex.continuousAt_cpow_const_of_re_pos {z w : ℂ} (hz : 0 ≤ z.re ∨ z.im ≠ 0) (hw : 0 < w.re) :
ContinuousAt (fun (x : ℂ) => x ^ w) z

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

source
theorem Complex.continuousAt_ofReal_cpow (x : ℝ) (y : ℂ) (h : 0 < y.re ∨ x ≠ 0) :
ContinuousAt (fun (p : ℝ × ℂ) => ↑p.1 ^ p.2) (x, y)

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

source
theorem Complex.continuousAt_ofReal_cpow_const (x : ℝ) (y : ℂ) (h : 0 < y.re ∨ x ≠ 0) :
ContinuousAt (fun (a : ℝ) => ↑a ^ y) x
source
theorem Complex.continuous_ofReal_cpow_const {y : ℂ} (hs : 0 < y.re) :
Continuous fun (x : ℝ) => ↑x ^ y

## Limits and continuity for `ℝ≥0` powers #

source
theorem NNReal.continuousAt_rpow {x : NNReal} {y : ℝ} (h : x ≠ 0 ∨ 0 < y) :
ContinuousAt (fun (p : NNReal × ℝ) => p.1 ^ p.2) (x, y)
source
theorem NNReal.eventually_pow_one_div_le (x : NNReal) {y : NNReal} (hy : 1 < y) :
∀ᶠ (n : ℕ) in Filter.atTop, x ^ (1 / ↑n) ≤ y
source
theorem Filter.Tendsto.nnrpow {α : Type u_1} {f : Filter α} {u : α → NNReal} {v : α → ℝ} {x : NNReal} {y : ℝ} (hx : Tendsto u f (nhds x)) (hy : Tendsto v f (nhds y)) (h : x ≠ 0 ∨ 0 < y) :
Tendsto (fun (a : α) => u a ^ v a) f (nhds (x ^ y))
source
theorem NNReal.continuousAt_rpow_const {x : NNReal} {y : ℝ} (h : x ≠ 0 ∨ 0 ≤ y) :
ContinuousAt (fun (z : NNReal) => z ^ y) x
source
theorem NNReal.continuous_rpow_const {y : ℝ} (h : 0 ≤ y) :
Continuous fun (x : NNReal) => x ^ y
source
theorem NNReal.continuousOn_rpow_const_compl_zero {r : ℝ} :
ContinuousOn (fun (z : NNReal) => z ^ r) {0}ᶜ
source
theorem NNReal.continuousOn_rpow_const {r : ℝ} {s : Set NNReal} (h : 0 ∉ s ∨ 0 ≤ r) :
ContinuousOn (fun (z : NNReal) => z ^ r) s

## Continuity for `ℝ≥0∞` powers #

source
theorem ENNReal.eventually_pow_one_div_le {x : ENNReal} (hx : x ≠ ⊤) {y : ENNReal} (hy : 1 < y) :
∀ᶠ (n : ℕ) in Filter.atTop, x ^ (1 / ↑n) ≤ y
source
theorem ENNReal.continuous_rpow_const {y : ℝ} :
Continuous fun (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 (fun (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 : Tendsto m f (nhds a)) :
Tendsto (fun (x : α) => m x ^ r) f (nhds (a ^ r))