Documentation

Mathlib.Analysis.SpecialFunctions.Complex.Analytic

Various complex special functions are analytic #

exp, log, and cpow are analytic, since they are differentiable.

exp is entire

exp is analytic at any point

theorem AnalyticAt.cexp {E : Type} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : E} (fa : AnalyticAt f x) :
AnalyticAt (fun (z : E) => Complex.exp (f z)) 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) => Complex.exp (f z)) 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) => Complex.log (f z)) 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 : zs, f z Complex.slitPlane) :
AnalyticOn (fun (z : E) => Complex.log (f z)) 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 : zs, 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