More migration from Theta_Functions_Library

--- a/src/HOL/Analysis/Infinite_Sum.thy	Mon Mar 24 21:24:03 2025 +0000
+++ b/src/HOL/Analysis/Infinite_Sum.thy	Tue Mar 25 21:19:26 2025 +0000
@@ -106,9 +106,18 @@
   shows \<open>infsum f A = 0\<close>
   by (simp add: assms infsum_def)
 
+lemma has_sum_unique:
+  fixes f :: "_ \<Rightarrow> 'a :: {topological_comm_monoid_add, t2_space}"
+  assumes "(f has_sum x) A" "(f has_sum y) A"
+  shows "x = y"
+  using assms infsumI by blast
+
 lemma summable_iff_has_sum_infsum: "f summable_on A \<longleftrightarrow> (f has_sum (infsum f A)) A"
   using infsumI summable_on_def by blast
 
+lemma has_sum_iff: "(f has_sum S) A \<longleftrightarrow> f summable_on A \<and> infsum f A = S"
+  using infsumI summable_iff_has_sum_infsum by blast
+
 lemma has_sum_infsum[simp]:
   assumes \<open>f summable_on S\<close>
   shows \<open>(f has_sum (infsum f S)) S\<close>
@@ -388,6 +397,41 @@
   shows "infsum f F = sum f F"
   by (simp add: assms infsumI)
 
+lemma has_sum_finiteI: "finite A \<Longrightarrow> S = sum f A \<Longrightarrow> (f has_sum S) A"
+  by simp
+
+lemma has_sum_strict_mono_neutral:
+  fixes f :: "'a \<Rightarrow> 'b :: {ordered_ab_group_add, topological_ab_group_add, linorder_topology}"
+  assumes \<open>(f has_sum a) A\<close> and "(g has_sum b) B"
+  assumes \<open>\<And>x. x \<in> A\<inter>B \<Longrightarrow> f x \<le> g x\<close>
+  assumes \<open>\<And>x. x \<in> A-B \<Longrightarrow> f x \<le> 0\<close>
+  assumes \<open>\<And>x. x \<in> B-A \<Longrightarrow> g x \<ge> 0\<close>
+  assumes \<open>x \<in> B\<close> \<open>if x \<in> A then f x < g x else 0 < g x\<close>
+  shows "a < b"
+proof -
+  define y where "y = (if x \<in> A then f x else 0)"
+  have "a - y \<le> b - g x"
+  proof (rule has_sum_mono_neutral)
+    show "(f has_sum (a - y)) (A - (if x \<in> A then {x} else {}))"
+      by (intro has_sum_Diff assms has_sum_finiteI) (auto simp: y_def)
+    show "(g has_sum (b - g x)) (B - {x})"
+      by (intro has_sum_Diff assms has_sum_finiteI) (use assms in auto)
+  qed (use assms in \<open>auto split: if_splits\<close>)
+  moreover have "y < g x"
+    using assms(3,4,5)[of x] assms(6-) by (auto simp: y_def split: if_splits)
+  ultimately show ?thesis
+    by (metis diff_strict_left_mono diff_strict_mono leD neqE)
+qed
+
+lemma has_sum_strict_mono:
+  fixes f :: "'a \<Rightarrow> 'b :: {ordered_ab_group_add, topological_ab_group_add, linorder_topology}"
+  assumes \<open>(f has_sum a) A\<close> and "(g has_sum b) A"
+  assumes \<open>\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x\<close>
+  assumes \<open>x \<in> A\<close> \<open>f x < g x\<close>
+  shows "a < b"
+  by (rule has_sum_strict_mono_neutral[OF assms(1,2), where x = x])
+     (use assms(3-) in auto)
+
 lemma has_sum_finite_approximation:
   fixes f :: "'a \<Rightarrow> 'b::{comm_monoid_add,metric_space}"
   assumes "(f has_sum x) A" and "\<epsilon> > 0"
@@ -708,6 +752,39 @@
   using norm_summable_imp_has_sum[OF assms, of "suminf f"] assms
   by (auto simp: sums_iff summable_on_def dest: summable_norm_cancel)
 
+lemma sums_nonneg_imp_has_sum_strong:
+  assumes "f sums (S::real)" "eventually (\<lambda>n. f n \<ge> 0) sequentially"
+  shows   "(f has_sum S) UNIV"
+proof -
+  from assms(2) obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> f n \<ge> 0"
+    by (auto simp: eventually_at_top_linorder)
+  from assms(1) have "summable f"
+    by (simp add: sums_iff)
+  hence "summable (\<lambda>n. f (n + N))"
+    by (rule summable_ignore_initial_segment)
+  hence "summable (\<lambda>n. norm (f (n + N)))"
+    using N by simp
+  hence "summable (\<lambda>n. norm (f n))"
+    using summable_iff_shift by blast
+  with assms(1) show ?thesis
+    using norm_summable_imp_has_sum by blast
+qed
+
+lemma sums_nonneg_imp_has_sum:
+  assumes "f sums (S::real)" and "\<And>n. f n \<ge> 0"
+  shows   "(f has_sum S) UNIV"
+  by (rule sums_nonneg_imp_has_sum_strong) (use assms in auto)
+
+lemma summable_nonneg_imp_summable_on_strong:
+  assumes "summable f" "eventually (\<lambda>n. f n \<ge> (0::real)) sequentially"
+  shows   "f summable_on UNIV"
+  using assms has_sum_iff sums_nonneg_imp_has_sum_strong by blast
+
+lemma summable_nonneg_imp_summable_on:
+  assumes "summable f" "\<And>n. f n \<ge> (0::real)"
+  shows   "f summable_on UNIV"
+  by (rule summable_nonneg_imp_summable_on_strong) (use assms in auto)
+
 text \<open>The following lemma indeed needs a complete space (as formalized by the premise \<^term>\<open>complete UNIV\<close>).
   The following two counterexamples show this:
   \begin{itemize}
@@ -2759,6 +2836,15 @@
   shows   "(g has_sum s) S = (h has_sum s') T"
   by (smt (verit, del_insts) assms bij_betwI' has_sum_cong has_sum_reindex_bij_betw)
 
+lemma summable_on_reindex_bij_witness:
+  assumes "\<And>a. a \<in> S \<Longrightarrow> i (j a) = a"
+  assumes "\<And>a. a \<in> S \<Longrightarrow> j a \<in> T"
+  assumes "\<And>b. b \<in> T \<Longrightarrow> j (i b) = b"
+  assumes "\<And>b. b \<in> T \<Longrightarrow> i b \<in> S"
+  assumes "\<And>a. a \<in> S \<Longrightarrow> h (j a) = g a"
+  shows   "g summable_on S \<longleftrightarrow> h summable_on T"
+  using has_sum_reindex_bij_witness[of S i j T h g, OF assms]
+  by (simp add: summable_on_def)
 
 lemma has_sum_homomorphism:
   assumes "(f has_sum S) A" "h 0 = 0" "\<And>a b. h (a + b) = h a + h b" "continuous_on UNIV h"
@@ -2835,6 +2921,19 @@
   shows   "infsum (\<lambda>x. mult c (f x)) A = mult c (infsum f A)"
   by (metis assms infsum_0 infsum_bounded_linear_strong)
 
+lemma has_sum_scaleR:
+  fixes f :: "'a \<Rightarrow> 'b :: real_normed_vector"
+  assumes "(f has_sum S) A"
+  shows   "((\<lambda>x. c *\<^sub>R f x) has_sum (c *\<^sub>R S)) A"
+  using has_sum_bounded_linear[OF bounded_linear_scaleR_right[of c], of f A S] assms by simp
+
+lemma has_sum_scaleR_iff:
+  fixes f :: "'a \<Rightarrow> 'b :: real_normed_vector"
+  assumes "c \<noteq> 0"
+  shows   "((\<lambda>x. c *\<^sub>R f x) has_sum S) A \<longleftrightarrow> (f has_sum (S /\<^sub>R c)) A"
+  using has_sum_scaleR[of f A "S /\<^sub>R c" c] has_sum_scaleR[of "\<lambda>x. c *\<^sub>R f x" A S "inverse c"] assms
+  by auto
+
 lemma has_sum_of_nat: "(f has_sum S) A \<Longrightarrow> ((\<lambda>x. of_nat (f x)) has_sum of_nat S) A"
   by (erule has_sum_homomorphism) (auto intro!: continuous_intros)
 
@@ -2847,6 +2946,31 @@
 lemma summable_on_of_int: "f summable_on A \<Longrightarrow> (\<lambda>x. of_int (f x)) summable_on A"
   by (erule summable_on_homomorphism) (auto intro!: continuous_intros)
 
+lemma summable_on_of_real:
+  "f summable_on A \<Longrightarrow> (\<lambda>x. of_real (f x) :: 'a :: real_normed_algebra_1) summable_on A"
+  using summable_on_bounded_linear[of "of_real :: real \<Rightarrow> 'a", OF bounded_linear_of_real, of f A]
+  by simp
+
+lemma has_sum_of_real_iff:
+  "((\<lambda>x. of_real (f x) :: 'a :: real_normed_div_algebra) has_sum (of_real c)) A \<longleftrightarrow> 
+   (f has_sum c) A"
+proof -
+  have "((\<lambda>x. of_real (f x) :: 'a) has_sum (of_real c)) A \<longleftrightarrow>
+        (sum (\<lambda>x. of_real (f x) :: 'a) \<longlongrightarrow> of_real c) (finite_subsets_at_top A)"
+    by (simp add: has_sum_def)
+  also have "sum (\<lambda>x. of_real (f x) :: 'a) = (\<lambda>X. of_real (sum f X))"
+    by simp
+  also have "((\<lambda>X. of_real (sum f X) :: 'a) \<longlongrightarrow> of_real c) (finite_subsets_at_top A) \<longleftrightarrow> 
+             (f has_sum c) A"
+    unfolding has_sum_def tendsto_of_real_iff ..
+  finally show ?thesis .
+qed
+
+lemma has_sum_of_real:
+  "(f has_sum S) A \<Longrightarrow> ((\<lambda>x. of_real (f x) :: 'a :: real_normed_algebra_1) has_sum of_real S) A"
+  using has_sum_bounded_linear[of "of_real :: real \<Rightarrow> 'a", OF bounded_linear_of_real, of f A S]
+  by simp
+
 lemma summable_on_discrete_iff:
   fixes f :: "'a \<Rightarrow> 'b :: {discrete_topology, topological_comm_monoid_add, cancel_comm_monoid_add}"
   shows "f summable_on A \<longleftrightarrow> finite {x\<in>A. f x \<noteq> 0}"
@@ -3027,9 +3151,6 @@
   shows "f summable_on insert x A \<longleftrightarrow> f summable_on A"
   using summable_on_union[of f A "{x}"] by (auto intro: summable_on_subset)
 
-lemma has_sum_finiteI: "finite A \<Longrightarrow> S = sum f A \<Longrightarrow> (f has_sum S) A"
-  by simp
-
 lemma has_sum_insert:
   fixes f :: "'a \<Rightarrow> 'b :: topological_comm_monoid_add"
   assumes "x \<notin> A" and "(f has_sum S) A"
@@ -3131,11 +3252,32 @@
   qed (insert Y(1,2), auto simp: Y1_def)
 qed
 
-lemma has_sum_unique:
-  fixes f :: "_ \<Rightarrow> 'a :: {topological_comm_monoid_add, t2_space}"
-  assumes "(f has_sum x) A" "(f has_sum y) A"
-  shows "x = y"
-  using assms unfolding has_sum_def using tendsto_unique finite_subsets_at_top_neq_bot by blast
+lemma has_sum_finite_iff: 
+  fixes S :: "'a :: {topological_comm_monoid_add,t2_space}"
+  assumes "finite A"
+  shows   "(f has_sum S) A \<longleftrightarrow> S = (\<Sum>x\<in>A. f x)"
+proof
+  assume "S = (\<Sum>x\<in>A. f x)"
+  thus "(f has_sum S) A"
+    by (intro has_sum_finiteI assms)
+next
+  assume "(f has_sum S) A"
+  moreover have "(f has_sum (\<Sum>x\<in>A. f x)) A"
+    by (intro has_sum_finiteI assms) auto
+  ultimately show "S = (\<Sum>x\<in>A. f x)"
+    using has_sum_unique by blast
+qed
+
+lemma has_sum_finite_neutralI:
+  assumes "finite B" "B \<subseteq> A" "\<And>x. x \<in> A - B \<Longrightarrow> f x = 0" "c = (\<Sum>x\<in>B. f x)"
+  shows   "(f has_sum c) A"
+proof -
+  have "(f has_sum c) B"
+    by (rule has_sum_finiteI) (use assms in auto)
+  also have "?this \<longleftrightarrow> (f has_sum c) A"
+    by (intro has_sum_cong_neutral) (use assms in auto)
+  finally show ?thesis .
+qed
 
 lemma has_sum_SigmaI:
   fixes f :: "_ \<Rightarrow> 'a :: {topological_comm_monoid_add, t3_space}"

--- a/src/HOL/Analysis/Uniform_Limit.thy	Mon Mar 24 21:24:03 2025 +0000
+++ b/src/HOL/Analysis/Uniform_Limit.thy	Tue Mar 25 21:19:26 2025 +0000
@@ -631,6 +631,22 @@
   qed
 qed
 
+lemma Weierstrass_m_test_general':
+  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c :: banach"
+  fixes M :: "'a \<Rightarrow> real"
+  assumes norm_le:  "\<And>x y. x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> norm (f x y) \<le> M x"
+  assumes has_sum: "\<And>y. y \<in> Y \<Longrightarrow> ((\<lambda>x. f x y) has_sum S y) X"
+  assumes summable: "M summable_on X"
+  shows "uniform_limit Y (\<lambda>X y. \<Sum>x\<in>X. f x y) S (finite_subsets_at_top X)"
+proof -
+  have "uniform_limit Y (\<lambda>X y. \<Sum>x\<in>X. f x y) (\<lambda>y. \<Sum>\<^sub>\<infinity>x\<in>X. f x y) (finite_subsets_at_top X)"
+    using norm_le summable by (rule Weierstrass_m_test_general)
+  also have "?this \<longleftrightarrow> ?thesis"
+    by (intro uniform_limit_cong refl always_eventually allI ballI)
+       (use has_sum in \<open>auto simp: has_sum_iff\<close>)
+  finally show ?thesis .
+qed
+
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Structural introduction rules\<close>
 

--- a/src/HOL/Complex.thy	Mon Mar 24 21:24:03 2025 +0000
+++ b/src/HOL/Complex.thy	Tue Mar 25 21:19:26 2025 +0000
@@ -878,6 +878,12 @@
 lemma cis_divide: "cis a / cis b = cis (a - b)"
   by (simp add: divide_complex_def cis_mult)
 
+lemma cis_power_int: "cis x powi n = cis (of_int n * x)"
+  by (auto simp: power_int_def DeMoivre)  
+
+lemma complex_cnj_power_int [simp]: "cnj (x powi n) = cnj x powi n"
+  by (auto simp: power_int_def)
+
 lemma divide_conv_cnj: "norm z = 1 \<Longrightarrow> x / z = x * cnj z"
   by (metis complex_div_cnj div_by_1 mult_1 of_real_1 power2_eq_square)
 

--- a/src/HOL/Int.thy	Mon Mar 24 21:24:03 2025 +0000
+++ b/src/HOL/Int.thy	Tue Mar 25 21:19:26 2025 +0000
@@ -1881,6 +1881,15 @@
 lemma power_int_mult: "power_int (x :: 'a) (m * n) = power_int (power_int x m) n"
   by (auto simp: power_int_def zero_le_mult_iff simp flip: power_mult power_inverse nat_mult_distrib)
 
+lemma power_int_power: "(a ^ b :: 'a :: division_ring) powi c = a powi (int b * c)"
+  by (subst power_int_mult) simp
+
+lemma power_int_power': "(a powi b :: 'a :: division_ring) ^ c = a powi (b * int c)"
+  by (simp add: power_int_mult)
+
+lemma power_int_nonneg_exp: "n \<ge> 0 \<Longrightarrow> x powi n = x ^ nat n"
+  by (simp add: power_int_def)
+
 end
 
 context

--- a/src/HOL/NthRoot.thy	Mon Mar 24 21:24:03 2025 +0000
+++ b/src/HOL/NthRoot.thy	Tue Mar 25 21:19:26 2025 +0000
@@ -548,16 +548,14 @@
 
 lemma not_real_square_gt_zero [simp]: "\<not> 0 < x * x \<longleftrightarrow> x = 0"
   for x :: real
-  apply auto
-  using linorder_less_linear [where x = x and y = 0]
-  apply (simp add: zero_less_mult_iff)
-  done
+  by (metis linorder_neq_iff zero_less_mult_iff)
 
 lemma real_sqrt_abs2 [simp]: "sqrt (x * x) = \<bar>x\<bar>"
-  apply (subst power2_eq_square [symmetric])
-  apply (rule real_sqrt_abs)
-  done
+  by (simp add: real_sqrt_mult)
 
+lemma real_sqrt_abs': "sqrt \<bar>x\<bar> = \<bar>sqrt x\<bar>"
+  by (metis real_sqrt_abs2 real_sqrt_mult)
+    
 lemma real_inv_sqrt_pow2: "0 < x \<Longrightarrow> (inverse (sqrt x))\<^sup>2 = inverse x"
   by (simp add: power_inverse)
 

--- a/src/HOL/Transcendental.thy	Mon Mar 24 21:24:03 2025 +0000
+++ b/src/HOL/Transcendental.thy	Tue Mar 25 21:19:26 2025 +0000
@@ -3978,12 +3978,24 @@
 lemma sin_npi2_numeral [simp]: "sin (pi * Num.numeral n) = 0"
   by (metis of_nat_numeral sin_npi2)
 
+lemma sin_npi_complex' [simp]: "sin (of_nat n * of_real pi) = 0"
+  by (metis of_real_0 of_real_mult of_real_of_nat_eq sin_npi sin_of_real)
+
 lemma cos_npi_numeral [simp]: "cos (Num.numeral n * pi) = (- 1) ^ Num.numeral n"
   by (metis cos_npi of_nat_numeral)
 
 lemma cos_npi2_numeral [simp]: "cos (pi * Num.numeral n) = (- 1) ^ Num.numeral n"
   by (metis cos_npi2 of_nat_numeral)
 
+lemma cos_npi_complex' [simp]: "cos (of_nat n * of_real pi) = (-1) ^ n" for n
+proof -
+  have "cos (of_nat n * of_real pi :: 'a) = of_real (cos (real n * pi))"
+    by (subst cos_of_real [symmetric]) simp
+  also have "cos (real n * pi) = (-1) ^ n"
+    by simp
+  finally show ?thesis by simp
+qed
+
 lemma cos_two_pi [simp]: "cos (2 * pi) = 1"
   by (simp add: cos_double)