mathlib3 documentation

analysis.special_functions.complex.log

The complex `log` function #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 : ℂ) :

(complex.log x).re = real.log (⇑complex.abs x)

theorem complex.log_im (x : ℂ) :

(complex.log x).im = x.arg

theorem complex.neg_pi_lt_log_im (x : ℂ) :

-real.pi < (complex.log x).im

theorem complex.log_im_le_pi (x : ℂ) :

(complex.log x).im ≤ real.pi

theorem complex.exp_log {x : ℂ} (hx : x ≠ 0) :

cexp (complex.log x) = x

@[simp]

theorem complex.range_exp :

set.range cexp = {0}ᶜ

theorem complex.log_exp {x : ℂ} (hx₁ : -real.pi < x.im) (hx₂ : x.im ≤ real.pi) :

complex.log (cexp 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 : cexp x = cexp y) :

x = y

theorem complex.of_real_log {x : ℝ} (hx : 0 ≤ x) :

↑(real.log x) = complex.log ↑x

theorem complex.log_of_real_re (x : ℝ) :

(complex.log ↑x).re = real.log x

theorem complex.log_of_real_mul {r : ℝ} (hr : 0 < r) {x : ℂ} (hx : x ≠ 0) :

complex.log (↑r * x) = ↑(real.log r) + complex.log x

theorem complex.log_mul_of_real (r : ℝ) (hr : 0 < r) (x : ℂ) (hx : x ≠ 0) :

complex.log (x * ↑r) = ↑(real.log r) + complex.log x

@[simp]

theorem complex.log_zero :

complex.log 0 = 0

@[simp]

theorem complex.log_one :

complex.log 1 = 0

theorem complex.log_neg_one :

complex.log (-1) = ↑real.pi * complex.I

theorem complex.log_I :

complex.log complex.I = ↑real.pi / 2 * complex.I

theorem complex.log_neg_I :

complex.log (-complex.I) = -(↑real.pi / 2) * complex.I

theorem complex.log_conj_eq_ite (x : ℂ) :

complex.log (⇑(star_ring_end ℂ) x) = ite (x.arg = real.pi) (complex.log x) (⇑(star_ring_end ℂ) (complex.log x))

theorem complex.log_conj (x : ℂ) (h : x.arg ≠ real.pi) :

complex.log (⇑(star_ring_end ℂ) x) = ⇑(star_ring_end ℂ) (complex.log x)

theorem complex.log_inv_eq_ite (x : ℂ) :

complex.log x⁻¹ = ite (x.arg = real.pi) (-⇑(star_ring_end ℂ) (complex.log x)) (-complex.log x)

theorem complex.log_inv (x : ℂ) (hx : x.arg ≠ real.pi) :

complex.log x⁻¹ = -complex.log x

theorem complex.two_pi_I_ne_zero :

2 * ↑real.pi * complex.I ≠ 0

theorem complex.exp_eq_one_iff {x : ℂ} :

cexp x = 1 ↔ ∃ (n : ℤ), x = ↑n * (2 * ↑real.pi * complex.I)

theorem complex.exp_eq_exp_iff_exp_sub_eq_one {x y : ℂ} :

cexp x = cexp y ↔ cexp (x - y) = 1

theorem complex.exp_eq_exp_iff_exists_int {x y : ℂ} :

cexp x = cexp y ↔ ∃ (n : ℤ), x = y + ↑n * (2 * ↑real.pi * complex.I)

@[simp]

theorem complex.countable_preimage_exp {s : set ℂ} :

(cexp ⁻¹' s).countable ↔ s.countable

theorem set.countable.preimage_cexp {s : set ℂ} :

s.countable → (cexp ⁻¹' s).countable

Alias of the reverse direction of complex.countable_preimage_exp.

theorem complex.tendsto_log_nhds_within_im_neg_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0) (him : z.im = 0) :

filter.tendsto complex.log (nhds_within z {z : ℂ | z.im < 0}) (nhds (↑(real.log (⇑complex.abs z)) - ↑real.pi * complex.I))

theorem complex.continuous_within_at_log_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0) (him : z.im = 0) :

continuous_within_at complex.log {z : ℂ | 0 ≤ z.im} z

theorem complex.tendsto_log_nhds_within_im_nonneg_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0) (him : z.im = 0) :

filter.tendsto complex.log (nhds_within z {z : ℂ | 0 ≤ z.im}) (nhds (↑(real.log (⇑complex.abs z)) + ↑real.pi * complex.I))

@[simp]

theorem complex.map_exp_comap_re_at_bot :

filter.map cexp (filter.comap complex.re filter.at_bot) = nhds_within 0 {0}ᶜ

@[simp]

theorem complex.map_exp_comap_re_at_top :

filter.map cexp (filter.comap complex.re filter.at_top) = filter.comap ⇑complex.abs filter.at_top

theorem continuous_at_clog {x : ℂ} (h : 0 < x.re ∨ x.im ≠ 0) :

continuous_at complex.log x

theorem filter.tendsto.clog {α : Type u_1} {l : filter α} {f : α → ℂ} {x : ℂ} (h : filter.tendsto f l (nhds x)) (hx : 0 < x.re ∨ x.im ≠ 0) :

filter.tendsto (λ (t : α), complex.log (f t)) l (nhds (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 ∈ s → 0 < (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))