Various complex special functions are analytic

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

theorem analyticAt_clog {z : ℂ} (m : z ∈ Complex.slitPlane) : AnalyticAt ℂ Complex.log z

log is analytic away from nonpositive reals

theorem AnalyticAt.clog {E : Type u_1} [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 u_1} [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 u_1} [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 u_1} [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 u_1} [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 u_1} [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 u_1} [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 u_1} [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

theorem AnalyticAt.re_ofReal {f : ℂ → ℂ} {x : ℝ} (hf : AnalyticAt ℂ f ↑x) : AnalyticAt ℝ (fun (x : ℝ) => (f ↑x).re) x

theorem AnalyticAt.im_ofReal {f : ℂ → ℂ} {x : ℝ} (hf : AnalyticAt ℂ f ↑x) : AnalyticAt ℝ (fun (x : ℝ) => (f ↑x).im) x

theorem AnalyticWithinAt.re_ofReal {f : ℂ → ℂ} {s : Set ℝ} {x : ℝ} (hf : AnalyticWithinAt ℂ f (Complex.ofReal '' s) ↑x) : AnalyticWithinAt ℝ (fun (x : ℝ) => (f ↑x).re) s x

theorem AnalyticWithinAt.im_ofReal {f : ℂ → ℂ} {s : Set ℝ} {x : ℝ} (hf : AnalyticWithinAt ℂ f (Complex.ofReal '' s) ↑x) : AnalyticWithinAt ℝ (fun (x : ℝ) => (f ↑x).im) s x

theorem AnalyticOn.re_ofReal {f : ℂ → ℂ} {s : Set ℝ} (hf : AnalyticOn ℂ f (Complex.ofReal '' s)) : AnalyticOn ℝ (fun (x : ℝ) => (f ↑x).re) s

theorem AnalyticOn.im_ofReal {f : ℂ → ℂ} {s : Set ℝ} (hf : AnalyticOn ℂ f (Complex.ofReal '' s)) : AnalyticOn ℝ (fun (x : ℝ) => (f ↑x).im) s

theorem AnalyticOnNhd.re_ofReal {f : ℂ → ℂ} {s : Set ℝ} (hf : AnalyticOnNhd ℂ f (Complex.ofReal '' s)) : AnalyticOnNhd ℝ (fun (x : ℝ) => (f ↑x).re) s

theorem AnalyticOnNhd.im_ofReal {f : ℂ → ℂ} {s : Set ℝ} (hf : AnalyticOnNhd ℂ f (Complex.ofReal '' s)) : AnalyticOnNhd ℝ (fun (x : ℝ) => (f ↑x).im) s

theorem analyticAt_log {x : ℝ} (hx : 0 < x) : AnalyticAt ℝ Real.log x

theorem analyticOnNhd_log : AnalyticOnNhd ℝ Real.log (Set.Ioi 0)

theorem analyticOn_log : AnalyticOn ℝ Real.log (Set.Ioi 0)

theorem AnalyticAt.log {f : ℝ → ℝ} {x : ℝ} (fa : AnalyticAt ℝ f x) (m : 0 < f x) : AnalyticAt ℝ (fun (z : ℝ) => Real.log (f z)) x

theorem AnalyticWithinAt.log {f : ℝ → ℝ} {s : Set ℝ} {x : ℝ} (fa : AnalyticWithinAt ℝ f s x) (m : 0 < f x) : AnalyticWithinAt ℝ (fun (z : ℝ) => Real.log (f z)) s x

theorem AnalyticOnNhd.log {f : ℝ → ℝ} {s : Set ℝ} (fs : AnalyticOnNhd ℝ f s) (m : ∀ x ∈ s, 0 < f x) : AnalyticOnNhd ℝ (fun (z : ℝ) => Real.log (f z)) s

theorem AnalyticOn.log {f : ℝ → ℝ} {s : Set ℝ} (fs : AnalyticOn ℝ f s) (m : ∀ x ∈ s, 0 < f x) : AnalyticOn ℝ (fun (z : ℝ) => Real.log (f z)) s

theorem iteratedDeriv_succ_log {n : ℕ} {x : ℂ} (hx : x ∈ Complex.slitPlane) : iteratedDeriv (n + 1) Complex.log x = (-1) ^ n * ↑n.factorial * x ^ (-↑n - 1)

theorem hasFPowerSeriesAt_clog_one : HasFPowerSeriesAt Complex.log (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) => -(-1) ^ n / ↑n) 1

theorem hasFPowerSeriesAt_clog_one_add : HasFPowerSeriesAt (fun (x : ℂ) => Complex.log (1 + x)) (FormalMultilinearSeries.ofScalars ℂ fun (n : ℕ) => -(-1) ^ n / ↑n) 0

theorem hasFPowerSeriesAt_log_one : HasFPowerSeriesAt Real.log (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) => -(-1) ^ n / ↑n) 1

theorem hasFPowerSeriesAt_log_one_add : HasFPowerSeriesAt (fun (x : ℝ) => Real.log (1 + x)) (FormalMultilinearSeries.ofScalars ℝ fun (n : ℕ) => -(-1) ^ n / ↑n) 0