mathlib documentation

analysis.special_functions.complex.log

The complex log function #

Basic properties, relationship with exp, and differentiability.

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.exp_inj_of_neg_pi_lt_of_le_pi {x y : } (hx₁ : -π < x.im) (hx₂ : x.im π) (hy₁ : -π < y.im) (hy₂ : y.im π) (hxy : complex.exp x = complex.exp y) :
x = y
theorem complex.log_exp {x : } (hx₁ : -π < x.im) (hx₂ : x.im π) :
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 * π) * complex.I
theorem complex.exp_eq_exp_iff_exists_int {x y : } :
complex.exp x = complex.exp y ∃ (n : ), x = y + (n) * (2 * π) * complex.I

Alias of countable_preimage_exp.

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

Equations
theorem filter.tendsto.clog {α : Type u_1} {l : filter α} {f : α → } {x : } (h : filter.tendsto f l (𝓝 x)) (hx : 0 < x.re x.im 0) :
filter.tendsto (λ (t : α), complex.log (f t)) l (𝓝 (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))
theorem has_strict_fderiv_at.clog {E : Type u_2} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (h₁ : has_strict_fderiv_at f f' x) (h₂ : 0 < (f x).re (f x).im 0) :
has_strict_fderiv_at (λ (t : E), complex.log (f t)) ((f x)⁻¹ f') x
theorem has_strict_deriv_at.clog {f : } {f' x : } (h₁ : has_strict_deriv_at f f' x) (h₂ : 0 < (f x).re (f x).im 0) :
has_strict_deriv_at (λ (t : ), complex.log (f t)) (f' / f x) x
theorem has_strict_deriv_at.clog_real {f : } {x : } {f' : } (h₁ : has_strict_deriv_at f f' x) (h₂ : 0 < (f x).re (f x).im 0) :
has_strict_deriv_at (λ (t : ), complex.log (f t)) (f' / f x) x
theorem has_fderiv_at.clog {E : Type u_2} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {x : E} (h₁ : has_fderiv_at f f' x) (h₂ : 0 < (f x).re (f x).im 0) :
has_fderiv_at (λ (t : E), complex.log (f t)) ((f x)⁻¹ f') x
theorem has_deriv_at.clog {f : } {f' x : } (h₁ : has_deriv_at f f' x) (h₂ : 0 < (f x).re (f x).im 0) :
has_deriv_at (λ (t : ), complex.log (f t)) (f' / f x) x
theorem has_deriv_at.clog_real {f : } {x : } {f' : } (h₁ : has_deriv_at f f' x) (h₂ : 0 < (f x).re (f x).im 0) :
has_deriv_at (λ (t : ), complex.log (f t)) (f' / f x) x
theorem differentiable_at.clog {E : Type u_2} [normed_group E] [normed_space E] {f : E → } {x : E} (h₁ : differentiable_at f x) (h₂ : 0 < (f x).re (f x).im 0) :
differentiable_at (λ (t : E), complex.log (f t)) x
theorem has_fderiv_within_at.clog {E : Type u_2} [normed_group E] [normed_space E] {f : E → } {f' : E →L[] } {s : set E} {x : E} (h₁ : has_fderiv_within_at f f' s x) (h₂ : 0 < (f x).re (f x).im 0) :
has_fderiv_within_at (λ (t : E), complex.log (f t)) ((f x)⁻¹ f') s x
theorem has_deriv_within_at.clog {f : } {f' x : } {s : set } (h₁ : has_deriv_within_at f f' s x) (h₂ : 0 < (f x).re (f x).im 0) :
has_deriv_within_at (λ (t : ), complex.log (f t)) (f' / f x) s x
theorem has_deriv_within_at.clog_real {f : } {s : set } {x : } {f' : } (h₁ : has_deriv_within_at f f' s x) (h₂ : 0 < (f x).re (f x).im 0) :
has_deriv_within_at (λ (t : ), complex.log (f t)) (f' / f x) s x
theorem differentiable_within_at.clog {E : Type u_2} [normed_group E] [normed_space E] {f : E → } {s : set E} {x : E} (h₁ : differentiable_within_at f s x) (h₂ : 0 < (f x).re (f x).im 0) :
differentiable_within_at (λ (t : E), complex.log (f t)) s x
theorem differentiable_on.clog {E : Type u_2} [normed_group E] [normed_space E] {f : E → } {s : set E} (h₁ : differentiable_on f s) (h₂ : ∀ (x : E), x s0 < (f x).re (f x).im 0) :
differentiable_on (λ (t : E), complex.log (f t)) s
theorem differentiable.clog {E : Type u_2} [normed_group E] [normed_space E] {f : E → } (h₁ : differentiable f) (h₂ : ∀ (x : E), 0 < (f x).re (f x).im 0) :
differentiable (λ (t : E), complex.log (f t))