# HG changeset patch
# User desharna
# Date 1743773403 -7200
# Node ID 9d457dfb56c5175a5e31722eb4ed91bc650603e3
# Parent  b3b8c278af235918aa2d329f5a889bda3ee44542# Parent  918c50e0447e9eafbe1fdf7f1832808d3a5ad100
merged

diff -r b3b8c278af23 -r 9d457dfb56c5 src/HOL/Analysis/Uniform_Limit.thy
--- a/src/HOL/Analysis/Uniform_Limit.thy	Wed Apr 02 11:26:40 2025 +0200
+++ b/src/HOL/Analysis/Uniform_Limit.thy	Fri Apr 04 15:30:03 2025 +0200
@@ -112,15 +112,14 @@
     by eventually_elim force
 qed
 
-
 subsection \<open>Exchange limits\<close>
-
-proposition swap_uniform_limit:
-  assumes f: "\<forall>\<^sub>F n in F. (f n \<longlongrightarrow> g n) (at x within S)"
+proposition swap_uniform_limit':
+  assumes f: "\<forall>\<^sub>F n in F. (f n \<longlongrightarrow> g n) G"
   assumes g: "(g \<longlongrightarrow> l) F"
   assumes uc: "uniform_limit S f h F"
+  assumes ev: "\<forall>\<^sub>F x in G. x \<in> S"
   assumes "\<not>trivial_limit F"
-  shows "(h \<longlongrightarrow> l) (at x within S)"
+  shows "(h \<longlongrightarrow> l) G"
 proof (rule tendstoI)
   fix e :: real
   define e' where "e' = e/3"
@@ -131,21 +130,19 @@
     by (simp add: dist_commute)
   moreover
   from f
-  have "\<forall>\<^sub>F n in F. \<forall>\<^sub>F x in at x within S. dist (g n) (f n x) < e'"
+  have "\<forall>\<^sub>F n in F. \<forall>\<^sub>F x in G. dist (g n) (f n x) < e'"
     by eventually_elim (auto dest!: tendstoD[OF _ \<open>0 < e'\<close>] simp: dist_commute)
   moreover
   from tendstoD[OF g \<open>0 < e'\<close>] have "\<forall>\<^sub>F x in F. dist l (g x) < e'"
     by (simp add: dist_commute)
   ultimately
-  have "\<forall>\<^sub>F _ in F. \<forall>\<^sub>F x in at x within S. dist (h x) l < e"
+  have "\<forall>\<^sub>F _ in F. \<forall>\<^sub>F x in G. dist (h x) l < e"
   proof eventually_elim
     case (elim n)
     note fh = elim(1)
     note gl = elim(3)
-    have "\<forall>\<^sub>F x in at x within S. x \<in> S"
-      by (auto simp: eventually_at_filter)
-    with elim(2)
     show ?case
+      using elim(2) ev
     proof eventually_elim
       case (elim x)
       from fh[rule_format, OF \<open>x \<in> S\<close>] elim(1)
@@ -155,10 +152,17 @@
       show ?case by (simp add: e'_def)
     qed
   qed
-  thus "\<forall>\<^sub>F x in at x within S. dist (h x) l < e"
+  thus "\<forall>\<^sub>F x in G. dist (h x) l < e"
     using eventually_happens by (metis \<open>\<not>trivial_limit F\<close>)
 qed
 
+corollary swap_uniform_limit:
+  assumes "\<forall>\<^sub>F n in F. (f n \<longlongrightarrow> g n) (at x within S)"
+  assumes "(g \<longlongrightarrow> l) F" "uniform_limit S f h F" "\<not>trivial_limit F"
+  shows "(h \<longlongrightarrow> l) (at x within S)"
+  using swap_uniform_limit' eventually_at_topological assms
+  by blast 
+
 
 subsection \<open>Uniform limit theorem\<close>
 
@@ -998,27 +1002,98 @@
   fixes a :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
   assumes "r < conv_radius a"
   shows "uniform_limit (cball \<xi> r) (\<lambda>n x. \<Sum>i<n. a i * (x - \<xi>) ^ i) (\<lambda>x. suminf (\<lambda>i. a i * (x - \<xi>) ^ i)) sequentially"
-using powser_uniformly_convergent [OF assms]
-by (simp add: Uniform_Limit.uniformly_convergent_uniform_limit_iff Series.suminf_eq_lim)
+  using powser_uniformly_convergent [OF assms]
+  by (simp add: Uniform_Limit.uniformly_convergent_uniform_limit_iff Series.suminf_eq_lim)
 
 lemma powser_continuous_suminf:
   fixes a :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
   assumes "r < conv_radius a"
   shows "continuous_on (cball \<xi> r) (\<lambda>x. suminf (\<lambda>i. a i * (x - \<xi>) ^ i))"
-apply (rule uniform_limit_theorem [OF _ powser_uniform_limit])
-apply (rule eventuallyI continuous_intros assms)+
-apply auto
-done
+  apply (rule uniform_limit_theorem [OF _ powser_uniform_limit])
+    apply (rule eventuallyI continuous_intros assms)+
+  apply auto
+  done
 
 lemma powser_continuous_sums:
   fixes a :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
   assumes r: "r < conv_radius a"
-      and sm: "\<And>x. x \<in> cball \<xi> r \<Longrightarrow> (\<lambda>n. a n * (x - \<xi>) ^ n) sums (f x)"
+    and sm: "\<And>x. x \<in> cball \<xi> r \<Longrightarrow> (\<lambda>n. a n * (x - \<xi>) ^ n) sums (f x)"
   shows "continuous_on (cball \<xi> r) f"
-apply (rule continuous_on_cong [THEN iffD1, OF refl _ powser_continuous_suminf [OF r]])
-using sm sums_unique by fastforce
+  apply (rule continuous_on_cong [THEN iffD1, OF refl _ powser_continuous_suminf [OF r]])
+  using sm sums_unique by fastforce
 
 lemmas uniform_limit_subset_union = uniform_limit_on_subset[OF uniform_limit_on_Union]
 
+subsection \<open>Tannery's Theorem\<close>
+
+text \<open>
+  Tannery's Theorem proves that, under certain boundedness conditions:
+  \[ \lim_{x\to\bar x} \sum_{k=0}^\infty f(k,n) = \sum_{k=0}^\infty \lim_{x\to\bar x} f(k,n) \]
+\<close>
+lemma tannerys_theorem:
+  fixes a :: "nat \<Rightarrow> _ \<Rightarrow> 'a :: {real_normed_algebra, banach}"
+  assumes limit: "\<And>k. ((\<lambda>n. a k n) \<longlongrightarrow> b k) F"
+  assumes bound: "eventually (\<lambda>(k,n). norm (a k n) \<le> M k) (at_top \<times>\<^sub>F F)"
+  assumes "summable M"
+  assumes [simp]: "F \<noteq> bot"
+  shows   "eventually (\<lambda>n. summable (\<lambda>k. norm (a k n))) F \<and>
+           summable (\<lambda>n. norm (b n)) \<and>
+           ((\<lambda>n. suminf (\<lambda>k. a k n)) \<longlongrightarrow> suminf b) F"
+proof (intro conjI allI)
+  show "eventually (\<lambda>n. summable (\<lambda>k. norm (a k n))) F"
+  proof -
+    have "eventually (\<lambda>n. eventually (\<lambda>k. norm (a k n) \<le> M k) at_top) F"
+      using eventually_eventually_prod_filter2[OF bound] by simp
+    thus ?thesis
+    proof eventually_elim
+      case (elim n)
+      show "summable (\<lambda>k. norm (a k n))"
+      proof (rule summable_comparison_test_ev)
+        show "eventually (\<lambda>k. norm (norm (a k n)) \<le> M k) at_top"
+          using elim by auto
+      qed fact
+    qed
+  qed
+
+  have bound': "eventually (\<lambda>k. norm (b k) \<le> M k) at_top"
+  proof -
+    have "eventually (\<lambda>k. eventually (\<lambda>n. norm (a k n) \<le> M k) F) at_top"
+      using eventually_eventually_prod_filter1[OF bound] by simp
+    thus ?thesis
+    proof eventually_elim
+      case (elim k)
+      show "norm (b k) \<le> M k"
+      proof (rule tendsto_upperbound)
+        show "((\<lambda>n. norm (a k n)) \<longlongrightarrow> norm (b k)) F"
+          by (intro tendsto_intros limit)
+      qed (use elim in auto)
+    qed
+  qed
+  show "summable (\<lambda>n. norm (b n))"
+    by (rule summable_comparison_test_ev[OF _ \<open>summable M\<close>]) (use bound' in auto)
+
+  from bound obtain Pf Pg where
+    *: "eventually Pf at_top" "eventually Pg F" "\<And>k n. Pf k \<Longrightarrow> Pg n \<Longrightarrow> norm (a k n) \<le> M k"
+    unfolding eventually_prod_filter by auto
+
+  show "((\<lambda>n. \<Sum>k. a k n) \<longlongrightarrow> (\<Sum>k. b k)) F"
+  proof (rule swap_uniform_limit')
+    show "(\<lambda>K. (\<Sum>k<K. b k)) \<longlonglongrightarrow> (\<Sum>k. b k)"
+      using \<open>summable (\<lambda>n. norm (b n))\<close>
+      by (intro summable_LIMSEQ) (auto dest: summable_norm_cancel)
+    show "\<forall>\<^sub>F K in sequentially. ((\<lambda>n. \<Sum>k<K. a k n) \<longlongrightarrow> (\<Sum>k<K. b k)) F"
+      by (intro tendsto_intros always_eventually allI limit)
+    show "\<forall>\<^sub>F x in F. x \<in> {n. Pg n}"
+      using *(2) by simp
+    show "uniform_limit {n. Pg n} (\<lambda>K n. \<Sum>k<K. a k n) (\<lambda>n. \<Sum>k. a k n) sequentially"
+    proof (rule Weierstrass_m_test_ev)
+      show "\<forall>\<^sub>F k in at_top. \<forall>n\<in>{n. Pg n}. norm (a k n) \<le> M k"
+        using *(1) by eventually_elim (use *(3) in auto)
+      show "summable M"
+        by fact
+    qed
+  qed auto
+qed
+
 end
 
diff -r b3b8c278af23 -r 9d457dfb56c5 src/HOL/Computational_Algebra/Formal_Laurent_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy	Wed Apr 02 11:26:40 2025 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy	Fri Apr 04 15:30:03 2025 +0200
@@ -912,6 +912,9 @@
 instance fls :: (comm_monoid_add) comm_monoid_add
   by (standard, transfer, auto simp: add.commute)
 
+lemma fls_nth_sum: "fls_nth (\<Sum>x\<in>A. f x) n = (\<Sum>x\<in>A. fls_nth (f x) n)"
+  by (induction A rule: infinite_finite_induct) auto
+
 
 subsubsection \<open>Subtraction and negatives\<close>
 
@@ -2923,6 +2926,20 @@
     by simp_all
 qed
 
+lemma one_plus_fls_X_powi_eq:
+  "(1 + fls_X) powi n = fps_to_fls (fps_binomial (of_int n :: 'a :: field_char_0))"
+proof (cases "n \<ge> 0")
+  case True
+  thus ?thesis
+    using fps_binomial_of_nat[of "nat n", where ?'a = 'a]
+    by (simp add: power_int_def fps_to_fls_power)
+next
+  case False
+  thus ?thesis
+    using fps_binomial_minus_of_nat[of "nat (-n)", where ?'a = 'a]
+    by (simp add: power_int_def fps_to_fls_power fps_inverse_power flip: fls_inverse_fps_to_fls)
+qed
+
 instance fls :: (field) field
   by (standard, simp_all add: field_simps)
 
diff -r b3b8c278af23 -r 9d457dfb56c5 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Wed Apr 02 11:26:40 2025 +0200
+++ b/src/HOL/Deriv.thy	Fri Apr 04 15:30:03 2025 +0200
@@ -1130,18 +1130,19 @@
   using DERIV_power [OF DERIV_ident] by simp
 
 lemma DERIV_power_int [derivative_intros]:
-  assumes [derivative_intros]: "(f has_field_derivative d) (at x within s)" and [simp]: "f x \<noteq> 0"
+  assumes [derivative_intros]: "(f has_field_derivative d) (at x within s)"
+  and "n \<ge> 0 \<or> f x \<noteq> 0"
   shows   "((\<lambda>x. power_int (f x) n) has_field_derivative
              (of_int n * power_int (f x) (n - 1) * d)) (at x within s)"
 proof (cases n rule: int_cases4)
   case (nonneg n)
   thus ?thesis 
-    by (cases "n = 0")
-       (auto intro!: derivative_eq_intros simp: field_simps power_int_diff
-             simp flip: power_Suc power_Suc2 power_add)
+    by (cases "n = 0"; cases "f x = 0")
+       (auto intro!: derivative_eq_intros simp: field_simps power_int_diff 
+                     power_diff power_int_0_left_if)
 next
   case (neg n)
-  thus ?thesis
+  thus ?thesis using assms(2)
     by (auto intro!: derivative_eq_intros simp: field_simps power_int_diff power_int_minus
              simp flip: power_Suc power_Suc2 power_add)
 qed
diff -r b3b8c278af23 -r 9d457dfb56c5 src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Wed Apr 02 11:26:40 2025 +0200
+++ b/src/HOL/Filter.thy	Fri Apr 04 15:30:03 2025 +0200
@@ -1132,6 +1132,38 @@
     by (intro exI[of _ P] exI[of _ "\<lambda>x. True"]) auto
 qed
 
+lemma eventually_eventually_prod_filter1:
+  assumes "eventually P (F \<times>\<^sub>F G)"
+  shows   "eventually (\<lambda>x. eventually (\<lambda>y. P (x, y)) G) F"
+proof -
+  from assms obtain Pf Pg where
+    *: "eventually Pf F" "eventually Pg G" "\<And>x y. Pf x \<Longrightarrow> Pg y \<Longrightarrow> P (x, y)"
+    unfolding eventually_prod_filter by auto
+  show ?thesis
+    using *(1)
+  proof eventually_elim
+    case x: (elim x)
+    show ?case
+      using *(2) by eventually_elim (use x *(3) in auto)
+  qed
+qed
+
+lemma eventually_eventually_prod_filter2:
+  assumes "eventually P (F \<times>\<^sub>F G)"
+  shows   "eventually (\<lambda>y. eventually (\<lambda>x. P (x, y)) F) G"
+proof -
+  from assms obtain Pf Pg where
+    *: "eventually Pf F" "eventually Pg G" "\<And>x y. Pf x \<Longrightarrow> Pg y \<Longrightarrow> P (x, y)"
+    unfolding eventually_prod_filter by auto
+  show ?thesis
+    using *(2)
+  proof eventually_elim
+    case y: (elim y)
+    show ?case
+      using *(1) by eventually_elim (use y *(3) in auto)
+  qed
+qed
+
 lemma INF_filter_bot_base:
   fixes F :: "'a \<Rightarrow> 'b filter"
   assumes *: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. F k \<le> F i \<sqinter> F j"
diff -r b3b8c278af23 -r 9d457dfb56c5 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Wed Apr 02 11:26:40 2025 +0200
+++ b/src/HOL/Fun.thy	Fri Apr 04 15:30:03 2025 +0200
@@ -368,6 +368,15 @@
 lemma bij_betw_singletonI [intro]: "f x = y \<Longrightarrow> bij_betw f {x} {y}"
   by auto
 
+lemma bij_betw_imp_empty_iff: "bij_betw f A B \<Longrightarrow> A = {} \<longleftrightarrow> B = {}"
+  unfolding bij_betw_def by blast
+
+lemma bij_betw_imp_Ex_iff: "bij_betw f {x. P x} {x. Q x} \<Longrightarrow> (\<exists>x. P x) \<longleftrightarrow> (\<exists>x. Q x)"
+  unfolding bij_betw_def by blast
+
+lemma bij_betw_imp_Bex_iff: "bij_betw f {x\<in>A. P x} {x\<in>B. Q x} \<Longrightarrow> (\<exists>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>B. Q x)"
+  unfolding bij_betw_def by blast
+
 lemma bij_betw_apply: "\<lbrakk>bij_betw f A B; a \<in> A\<rbrakk> \<Longrightarrow> f a \<in> B"
   unfolding bij_betw_def by auto
 
diff -r b3b8c278af23 -r 9d457dfb56c5 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Wed Apr 02 11:26:40 2025 +0200
+++ b/src/HOL/Groups_Big.thy	Fri Apr 04 15:30:03 2025 +0200
@@ -1580,6 +1580,16 @@
   qed
 qed
 
+lemma prod_uminus: "(\<Prod>x\<in>A. -f x :: 'a :: comm_ring_1) = (-1) ^ card A * (\<Prod>x\<in>A. f x)"
+  by (induction A rule: infinite_finite_induct) (auto simp: algebra_simps)
+
+lemma prod_diff:
+  fixes f :: "'a \<Rightarrow> 'b :: field"
+  assumes "finite A" "B \<subseteq> A" "\<And>x. x \<in> B \<Longrightarrow> f x \<noteq> 0"
+  shows   "prod f (A - B) = prod f A / prod f B"
+  by (metis assms finite_subset nonzero_eq_divide_eq prod.subset_diff
+      prod_zero_iff)
+
 lemma sum_zero_power [simp]: "(\<Sum>i\<in>A. c i * 0^i) = (if finite A \<and> 0 \<in> A then c 0 else 0)"
   for c :: "nat \<Rightarrow> 'a::division_ring"
   by (induct A rule: infinite_finite_induct) auto
@@ -1712,10 +1722,22 @@
   for y :: "'a::comm_monoid_mult"
   by (induct A rule: infinite_finite_induct) simp_all
 
+lemma prod_diff_swap:
+  fixes f :: "'a \<Rightarrow> 'b :: comm_ring_1"
+  shows "prod (\<lambda>x. f x - g x) A = (-1) ^ card A * prod (\<lambda>x. g x - f x) A"
+  using prod.distrib[of "\<lambda>_. -1" "\<lambda>x. f x - g x" A]
+  by simp
+
 lemma prod_power_distrib: "prod f A ^ n = prod (\<lambda>x. (f x) ^ n) A"
   for f :: "'a \<Rightarrow> 'b::comm_semiring_1"
   by (induct A rule: infinite_finite_induct) (auto simp add: power_mult_distrib)
 
+lemma power_inject_exp':
+  assumes "a \<noteq> 1" "a > (0 :: 'a :: linordered_semidom)"
+  shows   "a ^ m = a ^ n \<longleftrightarrow> m = n"
+  by (metis assms not_less_iff_gr_or_eq order_le_less power_decreasing_iff
+      power_inject_exp)
+
 lemma power_sum: "c ^ (\<Sum>a\<in>A. f a) = (\<Prod>a\<in>A. c ^ f a)"
   by (induct A rule: infinite_finite_induct) (simp_all add: power_add)
 
diff -r b3b8c278af23 -r 9d457dfb56c5 src/HOL/Library/Infinite_Typeclass.thy
--- a/src/HOL/Library/Infinite_Typeclass.thy	Wed Apr 02 11:26:40 2025 +0200
+++ b/src/HOL/Library/Infinite_Typeclass.thy	Fri Apr 04 15:30:03 2025 +0200
@@ -27,6 +27,9 @@
     by auto
 qed
 
+lemma arb_inj_on_finite_infinite: "finite(A :: 'b set) \<Longrightarrow> \<exists>f :: 'b \<Rightarrow> 'a. inj_on f A"
+by (meson arb_finite_subset card_le_inj infinite_imp_nonempty)
+
 lemma arb_countable_map: "finite Y \<Longrightarrow> \<exists>f :: (nat \<Rightarrow> 'a). inj f \<and> range f \<subseteq> UNIV - Y"
   using infinite_UNIV
   by (auto simp: infinite_countable_subset)