(* Author: Amine Chaieb, TU Muenchen *)
header{*Fundamental Theorem of Algebra*}
theory Fundamental_Theorem_Algebra
imports Polynomial Complex
begin
subsection {* Square root of complex numbers *}
definition csqrt :: "complex \ complex" where
"csqrt z = (if Im z = 0 then
if 0 \ Re z then Complex (sqrt(Re z)) 0
else Complex 0 (sqrt(- Re z))
else Complex (sqrt((cmod z + Re z) /2))
((Im z / abs(Im z)) * sqrt((cmod z - Re z) /2)))"
lemma csqrt[algebra]: "csqrt z ^ 2 = z"
proof-
obtain x y where xy: "z = Complex x y" by (cases z)
{assume y0: "y = 0"
{assume x0: "x \ 0"
then have ?thesis using y0 xy real_sqrt_pow2[OF x0]
by (simp add: csqrt_def power2_eq_square)}
moreover
{assume "\ x \ 0" hence x0: "- x \ 0" by arith
then have ?thesis using y0 xy real_sqrt_pow2[OF x0]
by (simp add: csqrt_def power2_eq_square) }
ultimately have ?thesis by blast}
moreover
{assume y0: "y\0"
{fix x y
let ?z = "Complex x y"
from abs_Re_le_cmod[of ?z] have tha: "abs x \ cmod ?z" by auto
hence "cmod ?z - x \ 0" "cmod ?z + x \ 0" by arith+
hence "(sqrt (x * x + y * y) + x) / 2 \ 0" "(sqrt (x * x + y * y) - x) / 2 \ 0" by (simp_all add: power2_eq_square) }
note th = this
have sq4: "\x::real. x^2 / 4 = (x / 2) ^ 2"
by (simp add: power2_eq_square)
from th[of x y]
have sq4': "sqrt (((sqrt (x * x + y * y) + x)^2 / 4)) = (sqrt (x * x + y * y) + x) / 2" "sqrt (((sqrt (x * x + y * y) - x)^2 / 4)) = (sqrt (x * x + y * y) - x) / 2" unfolding sq4 by simp_all
then have th1: "sqrt ((sqrt (x * x + y * y) + x) * (sqrt (x * x + y * y) + x) / 4) - sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) - x) / 4) = x"
unfolding power2_eq_square by simp
have "sqrt 4 = sqrt (2^2)" by simp
hence sqrt4: "sqrt 4 = 2" by (simp only: real_sqrt_abs)
have th2: "2 *(y * sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) + x) / 4)) / \y\ = y"
using iffD2[OF real_sqrt_pow2_iff sum_power2_ge_zero[of x y]] y0
unfolding power2_eq_square
by (simp add: algebra_simps real_sqrt_divide sqrt4)
from y0 xy have ?thesis apply (simp add: csqrt_def power2_eq_square)
apply (simp add: real_sqrt_sum_squares_mult_ge_zero[of x y] real_sqrt_pow2[OF th(1)[of x y], unfolded power2_eq_square] real_sqrt_pow2[OF th(2)[of x y], unfolded power2_eq_square] real_sqrt_mult[symmetric])
using th1 th2 ..}
ultimately show ?thesis by blast
qed
subsection{* More lemmas about module of complex numbers *}
lemma complex_of_real_power: "complex_of_real x ^ n = complex_of_real (x^n)"
by (rule of_real_power [symmetric])
lemma real_down2: "(0::real) < d1 \ 0 < d2 ==> EX e. 0 < e & e < d1 & e < d2"
apply (rule exI[where x = "min d1 d2 / 2"])
by (simp add: field_simps min_def)
text{* The triangle inequality for cmod *}
lemma complex_mod_triangle_sub: "cmod w \ cmod (w + z) + norm z"
using complex_mod_triangle_ineq2[of "w + z" "-z"] by auto
subsection{* Basic lemmas about complex polynomials *}
lemma poly_bound_exists:
shows "\m. m > 0 \ (\z. cmod z <= r \ cmod (poly p z) \ m)"
proof(induct p)
case 0 thus ?case by (rule exI[where x=1], simp)
next
case (pCons c cs)
from pCons.hyps obtain m where m: "\z. cmod z \ r \ cmod (poly cs z) \ m"
by blast
let ?k = " 1 + cmod c + \r * m\"
have kp: "?k > 0" using abs_ge_zero[of "r*m"] norm_ge_zero[of c] by arith
{fix z
assume H: "cmod z \ r"
from m H have th: "cmod (poly cs z) \ m" by blast
from H have rp: "r \ 0" using norm_ge_zero[of z] by arith
have "cmod (poly (pCons c cs) z) \ cmod c + cmod (z* poly cs z)"
using norm_triangle_ineq[of c "z* poly cs z"] by simp
also have "\ \ cmod c + r*m" using mult_mono[OF H th rp norm_ge_zero[of "poly cs z"]] by (simp add: norm_mult)
also have "\ \ ?k" by simp
finally have "cmod (poly (pCons c cs) z) \ ?k" .}
with kp show ?case by blast
qed
text{* Offsetting the variable in a polynomial gives another of same degree *}
definition
"offset_poly p h = poly_rec 0 (\a p q. smult h q + pCons a q) p"
lemma offset_poly_0: "offset_poly 0 h = 0"
unfolding offset_poly_def by (simp add: poly_rec_0)
lemma offset_poly_pCons:
"offset_poly (pCons a p) h =
smult h (offset_poly p h) + pCons a (offset_poly p h)"
unfolding offset_poly_def by (simp add: poly_rec_pCons)
lemma offset_poly_single: "offset_poly [:a:] h = [:a:]"
by (simp add: offset_poly_pCons offset_poly_0)
lemma poly_offset_poly: "poly (offset_poly p h) x = poly p (h + x)"
apply (induct p)
apply (simp add: offset_poly_0)
apply (simp add: offset_poly_pCons algebra_simps)
done
lemma offset_poly_eq_0_lemma: "smult c p + pCons a p = 0 \ p = 0"
by (induct p arbitrary: a, simp, force)
lemma offset_poly_eq_0_iff: "offset_poly p h = 0 \ p = 0"
apply (safe intro!: offset_poly_0)
apply (induct p, simp)
apply (simp add: offset_poly_pCons)
apply (frule offset_poly_eq_0_lemma, simp)
done
lemma degree_offset_poly: "degree (offset_poly p h) = degree p"
apply (induct p)
apply (simp add: offset_poly_0)
apply (case_tac "p = 0")
apply (simp add: offset_poly_0 offset_poly_pCons)
apply (simp add: offset_poly_pCons)
apply (subst degree_add_eq_right)
apply (rule le_less_trans [OF degree_smult_le])
apply (simp add: offset_poly_eq_0_iff)
apply (simp add: offset_poly_eq_0_iff)
done
definition
"psize p = (if p = 0 then 0 else Suc (degree p))"
lemma psize_eq_0_iff [simp]: "psize p = 0 \ p = 0"
unfolding psize_def by simp
lemma poly_offset: "\ q. psize q = psize p \ (\x. poly q (x::complex) = poly p (a + x))"
proof (intro exI conjI)
show "psize (offset_poly p a) = psize p"
unfolding psize_def
by (simp add: offset_poly_eq_0_iff degree_offset_poly)
show "\x. poly (offset_poly p a) x = poly p (a + x)"
by (simp add: poly_offset_poly)
qed
text{* An alternative useful formulation of completeness of the reals *}
lemma real_sup_exists: assumes ex: "\x. P x" and bz: "\z. \x. P x \ x < z"
shows "\(s::real). \y. (\x. P x \ y < x) \ y < s"
proof-
from ex bz obtain x Y where x: "P x" and Y: "\x. P x \ x < Y" by blast
from ex have thx:"\x. x \ Collect P" by blast
from bz have thY: "\Y. isUb UNIV (Collect P) Y"
by(auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def order_le_less)
from reals_complete[OF thx thY] obtain L where L: "isLub UNIV (Collect P) L"
by blast
from Y[OF x] have xY: "x < Y" .
from L have L': "\x. P x \ x \ L" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
from Y have Y': "\x. P x \ x \ Y"
apply (clarsimp, atomize (full)) by auto
from L Y' have "L \ Y" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
{fix y
{fix z assume z: "P z" "y < z"
from L' z have "y < L" by auto }
moreover
{assume yL: "y < L" "\z. P z \ \ y < z"
hence nox: "\z. P z \ y \ z" by auto
from nox L have "y \ L" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
with yL(1) have False by arith}
ultimately have "(\x. P x \ y < x) \ y < L" by blast}
thus ?thesis by blast
qed
subsection {* Fundamental theorem of algebra *}
lemma unimodular_reduce_norm:
assumes md: "cmod z = 1"
shows "cmod (z + 1) < 1 \ cmod (z - 1) < 1 \ cmod (z + ii) < 1 \ cmod (z - ii) < 1"
proof-
obtain x y where z: "z = Complex x y " by (cases z, auto)
from md z have xy: "x^2 + y^2 = 1" by (simp add: cmod_def)
{assume C: "cmod (z + 1) \ 1" "cmod (z - 1) \ 1" "cmod (z + ii) \ 1" "cmod (z - ii) \ 1"
from C z xy have "2*x \ 1" "2*x \ -1" "2*y \ 1" "2*y \ -1"
by (simp_all add: cmod_def power2_eq_square algebra_simps)
hence "abs (2*x) \ 1" "abs (2*y) \ 1" by simp_all
hence "(abs (2 * x))^2 <= 1^2" "(abs (2 * y)) ^2 <= 1^2"
by - (rule power_mono, simp, simp)+
hence th0: "4*x^2 \ 1" "4*y^2 \ 1"
by (simp_all add: power2_abs power_mult_distrib)
from add_mono[OF th0] xy have False by simp }
thus ?thesis unfolding linorder_not_le[symmetric] by blast
qed
text{* Hence we can always reduce modulus of @{text "1 + b z^n"} if nonzero *}
lemma reduce_poly_simple:
assumes b: "b \ 0" and n: "n\0"
shows "\z. cmod (1 + b * z^n) < 1"
using n
proof(induct n rule: nat_less_induct)
fix n
assume IH: "\m 0 \ (\z. cmod (1 + b * z ^ m) < 1)" and n: "n \ 0"
let ?P = "\z n. cmod (1 + b * z ^ n) < 1"
{assume e: "even n"
hence "\m. n = 2*m" by presburger
then obtain m where m: "n = 2*m" by blast
from n m have "m\0" "m < n" by presburger+
with IH[rule_format, of m] obtain z where z: "?P z m" by blast
from z have "?P (csqrt z) n" by (simp add: m power_mult csqrt)
hence "\z. ?P z n" ..}
moreover
{assume o: "odd n"
have th0: "cmod (complex_of_real (cmod b) / b) = 1"
using b by (simp add: norm_divide)
from o have "\m. n = Suc (2*m)" by presburger+
then obtain m where m: "n = Suc (2*m)" by blast
from unimodular_reduce_norm[OF th0] o
have "\v. cmod (complex_of_real (cmod b) / b + v^n) < 1"
apply (cases "cmod (complex_of_real (cmod b) / b + 1) < 1", rule_tac x="1" in exI, simp)
apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1", rule_tac x="-1" in exI, simp add: diff_minus)
apply (cases "cmod (complex_of_real (cmod b) / b + ii) < 1")
apply (cases "even m", rule_tac x="ii" in exI, simp add: m power_mult)
apply (rule_tac x="- ii" in exI, simp add: m power_mult)
apply (cases "even m", rule_tac x="- ii" in exI, simp add: m power_mult diff_minus)
apply (rule_tac x="ii" in exI, simp add: m power_mult diff_minus)
done
then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1" by blast
let ?w = "v / complex_of_real (root n (cmod b))"
from odd_real_root_pow[OF o, of "cmod b"]
have th1: "?w ^ n = v^n / complex_of_real (cmod b)"
by (simp add: power_divide complex_of_real_power)
have th2:"cmod (complex_of_real (cmod b) / b) = 1" using b by (simp add: norm_divide)
hence th3: "cmod (complex_of_real (cmod b) / b) \ 0" by simp
have th4: "cmod (complex_of_real (cmod b) / b) *
cmod (1 + b * (v ^ n / complex_of_real (cmod b)))
< cmod (complex_of_real (cmod b) / b) * 1"
apply (simp only: norm_mult[symmetric] right_distrib)
using b v by (simp add: th2)
from mult_less_imp_less_left[OF th4 th3]
have "?P ?w n" unfolding th1 .
hence "\z. ?P z n" .. }
ultimately show "\z. ?P z n" by blast
qed
text{* Bolzano-Weierstrass type property for closed disc in complex plane. *}
lemma metric_bound_lemma: "cmod (x - y) <= \Re x - Re y\ + \Im x - Im y\"
using real_sqrt_sum_squares_triangle_ineq[of "Re x - Re y" 0 0 "Im x - Im y" ]
unfolding cmod_def by simp
lemma bolzano_weierstrass_complex_disc:
assumes r: "\n. cmod (s n) \ r"
shows "\f z. subseq f \ (\e >0. \N. \n \ N. cmod (s (f n) - z) < e)"
proof-
from seq_monosub[of "Re o s"]
obtain f g where f: "subseq f" "monoseq (\n. Re (s (f n)))"
unfolding o_def by blast
from seq_monosub[of "Im o s o f"]
obtain g where g: "subseq g" "monoseq (\n. Im (s(f(g n))))" unfolding o_def by blast
let ?h = "f o g"
from r[rule_format, of 0] have rp: "r \ 0" using norm_ge_zero[of "s 0"] by arith
have th:"\n. r + 1 \ \ Re (s n)\"
proof
fix n
from abs_Re_le_cmod[of "s n"] r[rule_format, of n] show "\Re (s n)\ \ r + 1" by arith
qed
have conv1: "convergent (\n. Re (s ( f n)))"
apply (rule Bseq_monoseq_convergent)
apply (simp add: Bseq_def)
apply (rule exI[where x= "r + 1"])
using th rp apply simp
using f(2) .
have th:"\n. r + 1 \ \ Im (s n)\"
proof
fix n
from abs_Im_le_cmod[of "s n"] r[rule_format, of n] show "\Im (s n)\ \ r + 1" by arith
qed
have conv2: "convergent (\n. Im (s (f (g n))))"
apply (rule Bseq_monoseq_convergent)
apply (simp add: Bseq_def)
apply (rule exI[where x= "r + 1"])
using th rp apply simp
using g(2) .
from conv1[unfolded convergent_def] obtain x where "LIMSEQ (\n. Re (s (f n))) x"
by blast
hence x: "\r>0. \n0. \n\n0. \ Re (s (f n)) - x \ < r"
unfolding LIMSEQ_iff real_norm_def .
from conv2[unfolded convergent_def] obtain y where "LIMSEQ (\n. Im (s (f (g n)))) y"
by blast
hence y: "\r>0. \n0. \n\n0. \ Im (s (f (g n))) - y \ < r"
unfolding LIMSEQ_iff real_norm_def .
let ?w = "Complex x y"
from f(1) g(1) have hs: "subseq ?h" unfolding subseq_def by auto
{fix e assume ep: "e > (0::real)"
hence e2: "e/2 > 0" by simp
from x[rule_format, OF e2] y[rule_format, OF e2]
obtain N1 N2 where N1: "\n\N1. \Re (s (f n)) - x\ < e / 2" and N2: "\n\N2. \Im (s (f (g n))) - y\ < e / 2" by blast
{fix n assume nN12: "n \ N1 + N2"
hence nN1: "g n \ N1" and nN2: "n \ N2" using seq_suble[OF g(1), of n] by arith+
from add_strict_mono[OF N1[rule_format, OF nN1] N2[rule_format, OF nN2]]
have "cmod (s (?h n) - ?w) < e"
using metric_bound_lemma[of "s (f (g n))" ?w] by simp }
hence "\N. \n\N. cmod (s (?h n) - ?w) < e" by blast }
with hs show ?thesis by blast
qed
text{* Polynomial is continuous. *}
lemma poly_cont:
assumes ep: "e > 0"
shows "\d >0. \w. 0 < cmod (w - z) \ cmod (w - z) < d \ cmod (poly p w - poly p z) < e"
proof-
obtain q where q: "degree q = degree p" "\x. poly q x = poly p (z + x)"
proof
show "degree (offset_poly p z) = degree p"
by (rule degree_offset_poly)
show "\x. poly (offset_poly p z) x = poly p (z + x)"
by (rule poly_offset_poly)
qed
{fix w
note q(2)[of "w - z", simplified]}
note th = this
show ?thesis unfolding th[symmetric]
proof(induct q)
case 0 thus ?case using ep by auto
next
case (pCons c cs)
from poly_bound_exists[of 1 "cs"]
obtain m where m: "m > 0" "\z. cmod z \ 1 \ cmod (poly cs z) \ m" by blast
from ep m(1) have em0: "e/m > 0" by (simp add: field_simps)
have one0: "1 > (0::real)" by arith
from real_lbound_gt_zero[OF one0 em0]
obtain d where d: "d >0" "d < 1" "d < e / m" by blast
from d(1,3) m(1) have dm: "d*m > 0" "d*m < e"
by (simp_all add: field_simps mult_pos_pos)
show ?case
proof(rule ex_forward[OF real_lbound_gt_zero[OF one0 em0]], clarsimp simp add: norm_mult)
fix d w
assume H: "d > 0" "d < 1" "d < e/m" "w\z" "cmod (w-z) < d"
hence d1: "cmod (w-z) \ 1" "d \ 0" by simp_all
from H(3) m(1) have dme: "d*m < e" by (simp add: field_simps)
from H have th: "cmod (w-z) \ d" by simp
from mult_mono[OF th m(2)[OF d1(1)] d1(2) norm_ge_zero] dme
show "cmod (w - z) * cmod (poly cs (w - z)) < e" by simp
qed
qed
qed
text{* Hence a polynomial attains minimum on a closed disc
in the complex plane. *}
lemma poly_minimum_modulus_disc:
"\z. \w. cmod w \ r \ cmod (poly p z) \ cmod (poly p w)"
proof-
{assume "\ r \ 0" hence ?thesis unfolding linorder_not_le
apply -
apply (rule exI[where x=0])
apply auto
apply (subgoal_tac "cmod w < 0")
apply simp
apply arith
done }
moreover
{assume rp: "r \ 0"
from rp have "cmod 0 \ r \ cmod (poly p 0) = - (- cmod (poly p 0))" by simp
hence mth1: "\x z. cmod z \ r \ cmod (poly p z) = - x" by blast
{fix x z
assume H: "cmod z \ r" "cmod (poly p z) = - x" "\x < 1"
hence "- x < 0 " by arith
with H(2) norm_ge_zero[of "poly p z"] have False by simp }
then have mth2: "\z. \x. (\z. cmod z \ r \ cmod (poly p z) = - x) \ x < z" by blast
from real_sup_exists[OF mth1 mth2] obtain s where
s: "\y. (\x. (\z. cmod z \ r \ cmod (poly p z) = - x) \ y < x) \(y < s)" by blast
let ?m = "-s"
{fix y
from s[rule_format, of "-y"] have
"(\z x. cmod z \ r \ -(- cmod (poly p z)) < y) \ ?m < y"
unfolding minus_less_iff[of y ] equation_minus_iff by blast }
note s1 = this[unfolded minus_minus]
from s1[of ?m] have s1m: "\z x. cmod z \ r \ cmod (poly p z) \ ?m"
by auto
{fix n::nat
from s1[rule_format, of "?m + 1/real (Suc n)"]
have "\z. cmod z \ r \ cmod (poly p z) < - s + 1 / real (Suc n)"
by simp}
hence th: "\n. \z. cmod z \ r \ cmod (poly p z) < - s + 1 / real (Suc n)" ..
from choice[OF th] obtain g where
g: "\n. cmod (g n) \ r" "\n. cmod (poly p (g n)) e>0. \N. \n\N. cmod (g (f n) - z) < e"
by blast
{fix w
assume wr: "cmod w \ r"
let ?e = "\cmod (poly p z) - ?m\"
{assume e: "?e > 0"
hence e2: "?e/2 > 0" by simp
from poly_cont[OF e2, of z p] obtain d where
d: "d>0" "\w. 0 cmod(w - z) < d \ cmod(poly p w - poly p z) < ?e/2" by blast
{fix w assume w: "cmod (w - z) < d"
have "cmod(poly p w - poly p z) < ?e / 2"
using d(2)[rule_format, of w] w e by (cases "w=z", simp_all)}
note th1 = this
from fz(2)[rule_format, OF d(1)] obtain N1 where
N1: "\n\N1. cmod (g (f n) - z) < d" by blast
from reals_Archimedean2[of "2/?e"] obtain N2::nat where
N2: "2/?e < real N2" by blast
have th2: "cmod(poly p (g(f(N1 + N2))) - poly p z) < ?e/2"
using N1[rule_format, of "N1 + N2"] th1 by simp
{fix a b e2 m :: real
have "a < e2 \ abs(b - m) < e2 \ 2 * e2 <= abs(b - m) + a
==> False" by arith}
note th0 = this
have ath:
"\m x e. m <= x \ x < m + e ==> abs(x - m::real) < e" by arith
from s1m[OF g(1)[rule_format]]
have th31: "?m \ cmod(poly p (g (f (N1 + N2))))" .
from seq_suble[OF fz(1), of "N1+N2"]
have th00: "real (Suc (N1+N2)) \ real (Suc (f (N1+N2)))" by simp
have th000: "0 \ (1::real)" "(1::real) \ 1" "real (Suc (N1+N2)) > 0"
using N2 by auto
from frac_le[OF th000 th00] have th00: "?m +1 / real (Suc (f (N1 + N2))) \ ?m + 1 / real (Suc (N1 + N2))" by simp
from g(2)[rule_format, of "f (N1 + N2)"]
have th01:"cmod (poly p (g (f (N1 + N2)))) < - s + 1 / real (Suc (f (N1 + N2)))" .
from order_less_le_trans[OF th01 th00]
have th32: "cmod(poly p (g (f (N1 + N2)))) < ?m + (1/ real(Suc (N1 + N2)))" .
from N2 have "2/?e < real (Suc (N1 + N2))" by arith
with e2 less_imp_inverse_less[of "2/?e" "real (Suc (N1 + N2))"]
have "?e/2 > 1/ real (Suc (N1 + N2))" by (simp add: inverse_eq_divide)
with ath[OF th31 th32]
have thc1:"\cmod(poly p (g (f (N1 + N2)))) - ?m\< ?e/2" by arith
have ath2: "\(a::real) b c m. \a - b\ <= c ==> \b - m\ <= \a - m\