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

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

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

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

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

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

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

@[simp]

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

theorem Complex.log_exp {x : ℂ} (hx₁ : -Real.pi < x.im) (hx₂ : x.im ≤ Real.pi) : x.exp.log = 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 : x.exp = y.exp) : x = y

theorem Complex.ofReal_log {x : ℝ} (hx : 0 ≤ x) : ↑x.log = (↑x).log

@[simp]

theorem Complex.natCast_log {n : ℕ} : ↑(↑n).log = (↑n).log

@[simp]

theorem Complex.ofNat_log {n : ℕ} [n.AtLeastTwo] : ↑(OfNat.ofNat n).log = Complex.log (OfNat.ofNat n)

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

theorem Complex.log_ofReal_mul {r : ℝ} (hr : 0 < r) {x : ℂ} (hx : x ≠ 0) : (↑r * x).log = ↑r.log + x.log

theorem Complex.log_mul_ofReal (r : ℝ) (hr : 0 < r) (x : ℂ) (hx : x ≠ 0) : (x * ↑r).log = ↑r.log + x.log

theorem Complex.log_mul_eq_add_log_iff {x : ℂ} {y : ℂ} (hx₀ : x ≠ 0) (hy₀ : y ≠ 0) : (x * y).log = x.log + y.log ↔ 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 → (x * y).log = x.log + y.log

Alias of the reverse direction of Complex.log_mul_eq_add_log_iff.

@[simp]

theorem Complex.log_zero : Complex.log 0 = 0

@[simp]

theorem Complex.log_one : Complex.log 1 = 0

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

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

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

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

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

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

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

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

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

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

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

@[simp]

theorem Complex.countable_preimage_exp {s : Set ℂ} : (Complex.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 Complex.log (nhdsWithin z {z : ℂ | z.im < 0}) (nhds (↑(Complex.abs z).log - ↑Real.pi * Complex.I))

theorem Complex.continuousWithinAt_log_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0) (him : z.im = 0) : ContinuousWithinAt Complex.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 Complex.log (nhdsWithin z {z : ℂ | 0 ≤ z.im}) (nhds (↑(Complex.abs z).log + ↑Real.pi * Complex.I))

@[simp]

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

@[simp]

theorem Complex.map_exp_comap_re_atTop : Filter.map Complex.exp (Filter.comap Complex.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 : Filter.Tendsto f l (nhds x)) (hx : x ∈ Complex.slitPlane) : Filter.Tendsto (fun (t : α) => (f t).log) l (nhds x.log)

theorem ContinuousAt.clog {α : Type u_1} [TopologicalSpace α] {f : α → ℂ} {x : α} (h₁ : ContinuousAt f x) (h₂ : f x ∈ Complex.slitPlane) : ContinuousAt (fun (t : α) => (f t).log) 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 : α) => (f t).log) 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 : α) => (f t).log) s

theorem Continuous.clog {α : Type u_1} [TopologicalSpace α] {f : α → ℂ} (h₁ : Continuous f) (h₂ : ∀ (x : α), f x ∈ Complex.slitPlane) : Continuous fun (t : α) => (f t).log