mathlib documentation

analysis.special_functions.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 : ) :
theorem complex.exp_log {x : } (hx : x 0) :
theorem complex.log_exp {x : } (hx₁ : -real.pi < x.im) (hx₂ : x.im real.pi) :
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 : complex.exp x = complex.exp y) :
x = y
theorem complex.of_real_log {x : } (hx : 0 x) :
@[simp]
theorem complex.log_zero  :
@[simp]
theorem complex.log_one  :
theorem complex.exp_eq_one_iff {x : } :
complex.exp x = 1 ∃ (n : ), x = n * (2 * real.pi * complex.I)

Alias of the reverse direction of complex.countable_preimage_exp.

theorem continuous_at_clog {x : } (h : 0 < x.re x.im 0) :
theorem filter.tendsto.clog {α : Type u_1} {l : filter α} {f : α → } {x : } (h : filter.tendsto f l (nhds x)) (hx : 0 < x.re x.im 0) :
filter.tendsto (λ (t : α), complex.log (f t)) l (nhds (complex.log x))
theorem continuous_at.clog {α : Type u_1} [topological_space α] {f : α → } {x : α} (h₁ : continuous_at f x) (h₂ : 0 < (f x).re (f x).im 0) :
continuous_at (λ (t : α), complex.log (f t)) x
theorem continuous_within_at.clog {α : Type u_1} [topological_space α] {f : α → } {s : set α} {x : α} (h₁ : continuous_within_at f s x) (h₂ : 0 < (f x).re (f x).im 0) :
continuous_within_at (λ (t : α), complex.log (f t)) s x
theorem continuous_on.clog {α : Type u_1} [topological_space α] {f : α → } {s : set α} (h₁ : continuous_on f s) (h₂ : ∀ (x : α), x s0 < (f x).re (f x).im 0) :
continuous_on (λ (t : α), complex.log (f t)) s
theorem continuous.clog {α : Type u_1} [topological_space α] {f : α → } (h₁ : continuous f) (h₂ : ∀ (x : α), 0 < (f x).re (f x).im 0) :
continuous (λ (t : α), complex.log (f t))