/-1The complex numbers.2A documented remix of part of mathlib34Our goal is to define the complex numbers, and then "extract some API".5Our first goal is to define addition and multiplication,6and prove that the complex numbers are a commutative ring.7We then do a slightly more computer-sciency worked development of the8natural inclusion from the reals to the complexes.910There are then a bunch of API-building exercises, which can be solved in term mode11or tactic mode. The first is `I`, the second is complex conjugation,12and the third is the "squared norm" function.1314There is then a speculative last exercise on harder properties15of the complexes.16-/1718-- We will assume that the real numbers are a field.19import data.real.basic2021/-- A complex number is defined to be a structure consisting of two real numbers,22the real part and the imaginary part of the complex number . -/23structure complex : Type :=24(re : ℝ) (im : ℝ)2526-- Let's use the usual notation for the complex numbers27notation `ℂ` := complex2829-- You make the complex number with real part 3 and imaginary part 4 like this:30example : ℂ :=31{ re := 3,32im := 4 }3334-- Or like this:35example : ℂ := complex.mk 3 43637-- or like this:38example : ℂ := ⟨3, 4⟩3940-- They all give the same complex number.4142-- If you have a complex number, then you can get its real and43-- imaginary parts with the `complex.re` and `complex.im` functions.4445example : ℝ := complex.re(complex.mk 3 4) -- this term is (3 : ℝ)4647example : complex.re(complex.mk 3 4) = 3 := rfl -- true by definition.4849-- We clearly don't want to be constantly saying `complex.blah` so let's50-- move into the `complex` namespace5152namespace complex5354-- All our theorems and definitions will now be called complex.something,55-- and we can in general just drop `complex.`5657-- For example5859example : re(mk 3 4) = 3 := rfl6061-- Computer scientists prefer the style `z.re` to `re(z)` for some reason.6263example : (mk 3 4).re = 3 := rfl6465example (z : ℂ) : re(z) = z.re := rfl6667-- We now prove the basic theorems and make the basic definitions for68-- complex numbers. For example, we will define addition and multiplication on69-- the complex numbers, and prove that it is a commutative ring.7071/-! # Mathematical trivialities -/7273-- We start with some facts about complex numbers which are so obvious that we do not74-- often explicitly state them. The first is that if z is a complex number, then75-- the complex number with real part re(z) and imaginary part im(z) is equal to z.76-- This is called eta reduction in type theory. Let's work through the77-- simple tactic mode proof.7879example : ∀ z : ℂ, complex.mk z.re z.im = z :=80begin81intro z,82cases z with x y,83-- goal now looks complicated, and contains terms which look84-- like {re := a, im := b}.re which obviously simplify to a.85-- The `dsimp` tactic will do some tidying up for us, although86-- it is not logically necessary. `dsimp` does definitional simplification.87dsimp,88-- Now we see the goal can be solved by reflexivity89refl,90end9192-- The proof was "unfold everything, and it's true by definition".93-- This proof does not teach a mathematician anything, so we may as well write94-- it in term mode, because each tactic has a term equivalent.95-- The equation compiler does the `intro` and `cases` steps,96-- and `dsimp` was unnecessary -- the two sides of the equation97-- were definitionally equal.9899-- It's important we give this theorem a name, because we want `simp`100-- to be able to use it. In short, the `simp` tactic tries to solve101-- goals of the form A = B, when `refl` doesn't work (i.e. the goals are102-- not definitionally equal) but when any mathematician would be able103-- to simplify A and B via "obvious" steps such as `0 + x = x` or104-- `⟨z.re, z.im⟩ = z`. These things are sometimes not true by definition,105-- but they should be tagged as being well-known ways to simplify an equality.106-- When building our API for the complex numbers, if we prove a theorem of the107-- form `A = B` where `B` is a bit simpler than `A`, we should probably108-- tag it with the `@[simp]` attribute, so `simp` can use it.109110-- Note: `simp` does *not* prove "all simple things". It proves *equalities*.111-- It proves `A = B` when, and only when, it can do it by applying112-- its "simplification rules", where a simplification rule is simply a proof113-- of a theorem of the form `A = B` and `B` is simpler than `A`.114@[simp] theorem eta : ∀ z : ℂ, complex.mk z.re z.im = z115| ⟨x, y⟩ := rfl116117-- The second triviality is the assertion that two complex numbers118-- with the same and imaginary parts are equal. Again this is not119-- hard to prove, and mathematicians deem it not worth documenting.120121example (z w : ℂ) : z.re = w.re → z.im = w.im → z = w :=122begin123cases z with zr zi,124cases w,125intros, cc,126end127128-- This lemma is called extensionality by type theorists.129-- Here is another tactic mode proof. Note that we have moved130-- the z and w to the other side of the colon; this does not131-- change the fully expanded proof term. It shows the power132-- of the `rintros` tactic.133134example : ∀ z w : ℂ, z.re = w.re → z.im = w.im → z = w :=135begin136rintros ⟨zr, zi⟩ ⟨_, _⟩ ⟨rfl⟩ ⟨rfl⟩,137refl,138end139140-- `rintros` does `cases` as many times as you like using this cool `⟨, ⟩` syntax141-- for the case splits. Note that if you do cases on `h : a = b` then, because142-- `=` is notation for `eq`, an inductive type with one constructor `a = a`,143-- it will just delete `b` and change all `b`s to `a`s. That is one of the144-- things going on in the above proof.145146-- Here is the same proof in term mode. Even though it's obvious, we still147-- give it a name, namely `ext`. It's important to prove it, so we can148-- tag it with the `ext` attribute. If we do this, the `ext` tactic can use it.149-- The `ext` tactic applies all theorems of the form "two150-- objects are the same if they are made from the same pieces".151152@[ext]153theorem ext : ∀ {z w : ℂ}, z.re = w.re → z.im = w.im → z = w154| ⟨zr, zi⟩ ⟨_, _⟩ rfl rfl := rfl155156-- The theorem `complex.ext` is trivially true to a mathematician.157-- But it is often used: for example it will be used all the time158-- in our proof that the complex numbers are a ring.159160-- Note that `ext` is an implication -- if re(z)=re(w) and im(z)=im(w) then z=w.161-- The below variant `ext_iff` is the two-way implication: two complex162-- numbers are equal if and only if they have the same real and imaginary part.163-- Let's first see a tactic mode proof. See how the `ext` tactic is used?164-- After it is applied, we have two goals, both of which are hypotheses.165-- The semicolon means "apply the next tactic to all the goals produced by this one"166167example (z w : ℂ) : z = w ↔ z.re = w.re ∧ z.im = w.im :=168begin169split,170{ intro H,171simp [H]},172{173rintro ⟨hre, him⟩,174ext; assumption,175}176end177178-- Again this is easy to write in term mode, and no mathematician179-- wants to read the proof anyway.180181theorem ext_iff {z w : ℂ} : z = w ↔ z.re = w.re ∧ z.im = w.im :=182⟨λ H, by simp [H], and.rec ext⟩183184/-! # Main course: the complex numbers are a ring. -/185186-- Our goal is to prove that the complexes are a ring. Let's187-- define the structure first; the zero, one, addition and multiplication188-- on the complexes.189190/-! ## 0 -/191192-- Let's define the zero complex number. Once we have done this we will be193-- able to talk about (0 : ℂ).194195/-- notation: `0`, or (0 : ℂ), will mean the complex number with196real and imaginary part equal to (0 : ℝ). -/197instance : has_zero ℂ := ⟨⟨0, 0⟩⟩198199-- Let's prove its basic properties, all of which are true by definition,200-- and then tag them with the appropriate attributes.201@[simp] lemma zero_re : (0 : ℂ).re = 0 := rfl202@[simp] lemma zero_im : (0 : ℂ).im = 0 := rfl203204/-! ## 1 -/205206-- Now let's do the same thing for 1.207208/-- Notation `1` or `(1 : ℂ)`, means `⟨(1 : ℝ), (0 : ℝ)⟩`. -/209instance : has_one ℂ := ⟨⟨1, 0⟩⟩210211-- name basic properties and tag them appropriately212@[simp] lemma one_re : (1 : ℂ).re = 1 := rfl213@[simp] lemma one_im : (1 : ℂ).im = 0 := rfl214215/-! ## + -/216217-- Now let's define addition218219/-- Notation `+` for usual addition of complex numbers-/220instance : has_add ℂ := ⟨λ z w, ⟨z.re + w.re, z.im + w.im⟩⟩221222-- and state and tag its basic properties. We want to prove223-- theorems like $$a(b+c)=ab+ac$$ by checking on real and224-- imaginary parts, so we need to teach the simplifier225-- these tricks.226227@[simp] lemma add_re (z w : ℂ) : (z + w).re = z.re + w.re := rfl228@[simp] lemma add_im (z w : ℂ) : (z + w).im = z.im + w.im := rfl229230231232instance : has_neg ℂ := ⟨λ z, ⟨-z.re, -z.im⟩⟩233234@[simp] lemma neg_re (z : ℂ) : (-z).re = -z.re := rfl235@[simp] lemma neg_im (z : ℂ) : (-z).im = -z.im := rfl236237instance : has_mul ℂ := ⟨λ z w, ⟨z.re * w.re - z.im * w.im, z.re * w.im + z.im * w.re⟩⟩238239@[simp] lemma mul_re (z w : ℂ) : (z * w).re = z.re * w.re - z.im * w.im := rfl240@[simp] lemma mul_im (z w : ℂ) : (z * w).im = z.re * w.im + z.im * w.re := rfl241242/-! ## Example of what `simp` can now do -/243244example (a b c : ℂ) : re(a*(b+c)) = re(a) * (re(b) + re(c)) - im(a) * (im(b) + im(c)) :=245begin246simp,247end248249250/-! # Theorem: The complex numbers are a commutative ring -/251252-- Proof: we've defined all the structure, and every axiom can be checked by reducing it253-- to checking real and imaginary parts with `ext`, expanding everything out with `simp`254-- and then using the fact that the real numbers are a ring.255instance : comm_ring ℂ :=256by refine { zero := 0, add := (+), neg := has_neg.neg, one := 1, mul := (*), ..};257{ intros, apply ext_iff.2; split; simp; ring }258259-- That is the end of the proof that the complexes form a ring. We built260-- a basic API which was honed towards the general idea that to prove261-- certain statements about the complex numbers, for example distributivity,262-- we could just check on real and imaginary parts. We trained the `simp`263-- lemma to simplify every264265266/-! # Coercion267268This is a worked example of how coercions work from the reals to the complexes.269It's convenient to do this early, and very straightforward.270I have left in the term mode proofs, with explanations.271272-/273274-- Let's define a "canonical" map from ℝ to ℂ. Instead of making it a definition, we will275-- make it a coercion instance, which means that if `(r : ℝ)` is a real276-- number, then `(r : ℂ)` or `(↑r : ℂ)` will indicate the corresponding277-- complex number with no imaginary part278279/-- The coercion from ℝ to ℂ sending `r` to the complex number `⟨r, 0⟩` -/280instance : has_coe ℝ ℂ := ⟨λ r, ⟨r, 0⟩⟩281282-- The concept of the complex number associated283-- to a real number `r` is a new definition, so we had better formulate its basic284-- properties immediately, namely what its real and imaginary parts are,285-- and their basic behaviour. Here are two properties, both true by definition.286-- We name them because we want to tag them.287@[simp] lemma of_real_re (r : ℝ) : (r : ℂ).re = r := rfl288@[simp] lemma of_real_im (r : ℝ) : (r : ℂ).im = 0 := rfl289290-- The `simp` tactic will now simplify `re(↑r)` to `r` and `im(↑r)` to `0`.291-- The `norm_cast` tactic might help you if you have proved a general292-- equality about complex numbers but you want it to be about real numbers,293-- or vice-versa.294295-- The map from the reals to the complexes is injective, something we296-- write in iff form so `simp` can use it; `simp` also works on `iff` goals.297@[simp] theorem of_real_inj {z w : ℝ} : (z : ℂ) = w ↔ z = w :=298⟨congr_arg re, congr_arg _⟩299300-- We now go through all our basic constants, namely 0, 1, + and *,301-- and tell the simplifier how they behave with respect to this new function.302303/-! ## 0 -/304@[simp] lemma of_real_zero : ((0 : ℝ) : ℂ) = 0 := rfl305306@[simp] theorem of_real_eq_zero {z : ℝ} : (z : ℂ) = 0 ↔ z = 0 := of_real_inj307theorem of_real_ne_zero {z : ℝ} : (z : ℂ) ≠ 0 ↔ z ≠ 0 := not_congr of_real_eq_zero308309/-! ## 1 -/310@[simp] lemma of_real_one : ((1 : ℝ) : ℂ) = 1 := rfl311312/-! ## + -/313314-- TODO: some crazy bug? in Lean is sometimes stopping me from315-- uncommenting the following example and then putting316-- some code after it. Probably the commit before this one.317318-- It is a theorem that the canonical map from ℝ to ℂ commutes with addition.319-- We should prove this and tag it appropriately.320321example (r s : ℝ) : ((r + s : ℝ) : ℂ) = r + s :=322begin323-- goal: to prove two complex numbers are equal.324ext,325-- goal: to prove that their real and imaginary326-- parts are equal.327{ -- real part328simp},329{ -- imaginary part330simp},331end332333-- Here's the term mode version. It's not true by definition, but `ext` and `simp` solve it.334@[simp] lemma of_real_add (r s : ℝ) : ((r + s : ℝ) : ℂ) = r + s := ext_iff.2 $ by simp335336/-! ## - -/337@[simp] lemma of_real_neg (r : ℝ) : ((-r : ℝ) : ℂ) = -r := ext_iff.2 $ by simp338339/-! ## * -/340341@[simp] lemma of_real_mul (r s : ℝ) : ((r * s : ℝ) : ℂ) = r * s := ext_iff.2 $ by simp342343/-! ## Example `simp` usage -/344345-- examples of the power of `simp` now. Change to -- `by squeeze_simp` to see which346-- lemmas `simp` uses347lemma smul_re (r : ℝ) (z : ℂ) : (↑r * z).re = r * z.re := by simp -- or by squeeze_simp348lemma smul_im (r : ℝ) (z : ℂ) : (↑r * z).im = r * z.im := by simp -- or by squeeze_simp349350/-! ## Appendix: numerals.351352If you're not a computer scientist feel free to skip 15 lines down to `I`.353354These last two are to do with the canonical map from numerals into the complexes, e.g. `(23 : ℂ)`.355Lean stores the numeral in binary. See for example356357set_option pp.numerals false358#check (37 : ℂ)-- bit1 (bit0 (bit1 (bit0 (bit0 has_one.one)))) : ℂ359-/360361@[simp] lemma of_real_bit0 (r : ℝ) : ((bit0 r : ℝ) : ℂ) = bit0 r := ext_iff.2 $ by simp [bit0]362@[simp] lemma of_real_bit1 (r : ℝ) : ((bit1 r : ℝ) : ℂ) = bit1 r := ext_iff.2 $ by simp [bit1]363364/-!365366# Exercise 1: I367368I find it unbelievable that we have written 350+ lines of code about the complex numbers369and we've still never defined i, or j, or I, or $$\sqrt{-1}$$, or whatever it's called.370I will supply the definition, Why don't you try making its basic API?371372All the proofs below are sorried. You can try them in tactic mode373by replacing `sorry` with `begin end` and then starting to write374tactics in the `begin end` block.375-/376377/-- complex.I is the square root of -1 above the imaginary axis -/378def I : ℂ := ⟨0, 1⟩379380@[simp] lemma I_re : I.re = 0 := sorry381@[simp] lemma I_im : I.im = 1 := sorry382383@[simp] lemma I_mul_I : I * I = -1 := sorry384385lemma mk_eq_add_mul_I (a b : ℝ) : complex.mk a b = a + b * I := sorry386387@[simp] lemma re_add_im (z : ℂ) : (z.re : ℂ) + z.im * I = z := sorry388389-- boss level390lemma I_ne_zero : (I : ℂ) ≠ 0 := sorry391392/-!393394# Exercise 2: Complex conjugation395396Again I'll give you the definition, you supply the proofs.397398-/399400401def conj (z : ℂ) : ℂ := ⟨z.re, -z.im⟩402403@[simp] lemma conj_re (z : ℂ) : (conj z).re = z.re := sorry404@[simp] lemma conj_im (z : ℂ) : (conj z).im = -z.im := sorry405406@[simp] lemma conj_of_real (r : ℝ) : conj r = r := sorry407408@[simp] lemma conj_zero : conj 0 = 0 := sorry409@[simp] lemma conj_one : conj 1 = 1 := sorry410@[simp] lemma conj_I : conj I = -I := sorry411412@[simp] lemma conj_add (z w : ℂ) : conj (z + w) = conj z + conj w :=413sorry414415@[simp] lemma conj_neg (z : ℂ) : conj (-z) = -conj z := sorry416417@[simp] lemma conj_neg_I : conj (-I) = I := sorry418419@[simp] lemma conj_mul (z w : ℂ) : conj (z * w) = conj z * conj w :=420sorry421422@[simp] lemma conj_conj (z : ℂ) : conj (conj z) = z :=423sorry424425lemma conj_involutive : function.involutive conj := sorry426427lemma conj_bijective : function.bijective conj := sorry428429lemma conj_inj {z w : ℂ} : conj z = conj w ↔ z = w :=430sorry431432@[simp] lemma conj_eq_zero {z : ℂ} : conj z = 0 ↔ z = 0 :=433sorry434435lemma eq_conj_iff_real {z : ℂ} : conj z = z ↔ ∃ r : ℝ, z = r :=436sorry437438lemma eq_conj_iff_re {z : ℂ} : conj z = z ↔ (z.re : ℂ) = z :=439sorry440441theorem add_conj (z : ℂ) : z + conj z = (2 * z.re : ℝ) :=442sorry443444/-- the ring homomorphism complex conjugation -/445def Conj : ℂ →+* ℂ :=446{ to_fun := conj,447map_one' := sorry,448map_mul' := sorry,449map_zero' := sorry,450map_add' := sorry}451452/-!453454# Exercise 3: Norms455456-/457458def norm_sq (z : ℂ) : ℝ := z.re * z.re + z.im * z.im459460@[simp] lemma norm_sq_of_real (r : ℝ) : norm_sq r = r * r :=461sorry462463@[simp] lemma norm_sq_zero : norm_sq 0 = 0 := sorry464@[simp] lemma norm_sq_one : norm_sq 1 = 1 := sorry465@[simp] lemma norm_sq_I : norm_sq I = 1 := sorry466467lemma norm_sq_nonneg (z : ℂ) : 0 ≤ norm_sq z := sorry468469@[simp] lemma norm_sq_eq_zero {z : ℂ} : norm_sq z = 0 ↔ z = 0 :=470sorry471472@[simp] lemma norm_sq_pos {z : ℂ} : 0 < norm_sq z ↔ z ≠ 0 :=473sorry474475@[simp] lemma norm_sq_neg (z : ℂ) : norm_sq (-z) = norm_sq z :=476sorry477478@[simp] lemma norm_sq_conj (z : ℂ) : norm_sq (conj z) = norm_sq z :=479sorry480481@[simp] lemma norm_sq_mul (z w : ℂ) : norm_sq (z * w) = norm_sq z * norm_sq w :=482sorry483484lemma norm_sq_add (z w : ℂ) : norm_sq (z + w) =485norm_sq z + norm_sq w + 2 * (z * conj w).re :=486sorry487488lemma re_sq_le_norm_sq (z : ℂ) : z.re * z.re ≤ norm_sq z :=489sorry490491lemma im_sq_le_norm_sq (z : ℂ) : z.im * z.im ≤ norm_sq z :=492sorry493494theorem mul_conj (z : ℂ) : z * conj z = norm_sq z :=495sorry496497end complex498499/-! # Exercise 4 (advanced)5005011) Prove the complex numbers are a field.5025032) Prove the complex numbers are an algebraically closed field.504505506-/507508instance : field ℂ := sorry509510-- As for it being algebraically closed, [here](https://github.com/leanprover-community/mathlib/blob/3710744/src/analysis/complex/polynomial.lean#L34)511-- is where it is proved in mathlib. The mathlib proof was written by Chris Hughes, a mathematics512-- undergraduate at Imperial College London.513514