The complex log function

Basic properties, relationship with exp.

noncomputable def Complex.log (x : ℂ) : ℂ

Inverse of the exp function. Returns values such that (log x).im > - π and (log x).im ≤ π. log 0 = 0

theorem Complex.log_re (x : ℂ) : (log x).re = Real.log ‖x‖

theorem Complex.log_im (x : ℂ) : (log x).im = x.arg

theorem Complex.neg_pi_lt_log_im (x : ℂ) : -Real.pi < (log x).im

theorem Complex.log_im_le_pi (x : ℂ) : (log x).im ≤ Real.pi

theorem Complex.exp_log {x : ℂ} (hx : x ≠ 0) : exp (log x) = x

@[simp]

theorem Complex.range_exp : Set.range exp = {0}ᶜ

theorem Complex.log_exp {x : ℂ} (hx₁ : -Real.pi < x.im) (hx₂ : x.im ≤ Real.pi) : log (exp x) = x

theorem Complex.log_exp_eq_re_add_toIocMod (x : ℂ) : log (exp x) = ↑x.re + ↑(toIocMod Real.two_pi_pos (-Real.pi) x.im) * I

theorem Complex.log_exp_eq_sub_toIocDiv (x : ℂ) : log (exp x) = x - ↑(toIocDiv Real.two_pi_pos (-Real.pi) x.im) * (2 * ↑Real.pi * I)

theorem Complex.exp_inj_of_neg_pi_lt_of_le_pi {x y : ℂ} (hx₁ : -Real.pi < x.im) (hx₂ : x.im ≤ Real.pi) (hy₁ : -Real.pi < y.im) (hy₂ : y.im ≤ Real.pi) (hxy : exp x = exp y) : x = y

theorem Complex.ofReal_log {x : ℝ} (hx : 0 ≤ x) : ↑(Real.log x) = log ↑x

@[simp]

theorem Complex.natCast_log {n : ℕ} : ↑(Real.log ↑n) = log ↑n

@[simp]

theorem Complex.ofNat_log {n : ℕ} [n.AtLeastTwo] : ↑(Real.log (OfNat.ofNat n)) = log (OfNat.ofNat n)

theorem Complex.log_ofReal_re (x : ℝ) : (log ↑x).re = Real.log x

theorem Complex.log_ofReal_mul {r : ℝ} (hr : 0 < r) {x : ℂ} (hx : x ≠ 0) : log (↑r * x) = ↑(Real.log r) + log x

theorem Complex.log_mul_ofReal (r : ℝ) (hr : 0 < r) (x : ℂ) (hx : x ≠ 0) : log (x * ↑r) = ↑(Real.log r) + log x

theorem Complex.log_mul_eq_add_log_iff {x y : ℂ} (hx₀ : x ≠ 0) (hy₀ : y ≠ 0) : log (x * y) = log x + 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 → log (x * y) = log x + log y

Alias of the reverse direction of Complex.log_mul_eq_add_log_iff.

@[simp]

theorem Complex.log_zero : log 0 = 0

@[simp]

theorem Complex.log_one : log 1 = 0

@[simp]

theorem Complex.log_div_self (x : ℂ) : log (x / x) = 0

This holds true for all x : ℂ because of the junk values 0 / 0 = 0 and log 0 = 0.

theorem Complex.log_neg_one : log (-1) = ↑Real.pi * I

theorem Complex.log_I : log I = ↑Real.pi / 2 * I

theorem Complex.log_neg_I : log (-I) = -(↑Real.pi / 2) * I

theorem Complex.log_conj_eq_ite (x : ℂ) : log ((starRingEnd ℂ) x) = if x.arg = Real.pi then log x else (starRingEnd ℂ) (log x)

theorem Complex.log_conj (x : ℂ) (h : x.arg ≠ Real.pi) : log ((starRingEnd ℂ) x) = (starRingEnd ℂ) (log x)

theorem Complex.log_inv_eq_ite (x : ℂ) : log x⁻¹ = if x.arg = Real.pi then -(starRingEnd ℂ) (log x) else -log x

theorem Complex.log_inv (x : ℂ) (hx : x.arg ≠ Real.pi) : log x⁻¹ = -log x

theorem Complex.two_pi_I_ne_zero : 2 * ↑Real.pi * I ≠ 0

theorem Complex.exp_eq_one_iff {x : ℂ} : exp x = 1 ↔ ∃ (n : ℤ), x = ↑n * (2 * ↑Real.pi * I)

theorem Complex.exp_eq_exp_iff_exp_sub_eq_one {x y : ℂ} : exp x = exp y ↔ exp (x - y) = 1

theorem Complex.exp_eq_exp_iff_exists_int {x y : ℂ} : exp x = exp y ↔ ∃ (n : ℤ), x = y + ↑n * (2 * ↑Real.pi * I)

theorem Complex.re_eq_re_of_cexp_eq_cexp {x y : ℂ} (h : exp x = exp y) : x.re = y.re

theorem Complex.log_exp_exists (z : ℂ) : ∃ (n : ℤ), log (exp z) = z + ↑n * (2 * ↑Real.pi * I)

@[simp]

theorem Complex.countable_preimage_exp {s : Set ℂ} : (exp ⁻¹' s).Countable ↔ s.Countable

theorem Set.Countable.preimage_cexp {s : Set ℂ} : s.Countable → (Complex.exp ⁻¹' s).Countable

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 log (nhdsWithin z {z : ℂ | z.im < 0}) (nhds (↑(Real.log ‖z‖) - ↑Real.pi * I))

theorem Complex.continuousWithinAt_log_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0) (him : z.im = 0) : ContinuousWithinAt 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 log (nhdsWithin z {z : ℂ | 0 ≤ z.im}) (nhds (↑(Real.log ‖z‖) + ↑Real.pi * I))

@[simp]

theorem Complex.map_exp_comap_re_atBot : Filter.map exp (Filter.comap re Filter.atBot) = nhdsWithin 0 {0}ᶜ

@[simp]

theorem Complex.map_exp_comap_re_atTop : Filter.map exp (Filter.comap re Filter.atTop) = Bornology.cobounded ℂ

theorem continuousAt_clog {x : ℂ} (h : x ∈ Complex.slitPlane) : ContinuousAt Complex.log x

theorem Filter.Tendsto.clog {α : Type u_1} {l : Filter α} {f : α → ℂ} {x : ℂ} (h : Tendsto f l (nhds x)) (hx : x ∈ Complex.slitPlane) : 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)

noncomputable def Complex.expOpenPartialHomeomorph : OpenPartialHomeomorph ℂ ℂ

Complex.exp as an OpenPartialHomeomorph with source = {z | -π < im z < π} and target = {z | 0 < re z} ∪ {z | im z ≠ 0} (a.k.a. slitPlane). This definition is used to prove that Complex.log is complex differentiable at all points but the negative real semi-axis.

@[deprecated Complex.expOpenPartialHomeomorph (since := "2026-01-13")]

def Complex.expPartialHomeomorph : OpenPartialHomeomorph ℂ ℂ

Alias of Complex.expOpenPartialHomeomorph.

---

Complex.exp as an OpenPartialHomeomorph with source = {z | -π < im z < π} and target = {z | 0 < re z} ∪ {z | im z ≠ 0} (a.k.a. slitPlane). This definition is used to prove that Complex.log is complex differentiable at all points but the negative real semi-axis.