mathlib3 documentation

analysis.special_functions.complex.log

The complex log function #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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) :
@[simp]
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 : cexp x = cexp y) :
x = y
theorem complex.of_real_log {x : } (hx : 0 x) :
theorem complex.log_of_real_mul {r : } (hr : 0 < r) {x : } (hx : x 0) :
theorem complex.log_mul_of_real (r : ) (hr : 0 < r) (x : ) (hx : x 0) :
@[simp]
theorem complex.log_zero  :
@[simp]
theorem complex.log_one  :
theorem complex.exp_eq_one_iff {x : } :
cexp 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 s 0 < (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))