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