theorem
Complex.log_exp
{x : ℂ}
(hx₁ : -Real.pi < x.im)
(hx₂ : x.im ≤ Real.pi)
:
Complex.log (Complex.exp x) = x
@[simp]
theorem
Complex.ofNat_log
{n : ℕ}
[n.AtLeastTwo]
:
↑(Real.log (OfNat.ofNat n)) = Complex.log (OfNat.ofNat n)
theorem
Complex.log_ofReal_mul
{r : ℝ}
(hr : 0 < r)
{x : ℂ}
(hx : x ≠ 0)
:
Complex.log (↑r * x) = ↑(Real.log r) + Complex.log x
theorem
Complex.log_mul_ofReal
(r : ℝ)
(hr : 0 < r)
(x : ℂ)
(hx : x ≠ 0)
:
Complex.log (x * ↑r) = ↑(Real.log r) + Complex.log x
theorem
Complex.log_mul_eq_add_log_iff
{x : ℂ}
{y : ℂ}
(hx₀ : x ≠ 0)
(hy₀ : y ≠ 0)
:
Complex.log (x * y) = Complex.log x + Complex.log y ↔ x.arg + y.arg ∈ Set.Ioc (-Real.pi) Real.pi
theorem
Complex.log_mul
{x : ℂ}
{y : ℂ}
(hx₀ : x ≠ 0)
(hy₀ : y ≠ 0)
:
x.arg + y.arg ∈ Set.Ioc (-Real.pi) Real.pi → Complex.log (x * y) = Complex.log x + Complex.log y
Alias of the reverse direction of Complex.log_mul_eq_add_log_iff
.
theorem
Complex.log_conj_eq_ite
(x : ℂ)
:
Complex.log ((starRingEnd ℂ) x) = if x.arg = Real.pi then Complex.log x else (starRingEnd ℂ) (Complex.log x)
theorem
Complex.log_conj
(x : ℂ)
(h : x.arg ≠ Real.pi)
:
Complex.log ((starRingEnd ℂ) x) = (starRingEnd ℂ) (Complex.log x)
theorem
Complex.log_inv_eq_ite
(x : ℂ)
:
Complex.log x⁻¹ = if x.arg = Real.pi then -(starRingEnd ℂ) (Complex.log x) else -Complex.log x
theorem
Complex.exp_eq_exp_iff_exp_sub_eq_one
{x : ℂ}
{y : ℂ}
:
Complex.exp x = Complex.exp y ↔ Complex.exp (x - y) = 1
@[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 (↑(Real.log (Complex.abs z)) - ↑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 (↑(Real.log (Complex.abs z)) + ↑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 : α) => Complex.log (f t)) l (nhds (Complex.log x))
theorem
ContinuousAt.clog
{α : Type u_1}
[TopologicalSpace α]
{f : α → ℂ}
{x : α}
(h₁ : ContinuousAt f x)
(h₂ : f x ∈ Complex.slitPlane)
:
ContinuousAt (fun (t : α) => Complex.log (f t)) 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 : α) => Complex.log (f t)) 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 : α) => Complex.log (f t)) s
theorem
Continuous.clog
{α : Type u_1}
[TopologicalSpace α]
{f : α → ℂ}
(h₁ : Continuous f)
(h₂ : ∀ (x : α), f x ∈ Complex.slitPlane)
:
Continuous fun (t : α) => Complex.log (f t)