--- a/src/HOL/Analysis/Derivative.thy Mon Apr 21 08:24:58 2025 +0200
+++ b/src/HOL/Analysis/Derivative.thy Fri Apr 18 10:58:16 2025 +0200
@@ -1742,7 +1742,7 @@
using islimpt_approachable_real[of x S] not_bot
by (auto simp add: trivial_limit_within)
then show ?thesis
- using eq_iff_diff_eq_0 by fastforce
+ using eq_iff_diff_eq_0 by (metis add.commute diff_add_cancel)
qed
qed (use f' f'' in \<open>auto simp: has_vector_derivative_def\<close>)
then show ?thesis
@@ -1777,6 +1777,17 @@
by (intro vector_derivative_unique_within[OF not_bot vector_derivative_works[THEN iffD1] y])
(auto simp: differentiable_def has_vector_derivative_def)
+lemma vector_derivative_translate [simp]:
+ "vector_derivative ((+) z \<circ> g) (at x within A) = vector_derivative g (at x within A)"
+proof -
+ have "(((+) z \<circ> g) has_vector_derivative g') (at x within A)"
+ if "(g has_vector_derivative g') (at x within A)" for g :: "real \<Rightarrow> 'a" and z g'
+ unfolding o_def using that by (auto intro!: derivative_eq_intros)
+ from this[of g _ z] this[of "\<lambda>x. z + g x" _ "-z"] show ?thesis
+ unfolding vector_derivative_def
+ by (intro arg_cong[where f = Eps] ext) (auto simp: o_def algebra_simps)
+qed
+
lemma deriv_of_real [simp]:
"at x within A \<noteq> bot \<Longrightarrow> vector_derivative of_real (at x within A) = 1"
by (auto intro!: vector_derivative_within derivative_eq_intros)
@@ -2256,6 +2267,43 @@
definition\<^marker>\<open>tag important\<close> deriv :: "('a \<Rightarrow> 'a::real_normed_field) \<Rightarrow> 'a \<Rightarrow> 'a" where
"deriv f x \<equiv> SOME D. DERIV f x :> D"
+lemma deriv_shift_0: "deriv f z = deriv (f \<circ> (\<lambda>x. z + x)) 0"
+proof -
+ have *: "(f \<circ> (+) z has_field_derivative D) (at z')"
+ if "(f has_field_derivative D) (at (z + z'))" for D z z' and f :: "'a \<Rightarrow> 'a"
+ proof -
+ have "(f \<circ> (+) z has_field_derivative D * 1) (at z')"
+ by (rule DERIV_chain that derivative_eq_intros refl)+ auto
+ thus ?thesis by simp
+ qed
+ have "(\<lambda>D. (f has_field_derivative D) (at z)) = (\<lambda> D. (f \<circ> (+) z has_field_derivative D) (at 0))"
+ using *[of f _ z 0] *[of "f \<circ> (+) z" _ "-z" z] by (intro ext iffI) (auto simp: o_def)
+ thus ?thesis
+ by (simp add: deriv_def)
+qed
+
+lemma deriv_shift_0': "NO_MATCH 0 z \<Longrightarrow> deriv f z = deriv (f \<circ> (\<lambda>x. z + x)) 0"
+ by (rule deriv_shift_0)
+
+lemma higher_deriv_shift_0: "(deriv ^^ n) f z = (deriv ^^ n) (f \<circ> (\<lambda>x. z + x)) 0"
+proof (induction n arbitrary: f)
+ case (Suc n)
+ have "(deriv ^^ Suc n) f z = (deriv ^^ n) (deriv f) z"
+ by (subst funpow_Suc_right) auto
+ also have "\<dots> = (deriv ^^ n) (\<lambda>x. deriv f (z + x)) 0"
+ by (subst Suc) (auto simp: o_def)
+ also have "\<dots> = (deriv ^^ n) (\<lambda>x. deriv (\<lambda>xa. f (z + x + xa)) 0) 0"
+ by (subst deriv_shift_0) (auto simp: o_def)
+ also have "(\<lambda>x. deriv (\<lambda>xa. f (z + x + xa)) 0) = deriv (\<lambda>x. f (z + x))"
+ by (rule ext) (simp add: deriv_shift_0' o_def add_ac)
+ also have "(deriv ^^ n) \<dots> 0 = (deriv ^^ Suc n) (f \<circ> (\<lambda>x. z + x)) 0"
+ by (subst funpow_Suc_right) (auto simp: o_def)
+ finally show ?case .
+qed auto
+
+lemma higher_deriv_shift_0': "NO_MATCH 0 z \<Longrightarrow> (deriv ^^ n) f z = (deriv ^^ n) (f \<circ> (\<lambda>x. z + x)) 0"
+ by (rule higher_deriv_shift_0)
+
lemma DERIV_imp_deriv: "DERIV f x :> f' \<Longrightarrow> deriv f x = f'"
unfolding deriv_def by (metis some_equality DERIV_unique)
--- a/src/HOL/Analysis/FPS_Convergence.thy Mon Apr 21 08:24:58 2025 +0200
+++ b/src/HOL/Analysis/FPS_Convergence.thy Fri Apr 18 10:58:16 2025 +0200
@@ -61,6 +61,9 @@
lemma open_eball [simp, intro]: "open (eball z r)"
by (cases r) auto
+lemma connected_eball [intro]: "connected (eball (z :: 'a :: real_normed_vector) r)"
+ by (cases r) auto
+
subsection \<open>Basic properties of convergent power series\<close>
--- a/src/HOL/Analysis/Infinite_Products.thy Mon Apr 21 08:24:58 2025 +0200
+++ b/src/HOL/Analysis/Infinite_Products.thy Fri Apr 18 10:58:16 2025 +0200
@@ -846,11 +846,16 @@
by (metis convergent_mult_const_iff \<open>C \<noteq> 0\<close> cong cf convergent_LIMSEQ_iff convergent_prod_iff_convergent convergent_prod_imp_convergent g)
next
assume cg: "convergent_prod g"
- have "\<exists>a. C * a \<noteq> 0 \<and> (\<lambda>n. prod g {..n}) \<longlonglongrightarrow> a"
- by (metis (no_types) \<open>C \<noteq> 0\<close> cg convergent_prod_iff_nz_lim divide_eq_0_iff g nonzero_mult_div_cancel_right)
+ have **: "eventually (\<lambda>n. prod g {..n} = prod f {..n} / C) sequentially"
+ using * by eventually_elim (use \<open>C \<noteq> 0\<close> in auto)
+ from cg and g have "\<not> (\<lambda>n. prod g {..n}) \<longlonglongrightarrow> 0"
+ by simp
+ then have "\<not> (\<lambda>n. prod f {..n}) \<longlonglongrightarrow> 0"
+ using ** \<open>C \<noteq> 0\<close> filterlim_cong by fastforce
then show "convergent_prod f"
- using "*" tendsto_mult_left filterlim_cong
- by (fastforce simp add: convergent_prod_iff_nz_lim f)
+ by (metis \<open>C \<noteq> 0\<close> cg convergent_LIMSEQ_iff
+ convergent_mult_const_iff convergent_prod_iff_convergent
+ convergent_prod_imp_convergent f local.cong)
qed
qed
@@ -953,8 +958,14 @@
lemma convergent_prod_If_finite[simp, intro]:
fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
- shows "finite {r. P r} \<Longrightarrow> convergent_prod (\<lambda>r. if P r then f r else 1)"
- using convergent_prod_def has_prod_If_finite has_prod_def by fastforce
+ assumes "finite {r. P r}"
+ shows "convergent_prod (\<lambda>r. if P r then f r else 1)"
+proof -
+ have "(\<lambda>r. if P r then f r else 1) has_prod (\<Prod>r | P r. f r)"
+ by (rule has_prod_If_finite) fact
+ thus ?thesis
+ by (meson convergent_prod_def has_prod_def)
+qed
lemma has_prod_single:
fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
--- a/src/HOL/Analysis/Infinite_Sum.thy Mon Apr 21 08:24:58 2025 +0200
+++ b/src/HOL/Analysis/Infinite_Sum.thy Fri Apr 18 10:58:16 2025 +0200
@@ -27,6 +27,7 @@
Elementary_Topology
"HOL-Library.Extended_Nonnegative_Real"
"HOL-Library.Complex_Order"
+ "HOL-Computational_Algebra.Formal_Power_Series"
begin
subsection \<open>Definition and syntax\<close>
@@ -3578,5 +3579,79 @@
shows "(f has_sum S) A \<Longrightarrow> ((\<lambda>x. -f x) has_sum (-S)) A"
using has_sum_cmult_right[of f A S "-1"] by simp
+
+subsection \<open>Infinite sums of formal power series\<close>
+
+text \<open>
+ Consequently, a family $(f_x)_{x\in A}$ of formal power series sums to a series $s$ iff for
+ any $n\geq 0$, the set $A_n = \{x\in A \mid [X^n]\,f_x \neq 0\}$ is finite and
+ $[X^n]\,s = \sum_{x\in A_n} [X^n]\,f_x$.
+
+ The first condition can be rephrased as follows: for any $n\geq 0$, for all but finitely many
+ $x$, the series $f_x$ has subdegree ${>}\,n$.
+\<close>
+lemma has_sum_fpsI:
+ assumes "\<And>n. finite {x\<in>A. fps_nth (F x) n \<noteq> 0}"
+ assumes "\<And>n. fps_nth S n = (\<Sum>x | x \<in> A \<and> fps_nth (F x) n \<noteq> 0. fps_nth (F x) n)"
+ shows "(F has_sum S) A"
+ unfolding has_sum_def
+proof (rule tendsto_fpsI)
+ fix n :: nat
+ define B where "B = {x\<in>A. fps_nth (F x) n \<noteq> 0}"
+ from assms(1) have [intro]: "finite B"
+ unfolding B_def by auto
+ moreover have "B \<subseteq> A"
+ by (auto simp: B_def)
+ ultimately have "eventually (\<lambda>X. finite X \<and> B \<subseteq> X \<and> X \<subseteq> A) (finite_subsets_at_top A)"
+ by (subst eventually_finite_subsets_at_top) blast
+ thus "eventually (\<lambda>X. fps_nth (\<Sum>x\<in>X. F x) n = fps_nth S n) (finite_subsets_at_top A)"
+ proof eventually_elim
+ case (elim X)
+ have "fps_nth (\<Sum>x\<in>X. F x) n = (\<Sum>x\<in>X. fps_nth (F x) n)"
+ by (simp add: fps_sum_nth)
+ also have "\<dots> = (\<Sum>x\<in>B. fps_nth (F x) n)"
+ by (rule sum.mono_neutral_right) (use \<open>finite B\<close> \<open>B \<subseteq> A\<close> elim in \<open>auto simp: B_def\<close>)
+ also have "\<dots> = fps_nth S n"
+ using assms(2)[of n] by (simp add: B_def)
+ finally show "fps_nth (\<Sum>x\<in>X. F x) n = fps_nth S n" .
+ qed
+qed
+
+lemma has_sum_fpsD:
+ fixes F :: "'a \<Rightarrow> 'b :: ab_group_add fps"
+ assumes "(F has_sum S) A"
+ shows "finite {x\<in>A. fps_nth (F x) n \<noteq> 0}"
+ "fps_nth S n = (\<Sum>x | x \<in> A \<and> fps_nth (F x) n \<noteq> 0. fps_nth (F x) n)"
+proof -
+ from assms have "\<forall>\<^sub>F X in finite_subsets_at_top A. fps_nth (sum F X) k = fps_nth S k" for k
+ unfolding has_sum_def tendsto_fps_iff by blast
+ hence "\<forall>\<^sub>F X in finite_subsets_at_top A. fps_nth (sum F X) n = fps_nth S n"
+ by eventually_elim force
+ then obtain B where [intro, simp]: "finite B" and B: "B \<subseteq> A"
+ "\<And>X. finite X \<Longrightarrow> B \<subseteq> X \<Longrightarrow> X \<subseteq> A \<Longrightarrow> fps_nth (sum F X) n = fps_nth S n"
+ unfolding eventually_finite_subsets_at_top by metis
+
+ have subset: "{x\<in>A. fps_nth (F x) n \<noteq> 0} \<subseteq> B"
+ proof safe
+ fix x assume x: "x \<in> A" "fps_nth (F x) n \<noteq> 0"
+ have "fps_nth (sum F B) n = fps_nth S n"
+ by (rule B(2)) (use B(1) in auto)
+ moreover have "fps_nth (sum F (insert x B)) n = fps_nth S n"
+ by (rule B(2)) (use B(1) x in auto)
+ ultimately show "x \<in> B"
+ using x by (auto simp: sum.insert_if split: if_splits)
+ qed
+ thus finite: "finite {x\<in>A. fps_nth (F x) n \<noteq> 0}"
+ by (rule finite_subset) auto
+
+ have "fps_nth S n = fps_nth (\<Sum>x\<in>B. F x) n"
+ by (rule sym, rule B(2)) (use B(1) in auto)
+ also have "\<dots> = (\<Sum>x\<in>B. fps_nth (F x) n)"
+ by (simp add: fps_sum_nth)
+ also have "\<dots> = (\<Sum>x | x \<in> A \<and> fps_nth (F x) n \<noteq> 0. fps_nth (F x) n)"
+ by (rule sum.mono_neutral_right) (use subset B(1) in auto)
+ finally show "fps_nth S n = (\<Sum>x | x \<in> A \<and> fps_nth (F x) n \<noteq> 0. fps_nth (F x) n)" .
+qed
+
end
--- a/src/HOL/Complex_Analysis/Complex_Residues.thy Mon Apr 21 08:24:58 2025 +0200
+++ b/src/HOL/Complex_Analysis/Complex_Residues.thy Fri Apr 18 10:58:16 2025 +0200
@@ -52,6 +52,26 @@
with assms show ?thesis by simp
qed
+lemma residue_shift_0: "residue f z = residue (\<lambda>x. f (z + x)) 0"
+proof -
+ define Q where
+ "Q = (\<lambda>r f z \<epsilon>. (f has_contour_integral complex_of_real (2 * pi) * \<i> * r) (circlepath z \<epsilon>))"
+ define P where
+ "P = (\<lambda>r f z. \<exists>e>0. \<forall>\<epsilon>>0. \<epsilon> < e \<longrightarrow> Q r f z \<epsilon>)"
+ have path_eq: "circlepath (z - w) \<epsilon> = (+) (-w) \<circ> circlepath z \<epsilon>" for z w \<epsilon>
+ by (simp add: circlepath_def o_def part_circlepath_def algebra_simps)
+ have *: "P r f z" if "P r (\<lambda>x. f (x + w)) (z - w)" for r w f z
+ using that by (auto simp: P_def Q_def path_eq has_contour_integral_translate)
+ have "(SOME r. P r f z) = (SOME r. P r (\<lambda>x. f (z + x)) 0)"
+ using *[of _ f z z] *[of _ "\<lambda>x. f (z + x)" "-z"]
+ by (intro arg_cong[where f = Eps] ext iffI) (simp_all add: add_ac)
+ thus ?thesis
+ by (simp add: residue_def P_def Q_def)
+qed
+
+lemma residue_shift_0': "NO_MATCH 0 z \<Longrightarrow> residue f z = residue (\<lambda>x. f (z + x)) 0"
+ by (rule residue_shift_0)
+
lemma contour_integral_circlepath_eq:
assumes "open s" and f_holo:"f holomorphic_on (s-{z})" and "0<e1" "e1\<le>e2"
and e2_cball:"cball z e2 \<subseteq> s"
--- a/src/HOL/Complex_Analysis/Contour_Integration.thy Mon Apr 21 08:24:58 2025 +0200
+++ b/src/HOL/Complex_Analysis/Contour_Integration.thy Fri Apr 18 10:58:16 2025 +0200
@@ -68,6 +68,18 @@
using has_integral_unique
by (auto simp: has_contour_integral_def)
+lemma has_contour_integral_translate:
+ "(f has_contour_integral I) ((+) z \<circ> g) \<longleftrightarrow> ((\<lambda>x. f (x + z)) has_contour_integral I) g"
+ by (simp add: has_contour_integral_def add_ac)
+
+lemma contour_integrable_translate:
+ "f contour_integrable_on ((+) z \<circ> g) \<longleftrightarrow> (\<lambda>x. f (x + z)) contour_integrable_on g"
+ by (simp add: contour_integrable_on_def has_contour_integral_translate)
+
+lemma contour_integral_translate:
+ "contour_integral ((+) z \<circ> g) f = contour_integral g (\<lambda>x. f (x + z))"
+ by (simp add: contour_integral_def contour_integrable_translate has_contour_integral_translate)
+
lemma has_contour_integral_integrable: "(f has_contour_integral i) g \<Longrightarrow> f contour_integrable_on g"
using contour_integrable_on_def by blast
--- a/src/HOL/Complex_Analysis/Laurent_Convergence.thy Mon Apr 21 08:24:58 2025 +0200
+++ b/src/HOL/Complex_Analysis/Laurent_Convergence.thy Fri Apr 18 10:58:16 2025 +0200
@@ -4,80 +4,6 @@
begin
-instance fps :: (semiring_char_0) semiring_char_0
-proof
- show "inj (of_nat :: nat \<Rightarrow> 'a fps)"
- proof
- fix m n :: nat
- assume "of_nat m = (of_nat n :: 'a fps)"
- hence "fps_nth (of_nat m) 0 = (fps_nth (of_nat n) 0 :: 'a)"
- by (simp only: )
- thus "m = n"
- by simp
- qed
-qed
-
-instance fls :: (semiring_char_0) semiring_char_0
-proof
- show "inj (of_nat :: nat \<Rightarrow> 'a fls)"
- by (metis fls_regpart_of_nat injI of_nat_eq_iff)
-qed
-
-lemma fls_const_eq_0_iff [simp]: "fls_const c = 0 \<longleftrightarrow> c = 0"
- using fls_const_0 fls_const_nonzero by blast
-
-lemma fls_subdegree_add_eq1:
- assumes "f \<noteq> 0" "fls_subdegree f < fls_subdegree g"
- shows "fls_subdegree (f + g) = fls_subdegree f"
-proof (intro antisym)
- from assms have *: "fls_nth (f + g) (fls_subdegree f) \<noteq> 0"
- by auto
- from * show "fls_subdegree (f + g) \<le> fls_subdegree f"
- by (rule fls_subdegree_leI)
- from * have "f + g \<noteq> 0"
- using fls_nonzeroI by blast
- thus "fls_subdegree f \<le> fls_subdegree (f + g)"
- using assms(2) fls_plus_subdegree by force
-qed
-
-lemma fls_subdegree_add_eq2:
- assumes "g \<noteq> 0" "fls_subdegree g < fls_subdegree f"
- shows "fls_subdegree (f + g) = fls_subdegree g"
-proof (intro antisym)
- from assms have *: "fls_nth (f + g) (fls_subdegree g) \<noteq> 0"
- by auto
- from * show "fls_subdegree (f + g) \<le> fls_subdegree g"
- by (rule fls_subdegree_leI)
- from * have "f + g \<noteq> 0"
- using fls_nonzeroI by blast
- thus "fls_subdegree g \<le> fls_subdegree (f + g)"
- using assms(2) fls_plus_subdegree by force
-qed
-
-lemma fls_subdegree_diff_eq1:
- assumes "f \<noteq> 0" "fls_subdegree f < fls_subdegree g"
- shows "fls_subdegree (f - g) = fls_subdegree f"
- using fls_subdegree_add_eq1[of f "-g"] assms by simp
-
-lemma fls_subdegree_diff_eq2:
- assumes "g \<noteq> 0" "fls_subdegree g < fls_subdegree f"
- shows "fls_subdegree (f - g) = fls_subdegree g"
- using fls_subdegree_add_eq2[of "-g" f] assms by simp
-
-lemma nat_minus_fls_subdegree_plus_const_eq:
- "nat (-fls_subdegree (F + fls_const c)) = nat (-fls_subdegree F)"
-proof (cases "fls_subdegree F < 0")
- case True
- hence "fls_subdegree (F + fls_const c) = fls_subdegree F"
- by (intro fls_subdegree_add_eq1) auto
- thus ?thesis
- by simp
-next
- case False
- thus ?thesis
- by (auto simp: fls_subdegree_ge0I)
-qed
-
definition%important fls_conv_radius :: "complex fls \<Rightarrow> ereal" where
"fls_conv_radius f = fps_conv_radius (fls_regpart f)"
@@ -139,12 +65,6 @@
and eval_fps_of_int [simp]: "eval_fps (of_int m) z = of_int m"
by (simp_all flip: fps_of_nat fps_of_int)
-lemma fls_subdegree_numeral [simp]: "fls_subdegree (numeral n) = 0"
- by (metis fls_subdegree_of_nat of_nat_numeral)
-
-lemma fls_regpart_numeral [simp]: "fls_regpart (numeral n) = numeral n"
- by (metis fls_regpart_of_nat of_nat_numeral)
-
lemma fps_conv_radius_of_nat [simp]: "fps_conv_radius (of_nat n) = \<infinity>"
and fps_conv_radius_of_int [simp]: "fps_conv_radius (of_int m) = \<infinity>"
by (simp_all flip: fps_of_nat fps_of_int)
@@ -486,9 +406,6 @@
lemmas has_field_derivative_eval_fps' [derivative_intros] =
DERIV_chain2[OF has_field_derivative_eval_fps]
-lemma fps_deriv_fls_regpart: "fps_deriv (fls_regpart F) = fls_regpart (fls_deriv F)"
- by (intro fps_ext) (auto simp: add_ac)
-
(* TODO: generalise for nonneg subdegree *)
lemma has_field_derivative_eval_fls:
assumes "z \<in> eball 0 (fls_conv_radius f) - {0}"
@@ -1186,43 +1103,6 @@
shows "f has_fps_expansion fps_expansion f 0"
using assms has_fps_expansion_fps_expansion analytic_at by fast
-lemma deriv_shift_0: "deriv f z = deriv (f \<circ> (\<lambda>x. z + x)) 0"
-proof -
- have *: "(f \<circ> (+) z has_field_derivative D) (at z')"
- if "(f has_field_derivative D) (at (z + z'))" for D z z' and f :: "'a \<Rightarrow> 'a"
- proof -
- have "(f \<circ> (+) z has_field_derivative D * 1) (at z')"
- by (rule DERIV_chain that derivative_eq_intros refl)+ auto
- thus ?thesis by simp
- qed
- have "(\<lambda>D. (f has_field_derivative D) (at z)) = (\<lambda> D. (f \<circ> (+) z has_field_derivative D) (at 0))"
- using *[of f _ z 0] *[of "f \<circ> (+) z" _ "-z" z] by (intro ext iffI) (auto simp: o_def)
- thus ?thesis
- by (simp add: deriv_def)
-qed
-
-lemma deriv_shift_0': "NO_MATCH 0 z \<Longrightarrow> deriv f z = deriv (f \<circ> (\<lambda>x. z + x)) 0"
- by (rule deriv_shift_0)
-
-lemma higher_deriv_shift_0: "(deriv ^^ n) f z = (deriv ^^ n) (f \<circ> (\<lambda>x. z + x)) 0"
-proof (induction n arbitrary: f)
- case (Suc n)
- have "(deriv ^^ Suc n) f z = (deriv ^^ n) (deriv f) z"
- by (subst funpow_Suc_right) auto
- also have "\<dots> = (deriv ^^ n) (\<lambda>x. deriv f (z + x)) 0"
- by (subst Suc) (auto simp: o_def)
- also have "\<dots> = (deriv ^^ n) (\<lambda>x. deriv (\<lambda>xa. f (z + x + xa)) 0) 0"
- by (subst deriv_shift_0) (auto simp: o_def)
- also have "(\<lambda>x. deriv (\<lambda>xa. f (z + x + xa)) 0) = deriv (\<lambda>x. f (z + x))"
- by (rule ext) (simp add: deriv_shift_0' o_def add_ac)
- also have "(deriv ^^ n) \<dots> 0 = (deriv ^^ Suc n) (f \<circ> (\<lambda>x. z + x)) 0"
- by (subst funpow_Suc_right) (auto simp: o_def)
- finally show ?case .
-qed auto
-
-lemma higher_deriv_shift_0': "NO_MATCH 0 z \<Longrightarrow> (deriv ^^ n) f z = (deriv ^^ n) (f \<circ> (\<lambda>x. z + x)) 0"
- by (rule higher_deriv_shift_0)
-
lemma analytic_at_imp_has_fps_expansion:
assumes "f analytic_on {z}"
shows "(\<lambda>x. f (z + x)) has_fps_expansion fps_expansion f z"
@@ -1624,49 +1504,6 @@
by (simp add: field_simps)
qed
-lemma vector_derivative_translate [simp]:
- "vector_derivative ((+) z \<circ> g) (at x within A) = vector_derivative g (at x within A)"
-proof -
- have "(((+) z \<circ> g) has_vector_derivative g') (at x within A)"
- if "(g has_vector_derivative g') (at x within A)" for g :: "real \<Rightarrow> 'a" and z g'
- unfolding o_def using that by (auto intro!: derivative_eq_intros)
- from this[of g _ z] this[of "\<lambda>x. z + g x" _ "-z"] show ?thesis
- unfolding vector_derivative_def
- by (intro arg_cong[where f = Eps] ext) (auto simp: o_def algebra_simps)
-qed
-
-lemma has_contour_integral_translate:
- "(f has_contour_integral I) ((+) z \<circ> g) \<longleftrightarrow> ((\<lambda>x. f (x + z)) has_contour_integral I) g"
- by (simp add: has_contour_integral_def add_ac)
-
-lemma contour_integrable_translate:
- "f contour_integrable_on ((+) z \<circ> g) \<longleftrightarrow> (\<lambda>x. f (x + z)) contour_integrable_on g"
- by (simp add: contour_integrable_on_def has_contour_integral_translate)
-
-lemma contour_integral_translate:
- "contour_integral ((+) z \<circ> g) f = contour_integral g (\<lambda>x. f (x + z))"
- by (simp add: contour_integral_def contour_integrable_translate has_contour_integral_translate)
-
-lemma residue_shift_0: "residue f z = residue (\<lambda>x. f (z + x)) 0"
-proof -
- define Q where
- "Q = (\<lambda>r f z \<epsilon>. (f has_contour_integral complex_of_real (2 * pi) * \<i> * r) (circlepath z \<epsilon>))"
- define P where
- "P = (\<lambda>r f z. \<exists>e>0. \<forall>\<epsilon>>0. \<epsilon> < e \<longrightarrow> Q r f z \<epsilon>)"
- have path_eq: "circlepath (z - w) \<epsilon> = (+) (-w) \<circ> circlepath z \<epsilon>" for z w \<epsilon>
- by (simp add: circlepath_def o_def part_circlepath_def algebra_simps)
- have *: "P r f z" if "P r (\<lambda>x. f (x + w)) (z - w)" for r w f z
- using that by (auto simp: P_def Q_def path_eq has_contour_integral_translate)
- have "(SOME r. P r f z) = (SOME r. P r (\<lambda>x. f (z + x)) 0)"
- using *[of _ f z z] *[of _ "\<lambda>x. f (z + x)" "-z"]
- by (intro arg_cong[where f = Eps] ext iffI) (simp_all add: add_ac)
- thus ?thesis
- by (simp add: residue_def P_def Q_def)
-qed
-
-lemma residue_shift_0': "NO_MATCH 0 z \<Longrightarrow> residue f z = residue (\<lambda>x. f (z + x)) 0"
- by (rule residue_shift_0)
-
lemma has_laurent_expansion_residue_0:
assumes "f has_laurent_expansion F"
shows "residue f 0 = fls_residue F"
@@ -1768,9 +1605,6 @@
by (simp add: fls_conv_radius_altdef G_def)
qed
-lemma connected_eball [intro]: "connected (eball (z :: 'a :: real_normed_vector) r)"
- by (cases r) auto
-
lemma eval_fls_eqI:
assumes "f has_laurent_expansion F" "f holomorphic_on eball 0 r - {0}"
assumes "z \<in> eball 0 r - {0}"
@@ -1821,7 +1655,7 @@
lemma tendsto_0_subdegree_iff_0:
assumes F:"f has_laurent_expansion F" and "F\<noteq>0"
- shows "(f \<midarrow>0\<rightarrow>0) \<longleftrightarrow> fls_subdegree F > 0"
+ shows "(f \<midarrow>0\<rightarrow> 0) \<longleftrightarrow> fls_subdegree F > 0"
proof -
have ?thesis if "is_pole f 0"
proof -
@@ -1872,15 +1706,15 @@
qed
lemma tendsto_0_subdegree_iff:
- assumes F:"(\<lambda>w. f (z+w)) has_laurent_expansion F" and "F\<noteq>0"
- shows "(f \<midarrow>z\<rightarrow>0) \<longleftrightarrow> fls_subdegree F > 0"
+ assumes F: "(\<lambda>w. f (z+w)) has_laurent_expansion F" and "F \<noteq> 0"
+ shows "(f \<midarrow>z\<rightarrow> 0) \<longleftrightarrow> fls_subdegree F > 0"
apply (subst Lim_at_zero)
apply (rule tendsto_0_subdegree_iff_0)
using assms by auto
lemma is_pole_0_deriv_divide_iff:
- assumes F:"f has_laurent_expansion F" and "F\<noteq>0"
- shows "is_pole (\<lambda>x. deriv f x / f x) 0 \<longleftrightarrow> is_pole f 0 \<or> (f \<midarrow>0\<rightarrow>0)"
+ assumes F: "f has_laurent_expansion F" and "F \<noteq> 0"
+ shows "is_pole (\<lambda>x. deriv f x / f x) 0 \<longleftrightarrow> is_pole f 0 \<or> (f \<midarrow>0\<rightarrow> 0)"
proof -
have "(\<lambda>x. deriv f x / f x) has_laurent_expansion fls_deriv F / F"
using F by (auto intro:laurent_expansion_intros)
@@ -2396,43 +2230,6 @@
qed
qed
-lemma subdegree_fps_compose [simp]:
- fixes F G :: "'a :: idom fps"
- assumes [simp]: "fps_nth G 0 = 0"
- shows "subdegree (fps_compose F G) = subdegree F * subdegree G"
-proof (cases "G = 0"; cases "F = 0")
- assume [simp]: "G \<noteq> 0" "F \<noteq> 0"
- define m where "m = subdegree F"
- define F' where "F' = fps_shift m F"
- have F_eq: "F = F' * fps_X ^ m"
- unfolding F'_def by (simp add: fps_shift_times_fps_X_power m_def)
- have [simp]: "F' \<noteq> 0"
- using \<open>F \<noteq> 0\<close> unfolding F_eq by auto
- have "subdegree (fps_compose F G) = subdegree (fps_compose F' G) + m * subdegree G"
- by (simp add: F_eq fps_compose_mult_distrib fps_compose_eq_0_iff flip: fps_compose_power)
- also have "subdegree (fps_compose F' G) = 0"
- by (intro subdegree_eq_0) (auto simp: F'_def m_def)
- finally show ?thesis by (simp add: m_def)
-qed auto
-
-lemma fls_subdegree_power_int [simp]:
- fixes F :: "'a :: field fls"
- shows "fls_subdegree (F powi n) = n * fls_subdegree F"
- by (auto simp: power_int_def fls_subdegree_pow)
-
-lemma subdegree_fls_compose_fps [simp]:
- fixes G :: "'a :: field fps"
- assumes [simp]: "fps_nth G 0 = 0"
- shows "fls_subdegree (fls_compose_fps F G) = fls_subdegree F * subdegree G"
-proof (cases "F = 0"; cases "G = 0")
- assume [simp]: "G \<noteq> 0" "F \<noteq> 0"
- have nz1: "fls_base_factor_to_fps F \<noteq> 0"
- using \<open>F \<noteq> 0\<close> fls_base_factor_to_fps_nonzero by blast
- show ?thesis
- unfolding fls_compose_fps_def using nz1
- by (subst fls_subdegree_mult) (simp_all add: fps_compose_eq_0_iff fls_subdegree_fls_to_fps)
-qed (auto simp: fls_compose_fps_0_right)
-
lemma zorder_compose_aux:
assumes "isolated_singularity_at f 0" "not_essential f 0"
assumes G: "g has_fps_expansion G" "G \<noteq> 0" "g 0 = 0"
--- a/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy Mon Apr 21 08:24:58 2025 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy Fri Apr 18 10:58:16 2025 +0200
@@ -1165,6 +1165,58 @@
shows "fls_const x * fls_const y = fls_const (x*y)"
by (intro fls_eqI) simp
+lemma fls_subdegree_add_eq1:
+ assumes "f \<noteq> 0" "fls_subdegree f < fls_subdegree g"
+ shows "fls_subdegree (f + g) = fls_subdegree f"
+proof (intro antisym)
+ from assms have *: "fls_nth (f + g) (fls_subdegree f) \<noteq> 0"
+ by auto
+ from * show "fls_subdegree (f + g) \<le> fls_subdegree f"
+ by (rule fls_subdegree_leI)
+ from * have "f + g \<noteq> 0"
+ using fls_nonzeroI by blast
+ thus "fls_subdegree f \<le> fls_subdegree (f + g)"
+ using assms(2) fls_plus_subdegree by force
+qed
+
+lemma fls_subdegree_add_eq2:
+ assumes "g \<noteq> 0" "fls_subdegree g < fls_subdegree f"
+ shows "fls_subdegree (f + g) = fls_subdegree g"
+proof (intro antisym)
+ from assms have *: "fls_nth (f + g) (fls_subdegree g) \<noteq> 0"
+ by auto
+ from * show "fls_subdegree (f + g) \<le> fls_subdegree g"
+ by (rule fls_subdegree_leI)
+ from * have "f + g \<noteq> 0"
+ using fls_nonzeroI by blast
+ thus "fls_subdegree g \<le> fls_subdegree (f + g)"
+ using assms(2) fls_plus_subdegree by force
+qed
+
+lemma fls_subdegree_diff_eq1:
+ assumes "f \<noteq> 0" "fls_subdegree f < fls_subdegree g"
+ shows "fls_subdegree (f - g) = fls_subdegree f"
+ using fls_subdegree_add_eq1[of f "-g"] assms by simp
+
+lemma fls_subdegree_diff_eq2:
+ assumes "g \<noteq> 0" "fls_subdegree g < fls_subdegree f"
+ shows "fls_subdegree (f - g) = fls_subdegree g"
+ using fls_subdegree_add_eq2[of "-g" f] assms by simp
+
+lemma nat_minus_fls_subdegree_plus_const_eq:
+ "nat (-fls_subdegree (F + fls_const c)) = nat (-fls_subdegree F)"
+proof (cases "fls_subdegree F < 0")
+ case True
+ hence "fls_subdegree (F + fls_const c) = fls_subdegree F"
+ by (intro fls_subdegree_add_eq1) auto
+ thus ?thesis
+ by simp
+next
+ case False
+ thus ?thesis
+ by (auto simp: fls_subdegree_ge0I)
+qed
+
lemma fls_mult_subdegree_ge:
fixes f g :: "'a::{comm_monoid_add,mult_zero} fls"
assumes "f*g \<noteq> 0"
@@ -1705,6 +1757,13 @@
by standard
+lemma fls_subdegree_numeral [simp]: "fls_subdegree (numeral n) = 0"
+ by (metis fls_subdegree_of_nat of_nat_numeral)
+
+lemma fls_regpart_numeral [simp]: "fls_regpart (numeral n) = numeral n"
+ by (metis fls_regpart_of_nat of_nat_numeral)
+
+
subsubsection \<open>Powers\<close>
lemma fls_subdegree_prod:
@@ -2946,6 +3005,20 @@
instance fls :: ("{field_prime_char,comm_semiring_1}") field_prime_char
by (rule field_prime_charI') auto
+instance fls :: (semiring_char_0) semiring_char_0
+proof
+ show "inj (of_nat :: nat \<Rightarrow> 'a fls)"
+ by (metis fls_regpart_of_nat injI of_nat_eq_iff)
+qed
+
+instance fls :: (field_char_0) field_char_0 ..
+
+
+lemma fls_subdegree_power_int [simp]:
+ fixes F :: "'a :: field fls"
+ shows "fls_subdegree (F powi n) = n * fls_subdegree F"
+ by (auto simp: power_int_def fls_subdegree_pow)
+
subsubsection \<open>Division\<close>
@@ -3440,45 +3513,6 @@
shows "fls_compose_fps (F - G) H = fls_compose_fps F H - fls_compose_fps G H"
using fls_compose_fps_add[of H F "-G"] by simp
-lemma fps_compose_eq_0_iff:
- fixes F G :: "'a :: idom fps"
- assumes "fps_nth G 0 = 0"
- shows "fps_compose F G = 0 \<longleftrightarrow> F = 0 \<or> (G = 0 \<and> fps_nth F 0 = 0)"
-proof safe
- assume *: "fps_compose F G = 0" "F \<noteq> 0"
- have "fps_nth (fps_compose F G) 0 = fps_nth F 0"
- by simp
- also have "fps_compose F G = 0"
- by (simp add: *)
- finally show "fps_nth F 0 = 0"
- by simp
- show "G = 0"
- proof (rule ccontr)
- assume "G \<noteq> 0"
- hence "subdegree G > 0" using assms
- using subdegree_eq_0_iff by blast
- define N where "N = subdegree F * subdegree G"
- have "fps_nth (fps_compose F G) N = (\<Sum>i = 0..N. fps_nth F i * fps_nth (G ^ i) N)"
- unfolding fps_compose_def by (simp add: N_def)
- also have "\<dots> = (\<Sum>i\<in>{subdegree F}. fps_nth F i * fps_nth (G ^ i) N)"
- proof (intro sum.mono_neutral_right ballI)
- fix i assume i: "i \<in> {0..N} - {subdegree F}"
- show "fps_nth F i * fps_nth (G ^ i) N = 0"
- proof (cases i "subdegree F" rule: linorder_cases)
- assume "i > subdegree F"
- hence "fps_nth (G ^ i) N = 0"
- using i \<open>subdegree G > 0\<close> by (intro fps_pow_nth_below_subdegree) (auto simp: N_def)
- thus ?thesis by simp
- qed (use i in \<open>auto simp: N_def\<close>)
- qed (use \<open>subdegree G > 0\<close> in \<open>auto simp: N_def\<close>)
- also have "\<dots> = fps_nth F (subdegree F) * fps_nth (G ^ subdegree F) N"
- by simp
- also have "\<dots> \<noteq> 0"
- using \<open>G \<noteq> 0\<close> \<open>F \<noteq> 0\<close> by (auto simp: N_def)
- finally show False using * by auto
- qed
-qed auto
-
lemma fls_compose_fps_eq_0_iff:
assumes "H \<noteq> 0" "fps_nth H 0 = 0"
shows "fls_compose_fps F H = 0 \<longleftrightarrow> F = 0"
@@ -3588,7 +3622,7 @@
assumes "d > 0"
shows "fls_compose_power f d $$ n = (if int d dvd n then f $$ (n div int d) else 0)"
by (simp add: assms fls_compose_power.rep_eq)
-
+
lemma fls_compose_power_0_left [simp]: "fls_compose_power 0 d = 0"
by transfer auto
@@ -3680,6 +3714,20 @@
"d dvd n \<Longrightarrow> d > 0 \<Longrightarrow> fls_compose_power f d $$ int n = f $$ int (n div d)"
by (transfer; force; fail)+
+lemma subdegree_fls_compose_fps [simp]:
+ fixes G :: "'a :: field fps"
+ assumes [simp]: "fps_nth G 0 = 0"
+ shows "fls_subdegree (fls_compose_fps F G) = fls_subdegree F * subdegree G"
+proof (cases "F = 0"; cases "G = 0")
+ assume [simp]: "G \<noteq> 0" "F \<noteq> 0"
+ have nz1: "fls_base_factor_to_fps F \<noteq> 0"
+ using \<open>F \<noteq> 0\<close> fls_base_factor_to_fps_nonzero by blast
+ show ?thesis
+ unfolding fls_compose_fps_def using nz1
+ by (subst fls_subdegree_mult) (simp_all add: fps_compose_eq_0_iff fls_subdegree_fls_to_fps)
+qed (auto simp: fls_compose_fps_0_right)
+
+
subsection \<open>Formal differentiation and integration\<close>
subsubsection \<open>Derivative\<close>
@@ -3747,6 +3795,9 @@
shows "fls_subdegree (fls_deriv f) = fls_subdegree f - 1"
by (auto intro: fls_subdegree_deriv' simp: assms)
+lemma fps_deriv_fls_regpart: "fps_deriv (fls_regpart F) = fls_regpart (fls_deriv F)"
+ by (intro fps_ext) (auto simp: add_ac)
+
text \<open>
Shifting is like multiplying by a power of the implied variable, and so satisfies a product-like
rule.
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Mon Apr 21 08:24:58 2025 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Fri Apr 18 10:58:16 2025 +0200
@@ -11,6 +11,7 @@
Complex_Main
Euclidean_Algorithm
Primes
+ "HOL-Library.FuncSet"
begin
@@ -748,6 +749,19 @@
from arg_cong[of _ _ "\<lambda>F. F $ 0", OF this] show False by simp
qed
+instance fps :: (semiring_char_0) semiring_char_0
+proof
+ show "inj (of_nat :: nat \<Rightarrow> 'a fps)"
+ proof
+ fix m n :: nat
+ assume "of_nat m = (of_nat n :: 'a fps)"
+ hence "fps_nth (of_nat m) 0 = (fps_nth (of_nat n) 0 :: 'a)"
+ by (simp only: )
+ thus "m = n"
+ by simp
+ qed
+qed
+
lemma subdegree_power_ge:
"f^n \<noteq> 0 \<Longrightarrow> subdegree (f^n) \<ge> n * subdegree f"
proof (induct n)
@@ -801,6 +815,12 @@
"subdegree ((f :: ('a :: semiring_1_no_zero_divisors) fps) ^ n) = n * subdegree f"
by (cases "f = 0"; induction n) simp_all
+lemma subdegree_prod:
+ fixes f :: "'a \<Rightarrow> 'b :: idom fps"
+ assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> 0"
+ shows "subdegree (\<Prod>x\<in>A. f x) = (\<Sum>x\<in>A. subdegree (f x))"
+ using assms by (induction A rule: infinite_finite_induct) auto
+
lemma minus_one_power_iff: "(- (1::'a::ring_1)) ^ n = (if even n then 1 else - 1)"
by (induct n) auto
@@ -976,6 +996,25 @@
qed simp_all
+subsection \<open>Truncation\<close>
+
+text \<open>
+ Truncation of formal power series: all monomials $cx^k$ with $k\geq n$ are removed;
+ the remainder is a polynomial of degree at most $n-1$.
+\<close>
+definition truncate_fps :: "nat \<Rightarrow> 'a fps \<Rightarrow> 'a :: zero fps" where
+ "truncate_fps n F = Abs_fps (\<lambda>k. if k \<ge> n then 0 else fps_nth F k)"
+
+lemma fps_nth_truncate' [simp]:
+ "k \<ge> n \<Longrightarrow> fps_nth (truncate_fps n F) k = 0"
+ "k < n \<Longrightarrow> fps_nth (truncate_fps n F) k = fps_nth F k"
+ by (auto simp: truncate_fps_def)
+
+lemma truncate_fps_eq_truncate_fps_iff:
+ "truncate_fps N F = truncate_fps N G \<longleftrightarrow> (\<forall>n<N. fps_nth F n = fps_nth G n)"
+ by (auto simp: fps_eq_iff truncate_fps_def)
+
+
subsection \<open>Shifting and slicing\<close>
definition fps_shift :: "nat \<Rightarrow> 'a fps \<Rightarrow> 'a fps" where
@@ -1402,6 +1441,144 @@
lemma open_fps_def: "open (S :: 'a::group_add fps set) = (\<forall>a \<in> S. \<exists>r. r >0 \<and> {y. dist y a < r} \<subseteq> S)"
unfolding open_dist subset_eq by simp
+
+text \<open>Topology\<close>
+
+subsection \<open>The topology of formal power series\<close>
+
+text \<open>
+ A set of formal power series is open iff for any power series $f$ in it, there exists some
+ number $n$ such that all power series that agree with $f$ on the first $n$ components are
+ also in it.
+\<close>
+lemma open_fps_iff:
+ "open A \<longleftrightarrow> (\<forall>F\<in>A. \<exists>n. {G. truncate_fps n G = truncate_fps n F} \<subseteq> A)"
+proof
+ assume "open A"
+ show "\<forall>F\<in>A. \<exists>n. {G. truncate_fps n G = truncate_fps n F} \<subseteq> A"
+ proof
+ fix F :: "'a fps"
+ assume F: "F \<in> A"
+ with \<open>open A\<close> obtain e where e: "e > 0" "\<And>G. dist G F < e \<Longrightarrow> G \<in> A"
+ by (force simp: open_fps_def)
+ thm dist_fps_def
+ have "filterlim (\<lambda>n. (1/2)^n :: real) (nhds 0) at_top"
+ by (intro LIMSEQ_realpow_zero) auto
+ from order_tendstoD(2)[OF this e(1)] have "eventually (\<lambda>n. 1 / 2 ^ n < e) at_top"
+ by (simp add: power_divide)
+ then obtain n where n: "1 / 2 ^ n < e"
+ by (auto simp: eventually_sequentially)
+ show "\<exists>n. {G. truncate_fps n G = truncate_fps n F} \<subseteq> A"
+ proof (rule exI[of _ n], safe)
+ fix G assume *: "truncate_fps n G = truncate_fps n F"
+ show "G \<in> A"
+ proof (cases "G = F")
+ case False
+ hence "dist G F = inverse (2 ^ subdegree (G - F))"
+ by (auto simp: dist_fps_def)
+ also have "subdegree (G - F) \<ge> n"
+ proof (rule subdegree_geI)
+ fix i assume "i < n"
+ hence "fps_nth (G - F) i = fps_nth (truncate_fps n G - truncate_fps n F) i"
+ by (auto simp: fps_eq_iff)
+ also from * have "\<dots> = 0"
+ by simp
+ finally show "fps_nth (G - F) i = 0" .
+ qed (use False in auto)
+ hence "inverse (2 ^ subdegree (G - F) :: real) \<le> inverse (2 ^ n)"
+ by (intro le_imp_inverse_le power_increasing) auto
+ also have "\<dots> < e"
+ using n by (simp add: field_simps)
+ finally show "G \<in> A"
+ using e(2)[of G] by auto
+ qed (use \<open>F \<in> A\<close> in auto)
+ qed
+ qed
+next
+ assume *: "\<forall>F\<in>A. \<exists>n. {G. truncate_fps n G = truncate_fps n F} \<subseteq> A"
+ show "open A"
+ unfolding open_fps_def
+ proof safe
+ fix F assume F: "F \<in> A"
+ with * obtain n where n: "\<And>G. truncate_fps n G = truncate_fps n F \<Longrightarrow> G \<in> A"
+ by blast
+ show "\<exists>r>0. {G. dist G F < r} \<subseteq> A"
+ proof (rule exI[of _ "1 / 2 ^ n"], safe)
+ fix G assume dist: "dist G F < 1 / 2 ^ n"
+ show "G \<in> A"
+ proof (cases "G = F")
+ case False
+ hence "dist G F = inverse (2 ^ subdegree (F - G))"
+ by (simp add: dist_fps_def)
+ with dist have "n < subdegree (F - G)"
+ by (auto simp: field_simps)
+ hence "fps_nth (F - G) i = 0" if "i \<le> n" for i
+ using that nth_less_subdegree_zero[of i "F - G"] by simp
+ hence "truncate_fps n G = truncate_fps n F"
+ by (auto simp: fps_eq_iff truncate_fps_def)
+ thus "G \<in> A"
+ by (rule n)
+ qed (use \<open>F \<in> A\<close> in auto)
+ qed auto
+ qed
+qed
+
+lemma open_truncate_fps: "open {H. truncate_fps N H = truncate_fps N G}"
+ unfolding open_fps_iff
+proof safe
+ fix F assume F: "truncate_fps N F = truncate_fps N G"
+ show "\<exists>n. {G. truncate_fps n G = truncate_fps n F}
+ \<subseteq> {H. truncate_fps N H = truncate_fps N G}"
+ by (rule exI[of _ N]) (use F in \<open>auto simp: fps_eq_iff\<close>)
+qed
+
+text \<open>
+ A family of formal power series $f_x$ tends to a limit series $g$ at some filter $F$
+ iff for any $N\geq 0$, the set of $x$ for which $f_x$ and $G$ agree on the first $N$ coefficients
+ is in $F$.
+
+ For a sequence $(f_i)_{n\geq 0}$ this means that $f_i \longrightarrow G$ iff for any
+ $N\geq 0$, $f_x$ and $G$ agree for all but finitely many $x$.
+\<close>
+
+lemma tendsto_fps_iff:
+ "filterlim f (nhds (g :: 'a :: group_add fps)) F \<longleftrightarrow>
+ (\<forall>n. eventually (\<lambda>x. fps_nth (f x) n = fps_nth g n) F)"
+proof safe
+ assume lim: "filterlim f (nhds (g :: 'a :: group_add fps)) F"
+ show "eventually (\<lambda>x. fps_nth (f x) n = fps_nth g n) F" for n
+ proof -
+ define S where "S = {H. truncate_fps (n+1) H = truncate_fps (n+1) g}"
+ have S: "open S" "g \<in> S"
+ unfolding S_def using open_truncate_fps[of "n+1" g] by (auto simp: S_def)
+ from lim and S have "eventually (\<lambda>x. f x \<in> S) F"
+ using topological_tendstoD by blast
+ thus "eventually (\<lambda>x. fps_nth (f x) n = fps_nth g n) F"
+ by eventually_elim (auto simp: S_def truncate_fps_eq_truncate_fps_iff)
+ qed
+next
+ assume *: "\<forall>n. eventually (\<lambda>x. fps_nth (f x) n = fps_nth g n) F"
+ show "filterlim f (nhds (g :: 'a :: group_add fps)) F"
+ proof (rule topological_tendstoI)
+ fix S :: "'a fps set"
+ assume S: "open S" "g \<in> S"
+ then obtain N where N: "{H. truncate_fps N H = truncate_fps N g} \<subseteq> S"
+ unfolding open_fps_iff by blast
+ have "eventually (\<lambda>x. \<forall>n\<in>{..<N}. fps_nth (f x) n = fps_nth g n) F"
+ by (subst eventually_ball_finite_distrib) (use * in auto)
+ hence "eventually (\<lambda>x. f x \<in> {H. truncate_fps N H = truncate_fps N g}) F"
+ by eventually_elim (auto simp: truncate_fps_eq_truncate_fps_iff)
+ thus "eventually (\<lambda>x. f x \<in> S) F"
+ by eventually_elim (use N in auto)
+ qed
+qed
+
+lemma tendsto_fpsI:
+ assumes "\<And>n. eventually (\<lambda>x. fps_nth (f x) n = fps_nth G n) F"
+ shows "filterlim f (nhds (G :: 'a :: group_add fps)) F"
+ unfolding tendsto_fps_iff using assms by blast
+
+
text \<open>The infinite sums and justification of the notation in textbooks.\<close>
lemma reals_power_lt_ex:
@@ -3447,6 +3624,333 @@
by (simp add: fps_deriv_power' fps_of_nat)
+subsection \<open>Finite and infinite products\<close>
+
+text \<open>
+ The following operator gives the set of all functions $A \to \mathbb{N}$ with
+ $\sum_{x\in A} f(x) = n$, i.e.\ all the different ways to put $n$ unlabelled balls into
+ the labelled bins $A$.
+\<close>
+definition nat_partitions :: "'a set \<Rightarrow> nat \<Rightarrow> ('a \<Rightarrow> nat) set" where
+ "nat_partitions A n =
+ {f. finite {x. f x > 0} \<and> {x. f x > 0} \<subseteq> A \<and> (\<Sum>x\<in>{x\<in>A. f x > 0}. f x) = n}"
+
+lemma
+ assumes "h \<in> nat_partitions A n"
+ shows nat_partitions_outside: "x \<notin> A \<Longrightarrow> h x = 0"
+ and nat_partitions_sum: "(\<Sum>x\<in>{x\<in>A. h x > 0}. h x) = n"
+ and nat_partitions_finite_support: "finite {x. h x > 0}"
+ using assms by (auto simp: nat_partitions_def)
+
+lemma nat_partitions_finite_def:
+ assumes "finite A"
+ shows "nat_partitions A n = {f. {x. f x > 0} \<subseteq> A \<and> (\<Sum>x\<in>A. f x) = n}"
+proof (intro equalityI subsetI)
+ fix f assume f: "f \<in> nat_partitions A n"
+ have "(\<Sum>x\<in>A. f x) = (\<Sum>x | x \<in> A \<and> f x > 0. f x)"
+ by (rule sum.mono_neutral_right) (use assms in auto)
+ thus "f \<in> {f. {x. f x > 0} \<subseteq> A \<and> (\<Sum>x\<in>A. f x) = n}"
+ using f nat_partitions_def by auto
+next
+ fix f assume "f \<in> {f. {x. f x > 0} \<subseteq> A \<and> (\<Sum>x\<in>A. f x) = n}"
+ hence f: "{x. f x > 0} \<subseteq> A" "(\<Sum>x\<in>A. f x) = n"
+ by blast+
+ have "(\<Sum>x\<in>A. f x) = (\<Sum>x | x \<in> A \<and> f x > 0. f x)"
+ by (rule sum.mono_neutral_right) (use assms in auto)
+ moreover have "finite {x. f x > 0}"
+ using f(1) assms by (rule finite_subset)
+ ultimately show "f \<in> nat_partitions A n"
+ using f by (simp add: nat_partitions_def)
+qed
+
+lemma nat_partitions_subset:
+ "nat_partitions A n \<subseteq> A \<rightarrow> {0..n}"
+proof
+ fix f assume f: "f \<in> nat_partitions A n"
+ have "f x \<le> n" if x: "x \<in> A" for x
+ proof (cases "f x = 0")
+ case False
+ have "f x \<le> (\<Sum>x\<in>{x\<in>A. f x \<noteq> 0}. f x)"
+ by (rule member_le_sum) (use x False f in \<open>auto simp: nat_partitions_def\<close>)
+ also have "\<dots> = n"
+ using f by (auto simp: nat_partitions_def)
+ finally show "f x \<le> n" .
+ qed auto
+ thus "f \<in> A \<rightarrow> {0..n}"
+ using f by (auto simp: nat_partitions_def)
+qed
+
+lemma conj_mono_strong: "(P1 \<longrightarrow> Q1) \<Longrightarrow> (P1 \<longrightarrow> P2 \<longrightarrow> Q2) \<Longrightarrow> (P1 \<and> P2) \<longrightarrow> (Q1 \<and> Q2)"
+ by iprover
+
+lemma nat_partitions_mono:
+ assumes "A \<subseteq> B"
+ shows "nat_partitions A n \<subseteq> nat_partitions B n"
+ unfolding nat_partitions_def
+proof (intro Collect_mono conj_mono_strong impI)
+ fix f :: "'a \<Rightarrow> nat"
+ assume 1: "finite {x. f x > 0}"
+ assume 2: "{x. f x > 0} \<subseteq> A"
+ thus "{x. f x > 0} \<subseteq> B"
+ using assms by blast
+ assume 3: "(\<Sum>x | x \<in> A \<and> f x > 0. f x) = n"
+ have *: "{x\<in>B. f x > 0} = {x\<in>A. f x > 0} \<union> {x\<in>B-A. f x > 0}"
+ using assms by auto
+ have "(\<Sum>x | x \<in> B \<and> f x > 0. f x) = (\<Sum>x | x \<in> A \<and> f x > 0. f x)"
+ by (intro sum.mono_neutral_right) (use assms 2 in \<open>auto intro: finite_subset[OF _ 1]\<close>)
+ with 3 show "(\<Sum>x | x \<in> B \<and> f x > 0. f x) = n"
+ by simp
+qed
+
+lemma in_nat_partitions_imp_le:
+ assumes "h \<in> nat_partitions A n" "x \<in> A"
+ shows "h x \<le> n"
+ using nat_partitions_subset[of A n] assms by (auto simp: PiE_def Pi_def)
+
+lemma nat_partitions_0 [simp]: "nat_partitions A 0 = {\<lambda>_. 0}"
+proof (intro equalityI subsetI)
+ fix h :: "'a \<Rightarrow> nat" assume "h \<in> {\<lambda>_. 0}"
+ thus "h \<in> nat_partitions A 0"
+ by (auto simp: nat_partitions_def)
+qed (auto simp: nat_partitions_def fun_eq_iff)
+
+lemma nat_partitions_empty [simp]: "n > 0 \<Longrightarrow> nat_partitions {} n = {}"
+ by (auto simp: nat_partitions_def fun_eq_iff)
+
+lemma nat_partitions_insert:
+ assumes [simp]: "a \<notin> A"
+ shows "bij_betw (\<lambda>(m,f). f(a := m))
+ (SIGMA m:{0..n}. nat_partitions A (n - m)) (nat_partitions (insert a A) n)"
+proof (rule bij_betwI[of _ _ _ "\<lambda>f. (f a, f(a := 0))"], goal_cases)
+ case 1
+ show ?case
+ proof safe
+ fix m f assume m: "m \<in> {0..n}" and f: "f \<in> nat_partitions A (n - m)"
+ define f' where "f' = f(a := m)"
+ have "(\<Sum>x\<in>{x\<in>insert a A. f' x > 0}. f' x) = (\<Sum>x\<in>insert a {x\<in>A. f x > 0}. f' x)"
+ by (rule sum.mono_neutral_cong_left)
+ (use f in \<open>auto simp: f'_def nat_partitions_def\<close>)
+ also have "\<dots> = m + (\<Sum>x\<in>{x\<in>A. f x > 0}. f' x)"
+ by (subst sum.insert) (use f in \<open>auto simp: nat_partitions_def f'_def\<close>)
+ also have "(\<Sum>x\<in>{x\<in>A. f x > 0}. f' x) = (\<Sum>x\<in>{x\<in>A. f x > 0}. f x)"
+ by (intro sum.cong) (auto simp: f'_def)
+ also have "\<dots> = n - m"
+ using f by (auto simp: nat_partitions_def)
+ finally have "(\<Sum>x\<in>{x\<in>insert a A. f' x > 0}. f' x) = n"
+ using m by simp
+ moreover have "finite {x. f' x > 0}"
+ by (rule finite_subset[of _ "insert a {x\<in>A. f x > 0}"])
+ (use f in \<open>auto simp: nat_partitions_def f'_def\<close>)
+ moreover have "{x. f' x > 0} \<subseteq> insert a A"
+ using f by (auto simp: f'_def nat_partitions_def)
+ ultimately show "f' \<in> nat_partitions (insert a A) n"
+ by (simp add: nat_partitions_def)
+ qed
+next
+ case 2
+ show ?case
+ proof safe
+ fix f assume "f \<in> nat_partitions (insert a A) n"
+ define f' where "f' = f(a := 0)"
+ have fin: "finite {x. f x > 0}"
+ and subset: "{x. f x > 0} \<subseteq> insert a A"
+ and sum: "(\<Sum>x\<in>{x\<in>insert a A. f x > 0}. f x) = n"
+ using \<open>f \<in> _\<close> by (auto simp: nat_partitions_def)
+
+ show le: "f a \<in> {0..n}"
+ proof (cases "f a = 0")
+ case False
+ hence "f a \<le> (\<Sum>x\<in>{x\<in>insert a A. f x > 0}. f x)"
+ by (intro member_le_sum) (use fin in auto)
+ with sum show ?thesis
+ by simp
+ qed auto
+
+ have "n = (\<Sum>x\<in>{x\<in>insert a A. f x > 0}. f x)"
+ using sum by simp
+ also have "(\<Sum>x\<in>{x\<in>insert a A. f x > 0}. f x) = (\<Sum>x\<in>insert a {x\<in>A. f x > 0}. f x)"
+ by (rule sum.mono_neutral_left) (auto intro: finite_subset[OF _ fin])
+ also have "\<dots> = f a + (\<Sum>x\<in>{x\<in>A. f x > 0}. f x)"
+ by (subst sum.insert) (auto intro: finite_subset[OF _ fin])
+ also have "(\<Sum>x\<in>{x\<in>A. f x > 0}. f x) = (\<Sum>x\<in>{x\<in>A. f' x > 0}. f' x)"
+ by (intro sum.cong) (auto simp: f'_def)
+ finally have "(\<Sum>x\<in>{x\<in>A. f' x > 0}. f' x) = n - f a"
+ using le by simp
+
+ moreover have "finite {x. 0 < f' x}"
+ by (rule finite_subset[OF _ fin]) (auto simp: f'_def)
+ moreover have "{x. 0 < f' x} \<subseteq> A"
+ using subset by (auto simp: f'_def)
+ ultimately show "f' \<in> nat_partitions A (n - f a)"
+ by (auto simp: nat_partitions_def)
+ qed
+next
+ case (3 f)
+ thus ?case
+ by (fastforce simp: nat_partitions_def fun_eq_iff)
+qed (auto simp: nat_partitions_def)
+
+lemma finite_nat_partitions [intro]:
+ assumes "finite A"
+ shows "finite (nat_partitions A n)"
+ using assms
+proof (induction arbitrary: n rule: finite_induct)
+ case empty
+ thus ?case
+ by (cases "n = 0") auto
+next
+ case (insert x A n)
+ have "finite (SIGMA m:{0..n}. nat_partitions A (n - m))"
+ by (auto intro: insert.IH)
+ also have "?this \<longleftrightarrow> finite (nat_partitions (insert x A) n)"
+ by (rule bij_betw_finite, rule nat_partitions_insert) fact
+ finally show ?case .
+qed
+
+lemma fps_prod_nth':
+ assumes "finite A"
+ shows "fps_nth (\<Prod>x\<in>A. f x) n = (\<Sum>h\<in>nat_partitions A n. \<Prod>x\<in>A. fps_nth (f x) (h x))"
+ using assms
+proof (induction A arbitrary: n rule: finite_induct)
+ case (insert a A n)
+ note [simp] = \<open>a \<notin> A\<close>
+ note [intro, simp] = \<open>finite A\<close>
+ have "(\<Sum>h\<in>nat_partitions (insert a A) n. \<Prod>x\<in>insert a A. fps_nth (f x) (h x)) =
+ (\<Sum>(m,h)\<in>(SIGMA m:{0..n}. nat_partitions A (n-m)). \<Prod>x\<in>insert a A. fps_nth (f x) ((h(a := m)) x))"
+ by (subst sum.reindex_bij_betw[OF nat_partitions_insert, symmetric])
+ (simp_all add: case_prod_unfold)
+ also have "\<dots> = (\<Sum>m=0..n. \<Sum>h\<in>nat_partitions A (n-m). \<Prod>x\<in>insert a A. fps_nth (f x) ((h(a := m)) x))"
+ by (rule sum.Sigma [symmetric]) auto
+ also have "\<dots> = (\<Sum>m=0..n. fps_nth (f a) m * fps_nth (\<Prod>x\<in>A. f x) (n - m))"
+ proof (rule sum.cong)
+ fix m
+ assume m: "m \<in> {0..n}"
+ have "(\<Sum>h\<in>nat_partitions A (n-m). \<Prod>x\<in>insert a A. fps_nth (f x) ((h(a := m)) x)) =
+ fps_nth (f a) m * (\<Sum>h\<in>nat_partitions A (n-m). \<Prod>x\<in>A. fps_nth (f x) ((h(a := m)) x))"
+ by (simp add: sum_distrib_left)
+ also have "(\<Sum>h\<in>nat_partitions A (n-m). \<Prod>x\<in>A. fps_nth (f x) ((h(a := m)) x)) =
+ (\<Sum>h\<in>nat_partitions A (n-m). \<Prod>x\<in>A. fps_nth (f x) (h x))"
+ by (intro sum.cong prod.cong) auto
+ also have "\<dots> = fps_nth (\<Prod>x\<in>A. f x) (n - m)"
+ by (rule insert.IH [symmetric])
+ finally show "(\<Sum>h\<in>nat_partitions A (n-m). \<Prod>x\<in>insert a A. fps_nth (f x) ((h(a := m)) x)) =
+ fps_nth (f a) m * fps_nth (\<Prod>x\<in>A. f x) (n - m)" .
+ qed auto
+ also have "\<dots> = fps_nth (\<Prod>x\<in>insert a A. f x) n"
+ by (simp add: fps_mult_nth)
+ finally show ?case ..
+qed auto
+
+theorem tendsto_prod_fps:
+ fixes f :: "nat \<Rightarrow> 'a :: {idom, t2_space} fps"
+ assumes [simp]: "\<And>k. f k \<noteq> 0"
+ assumes g: "\<And>n k. k > g n \<Longrightarrow> subdegree (f k - 1) > n"
+ defines "P \<equiv> Abs_fps (\<lambda>n. (\<Sum>h\<in>nat_partitions {..g n} n. \<Prod>i\<le>g n. fps_nth (f i) (h i)))"
+ shows "(\<lambda>n. \<Prod>k\<le>n. f k) \<longlonglongrightarrow> P"
+proof (rule tendsto_fpsI)
+ fix n :: nat
+ show "eventually (\<lambda>N. fps_nth (prod f {..N}) n = fps_nth P n) at_top"
+ using eventually_ge_at_top[of "g n"]
+ proof eventually_elim
+ case (elim N)
+ have "fps_nth (prod f {..N}) n = (\<Sum>h\<in>nat_partitions {..N} n. \<Prod>x\<le>N. fps_nth (f x) (h x))"
+ by (subst fps_prod_nth') auto
+ also have "\<dots> = (\<Sum>h | h \<in> nat_partitions {..N} n \<and> (\<forall>x\<le>N. fps_nth (f x) (h x) \<noteq> 0).
+ \<Prod>x\<le>N. fps_nth (f x) (h x))"
+ by (intro sum.mono_neutral_right) auto
+
+ also have "{h. h \<in> nat_partitions {..N} n \<and> (\<forall>x\<le>N. fps_nth (f x) (h x) \<noteq> 0)} =
+ {h. h \<in> nat_partitions {..g n} n \<and> (\<forall>x\<le>N. fps_nth (f x) (h x) \<noteq> 0)}" (is "?lhs = ?rhs")
+ proof (intro equalityI subsetI)
+ fix h assume "h \<in> ?rhs"
+ thus "h \<in> ?lhs" using elim nat_partitions_mono[of "{..g n}" "{..N}"] by auto
+ next
+ fix h assume "h \<in> ?lhs"
+ hence h: "{x. 0 < h x} \<subseteq> {..N}" "(\<Sum>x\<le>N. h x) = n" "\<And>x. x \<le> N \<Longrightarrow> fps_nth (f x) (h x) \<noteq> 0"
+ by (auto simp: nat_partitions_finite_def)
+ have "{x. 0 < h x} \<subseteq> {..g n}"
+ proof
+ fix x assume *: "x \<in> {x. h x > 0}"
+ show "x \<in> {..g n}"
+ proof (rule ccontr)
+ assume "x \<notin> {..g n}"
+ hence x: "x > g n" "x \<le> N"
+ using h(1) * by auto
+ have "h x \<le> n"
+ using \<open>h \<in> ?lhs\<close> nat_partitions_subset[of "{..N}" n] x by (auto simp: Pi_def)
+ also have "n < subdegree (f x - 1)"
+ by (rule g) (use x in auto)
+ finally have "fps_nth (f x - 1) (h x) = 0"
+ by blast
+ hence "fps_nth (f x) (h x) = 0"
+ using * by simp
+ moreover have "fps_nth (f x) (h x) \<noteq> 0"
+ by (intro h(3)) (use x in auto)
+ ultimately show False by contradiction
+ qed
+ qed
+ moreover from this have "(\<Sum>x\<le>N. h x) = (\<Sum>x\<le>g n. h x)"
+ by (intro sum.mono_neutral_right) (use elim in auto)
+ ultimately show "h \<in> ?rhs" using elim h
+ by (auto simp: nat_partitions_finite_def)
+ qed
+
+ also have "(\<Sum>h | h \<in> nat_partitions {..g n} n \<and> (\<forall>x\<le>N. fps_nth (f x) (h x) \<noteq> 0).
+ \<Prod>x\<le>N. fps_nth (f x) (h x)) =
+ (\<Sum>h | h \<in> nat_partitions {..g n} n \<and> (\<forall>x\<le>N. fps_nth (f x) (h x) \<noteq> 0).
+ \<Prod>i\<le>g n. fps_nth (f i) (h i))"
+ proof (intro sum.cong prod.mono_neutral_right ballI)
+ fix h i
+ assume i: "i \<in> {..N} - {..g n}"
+ assume "h \<in> {h. h \<in> nat_partitions {..g n} n \<and> (\<forall>x\<le>N. fps_nth (f x) (h x) \<noteq> 0)}"
+ hence h: "h \<in> nat_partitions {..g n} n" "\<And>x. x \<le> N \<Longrightarrow> fps_nth (f x) (h x) \<noteq> 0"
+ by blast+
+ have [simp]: "h i = 0"
+ using i h unfolding nat_partitions_def by auto
+ have "n < subdegree (f i - 1)"
+ by (intro g) (use i in auto)
+ moreover have "h i \<le> n"
+ by auto
+ ultimately have "fps_nth (f i - 1) (h i) = 0"
+ by (intro nth_less_subdegree_zero) auto
+ thus "fps_nth (f i) (h i) = 1"
+ using h(2) i by (auto split: if_splits)
+ qed (use elim in auto)
+
+ also have "(\<Sum>h | h \<in> nat_partitions {..g n} n \<and> (\<forall>x\<le>N. fps_nth (f x) (h x) \<noteq> 0).
+ \<Prod>i\<le>g n. fps_nth (f i) (h i)) =
+ (\<Sum>h \<in> nat_partitions {..g n} n. \<Prod>i\<le>g n. fps_nth (f i) (h i))"
+ proof (intro sum.mono_neutral_left ballI)
+ fix h assume "h \<in> nat_partitions {..g n} n - {h\<in>nat_partitions {..g n} n. \<forall>x\<le>N. fps_nth (f x) (h x) \<noteq> 0}"
+ then obtain i where h: "h \<in> nat_partitions {..g n} n" and i: "i \<le> N" "fps_nth (f i) (h i) = 0"
+ by blast
+ have "\<not>(i > g n)"
+ proof
+ assume i': "i > g n"
+ hence "h i = 0"
+ using h by (auto simp: nat_partitions_def)
+ have "subdegree (f i - 1) > n"
+ by (intro g) (use i' in auto)
+ hence "subdegree (f i - 1) > 0"
+ by simp
+ hence "fps_nth (f i - 1) 0 = 0"
+ by blast
+ hence "fps_nth (f i) (h i) = 1"
+ using \<open>h i = 0\<close> by simp
+ thus False using i by simp
+ qed
+ thus " (\<Prod>x\<le>g n. fps_nth (f x) (h x)) = 0"
+ using i by auto
+ qed auto
+
+ also have "\<dots> = fps_nth P n"
+ by (simp add: P_def)
+ finally show "fps_nth (\<Prod>k\<le>N. f k) n = fps_nth P n" .
+ qed
+qed
+
+
+
subsection \<open>Integration\<close>
definition fps_integral :: "'a::{semiring_1,inverse} fps \<Rightarrow> 'a \<Rightarrow> 'a fps"
@@ -4911,6 +5415,64 @@
lemma fps_X_fps_compose: "fps_X oo a = Abs_fps (\<lambda>n. if n = 0 then (0::'a::comm_ring_1) else a$n)"
by (simp add: fps_eq_iff fps_compose_nth mult_delta_left)
+lemma fps_compose_eq_0_iff:
+ fixes F G :: "'a :: idom fps"
+ assumes "fps_nth G 0 = 0"
+ shows "fps_compose F G = 0 \<longleftrightarrow> F = 0 \<or> (G = 0 \<and> fps_nth F 0 = 0)"
+proof safe
+ assume *: "fps_compose F G = 0" "F \<noteq> 0"
+ have "fps_nth (fps_compose F G) 0 = fps_nth F 0"
+ by simp
+ also have "fps_compose F G = 0"
+ by (simp add: *)
+ finally show "fps_nth F 0 = 0"
+ by simp
+ show "G = 0"
+ proof (rule ccontr)
+ assume "G \<noteq> 0"
+ hence "subdegree G > 0" using assms
+ using subdegree_eq_0_iff by blast
+ define N where "N = subdegree F * subdegree G"
+ have "fps_nth (fps_compose F G) N = (\<Sum>i = 0..N. fps_nth F i * fps_nth (G ^ i) N)"
+ unfolding fps_compose_def by (simp add: N_def)
+ also have "\<dots> = (\<Sum>i\<in>{subdegree F}. fps_nth F i * fps_nth (G ^ i) N)"
+ proof (intro sum.mono_neutral_right ballI)
+ fix i assume i: "i \<in> {0..N} - {subdegree F}"
+ show "fps_nth F i * fps_nth (G ^ i) N = 0"
+ proof (cases i "subdegree F" rule: linorder_cases)
+ assume "i > subdegree F"
+ hence "fps_nth (G ^ i) N = 0"
+ using i \<open>subdegree G > 0\<close> by (intro fps_pow_nth_below_subdegree) (auto simp: N_def)
+ thus ?thesis by simp
+ qed (use i in \<open>auto simp: N_def\<close>)
+ qed (use \<open>subdegree G > 0\<close> in \<open>auto simp: N_def\<close>)
+ also have "\<dots> = fps_nth F (subdegree F) * fps_nth (G ^ subdegree F) N"
+ by simp
+ also have "\<dots> \<noteq> 0"
+ using \<open>G \<noteq> 0\<close> \<open>F \<noteq> 0\<close> by (auto simp: N_def)
+ finally show False using * by auto
+ qed
+qed auto
+
+lemma subdegree_fps_compose [simp]:
+ fixes F G :: "'a :: idom fps"
+ assumes [simp]: "fps_nth G 0 = 0"
+ shows "subdegree (fps_compose F G) = subdegree F * subdegree G"
+proof (cases "G = 0"; cases "F = 0")
+ assume [simp]: "G \<noteq> 0" "F \<noteq> 0"
+ define m where "m = subdegree F"
+ define F' where "F' = fps_shift m F"
+ have F_eq: "F = F' * fps_X ^ m"
+ unfolding F'_def by (simp add: fps_shift_times_fps_X_power m_def)
+ have [simp]: "F' \<noteq> 0"
+ using \<open>F \<noteq> 0\<close> unfolding F_eq by auto
+ have "subdegree (fps_compose F G) = subdegree (fps_compose F' G) + m * subdegree G"
+ by (simp add: F_eq fps_compose_mult_distrib fps_compose_eq_0_iff flip: fps_compose_power)
+ also have "subdegree (fps_compose F' G) = 0"
+ by (intro subdegree_eq_0) (auto simp: F'_def m_def)
+ finally show ?thesis by (simp add: m_def)
+qed auto
+
lemma fps_inverse_compose:
assumes b0: "(b$0 :: 'a::field) = 0"
and a0: "a$0 \<noteq> 0"
--- a/src/HOL/Groups_Big.thy Mon Apr 21 08:24:58 2025 +0200
+++ b/src/HOL/Groups_Big.thy Fri Apr 18 10:58:16 2025 +0200
@@ -1792,4 +1792,74 @@
finally show ?case .
qed
+lemma prod_add:
+ fixes f1 f2 :: "'a \<Rightarrow> 'c :: comm_semiring_1"
+ assumes finite: "finite A"
+ shows "(\<Prod>x\<in>A. f1 x + f2 x) = (\<Sum>X\<in>Pow A. (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. f2 x))"
+ using assms
+proof (induction A rule: finite_induct)
+ case (insert x A)
+ have "(\<Sum>X\<in>Pow (insert x A). (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>insert x A-X. f2 x)) =
+ (\<Sum>X\<in>Pow A. (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>insert x A-X. f2 x)) +
+ (\<Sum>X\<in>insert x ` (Pow A). (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>insert x A-X. f2 x))"
+ unfolding Pow_insert by (rule sum.union_disjoint) (use insert.hyps in auto)
+ also have "(\<Sum>X\<in>Pow A. (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>insert x A-X. f2 x)) =
+ (\<Sum>X\<in>Pow A. f2 x * (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. f2 x))"
+ proof (rule sum.cong)
+ fix X assume X: "X \<in> Pow A"
+ have "(\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>insert x (A-X). f2 x) = f2 x * (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. f2 x)"
+ by (subst prod.insert) (use insert.hyps finite_subset[of X A] X in \<open>auto simp: mult_ac\<close>)
+ also have "insert x (A - X) = insert x A - X"
+ using insert.hyps X by auto
+ finally show "(\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>insert x A-X. f2 x) = f2 x * (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. f2 x)" .
+ qed auto
+ also have "(\<Sum>X\<in>insert x ` (Pow A). (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>insert x A-X. f2 x)) =
+ (\<Sum>X\<in>Pow A. (\<Prod>x\<in>insert x X. f1 x) * (\<Prod>x\<in>insert x A-insert x X. f2 x))"
+ by (subst sum.reindex) (use insert.hyps in \<open>auto intro!: inj_onI simp: o_def\<close>)
+ also have "(\<Sum>X\<in>Pow A. (\<Prod>x\<in>insert x X. f1 x) * (\<Prod>x\<in>insert x A-insert x X. f2 x)) =
+ (\<Sum>X\<in>Pow A. f1 x * (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. f2 x))"
+ proof (rule sum.cong)
+ fix X assume X: "X \<in> Pow A"
+ show "(\<Prod>x\<in>insert x X. f1 x) * (\<Prod>x\<in>insert x A-insert x X. f2 x) =
+ f1 x * (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. f2 x)"
+ by (subst prod.insert) (use insert.hyps finite_subset[of X A] X in auto)
+ qed auto
+ also have "(\<Sum>X\<in>Pow A. f2 x * prod f1 X * prod f2 (A - X)) +
+ (\<Sum>X\<in>Pow A. f1 x * prod f1 X * prod f2 (A - X)) =
+ (f1 x + f2 x) * (\<Sum>X\<in>Pow A. prod f1 X * prod f2 (A - X))"
+ by (simp add: algebra_simps flip: sum_distrib_left sum_distrib_right)
+ finally show ?case
+ by (subst (asm) insert.IH [symmetric]) (use insert.hyps in simp)
+qed auto
+
+lemma prod_diff1:
+ fixes f1 f2 :: "'a \<Rightarrow> 'c :: comm_ring_1"
+ assumes finite: "finite A"
+ shows "(\<Prod>x\<in>A. f1 x - f2 x) = (\<Sum>X\<in>Pow A. (-1) ^ card X * (\<Prod>x\<in>X. f2 x) * (\<Prod>x\<in>A-X. f1 x))"
+proof -
+ have "(\<Prod>x\<in>A. f1 x - f2 x) = (\<Prod>x\<in>A. -f2 x + f1 x)"
+ by simp
+ also have "\<dots> = (\<Sum>X\<in>Pow A. (\<Prod>x\<in>X. - f2 x) * prod f1 (A - X))"
+ by (rule prod_add) fact+
+ also have "\<dots> = (\<Sum>X\<in>Pow A. (-1) ^ card X * (\<Prod>x\<in>X. f2 x) * prod f1 (A - X))"
+ by (simp add: prod_uminus)
+ finally show ?thesis .
+qed
+
+lemma prod_diff2:
+ fixes f1 f2 :: "'a \<Rightarrow> 'c :: comm_ring_1"
+ assumes finite: "finite A"
+ shows "(\<Prod>x\<in>A. f1 x - f2 x) = (\<Sum>X\<in>Pow A. (-1) ^ (card A - card X) * (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. f2 x))"
+proof -
+ have "(\<Prod>x\<in>A. f1 x - f2 x) = (\<Prod>x\<in>A. f1 x + (-f2 x))"
+ by simp
+ also have "\<dots> = (\<Sum>X\<in>Pow A. (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. -f2 x))"
+ by (rule prod_add) fact+
+ also have "\<dots> = (\<Sum>X\<in>Pow A. (-1) ^ card (A - X) * (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. f2 x))"
+ by (simp add: prod_uminus mult_ac)
+ also have "\<dots> = (\<Sum>X\<in>Pow A. (-1) ^ (card A - card X) * (\<Prod>x\<in>X. f1 x) * (\<Prod>x\<in>A-X. f2 x))"
+ using finite_subset[OF _ assms] by (intro sum.cong refl, subst card_Diff_subset) auto
+ finally show ?thesis .
+qed
+
end
--- a/src/HOL/Library/FuncSet.thy Mon Apr 21 08:24:58 2025 +0200
+++ b/src/HOL/Library/FuncSet.thy Fri Apr 18 10:58:16 2025 +0200
@@ -810,4 +810,37 @@
by blast
qed
+subsection \<open>Products of sums\<close>
+
+lemma prod_sum_PiE:
+ fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: comm_semiring_1"
+ assumes finite: "finite A" and finite: "\<And>x. x \<in> A \<Longrightarrow> finite (B x)"
+ shows "(\<Prod>x\<in>A. \<Sum>y\<in>B x. f x y) = (\<Sum>g\<in>PiE A B. \<Prod>x\<in>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 "(\<Sum>g\<in>Pi\<^sub>E (insert x A) B. \<Prod>x\<in>insert x A. f x (g x)) =
+ (\<Sum>g\<in>Pi\<^sub>E (insert x A) B. f x (g x) * (\<Prod>x'\<in>A. f x' (g x')))"
+ using insert by simp
+ also have "(\<lambda>g. \<Prod>x'\<in>A. f x' (g x')) = (\<lambda>g. \<Prod>x'\<in>A. f x' (if x' = x then undefined else g x'))"
+ using insert by (intro ext prod.cong) auto
+ also have "(\<Sum>g\<in>Pi\<^sub>E (insert x A) B. f x (g x) * \<dots> g) =
+ (\<Sum>(y,g)\<in>B x \<times> Pi\<^sub>E A B. f x y * (\<Prod>x'\<in>A. f x' (g x')))"
+ using insert.prems insert.hyps
+ by (intro sum.reindex_bij_witness[of _ "\<lambda>(y,g). g(x := y)" "\<lambda>g. (g x, g(x := undefined))"])
+ (auto simp: PiE_def extensional_def)
+ also have "\<dots> = (\<Sum>y\<in>B x. \<Sum>g\<in>Pi\<^sub>E A B. f x y * (\<Prod>x'\<in>A. f x' (g x')))"
+ by (subst sum.cartesian_product) auto
+ also have "\<dots> = (\<Sum>y\<in>B x. f x y) * (\<Sum>g\<in>Pi\<^sub>E A B. \<Prod>x'\<in>A. f x' (g x'))"
+ using insert by (subst sum.swap) (simp add: sum_distrib_left sum_distrib_right)
+ also have "(\<Sum>g\<in>Pi\<^sub>E A B. \<Prod>x'\<in>A. f x' (g x')) = (\<Prod>x\<in>A. \<Sum>y\<in>B x. f x y)"
+ using insert.prems by (intro insert.IH [symmetric]) auto
+ also have "(\<Sum>y\<in>B x. f x y) * \<dots> = (\<Prod>x\<in>insert x A. \<Sum>y\<in>B x. f x y)"
+ using insert.hyps by simp
+ finally show ?case ..
+qed
+
end