Various complex special functions are 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
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
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
{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