mathlib documentation

data.complex.basic

The complex numbers

The complex numbers are modelled as ℝ^2 in the obvious way.

Definition and basic arithmmetic

source
structure complex  :
Type

Complex numbers consist of two reals: a real part re and an imaginary part im.

source
@[instance]
def complex.decidable_eq  :
decidable_eq ℂ

Equations
source
def complex.equiv_real_prod  :
ℂ ≃ ℝ × ℝ

The equivalence between the complex numbers and ℝ × ℝ.

Equations
source
@[simp]
theorem complex.equiv_real_prod_apply (z : ℂ) :
⇑complex.equiv_real_prod z = (z.re, z.im)

source
theorem complex.equiv_real_prod_symm_re (x y : ℝ) :
(⇑(complex.equiv_real_prod.symm) (x, y)).re = x

source
theorem complex.equiv_real_prod_symm_im (x y : ℝ) :
(⇑(complex.equiv_real_prod.symm) (x, y)).im = y

source
@[simp]
theorem complex.eta (z : ℂ) :
{re := z.re, im := z.im} = z

source
@[ext]
theorem complex.ext {z w : ℂ} (a : z.re = w.re) (a_1 : z.im = w.im) :
z = w

source
theorem complex.ext_iff {z w : ℂ} :
z = w ↔ z.re = w.re ∧ z.im = w.im

source
@[instance]
def complex.has_coe  :
has_coe ℝ ℂ

Equations
source
@[simp]
theorem complex.of_real_re (r : ℝ) :
↑r.re = r

source
@[simp]
theorem complex.of_real_im (r : ℝ) :
↑r.im = 0

source
@[simp]
theorem complex.of_real_inj {z w : ℝ} :
↑z = ↑w ↔ z = w

source
@[instance]
def complex.has_zero  :
has_zero ℂ

Equations
source
@[instance]
def complex.inhabited  :
inhabited ℂ

Equations
source
@[simp]
theorem complex.zero_re  :
0.re = 0

source
@[simp]
theorem complex.zero_im  :
0.im = 0

source
@[simp]
theorem complex.of_real_zero  :
↑0 = 0

source
@[simp]
theorem complex.of_real_eq_zero {z : ℝ} :
↑z = 0 ↔ z = 0

source
theorem complex.of_real_ne_zero {z : ℝ} :
↑z ≠ 0 ↔ z ≠ 0

source
@[instance]
def complex.has_one  :
has_one ℂ

Equations
source
@[simp]
theorem complex.one_re  :
1.re = 1

source
@[simp]
theorem complex.one_im  :
1.im = 0

source
@[simp]
theorem complex.of_real_one  :
↑1 = 1

source
@[instance]
def complex.has_add  :
has_add ℂ

Equations
source
@[simp]
theorem complex.add_re (z w : ℂ) :
(z + w).re = z.re + w.re

source
@[simp]
theorem complex.add_im (z w : ℂ) :
(z + w).im = z.im + w.im

source
@[simp]
theorem complex.bit0_re (z : ℂ) :
(bit0 z).re = bit0 z.re

source
@[simp]
theorem complex.bit1_re (z : ℂ) :
(bit1 z).re = bit1 z.re

source
@[simp]
theorem complex.bit0_im (z : ℂ) :
(bit0 z).im = bit0 z.im

source
@[simp]
theorem complex.bit1_im (z : ℂ) :
(bit1 z).im = bit0 z.im

source
@[simp]
theorem complex.of_real_add (r s : ℝ) :
↑(r + s) = ↑r + ↑s

source
@[simp]
theorem complex.of_real_bit0 (r : ℝ) :
↑(bit0 r) = bit0 ↑r

source
@[simp]
theorem complex.of_real_bit1 (r : ℝ) :
↑(bit1 r) = bit1 ↑r

source
@[instance]
def complex.has_neg  :
has_neg ℂ

Equations
source
@[simp]
theorem complex.neg_re (z : ℂ) :
(-z).re = -z.re

source
@[simp]
theorem complex.neg_im (z : ℂ) :
(-z).im = -z.im

source
@[simp]
theorem complex.of_real_neg (r : ℝ) :
↑-r = -↑r

source
@[instance]
def complex.has_mul  :
has_mul ℂ

Equations
source
@[simp]
theorem complex.mul_re (z w : ℂ) :
(z * w).re = (z.re) * w.re - (z.im) * w.im

source
@[simp]
theorem complex.mul_im (z w : ℂ) :
(z * w).im = (z.re) * w.im + (z.im) * w.re

source
@[simp]
theorem complex.of_real_mul (r s : ℝ) :
↑r * s = (↑r) * ↑s

source
theorem complex.smul_re (r : ℝ) (z : ℂ) :
((↑r) * z).re = r * z.re

source
theorem complex.smul_im (r : ℝ) (z : ℂ) :
((↑r) * z).im = r * z.im

source
theorem complex.of_real_smul (r : ℝ) (z : ℂ) :
(↑r) * z = {re := r * z.re, im := r * z.im}

The imaginary unit, I

source
def complex.I  :
ℂ

The imaginary unit.

Equations
source
@[simp]
theorem complex.I_re  :
complex.I.re = 0

source
@[simp]
theorem complex.I_im  :
complex.I.im = 1

source
@[simp]
theorem complex.I_mul_I  :
complex.I * complex.I = -1

source
theorem complex.I_mul (z : ℂ) :
complex.I * z = {re := -z.im, im := z.re}

source
theorem complex.I_ne_zero  :
complex.I ≠ 0

source
theorem complex.mk_eq_add_mul_I (a b : ℝ) :
{re := a, im := b} = ↑a + (↑b) * complex.I

source
@[simp]
theorem complex.re_add_im (z : ℂ) :
↑(z.re) + (↑(z.im)) * complex.I = z

Commutative ring instance and lemmas

source
@[instance]
def complex.comm_ring  :
comm_ring ℂ

Equations
source
@[instance]
def complex.re.is_add_group_hom  :
is_add_group_hom complex.re

source
@[instance]
def complex.im.is_add_group_hom  :
is_add_group_hom complex.im

Complex conjugation

source
def complex.conj  :
ℂ →+* ℂ

The complex conjugate.

Equations
source
@[simp]
theorem complex.conj_re (z : ℂ) :
(⇑complex.conj z).re = z.re

source
@[simp]
theorem complex.conj_im (z : ℂ) :
(⇑complex.conj z).im = -z.im

source
@[simp]
theorem complex.conj_of_real (r : ℝ) :
⇑complex.conj ↑r = ↑r

source
@[simp]
theorem complex.conj_I  :
⇑complex.conj complex.I = -complex.I

source
@[simp]
theorem complex.conj_bit0 (z : ℂ) :
⇑complex.conj (bit0 z) = bit0 (⇑complex.conj z)

source
@[simp]
theorem complex.conj_bit1 (z : ℂ) :
⇑complex.conj (bit1 z) = bit1 (⇑complex.conj z)

source
@[simp]
theorem complex.conj_neg_I  :
⇑complex.conj (-complex.I) = complex.I

source
@[simp]
theorem complex.conj_conj (z : ℂ) :
⇑complex.conj (⇑complex.conj z) = z

source
theorem complex.conj_involutive  :
function.involutive ⇑complex.conj

source
theorem complex.conj_bijective  :
function.bijective ⇑complex.conj

source
theorem complex.conj_inj {z w : ℂ} :
⇑complex.conj z = ⇑complex.conj w ↔ z = w

source
@[simp]
theorem complex.conj_eq_zero {z : ℂ} :
⇑complex.conj z = 0 ↔ z = 0

source
theorem complex.eq_conj_iff_real {z : ℂ} :
⇑complex.conj z = z ↔ ∃ (r : ℝ), z = ↑r

source
theorem complex.eq_conj_iff_re {z : ℂ} :
⇑complex.conj z = z ↔ ↑(z.re) = z

Norm squared

source
def complex.norm_sq (z : ℂ) :
ℝ

The norm squared function.

Equations
source
@[simp]
theorem complex.norm_sq_of_real (r : ℝ) :
complex.norm_sq ↑r = r * r

source
@[simp]
theorem complex.norm_sq_zero  :
complex.norm_sq 0 = 0

source
@[simp]
theorem complex.norm_sq_one  :
complex.norm_sq 1 = 1

source
@[simp]
theorem complex.norm_sq_I  :
complex.norm_sq complex.I = 1

source
theorem complex.norm_sq_nonneg (z : ℂ) :
0 ≤ complex.norm_sq z

source
@[simp]
theorem complex.norm_sq_eq_zero {z : ℂ} :
complex.norm_sq z = 0 ↔ z = 0

source
@[simp]
theorem complex.norm_sq_pos {z : ℂ} :
0 < complex.norm_sq z ↔ z ≠ 0

source
@[simp]
theorem complex.norm_sq_neg (z : ℂ) :
complex.norm_sq (-z) = complex.norm_sq z

source
@[simp]
theorem complex.norm_sq_conj (z : ℂ) :
complex.norm_sq (⇑complex.conj z) = complex.norm_sq z

source
@[simp]
theorem complex.norm_sq_mul (z w : ℂ) :
complex.norm_sq (z * w) = (complex.norm_sq z) * complex.norm_sq w

source
theorem complex.norm_sq_add (z w : ℂ) :
complex.norm_sq (z + w) = complex.norm_sq z + complex.norm_sq w + 2 * (z * ⇑complex.conj w).re

source
theorem complex.re_sq_le_norm_sq (z : ℂ) :
(z.re) * z.re ≤ complex.norm_sq z

source
theorem complex.im_sq_le_norm_sq (z : ℂ) :
(z.im) * z.im ≤ complex.norm_sq z

source
theorem complex.mul_conj (z : ℂ) :
z * ⇑complex.conj z = ↑(complex.norm_sq z)

source
theorem complex.add_conj (z : ℂ) :
z + ⇑complex.conj z = ↑2 * z.re

source
def complex.of_real  :
ℝ →+* ℂ

The coercion ℝ → ℂ as a ring_hom.

Equations
source
@[simp]
theorem complex.of_real_eq_coe (r : ℝ) :
⇑complex.of_real r = ↑r

source
@[simp]
theorem complex.I_sq  :
complex.I ^ 2 = -1

source
@[simp]
theorem complex.sub_re (z w : ℂ) :
(z - w).re = z.re - w.re

source
@[simp]
theorem complex.sub_im (z w : ℂ) :
(z - w).im = z.im - w.im

source
@[simp]
theorem complex.of_real_sub (r s : ℝ) :
↑(r - s) = ↑r - ↑s

source
@[simp]
theorem complex.of_real_pow (r : ℝ) (n : ℕ) :
↑(r ^ n) = ↑r ^ n

source
theorem complex.sub_conj (z : ℂ) :
z - ⇑complex.conj z = (↑2 * z.im) * complex.I

source
theorem complex.norm_sq_sub (z w : ℂ) :
complex.norm_sq (z - w) = complex.norm_sq z + complex.norm_sq w - 2 * (z * ⇑complex.conj w).re

Inversion

source
@[instance]
def complex.has_inv  :
has_inv ℂ

Equations
source
theorem complex.inv_def (z : ℂ) :
z⁻¹ = (⇑complex.conj z) * ↑(complex.norm_sq z)⁻¹

source
@[simp]
theorem complex.inv_re (z : ℂ) :
z⁻¹.re = z.re / complex.norm_sq z

source
@[simp]
theorem complex.inv_im (z : ℂ) :
z⁻¹.im = -z.im / complex.norm_sq z

source
@[simp]
theorem complex.of_real_inv (r : ℝ) :
↑r⁻¹ = (↑r)⁻¹

source
theorem complex.inv_zero  :
0⁻¹ = 0

source
theorem complex.mul_inv_cancel {z : ℂ} (h : z ≠ 0) :
z * z⁻¹ = 1

Field instance and lemmas

source
@[instance]
def complex.field  :
field ℂ

Equations
source
theorem complex.div_re (z w : ℂ) :
(z / w).re = (z.re) * w.re / complex.norm_sq w + (z.im) * w.im / complex.norm_sq w

source
theorem complex.div_im (z w : ℂ) :
(z / w).im = (z.im) * w.re / complex.norm_sq w - (z.re) * w.im / complex.norm_sq w

source
@[simp]
theorem complex.of_real_div (r s : ℝ) :
↑(r / s) = ↑r / ↑s

source
@[simp]
theorem complex.of_real_fpow (r : ℝ) (n : ℤ) :
↑(r ^ n) = ↑r ^ n

source
@[simp]
theorem complex.div_I (z : ℂ) :
z / complex.I = -z * complex.I

source
@[simp]
theorem complex.inv_I  :
complex.I⁻¹ = -complex.I

source
@[simp]
theorem complex.norm_sq_inv (z : ℂ) :
complex.norm_sq z⁻¹ = (complex.norm_sq z)⁻¹

source
@[simp]
theorem complex.norm_sq_div (z w : ℂ) :
complex.norm_sq (z / w) = complex.norm_sq z / complex.norm_sq w

Cast lemmas

source
@[simp]
theorem complex.of_real_nat_cast (n : ℕ) :
↑↑n = ↑n

source
@[simp]
theorem complex.nat_cast_re (n : ℕ) :
↑n.re = ↑n

source
@[simp]
theorem complex.nat_cast_im (n : ℕ) :
↑n.im = 0

source
@[simp]
theorem complex.of_real_int_cast (n : ℤ) :
↑↑n = ↑n

source
@[simp]
theorem complex.int_cast_re (n : ℤ) :
↑n.re = ↑n

source
@[simp]
theorem complex.int_cast_im (n : ℤ) :
↑n.im = 0

source
@[simp]
theorem complex.of_real_rat_cast (n : ℚ) :
↑↑n = ↑n

source
@[simp]
theorem complex.rat_cast_re (q : ℚ) :
↑q.re = ↑q

source
@[simp]
theorem complex.rat_cast_im (q : ℚ) :
↑q.im = 0

Characteristic zero

source
@[instance]
def complex.char_zero_complex  :
char_zero ℂ

source
theorem complex.re_eq_add_conj (z : ℂ) :
↑(z.re) = (z + ⇑complex.conj z) / 2

Absolute value

source
def complex.abs (z : ℂ) :
ℝ

The complex absolute value function, defined as the square root of the norm squared.

Equations
source
@[simp]
theorem complex.abs_of_real (r : ℝ) :
complex.abs ↑r = abs r

source
theorem complex.abs_of_nonneg {r : ℝ} (h : 0 ≤ r) :
complex.abs ↑r = r

source
theorem complex.abs_of_nat (n : ℕ) :
complex.abs ↑n = ↑n

source
theorem complex.mul_self_abs (z : ℂ) :
(complex.abs z) * complex.abs z = complex.norm_sq z

source
@[simp]
theorem complex.abs_zero  :
complex.abs 0 = 0

source
@[simp]
theorem complex.abs_one  :
complex.abs 1 = 1

source
@[simp]
theorem complex.abs_I  :
complex.abs complex.I = 1

source
@[simp]
theorem complex.abs_two  :
complex.abs 2 = 2

source
theorem complex.abs_nonneg (z : ℂ) :
0 ≤ complex.abs z

source
@[simp]
theorem complex.abs_eq_zero {z : ℂ} :
complex.abs z = 0 ↔ z = 0

source
theorem complex.abs_ne_zero {z : ℂ} :
complex.abs z ≠ 0 ↔ z ≠ 0

source
@[simp]
theorem complex.abs_conj (z : ℂ) :
complex.abs (⇑complex.conj z) = complex.abs z

source
@[simp]
theorem complex.abs_mul (z w : ℂ) :
complex.abs (z * w) = (complex.abs z) * complex.abs w

source
theorem complex.abs_re_le_abs (z : ℂ) :
abs z.re ≤ complex.abs z

source
theorem complex.abs_im_le_abs (z : ℂ) :
abs z.im ≤ complex.abs z

source
theorem complex.re_le_abs (z : ℂ) :
z.re ≤ complex.abs z

source
theorem complex.im_le_abs (z : ℂ) :
z.im ≤ complex.abs z

source
theorem complex.abs_add (z w : ℂ) :
complex.abs (z + w) ≤ complex.abs z + complex.abs w

source
@[instance]
def complex.is_absolute_value  :
is_absolute_value complex.abs

source
@[simp]
theorem complex.abs_abs (z : ℂ) :
abs (complex.abs z) = complex.abs z

source
@[simp]
theorem complex.abs_pos {z : ℂ} :
0 < complex.abs z ↔ z ≠ 0

source
@[simp]
theorem complex.abs_neg (z : ℂ) :
complex.abs (-z) = complex.abs z

source
theorem complex.abs_sub (z w : ℂ) :
complex.abs (z - w) = complex.abs (w - z)

source
theorem complex.abs_sub_le (a b c : ℂ) :
complex.abs (a - c) ≤ complex.abs (a - b) + complex.abs (b - c)

source
@[simp]
theorem complex.abs_inv (z : ℂ) :
complex.abs z⁻¹ = (complex.abs z)⁻¹

source
@[simp]
theorem complex.abs_div (z w : ℂ) :
complex.abs (z / w) = complex.abs z / complex.abs w

source
theorem complex.abs_abs_sub_le_abs_sub (z w : ℂ) :
abs (complex.abs z - complex.abs w) ≤ complex.abs (z - w)

source
theorem complex.abs_le_abs_re_add_abs_im (z : ℂ) :
complex.abs z ≤ abs z.re + abs z.im

source
theorem complex.abs_re_div_abs_le_one (z : ℂ) :
abs (z.re / complex.abs z) ≤ 1

source
theorem complex.abs_im_div_abs_le_one (z : ℂ) :
abs (z.im / complex.abs z) ≤ 1

source
@[simp]
theorem complex.abs_cast_nat (n : ℕ) :
complex.abs ↑n = ↑n

source
theorem complex.norm_sq_eq_abs (x : ℂ) :
complex.norm_sq x = complex.abs x ^ 2

Cauchy sequences

source
theorem complex.is_cau_seq_re (f : cau_seq ℂ complex.abs) :
is_cau_seq abs (λ (n : ℕ), (⇑f n).re)

source
theorem complex.is_cau_seq_im (f : cau_seq ℂ complex.abs) :
is_cau_seq abs (λ (n : ℕ), (⇑f n).im)

source
def complex.cau_seq_re (f : cau_seq ℂ complex.abs) :
cau_seq ℝ abs

The real part of a complex Cauchy sequence, as a real Cauchy sequence.

Equations
source
def complex.cau_seq_im (f : cau_seq ℂ complex.abs) :
cau_seq ℝ abs

The imaginary part of a complex Cauchy sequence, as a real Cauchy sequence.

Equations
source
theorem complex.is_cau_seq_abs {f : ℕ → ℂ} (hf : is_cau_seq complex.abs f) :
is_cau_seq abs (complex.abs ∘ f)

source
def complex.lim_aux (f : cau_seq ℂ complex.abs) :
ℂ

The limit of a Cauchy sequence of complex numbers.

Equations
source
theorem complex.equiv_lim_aux (f : cau_seq ℂ complex.abs) :
f ≈ cau_seq.const complex.abs (complex.lim_aux f)

source
@[instance]
def complex.cau_seq.is_complete  :
cau_seq.is_complete ℂ complex.abs

Equations
source
theorem complex.lim_eq_lim_im_add_lim_re (f : cau_seq ℂ complex.abs) :
f.lim = ↑((complex.cau_seq_re f).lim) + (↑((complex.cau_seq_im f).lim)) * complex.I

source
theorem complex.lim_re (f : cau_seq ℂ complex.abs) :
(complex.cau_seq_re f).lim = f.lim.re

source
theorem complex.lim_im (f : cau_seq ℂ complex.abs) :
(complex.cau_seq_im f).lim = f.lim.im

source
theorem complex.is_cau_seq_conj (f : cau_seq ℂ complex.abs) :
is_cau_seq complex.abs (λ (n : ℕ), ⇑complex.conj (⇑f n))

source
def complex.cau_seq_conj (f : cau_seq ℂ complex.abs) :
cau_seq ℂ complex.abs

The complex conjugate of a complex Cauchy sequence, as a complex Cauchy sequence.

Equations
source
theorem complex.lim_conj (f : cau_seq ℂ complex.abs) :
(complex.cau_seq_conj f).lim = ⇑complex.conj f.lim

source
def complex.cau_seq_abs (f : cau_seq ℂ complex.abs) :
cau_seq ℝ abs

The absolute value of a complex Cauchy sequence, as a real Cauchy sequence.

Equations
source
theorem complex.lim_abs (f : cau_seq ℂ complex.abs) :
(complex.cau_seq_abs f).lim = complex.abs f.lim