# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1525871239 -3600
# Node ID 137d5d0112bb25c2520142f6203f9bd89aa48923
# Parent  2e5b737810a60a9f504f9c7f4168b3433d71a9c4
more infinite product theorems

diff -r 2e5b737810a6 -r 137d5d0112bb src/HOL/Analysis/Infinite_Products.thy
--- a/src/HOL/Analysis/Infinite_Products.thy	Wed May 09 07:48:54 2018 +0200
+++ b/src/HOL/Analysis/Infinite_Products.thy	Wed May 09 14:07:19 2018 +0100
@@ -688,4 +688,31 @@
     by (simp add: convergent_prod_def)
 qed
 
+lemma has_prod_If_finite_set:
+  fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
+  shows "finite A \<Longrightarrow> (\<lambda>r. if r \<in> A then f r else 1) has_prod (\<Prod>r\<in>A. f r)"
+  using has_prod_finite[of A "(\<lambda>r. if r \<in> A then f r else 1)"]
+  by simp
+
+lemma has_prod_If_finite:
+  fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
+  shows "finite {r. P r} \<Longrightarrow> (\<lambda>r. if P r then f r else 1) has_prod (\<Prod>r | P r. f r)"
+  using has_prod_If_finite_set[of "{r. P r}"] by simp
+
+lemma convergent_prod_If_finite_set[simp, intro]:
+  fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
+  shows "finite A \<Longrightarrow> convergent_prod (\<lambda>r. if r \<in> A then f r else 1)"
+  by (simp add: convergent_prod_finite)
+
+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
+
+lemma has_prod_single:
+  fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
+  shows "(\<lambda>r. if r = i then f r else 1) has_prod f i"
+  using has_prod_If_finite[of "\<lambda>r. r = i"] by simp
+
+
 end
diff -r 2e5b737810a6 -r 137d5d0112bb src/HOL/Series.thy
--- a/src/HOL/Series.thy	Wed May 09 07:48:54 2018 +0200
+++ b/src/HOL/Series.thy	Wed May 09 14:07:19 2018 +0100
@@ -115,24 +115,11 @@
   shows "f sums (\<Sum>n\<in>N. f n)"
 proof -
   have eq: "sum f {..<n + Suc (Max N)} = sum f N" for n
-  proof (cases "N = {}")
-    case True
-    with f have "f = (\<lambda>x. 0)" by auto
-    then show ?thesis by simp
-  next
-    case [simp]: False
-    show ?thesis
-    proof (safe intro!: sum.mono_neutral_right f)
-      fix i
-      assume "i \<in> N"
-      then have "i \<le> Max N" by simp
-      then show "i < n + Suc (Max N)" by simp
-    qed
-  qed
+    by (rule sum.mono_neutral_right) (auto simp: add_increasing less_Suc_eq_le f)
   show ?thesis
     unfolding sums_def
     by (rule LIMSEQ_offset[of _ "Suc (Max N)"])
-       (simp add: eq atLeast0LessThan del: add_Suc_right)
+      (simp add: eq atLeast0LessThan del: add_Suc_right)
 qed
 
 corollary sums_0: "(\<And>n. f n = 0) \<Longrightarrow> (f sums 0)"