Various complex special functions are analytic #
exp, log, and cpow are analytic, since they are differentiable.
theorem
AnalyticAt.cexp
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{f : E → ℂ}
{x : E}
(fa : AnalyticAt ℂ f x)
:
AnalyticAt ℂ (fun (z : E) => (f z).exp) x
exp ∘ f is analytic
theorem
AnalyticOn.cexp
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{f : E → ℂ}
{s : Set E}
(fs : AnalyticOn ℂ f s)
:
AnalyticOn ℂ (fun (z : E) => (f z).exp) s
exp ∘ f is analytic
log is analytic away from nonpositive reals
theorem
AnalyticAt.clog
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{f : E → ℂ}
{x : E}
(fa : AnalyticAt ℂ f x)
(m : f x ∈ Complex.slitPlane)
:
AnalyticAt ℂ (fun (z : E) => (f z).log) x
log is analytic away from nonpositive reals
theorem
AnalyticOn.clog
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{f : E → ℂ}
{s : Set E}
(fs : AnalyticOn ℂ f s)
(m : ∀ z ∈ s, f z ∈ Complex.slitPlane)
:
AnalyticOn ℂ (fun (z : E) => (f z).log) s
log is analytic away from nonpositive reals
theorem
AnalyticAt.cpow
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{f : E → ℂ}
{g : E → ℂ}
{x : E}
(fa : AnalyticAt ℂ f x)
(ga : AnalyticAt ℂ g x)
(m : f x ∈ Complex.slitPlane)
:
AnalyticAt ℂ (fun (z : E) => f z ^ g z) x
f z ^ g z is analytic if f z is not a nonpositive real
theorem
AnalyticOn.cpow
{E : Type}
[NormedAddCommGroup E]
[NormedSpace ℂ E]
{f : E → ℂ}
{g : E → ℂ}
{s : Set E}
(fs : AnalyticOn ℂ f s)
(gs : AnalyticOn ℂ g s)
(m : ∀ z ∈ s, f z ∈ Complex.slitPlane)
:
AnalyticOn ℂ (fun (z : E) => f z ^ g z) s
f z ^ g z is analytic if f z avoids nonpositive reals