Theory Vieta
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