Continuity of power functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file contains lemmas about continuity of the power functions on ℂ, ℝ, ℝ≥0, and ℝ≥0∞.
Continuity for complex powers #
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.continuous_at_cpow_zero_of_re_pos for a version that
works for z = 0 but assumes 0 < re w.
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 (λ (x : α), f x ^ g x) l (nhds (a ^ b))
theorem
continuous_within_at.cpow
{α : Type u_1}
[topological_space α]
{f g : α → ℂ}
{s : set α}
{a : α}
(hf : continuous_within_at f s a)
(hg : continuous_within_at g s a)
(h0 : 0 < (f a).re ∨ (f a).im ≠ 0) :
continuous_within_at (λ (x : α), f x ^ g x) s a
theorem
continuous_within_at.const_cpow
{α : Type u_1}
[topological_space α]
{f : α → ℂ}
{s : set α}
{a : α}
{b : ℂ}
(hf : continuous_within_at f s a)
(h : b ≠ 0 ∨ f a ≠ 0) :
continuous_within_at (λ (x : α), b ^ f x) s a
theorem
continuous_at.cpow
{α : Type u_1}
[topological_space α]
{f g : α → ℂ}
{a : α}
(hf : continuous_at f a)
(hg : continuous_at g a)
(h0 : 0 < (f a).re ∨ (f a).im ≠ 0) :
continuous_at (λ (x : α), f x ^ g x) a
theorem
continuous_at.const_cpow
{α : Type u_1}
[topological_space α]
{f : α → ℂ}
{a : α}
{b : ℂ}
(hf : continuous_at f a)
(h : b ≠ 0 ∨ f a ≠ 0) :
continuous_at (λ (x : α), b ^ f x) a
theorem
continuous_on.cpow
{α : Type u_1}
[topological_space α]
{f g : α → ℂ}
{s : set α}
(hf : continuous_on f s)
(hg : continuous_on g s)
(h0 : ∀ (a : α), a ∈ s → 0 < (f a).re ∨ (f a).im ≠ 0) :
continuous_on (λ (x : α), f x ^ g x) s
theorem
continuous_on.const_cpow
{α : Type u_1}
[topological_space α]
{f : α → ℂ}
{s : set α}
{b : ℂ}
(hf : continuous_on f s)
(h : b ≠ 0 ∨ ∀ (a : α), a ∈ s → f a ≠ 0) :
continuous_on (λ (x : α), b ^ f x) s
theorem
continuous.cpow
{α : Type u_1}
[topological_space α]
{f g : α → ℂ}
(hf : continuous f)
(hg : continuous g)
(h0 : ∀ (a : α), 0 < (f a).re ∨ (f a).im ≠ 0) :
continuous (λ (x : α), f x ^ g x)
theorem
continuous.const_cpow
{α : Type u_1}
[topological_space α]
{f : α → ℂ}
{b : ℂ}
(hf : continuous f)
(h : b ≠ 0 ∨ ∀ (a : α), f a ≠ 0) :
continuous (λ (x : α), b ^ f x)
theorem
continuous_on.cpow_const
{α : Type u_1}
[topological_space α]
{f : α → ℂ}
{s : set α}
{b : ℂ}
(hf : continuous_on f s)
(h : ∀ (a : α), a ∈ s → 0 < (f a).re ∨ (f a).im ≠ 0) :
continuous_on (λ (x : α), f x ^ b) s
Continuity for real powers #
theorem
real.continuous_at_rpow_const
(x q : ℝ)
(h : x ≠ 0 ∨ 0 < q) :
continuous_at (λ (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 (λ (t : α), f t ^ g t) l (nhds (x ^ y))
theorem
continuous_at.rpow
{α : Type u_1}
[topological_space α]
{f g : α → ℝ}
{x : α}
(hf : continuous_at f x)
(hg : continuous_at g x)
(h : f x ≠ 0 ∨ 0 < g x) :
continuous_at (λ (t : α), f t ^ g t) x
theorem
continuous_within_at.rpow
{α : Type u_1}
[topological_space α]
{f g : α → ℝ}
{s : set α}
{x : α}
(hf : continuous_within_at f s x)
(hg : continuous_within_at g s x)
(h : f x ≠ 0 ∨ 0 < g x) :
continuous_within_at (λ (t : α), f t ^ g t) s x
theorem
continuous_on.rpow
{α : Type u_1}
[topological_space α]
{f g : α → ℝ}
{s : set α}
(hf : continuous_on f s)
(hg : continuous_on g s)
(h : ∀ (x : α), x ∈ s → f x ≠ 0 ∨ 0 < g x) :
continuous_on (λ (t : α), f t ^ g t) s
theorem
continuous.rpow
{α : Type u_1}
[topological_space α]
{f g : α → ℝ}
(hf : continuous f)
(hg : continuous g)
(h : ∀ (x : α), f x ≠ 0 ∨ 0 < g x) :
continuous (λ (x : α), f x ^ g x)
theorem
continuous_within_at.rpow_const
{α : Type u_1}
[topological_space α]
{f : α → ℝ}
{s : set α}
{x : α}
{p : ℝ}
(hf : continuous_within_at f s x)
(h : f x ≠ 0 ∨ 0 ≤ p) :
continuous_within_at (λ (x : α), f x ^ p) s x
theorem
continuous_at.rpow_const
{α : Type u_1}
[topological_space α]
{f : α → ℝ}
{x : α}
{p : ℝ}
(hf : continuous_at f x)
(h : f x ≠ 0 ∨ 0 ≤ p) :
continuous_at (λ (x : α), f x ^ p) x
theorem
continuous_on.rpow_const
{α : Type u_1}
[topological_space α]
{f : α → ℝ}
{s : set α}
{p : ℝ}
(hf : continuous_on f s)
(h : ∀ (x : α), x ∈ s → f x ≠ 0 ∨ 0 ≤ p) :
continuous_on (λ (x : α), f x ^ p) s
theorem
continuous.rpow_const
{α : Type u_1}
[topological_space α]
{f : α → ℝ}
{p : ℝ}
(hf : continuous f)
(h : ∀ (x : α), f x ≠ 0 ∨ 0 ≤ p) :
continuous (λ (x : α), f x ^ p)
Continuity results for cpow, part II #
These results involve relating real and complex powers, so cannot be done higher up.
See also continuous_at_cpow and complex.continuous_at_cpow_of_re_pos.
theorem
complex.continuous_at_cpow_const_of_re_pos
{z w : ℂ}
(hz : 0 ≤ z.re ∨ z.im ≠ 0)
(hw : 0 < w.re) :
continuous_at (λ (x : ℂ), x ^ w) z
See also continuous_at_cpow_const for a version that assumes z ≠ 0 but makes no
assumptions about w.
theorem
complex.continuous_of_real_cpow_const
{y : ℂ}
(hs : 0 < y.re) :
continuous (λ (x : ℝ), ↑x ^ y)
Limits and continuity for ℝ≥0 powers #
theorem
nnreal.continuous_at_rpow_const
{x : nnreal}
{y : ℝ}
(h : x ≠ 0 ∨ 0 ≤ y) :
continuous_at (λ (z : nnreal), z ^ y) x
Continuity for ℝ≥0∞ powers #
@[continuity]
theorem
filter.tendsto.ennrpow_const
{α : Type u_1}
{f : filter α}
{m : α → ennreal}
{a : ennreal}
(r : ℝ)
(hm : filter.tendsto m f (nhds a)) :
filter.tendsto (λ (x : α), m x ^ r) f (nhds (a ^ r))