@[simp]
theorem
Complex.ofNat_log
{n : ℕ}
[n.AtLeastTwo]
:
↑(OfNat.ofNat n).log = Complex.log (OfNat.ofNat n)
theorem
Complex.log_conj_eq_ite
(x : ℂ)
:
((starRingEnd ℂ) x).log = if x.arg = Real.pi then x.log else (starRingEnd ℂ) x.log
theorem
Complex.log_conj
(x : ℂ)
(h : x.arg ≠ Real.pi)
:
((starRingEnd ℂ) x).log = (starRingEnd ℂ) x.log
@[simp]
Alias of the reverse direction of Complex.countable_preimage_exp
.
theorem
Complex.tendsto_log_nhdsWithin_im_neg_of_re_neg_of_im_zero
{z : ℂ}
(hre : z.re < 0)
(him : z.im = 0)
:
Filter.Tendsto Complex.log (nhdsWithin z {z : ℂ | z.im < 0}) (nhds (↑(Complex.abs z).log - ↑Real.pi * Complex.I))
theorem
Complex.continuousWithinAt_log_of_re_neg_of_im_zero
{z : ℂ}
(hre : z.re < 0)
(him : z.im = 0)
:
ContinuousWithinAt Complex.log {z : ℂ | 0 ≤ z.im} z
theorem
Complex.tendsto_log_nhdsWithin_im_nonneg_of_re_neg_of_im_zero
{z : ℂ}
(hre : z.re < 0)
(him : z.im = 0)
:
Filter.Tendsto Complex.log (nhdsWithin z {z : ℂ | 0 ≤ z.im}) (nhds (↑(Complex.abs z).log + ↑Real.pi * Complex.I))
@[simp]
theorem
Complex.map_exp_comap_re_atBot :
Filter.map Complex.exp (Filter.comap Complex.re Filter.atBot) = nhdsWithin 0 {0}ᶜ
@[simp]
theorem
Complex.map_exp_comap_re_atTop :
Filter.map Complex.exp (Filter.comap Complex.re Filter.atTop) = Bornology.cobounded ℂ
theorem
Filter.Tendsto.clog
{α : Type u_1}
{l : Filter α}
{f : α → ℂ}
{x : ℂ}
(h : Filter.Tendsto f l (nhds x))
(hx : x ∈ Complex.slitPlane)
:
Filter.Tendsto (fun (t : α) => (f t).log) l (nhds x.log)
theorem
ContinuousAt.clog
{α : Type u_1}
[TopologicalSpace α]
{f : α → ℂ}
{x : α}
(h₁ : ContinuousAt f x)
(h₂ : f x ∈ Complex.slitPlane)
:
ContinuousAt (fun (t : α) => (f t).log) x
theorem
ContinuousWithinAt.clog
{α : Type u_1}
[TopologicalSpace α]
{f : α → ℂ}
{s : Set α}
{x : α}
(h₁ : ContinuousWithinAt f s x)
(h₂ : f x ∈ Complex.slitPlane)
:
ContinuousWithinAt (fun (t : α) => (f t).log) s x
theorem
ContinuousOn.clog
{α : Type u_1}
[TopologicalSpace α]
{f : α → ℂ}
{s : Set α}
(h₁ : ContinuousOn f s)
(h₂ : ∀ x ∈ s, f x ∈ Complex.slitPlane)
:
ContinuousOn (fun (t : α) => (f t).log) s
theorem
Continuous.clog
{α : Type u_1}
[TopologicalSpace α]
{f : α → ℂ}
(h₁ : Continuous f)
(h₂ : ∀ (x : α), f x ∈ Complex.slitPlane)
:
Continuous fun (t : α) => (f t).log