# Continuity of power functions #

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

## Continuity for complex powers #

theorem zero_cpow_eq_nhds {b : } (hb : b 0) :
(nhds b).EventuallyEq (fun (x : ) => 0 ^ x) 0
theorem cpow_eq_nhds {a : } {b : } (ha : a 0) :
(nhds a).EventuallyEq (fun (x : ) => x ^ b) fun (x : ) => (x.log * b).exp
theorem cpow_eq_nhds' {p : } (hp_fst : p.1 0) :
(nhds p).EventuallyEq (fun (x : ) => x.1 ^ x.2) fun (x : ) => (x.1.log * x.2).exp
theorem continuousAt_const_cpow {a : } {b : } (ha : a 0) :
ContinuousAt (fun (x : ) => a ^ x) b
theorem continuousAt_const_cpow' {a : } {b : } (h : b 0) :
ContinuousAt (fun (x : ) => a ^ x) b
theorem continuousAt_cpow {p : } (hp_fst : ) :
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.

theorem continuousAt_cpow_const {a : } {b : } (ha : ) :
ContinuousAt (fun (x : ) => x ^ b) a
theorem Filter.Tendsto.cpow {α : Type u_1} {l : } {f : α} {g : α} {a : } {b : } (hf : Filter.Tendsto f l (nhds a)) (hg : Filter.Tendsto g l (nhds b)) (ha : ) :
Filter.Tendsto (fun (x : α) => f x ^ g x) l (nhds (a ^ b))
theorem Filter.Tendsto.const_cpow {α : Type u_1} {l : } {f : α} {a : } {b : } (hf : Filter.Tendsto f l (nhds b)) (h : a 0 b 0) :
Filter.Tendsto (fun (x : α) => a ^ f x) l (nhds (a ^ b))
theorem ContinuousWithinAt.cpow {α : Type u_1} [] {f : α} {g : α} {s : Set α} {a : α} (hf : ) (hg : ) (h0 : ) :
ContinuousWithinAt (fun (x : α) => f x ^ g x) s a
theorem ContinuousWithinAt.const_cpow {α : Type u_1} [] {f : α} {s : Set α} {a : α} {b : } (hf : ) (h : b 0 f a 0) :
ContinuousWithinAt (fun (x : α) => b ^ f x) s a
theorem ContinuousAt.cpow {α : Type u_1} [] {f : α} {g : α} {a : α} (hf : ) (hg : ) (h0 : ) :
ContinuousAt (fun (x : α) => f x ^ g x) a
theorem ContinuousAt.const_cpow {α : Type u_1} [] {f : α} {a : α} {b : } (hf : ) (h : b 0 f a 0) :
ContinuousAt (fun (x : α) => b ^ f x) a
theorem ContinuousOn.cpow {α : Type u_1} [] {f : α} {g : α} {s : Set α} (hf : ) (hg : ) (h0 : as, ) :
ContinuousOn (fun (x : α) => f x ^ g x) s
theorem ContinuousOn.const_cpow {α : Type u_1} [] {f : α} {s : Set α} {b : } (hf : ) (h : b 0 as, f a 0) :
ContinuousOn (fun (x : α) => b ^ f x) s
theorem Continuous.cpow {α : Type u_1} [] {f : α} {g : α} (hf : ) (hg : ) (h0 : ∀ (a : α), ) :
Continuous fun (x : α) => f x ^ g x
theorem Continuous.const_cpow {α : Type u_1} [] {f : α} {b : } (hf : ) (h : b 0 ∀ (a : α), f a 0) :
Continuous fun (x : α) => b ^ f x
theorem ContinuousOn.cpow_const {α : Type u_1} [] {f : α} {s : Set α} {b : } (hf : ) (h : as, ) :
ContinuousOn (fun (x : α) => f x ^ b) s

## Continuity for real powers #

theorem Real.continuousAt_const_rpow {a : } {b : } (h : a 0) :
ContinuousAt (fun (x : ) => a ^ x) b
theorem Real.continuousAt_const_rpow' {a : } {b : } (h : b 0) :
ContinuousAt (fun (x : ) => a ^ x) b
theorem Real.rpow_eq_nhds_of_neg {p : } (hp_fst : p.1 < 0) :
(nhds p).EventuallyEq (fun (x : ) => x.1 ^ x.2) fun (x : ) => (x.1.log * x.2).exp * (x.2 * Real.pi).cos
theorem Real.rpow_eq_nhds_of_pos {p : } (hp_fst : 0 < p.1) :
(nhds p).EventuallyEq (fun (x : ) => x.1 ^ x.2) fun (x : ) => (x.1.log * x.2).exp
theorem Real.continuousAt_rpow_of_ne (p : ) (hp : p.1 0) :
ContinuousAt (fun (p : ) => p.1 ^ p.2) p
theorem Real.continuousAt_rpow_of_pos (p : ) (hp : 0 < p.2) :
ContinuousAt (fun (p : ) => p.1 ^ p.2) p
theorem Real.continuousAt_rpow (p : ) (h : p.1 0 0 < p.2) :
ContinuousAt (fun (p : ) => p.1 ^ p.2) p
theorem Real.continuousAt_rpow_const (x : ) (q : ) (h : x 0 0 < q) :
ContinuousAt (fun (x : ) => x ^ q) x
theorem Filter.Tendsto.rpow {α : Type u_1} {l : } {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 (fun (t : α) => f t ^ g t) l (nhds (x ^ y))
theorem Filter.Tendsto.rpow_const {α : Type u_1} {l : } {f : α} {x : } {p : } (hf : Filter.Tendsto f l (nhds x)) (h : x 0 0 p) :
Filter.Tendsto (fun (a : α) => f a ^ p) l (nhds (x ^ p))
theorem ContinuousAt.rpow {α : Type u_1} [] {f : α} {g : α} {x : α} (hf : ) (hg : ) (h : f x 0 0 < g x) :
ContinuousAt (fun (t : α) => f t ^ g t) x
theorem ContinuousWithinAt.rpow {α : Type u_1} [] {f : α} {g : α} {s : Set α} {x : α} (hf : ) (hg : ) (h : f x 0 0 < g x) :
ContinuousWithinAt (fun (t : α) => f t ^ g t) s x
theorem ContinuousOn.rpow {α : Type u_1} [] {f : α} {g : α} {s : Set α} (hf : ) (hg : ) (h : xs, f x 0 0 < g x) :
ContinuousOn (fun (t : α) => f t ^ g t) s
theorem Continuous.rpow {α : Type u_1} [] {f : α} {g : α} (hf : ) (hg : ) (h : ∀ (x : α), f x 0 0 < g x) :
Continuous fun (x : α) => f x ^ g x
theorem ContinuousWithinAt.rpow_const {α : Type u_1} [] {f : α} {s : Set α} {x : α} {p : } (hf : ) (h : f x 0 0 p) :
ContinuousWithinAt (fun (x : α) => f x ^ p) s x
theorem ContinuousAt.rpow_const {α : Type u_1} [] {f : α} {x : α} {p : } (hf : ) (h : f x 0 0 p) :
ContinuousAt (fun (x : α) => f x ^ p) x
theorem ContinuousOn.rpow_const {α : Type u_1} [] {f : α} {s : Set α} {p : } (hf : ) (h : xs, f x 0 0 p) :
ContinuousOn (fun (x : α) => f x ^ p) s
theorem Continuous.rpow_const {α : Type u_1} [] {f : α} {p : } (hf : ) (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.

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.

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.

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.

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 ℝ × ℂ.

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

## Limits and continuity for ℝ≥0 powers #

theorem NNReal.continuousAt_rpow {x : NNReal} {y : } (h : x 0 0 < y) :
ContinuousAt (fun (p : ) => p.1 ^ p.2) (x, y)
theorem NNReal.eventually_pow_one_div_le (x : NNReal) {y : NNReal} (hy : 1 < y) :
∀ᶠ (n : ) in Filter.atTop, x ^ (1 / n) y
theorem Filter.Tendsto.nnrpow {α : Type u_1} {f : } {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 (fun (a : α) => u a ^ v a) f (nhds (x ^ y))
theorem NNReal.continuousAt_rpow_const {x : NNReal} {y : } (h : x 0 0 y) :
ContinuousAt (fun (z : NNReal) => z ^ y) x
theorem NNReal.continuous_rpow_const {y : } (h : 0 y) :
Continuous fun (x : NNReal) => x ^ y

## Continuity for ℝ≥0∞ powers #

theorem ENNReal.eventually_pow_one_div_le {x : ENNReal} (hx : x ) {y : ENNReal} (hy : 1 < y) :
∀ᶠ (n : ) in Filter.atTop, x ^ (1 / n) y
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)
theorem Filter.Tendsto.ennrpow_const {α : Type u_1} {f : } {m : αENNReal} {a : ENNReal} (r : ) (hm : Filter.Tendsto m f (nhds a)) :
Filter.Tendsto (fun (x : α) => m x ^ r) f (nhds (a ^ r))