--- a/src/HOL/Complex_Analysis/Meromorphic.thy Wed May 21 20:13:43 2025 +0200
+++ b/src/HOL/Complex_Analysis/Meromorphic.thy Wed May 21 21:48:42 2025 +0200
@@ -155,6 +155,21 @@
by (intro is_pole_cong eventually_remove_sings_eq_at refl zorder_cong
zor_poly_cong has_laurent_expansion_cong' tendsto_cong assms)+
+lemma remove_sings_has_laurent_expansion [laurent_expansion_intros]:
+ assumes "f has_laurent_expansion F"
+ shows "remove_sings f has_laurent_expansion F"
+proof -
+ have "remove_sings f has_laurent_expansion F \<longleftrightarrow> f has_laurent_expansion F"
+ proof (rule has_laurent_expansion_cong)
+ have "isolated_singularity_at f 0"
+ using assms by (metis has_laurent_expansion_isolated_0)
+ thus "eventually (\<lambda>x. remove_sings f x = f x) (at 0)"
+ by (rule eventually_remove_sings_eq_at)
+ qed auto
+ with assms show ?thesis
+ by simp
+qed
+
lemma get_all_poles_from_remove_sings:
fixes f:: "complex \<Rightarrow> complex"
defines "ff\<equiv>remove_sings f"
@@ -242,7 +257,7 @@
using False remove_sings_eqI by auto
qed simp
-lemma remove_sings_analytic_on:
+lemma remove_sings_analytic_at:
assumes "isolated_singularity_at f z" "f \<midarrow>z\<rightarrow> c"
shows "remove_sings f analytic_on {z}"
proof -
@@ -270,6 +285,24 @@
using A(1,2) analytic_at by blast
qed
+lemma remove_sings_analytic_on:
+ assumes "f analytic_on A"
+ shows "remove_sings f analytic_on A"
+proof -
+ from assms obtain B where B: "open B" "A \<subseteq> B" "f holomorphic_on B"
+ by (metis analytic_on_holomorphic)
+ have "remove_sings f holomorphic_on B \<longleftrightarrow> f holomorphic_on B"
+ proof (rule holomorphic_cong)
+ fix z assume "z \<in> B"
+ have "f analytic_on {z}"
+ using \<open>z \<in> B\<close> B holomorphic_on_imp_analytic_at by blast
+ thus "remove_sings f z = f z"
+ by (rule remove_sings_at_analytic)
+ qed auto
+ thus ?thesis
+ using B analytic_on_holomorphic by blast
+qed
+
lemma residue_remove_sings [simp]:
assumes "isolated_singularity_at f z"
shows "residue (remove_sings f) z = residue f z"
@@ -1585,7 +1618,7 @@
from assms(1) have "f \<midarrow>z\<rightarrow> 0"
by (simp add: isolated_zero_def)
with assms(2) have "remove_sings f analytic_on {z}"
- by (intro remove_sings_analytic_on)
+ by (intro remove_sings_analytic_at)
hence "zorder (remove_sings f) z > 0"
using assms by (intro zorder_isolated_zero_pos) auto
thus ?thesis
@@ -1714,7 +1747,7 @@
shows "zorder f z = 0"
proof -
have "remove_sings f analytic_on {z}"
- using assms meromorphic_at_iff not_essential_def remove_sings_analytic_on by blast
+ using assms meromorphic_at_iff not_essential_def remove_sings_analytic_at by blast
moreover from this and assms have "remove_sings f z \<noteq> 0"
using isolated_zero_def meromorphic_at_iff non_zero_neighbour remove_sings_eq_0_iff by blast
moreover have "frequently (\<lambda>z. remove_sings f z \<noteq> 0) (at z)"
--- a/src/HOL/Computational_Algebra/Polynomial.thy Wed May 21 20:13:43 2025 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy Wed May 21 21:48:42 2025 +0200
@@ -2042,6 +2042,42 @@
ultimately show False by linarith
qed
+lemma poly_eqI_degree_lead_coeff:
+ fixes p q :: "'a :: {comm_ring_1, ring_no_zero_divisors} poly"
+ assumes "poly.coeff p n = poly.coeff q n" "card A \<ge> n" "degree p \<le> n" "degree q \<le> n"
+ assumes "\<And>z. z \<in> A \<Longrightarrow> poly p z = poly q z"
+ shows "p = q"
+proof (rule ccontr)
+ assume "p \<noteq> q"
+
+ have "n > 0"
+ proof (rule ccontr)
+ assume "\<not>(n > 0)"
+ thus False
+ using assms \<open>p \<noteq> q\<close> by (auto elim!: degree_eq_zeroE)
+ qed
+
+ have "n \<le> card A"
+ by fact
+ also have "card A \<le> card {x. poly (p - q) x = 0}"
+ by (intro card_mono poly_roots_finite) (use \<open>p \<noteq> q\<close> assms in auto)
+ also have "card {x. poly (p - q) x = 0} \<le> degree (p - q)"
+ by (rule card_poly_roots_bound) (use \<open>p \<noteq> q\<close> in auto)
+ also have "degree (p - q) < n"
+ proof (intro degree_lessI allI impI)
+ fix k assume "k \<ge> n"
+ show "poly.coeff (p - q) k = 0"
+ proof (cases "k = n")
+ case False
+ hence "poly.coeff p k = 0" "poly.coeff q k = 0"
+ using assms \<open>k \<ge> n\<close> by (auto simp: coeff_eq_0)
+ thus ?thesis
+ by simp
+ qed (use assms in auto)
+ qed (use \<open>n > 0\<close> in auto)
+ finally show False
+ by simp
+qed
subsubsection \<open>Order of polynomial roots\<close>