src/HOL/Analysis/Infinite_Products.thy
changeset 68071 c18af2b0f83e
parent 68064 b249fab48c76
child 68076 315043faa871
     1.1 --- a/src/HOL/Analysis/Infinite_Products.thy	Wed May 02 23:33:00 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Infinite_Products.thy	Thu May 03 17:14:08 2018 +0100
     1.3 @@ -72,6 +72,12 @@
     1.4  lemma has_prod_cong: "(\<And>n. f n = g n) \<Longrightarrow> f has_prod c \<longleftrightarrow> g has_prod c"
     1.5    by presburger
     1.6  
     1.7 +lemma gen_has_prod_nonzero [simp]: "\<not> gen_has_prod f M 0"
     1.8 +  by (simp add: gen_has_prod_def)
     1.9 +
    1.10 +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))"
    1.11 +  by (simp add: has_prod_def)
    1.12 +
    1.13  lemma convergent_prod_altdef:
    1.14    fixes f :: "nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}"
    1.15    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)"
    1.16 @@ -604,4 +610,81 @@
    1.17    qed
    1.18  qed
    1.19  
    1.20 +lemma has_prod_finite:
    1.21 +  fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
    1.22 +  assumes [simp]: "finite N"
    1.23 +    and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 1"
    1.24 +  shows "f has_prod (\<Prod>n\<in>N. f n)"
    1.25 +proof -
    1.26 +  have eq: "prod f {..n + Suc (Max N)} = prod f N" for n
    1.27 +  proof (rule prod.mono_neutral_right)
    1.28 +    show "N \<subseteq> {..n + Suc (Max N)}"
    1.29 +      by (auto simp add: le_Suc_eq trans_le_add2)
    1.30 +    show "\<forall>i\<in>{..n + Suc (Max N)} - N. f i = 1"
    1.31 +      using f by blast
    1.32 +  qed auto
    1.33 +  show ?thesis
    1.34 +  proof (cases "\<forall>n\<in>N. f n \<noteq> 0")
    1.35 +    case True
    1.36 +    then have "prod f N \<noteq> 0"
    1.37 +      by simp
    1.38 +    moreover have "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> prod f N"
    1.39 +      by (rule LIMSEQ_offset[of _ "Suc (Max N)"]) (simp add: eq atLeast0LessThan del: add_Suc_right)
    1.40 +    ultimately show ?thesis
    1.41 +      by (simp add: gen_has_prod_def has_prod_def)
    1.42 +  next
    1.43 +    case False
    1.44 +    then obtain k where "k \<in> N" "f k = 0"
    1.45 +      by auto
    1.46 +    let ?Z = "{n \<in> N. f n = 0}"
    1.47 +    have maxge: "Max ?Z \<ge> n" if "f n = 0" for n
    1.48 +      using Max_ge [of ?Z] \<open>finite N\<close> \<open>f n = 0\<close>
    1.49 +      by (metis (mono_tags) Collect_mem_eq f finite_Collect_conjI mem_Collect_eq zero_neq_one)
    1.50 +    let ?q = "prod f {Suc (Max ?Z)..Max N}"
    1.51 +    have [simp]: "?q \<noteq> 0"
    1.52 +      using maxge Suc_n_not_le_n le_trans by force
    1.53 +    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
    1.54 +      apply (rule sym)
    1.55 +      apply (rule prod.reindex_cong [where l = "\<lambda>i. i + Suc (Max ?Z)"])
    1.56 +        apply (auto simp: )
    1.57 +       apply (simp add: inj_on_def)
    1.58 +      apply (auto simp: image_iff)
    1.59 +      using le_Suc_ex by fastforce
    1.60 +    have eq: "prod f {Suc (Max ?Z)..n + (Max N) + Suc (Max ?Z)} = ?q" for n
    1.61 +      apply (rule prod.mono_neutral_right)
    1.62 +        apply (auto simp: )
    1.63 +      using Max.coboundedI assms(1) f by blast
    1.64 +    have q: "gen_has_prod f (Suc (Max ?Z)) ?q"
    1.65 +      apply (auto simp: gen_has_prod_def)
    1.66 +      apply (rule LIMSEQ_offset[of _ "(Max N)"])
    1.67 +      apply (simp add: eq1 eq atLeast0LessThan del: add_Suc_right)
    1.68 +      done
    1.69 +    show ?thesis
    1.70 +      unfolding has_prod_def
    1.71 +    proof (intro disjI2 exI conjI)      
    1.72 +      show "prod f N = 0"
    1.73 +        using \<open>f k = 0\<close> \<open>k \<in> N\<close> \<open>finite N\<close> prod_zero by blast
    1.74 +      show "f (Max ?Z) = 0"
    1.75 +        using Max_in [of ?Z] \<open>finite N\<close> \<open>f k = 0\<close> \<open>k \<in> N\<close> by auto
    1.76 +    qed (use q in auto)
    1.77 +  qed
    1.78 +qed
    1.79 +
    1.80 +corollary has_prod_0:
    1.81 +  fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
    1.82 +  assumes "\<And>n. f n = 1"
    1.83 +  shows "f has_prod 1"
    1.84 +  by (simp add: assms has_prod_cong)
    1.85 +
    1.86 +lemma convergent_prod_finite:
    1.87 +  fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
    1.88 +  assumes "finite N" "\<And>n. n \<notin> N \<Longrightarrow> f n = 1"
    1.89 +  shows "convergent_prod f"
    1.90 +proof -
    1.91 +  have "\<exists>n p. gen_has_prod f n p"
    1.92 +    using assms has_prod_def has_prod_finite by blast
    1.93 +  then show ?thesis
    1.94 +    by (simp add: convergent_prod_def)
    1.95 +qed
    1.96 +
    1.97  end