CoCalc Public Filescomplex.leanOpen with one click!
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
/-
2
The complex numbers.
3
A documented remix of part of mathlib
4
5
Our goal is to define the complex numbers, and then "extract some API".
6
Our first goal is to define addition and multiplication,
7
and prove that the complex numbers are a commutative ring.
8
We then do a slightly more computer-sciency worked development of the
9
natural inclusion from the reals to the complexes.
10
11
There are then a bunch of API-building exercises, which can be solved in term mode
12
or tactic mode. The first is `I`, the second is complex conjugation,
13
and the third is the "squared norm" function.
14
15
There is then a speculative last exercise on harder properties
16
of the complexes.
17
-/
18
19
-- We will assume that the real numbers are a field.
20
import 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 . -/
24
structure complex : Type :=
25
(re : ) (im : )
26
27
-- Let's use the usual notation for the complex numbers
28
notation `` := complex
29
30
-- You make the complex number with real part 3 and imaginary part 4 like this:
31
example : :=
32
{ re := 3,
33
im := 4 }
34
35
-- Or like this:
36
example : := complex.mk 3 4
37
38
-- or like this:
39
example : := 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
46
example : := complex.re(complex.mk 3 4) -- this term is (3 : ℝ)
47
48
example : 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
53
namespace 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
60
example : re(mk 3 4) = 3 := rfl
61
62
-- Computer scientists prefer the style `z.re` to `re(z)` for some reason.
63
64
example : (mk 3 4).re = 3 := rfl
65
66
example (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
80
example : z : , complex.mk z.re z.im = z :=
81
begin
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,
91
end
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
122
example (z w : ) : z.re = w.re z.im = w.im z = w :=
123
begin
124
cases z with zr zi,
125
cases w,
126
intros, cc,
127
end
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
135
example : z w : , z.re = w.re z.im = w.im z = w :=
136
begin
137
rintros zr, zi _, _ rfl rfl,
138
refl,
139
end
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 `b`s to `a`s. 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]
154
theorem 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
168
example (z w : ) : z = w z.re = w.re z.im = w.im :=
169
begin
170
split,
171
{ intro H,
172
simp [H]},
173
{
174
rintro hre, him,
175
ext; assumption,
176
}
177
end
178
179
-- Again this is easy to write in term mode, and no mathematician
180
-- wants to read the proof anyway.
181
182
theorem 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 : ℝ). -/
198
instance : 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 : ℝ)⟩`. -/
210
instance : 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
218
-- Now let's define addition
219
220
/-- Notation `+` for usual addition of complex numbers-/
221
instance : 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
233
instance : 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
238
instance : 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
245
example (a b c : ) : re(a*(b+c)) = re(a) * (re(b) + re(c)) - im(a) * (im(b) + im(c)) :=
246
begin
247
simp,
248
end
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.
256
instance : comm_ring :=
257
by 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
269
This is a worked example of how coercions work from the reals to the complexes.
270
It'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⟩` -/
281
instance : 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
308
theorem 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
322
example (r s : ) : ((r + s : ) : ) = r + s :=
323
begin
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},
332
end
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
348
lemma smul_re (r : ) (z : ) : (r * z).re = r * z.re := by simp -- or by squeeze_simp
349
lemma smul_im (r : ) (z : ) : (r * z).im = r * z.im := by simp -- or by squeeze_simp
350
351
/-! ## Appendix: numerals.
352
353
If you're not a computer scientist feel free to skip 15 lines down to `I`.
354
355
These last two are to do with the canonical map from numerals into the complexes, e.g. `(23 : ℂ)`.
356
Lean stores the numeral in binary. See for example
357
358
set_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
369
I find it unbelievable that we have written 350+ lines of code about the complex numbers
370
and we've still never defined i, or j, or I, or $$\sqrt{-1}$$, or whatever it's called.
371
I will supply the definition, Why don't you try making its basic API?
372
373
All the proofs below are sorried. You can try them in tactic mode
374
by replacing `sorry` with `begin end` and then starting to write
375
tactics in the `begin end` block.
376
-/
377
378
/-- complex.I is the square root of -1 above the imaginary axis -/
379
def 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
386
lemma 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
391
lemma I_ne_zero : (I : ) 0 := sorry
392
393
/-!
394
395
# Exercise 2: Complex conjugation
396
397
Again I'll give you the definition, you supply the proofs.
398
399
-/
400
401
402
def 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 :=
414
sorry
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 :=
421
sorry
422
423
@[simp] lemma conj_conj (z : ) : conj (conj z) = z :=
424
sorry
425
426
lemma conj_involutive : function.involutive conj := sorry
427
428
lemma conj_bijective : function.bijective conj := sorry
429
430
lemma conj_inj {z w : } : conj z = conj w z = w :=
431
sorry
432
433
@[simp] lemma conj_eq_zero {z : } : conj z = 0 z = 0 :=
434
sorry
435
436
lemma eq_conj_iff_real {z : } : conj z = z r : , z = r :=
437
sorry
438
439
lemma eq_conj_iff_re {z : } : conj z = z (z.re : ) = z :=
440
sorry
441
442
theorem add_conj (z : ) : z + conj z = (2 * z.re : ) :=
443
sorry
444
445
/-- the ring homomorphism complex conjugation -/
446
def Conj : +* :=
447
{ to_fun := conj,
448
map_one' := sorry,
449
map_mul' := sorry,
450
map_zero' := sorry,
451
map_add' := sorry}
452
453
/-!
454
455
# Exercise 3: Norms
456
457
-/
458
459
def 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 :=
462
sorry
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
468
lemma norm_sq_nonneg (z : ) : 0 norm_sq z := sorry
469
470
@[simp] lemma norm_sq_eq_zero {z : } : norm_sq z = 0 z = 0 :=
471
sorry
472
473
@[simp] lemma norm_sq_pos {z : } : 0 < norm_sq z z 0 :=
474
sorry
475
476
@[simp] lemma norm_sq_neg (z : ) : norm_sq (-z) = norm_sq z :=
477
sorry
478
479
@[simp] lemma norm_sq_conj (z : ) : norm_sq (conj z) = norm_sq z :=
480
sorry
481
482
@[simp] lemma norm_sq_mul (z w : ) : norm_sq (z * w) = norm_sq z * norm_sq w :=
483
sorry
484
485
lemma norm_sq_add (z w : ) : norm_sq (z + w) =
486
norm_sq z + norm_sq w + 2 * (z * conj w).re :=
487
sorry
488
489
lemma re_sq_le_norm_sq (z : ) : z.re * z.re norm_sq z :=
490
sorry
491
492
lemma im_sq_le_norm_sq (z : ) : z.im * z.im norm_sq z :=
493
sorry
494
495
theorem mul_conj (z : ) : z * conj z = norm_sq z :=
496
sorry
497
498
end complex
499
500
/-! # Exercise 4 (advanced)
501
502
1) Prove the complex numbers are a field.
503
504
2) Prove the complex numbers are an algebraically closed field.
505
506
507
-/
508
509
instance : 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