mathlib documentation

analysis.special_functions.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

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

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

complex.log (complex.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 : complex.exp x = complex.exp 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

@[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.two_pi_I_ne_zero :

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

theorem complex.exp_eq_one_iff {x : ℂ} :

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

theorem complex.exp_eq_exp_iff_exp_sub_eq_one {x y : ℂ} :

complex.exp x = complex.exp y ↔ complex.exp (x - y) = 1

theorem complex.exp_eq_exp_iff_exists_int {x y : ℂ} :

complex.exp x = complex.exp y ↔ ∃ (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 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 (𝓝[{z : ℂ | z.im < 0}] z) (𝓝 (↑(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 (𝓝[{z : ℂ | 0 ≤ z.im}] z) (𝓝 (↑(real.log (complex.abs z)) + (↑real.pi) * complex.I))

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 (𝓝 x)) (hx : 0 < x.re ∨ x.im ≠ 0) :

filter.tendsto (λ (t : α), complex.log (f t)) l (𝓝 (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))