Author: Kevin Buzzard
Views : 131
Description: A simple complex number game. You need to have played the natural number game https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/ first.
Compute Environment: Ubuntu 18.04 (Deprecated)
1/-
2The complex numbers.
3A documented remix of part of mathlib
4
5Our goal is to define the complex numbers, and then "extract some API".
6Our first goal is to define addition and multiplication,
7and prove that the complex numbers are a commutative ring.
8We then do a slightly more computer-sciency worked development of the
9natural inclusion from the reals to the complexes.
10
11There are then a bunch of API-building exercises, which can be solved in term mode
12or tactic mode. The first is I, the second is complex conjugation,
13and the third is the "squared norm" function.
14
15There is then a speculative last exercise on harder properties
16of the complexes.
17-/
18
19-- We will assume that the real numbers are a field.
20import data.real.basic
21
22/-- A complex number is defined to be a structure consisting of two real numbers,
23    the real part and the imaginary part of the complex number   . -/
24structure complex : Type :=
25(re : ℝ) (im : ℝ)
26
27-- Let's use the usual notation for the complex numbers
28notation ℂ := complex
29
30-- You make the complex number with real part 3 and imaginary part 4 like this:
31example : ℂ :=
32{ re := 3,
33  im := 4 }
34
35-- Or like this:
36example : ℂ := complex.mk 3 4
37
38-- or like this:
39example : ℂ := ⟨3, 4⟩
40
41-- They all give the same complex number.
42
43-- If you have a complex number, then you can get its real and
44-- imaginary parts with the complex.re and complex.im functions.
45
46example : ℝ := complex.re(complex.mk 3 4) -- this term is (3 : ℝ)
47
48example : complex.re(complex.mk 3 4) = 3 := rfl -- true by definition.
49
50-- We clearly don't want to be constantly saying complex.blah so let's
51-- move into the complex namespace
52
53namespace complex
54
55-- All our theorems and definitions will now be called complex.something,
56-- and we can in general just drop complex.
57
58-- For example
59
60example : re(mk 3 4) = 3 := rfl
61
62-- Computer scientists prefer the style z.re to re(z) for some reason.
63
64example : (mk 3 4).re = 3 := rfl
65
66example (z : ℂ) : re(z) = z.re := rfl
67
68-- We now prove the basic theorems and make the basic definitions for
69-- complex numbers. For example, we will define addition and multiplication on
70-- the complex numbers, and prove that it is a commutative ring.
71
72/-! # Mathematical trivialities -/
73
74-- We start with some facts about complex numbers which are so obvious that we do not
75-- often explicitly state them. The first is that if z is a complex number, then
76-- the complex number with real part re(z) and imaginary part im(z) is equal to z.
77-- This is called eta reduction in type theory. Let's work through the
78-- simple tactic mode proof.
79
80example : ∀ z : ℂ, complex.mk z.re z.im = z :=
81begin
82  intro z,
83  cases z with x y,
84  -- goal now looks complicated, and contains terms which look
85  -- like {re := a, im := b}.re which obviously simplify to a.
86  -- The dsimp tactic will do some tidying up for us, although
87  -- it is not logically necessary. dsimp does definitional simplification.
88  dsimp,
89  -- Now we see the goal can be solved by reflexivity
90  refl,
91end
92
93-- The proof was "unfold everything, and it's true by definition".
94-- This proof does not teach a mathematician anything, so we may as well write
95-- it in term mode, because each tactic has a term equivalent.
96-- The equation compiler does the intro and cases steps,
97-- and dsimp was unnecessary -- the two sides of the equation
98-- were definitionally equal.
99
100-- It's important we give this theorem a name, because we want simp
101-- to be able to use it. In short, the simp tactic tries to solve
102-- goals of the form A = B, when refl doesn't work (i.e. the goals are
103-- not definitionally equal) but when any mathematician would be able
104-- to simplify A and B via "obvious" steps such as 0 + x = x or
105-- ⟨z.re, z.im⟩ = z. These things are sometimes not true by definition,
106-- but they should be tagged as being well-known ways to simplify an equality.
107-- When building our API for the complex numbers, if we prove a theorem of the
108-- form A = B where B is a bit simpler than A, we should probably
109-- tag it with the @[simp] attribute, so simp can use it.
110
111-- Note: simp does *not* prove "all simple things". It proves *equalities*.
112-- It proves A = B when, and only when, it can do it by applying
113-- its "simplification rules", where a simplification rule is simply a proof
114-- of a theorem of the form A = B and B is simpler than A.
115@[simp] theorem eta : ∀ z : ℂ, complex.mk z.re z.im = z
116| ⟨x, y⟩ := rfl
117
118-- The second triviality is the assertion that two complex numbers
119-- with the same and imaginary parts are equal. Again this is not
120-- hard to prove, and mathematicians deem it not worth documenting.
121
122example (z w : ℂ) : z.re = w.re → z.im = w.im → z = w :=
123begin
124  cases z with zr zi,
125  cases w,
126  intros, cc,
127end
128
129-- This lemma is called extensionality by type theorists.
130-- Here is another tactic mode proof. Note that we have moved
131-- the z and w to the other side of the colon; this does not
132-- change the fully expanded proof term. It shows the power
133-- of the rintros tactic.
134
135example : ∀ z w : ℂ, z.re = w.re → z.im = w.im → z = w :=
136begin
137  rintros ⟨zr, zi⟩ ⟨_, _⟩ ⟨rfl⟩ ⟨rfl⟩,
138  refl,
139end
140
141-- rintros does cases as many times as you like using this cool ⟨, ⟩ syntax
142-- for the case splits. Note that if you do cases on h : a = b then, because
143-- = is notation for eq, an inductive type with one constructor a = a,
144-- it will just delete b and change all bs to as. That is one of the
145-- things going on in the above proof.
146
147-- Here is the same proof in term mode. Even though it's obvious, we still
148-- give it a name, namely ext. It's important to prove it, so we can
149-- tag it with the ext attribute. If we do this, the ext tactic can use it.
150-- The ext tactic applies all theorems of the form "two
151-- objects are the same if they are made from the same pieces".
152
153@[ext]
154theorem ext : ∀ {z w : ℂ}, z.re = w.re → z.im = w.im → z = w
155| ⟨zr, zi⟩ ⟨_, _⟩ rfl rfl := rfl
156
157-- The theorem complex.ext is trivially true to a mathematician.
158-- But it is often used: for example it will be used all the time
159-- in our proof that the complex numbers are a ring.
160
161-- Note that ext is an implication -- if re(z)=re(w) and im(z)=im(w) then z=w.
162-- The below variant ext_iff is the two-way implication: two complex
163-- numbers are equal if and only if they have the same real and imaginary part.
164-- Let's first see a tactic mode proof. See how the ext tactic is used?
165-- After it is applied, we have two goals, both of which are hypotheses.
166-- The semicolon means "apply the next tactic to all the goals produced by this one"
167
168example (z w : ℂ) : z = w ↔ z.re = w.re ∧ z.im = w.im :=
169begin
170  split,
171  { intro H,
172    simp [H]},
173  {
174    rintro ⟨hre, him⟩,
175    ext; assumption,
176  }
177end
178
179-- Again this is easy to write in term mode, and no mathematician
180-- wants to read the proof anyway.
181
182theorem ext_iff {z w : ℂ} : z = w ↔ z.re = w.re ∧ z.im = w.im :=
183⟨λ H, by simp [H], and.rec ext⟩
184
185/-! # Main course: the complex numbers are a ring. -/
186
187-- Our goal is to prove that the complexes are a ring. Let's
188-- define the structure first; the zero, one, addition and multiplication
189-- on the complexes.
190
191/-! ## 0 -/
192
193-- Let's define the zero complex number. Once we have done this we will be
194-- able to talk about (0 : ℂ).
195
196/-- notation: 0, or (0 : ℂ), will mean the complex number with
197  real and imaginary part equal to (0 : ℝ). -/
198instance : has_zero ℂ := ⟨⟨0, 0⟩⟩
199
200-- Let's prove its basic properties, all of which are true by definition,
201-- and then tag them with the appropriate attributes.
202@[simp] lemma zero_re : (0 : ℂ).re = 0 := rfl
203@[simp] lemma zero_im : (0 : ℂ).im = 0 := rfl
204
205/-! ## 1 -/
206
207-- Now let's do the same thing for 1.
208
209/-- Notation 1 or (1 : ℂ), means ⟨(1 : ℝ), (0 : ℝ)⟩. -/
210instance : has_one ℂ := ⟨⟨1, 0⟩⟩
211
212-- name basic properties and tag them appropriately
213@[simp] lemma one_re : (1 : ℂ).re = 1 := rfl
214@[simp] lemma one_im : (1 : ℂ).im = 0 := rfl
215
216/-! ## + -/
217
219
220/-- Notation + for usual addition of complex numbers-/
221instance : has_add ℂ := ⟨λ z w, ⟨z.re + w.re, z.im + w.im⟩⟩
222
223-- and state and tag its basic properties. We want to prove
224-- theorems like $$a(b+c)=ab+ac$$ by checking on real and
225-- imaginary parts, so we need to teach the simplifier
226-- these tricks.
227
228@[simp] lemma add_re (z w : ℂ) : (z + w).re = z.re + w.re := rfl
229@[simp] lemma add_im (z w : ℂ) : (z + w).im = z.im + w.im := rfl
230
231
232
233instance : has_neg ℂ := ⟨λ z, ⟨-z.re, -z.im⟩⟩
234
235@[simp] lemma neg_re (z : ℂ) : (-z).re = -z.re := rfl
236@[simp] lemma neg_im (z : ℂ) : (-z).im = -z.im := rfl
237
238instance : has_mul ℂ := ⟨λ z w, ⟨z.re * w.re - z.im * w.im, z.re * w.im + z.im * w.re⟩⟩
239
240@[simp] lemma mul_re (z w : ℂ) : (z * w).re = z.re * w.re - z.im * w.im := rfl
241@[simp] lemma mul_im (z w : ℂ) : (z * w).im = z.re * w.im + z.im * w.re := rfl
242
243/-! ## Example of what simp can now do -/
244
245example (a b c : ℂ) : re(a*(b+c)) = re(a) * (re(b) + re(c)) - im(a) * (im(b) + im(c)) :=
246begin
247  simp,
248end
249
250
251/-! # Theorem:  The complex numbers are a commutative ring -/
252
253-- Proof: we've defined all the structure, and every axiom can be checked by reducing it
254-- to checking real and imaginary parts with ext, expanding everything out with simp
255-- and then using the fact that the real numbers are a ring.
256instance : comm_ring ℂ :=
257by refine { zero := 0, add := (+), neg := has_neg.neg, one := 1, mul := (*), ..};
258   { intros, apply ext_iff.2; split; simp; ring }
259
260-- That is the end of the proof that the complexes form a ring. We built
261-- a basic API which was honed towards the general idea that to prove
262-- certain statements about the complex numbers, for example distributivity,
263-- we could just check on real and imaginary parts. We trained the simp
264-- lemma to simplify every
265
266
267/-! # Coercion
268
269This is a worked example of how coercions work from the reals to the complexes.
270It's convenient to do this early, and very straightforward.
271 I have left in the term mode proofs, with explanations.
272
273-/
274
275-- Let's define a "canonical" map from ℝ to ℂ. Instead of making it a definition, we will
276-- make it a coercion instance, which means that if (r : ℝ) is a real
277-- number, then (r : ℂ) or (↑r : ℂ) will indicate the corresponding
278-- complex number with no imaginary part
279
280/-- The coercion from ℝ to ℂ sending r to the complex number ⟨r, 0⟩ -/
281instance : has_coe ℝ ℂ := ⟨λ r, ⟨r, 0⟩⟩
282
283-- The concept of the complex number associated
284-- to a real number r is a new definition, so we had better formulate its basic
285-- properties immediately, namely what its real and imaginary parts are,
286-- and their basic behaviour. Here are two properties, both true by definition.
287-- We name them because we want to tag them.
288@[simp] lemma of_real_re (r : ℝ) : (r : ℂ).re = r := rfl
289@[simp] lemma of_real_im (r : ℝ) : (r : ℂ).im = 0 := rfl
290
291-- The simp tactic will now simplify re(↑r) to r and im(↑r) to 0.
292-- The norm_cast tactic might help you if you have proved a general
293-- equality about complex numbers but you want it to be about real numbers,
294-- or vice-versa.
295
296-- The map from the reals to the complexes is injective, something we
297-- write in iff form so simp can use it; simp also works on iff goals.
298@[simp] theorem of_real_inj {z w : ℝ} : (z : ℂ) = w ↔ z = w :=
299⟨congr_arg re, congr_arg _⟩
300
301-- We now go through all our basic constants, namely 0, 1, + and *,
302-- and tell the simplifier how they behave with respect to this new function.
303
304/-! ## 0 -/
305@[simp] lemma of_real_zero : ((0 : ℝ) : ℂ) = 0 := rfl
306
307@[simp] theorem of_real_eq_zero {z : ℝ} : (z : ℂ) = 0 ↔ z = 0 := of_real_inj
308theorem of_real_ne_zero {z : ℝ} : (z : ℂ) ≠ 0 ↔ z ≠ 0 := not_congr of_real_eq_zero
309
310/-! ## 1 -/
311@[simp] lemma of_real_one : ((1 : ℝ) : ℂ) = 1 := rfl
312
313/-! ## + -/
314
315-- TODO: some crazy bug? in Lean is sometimes stopping me from
316-- uncommenting the following example and then putting
317-- some code after it. Probably the commit before this one.
318
319-- It is a theorem that the canonical map from ℝ to ℂ commutes with addition.
320-- We should prove this and tag it appropriately.
321
322example (r s : ℝ) : ((r + s : ℝ) : ℂ) = r + s :=
323begin
324  -- goal: to prove two complex numbers are equal.
325  ext,
326  -- goal: to prove that their real and imaginary
327  -- parts are equal.
328  { -- real part
329    simp},
330  { -- imaginary part
331    simp},
332end
333
334-- Here's the term mode version. It's not true by definition, but ext and simp solve it.
335@[simp] lemma of_real_add (r s : ℝ) : ((r + s : ℝ) : ℂ) = r + s := ext_iff.2 $by simp 336 337/-! ## - -/ 338@[simp] lemma of_real_neg (r : ℝ) : ((-r : ℝ) : ℂ) = -r := ext_iff.2$ by simp
339
340/-! ## * -/
341
342@[simp] lemma of_real_mul (r s : ℝ) : ((r * s : ℝ) : ℂ) = r * s := ext_iff.2 $by simp 343 344/-! ## Example simp usage -/ 345 346-- examples of the power of simp now. Change to -- by squeeze_simp to see which 347-- lemmas simp uses 348lemma smul_re (r : ℝ) (z : ℂ) : (↑r * z).re = r * z.re := by simp -- or by squeeze_simp 349lemma smul_im (r : ℝ) (z : ℂ) : (↑r * z).im = r * z.im := by simp -- or by squeeze_simp 350 351/-! ## Appendix: numerals. 352 353If you're not a computer scientist feel free to skip 15 lines down to I. 354 355These last two are to do with the canonical map from numerals into the complexes, e.g. (23 : ℂ). 356Lean stores the numeral in binary. See for example 357 358set_option pp.numerals false 359#check (37 : ℂ)-- bit1 (bit0 (bit1 (bit0 (bit0 has_one.one)))) : ℂ 360-/ 361 362@[simp] lemma of_real_bit0 (r : ℝ) : ((bit0 r : ℝ) : ℂ) = bit0 r := ext_iff.2$ by simp [bit0]
363@[simp] lemma of_real_bit1 (r : ℝ) : ((bit1 r : ℝ) : ℂ) = bit1 r := ext_iff.2 \$ by simp [bit1]
364
365/-!
366
367# Exercise 1: I
368
369I find it unbelievable that we have written 350+ lines of code about the complex numbers
370and we've still never defined i, or j, or I, or $$\sqrt{-1}$$, or whatever it's called.
371I will supply the definition, Why don't you try making its basic API?
372
373All the proofs below are sorried. You can try them in tactic mode
374by replacing sorry with begin end and then starting to write
375tactics in the begin end block.
376-/
377
378/-- complex.I is the square root of -1 above the imaginary axis -/
379def I : ℂ := ⟨0, 1⟩
380
381@[simp] lemma I_re : I.re = 0 := sorry
382@[simp] lemma I_im : I.im = 1 := sorry
383
384@[simp] lemma I_mul_I : I * I = -1 := sorry
385
386lemma mk_eq_add_mul_I (a b : ℝ) : complex.mk a b = a + b * I := sorry
387
388@[simp] lemma re_add_im (z : ℂ) : (z.re : ℂ) + z.im * I = z := sorry
389
390-- boss level
391lemma I_ne_zero : (I : ℂ) ≠ 0 := sorry
392
393/-!
394
395# Exercise 2: Complex conjugation
396
397Again I'll give you the definition, you supply the proofs.
398
399-/
400
401
402def conj (z : ℂ) : ℂ := ⟨z.re, -z.im⟩
403
404@[simp] lemma conj_re (z : ℂ) : (conj z).re = z.re := sorry
405@[simp] lemma conj_im (z : ℂ) : (conj z).im = -z.im := sorry
406
407@[simp] lemma conj_of_real (r : ℝ) : conj r = r := sorry
408
409@[simp] lemma conj_zero : conj 0 = 0 := sorry
410@[simp] lemma conj_one : conj 1 = 1 := sorry
411@[simp] lemma conj_I : conj I = -I := sorry
412
413@[simp] lemma conj_add (z w : ℂ) : conj (z + w) = conj z + conj w :=
414sorry
415
416@[simp] lemma conj_neg (z : ℂ) : conj (-z) = -conj z := sorry
417
418@[simp] lemma conj_neg_I : conj (-I) = I := sorry
419
420@[simp] lemma conj_mul (z w : ℂ) : conj (z * w) = conj z * conj w :=
421sorry
422
423@[simp] lemma conj_conj (z : ℂ) : conj (conj z) = z :=
424sorry
425
426lemma conj_involutive : function.involutive conj := sorry
427
428lemma conj_bijective : function.bijective conj := sorry
429
430lemma conj_inj {z w : ℂ} : conj z = conj w ↔ z = w :=
431sorry
432
433@[simp] lemma conj_eq_zero {z : ℂ} : conj z = 0 ↔ z = 0 :=
434sorry
435
436lemma eq_conj_iff_real {z : ℂ} : conj z = z ↔ ∃ r : ℝ, z = r :=
437sorry
438
439lemma eq_conj_iff_re {z : ℂ} : conj z = z ↔ (z.re : ℂ) = z :=
440sorry
441
442theorem add_conj (z : ℂ) : z + conj z = (2 * z.re : ℝ) :=
443sorry
444
445/-- the ring homomorphism complex conjugation -/
446def Conj : ℂ →+* ℂ :=
447{ to_fun := conj,
448  map_one' := sorry,
449  map_mul' := sorry,
450  map_zero' := sorry,
452
453/-!
454
455# Exercise 3: Norms
456
457-/
458
459def norm_sq (z : ℂ) : ℝ := z.re * z.re + z.im * z.im
460
461@[simp] lemma norm_sq_of_real (r : ℝ) : norm_sq r = r * r :=
462sorry
463
464@[simp] lemma norm_sq_zero : norm_sq 0 = 0 := sorry
465@[simp] lemma norm_sq_one : norm_sq 1 = 1 := sorry
466@[simp] lemma norm_sq_I : norm_sq I = 1 := sorry
467
468lemma norm_sq_nonneg (z : ℂ) : 0 ≤ norm_sq z := sorry
469
470@[simp] lemma norm_sq_eq_zero {z : ℂ} : norm_sq z = 0 ↔ z = 0 :=
471sorry
472
473@[simp] lemma norm_sq_pos {z : ℂ} : 0 < norm_sq z ↔ z ≠ 0 :=
474sorry
475
476@[simp] lemma norm_sq_neg (z : ℂ) : norm_sq (-z) = norm_sq z :=
477sorry
478
479@[simp] lemma norm_sq_conj (z : ℂ) : norm_sq (conj z) = norm_sq z :=
480sorry
481
482@[simp] lemma norm_sq_mul (z w : ℂ) : norm_sq (z * w) = norm_sq z * norm_sq w :=
483sorry
484
485lemma norm_sq_add (z w : ℂ) : norm_sq (z + w) =
486  norm_sq z + norm_sq w + 2 * (z * conj w).re :=
487sorry
488
489lemma re_sq_le_norm_sq (z : ℂ) : z.re * z.re ≤ norm_sq z :=
490sorry
491
492lemma im_sq_le_norm_sq (z : ℂ) : z.im * z.im ≤ norm_sq z :=
493sorry
494
495theorem mul_conj (z : ℂ) : z * conj z = norm_sq z :=
496sorry
497
498end complex
499
501
5021) Prove the complex numbers are a field.
503
5042) Prove the complex numbers are an algebraically closed field.
505
506
507-/
508
509instance : field ℂ := sorry
510
511-- As for it being algebraically closed, [here](https://github.com/leanprover-community/mathlib/blob/3710744/src/analysis/complex/polynomial.lean#L34)
512-- is where it is proved in mathlib. The mathlib proof was written by Chris Hughes, a mathematics
513-- undergraduate at Imperial College London.
514