diff -r 4c3bc0d2568f -r 7448423e5dba src/HOL/Analysis/Infinite_Sum.thy
--- a/src/HOL/Analysis/Infinite_Sum.thy	Mon May 23 17:21:57 2022 +0100
+++ b/src/HOL/Analysis/Infinite_Sum.thy	Tue May 24 16:21:49 2022 +0100
@@ -696,11 +696,45 @@
   shows \<open>infsum f (A \<union> B) = infsum f A + infsum f B\<close>
   by (intro infsumI has_sum_Un_disjoint has_sum_infsum assms)  
 
-(* TODO move *)
-lemma (in uniform_space) cauchy_filter_complete_converges:
-  assumes "cauchy_filter F" "complete A" "F \<le> principal A" "F \<noteq> bot"
-  shows   "\<exists>c. F \<le> nhds c"
-  using assms unfolding complete_uniform by blast
+lemma norm_summable_imp_has_sum:
+  fixes f :: "nat \<Rightarrow> 'a :: banach"
+  assumes "summable (\<lambda>n. norm (f n))" and "f sums S"
+  shows   "has_sum f (UNIV :: nat set) S"
+  unfolding has_sum_def tendsto_iff eventually_finite_subsets_at_top
+proof (safe, goal_cases)
+  case (1 \<epsilon>)
+  from assms(1) obtain S' where S': "(\<lambda>n. norm (f n)) sums S'"
+    by (auto simp: summable_def)
+  with 1 obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> \<bar>S' - (\<Sum>i<n. norm (f i))\<bar> < \<epsilon>"
+    by (auto simp: tendsto_iff eventually_at_top_linorder sums_def dist_norm abs_minus_commute)
+  
+  show ?case
+  proof (rule exI[of _ "{..<N}"], safe, goal_cases)
+    case (2 Y)
+    from 2 have "(\<lambda>n. if n \<in> Y then 0 else f n) sums (S - sum f Y)"
+      by (intro sums_If_finite_set'[OF \<open>f sums S\<close>]) (auto simp: sum_negf)
+    hence "S - sum f Y = (\<Sum>n. if n \<in> Y then 0 else f n)"
+      by (simp add: sums_iff)
+    also have "norm \<dots> \<le> (\<Sum>n. norm (if n \<in> Y then 0 else f n))"
+      by (rule summable_norm[OF summable_comparison_test'[OF assms(1)]]) auto
+    also have "\<dots> \<le> (\<Sum>n. if n < N then 0 else norm (f n))"
+      using 2 by (intro suminf_le summable_comparison_test'[OF assms(1)]) auto
+    also have "(\<lambda>n. if n \<in> {..<N} then 0 else norm (f n)) sums (S' - (\<Sum>i<N. norm (f i)))" 
+      by (intro sums_If_finite_set'[OF S']) (auto simp: sum_negf)
+    hence "(\<Sum>n. if n < N then 0 else norm (f n)) = S' - (\<Sum>i<N. norm (f i))"
+      by (simp add: sums_iff)
+    also have "S' - (\<Sum>i<N. norm (f i)) \<le> \<bar>S' - (\<Sum>i<N. norm (f i))\<bar>" by simp
+    also have "\<dots> < \<epsilon>" by (rule N) auto
+    finally show ?case by (simp add: dist_norm norm_minus_commute)
+  qed auto
+qed
+
+lemma norm_summable_imp_summable_on:
+  fixes f :: "nat \<Rightarrow> 'a :: banach"
+  assumes "summable (\<lambda>n. norm (f n))"
+  shows   "f summable_on UNIV"
+  using norm_summable_imp_has_sum[OF assms, of "suminf f"] assms
+  by (auto simp: sums_iff summable_on_def dest: summable_norm_cancel)
 
 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: