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

• Complex.log x = ↑(Real.log (Complex.abs x)) + ↑x.arg * Complex.I

theorem Complex.log_re (x : ℂ) : (log x).re = Real.log (abs x)

theorem Complex.log_im (x : ℂ) : (log x).im = x.arg

theorem Complex.neg_pi_lt_log_im (x : ℂ) : -Real.pi < (log x).im

theorem Complex.log_im_le_pi (x : ℂ) : (log x).im ≤ Real.pi

theorem Complex.exp_log {x : ℂ} (hx : x ≠ 0) : exp (log x) = x

@[simp]

theorem Complex.range_exp : Set.range exp = {0}ᶜ

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.ofNat_log {n : ℕ} [n.AtLeastTwo] : ↑(Real.log (OfNat.ofNat n)) = log (OfNat.ofNat n)

theorem Complex.log_ofReal_re (x : ℝ) : (log ↑x).re = Real.log x

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) : log (x * y) = log x + log y ↔ x.arg + y.arg ∈ Set.Ioc (-Real.pi) Real.pi

theorem Complex.log_mul {x y : ℂ} (hx₀ : x ≠ 0) (hy₀ : y ≠ 0) : x.arg + y.arg ∈ Set.Ioc (-Real.pi) Real.pi → log (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

theorem Complex.log_neg_one : log (-1) = ↑Real.pi * I

theorem Complex.log_I : log I = ↑Real.pi / 2 * I

theorem Complex.log_neg_I : log (-I) = -(↑Real.pi / 2) * I

theorem Complex.log_conj_eq_ite (x : ℂ) : log ((starRingEnd ℂ) x) = if x.arg = Real.pi then log x else (starRingEnd ℂ) (log x)

theorem Complex.log_conj (x : ℂ) (h : x.arg ≠ Real.pi) : log ((starRingEnd ℂ) x) = (starRingEnd ℂ) (log x)

theorem Complex.log_inv_eq_ite (x : ℂ) : log x⁻¹ = if x.arg = Real.pi then -(starRingEnd ℂ) (log x) else -log x

theorem Complex.log_inv (x : ℂ) (hx : x.arg ≠ Real.pi) : log x⁻¹ = -log x

theorem Complex.two_pi_I_ne_zero : 2 * ↑Real.pi * I ≠ 0

theorem Complex.exp_eq_one_iff {x : ℂ} : exp x = 1 ↔ ∃ (n : ℤ), x = ↑n * (2 * ↑Real.pi * I)

theorem Complex.exp_eq_exp_iff_exp_sub_eq_one {x y : ℂ} : exp x = exp y ↔ exp (x - y) = 1

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)

@[simp]

theorem Complex.countable_preimage_exp {s : Set ℂ} : (exp ⁻¹' s).Countable ↔ s.Countable

theorem Set.Countable.preimage_cexp {s : Set ℂ} : s.Countable → (Complex.exp ⁻¹' s).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 log (nhdsWithin z {z : ℂ | z.im < 0}) (nhds (↑(Real.log (abs z)) - ↑Real.pi * I))

theorem Complex.continuousWithinAt_log_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0) (him : z.im = 0) : ContinuousWithinAt log {z : ℂ | 0 ≤ z.im} z

theorem Complex.tendsto_log_nhdsWithin_im_nonneg_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0) (him : z.im = 0) : Filter.Tendsto log (nhdsWithin z {z : ℂ | 0 ≤ z.im}) (nhds (↑(Real.log (abs z)) + ↑Real.pi * I))

@[simp]

theorem Complex.map_exp_comap_re_atBot : Filter.map exp (Filter.comap re Filter.atBot) = nhdsWithin 0 {0}ᶜ

@[simp]

theorem Complex.map_exp_comap_re_atTop : Filter.map exp (Filter.comap re Filter.atTop) = Bornology.cobounded ℂ

theorem continuousAt_clog {x : ℂ} (h : x ∈ Complex.slitPlane) : ContinuousAt Complex.log x

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₂ : ∀ x ∈ s, 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)

theorem Real.HasSum_rexp_HasProd {α : Type u_1} {ι : Type u_2} (f : ι → α → ℝ) (hfn : ∀ (x : α) (n : ι), 0 < f n x) (hf : ∀ (x : α), HasSum (fun (n : ι) => log (f n x)) (∑' (i : ι), 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 : ι) => log (f n x)) : (exp ∘ fun (a : α) => ∑' (n : ι), 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 : ι) => 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 : ι) => log (f n x)) (∑' (i : ι), 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 : ι) => 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 : ι) => log (f n x)) : (exp ∘ fun (a : α) => ∑' (n : ι), 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.