# 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_re (x : ) :
(Complex.log x).re = Real.log (Complex.abs x)
theorem Complex.log_im (x : ) :
(Complex.log x).im = x.arg
theorem Complex.exp_log {x : } (hx : x 0) :
= x
@[simp]
theorem Complex.log_exp {x : } (hx₁ : < x.im) (hx₂ : x.im Real.pi) :
= x
theorem Complex.exp_inj_of_neg_pi_lt_of_le_pi {x : } {y : } (hx₁ : < x.im) (hx₂ : x.im Real.pi) (hy₁ : < y.im) (hy₂ : y.im Real.pi) (hxy : ) :
x = y
theorem Complex.ofReal_log {x : } (hx : 0 x) :
(Real.log x) =
@[simp]
theorem Complex.natCast_log {n : } :
(Real.log n) =
@[simp]
theorem Complex.ofNat_log {n : } [n.AtLeastTwo] :
theorem Complex.log_ofReal_re (x : ) :
(Complex.log x).re =
theorem Complex.log_ofReal_mul {r : } (hr : 0 < r) {x : } (hx : x 0) :
Complex.log (r * x) = (Real.log r) +
theorem Complex.log_mul_ofReal (r : ) (hr : 0 < r) (x : ) (hx : x 0) :
Complex.log (x * r) = (Real.log r) +
theorem Complex.log_mul_eq_add_log_iff {x : } {y : } (hx₀ : x 0) (hy₀ : y 0) :
Complex.log (x * y) = x.arg + y.arg
theorem Complex.log_mul {x : } {y : } (hx₀ : x 0) (hy₀ : y 0) :
x.arg + y.arg Complex.log (x * y) =

Alias of the reverse direction of Complex.log_mul_eq_add_log_iff.

@[simp]
theorem Complex.log_zero :
= 0
@[simp]
theorem Complex.log_one :
= 0
theorem Complex.log_conj_eq_ite (x : ) :
Complex.log ( x) = if x.arg = Real.pi then else (Complex.log x)
theorem Complex.log_conj (x : ) (h : x.arg Real.pi) :
theorem Complex.log_inv_eq_ite (x : ) :
= if x.arg = Real.pi then - (Complex.log x) else
theorem Complex.log_inv (x : ) (hx : x.arg Real.pi) :
theorem Complex.exp_eq_one_iff {x : } :
= 1 ∃ (n : ), x = n * (2 * * Complex.I)
theorem Complex.exp_eq_exp_iff_exists_int {x : } {y : } :
∃ (n : ), x = y + n * (2 * * Complex.I)
@[simp]
theorem Complex.countable_preimage_exp {s : } :
.Countable s.Countable
theorem Set.Countable.preimage_cexp {s : } :
s.Countable.Countable

Alias of the reverse direction of Complex.countable_preimage_exp.

theorem Complex.tendsto_log_nhdsWithin_im_neg_of_re_neg_of_im_zero {z : } (hre : z.re < 0) (him : z.im = 0) :
Filter.Tendsto Complex.log (nhdsWithin z {z : | z.im < 0}) (nhds ((Real.log (Complex.abs z)) - ))
theorem Complex.continuousWithinAt_log_of_re_neg_of_im_zero {z : } (hre : z.re < 0) (him : z.im = 0) :
theorem Complex.tendsto_log_nhdsWithin_im_nonneg_of_re_neg_of_im_zero {z : } (hre : z.re < 0) (him : z.im = 0) :
Filter.Tendsto Complex.log (nhdsWithin z {z : | 0 z.im}) (nhds ((Real.log (Complex.abs z)) + ))
theorem continuousAt_clog {x : } (h : ) :
theorem Filter.Tendsto.clog {α : Type u_1} {l : } {f : α} {x : } (h : Filter.Tendsto f l (nhds x)) (hx : ) :
Filter.Tendsto (fun (t : α) => Complex.log (f t)) l (nhds (Complex.log x))
theorem ContinuousAt.clog {α : Type u_1} [] {f : α} {x : α} (h₁ : ) (h₂ : ) :
ContinuousAt (fun (t : α) => Complex.log (f t)) x
theorem ContinuousWithinAt.clog {α : Type u_1} [] {f : α} {s : Set α} {x : α} (h₁ : ) (h₂ : ) :
ContinuousWithinAt (fun (t : α) => Complex.log (f t)) s x
theorem ContinuousOn.clog {α : Type u_1} [] {f : α} {s : Set α} (h₁ : ) (h₂ : xs, ) :
ContinuousOn (fun (t : α) => Complex.log (f t)) s
theorem Continuous.clog {α : Type u_1} [] {f : α} (h₁ : ) (h₂ : ∀ (x : α), ) :
Continuous fun (t : α) => Complex.log (f t)
theorem Real.HasSum_rexp_HasProd {α : Type u_1} {ι : Type u_2} (f : ια) (hfn : ∀ (x : α) (n : ι), 0 < f n x) (hf : ∀ (x : α), HasSum (fun (n : ι) => Real.log (f n x)) (∑' (i : ι), Real.log (f i x))) (a : α) :
HasProd (fun (b : ι) => f b a) (∏' (n : ι), f n a)
theorem Real.rexp_tsum_eq_tprod {α : Type u_1} {ι : Type u_2} (f : ια) (hfn : ∀ (x : α) (n : ι), 0 < f n x) (hf : ∀ (x : α), Summable fun (n : ι) => Real.log (f n x)) :
(Real.exp fun (a : α) => ∑' (n : ι), Real.log (f n a)) = fun (a : α) => ∏' (n : ι), f n a

The exponential of a infinite sum of real logs (which converges absolutely) is an infinite product.

theorem Real.summable_cexp_multipliable {α : Type u_1} {ι : Type u_2} (f : ια) (hfn : ∀ (x : α) (n : ι), 0 < f n x) (hf : ∀ (x : α), Summable fun (n : ι) => Real.log (f n x)) (a : α) :
Multipliable fun (b : ι) => f b a
theorem Complex.HasSum_cexp_HasProd {α : Type u_1} {ι : Type u_2} (f : ια) (hfn : ∀ (x : α) (n : ι), f n x 0) (hf : ∀ (x : α), HasSum (fun (n : ι) => Complex.log (f n x)) (∑' (i : ι), Complex.log (f i x))) (a : α) :
HasProd (fun (b : ι) => f b a) (∏' (n : ι), f n a)
theorem Complex.summable_cexp_multipliable {α : Type u_1} {ι : Type u_2} (f : ια) (hfn : ∀ (x : α) (n : ι), f n x 0) (hf : ∀ (x : α), Summable fun (n : ι) => Complex.log (f n x)) (a : α) :
Multipliable fun (b : ι) => f b a
theorem Complex.cexp_tsum_eq_tprod {α : Type u_1} {ι : Type u_2} (f : ια) (hfn : ∀ (x : α) (n : ι), f n x 0) (hf : ∀ (x : α), Summable fun (n : ι) => Complex.log (f n x)) :
(Complex.exp fun (a : α) => ∑' (n : ι), Complex.log (f n a)) = fun (a : α) => ∏' (n : ι), f n a

The exponential of a infinite sum of comples logs (which converges absolutely) is an infinite product.