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) : (fun x => 0 ^ x) =ᶠ[nhds b] 0

theorem cpow_eq_nhds {a : ℂ} {b : ℂ} (ha : a ≠ 0) : (fun x => x ^ b) =ᶠ[nhds a] fun x => Complex.exp (Complex.log x * b)

theorem cpow_eq_nhds' {p : ℂ × ℂ} (hp_fst : p.fst ≠ 0) : (fun x => x.fst ^ x.snd) =ᶠ[nhds p] fun x => Complex.exp (Complex.log x.fst * x.snd)

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 : 0 < p.fst.re ∨ p.fst.im ≠ 0) : ContinuousAt (fun 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.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 : 0 < a.re ∨ a.im ≠ 0) : ContinuousAt (fun x => Complex.cpow x b) a

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 (fun x => f x ^ g x) l (nhds (a ^ b))

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 (fun x => a ^ f x) l (nhds (a ^ b))

theorem ContinuousWithinAt.cpow {α : Type u_1} [TopologicalSpace α] {f : α → ℂ} {g : α → ℂ} {s : Set α} {a : α} (hf : ContinuousWithinAt f s a) (hg : ContinuousWithinAt g s a) (h0 : 0 < (f a).re ∨ (f a).im ≠ 0) : ContinuousWithinAt (fun x => f x ^ g x) s a

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

theorem ContinuousAt.cpow {α : Type u_1} [TopologicalSpace α] {f : α → ℂ} {g : α → ℂ} {a : α} (hf : ContinuousAt f a) (hg : ContinuousAt g a) (h0 : 0 < (f a).re ∨ (f a).im ≠ 0) : ContinuousAt (fun x => f x ^ g x) a

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

theorem ContinuousOn.cpow {α : Type u_1} [TopologicalSpace α] {f : α → ℂ} {g : α → ℂ} {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) (h0 : ∀ (a : α), a ∈ s → 0 < (f a).re ∨ (f a).im ≠ 0) : ContinuousOn (fun x => f x ^ g x) s

theorem ContinuousOn.const_cpow {α : Type u_1} [TopologicalSpace α] {f : α → ℂ} {s : Set α} {b : ℂ} (hf : ContinuousOn f s) (h : b ≠ 0 ∨ ∀ (a : α), a ∈ s → f a ≠ 0) : ContinuousOn (fun x => b ^ f x) s

theorem Continuous.cpow {α : Type u_1} [TopologicalSpace α] {f : α → ℂ} {g : α → ℂ} (hf : Continuous f) (hg : Continuous g) (h0 : ∀ (a : α), 0 < (f a).re ∨ (f a).im ≠ 0) : Continuous fun x => f x ^ g x

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

theorem ContinuousOn.cpow_const {α : Type u_1} [TopologicalSpace α] {f : α → ℂ} {s : Set α} {b : ℂ} (hf : ContinuousOn f s) (h : ∀ (a : α), a ∈ s → 0 < (f a).re ∨ (f a).im ≠ 0) : ContinuousOn (fun x => f x ^ b) s

Continuity for real powers

theorem Real.continuousAt_const_rpow {a : ℝ} {b : ℝ} (h : a ≠ 0) : ContinuousAt (Real.rpow a) b

theorem Real.continuousAt_const_rpow' {a : ℝ} {b : ℝ} (h : b ≠ 0) : ContinuousAt (Real.rpow a) b

theorem Real.rpow_eq_nhds_of_neg {p : ℝ × ℝ} (hp_fst : p.fst < 0) : (fun x => x.fst ^ x.snd) =ᶠ[nhds p] fun x => Real.exp (Real.log x.fst * x.snd) * Real.cos (x.snd * Real.pi)

theorem Real.rpow_eq_nhds_of_pos {p : ℝ × ℝ} (hp_fst : 0 < p.fst) : (fun x => x.fst ^ x.snd) =ᶠ[nhds p] fun x => Real.exp (Real.log x.fst * x.snd)

theorem Real.continuousAt_rpow_of_ne (p : ℝ × ℝ) (hp : p.fst ≠ 0) : ContinuousAt (fun p => p.fst ^ p.snd) p

theorem Real.continuousAt_rpow_of_pos (p : ℝ × ℝ) (hp : 0 < p.snd) : ContinuousAt (fun p => p.fst ^ p.snd) p

theorem Real.continuousAt_rpow (p : ℝ × ℝ) (h : p.fst ≠ 0 ∨ 0 < p.snd) : ContinuousAt (fun p => p.fst ^ p.snd) 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 : 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 (fun t => f t ^ g t) l (nhds (x ^ y))

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 (fun a => f a ^ p) l (nhds (x ^ p))

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

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

theorem ContinuousOn.rpow {α : Type u_1} [TopologicalSpace α] {f : α → ℝ} {g : α → ℝ} {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) (h : ∀ (x : α), x ∈ s → f x ≠ 0 ∨ 0 < g x) : ContinuousOn (fun t => f t ^ g t) s

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

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

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

theorem ContinuousOn.rpow_const {α : Type u_1} [TopologicalSpace α] {f : α → ℝ} {s : Set α} {p : ℝ} (hf : ContinuousOn f s) (h : ∀ (x : α), x ∈ s → f x ≠ 0 ∨ 0 ≤ p) : ContinuousOn (fun x => f x ^ p) s

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.

theorem Complex.continuousAt_cpow_zero_of_re_pos {z : ℂ} (hz : 0 < z.re) : ContinuousAt (fun x => x.fst ^ x.snd) (0, z)

See also continuousAt_cpow and Complex.continuousAt_cpow_of_re_pos.

theorem Complex.continuousAt_cpow_of_re_pos {p : ℂ × ℂ} (h₁ : 0 ≤ p.fst.re ∨ p.fst.im ≠ 0) (h₂ : 0 < p.snd.re) : ContinuousAt (fun x => x.fst ^ x.snd) 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.fst ^ p.snd) (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.fst ^ p.snd) (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 : 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 (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 => z ^ y) x

theorem NNReal.continuous_rpow_const {y : ℝ} (h : 0 ≤ y) : Continuous fun x => 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.continuous_rpow_const {y : ℝ} : Continuous fun a => a ^ y

theorem ENNReal.tendsto_const_mul_rpow_nhds_zero_of_pos {c : ENNReal} (hc : c ≠ ⊤) {y : ℝ} (hy : 0 < y) : Filter.Tendsto (fun x => c * x ^ y) (nhds 0) (nhds 0)

theorem Filter.Tendsto.ennrpow_const {α : Type u_1} {f : Filter α} {m : α → ENNReal} {a : ENNReal} (r : ℝ) (hm : Filter.Tendsto m f (nhds a)) : Filter.Tendsto (fun x => m x ^ r) f (nhds (a ^ r))