1 (* ========================================================================= *)
2 (* Fundamental theorem of algebra. *)
3 (* ========================================================================= *)
5 needs "Complex/complex_transc.ml";;
6 needs "Complex/cpoly.ml";;
10 (* ------------------------------------------------------------------------- *)
11 (* A cute trick to reduce magnitude of unimodular number. *)
12 (* ------------------------------------------------------------------------- *)
14 let SQRT_SOS_LT_1 = prove
15 (`!x y. sqrt(x pow 2 + y pow 2) < &1 <=> x pow 2 + y pow 2 < &1`,
17 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM SQRT_1] THEN
18 REWRITE_TAC[REAL_POW_2] THEN
19 SIMP_TAC[SQRT_MONO_LT_EQ; REAL_POS; REAL_LE_ADD; REAL_LE_SQUARE]);;
21 let SQRT_SOS_EQ_1 = prove
22 (`!x y. (sqrt(x pow 2 + y pow 2) = &1) <=> (x pow 2 + y pow 2 = &1)`,
24 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM SQRT_1] THEN
25 REWRITE_TAC[REAL_POW_2] THEN
26 SIMP_TAC[SQRT_INJ; REAL_POS; REAL_LE_ADD; REAL_LE_SQUARE]);;
28 let UNIMODULAR_REDUCE_NORM = prove
30 ==> norm(z + Cx(&1)) < &1 \/
31 norm(z - Cx(&1)) < &1 \/
35 REWRITE_TAC[ii; CX_DEF; complex_add; complex_sub; complex_neg; complex_norm;
36 RE; IM; REAL_ADD_RID; REAL_NEG_0; SQRT_SOS_LT_1; SQRT_SOS_EQ_1] THEN
38 REAL_ARITH `a * a + (b + c) * (b + c) =
39 (a * a + b * b) + (&2 * b * c + c * c)`;
40 REAL_ARITH `(b + c) * (b + c) + a * a =
41 (b * b + a * a) + (&2 * b * c + c * c)`] THEN
42 DISCH_TAC THEN REWRITE_TAC[REAL_ARITH `&1 + x < &1 <=> &0 < --x`] THEN
43 REWRITE_TAC[REAL_NEG_ADD; REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_NEG_NEG] THEN
44 REWRITE_TAC[REAL_MUL_RID] THEN
45 MATCH_MP_TAC(REAL_ARITH
46 `~(abs(a) <= &1 /\ abs(b) <= &1)
47 ==> &0 < --a + --(&1) \/ &0 < a + --(&1) \/
48 &0 < --b + --(&1) \/ &0 < b + --(&1)`) THEN
49 STRIP_TAC THEN UNDISCH_TAC `Re z * Re z + Im z * Im z = &1` THEN
51 MATCH_MP_TAC(REAL_ARITH
52 `(&2 * r) * (&2 * r) <= &1 /\ (&2 * i) * (&2 * i) <= &1
53 ==> ~(r * r + i * i = &1)`) THEN
54 REWRITE_TAC[GSYM REAL_POW_2] THEN ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN
55 ASM_SIMP_TAC[REAL_POW_1_LE; REAL_ABS_POS]);;
57 (* ------------------------------------------------------------------------- *)
58 (* Hence we can always reduce modulus of 1 + b z^n if nonzero *)
59 (* ------------------------------------------------------------------------- *)
61 let REDUCE_POLY_SIMPLE = prove
62 (`!b n. ~(b = Cx(&0)) /\ ~(n = 0)
63 ==> ?z. norm(Cx(&1) + b * z pow n) < &1`,
64 GEN_TAC THEN MATCH_MP_TAC num_WF THEN REPEAT STRIP_TAC THEN
65 ASM_CASES_TAC `EVEN(n)` THENL
66 [FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [EVEN_EXISTS]) THEN
67 DISCH_THEN(X_CHOOSE_THEN `m:num` SUBST_ALL_TAC) THEN
68 FIRST_X_ASSUM(MP_TAC o SPEC `m:num`) THEN
69 ASM_SIMP_TAC[ARITH_RULE `~(2 * m = 0) ==> m < 2 * m /\ ~(m = 0)`] THEN
70 DISCH_THEN(X_CHOOSE_TAC `w:complex`) THEN EXISTS_TAC `csqrt w` THEN
71 ASM_REWRITE_TAC[GSYM COMPLEX_POW_POW; CSQRT]; ALL_TAC] THEN
72 MP_TAC(SPEC `Cx(norm b) / b` UNIMODULAR_REDUCE_NORM) THEN ANTS_TAC THENL
73 [REWRITE_TAC[COMPLEX_NORM_DIV; COMPLEX_NORM_CX] THEN
74 ASM_SIMP_TAC[COMPLEX_ABS_NORM; REAL_DIV_REFL; COMPLEX_NORM_ZERO];
75 ALL_TAC] THEN DISCH_TAC THEN
76 SUBGOAL_THEN `?v. norm(Cx(norm b) / b + v pow n) < &1` MP_TAC THENL
77 [SUBGOAL_THEN `(Cx(&1) pow n = Cx(&1)) /\
78 (--Cx(&1) pow n = --Cx(&1)) /\
79 (((ii pow n = ii) /\ (--ii pow n = --ii)) \/
80 ((ii pow n = --ii) /\ (--ii pow n = ii)))`
83 RULE_ASSUM_TAC(REWRITE_RULE[complex_sub]) THEN ASM_MESON_TAC[]] THEN
84 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_EVEN]) THEN
85 SIMP_TAC[ODD_EXISTS; LEFT_IMP_EXISTS_THM] THEN
86 X_GEN_TAC `m:num` THEN DISCH_THEN(K ALL_TAC) THEN
87 REWRITE_TAC[complex_pow; COMPLEX_POW_NEG; EVEN; EVEN_MULT; ARITH_EVEN] THEN
88 REWRITE_TAC[GSYM COMPLEX_POW_POW] THEN
89 REWRITE_TAC[COMPLEX_POW_ONE; COMPLEX_POW_II_2; COMPLEX_MUL_LID;
92 REWRITE_TAC[COMPLEX_MUL_RID; COMPLEX_MUL_RNEG; COMPLEX_NEG_NEG];
94 DISCH_THEN(X_CHOOSE_THEN `v:complex` ASSUME_TAC) THEN
95 EXISTS_TAC `v / Cx(root(n) (norm b))` THEN
96 REWRITE_TAC[COMPLEX_POW_DIV; GSYM CX_POW] THEN
97 SUBGOAL_THEN `root n (norm b) pow n = norm b` SUBST1_TAC THENL
98 [UNDISCH_TAC `~(EVEN n)` THEN SPEC_TAC(`n:num`,`n:num`) THEN
99 INDUCT_TAC THEN SIMP_TAC[EVEN; ROOT_POW_POS; COMPLEX_NORM_POS];
101 MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN EXISTS_TAC `norm(Cx(norm b) / b)` THEN
102 REWRITE_TAC[GSYM COMPLEX_NORM_MUL; COMPLEX_ADD_LDISTRIB] THEN
103 REWRITE_TAC[COMPLEX_MUL_RID; REAL_MUL_RID] THEN
104 SUBGOAL_THEN `norm(Cx(norm b) / b) = &1` SUBST1_TAC THENL
105 [REWRITE_TAC[COMPLEX_NORM_DIV; COMPLEX_NORM_CX; COMPLEX_ABS_NORM] THEN
106 ASM_SIMP_TAC[REAL_DIV_REFL; COMPLEX_NORM_ZERO]; ALL_TAC] THEN
107 REWRITE_TAC[REAL_LT_01; complex_div] THEN
108 ONCE_REWRITE_TAC[AC COMPLEX_MUL_AC
109 `(m * b') * b * p * m' = (m * m') * (b * b') * p`] THEN
110 ASM_SIMP_TAC[COMPLEX_MUL_RINV; COMPLEX_MUL_LID;
111 CX_INJ; COMPLEX_NORM_ZERO] THEN
112 ASM_REWRITE_TAC[GSYM complex_div]);;
114 (* ------------------------------------------------------------------------- *)
115 (* Basic lemmas about polynomials. *)
116 (* ------------------------------------------------------------------------- *)
118 let POLY_CMUL_MAP = prove
119 (`!p c x. poly (MAP (( * ) c) p) x = c * poly p x`,
120 LIST_INDUCT_TAC THEN REWRITE_TAC[MAP; poly; COMPLEX_MUL_RZERO] THEN
121 ASM_REWRITE_TAC[COMPLEX_ADD_LDISTRIB] THEN REWRITE_TAC[COMPLEX_MUL_AC]);;
124 (`!p x. ALL (\b. b = Cx(&0)) p ==> (poly p x = Cx(&0))`,
126 ASM_SIMP_TAC[ALL; poly; COMPLEX_MUL_RZERO; COMPLEX_ADD_RID]);;
128 let POLY_BOUND_EXISTS = prove
129 (`!p r. ?m. &0 < m /\ !z. norm(z) <= r ==> norm(poly p z) <= m`,
130 ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN GEN_TAC THEN
131 LIST_INDUCT_TAC THENL
132 [EXISTS_TAC `&1` THEN REWRITE_TAC[poly; COMPLEX_NORM_CX] THEN
133 REWRITE_TAC[REAL_ABS_NUM; REAL_LT_01; REAL_POS]; ALL_TAC] THEN
134 POP_ASSUM(X_CHOOSE_THEN `m:real` STRIP_ASSUME_TAC) THEN
135 EXISTS_TAC `&1 + norm(h) + abs(r * m)` THEN
136 ASM_SIMP_TAC[REAL_ARITH `&0 <= x /\ &0 <= y ==> &0 < &1 + x + y`;
137 REAL_ABS_POS; COMPLEX_NORM_POS] THEN
138 X_GEN_TAC `z:complex` THEN DISCH_TAC THEN
139 REWRITE_TAC[poly] THEN MATCH_MP_TAC REAL_LE_TRANS THEN
140 EXISTS_TAC `norm(h) + norm(z * poly t z)` THEN
141 REWRITE_TAC[COMPLEX_NORM_TRIANGLE] THEN
142 MATCH_MP_TAC(REAL_ARITH `y <= z ==> x + y <= &1 + x + abs(z)`) THEN
143 REWRITE_TAC[COMPLEX_NORM_MUL] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN
144 ASM_SIMP_TAC[COMPLEX_NORM_POS]);;
146 (* ------------------------------------------------------------------------- *)
147 (* Offsetting the variable in a polynomial gives another of same degree. *)
148 (* ------------------------------------------------------------------------- *)
150 let POLY_OFFSET_LEMMA = prove
151 (`!a p. ?b q. (LENGTH q = LENGTH p) /\
152 !x. poly (CONS b q) x = (a + x) * poly p x`,
153 GEN_TAC THEN LIST_INDUCT_TAC THENL
154 [EXISTS_TAC `Cx(&0)` THEN EXISTS_TAC `[]:complex list` THEN
155 REWRITE_TAC[poly; LENGTH; COMPLEX_MUL_RZERO; COMPLEX_ADD_RID];
157 POP_ASSUM STRIP_ASSUME_TAC THEN
158 EXISTS_TAC `a * h` THEN EXISTS_TAC `CONS (b + h) q` THEN
159 ASM_REWRITE_TAC[LENGTH; poly] THEN X_GEN_TAC `x:complex ` THEN
160 FIRST_ASSUM(MP_TAC o SPEC `x:complex`) THEN
161 REWRITE_TAC[poly] THEN DISCH_THEN(MP_TAC o AP_TERM `( * ) x`) THEN
162 SIMPLE_COMPLEX_ARITH_TAC);;
164 let POLY_OFFSET = prove
165 (`!a p. ?q. (LENGTH q = LENGTH p) /\ !x. poly q x = poly p (a + x)`,
166 GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[LENGTH; poly] THENL
167 [EXISTS_TAC `[]:complex list` THEN REWRITE_TAC[poly; LENGTH]; ALL_TAC] THEN
168 POP_ASSUM(X_CHOOSE_THEN `p:complex list` (STRIP_ASSUME_TAC o GSYM)) THEN
169 ASM_REWRITE_TAC[] THEN
170 MP_TAC(SPECL [`a:complex`; `p:complex list`] POLY_OFFSET_LEMMA) THEN
171 DISCH_THEN(X_CHOOSE_THEN `b:complex` (X_CHOOSE_THEN `r: complex list`
172 (STRIP_ASSUME_TAC o GSYM))) THEN
173 EXISTS_TAC `CONS (h + b) r` THEN ASM_REWRITE_TAC[LENGTH] THEN
174 REWRITE_TAC[poly] THEN SIMPLE_COMPLEX_ARITH_TAC);;
176 (* ------------------------------------------------------------------------- *)
177 (* Bolzano-Weierstrass type property for closed disc in complex plane. *)
178 (* ------------------------------------------------------------------------- *)
180 let METRIC_BOUND_LEMMA = prove
181 (`!x y. norm(x - y) <= abs(Re(x) - Re(y)) + abs(Im(x) - Im(y))`,
182 REPEAT GEN_TAC THEN REWRITE_TAC[complex_norm] THEN
183 MATCH_MP_TAC(REAL_ARITH
184 `a <= abs(abs x + abs y) ==> a <= abs x + abs y`) THEN
185 GEN_REWRITE_TAC RAND_CONV [GSYM POW_2_SQRT_ABS] THEN
186 MATCH_MP_TAC SQRT_MONO_LE THEN
187 SIMP_TAC[REAL_POW_2; REAL_LE_ADD; REAL_LE_SQUARE] THEN
188 REWRITE_TAC[complex_add; complex_sub; complex_neg; RE; IM] THEN
189 REWRITE_TAC[GSYM real_sub] THEN
190 REWRITE_TAC[REAL_ARITH `(a + b) * (a + b) = a * a + b * b + &2 * a * b`] THEN
191 REWRITE_TAC[GSYM REAL_ABS_MUL] THEN
192 REWRITE_TAC[REAL_ARITH `a + b <= abs a + abs b + &2 * abs c`]);;
194 let BOLZANO_WEIERSTRASS_COMPLEX_DISC = prove
195 (`!s r. (!n. norm(s n) <= r)
196 ==> ?f z. subseq f /\
197 !e. &0 < e ==> ?N. !n. n >= N ==> norm(s(f n) - z) < e`,
198 REPEAT STRIP_TAC THEN
199 MP_TAC(SPEC `Re o (s:num->complex)` SEQ_MONOSUB) THEN
200 DISCH_THEN(X_CHOOSE_THEN `f:num->num` MP_TAC) THEN
201 REWRITE_TAC[o_THM] THEN STRIP_TAC THEN
202 MP_TAC(SPEC `Im o (s:num->complex) o (f:num->num)` SEQ_MONOSUB) THEN
203 DISCH_THEN(X_CHOOSE_THEN `g:num->num` MP_TAC) THEN
204 REWRITE_TAC[o_THM] THEN STRIP_TAC THEN
205 EXISTS_TAC `(f:num->num) o (g:num->num)` THEN
206 SUBGOAL_THEN `convergent (\n. Re(s(f n :num))) /\
207 convergent (\n. Im(s((f:num->num)(g n))))`
209 [CONJ_TAC THEN MATCH_MP_TAC SEQ_BCONV THEN ASM_REWRITE_TAC[bounded] THEN
210 MAP_EVERY EXISTS_TAC [`r + &1`; `&0`; `0`] THEN
211 REWRITE_TAC[GE; LE_0; MR1_DEF; REAL_SUB_LZERO; REAL_ABS_NEG] THEN
212 X_GEN_TAC `n:num` THEN
213 W(fun (_,w) -> FIRST_ASSUM(MP_TAC o SPEC (funpow 3 rand (lhand w)))) THEN
214 REWRITE_TAC[complex_norm] THEN
215 MATCH_MP_TAC(REAL_ARITH `a <= b ==> b <= r ==> a < r + &1`) THEN
216 GEN_REWRITE_TAC LAND_CONV [GSYM POW_2_SQRT_ABS] THEN
217 MATCH_MP_TAC SQRT_MONO_LE THEN
218 REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE; REAL_LE_ADDR; REAL_LE_ADDL];
220 REWRITE_TAC[convergent; SEQ; GE] THEN
221 DISCH_THEN(CONJUNCTS_THEN2
222 (X_CHOOSE_TAC `x:real`) (X_CHOOSE_TAC `y:real`)) THEN
223 EXISTS_TAC `complex(x,y)` THEN CONJ_TAC THENL
224 [MAP_EVERY UNDISCH_TAC [`subseq f`; `subseq g`] THEN
225 REWRITE_TAC[subseq; o_THM] THEN MESON_TAC[]; ALL_TAC] THEN
226 X_GEN_TAC `e:real` THEN DISCH_TAC THEN
229 ==> (?N. !n. N <= n ==> abs(Re(s ((f:num->num) n)) - x) < e)` THEN
230 DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN
231 FIRST_X_ASSUM(MP_TAC o SPEC `e / &2`) THEN
232 ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
233 DISCH_THEN(X_CHOOSE_TAC `N2:num`) THEN DISCH_THEN(X_CHOOSE_TAC `N1:num`) THEN
234 EXISTS_TAC `N1 + N2:num` THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN
235 MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&2 * e / &2` THEN
238 SIMP_TAC[REAL_DIV_LMUL; REAL_OF_NUM_EQ; ARITH; REAL_LE_REFL]] THEN
239 W(MP_TAC o PART_MATCH lhand METRIC_BOUND_LEMMA o lhand o snd) THEN
240 MATCH_MP_TAC(REAL_ARITH
241 `a < c /\ b < c ==> x <= a + b ==> x < &2 * c`) THEN
242 REWRITE_TAC[o_THM; RE; IM] THEN CONJ_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
243 ASM_MESON_TAC[LE_ADD; SEQ_SUBLE; LE_TRANS; ADD_SYM]);;
245 (* ------------------------------------------------------------------------- *)
246 (* Polynomial is continuous. *)
247 (* ------------------------------------------------------------------------- *)
249 let POLY_CONT = prove
251 ==> ?d. &0 < d /\ !w. &0 < norm(w - z) /\ norm(w - z) < d
252 ==> norm(poly p w - poly p z) < e`,
253 REPEAT STRIP_TAC THEN
254 MP_TAC(SPECL [`z:complex`; `p:complex list`] POLY_OFFSET) THEN
255 DISCH_THEN(X_CHOOSE_THEN `q:complex list` (MP_TAC o CONJUNCT2)) THEN
256 DISCH_THEN(MP_TAC o GEN `w:complex` o SYM o SPEC `w - z`) THEN
257 REWRITE_TAC[COMPLEX_SUB_ADD2] THEN
258 DISCH_THEN(fun th -> ONCE_REWRITE_TAC[th]) THEN
259 REWRITE_TAC[COMPLEX_SUB_REFL] THEN
260 SPEC_TAC(`q:complex list`,`p:complex list`) THEN
261 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[poly] THENL
262 [EXISTS_TAC `e:real` THEN
263 ASM_REWRITE_TAC[COMPLEX_SUB_REFL; COMPLEX_NORM_CX; REAL_ABS_NUM];
265 REWRITE_TAC[COMPLEX_MUL_LZERO; COMPLEX_ADD_RID; COMPLEX_ADD_SUB] THEN
266 MP_TAC(SPECL [`t:complex list`; `&1`] POLY_BOUND_EXISTS) THEN
267 DISCH_THEN(X_CHOOSE_THEN `m:real` STRIP_ASSUME_TAC) THEN
268 MP_TAC(SPECL [`&1`; `e / m:real`] REAL_DOWN2) THEN
269 ASM_SIMP_TAC[REAL_LT_DIV; REAL_LT_01] THEN
270 MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `d:real` THEN
271 STRIP_TAC THEN ASM_REWRITE_TAC[] THEN X_GEN_TAC `w:complex` THEN
272 STRIP_TAC THEN REWRITE_TAC[COMPLEX_NORM_MUL] THEN
273 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `d * m:real` THEN
274 ASM_SIMP_TAC[GSYM REAL_LT_RDIV_EQ] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN
275 ASM_MESON_TAC[REAL_LT_TRANS; REAL_LT_IMP_LE; COMPLEX_NORM_POS]);;
277 (* ------------------------------------------------------------------------- *)
278 (* Hence a polynomial attains minimum on a closed disc in the complex plane. *)
279 (* ------------------------------------------------------------------------- *)
281 let POLY_MINIMUM_MODULUS_DISC = prove
282 (`!p r. ?z. !w. norm(w) <= r ==> norm(poly p z) <= norm(poly p w)`,
284 (`P /\ (m = --x) /\ --x < y <=> (--x = m) /\ P /\ m < y`,
287 ASM_CASES_TAC `&0 <= r` THENL
288 [ALL_TAC; ASM_MESON_TAC[COMPLEX_NORM_POS; REAL_LE_TRANS]] THEN
289 MP_TAC(SPEC `\x. ?z. norm(z) <= r /\ (norm(poly p z) = --x)`
290 REAL_SUP_EXISTS) THEN
291 REWRITE_TAC[] THEN ANTS_TAC THENL
293 [MAP_EVERY EXISTS_TAC [`--norm(poly p (Cx(&0)))`; `Cx(&0)`] THEN
294 ASM_REWRITE_TAC[REAL_NEG_NEG; COMPLEX_NORM_CX; REAL_ABS_NUM];
296 REWRITE_TAC[REAL_ARITH `(a = --b) <=> (--b = a:real)`] THEN
297 REWRITE_TAC[REAL_ARITH `x < &1 <=> --(&1) < --x`] THEN
298 SIMP_TAC[LEFT_IMP_EXISTS_THM] THEN
299 SIMP_TAC[REAL_ARITH `&0 <= x ==> --(&1) < x`; COMPLEX_NORM_POS]];
301 DISCH_THEN(X_CHOOSE_THEN `s:real` MP_TAC) THEN
302 ONCE_REWRITE_TAC[REAL_ARITH `a < b <=> --b < --a:real`] THEN
303 ABBREV_TAC `m = --s:real` THEN
304 DISCH_THEN(MP_TAC o GEN `y:real` o SPEC `--y:real`) THEN
305 REWRITE_TAC[REAL_NEG_NEG] THEN
306 REWRITE_TAC[LEFT_AND_EXISTS_THM; GSYM CONJ_ASSOC; lemma] THEN
307 ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
308 ONCE_REWRITE_TAC[REAL_ARITH `(--a = b) <=> (a = --b:real)`] THEN
309 REWRITE_TAC[LEFT_EXISTS_AND_THM; EXISTS_REFL] THEN
310 DISCH_THEN(fun th -> MP_TAC th THEN MP_TAC(SPEC `m:real` th)) THEN
311 REWRITE_TAC[REAL_LT_REFL; NOT_EXISTS_THM] THEN
312 REWRITE_TAC[TAUT `~(a /\ b) <=> a ==> ~b`] THEN
313 REWRITE_TAC[REAL_NOT_LT] THEN DISCH_TAC THEN
314 DISCH_THEN(MP_TAC o GEN `n:num` o SPEC `m + inv(&(SUC n))`) THEN
315 REWRITE_TAC[REAL_LT_ADDR; REAL_LT_INV_EQ; REAL_OF_NUM_LT; LT_0] THEN
316 REWRITE_TAC[SKOLEM_THM; FORALL_AND_THM] THEN
317 DISCH_THEN(X_CHOOSE_THEN `s:num->complex` STRIP_ASSUME_TAC) THEN
318 MP_TAC(SPECL [`s:num->complex`; `r:real`]
319 BOLZANO_WEIERSTRASS_COMPLEX_DISC) THEN ASM_REWRITE_TAC[] THEN
320 DISCH_THEN(X_CHOOSE_THEN `f:num->num` (X_CHOOSE_THEN `z:complex`
321 STRIP_ASSUME_TAC)) THEN
322 EXISTS_TAC `z:complex` THEN X_GEN_TAC `w:complex` THEN DISCH_TAC THEN
323 SUBGOAL_THEN `norm(poly p z) = m` (fun th -> ASM_SIMP_TAC[th]) THEN
324 MATCH_MP_TAC(REAL_ARITH `~(&0 < abs(a - b)) ==> (a = b)`) THEN DISCH_TAC THEN
325 ABBREV_TAC `e = abs(norm(poly p z) - m)` THEN
326 MP_TAC(SPECL [`p:complex list`; `z:complex`; `e / &2`] POLY_CONT) THEN
327 ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
328 DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
329 SUBGOAL_THEN `!w. norm(w - z) < d ==> norm(poly p w - poly p z) < e / &2`
331 [X_GEN_TAC `u:complex` THEN
332 ASM_CASES_TAC `u = z:complex` THEN
333 ASM_SIMP_TAC[COMPLEX_SUB_REFL; REAL_LT_DIV; REAL_OF_NUM_LT; ARITH;
334 COMPLEX_NORM_CX; REAL_ABS_NUM] THEN
335 DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
336 ASM_REWRITE_TAC[COMPLEX_NORM_NZ; COMPLEX_SUB_0]; ALL_TAC] THEN
337 FIRST_ASSUM(K ALL_TAC o check (is_conj o lhand o
338 snd o dest_forall o concl)) THEN
340 FIRST_X_ASSUM(MP_TAC o SPEC `d:real`) THEN ASM_REWRITE_TAC[GE] THEN
341 DISCH_THEN(X_CHOOSE_THEN `N1:num` ASSUME_TAC) THEN
342 MP_TAC(SPEC `&2 / e` REAL_ARCH_SIMPLE) THEN
343 DISCH_THEN(X_CHOOSE_THEN `N2:num` ASSUME_TAC) THEN
344 SUBGOAL_THEN `norm(poly p (s((f:num->num) (N1 + N2))) - poly p z) < e / &2`
346 [FIRST_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[LE_ADD]; ALL_TAC] THEN
347 MATCH_MP_TAC(REAL_ARITH
348 `!m. abs(norm(psfn) - m) < e2 /\
349 &2 * e2 <= abs(norm(psfn) - m) + norm(psfn - pz)
350 ==> norm(psfn - pz) < e2 ==> F`) THEN
351 EXISTS_TAC `m:real` THEN CONJ_TAC THENL
352 [MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `inv(&(SUC(N1 + N2)))` THEN
354 [MATCH_MP_TAC(REAL_ARITH
355 `m <= x /\ x < m + e ==> abs(x - m:real) < e`) THEN
357 MATCH_MP_TAC REAL_LTE_TRANS THEN
358 EXISTS_TAC `m + inv(&(SUC(f(N1 + N2:num))))` THEN
359 ASM_REWRITE_TAC[REAL_LE_LADD] THEN MATCH_MP_TAC REAL_LE_INV2 THEN
360 ASM_SIMP_TAC[REAL_OF_NUM_LT; REAL_OF_NUM_LE; LT_0; LE_SUC; SEQ_SUBLE];
361 GEN_REWRITE_TAC RAND_CONV [GSYM REAL_INV_DIV] THEN
362 MATCH_MP_TAC REAL_LE_INV2 THEN
363 ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN
364 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&N2` THEN
365 ASM_REWRITE_TAC[REAL_OF_NUM_LE] THEN ARITH_TAC]; ALL_TAC] THEN
366 SIMP_TAC[REAL_DIV_LMUL; REAL_OF_NUM_EQ; ARITH] THEN
368 MATCH_MP_TAC(REAL_ARITH
369 `abs(norm(psfn) - norm(pz)) <= norm(psfn - pz)
370 ==> abs(norm(pz) - m) <= abs(norm(psfn) - m) + norm(psfn - pz)`) THEN
371 REWRITE_TAC[COMPLEX_NORM_ABS_NORM]);;
373 (* ------------------------------------------------------------------------- *)
374 (* Nonzero polynomial in z goes to infinity as z does. *)
375 (* ------------------------------------------------------------------------- *)
377 let POLY_INFINITY = prove
378 (`!p a. EX (\b. ~(b = Cx(&0))) p
379 ==> !d. ?r. !z. r <= norm(z) ==> d <= norm(poly (CONS a p) z)`,
380 LIST_INDUCT_TAC THEN REWRITE_TAC[EX] THEN X_GEN_TAC `a:complex` THEN
381 ASM_CASES_TAC `EX (\b. ~(b = Cx(&0))) t` THEN ASM_REWRITE_TAC[] THENL
382 [X_GEN_TAC `d:real` THEN
383 FIRST_X_ASSUM(MP_TAC o SPEC `h:complex`) THEN ASM_REWRITE_TAC[] THEN
384 DISCH_THEN(X_CHOOSE_TAC `r:real` o SPEC `d + norm(a)`) THEN
385 EXISTS_TAC `&1 + abs(r)` THEN X_GEN_TAC `z:complex` THEN DISCH_TAC THEN
386 ONCE_REWRITE_TAC[poly] THEN
387 MATCH_MP_TAC REAL_LE_TRANS THEN
388 EXISTS_TAC `norm(z * poly (CONS h t) z) - norm(a)` THEN CONJ_TAC THENL
390 ONCE_REWRITE_TAC[COMPLEX_ADD_SYM] THEN
391 REWRITE_TAC[REAL_LE_SUB_RADD; COMPLEX_NORM_TRIANGLE_SUB]] THEN
392 REWRITE_TAC[REAL_LE_SUB_LADD] THEN
393 MATCH_MP_TAC REAL_LE_TRANS THEN
394 EXISTS_TAC `&1 * norm(poly (CONS h t) z)` THEN CONJ_TAC THENL
395 [REWRITE_TAC[REAL_MUL_LID] THEN FIRST_ASSUM MATCH_MP_TAC THEN
396 ASM_SIMP_TAC[REAL_ARITH `&1 + abs(r) <= x ==> r <= x`];
397 REWRITE_TAC[COMPLEX_NORM_MUL] THEN MATCH_MP_TAC REAL_LE_RMUL THEN
398 REWRITE_TAC[COMPLEX_NORM_POS] THEN
399 ASM_MESON_TAC[REAL_ARITH `&1 + abs(r) <= x ==> &1 <= x`]];
400 RULE_ASSUM_TAC(REWRITE_RULE[NOT_EX]) THEN
401 ASM_SIMP_TAC[poly; POLY_0; COMPLEX_MUL_RZERO; COMPLEX_ADD_RID] THEN
402 DISCH_TAC THEN X_GEN_TAC `d:real` THEN
403 EXISTS_TAC `(abs(d) + norm(a)) / norm(h)` THEN X_GEN_TAC `z:complex` THEN
404 ASM_SIMP_TAC[REAL_LE_LDIV_EQ; COMPLEX_NORM_NZ; GSYM COMPLEX_NORM_MUL] THEN
405 MATCH_MP_TAC(REAL_ARITH
406 `mzh <= mazh + ma ==> abs(d) + ma <= mzh ==> d <= mazh`) THEN
407 ONCE_REWRITE_TAC[COMPLEX_ADD_SYM] THEN
408 REWRITE_TAC[COMPLEX_NORM_TRIANGLE_SUB]]);;
410 (* ------------------------------------------------------------------------- *)
411 (* Hence polynomial's modulus attains its minimum somewhere. *)
412 (* ------------------------------------------------------------------------- *)
414 let POLY_MINIMUM_MODULUS = prove
415 (`!p. ?z. !w. norm(poly p z) <= norm(poly p w)`,
416 LIST_INDUCT_TAC THEN REWRITE_TAC[poly; REAL_LE_REFL] THEN
417 ASM_CASES_TAC `EX (\b. ~(b = Cx(&0))) t` THENL
418 [FIRST_ASSUM(MP_TAC o SPEC `h:complex` o MATCH_MP POLY_INFINITY) THEN
419 DISCH_THEN(MP_TAC o SPEC `norm(poly (CONS h t) (Cx(&0)))`) THEN
420 DISCH_THEN(X_CHOOSE_THEN `r:real` ASSUME_TAC) THEN
421 MP_TAC(SPECL [`CONS (h:complex) t`; `abs(r)`]
422 POLY_MINIMUM_MODULUS_DISC) THEN
423 REWRITE_TAC[GSYM(CONJUNCT2 poly)] THEN
424 ASM_MESON_TAC[REAL_ARITH `r <= z \/ z <= abs(r)`; REAL_LE_TRANS;
425 COMPLEX_NORM_CX; REAL_ABS_NUM; REAL_ABS_POS];
426 FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [NOT_EX]) THEN
427 REWRITE_TAC[] THEN DISCH_THEN(ASSUME_TAC o MATCH_MP POLY_0) THEN
428 ASM_REWRITE_TAC[COMPLEX_MUL_RZERO; REAL_LE_REFL]]);;
430 (* ------------------------------------------------------------------------- *)
431 (* Constant function (non-syntactic characterization). *)
432 (* ------------------------------------------------------------------------- *)
434 let constant = new_definition
435 `constant f = !w z. f(w) = f(z)`;;
437 let NONCONSTANT_LENGTH = prove
438 (`!p. ~constant(poly p) ==> 2 <= LENGTH p`,
439 REWRITE_TAC[constant] THEN
440 LIST_INDUCT_TAC THEN REWRITE_TAC[poly] THEN
441 REWRITE_TAC[LENGTH; ARITH_RULE `2 <= SUC n <=> ~(n = 0)`] THEN
442 SIMP_TAC[TAUT `~a ==> ~b <=> b ==> a`; LENGTH_EQ_NIL; poly] THEN
443 REWRITE_TAC[COMPLEX_MUL_RZERO]);;
445 (* ------------------------------------------------------------------------- *)
446 (* Decomposition of polynomial, skipping zero coefficients after the first. *)
447 (* ------------------------------------------------------------------------- *)
449 let POLY_DECOMPOSE_LEMMA = prove
450 (`!p. ~(!z. ~(z = Cx(&0)) ==> (poly p z = Cx(&0)))
451 ==> ?k a q. ~(a = Cx(&0)) /\
452 (SUC(LENGTH q + k) = LENGTH p) /\
453 !z. poly p z = z pow k * poly (CONS a q) z`,
454 LIST_INDUCT_TAC THENL [REWRITE_TAC[poly]; ALL_TAC] THEN
455 ASM_CASES_TAC `h = Cx(&0)` THENL
456 [GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [poly] THEN
457 ASM_SIMP_TAC[COMPLEX_ADD_LID; COMPLEX_ENTIRE] THEN
458 DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
459 DISCH_THEN(X_CHOOSE_THEN `k:num` (X_CHOOSE_THEN `a:complex`
460 (X_CHOOSE_THEN `q:complex list` STRIP_ASSUME_TAC))) THEN
461 MAP_EVERY EXISTS_TAC [`k + 1`; `a:complex`; `q:complex list`] THEN
462 ASM_REWRITE_TAC[poly; LENGTH; GSYM ADD1; ADD_CLAUSES] THEN
463 REWRITE_TAC[COMPLEX_ADD_LID; complex_pow; GSYM COMPLEX_MUL_ASSOC];
464 DISCH_THEN(K ALL_TAC) THEN
465 MAP_EVERY EXISTS_TAC [`0`; `h:complex`; `t:complex list`] THEN
466 ASM_REWRITE_TAC[complex_pow; COMPLEX_MUL_LID; ADD_CLAUSES; LENGTH]]);;
468 let POLY_DECOMPOSE = prove
469 (`!p. ~constant(poly p)
470 ==> ?k a q. ~(a = Cx(&0)) /\ ~(k = 0) /\
471 (LENGTH q + k + 1 = LENGTH p) /\
472 !z. poly p z = poly p (Cx(&0)) +
473 z pow k * poly (CONS a q) z`,
474 LIST_INDUCT_TAC THENL [REWRITE_TAC[constant; poly]; ALL_TAC] THEN
475 POP_ASSUM(K ALL_TAC) THEN DISCH_TAC THEN
476 MP_TAC(SPEC `t:complex list` POLY_DECOMPOSE_LEMMA) THEN ANTS_TAC THENL
477 [POP_ASSUM MP_TAC THEN REWRITE_TAC[constant; poly] THEN
478 REWRITE_TAC[TAUT `~b ==> ~a <=> a ==> b`; COMPLEX_EQ_ADD_LCANCEL] THEN
479 SIMP_TAC[TAUT `~a ==> b <=> a \/ b`; GSYM COMPLEX_ENTIRE]; ALL_TAC] THEN
480 DISCH_THEN(X_CHOOSE_THEN `k:num` (X_CHOOSE_THEN `a:complex`
481 (X_CHOOSE_THEN `q:complex list` STRIP_ASSUME_TAC))) THEN
482 MAP_EVERY EXISTS_TAC [`SUC k`; `a:complex`; `q:complex list`] THEN
483 ASM_REWRITE_TAC[ADD_CLAUSES; GSYM ADD1; LENGTH; NOT_SUC] THEN
484 ASM_REWRITE_TAC[poly; COMPLEX_MUL_LZERO; COMPLEX_ADD_RID; complex_pow] THEN
485 REWRITE_TAC[GSYM COMPLEX_MUL_ASSOC]);;
487 let POLY_REPLICATE_APPEND = prove
488 (`!n p x. poly (APPEND (REPLICATE n (Cx(&0))) p) x = x pow n * poly p x`,
490 REWRITE_TAC[REPLICATE; APPEND; complex_pow; COMPLEX_MUL_LID] THEN
491 ASM_REWRITE_TAC[poly; COMPLEX_ADD_LID] THEN REWRITE_TAC[COMPLEX_MUL_ASSOC]);;
493 (* ------------------------------------------------------------------------- *)
494 (* Fundamental theorem. *)
495 (* ------------------------------------------------------------------------- *)
497 let FUNDAMENTAL_THEOREM_OF_ALGEBRA = prove
498 (`!p. ~constant(poly p) ==> ?z. poly p z = Cx(&0)`,
500 `!n p. (LENGTH p = n) /\ ~constant(poly p) ==> ?z. poly p z = Cx(&0)`
501 (fun th -> MESON_TAC[th]) THEN
502 MATCH_MP_TAC num_WF THEN
503 X_GEN_TAC `n:num` THEN STRIP_TAC THEN
504 X_GEN_TAC `p:complex list` THEN STRIP_TAC THEN
505 FIRST_ASSUM(MP_TAC o MATCH_MP NONCONSTANT_LENGTH) THEN
506 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
507 X_CHOOSE_TAC `c:complex` (SPEC `p:complex list` POLY_MINIMUM_MODULUS) THEN
508 ASM_CASES_TAC `poly p c = Cx(&0)` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
509 MP_TAC(SPECL [`c:complex`; `p:complex list`] POLY_OFFSET) THEN
510 DISCH_THEN(X_CHOOSE_THEN `q:complex list` MP_TAC) THEN
511 DISCH_THEN(CONJUNCTS_THEN2 (SUBST_ALL_TAC o SYM) ASSUME_TAC) THEN
512 SUBGOAL_THEN `~constant(poly q)` ASSUME_TAC THENL
513 [UNDISCH_TAC `~(constant(poly p))` THEN
514 SUBGOAL_THEN `!z. poly q (z - c) = poly p z`
515 (fun th -> MESON_TAC[th; constant]) THEN
516 ASM_MESON_TAC[SIMPLE_COMPLEX_ARITH `a + (x - a) = x`]; ALL_TAC] THEN
517 SUBGOAL_THEN `poly p c = poly q (Cx(&0))` SUBST_ALL_TAC THENL
518 [ASM_MESON_TAC[COMPLEX_ADD_RID]; ALL_TAC] THEN
519 SUBGOAL_THEN `!w. norm(poly q (Cx(&0))) <= norm(poly q w)` MP_TAC THENL
520 [ASM_MESON_TAC[]; ALL_TAC] THEN
521 POP_ASSUM_LIST(MAP_EVERY (fun th ->
522 if free_in `p:complex list` (concl th)
523 then ALL_TAC else ASSUME_TAC th)) THEN
524 MATCH_MP_TAC(TAUT `~a ==> a ==> b`) THEN
525 REWRITE_TAC[NOT_FORALL_THM; REAL_NOT_LE] THEN
526 ABBREV_TAC `a0 = poly q (Cx(&0))` THEN
528 `!z. poly q z = poly (MAP (( * ) (inv(a0))) q) z * a0`
530 [REWRITE_TAC[POLY_CMUL_MAP] THEN
531 ONCE_REWRITE_TAC[AC COMPLEX_MUL_AC `(a * b) * c = b * c * a`] THEN
532 ASM_SIMP_TAC[COMPLEX_MUL_RINV; COMPLEX_MUL_RID];
534 ABBREV_TAC `r = MAP (( * ) (inv(a0))) q` THEN
535 SUBGOAL_THEN `LENGTH(q:complex list) = LENGTH(r:complex list)`
537 [EXPAND_TAC "r" THEN REWRITE_TAC[LENGTH_MAP]; ALL_TAC] THEN
538 SUBGOAL_THEN `~(constant(poly r))` ASSUME_TAC THENL
539 [UNDISCH_TAC `~constant(poly q)` THEN
540 ASM_REWRITE_TAC[constant; COMPLEX_EQ_MUL_RCANCEL] THEN MESON_TAC[];
542 SUBGOAL_THEN `poly r (Cx(&0)) = Cx(&1)` ASSUME_TAC THENL
543 [FIRST_X_ASSUM(MP_TAC o SPEC `Cx(&0)`) THEN
544 ASM_REWRITE_TAC[] THEN
545 GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [GSYM COMPLEX_MUL_LID] THEN
546 ASM_SIMP_TAC[COMPLEX_EQ_MUL_RCANCEL]; ALL_TAC] THEN
547 ASM_REWRITE_TAC[] THEN
548 POP_ASSUM_LIST(MAP_EVERY (fun th ->
549 if free_in `q:complex list` (concl th)
550 then ALL_TAC else ASSUME_TAC th)) THEN
551 ASM_SIMP_TAC[GSYM REAL_LT_RDIV_EQ; COMPLEX_NORM_NZ; COMPLEX_NORM_MUL;
552 REAL_DIV_REFL; COMPLEX_NORM_ZERO] THEN
553 FIRST_ASSUM(MP_TAC o MATCH_MP POLY_DECOMPOSE) THEN
554 DISCH_THEN(X_CHOOSE_THEN `k:num` (X_CHOOSE_THEN `a:complex`
555 (X_CHOOSE_THEN `s:complex list` MP_TAC))) THEN
556 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
557 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
558 DISCH_THEN(CONJUNCTS_THEN2 (SUBST_ALL_TAC o SYM) MP_TAC) THEN
559 DISCH_THEN(fun th -> ONCE_REWRITE_TAC[th]) THEN ASM_REWRITE_TAC[] THEN
560 ASM_CASES_TAC `k + 1 = n` THENL
561 [UNDISCH_TAC `LENGTH(s:complex list) + k + 1 = n` THEN
562 ASM_REWRITE_TAC[ARITH_RULE `(s + m = m) <=> (s = 0)`; LENGTH_EQ_NIL] THEN
563 REWRITE_TAC[LENGTH_EQ_NIL] THEN DISCH_THEN SUBST1_TAC THEN
564 REWRITE_TAC[poly; COMPLEX_MUL_RZERO; COMPLEX_ADD_RID] THEN
565 ONCE_REWRITE_TAC[COMPLEX_MUL_SYM] THEN
566 MATCH_MP_TAC REDUCE_POLY_SIMPLE THEN ASM_REWRITE_TAC[] THEN
567 MAP_EVERY UNDISCH_TAC [`k + 1 = n`; `2 <= n`] THEN ARITH_TAC; ALL_TAC] THEN
568 FIRST_X_ASSUM(MP_TAC o SPEC `k + 1`) THEN ANTS_TAC THENL
569 [UNDISCH_TAC `~(k + 1 = n)` THEN
570 UNDISCH_TAC `LENGTH(s:complex list) + k + 1 = n` THEN ARITH_TAC;
572 DISCH_THEN(MP_TAC o SPEC
573 `CONS (Cx(&1)) (APPEND (REPLICATE (k - 1) (Cx(&0))) [a])`) THEN
576 [REWRITE_TAC[LENGTH; LENGTH_APPEND; LENGTH_REPLICATE] THEN
577 UNDISCH_TAC `~(k = 0)` THEN ARITH_TAC; ALL_TAC] THEN
578 REWRITE_TAC[constant; POLY_REPLICATE_APPEND; poly] THEN
579 REWRITE_TAC[COMPLEX_MUL_RZERO; COMPLEX_ADD_RID] THEN
580 DISCH_THEN(MP_TAC o SPECL [`Cx(&0)`; `Cx(&1)`]) THEN
581 REWRITE_TAC[COMPLEX_MUL_LID; COMPLEX_MUL_LZERO; COMPLEX_ADD_RID] THEN
582 ASM_REWRITE_TAC[COMPLEX_ENTIRE; COMPLEX_POW_ONE; SIMPLE_COMPLEX_ARITH
583 `(a = a + b) <=> (b = Cx(&0))`] THEN
584 REWRITE_TAC[CX_INJ; REAL_OF_NUM_EQ; ARITH_EQ]; ALL_TAC] THEN
585 REWRITE_TAC[constant; POLY_REPLICATE_APPEND; poly] THEN
586 REWRITE_TAC[COMPLEX_MUL_RZERO; COMPLEX_ADD_RID] THEN
587 ONCE_REWRITE_TAC[AC COMPLEX_MUL_AC `a * b * c = (a * b) * c`] THEN
588 REWRITE_TAC[GSYM(CONJUNCT2 complex_pow)] THEN
589 ASM_SIMP_TAC[ARITH_RULE `~(k = 0) ==> (SUC(k - 1) = k)`] THEN
590 DISCH_THEN(X_CHOOSE_TAC `w:complex`) THEN
591 MP_TAC(SPECL [`s:complex list`; `norm(w)`] POLY_BOUND_EXISTS) THEN
592 DISCH_THEN(X_CHOOSE_THEN `m:real` STRIP_ASSUME_TAC) THEN
593 SUBGOAL_THEN `~(w = Cx(&0))` ASSUME_TAC THENL
594 [UNDISCH_TAC `Cx(&1) + w pow k * a = Cx(&0)` THEN
595 ONCE_REWRITE_TAC[TAUT `a ==> ~b <=> b ==> ~a`] THEN
596 DISCH_THEN SUBST1_TAC THEN
597 UNDISCH_TAC `~(k = 0)` THEN SPEC_TAC(`k:num`,`k:num`) THEN
598 INDUCT_TAC THEN REWRITE_TAC[complex_pow; COMPLEX_MUL_LZERO] THEN
599 REWRITE_TAC[COMPLEX_ADD_RID; CX_INJ; REAL_OF_NUM_EQ; ARITH_EQ];
601 MP_TAC(SPECL [`&1`; `inv(norm(w) pow (k + 1) * m)`] REAL_DOWN2) THEN
602 ASM_SIMP_TAC[REAL_LT_01; REAL_LT_INV_EQ; REAL_LT_MUL; REAL_POW_LT;
603 COMPLEX_NORM_NZ] THEN
604 DISCH_THEN(X_CHOOSE_THEN `t:real` STRIP_ASSUME_TAC) THEN
605 EXISTS_TAC `Cx(t) * w` THEN REWRITE_TAC[COMPLEX_POW_MUL] THEN
606 REWRITE_TAC[COMPLEX_ADD_LDISTRIB; GSYM COMPLEX_MUL_ASSOC] THEN
607 FIRST_ASSUM(SUBST1_TAC o MATCH_MP (SIMPLE_COMPLEX_ARITH
608 `(a + w = Cx(&0)) ==> (w = --a)`)) THEN
609 REWRITE_TAC[GSYM CX_NEG; GSYM CX_POW; GSYM CX_MUL] THEN
610 REWRITE_TAC[COMPLEX_ADD_ASSOC; GSYM CX_ADD] THEN
611 MATCH_MP_TAC REAL_LET_TRANS THEN
612 EXISTS_TAC `norm(Cx(&1 + t pow k * -- &1)) +
613 norm(Cx(t pow k) * w pow k * Cx t * w * poly s (Cx t * w))` THEN
614 REWRITE_TAC[COMPLEX_NORM_TRIANGLE] THEN REWRITE_TAC[COMPLEX_NORM_CX] THEN
615 MATCH_MP_TAC(REAL_ARITH
616 `&0 <= x /\ x < t /\ t <= &1 ==> abs(&1 + t * --(&1)) + x < &1`) THEN
617 REWRITE_TAC[COMPLEX_NORM_POS] THEN
618 ASM_SIMP_TAC[REAL_POW_1_LE; REAL_LT_IMP_LE] THEN
619 ONCE_REWRITE_TAC[COMPLEX_NORM_MUL] THEN REWRITE_TAC[COMPLEX_NORM_CX] THEN
620 ASM_SIMP_TAC[real_abs; REAL_LT_IMP_LE; REAL_POW_LE] THEN
621 GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN
622 MATCH_MP_TAC REAL_LT_LMUL THEN ASM_SIMP_TAC[REAL_POW_LT] THEN
623 ONCE_REWRITE_TAC[AC COMPLEX_MUL_AC `a * b * c * d = b * (c * a) * d`] THEN
624 REWRITE_TAC[GSYM(CONJUNCT2 complex_pow)] THEN
625 REWRITE_TAC[COMPLEX_NORM_MUL; ADD1; COMPLEX_NORM_CX] THEN
626 MATCH_MP_TAC REAL_LET_TRANS THEN
627 EXISTS_TAC `abs t * norm(w pow (k + 1)) * m` THEN CONJ_TAC THENL
628 [MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN
629 MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[COMPLEX_NORM_POS] THEN
630 FIRST_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[COMPLEX_NORM_MUL] THEN
631 GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN
632 MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[COMPLEX_NORM_POS] THEN
633 ASM_SIMP_TAC[COMPLEX_NORM_CX; REAL_ARITH
634 `&0 < t /\ t < &1 ==> abs(t) <= &1`]; ALL_TAC] THEN
635 ASM_SIMP_TAC[GSYM REAL_LT_RDIV_EQ; REAL_LT_MUL; COMPLEX_NORM_POW;
636 REAL_POW_LT; COMPLEX_NORM_NZ] THEN
637 ASM_SIMP_TAC[real_div; REAL_MUL_LID;
638 REAL_ARITH `&0 < t /\ t < x ==> abs(t) < x`]);;
640 (* ------------------------------------------------------------------------- *)
641 (* Alternative version with a syntactic notion of constant polynomial. *)
642 (* ------------------------------------------------------------------------- *)
644 let FUNDAMENTAL_THEOREM_OF_ALGEBRA_ALT = prove
645 (`!p. ~(?a l. ~(a = Cx(&0)) /\ ALL (\b. b = Cx(&0)) l /\ (p = CONS a l))
646 ==> ?z. poly p z = Cx(&0)`,
647 LIST_INDUCT_TAC THEN REWRITE_TAC[poly; CONS_11] THEN
648 POP_ASSUM_LIST(K ALL_TAC) THEN
649 ONCE_REWRITE_TAC[AC CONJ_ACI `a /\ b /\ c /\ d <=> c /\ d /\ a /\ b`] THEN
650 REWRITE_TAC[RIGHT_EXISTS_AND_THM; UNWIND_THM1] THEN
651 ASM_CASES_TAC `h = Cx(&0)` THEN ASM_REWRITE_TAC[COMPLEX_ADD_LID] THENL
652 [EXISTS_TAC `Cx(&0)` THEN ASM_REWRITE_TAC[COMPLEX_MUL_LZERO]; ALL_TAC] THEN
653 DISCH_TAC THEN REWRITE_TAC[GSYM(CONJUNCT2 poly)] THEN
654 MATCH_MP_TAC FUNDAMENTAL_THEOREM_OF_ALGEBRA THEN
655 UNDISCH_TAC `~ALL (\b. b = Cx (&0)) t` THEN
656 REWRITE_TAC[TAUT `~b ==> ~a <=> a ==> b`] THEN POP_ASSUM(K ALL_TAC) THEN
657 REWRITE_TAC[constant; poly; REAL_EQ_LADD] THEN
658 DISCH_THEN(MP_TAC o SPEC `Cx(&0)` o ONCE_REWRITE_RULE[SWAP_FORALL_THM]) THEN
659 REWRITE_TAC[COMPLEX_MUL_LZERO; COMPLEX_EQ_ADD_LCANCEL] THEN
660 REWRITE_TAC[COMPLEX_ENTIRE; TAUT `a \/ b <=> ~a ==> b`] THEN
661 SPEC_TAC(`t:complex list`,`p:complex list`) THEN
662 LIST_INDUCT_TAC THEN REWRITE_TAC[ALL] THEN
663 ASM_CASES_TAC `h = Cx(&0)` THEN
664 ASM_SIMP_TAC[poly; COMPLEX_ADD_LID; COMPLEX_ENTIRE] THEN
665 MP_TAC(SPECL [`t:complex list`; `&1`] POLY_BOUND_EXISTS) THEN
666 DISCH_THEN(X_CHOOSE_THEN `m:real` STRIP_ASSUME_TAC) THEN
667 MP_TAC(SPECL [`norm(h) / m`; `&1`] REAL_DOWN2) THEN
668 ASM_SIMP_TAC[REAL_LT_01; REAL_LT_DIV; COMPLEX_NORM_NZ] THEN
669 DISCH_THEN(X_CHOOSE_THEN `x:real` STRIP_ASSUME_TAC) THEN
670 DISCH_THEN(MP_TAC o SPEC `Cx(x)`) THEN
671 ASM_SIMP_TAC[CX_INJ; REAL_LT_IMP_NZ] THEN
672 REWRITE_TAC[SIMPLE_COMPLEX_ARITH `(x + y = Cx(&0)) <=> (y = --x)`] THEN
673 DISCH_THEN(MP_TAC o AP_TERM `norm`) THEN REWRITE_TAC[COMPLEX_NORM_NEG] THEN
674 MATCH_MP_TAC(REAL_ARITH `abs(a) < abs(b) ==> ~(a = b)`) THEN
675 REWRITE_TAC[real_abs; COMPLEX_NORM_POS] THEN
676 REWRITE_TAC[COMPLEX_NORM_MUL; COMPLEX_NORM_CX] THEN
677 MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `norm(h) / m * m` THEN
679 [ALL_TAC; ASM_SIMP_TAC[REAL_LE_REFL; REAL_DIV_RMUL; REAL_LT_IMP_NZ]] THEN
680 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `abs(x) * m` THEN
681 ASM_SIMP_TAC[REAL_LT_RMUL; REAL_ARITH `&0 < x /\ x < a ==> abs(x) < a`] THEN
682 ASM_MESON_TAC[REAL_LE_LMUL; REAL_ABS_POS; COMPLEX_NORM_CX;
683 REAL_ARITH `&0 < x /\ x < &1 ==> abs(x) <= &1`]);;