mathlib3 documentation

analysis.special_functions.pow.continuity

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 #

theorem zero_cpow_eq_nhds {b : } (hb : b 0) :
(λ (x : ), 0 ^ x) =ᶠ[nhds b] 0
theorem cpow_eq_nhds {a b : } (ha : a 0) :
(λ (x : ), x ^ b) =ᶠ[nhds a] λ (x : ), cexp (complex.log x * b)
theorem cpow_eq_nhds' {p : × } (hp_fst : p.fst 0) :
(λ (x : × ), x.fst ^ x.snd) =ᶠ[nhds p] λ (x : × ), cexp (complex.log x.fst * x.snd)
theorem continuous_at_const_cpow {a b : } (ha : a 0) :
continuous_at (λ (x : ), a ^ x) b
theorem continuous_at_const_cpow' {a b : } (h : b 0) :
continuous_at (λ (x : ), a ^ x) b
theorem continuous_at_cpow {p : × } (hp_fst : 0 < p.fst.re p.fst.im 0) :
continuous_at (λ (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.continuous_at_cpow_zero_of_re_pos for a version that works for z = 0 but assumes 0 < re w.

theorem continuous_at_cpow_const {a b : } (ha : 0 < a.re a.im 0) :
continuous_at (λ (x : ), x.cpow 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 (λ (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 (λ (x : α), a ^ f 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_const_rpow {a b : } (h : a 0) :
theorem real.continuous_at_const_rpow' {a b : } (h : b 0) :
theorem real.rpow_eq_nhds_of_neg {p : × } (hp_fst : p.fst < 0) :
(λ (x : × ), x.fst ^ x.snd) =ᶠ[nhds p] λ (x : × ), rexp (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) :
(λ (x : × ), x.fst ^ x.snd) =ᶠ[nhds p] λ (x : × ), rexp (real.log x.fst * x.snd)
theorem real.continuous_at_rpow_of_ne (p : × ) (hp : p.fst 0) :
continuous_at (λ (p : × ), p.fst ^ p.snd) p
theorem real.continuous_at_rpow_of_pos (p : × ) (hp : 0 < p.snd) :
continuous_at (λ (p : × ), p.fst ^ p.snd) p
theorem real.continuous_at_rpow (p : × ) (h : p.fst 0 0 < p.snd) :
continuous_at (λ (p : × ), p.fst ^ p.snd) p
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 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 (λ (a : α), f a ^ p) l (nhds (x ^ p))
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.

theorem complex.continuous_at_cpow_of_re_pos {p : × } (h₁ : 0 p.fst.re p.fst.im 0) (h₂ : 0 < p.snd.re) :
continuous_at (λ (x : × ), x.fst ^ x.snd) p

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

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_at_of_real_cpow (x : ) (y : ) (h : 0 < y.re x 0) :
continuous_at (λ (p : × ), (p.fst) ^ p.snd) (x, y)

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

theorem complex.continuous_at_of_real_cpow_const (x : ) (y : ) (h : 0 < y.re x 0) :
continuous_at (λ (a : ), a ^ y) x
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 {x : nnreal} {y : } (h : x 0 0 < y) :
continuous_at (λ (p : nnreal × ), p.fst ^ p.snd) (x, y)
theorem nnreal.eventually_pow_one_div_le (x : nnreal) {y : nnreal} (hy : 1 < y) :
∀ᶠ (n : ) in filter.at_top, 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 (λ (a : α), u a ^ v a) f (nhds (x ^ y))
theorem nnreal.continuous_at_rpow_const {x : nnreal} {y : } (h : x 0 0 y) :
continuous_at (λ (z : nnreal), z ^ y) x
theorem nnreal.continuous_rpow_const {y : } (h : 0 y) :
continuous (λ (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.at_top, x ^ (1 / n) y
@[continuity]
theorem ennreal.continuous_rpow_const {y : } :
continuous (λ (a : ennreal), a ^ y)
theorem ennreal.tendsto_const_mul_rpow_nhds_zero_of_pos {c : ennreal} (hc : c ) {y : } (hy : 0 < y) :
filter.tendsto (λ (x : ennreal), 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 (λ (x : α), m x ^ r) f (nhds (a ^ r))