(* Author: René Thiemann Akihisa Yamada License: BSD *) section ‹Complex Roots of Real Valued Polynomials› text ‹We provide conversion functions between polynomials over the real and the complex numbers, and prove that the complex roots of real-valued polynomial always come in conjugate pairs. We further show that also the order of the complex conjugate roots is identical. As a consequence, we derive that every real-valued polynomial can be factored into real factors of degree at most 2, and we prove that every polynomial over the reals with odd degree has a real root.› theory Complex_Roots_Real_Poly imports "HOL-Computational_Algebra.Fundamental_Theorem_Algebra" Polynomial_Factorization.Order_Polynomial Polynomial_Factorization.Explicit_Roots Polynomial_Interpolation.Ring_Hom_Poly begin interpretation of_real_poly_hom: map_poly_idom_hom complex_of_real.. lemma real_poly_real_coeff: assumes "set (coeffs p) ⊆ ℝ" shows "coeff p x ∈ ℝ" proof - have "coeff p x ∈ range (coeff p)" by auto from this[unfolded range_coeff] assms show ?thesis by auto qed lemma complex_conjugate_root: assumes real: "set (coeffs p) ⊆ ℝ" and rt: "poly p c = 0" shows "poly p (cnj c) = 0" proof - let ?c = "cnj c" { fix x have "coeff p x ∈ ℝ" by (rule real_poly_real_coeff[OF real]) hence "cnj (coeff p x) = coeff p x" by (cases "coeff p x", auto) } note cnj_coeff = this have "poly p ?c = poly (∑x≤degree p. monom (coeff p x) x) ?c" unfolding poly_as_sum_of_monoms .. also have "… = (∑x≤degree p . coeff p x * cnj (c ^ x))" unfolding poly_sum poly_monom complex_cnj_power .. also have "… = (∑x≤degree p . cnj (coeff p x * c ^ x))" unfolding complex_cnj_mult cnj_coeff .. also have "… = cnj (∑x≤degree p . coeff p x * c ^ x)" unfolding cnj_sum .. also have "(∑x≤degree p . coeff p x * c ^ x) = poly (∑x≤degree p. monom (coeff p x) x) c" unfolding poly_sum poly_monom .. also have "… = 0" unfolding poly_as_sum_of_monoms rt .. also have "cnj 0 = 0" by simp finally show ?thesis . qed context fixes p :: "complex poly" assumes coeffs: "set (coeffs p) ⊆ ℝ" begin lemma map_poly_Re_poly: fixes x :: real shows "poly (map_poly Re p) x = poly p (of_real x)" proof - have id: "map_poly (of_real o Re) p = p" by (rule map_poly_idI, insert coeffs, auto) show ?thesis unfolding arg_cong[OF id, of poly, symmetric] by (subst map_poly_map_poly[symmetric], auto) qed lemma map_poly_Re_coeffs: "coeffs (map_poly Re p) = map Re (coeffs p)" proof (rule coeffs_map_poly) have "lead_coeff p ∈ range (coeff p)" by auto hence x: "lead_coeff p ∈ ℝ" using coeffs by (auto simp: range_coeff) show "(Re (lead_coeff p) = 0) = (p = 0)" using of_real_Re[OF x] by auto qed lemma map_poly_Re_0: "map_poly Re p = 0 ⟹ p = 0" using map_poly_Re_coeffs by auto end lemma real_poly_add: assumes "set (coeffs p) ⊆ ℝ" "set (coeffs q) ⊆ ℝ" shows "set (coeffs (p + q)) ⊆ ℝ" proof - define pp where "pp = coeffs p" define qq where "qq = coeffs q" show ?thesis using assms unfolding coeffs_plus_eq_plus_coeffs pp_def[symmetric] qq_def[symmetric] by (induct pp qq rule: plus_coeffs.induct, auto simp: cCons_def) qed lemma real_poly_sum: assumes "⋀ x. x ∈ S ⟹ set (coeffs (f x)) ⊆ ℝ" shows "set (coeffs (sum f S)) ⊆ ℝ" using assms proof (induct S rule: infinite_finite_induct) case (insert x S) hence id: "sum f (insert x S) = f x + sum f S" by auto show ?case unfolding id by (rule real_poly_add[OF _ insert(3)], insert insert, auto) qed auto lemma real_poly_smult: fixes p :: "'a :: {idom,real_algebra_1} poly" assumes "c ∈ ℝ" "set (coeffs p) ⊆ ℝ" shows "set (coeffs (smult c p)) ⊆ ℝ" using assms by (auto simp: coeffs_smult) lemma real_poly_pCons: assumes "c ∈ ℝ" "set (coeffs p) ⊆ ℝ" shows "set (coeffs (pCons c p)) ⊆ ℝ" using assms by (auto simp: cCons_def) lemma real_poly_mult: fixes p :: "'a :: {idom,real_algebra_1} poly" assumes p: "set (coeffs p) ⊆ ℝ" and q: "set (coeffs q) ⊆ ℝ" shows "set (coeffs (p * q)) ⊆ ℝ" using p proof (induct p) case (pCons a p) show ?case unfolding mult_pCons_left by (intro real_poly_add real_poly_smult real_poly_pCons pCons(2) q, insert pCons(1,3), auto simp: cCons_def if_splits) qed simp lemma real_poly_power: fixes p :: "'a :: {idom,real_algebra_1} poly" assumes p: "set (coeffs p) ⊆ ℝ" shows "set (coeffs (p ^ n)) ⊆ ℝ" proof (induct n) case (Suc n) from real_poly_mult[OF p this] show ?case by simp qed simp lemma real_poly_prod: fixes f :: "'a ⇒ 'b :: {idom,real_algebra_1} poly" assumes "⋀ x. x ∈ S ⟹ set (coeffs (f x)) ⊆ ℝ" shows "set (coeffs (prod f S)) ⊆ ℝ" using assms proof (induct S rule: infinite_finite_induct) case (insert x S) hence id: "prod f (insert x S) = f x * prod f S" by auto show ?case unfolding id by (rule real_poly_mult[OF _ insert(3)], insert insert, auto) qed auto lemma real_poly_uminus: assumes "set (coeffs p) ⊆ ℝ" shows "set (coeffs (-p)) ⊆ ℝ" using assms unfolding coeffs_uminus by auto lemma real_poly_minus: assumes "set (coeffs p) ⊆ ℝ" "set (coeffs q) ⊆ ℝ" shows "set (coeffs (p - q)) ⊆ ℝ" using assms unfolding diff_conv_add_uminus by (intro real_poly_uminus real_poly_add, auto) lemma fixes p :: "'a :: real_field poly" assumes p: "set (coeffs p) ⊆ ℝ" and *: "set (coeffs q) ⊆ ℝ" shows real_poly_div: "set (coeffs (q div p)) ⊆ ℝ" and real_poly_mod: "set (coeffs (q mod p)) ⊆ ℝ" proof (atomize(full), insert *, induct q) case 0 thus ?case by auto next case (pCons a q) from pCons(1,3) have a: "a ∈ ℝ" and q: "set (coeffs q) ⊆ ℝ" by auto note res = pCons show ?case proof (cases "p = 0") case True with res pCons(3) show ?thesis by auto next case False from pCons have IH: "set (coeffs (q div p)) ⊆ ℝ" "set (coeffs (q mod p)) ⊆ ℝ" by auto define c where "c = coeff (pCons a (q mod p)) (degree p) / coeff p (degree p)" { have "coeff (pCons a (q mod p)) (degree p) ∈ ℝ" by (rule real_poly_real_coeff, insert IH a, intro real_poly_pCons) moreover have "coeff p (degree p) ∈ ℝ" by (rule real_poly_real_coeff[OF p]) ultimately have "c ∈ ℝ" unfolding c_def by simp } note c = this from False have r: "pCons a q div p = pCons c (q div p)" and s: "pCons a q mod p = pCons a (q mod p) - smult c p" unfolding c_def div_pCons_eq mod_pCons_eq by simp_all show ?thesis unfolding r s using a p c IH by (intro conjI real_poly_pCons real_poly_minus real_poly_smult) qed qed lemma real_poly_factor: fixes p :: "'a :: real_field poly" assumes "set (coeffs (p * q)) ⊆ ℝ" "set (coeffs p) ⊆ ℝ" "p ≠ 0" shows "set (coeffs q) ⊆ ℝ" proof - have "q = p * q div p" using ‹p ≠ 0› by simp hence id: "coeffs q = coeffs (p * q div p)" by simp show ?thesis unfolding id by (rule real_poly_div, insert assms, auto) qed lemma complex_conjugate_order: assumes real: "set (coeffs p) ⊆ ℝ" "p ≠ 0" shows "order (cnj c) p = order c p" proof - define n where "n = degree p" have "degree p ≤ n" unfolding n_def by auto thus ?thesis using assms proof (induct n arbitrary: p) case (0 p) { fix x have "order x p ≤ degree p" by (rule order_degree[OF 0(3)]) hence "order x p = 0" using 0 by auto } thus ?case by simp next case (Suc m p) note order = order[OF ‹p ≠ 0›] let ?c = "cnj c" show ?case proof (cases "poly p c = 0") case True note rt1 = this from complex_conjugate_root[OF Suc(3) True] have rt2: "poly p ?c = 0" . show ?thesis proof (cases "c ∈ ℝ") case True hence "?c = c" by (cases c, auto) thus ?thesis by auto next case False hence neq: "?c ≠ c" by (simp add: Reals_cnj_iff) let ?fac1 = "[: -c, 1 :]" let ?fac2 = "[: -?c, 1 :]" let ?fac = "?fac1 * ?fac2" from rt1 have "?fac1 dvd p" unfolding poly_eq_0_iff_dvd . from this[unfolded dvd_def] obtain q where p: "p = ?fac1 * q" by auto from rt2[unfolded p poly_mult] neq have "poly q ?c = 0" by auto hence "?fac2 dvd q" unfolding poly_eq_0_iff_dvd . from this[unfolded dvd_def] obtain r where q: "q = ?fac2 * r" by auto have p: "p = ?fac * r" unfolding p q by algebra from ‹p ≠ 0› have nz: "?fac1 ≠ 0" "?fac2 ≠ 0" "?fac ≠ 0" "r ≠ 0" unfolding p by auto have id: "?fac = [: ?c * c, - (?c + c), 1 :]" by simp have cfac: "coeffs ?fac = [ ?c * c, - (?c + c), 1 ]" unfolding id by simp have cfac: "set (coeffs ?fac) ⊆ ℝ" unfolding cfac by (cases c, auto simp: Reals_cnj_iff) have "degree p = degree ?fac + degree r" unfolding p by (rule degree_mult_eq, insert nz, auto) also have "degree ?fac = degree ?fac1 + degree ?fac2" by (rule degree_mult_eq, insert nz, auto) finally have "degree p = 2 + degree r" by simp with Suc have deg: "degree r ≤ m" by auto from real_poly_factor[OF Suc(3)[unfolded p] cfac] nz have "set (coeffs r) ⊆ ℝ" by auto from Suc(1)[OF deg this ‹r ≠ 0›] have IH: "order ?c r = order c r" . { fix cc have "order cc p = order cc ?fac + order cc r" using ‹p ≠ 0› unfolding p by (rule order_mult) also have "order cc ?fac = order cc ?fac1 + order cc ?fac2" by (rule order_mult, rule nz) also have "order cc ?fac1 = (if cc = c then 1 else 0)" unfolding order_linear' by simp also have "order cc ?fac2 = (if cc = ?c then 1 else 0)" unfolding order_linear' by simp finally have "order cc p = (if cc = c then 1 else 0) + (if cc = cnj c then 1 else 0) + order cc r" . } note order = this show ?thesis unfolding order IH by auto qed next case False note rt1 = this { assume "poly p ?c = 0" from complex_conjugate_root[OF Suc(3) this] rt1 have False by auto } hence rt2: "poly p ?c ≠ 0" by auto from rt1 rt2 show ?thesis unfolding order_root by simp qed qed qed lemma map_poly_of_real_Re: assumes "set (coeffs p) ⊆ ℝ" shows "map_poly of_real (map_poly Re p) = p" by (subst map_poly_map_poly, force+, rule map_poly_idI, insert assms, auto) lemma map_poly_Re_of_real: "map_poly Re (map_poly of_real p) = p" by (subst map_poly_map_poly, force+, rule map_poly_idI, auto) lemma map_poly_Re_mult: assumes p: "set (coeffs p) ⊆ ℝ" and q: "set (coeffs q) ⊆ ℝ" shows "map_poly Re (p * q) = map_poly Re p * map_poly Re q" proof - let ?r = "map_poly Re" let ?c = "map_poly complex_of_real" have "?r (p * q) = ?r (?c (?r p) * ?c (?r q))" unfolding map_poly_of_real_Re[OF p] map_poly_of_real_Re[OF q] by simp also have "?c (?r p) * ?c (?r q) = ?c (?r p * ?r q)" by (simp add: hom_distribs) also have "?r … = ?r p * ?r q" unfolding map_poly_Re_of_real .. finally show ?thesis . qed lemma map_poly_Re_power: assumes p: "set (coeffs p) ⊆ ℝ" shows "map_poly Re (p^n) = (map_poly Re p)^n" proof (induct n) case (Suc n) let ?r = "map_poly Re" have "?r (p^Suc n) = ?r (p * p^n)" by simp also have "… = ?r p * ?r (p^n)" by (rule map_poly_Re_mult[OF p real_poly_power[OF p]]) also have "?r (p^n) = (?r p)^n" by (rule Suc) finally show ?case by simp qed simp lemma real_degree_2_factorization_exists_complex: fixes p :: "complex poly" assumes pR: "set (coeffs p) ⊆ ℝ" shows "∃ qs. p = prod_list qs ∧ (∀ q ∈ set qs. set (coeffs q) ⊆ ℝ ∧ degree q ≤ 2)" proof - obtain n where "degree p = n" by auto thus ?thesis using pR proof (induct n arbitrary: p rule: less_induct) case (less n p) hence pR: "set (coeffs p) ⊆ ℝ" by auto show ?case proof (cases "n ≤ 2") case True thus ?thesis using pR by (intro exI[of _ "[p]"], insert less(2), auto) next case False hence degp: "degree p ≥ 2" using less(2) by auto hence "¬ constant (poly p)" by (simp add: constant_degree) from fundamental_theorem_of_algebra[OF this] obtain x where x: "poly p x = 0" by auto from x have dvd: "[: -x, 1 :] dvd p" using poly_eq_0_iff_dvd by blast have "∃ f. f dvd p ∧ set (coeffs f) ⊆ ℝ ∧ 1 ≤ degree f ∧ degree f ≤ 2" proof (cases "x ∈ ℝ") case True with dvd show ?thesis by (intro exI[of _ "[: -x, 1:]"], auto) next case False let ?x = "cnj x" let ?a = "?x * x" let ?b = "- ?x - x" from complex_conjugate_root[OF pR x] have xx: "poly p ?x = 0" by auto from False have diff: "x ≠ ?x" by (simp add: Reals_cnj_iff) from dvd obtain r where p: "p = [: -x, 1 :] * r" unfolding dvd_def by auto from xx[unfolded this] diff have "poly r ?x = 0" by simp hence "[: -?x, 1 :] dvd r" using poly_eq_0_iff_dvd by blast then obtain s where r: "r = [: -?x, 1 :] * s" unfolding dvd_def by auto have "p = ([: -x, 1:] * [: -?x, 1 :]) * s" unfolding p r by algebra also have "[: -x, 1:] * [: -?x, 1 :] = [: ?a, ?b, 1 :]" by simp finally have "[: ?a, ?b, 1 :] dvd p" unfolding dvd_def by auto moreover have "?a ∈ ℝ" by (simp add: Reals_cnj_iff) moreover have "?b ∈ ℝ" by (simp add: Reals_cnj_iff) ultimately show ?thesis by (intro exI[of _ "[:?a,?b,1:]"], auto) qed then obtain f where dvd: "f dvd p" and fR: "set (coeffs f) ⊆ ℝ" and degf: "1 ≤ degree f" "degree f ≤ 2" by auto from dvd obtain r where p: "p = f * r" unfolding dvd_def by auto from degp have p0: "p ≠ 0" by auto with p have f0: "f ≠ 0" and r0: "r ≠ 0" by auto from real_poly_factor[OF pR[unfolded p] fR f0] have rR: "set (coeffs r) ⊆ ℝ" . have deg: "degree p = degree f + degree r" unfolding p by (rule degree_mult_eq[OF f0 r0]) with degf less(2) have degr: "degree r < n" by auto from less(1)[OF this refl rR] obtain qs where IH: "r = prod_list qs" "(∀q∈set qs. set (coeffs q) ⊆ ℝ ∧ degree q ≤ 2)" by auto from IH(1) have p: "p = prod_list (f # qs)" unfolding p by auto with IH(2) fR degf show ?thesis by (intro exI[of _ "f # qs"], auto) qed qed qed lemma real_degree_2_factorization_exists: fixes p :: "real poly" shows "∃ qs. p = prod_list qs ∧ (∀ q ∈ set qs. degree q ≤ 2)" proof - let ?cp = "map_poly complex_of_real" let ?rp = "map_poly Re" let ?p = "?cp p" have "set (coeffs ?p) ⊆ ℝ" by auto from real_degree_2_factorization_exists_complex[OF this] obtain qs where p: "?p = prod_list qs" and qs: "⋀ q. q ∈ set qs ⟹ set (coeffs q) ⊆ ℝ ∧ degree q ≤ 2" by auto have p: "p = ?rp (prod_list qs)" unfolding arg_cong[OF p, of ?rp, symmetric] by (subst map_poly_map_poly, force, rule sym, rule map_poly_idI, auto) from qs have "∃ rs. prod_list qs = ?cp (prod_list rs) ∧ (∀ r ∈ set rs. degree r ≤ 2)" proof (induct qs) case Nil show ?case by (auto intro!: exI[of _ Nil]) next case (Cons q qs) then obtain rs where qs: "prod_list qs = ?cp (prod_list rs)" and rs: "⋀ q. q∈set rs ⟹ degree q ≤ 2" by force+ from Cons(2)[of q] have q: "set (coeffs q) ⊆ ℝ" and dq: "degree q ≤ 2" by auto define r where "r = ?rp q" have q: "q = ?cp r" unfolding r_def by (subst map_poly_map_poly, force, rule sym, rule map_poly_idI, insert q, auto) have dr: "degree r ≤ 2" using dq unfolding q by (simp add: degree_map_poly) show ?case by (rule exI[of _ "r # rs"], unfold prod_list.Cons qs q, insert dr rs, auto simp: hom_distribs) qed then obtain rs where id: "prod_list qs = ?cp (prod_list rs)" and deg: "∀ r ∈ set rs. degree r ≤ 2" by auto show ?thesis unfolding p id by (intro exI, rule conjI[OF _ deg], subst map_poly_map_poly, force, rule map_poly_idI, auto) qed lemma odd_degree_imp_real_root: assumes "odd (degree p)" shows "∃ x. poly p x = (0 :: real)" proof - from real_degree_2_factorization_exists[of p] obtain qs where id: "p = prod_list qs" and qs: "⋀ q. q ∈ set qs ⟹ degree q ≤ 2" by auto show ?thesis using assms qs unfolding id proof (induct qs) case (Cons q qs) from Cons(3)[of q] have dq: "degree q ≤ 2" by auto show ?case proof (cases "degree q = 1") case True from roots1[OF this] show ?thesis by auto next case False with dq have deg: "degree q = 0 ∨ degree q = 2" by arith from Cons(2) have "q * prod_list qs ≠ 0" by fastforce hence "q ≠ 0" "prod_list qs ≠ 0" by auto from degree_mult_eq[OF this] have "degree (prod_list (q # qs)) = degree q + degree (prod_list qs)" by simp from Cons(2)[unfolded this] deg have "odd (degree (prod_list qs))" by auto from Cons(1)[OF this Cons(3)] obtain x where "poly (prod_list qs) x = 0" by auto thus ?thesis by auto qed qed simp qed end