# The complex `log` function #

Basic properties, relationship with `exp`.

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

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

Equations

- Complex.log x = ↑(Real.log ‖x‖) + ↑x.arg * Complex.I

Instances For

source
theorem Complex.log_re (x : ℂ) :
(log x).re = Real.log ‖x‖
source
theorem Complex.log_im (x : ℂ) :
(log x).im = x.arg
source
theorem Complex.neg_pi_lt_log_im (x : ℂ) :
-Real.pi < (log x).im
source
theorem Complex.log_im_le_pi (x : ℂ) :
(log x).im ≤ Real.pi
source
theorem Complex.exp_log {x : ℂ} (hx : x ≠ 0) :
exp (log x) = x
source
@[simp]
theorem Complex.range_exp :
Set.range exp = {0}ᶜ
source
theorem Complex.log_exp {x : ℂ} (hx₁ : -Real.pi < x.im) (hx₂ : x.im ≤ Real.pi) :
log (exp x) = x
source
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
source
theorem Complex.ofReal_log {x : ℝ} (hx : 0 ≤ x) :
↑(Real.log x) = log ↑x
source
@[simp]
theorem Complex.natCast_log {n : ℕ} :
↑(Real.log ↑n) = log ↑n
source
@[simp]
theorem Complex.ofNat_log {n : ℕ} [n.AtLeastTwo] :
↑(Real.log (OfNat.ofNat n)) = log (OfNat.ofNat n)
source
theorem Complex.log_ofReal_re (x : ℝ) :
(log ↑x).re = Real.log x
source
theorem Complex.log_ofReal_mul {r : ℝ} (hr : 0 < r) {x : ℂ} (hx : x ≠ 0) :
log (↑r * x) = ↑(Real.log r) + log x
source
theorem Complex.log_mul_ofReal (r : ℝ) (hr : 0 < r) (x : ℂ) (hx : x ≠ 0) :
log (x * ↑r) = ↑(Real.log r) + log x
source
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
source
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`.

source
@[simp]
theorem Complex.log_zero :
log 0 = 0
source
@[simp]
theorem Complex.log_one :
log 1 = 0
source
@[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`.

source
theorem Complex.log_neg_one :
log (-1) = ↑Real.pi * I
source
theorem Complex.log_I :
log I = ↑Real.pi / 2 * I
source
theorem Complex.log_neg_I :
log (-I) = -(↑Real.pi / 2) * I
source
theorem Complex.log_conj_eq_ite (x : ℂ) :
log ((starRingEnd ℂ) x) = if x.arg = Real.pi then log x else (starRingEnd ℂ) (log x)
source
theorem Complex.log_conj (x : ℂ) (h : x.arg ≠ Real.pi) :
log ((starRingEnd ℂ) x) = (starRingEnd ℂ) (log x)
source
theorem Complex.log_inv_eq_ite (x : ℂ) :
log x⁻¹ = if x.arg = Real.pi then -(starRingEnd ℂ) (log x) else -log x
source
theorem Complex.log_inv (x : ℂ) (hx : x.arg ≠ Real.pi) :
log x⁻¹ = -log x
source
theorem Complex.two_pi_I_ne_zero :
2 * ↑Real.pi * I ≠ 0
source
theorem Complex.exp_eq_one_iff {x : ℂ} :
exp x = 1 ↔ ∃ (n : ℤ), x = ↑n * (2 * ↑Real.pi * I)
source
theorem Complex.exp_eq_exp_iff_exp_sub_eq_one {x y : ℂ} :
exp x = exp y ↔ exp (x - y) = 1
source
theorem Complex.exp_eq_exp_iff_exists_int {x y : ℂ} :
exp x = exp y ↔ ∃ (n : ℤ), x = y + ↑n * (2 * ↑Real.pi * I)
source
theorem Complex.log_exp_exists (z : ℂ) :
∃ (n : ℤ), log (exp z) = z + ↑n * (2 * ↑Real.pi * I)
source
@[simp]
theorem Complex.countable_preimage_exp {s : Set ℂ} :
(exp ⁻¹' s).Countable ↔ s.Countable
source
theorem Set.Countable.preimage_cexp {s : Set ℂ} :
s.Countable → (Complex.exp ⁻¹' s).Countable

Alias of the reverse direction of `Complex.countable_preimage_exp`.

source
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))
source
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
source
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))
source
@[simp]
theorem Complex.map_exp_comap_re_atBot :
Filter.map exp (Filter.comap re Filter.atBot) = nhdsWithin 0 {0}ᶜ
source
@[simp]
theorem Complex.map_exp_comap_re_atTop :
Filter.map exp (Filter.comap re Filter.atTop) = Bornology.cobounded ℂ
source
theorem continuousAt_clog {x : ℂ} (h : x ∈ Complex.slitPlane) :
ContinuousAt Complex.log x
source
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))
source
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
source
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
source
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
source
theorem Continuous.clog {α : Type u_1} [TopologicalSpace α] {f : α → ℂ} (h₁ : Continuous f) (h₂ : ∀ (x : α), f x ∈ Complex.slitPlane) :
Continuous fun (t : α) => Complex.log (f t)