Documentation

Mathlib.Analysis.SpecialFunctions.Complex.Log

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

Equations
theorem Complex.log_im (x : ) :
(log x).im = x.arg
theorem Complex.exp_log {x : } (hx : x 0) :
exp (log x) = x
theorem Complex.log_exp {x : } (hx₁ : -Real.pi < x.im) (hx₂ : x.im Real.pi) :
log (exp x) = x
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.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) :
theorem Complex.log_mul {x y : } (hx₀ : x 0) (hy₀ : y 0) :
x.arg + y.arg Set.Ioc (-Real.pi) Real.pilog (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_inv (x : ) (hx : x.arg Real.pi) :
theorem Complex.exp_eq_one_iff {x : } :
exp x = 1 ∃ (n : ), x = n * (2 * Real.pi * I)
theorem Complex.exp_eq_exp_iff_exists_int {x y : } :
exp x = exp y ∃ (n : ), x = y + n * (2 * Real.pi * I)
theorem Complex.log_exp_exists (z : ) :
∃ (n : ), log (exp z) = z + n * (2 * Real.pi * I)
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₂ : xs, 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)