# HG changeset patch
# User paulson
# Date 1677756894 0
# Node ID df1150ec6cd770e94ae05a9e74e4bb8597631e0c
# Parent  5b3139a6b0de674135326ceb6ebcffa1122f5560# Parent  da41823d09a7aba054d6bcd5fc7e6730dde47f00
merged

diff -r 5b3139a6b0de -r df1150ec6cd7 NEWS
--- a/NEWS	Wed Mar 01 21:05:09 2023 +0000
+++ b/NEWS	Thu Mar 02 11:34:54 2023 +0000
@@ -231,6 +231,13 @@
       totalp_on_multpDM
       totalp_on_multpHO
 
+* HOL-Algebra: new theories SimpleGroups (simple groups) 
+  and SndIsomorphismGrp (second isomorphism theorem for groups), 
+  by Jakob von Raumer
+
+* HOL-Analysis and HOL-Complex_Analysis:  much new material, due to
+   Manuel Eberl and Wenda Li.
+
 * Mirabelle:
   - Added session to output directory structure. Minor INCOMPATIBILITY.
 
diff -r 5b3139a6b0de -r df1150ec6cd7 src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Wed Mar 01 21:05:09 2023 +0000
+++ b/src/HOL/Analysis/Further_Topology.thy	Thu Mar 02 11:34:54 2023 +0000
@@ -3333,7 +3333,7 @@
       then have "z \<noteq> 0" by auto
       have "(w/z)^n = 1"
         by (metis False divide_self_if eq power_divide power_one)
-      then obtain j where j: "w / z = exp (2 * of_real pi * \<i> * j / n)" and "j < n"
+      then obtain j::nat where j: "w / z = exp (2 * of_real pi * \<i> * j / n)" and "j < n"
         using Suc_leI assms \<open>2 \<le> n\<close> complex_roots_unity [THEN eqset_imp_iff, of n "w/z"]
         by force
       have "cmod (w/z - 1) < 2 * sin (pi / real n)"
diff -r 5b3139a6b0de -r df1150ec6cd7 src/HOL/Analysis/Uniform_Limit.thy
--- a/src/HOL/Analysis/Uniform_Limit.thy	Wed Mar 01 21:05:09 2023 +0000
+++ b/src/HOL/Analysis/Uniform_Limit.thy	Thu Mar 02 11:34:54 2023 +0000
@@ -6,7 +6,7 @@
 section \<open>Uniform Limit and Uniform Convergence\<close>
 
 theory Uniform_Limit
-imports Connected Summation_Tests
+imports Connected Summation_Tests Infinite_Sum
 begin
 
 
@@ -560,12 +560,67 @@
   shows   "uniformly_convergent_on A (\<lambda>n x. \<Sum>i<n. f i x)"
   unfolding uniformly_convergent_on_def by (rule exI, rule Weierstrass_m_test[OF assms])
 
-lemma uniform_limit_eq_rhs: "uniform_limit X f l F \<Longrightarrow> l = m \<Longrightarrow> uniform_limit X f m F"
-  by simp
+
+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 summable: "M summable_on X"
+  shows "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)"
+proof (rule uniform_limitI)
+  fix \<epsilon> :: real
+  assume "\<epsilon> > 0"
+  define S where "S = (\<lambda>y. \<Sum>\<^sub>\<infinity>x\<in>X. f x y)"
+  have S: "((\<lambda>x. f x y) has_sum S y) X" if y: "y \<in> Y" for y
+    unfolding S_def 
+  proof (rule has_sum_infsum)
+    have "(\<lambda>x. norm (f x y)) summable_on X"
+      by (rule abs_summable_on_comparison_test'[OF summable norm_le]) (use y in auto)
+    thus "(\<lambda>x. f x y) summable_on X"
+      by (metis abs_summable_summable)
+  qed
+
+  define T where "T = (\<Sum>\<^sub>\<infinity>x\<in>X. M x)"
+  have T: "(M has_sum T) X"
+    unfolding T_def by (simp add: local.summable)
+  have M_summable: "M summable_on X'" if "X' \<subseteq> X" for X'
+    using local.summable summable_on_subset_banach that by blast
+
+  have f_summable: "(\<lambda>x. f x y) summable_on X'" if "X' \<subseteq> X" "y \<in> Y" for X' y
+    using S summable_on_def summable_on_subset_banach that by blast
+  have "eventually (\<lambda>X'. dist (\<Sum>x\<in>X'. M x) T < \<epsilon>) (finite_subsets_at_top X)"
+    using T \<open>\<epsilon> > 0\<close> unfolding T_def has_sum_def tendsto_iff by blast
+  moreover have "eventually (\<lambda>X'. finite X' \<and> X' \<subseteq> X) (finite_subsets_at_top X)"
+    by (simp add: eventually_finite_subsets_at_top_weakI)
+  ultimately show "\<forall>\<^sub>F X' in finite_subsets_at_top X. \<forall>y\<in>Y. dist (\<Sum>x\<in>X'. f x y) (\<Sum>\<^sub>\<infinity>x\<in>X. f x y) < \<epsilon>"
+  proof eventually_elim
+    case X': (elim X')
+    show "\<forall>y\<in>Y. dist (\<Sum>x\<in>X'. f x y) (\<Sum>\<^sub>\<infinity>x\<in>X. f x y) < \<epsilon>"
+    proof
+      fix y assume y: "y \<in> Y"
+      have 1: "((\<lambda>x. f x y) has_sum (S y - (\<Sum>x\<in>X'. f x y))) (X - X')"
+        using X' y by (intro has_sum_Diff S has_sum_finite[of X'] f_summable) auto
+      have 2: "(M has_sum (T - (\<Sum>x\<in>X'. M x))) (X - X')"
+        using X' y by (intro has_sum_Diff T has_sum_finite[of X'] M_summable) auto
+      have "dist (\<Sum>x\<in>X'. f x y) (\<Sum>\<^sub>\<infinity>x\<in>X. f x y) = norm (S y - (\<Sum>x\<in>X'. f x y))"
+        by (simp add: dist_norm norm_minus_commute S_def)
+      also have "norm (S y - (\<Sum>x\<in>X'. f x y)) \<le> (\<Sum>\<^sub>\<infinity>x\<in>X-X'. M x)"
+        using 2 y by (intro norm_infsum_le[OF 1 _ norm_le]) (auto simp: infsumI)
+      also have "\<dots> = T - (\<Sum>x\<in>X'. M x)"
+        using 2 by (auto simp: infsumI)
+      also have "\<dots> < \<epsilon>"
+        using X' by (simp add: dist_norm)
+      finally show "dist (\<Sum>x\<in>X'. f x y) (\<Sum>\<^sub>\<infinity>x\<in>X. f x y) < \<epsilon>" .
+    qed
+  qed
+qed
 
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Structural introduction rules\<close>
 
+lemma uniform_limit_eq_rhs: "uniform_limit X f l F \<Longrightarrow> l = m \<Longrightarrow> uniform_limit X f m F"
+  by simp
+
 named_theorems uniform_limit_intros "introduction rules for uniform_limit"
 setup \<open>
   Global_Theory.add_thms_dynamic (\<^binding>\<open>uniform_limit_eq_intros\<close>,
diff -r 5b3139a6b0de -r df1150ec6cd7 src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Wed Mar 01 21:05:09 2023 +0000
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Thu Mar 02 11:34:54 2023 +0000
@@ -12,6 +12,9 @@
   "HOL-Library.Multiset"
 begin
 
+text \<open>Conflicting notation from \<^theory>\<open>HOL-Analysis.Infinite_Sum\<close>\<close>
+no_notation Infinite_Sum.abs_summable_on (infixr "abs'_summable'_on" 46)
+
 lemma AE_emeasure_singleton:
   assumes x: "emeasure M {x} \<noteq> 0" and ae: "AE x in M. P x" shows "P x"
 proof -
diff -r 5b3139a6b0de -r df1150ec6cd7 src/HOL/Probability/Product_PMF.thy
--- a/src/HOL/Probability/Product_PMF.thy	Wed Mar 01 21:05:09 2023 +0000
+++ b/src/HOL/Probability/Product_PMF.thy	Thu Mar 02 11:34:54 2023 +0000
@@ -7,6 +7,9 @@
   imports Probability_Mass_Function Independent_Family
 begin
 
+text \<open>Conflicting notation from \<^theory>\<open>HOL-Analysis.Infinite_Sum\<close>\<close>
+no_notation Infinite_Sum.abs_summable_on (infixr "abs'_summable'_on" 46)
+
 subsection \<open>Preliminaries\<close>
 
 lemma pmf_expectation_eq_infsetsum: "measure_pmf.expectation p f = infsetsum (\<lambda>x. pmf p x * f x) UNIV"
diff -r 5b3139a6b0de -r df1150ec6cd7 src/HOL/Probability/SPMF.thy
--- a/src/HOL/Probability/SPMF.thy	Wed Mar 01 21:05:09 2023 +0000
+++ b/src/HOL/Probability/SPMF.thy	Thu Mar 02 11:34:54 2023 +0000
@@ -2338,20 +2338,23 @@
 lemma scale_scale_spmf:
   "scale_spmf r (scale_spmf r' p) = scale_spmf (r * max 0 (min (inverse (weight_spmf p)) r')) p"
   (is "?lhs = ?rhs")
-proof(rule spmf_eqI)
-  fix i
-  have "max 0 (min (1 / weight_spmf p) r') *
-    max 0 (min (1 / min 1 (weight_spmf p * max 0 r')) r) =
-    max 0 (min (1 / weight_spmf p) (r * max 0 (min (1 / weight_spmf p) r')))"
-  proof(cases "weight_spmf p > 0")
-    case False
-    thus ?thesis by(simp add: not_less weight_spmf_le_0)
-  next
-    case True
-    thus ?thesis by(simp add: field_simps max_def min.absorb_iff2[symmetric])(auto simp add: min_def field_simps zero_le_mult_iff)
+proof(cases "weight_spmf p > 0")
+  case False
+  thus ?thesis
+    by (simp add: weight_spmf_eq_0 zero_less_measure_iff)
+next
+  case True
+  show ?thesis
+  proof(rule spmf_eqI)
+    fix i
+    have "max 0 (min (1 / weight_spmf p) r') * max 0 (min (1 / min 1 (weight_spmf p * max 0 r')) r) =
+          max 0 (min (1 / weight_spmf p) (r * max 0 (min (1 / weight_spmf p) r')))"
+      using True
+      by(simp add: field_simps max_def min.absorb_iff2[symmetric])(auto simp add: min_def field_simps zero_le_mult_iff)
+    then show "spmf ?lhs i = spmf ?rhs i"
+      apply (subst spmf_scale_spmf)+  (*FOR SOME REASON we now get linarith_split_limit exceeded if simp is used*)
+      by (metis (no_types, opaque_lifting) inverse_eq_divide mult.commute mult.left_commute weight_scale_spmf)
   qed
-  then show "spmf ?lhs i = spmf ?rhs i"
-    by(simp add: spmf_scale_spmf field_simps weight_scale_spmf)
 qed
 
 lemma scale_scale_spmf' [simp]: