# HG changeset patch
# User immler
# Date 1525366150 -7200
# Node ID 262b42b5915130e6bb8553769abcabfd9a63db7a
# Parent  8d50467f7555e00e7768b7e77fa5b8905c7530ae# Parent  c18af2b0f83e059b3f929e41b5de485c88d21148
merged

diff -r 8d50467f7555 -r 262b42b59151 src/HOL/Analysis/Infinite_Products.thy
--- a/src/HOL/Analysis/Infinite_Products.thy	Thu May 03 16:17:44 2018 +0200
+++ b/src/HOL/Analysis/Infinite_Products.thy	Thu May 03 18:49:10 2018 +0200
@@ -72,6 +72,12 @@
 lemma has_prod_cong: "(\<And>n. f n = g n) \<Longrightarrow> f has_prod c \<longleftrightarrow> g has_prod c"
   by presburger
 
+lemma gen_has_prod_nonzero [simp]: "\<not> gen_has_prod f M 0"
+  by (simp add: gen_has_prod_def)
+
+lemma has_prod_0_iff: "f has_prod 0 \<longleftrightarrow> (\<exists>i. f i = 0 \<and> (\<exists>p. gen_has_prod f (Suc i) p))"
+  by (simp add: has_prod_def)
+
 lemma convergent_prod_altdef:
   fixes f :: "nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}"
   shows "convergent_prod f \<longleftrightarrow> (\<exists>M L. (\<forall>n\<ge>M. f n \<noteq> 0) \<and> (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> L \<and> L \<noteq> 0)"
@@ -604,4 +610,81 @@
   qed
 qed
 
+lemma has_prod_finite:
+  fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
+  assumes [simp]: "finite N"
+    and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 1"
+  shows "f has_prod (\<Prod>n\<in>N. f n)"
+proof -
+  have eq: "prod f {..n + Suc (Max N)} = prod f N" for n
+  proof (rule prod.mono_neutral_right)
+    show "N \<subseteq> {..n + Suc (Max N)}"
+      by (auto simp add: le_Suc_eq trans_le_add2)
+    show "\<forall>i\<in>{..n + Suc (Max N)} - N. f i = 1"
+      using f by blast
+  qed auto
+  show ?thesis
+  proof (cases "\<forall>n\<in>N. f n \<noteq> 0")
+    case True
+    then have "prod f N \<noteq> 0"
+      by simp
+    moreover have "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> prod f N"
+      by (rule LIMSEQ_offset[of _ "Suc (Max N)"]) (simp add: eq atLeast0LessThan del: add_Suc_right)
+    ultimately show ?thesis
+      by (simp add: gen_has_prod_def has_prod_def)
+  next
+    case False
+    then obtain k where "k \<in> N" "f k = 0"
+      by auto
+    let ?Z = "{n \<in> N. f n = 0}"
+    have maxge: "Max ?Z \<ge> n" if "f n = 0" for n
+      using Max_ge [of ?Z] \<open>finite N\<close> \<open>f n = 0\<close>
+      by (metis (mono_tags) Collect_mem_eq f finite_Collect_conjI mem_Collect_eq zero_neq_one)
+    let ?q = "prod f {Suc (Max ?Z)..Max N}"
+    have [simp]: "?q \<noteq> 0"
+      using maxge Suc_n_not_le_n le_trans by force
+    have eq1: "(\<Prod>i\<le>n + Max N. f (Suc (i + Max ?Z))) = prod f {Suc (Max ?Z)..n + (Max N) + Suc (Max ?Z)}" for n
+      apply (rule sym)
+      apply (rule prod.reindex_cong [where l = "\<lambda>i. i + Suc (Max ?Z)"])
+        apply (auto simp: )
+       apply (simp add: inj_on_def)
+      apply (auto simp: image_iff)
+      using le_Suc_ex by fastforce
+    have eq: "prod f {Suc (Max ?Z)..n + (Max N) + Suc (Max ?Z)} = ?q" for n
+      apply (rule prod.mono_neutral_right)
+        apply (auto simp: )
+      using Max.coboundedI assms(1) f by blast
+    have q: "gen_has_prod f (Suc (Max ?Z)) ?q"
+      apply (auto simp: gen_has_prod_def)
+      apply (rule LIMSEQ_offset[of _ "(Max N)"])
+      apply (simp add: eq1 eq atLeast0LessThan del: add_Suc_right)
+      done
+    show ?thesis
+      unfolding has_prod_def
+    proof (intro disjI2 exI conjI)      
+      show "prod f N = 0"
+        using \<open>f k = 0\<close> \<open>k \<in> N\<close> \<open>finite N\<close> prod_zero by blast
+      show "f (Max ?Z) = 0"
+        using Max_in [of ?Z] \<open>finite N\<close> \<open>f k = 0\<close> \<open>k \<in> N\<close> by auto
+    qed (use q in auto)
+  qed
+qed
+
+corollary has_prod_0:
+  fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
+  assumes "\<And>n. f n = 1"
+  shows "f has_prod 1"
+  by (simp add: assms has_prod_cong)
+
+lemma convergent_prod_finite:
+  fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
+  assumes "finite N" "\<And>n. n \<notin> N \<Longrightarrow> f n = 1"
+  shows "convergent_prod f"
+proof -
+  have "\<exists>n p. gen_has_prod f n p"
+    using assms has_prod_def has_prod_finite by blast
+  then show ?thesis
+    by (simp add: convergent_prod_def)
+qed
+
 end