1.1. Data structure for complex numbers🔗

section Complex_arithmetic

We define a complex number as an ordered pair of real numbers (a, b).

In Mathlib, complex number is represented by structure Complex with two fields re and im, representing the real and imaginary parts respectively.

structure Complex : Type where
  /-- The real part of a complex number. -/
  re : ℝ
  /-- The imaginary part of a complex number. -/
  im : ℝ

We can represent a complex number as a pair, using the notation ⟨a,b⟩ or (a,b).

We construct a complex number using the constructor Complex.mk or the notation ⟨a,b⟩ for real numbers a and b.

Example.

def z1 : ℂ := Complex.mk 3 (-5) -- using constructor
def z2 : ℂ := ⟨3, -5⟩ -- using the notation ⟨a,b⟩

The two complex numbers z1 and z2 above are equal by definition.

example : z1 = z2 := by⊢ z1 = z2 rflAll goals completed! 🐙

The real and imaginary parts of a complex number can be accessed by the projection functions Complex.re and Complex.im respectively.

Real.ofCauchy (sorry /- 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, ... -/)#eval Complex.re ⟨3,-5⟩
Real.ofCauchy (sorry /- -5, -5, -5, -5, -5, -5, -5, -5, -5, -5, ... -/)#eval Complex.im ⟨3,-5⟩

example : Complex.re ⟨3,-5⟩ = 3 := by⊢ { re := 3, im := -5 }.re = 3 norm_numAll goals completed! 🐙
example : Complex.im ⟨3,-5⟩ = -5 := by⊢ { re := 3, im := -5 }.im = -5 norm_numAll goals completed! 🐙

Addition and Multiplicaiton.

Complex addition is the same as vector addition.

(a,b) + (c,d) = (a+c, b+d).

Complex multiplication is defined by

(a,b)·(c,d) = (ad-bc, ac+bd).

example (a b c d : ℝ) : (Complex.mk a b) + (Complex.mk c d)
   = Complex.mk (a+c) (b+d) := bya:ℝb:ℝc:ℝd:ℝ⊢ { re := a, im := b } + { re := c, im := d } = { re := a + c, im := b + d } rflAll goals completed! 🐙

example (a b c d : ℝ) : (Complex.mk a b) * (Complex.mk c d)
    = Complex.mk (a*c-b*d) (a*d+b*c):= bya:ℝb:ℝc:ℝd:ℝ⊢ { re := a, im := b } * { re := c, im := d } = { re := a * c - b * d, im := a * d + b * c }
  apply Complex.extaa:ℝb:ℝc:ℝd:ℝ⊢ ({ re := a, im := b } * { re := c, im := d }).re = { re := a * c - b * d, im := a * d + b * c }.reaa:ℝb:ℝc:ℝd:ℝ⊢ ({ re := a, im := b } * { re := c, im := d }).im = { re := a * c - b * d, im := a * d + b * c }.im <;>aa:ℝb:ℝc:ℝd:ℝ⊢ ({ re := a, im := b } * { re := c, im := d }).re = { re := a * c - b * d, im := a * d + b * c }.reaa:ℝb:ℝc:ℝd:ℝ⊢ ({ re := a, im := b } * { re := c, im := d }).im = { re := a * c - b * d, im := a * d + b * c }.im
  simpAll goals completed! 🐙

The imaginary unit I is defined as the complex number with zero real part and imaginary part equal to 1. The following example shows that I is equal to the ordered pair ⟨0,1⟩ by definition.

example : I = ⟨0,1⟩ := by⊢ I = { re := 0, im := 1 } rflAll goals completed! 🐙

A complex number is purely imaginary if its real part is zero.

def is_purely_imaginary (z : ℂ) : Prop :=
  re z = 0

example (a : ℝ) : is_purely_imaginary ⟨0, a⟩ := bya:ℝ⊢ is_purely_imaginary { re := 0, im := a }
  unfold is_purely_imaginarya:ℝ⊢ { re := 0, im := a }.re = 0
  rflAll goals completed! 🐙

/-- Prove that (a + ai)^2 is purely imaginary -/
example (a : ℝ) : is_purely_imaginary (⟨a, a⟩^2) := bya:ℝ⊢ is_purely_imaginary ({ re := a, im := a } ^ 2)
  unfold is_purely_imaginarya:ℝ⊢ ({ re := a, im := a } ^ 2).re = 0
  have h : ( (Complex.mk a a)^2 ).re = a*a - a*a := bya:ℝ⊢ is_purely_imaginary ({ re := a, im := a } ^ 2)
    simp [pow_two]All goals completed! 🐙
  simp [h]All goals completed! 🐙

Example. Show that

(\sqrt{2} - i) - i(1- \sqrt{2}i) = -2i.

/--  (√2-i) -i * (1-√2i) = -2i -/
example : (√2 - I) - I * (1 - √2 * I) = -2 * I := by⊢ ↑√2 - I - I * (1 - ↑√2 * I) = -2 * I
  calc
      -- (√2-i)	-i(1-√2i)
        (√2 - I) - I * (1 - √2 * I)
      -- = √2-i-i+√2*i*i
      = √2- I - I + √2  * (I * I) := by⊢ ↑√2 - I - I * (1 - ↑√2 * I) = ↑√2 - I - I + ↑√2 * (I * I) ringAll goals completed! 🐙
      -- = √2-i-i+√2*(-1)
    _ = √2  - I - I + √2 * (-1) := by⊢ ↑√2 - I - I + ↑√2 * (I * I) = ↑√2 - I - I + ↑√2 * -1 rw [I_mul_I]All goals completed! 🐙
    _ = -2 * I := by⊢ ↑√2 - I - I + ↑√2 * -1 = -2 * I ringAll goals completed! 🐙

We next show that there is no zero divisor in the field of complex numbers.

example (z1 z2 : ℂ) : z1 * z2 = 0 → z1 = 0 ∨ z2 = 0 := byz1:ℂz2:ℂ⊢ z1 * z2 = 0 → z1 = 0 ∨ z2 = 0
  intro hz1:ℂz2:ℂh:z1 * z2 = 0⊢ z1 = 0 ∨ z2 = 0
  by_cases hz1 : z1 = 0posz1:ℂz2:ℂh:z1 * z2 = 0hz1:z1 = 0⊢ z1 = 0 ∨ z2 = 0negz1:ℂz2:ℂh:z1 * z2 = 0hz1:¬z1 = 0⊢ z1 = 0 ∨ z2 = 0
  ·posz1:ℂz2:ℂh:z1 * z2 = 0hz1:z1 = 0⊢ z1 = 0 ∨ z2 = 0 leftpos.hz1:ℂz2:ℂh:z1 * z2 = 0hz1:z1 = 0⊢ z1 = 0; exact hz1All goals completed! 🐙
  ·negz1:ℂz2:ℂh:z1 * z2 = 0hz1:¬z1 = 0⊢ z1 = 0 ∨ z2 = 0 -- z1 ≠ 0, so it has an inverse
    -- multiply the equation z1 * z2 = 0 by z1⁻¹
    have inv_mul : z1⁻¹ * z1 = 1 := byz1:ℂz2:ℂ⊢ z1 * z2 = 0 → z1 = 0 ∨ z2 = 0
      calc
        z1⁻¹ * z1 = z1 * z1⁻¹ := byz1:ℂz2:ℂh:z1 * z2 = 0hz1:¬z1 = 0⊢ z1⁻¹ * z1 = z1 * z1⁻¹ simp [mul_comm]All goals completed! 🐙
        _ = 1 := byz1:ℂz2:ℂh:z1 * z2 = 0hz1:¬z1 = 0⊢ z1 * z1⁻¹ = 1 exact Complex.mul_inv_cancel hz1All goals completed! 🐙
    have : z2 = z1⁻¹ * (z1 * z2) := byz1:ℂz2:ℂ⊢ z1 * z2 = 0 → z1 = 0 ∨ z2 = 0
      calc
        z2 = 1 * z2 := byz1:ℂz2:ℂh:z1 * z2 = 0hz1:¬z1 = 0inv_mul:z1⁻¹ * z1 = 1⊢ z2 = 1 * z2 simpAll goals completed! 🐙
        _  = (z1⁻¹ * z1) * z2 := byz1:ℂz2:ℂh:z1 * z2 = 0hz1:¬z1 = 0inv_mul:z1⁻¹ * z1 = 1⊢ 1 * z2 = z1⁻¹ * z1 * z2 simp [inv_mul]All goals completed! 🐙
        _  = z1⁻¹ * (z1 * z2) := byz1:ℂz2:ℂh:z1 * z2 = 0hz1:¬z1 = 0inv_mul:z1⁻¹ * z1 = 1⊢ z1⁻¹ * z1 * z2 = z1⁻¹ * (z1 * z2) simp [mul_assoc]All goals completed! 🐙
    -- now we want to show z1 = 0 ∨ z2 = 0
    -- use h to conclude z2 = 0
    rightneg.hz1:ℂz2:ℂh:z1 * z2 = 0hz1:¬z1 = 0inv_mul:z1⁻¹ * z1 = 1this:z2 = z1⁻¹ * (z1 * z2)⊢ z2 = 0
    calc
      z2 = z1⁻¹ * (z1 * z2) := this
      _  = z1⁻¹ * 0 := byz1:ℂz2:ℂh:z1 * z2 = 0hz1:¬z1 = 0inv_mul:z1⁻¹ * z1 = 1this:z2 = z1⁻¹ * (z1 * z2)⊢ z1⁻¹ * (z1 * z2) = z1⁻¹ * 0 simp [h]All goals completed! 🐙
      _  = 0 := byz1:ℂz2:ℂh:z1 * z2 = 0hz1:¬z1 = 0inv_mul:z1⁻¹ * z1 = 1this:z2 = z1⁻¹ * (z1 * z2)⊢ z1⁻¹ * 0 = 0 simpAll goals completed! 🐙

Example. Prove

(1+i)^{1024} = 2^{512},

by using the fact that (1+i)^2 = 2i, and i^4=1.

/-- Prove that (1 + i)^1024 = 2^512 -/
example : (1 + I) ^ 1024 = 2 ^ 512 := by⊢ (1 + I) ^ 1024 = 2 ^ 512
  calc
    (1 + I) ^ 1024
      = (1 + I) ^ (2 * 512) := by⊢ (1 + I) ^ 1024 = (1 + I) ^ (2 * 512) rflAll goals completed! 🐙
    _ = ((1 + I) ^ 2) ^ 512 := by⊢ (1 + I) ^ (2 * 512) = ((1 + I) ^ 2) ^ 512 rw [pow_mul]All goals completed! 🐙
    _ = (2 * I) ^ 512 := by⊢ ((1 + I) ^ 2) ^ 512 = (2 * I) ^ 512
          congre_a⊢ (1 + I) ^ 2 = 2 * I
          -- (1+i)^2 = 2i
          ring_nfe_a⊢ 1 + I * 2 + I ^ 2 = I * 2
          simp [I_sq]All goals completed! 🐙
    _ = (2 : ℂ) ^ 512 * I ^ 512 := by⊢ (2 * I) ^ 512 = 2 ^ 512 * I ^ 512 rw [mul_pow]All goals completed! 🐙
    _ = (2 : ℂ) ^ 512 * 1 := by⊢ 2 ^ 512 * I ^ 512 = 2 ^ 512 * 1
          -- Focus on proving I^512 = 1
          congr 1e_a⊢ I ^ 512 = 1
          have h_idx : 512 = 4 * 128 := by⊢ 2 ^ 512 * I ^ 512 = 2 ^ 512 * 1 rflAll goals completed! 🐙
          -- Now we rewrite  the target:
          -- I^(4*128) -> (I^4)^128 -> 1^128 -> 1
          rw [h_idx, pow_mul, Complex.I_pow_four, one_pow]All goals completed! 🐙
    _ = (2 : ℂ) ^ 512 := by⊢ 2 ^ 512 * 1 = 2 ^ 512 rw [mul_one]All goals completed! 🐙

end Complex_arithmetic