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
    Instances For
      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)