(* File: Vieta.thy Author: Manuel Eberl (TU München) Vieta's formulas expressing the coefficients of a factored univariate polynomial in terms of its roots. *) section ‹Vieta's Formulas› theory Vieta imports "HOL-Library.FuncSet" "HOL-Computational_Algebra.Computational_Algebra" begin subsection ‹Auxiliary material› lemma card_vimage_inter: assumes inj: "inj_on f A" and subset: "X ⊆ f ` A" shows "card (f -` X ∩ A) = card X" proof - have "card (f -` X ∩ A) = card (f ` (f -` X ∩ A))" by (subst card_image) (auto intro!: inj_on_subset[OF inj]) also have "f ` (f -` X ∩ A) = X" using assms by auto finally show ?thesis . qed lemma bij_betw_image_fixed_card_subset: assumes "inj_on f A" shows "bij_betw (λX. f ` X) {X. X ⊆ A ∧ card X = k} {X. X ⊆ f ` A ∧ card X = k}" using assms inj_on_subset[OF assms] by (intro bij_betwI[of _ _ _ "λX. f -` X ∩ A"]) (auto simp: card_image card_vimage_inter) lemma image_image_fixed_card_subset: assumes "inj_on f A" shows "(λX. f ` X) ` {X. X ⊆ A ∧ card X = k} = {X. X ⊆ f ` A ∧ card X = k}" using bij_betw_imp_surj_on[OF bij_betw_image_fixed_card_subset[OF assms, of k]] . lemma prod_uminus: "(∏x∈A. -f x :: 'a :: comm_ring_1) = (-1) ^ card A * (∏x∈A. f x)" by (induction A rule: infinite_finite_induct) (auto simp: algebra_simps) theorem prod_sum_PiE: fixes f :: "'a ⇒ 'b ⇒ 'c :: comm_semiring_1" assumes finite: "finite A" and finite: "⋀x. x ∈ A ⟹ finite (B x)" shows "(∏x∈A. ∑y∈B x. f x y) = (∑g∈PiE A B. ∏x∈A. f x (g x))" using assms proof (induction A rule: finite_induct) case empty thus ?case by auto next case (insert x A) have "(∑g∈Pi⇩_{E}(insert x A) B. ∏x∈insert x A. f x (g x)) = (∑g∈Pi⇩_{E}(insert x A) B. f x (g x) * (∏x'∈A. f x' (g x')))" using insert by simp also have "(λg. ∏x'∈A. f x' (g x')) = (λg. ∏x'∈A. f x' (if x' = x then undefined else g x'))" using insert by (intro ext prod.cong) auto also have "(∑g∈Pi⇩_{E}(insert x A) B. f x (g x) * … g) = (∑(y,g)∈B x × Pi⇩_{E}A B. f x y * (∏x'∈A. f x' (g x')))" using insert.prems insert.hyps by (intro sum.reindex_bij_witness[of _ "λ(y,g). g(x := y)" "λg. (g x, g(x := undefined))"]) (auto simp: PiE_def extensional_def) also have "… = (∑y∈B x. ∑g∈Pi⇩_{E}A B. f x y * (∏x'∈A. f x' (g x')))" by (subst sum.cartesian_product) auto also have "… = (∑y∈B x. f x y) * (∑g∈Pi⇩_{E}A B. ∏x'∈A. f x' (g x'))" using insert by (subst sum.swap) (simp add: sum_distrib_left sum_distrib_right) also have "(∑g∈Pi⇩_{E}A B. ∏x'∈A. f x' (g x')) = (∏x∈A. ∑y∈B x. f x y)" using insert.prems by (intro insert.IH [symmetric]) auto also have "(∑y∈B x. f x y) * … = (∏x∈insert x A. ∑y∈B x. f x y)" using insert.hyps by simp finally show ?case .. qed corollary prod_add: fixes f1 f2 :: "'a ⇒ 'c :: comm_semiring_1" assumes finite: "finite A" shows "(∏x∈A. f1 x + f2 x) = (∑X∈Pow A. (∏x∈X. f1 x) * (∏x∈A-X. f2 x))" proof - have "(∏x∈A. f1 x + f2 x) = (∑g∈A →⇩_{E}UNIV. ∏x∈A. if g x then f1 x else f2 x)" using prod_sum_PiE[of A "λ_. UNIV :: bool set" "λx y. if y then f1 x else f2 x"] assms by (simp_all add: UNIV_bool add_ac) also have "… = (∑X∈Pow A. ∏x∈A. if x ∈ X then f1 x else f2 x)" by (intro sum.reindex_bij_witness [of _ "λX x. if x ∈ A then x ∈ X else undefined" "λP. {x∈A. P x}"]) auto also have "… = (∑X∈Pow A. (∏x∈X. f1 x) * (∏x∈A-X. f2 x))" proof (intro sum.cong refl, goal_cases) case (1 X) let ?f = "λx. if x ∈ X then f1 x else f2 x" have "prod f1 X * prod f2 (A - X) = prod ?f X * prod ?f (A - X)" by (intro arg_cong2[of _ _ _ _ "(*)"] prod.cong) auto also have "… = prod ?f (X ∪ (A - X))" using 1 by (subst prod.union_disjoint) (auto intro: finite_subset[OF _ finite]) also have "X ∪ (A - X) = A" using 1 by auto finally show ?case .. qed finally show ?thesis . qed corollary prod_diff1: fixes f1 f2 :: "'a ⇒ 'c :: comm_ring_1" assumes finite: "finite A" shows "(∏x∈A. f1 x - f2 x) = (∑X∈Pow A. (-1) ^ card X * (∏x∈X. f2 x) * (∏x∈A-X. f1 x))" proof - have "(∏x∈A. f1 x - f2 x) = (∏x∈A. -f2 x + f1 x)" by simp also have "… = (∑X∈Pow A. (∏x∈X. - f2 x) * prod f1 (A - X))" by (rule prod_add) fact+ also have "… = (∑X∈Pow A. (-1) ^ card X * (∏x∈X. f2 x) * prod f1 (A - X))" by (simp add: prod_uminus) finally show ?thesis . qed corollary prod_diff2: fixes f1 f2 :: "'a ⇒ 'c :: comm_ring_1" assumes finite: "finite A" shows "(∏x∈A. f1 x - f2 x) = (∑X∈Pow A. (-1) ^ (card A - card X) * (∏x∈X. f1 x) * (∏x∈A-X. f2 x))" proof - have "(∏x∈A. f1 x - f2 x) = (∏x∈A. f1 x + (-f2 x))" by simp also have "… = (∑X∈Pow A. (∏x∈X. f1 x) * (∏x∈A-X. -f2 x))" by (rule prod_add) fact+ also have "… = (∑X∈Pow A. (-1) ^ card (A - X) * (∏x∈X. f1 x) * (∏x∈A-X. f2 x))" by (simp add: prod_uminus mult_ac) also have "… = (∑X∈Pow A. (-1) ^ (card A - card X) * (∏x∈X. f1 x) * (∏x∈A-X. f2 x))" using finite_subset[OF _ assms] by (intro sum.cong refl, subst card_Diff_subset) auto finally show ?thesis . qed subsection ‹Main proofs› text ‹ Our goal is to determine the coefficients of some fully factored polynomial $p(X) = c (X - x_1) \ldots (X - x_n)$ in terms of the $x_i$. It is clear that it is sufficient to consider monic polynomials (i.e. $c = 1$), since the general case follows easily from this one. We start off by expanding the product over the linear factors: › lemma poly_from_roots: fixes f :: "'a ⇒ 'b :: comm_ring_1" assumes fin: "finite A" shows "(∏x∈A. [:-f x, 1:]) = (∑X∈Pow A. monom ((-1) ^ card X * (∏x∈X. f x)) (card (A - X)))" proof - have "(∏x∈A. [:-f x, 1:]) = (∏x∈A. [:0, 1:] - [:f x:])" by simp also have "… = (∑X∈Pow A. (-1) ^ card X * (∏x∈X. [:f x:]) * monom 1 (card (A - X)))" using fin by (subst prod_diff1) (auto simp: monom_altdef mult_ac) also have "… = (∑X∈Pow A. monom ((-1) ^ card X * (∏x∈X. f x)) (card (A - X)))" proof (intro sum.cong refl, goal_cases) case (1 X) have "(-1 :: 'b poly) ^ card X = [:(-1) ^ card X:]" by (induction X rule: infinite_finite_induct) (auto simp: one_pCons algebra_simps) moreover have "(∏x∈X. [:f x:]) = [:∏x∈X. f x:]" by (induction X rule: infinite_finite_induct) auto ultimately show ?case by (simp add: smult_monom) qed finally show ?thesis . qed text ‹ Comparing coefficients yields Vieta's formula: › theorem coeff_poly_from_roots: fixes f :: "'a ⇒ 'b :: comm_ring_1" assumes fin: "finite A" and k: "k ≤ card A" shows "coeff (∏x∈A. [:-f x, 1:]) k = (-1) ^ (card A - k) * (∑X | X ⊆ A ∧ card X = card A - k. (∏x∈X. f x))" proof - have "(∏x∈A. [:-f x, 1:]) = (∑X∈Pow A. monom ((-1) ^ card X * (∏x∈X. f x)) (card (A - X)))" by (intro poly_from_roots fin) also have "coeff … k = (∑X | X ⊆ A ∧ card X = card A - k. (-1) ^ (card A - k) * (∏x∈X. f x))" unfolding coeff_sum coeff_monom using finite_subset[OF _ fin] k card_mono[OF fin] by (intro sum.mono_neutral_cong_right) (auto simp: card_Diff_subset) also have "… = (-1) ^ (card A - k) * (∑X | X ⊆ A ∧ card X = card A - k. (∏x∈X. f x))" by (simp add: sum_distrib_left) finally show ?thesis . qed text ‹ If the roots are all distinct, we can get the following alternative representation: › corollary coeff_poly_from_roots': fixes f :: "'a ⇒ 'b :: comm_ring_1" assumes fin: "finite A" and inj: "inj_on f A" and k: "k ≤ card A" shows "coeff (∏x∈A. [:-f x, 1:]) k = (-1) ^ (card A - k) * (∑X | X ⊆ f ` A ∧ card X = card A - k. ∏X)" proof - have "coeff (∏x∈A. [:-f x, 1:]) k = (-1) ^ (card A - k) * (∑X | X ⊆ A ∧ card X = card A - k. (∏x∈X. f x))" by (intro coeff_poly_from_roots assms) also have "(∑X | X ⊆ A ∧ card X = card A - k. (∏x∈X. f x)) = (∑X | X ⊆ A ∧ card X = card A - k. ∏(f`X))" by (intro sum.cong refl, subst prod.reindex) (auto intro: inj_on_subset[OF inj]) also have "… = (∑X ∈ (λX. f`X) ` {X. X ⊆ A ∧ card X = card A - k}. ∏X)" by (subst sum.reindex) (auto intro!: inj_on_image inj_on_subset[OF inj]) also have "(λX. f ` X) ` {X. X ⊆ A ∧ card X = card A - k} = {X. X ⊆ f ` A ∧ card X = card A - k}" by (intro image_image_fixed_card_subset inj) finally show ?thesis . qed end