# HG changeset patch # User paulson # Date 1757105599 -3600 # Node ID d4ce097aa59fccdafeb30d2f5ec07ae66ef13645 # Parent 3edaac4585e850057d384f542117a54fc78ed6cb Some lemmas moved in from Winding_Number_Eval diff -r 3edaac4585e8 -r d4ce097aa59f src/HOL/Computational_Algebra/Polynomial.thy --- a/src/HOL/Computational_Algebra/Polynomial.thy Wed Sep 03 21:15:31 2025 +0100 +++ b/src/HOL/Computational_Algebra/Polynomial.thy Fri Sep 05 21:53:19 2025 +0100 @@ -706,6 +706,10 @@ "last (coeffs p) = lead_coeff p" if "p \ 0" using that by (simp add: coeffs_def) +lemma lead_coeff_list_def: + "lead_coeff p = (if coeffs p=[] then 0 else last (coeffs p))" + by (simp add: last_coeffs_eq_coeff_degree) + subsection \Addition and subtraction\ @@ -1333,6 +1337,11 @@ by (auto simp: assms map_poly_def nth_default_def coeffs_def not_less Suc_le_eq coeff_eq_0 simp del: upt_Suc) +lemma lead_coeff_map_poly_nz: + assumes "f (lead_coeff p) \ 0" "f 0 = 0" + shows "lead_coeff (map_poly f p) = f (lead_coeff p)" + by (metis (no_types, lifting) antisym assms coeff_0 coeff_map_poly le_degree leading_coeff_0_iff) + lemma coeffs_map_poly [code abstract]: "coeffs (map_poly f p) = strip_while ((=) 0) (map f (coeffs p))" by (simp add: map_poly_def) @@ -1460,8 +1469,43 @@ by (induction A rule: infinite_finite_induct) (auto simp: mult_to_poly mult_ac) lemma poly_map_poly_cnj [simp]: "poly (map_poly cnj p) x = cnj (poly p (cnj x))" - by (induction p) (auto simp: map_poly_pCons) - + using complex_cnj_cnj poly_cnj by force + +lemma map_poly_degree_eq: + assumes "f (lead_coeff p) \ 0" + shows "degree (map_poly f p) = degree p" + using assms + unfolding map_poly_def degree_eq_length_coeffs coeffs_Poly lead_coeff_list_def + by (metis (full_types) last_conv_nth_default length_map no_trailing_unfold nth_default_coeffs_eq + nth_default_map_eq strip_while_idem) + +lemma map_poly_degree_less: + assumes "f (lead_coeff p) =0" "degree p\0" + shows "degree (map_poly f p) < degree p" +proof - + have "length (coeffs p) >1" + using \degree p\0\ by (simp add: degree_eq_length_coeffs) + then obtain xs x where xs_def:"coeffs p=xs@[x]" "length xs>0" + by (metis One_nat_def add_0 append_Nil length_greater_0_conv list.size(4) nat_neq_iff not_less_zero rev_exhaust) + have "f x=0" using assms(1) by (simp add: lead_coeff_list_def xs_def(1)) + have "degree (map_poly f p) = length (strip_while ((=) 0) (map f (xs@[x]))) - 1" + unfolding map_poly_def degree_eq_length_coeffs coeffs_Poly + by (subst xs_def,auto) + also have "\ = length (strip_while ((=) 0) (map f xs)) - 1" + using \f x=0\ by simp + also have "\ \ length xs -1" + using length_strip_while_le by (metis diff_le_mono length_map) + also have "\ < length (xs@[x]) - 1" + using xs_def(2) by auto + also have "\ = degree p" + unfolding degree_eq_length_coeffs xs_def by simp + finally show ?thesis . +qed + +lemma map_poly_degree_leq[simp]: + shows "degree (map_poly f p) \ degree p" + unfolding map_poly_def degree_eq_length_coeffs + by (metis coeffs_Poly diff_le_mono length_map length_strip_while_le) subsection \Conversions\ @@ -2567,6 +2611,13 @@ lemma pcompose_0': "pcompose p 0 = [:coeff p 0:]" by (induct p) (auto simp add: pcompose_pCons) +lemma pcompose_coeff_0: + "coeff (pcompose p q) 0 = poly p (coeff q 0)" + by (metis poly_0_coeff_0 poly_pcompose) + +lemma pcompose_pCons_0: "pcompose p [:a:] = [:poly p a:]" + by (metis (no_types, lifting) coeff_pCons_0 pcompose_0' pcompose_assoc poly_0_coeff_0 poly_pcompose) + lemma degree_pcompose: "degree (pcompose p q) = degree p * degree q" for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" proof (induct p) @@ -6384,6 +6435,140 @@ qed (use \n > 0\ in \simp_all add: p_eq degree_power_eq\) qed +subsection \Polynomials and limits\ + +lemma filterlim_poly_at_infinity: + fixes p::"'a::real_normed_field poly" + assumes "degree p>0" + shows "filterlim (poly p) at_infinity at_infinity" +using assms +proof (induct p) + case 0 + then show ?case by auto +next + case (pCons a p) + have ?case when "degree p=0" + proof - + obtain c where c_def:"p=[:c:]" using \degree p = 0\ degree_eq_zeroE by blast + then have "c\0" using \0 < degree (pCons a p)\ by auto + then show ?thesis unfolding c_def + apply (auto intro!:tendsto_add_filterlim_at_infinity) + apply (subst mult.commute) + by (auto intro!:tendsto_mult_filterlim_at_infinity filterlim_ident) + qed + moreover have ?case when "degree p\0" + proof - + have "filterlim (poly p) at_infinity at_infinity" + using that by (auto intro:pCons) + then show ?thesis + by (auto intro!:tendsto_add_filterlim_at_infinity filterlim_at_infinity_times filterlim_ident) + qed + ultimately show ?case by auto +qed + +lemma poly_divide_tendsto_aux: + fixes p::"'a::real_normed_field poly" + shows "((\x. poly p x/x^(degree p)) \ lead_coeff p) at_infinity" +proof (induct p) + case 0 + then show ?case by (auto intro:tendsto_eq_intros) +next + case (pCons a p) + have ?case when "p=0" + using that by auto + moreover have ?case when "p\0" + proof - + define g where "g=(\x. a/(x*x^degree p))" + define f where "f=(\x. poly p x/x^degree p)" + have "\\<^sub>Fx in at_infinity. poly (pCons a p) x / x ^ degree (pCons a p) = g x + f x" + proof (rule eventually_at_infinityI[of 1]) + fix x::'a assume "norm x\1" + then have "x\0" by auto + then show "poly (pCons a p) x / x ^ degree (pCons a p) = g x + f x" + using that unfolding g_def f_def by (auto simp add:field_simps) + qed + moreover have "((\x. g x+f x) \ lead_coeff (pCons a p)) at_infinity" + proof - + have "(g \ 0) at_infinity" + unfolding g_def using filterlim_poly_at_infinity[of "monom 1 (Suc (degree p))"] + apply (auto intro!:tendsto_intros tendsto_divide_0 simp add: degree_monom_eq) + apply (subst filterlim_cong[where g="poly (monom 1 (Suc (degree p)))"]) + by (auto simp add:poly_monom) + moreover have "(f \ lead_coeff (pCons a p)) at_infinity" + using pCons \p\0\ unfolding f_def by auto + ultimately show ?thesis by (auto intro:tendsto_eq_intros) + qed + ultimately show ?thesis by (auto dest:tendsto_cong) + qed + ultimately show ?case by auto +qed + + +lemma filterlim_power_at_infinity: + assumes "n\0" + shows "filterlim (\x::'a::real_normed_field. x^n) at_infinity at_infinity" + using filterlim_poly_at_infinity[of "monom 1 n"] assms + by (simp add: filterlim_ident filterlim_power_at_infinity) + +lemma poly_divide_tendsto_0_at_infinity: + fixes p::"'a::real_normed_field poly" + assumes "degree p > degree q" + shows "((\x. poly q x / poly p x) \ 0 ) at_infinity" +proof - + define pp where "pp \ (\x. x^(degree p) / poly p x)" + define qq where "qq \ (\x. poly q x/x^(degree q))" + define dd where "dd \ (\x::'a. 1/x^(degree p - degree q))" + have "\\<^sub>Fx in at_infinity. poly q x / poly p x = qq x * pp x * dd x" + proof (rule eventually_at_infinityI[of 1]) + fix x::'a assume "norm x\1" + then have "x\0" by auto + then show "poly q x / poly p x = qq x * pp x * dd x" + unfolding qq_def pp_def dd_def using assms + by (auto simp add:field_simps divide_simps power_diff) + qed + moreover have "((\x. qq x * pp x * dd x) \ 0) at_infinity" + proof - + have "(qq \ lead_coeff q) at_infinity" + unfolding qq_def using poly_divide_tendsto_aux[of q] . + moreover have "(pp \ 1/lead_coeff p) at_infinity" + proof - + have "p\0" using assms by auto + then show ?thesis + unfolding pp_def using poly_divide_tendsto_aux[of p] + apply (drule_tac tendsto_inverse) + by (auto simp add:inverse_eq_divide) + qed + moreover have "(dd \ 0) at_infinity" + unfolding dd_def + apply (rule tendsto_divide_0) + by (auto intro!: filterlim_power_at_infinity simp add:assms) + ultimately show ?thesis by (auto intro:tendsto_eq_intros) + qed + ultimately show ?thesis by (auto dest:tendsto_cong) +qed + +lemma poly_eventually_not_zero: + fixes p::"real poly" + assumes "p\0" + shows "eventually (\x. poly p x \ 0) at_infinity" +proof (rule eventually_at_infinityI[of "Max (norm ` {x. poly p x = 0}) + 1"]) + fix x::real assume \
: "Max (norm ` {x. poly p x = 0}) + 1 \ norm x" + have False when "poly p x = 0" + proof - + define S where "S=norm `{x. poly p x = 0}" + have "norm x\S" + using that unfolding S_def by auto + moreover have "finite S" + using \p\0\ poly_roots_finite unfolding S_def by blast + ultimately have "norm x\Max S" + by simp + moreover have "Max S + 1 \ norm x" + using \
unfolding S_def by simp + ultimately show False by argo + qed + then show "poly p x \ 0" by auto +qed + no_notation cCons (infixr \##\ 65) end