more on infinite products
authorpaulson <lp15@cam.ac.uk>
Thu May 10 15:41:34 2018 +0100 (14 months ago)
changeset 68136f022083489d0
parent 68128 4646124e683e
child 68137 afcdc4c0ef0d
more on infinite products
src/HOL/Analysis/Infinite_Products.thy
     1.1 --- a/src/HOL/Analysis/Infinite_Products.thy	Wed May 09 15:07:20 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Infinite_Products.thy	Thu May 10 15:41:34 2018 +0100
     1.3 @@ -75,8 +75,33 @@
     1.4  lemma gen_has_prod_nonzero [simp]: "\<not> gen_has_prod f M 0"
     1.5    by (simp add: gen_has_prod_def)
     1.6  
     1.7 +lemma gen_has_prod_eq_0:
     1.8 +  fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
     1.9 +  assumes p: "gen_has_prod f m p" and i: "f i = 0" "i \<ge> m"
    1.10 +  shows "p = 0"
    1.11 +proof -
    1.12 +  have eq0: "(\<Prod>k\<le>n. f (k+m)) = 0" if "i - m \<le> n" for n
    1.13 +    by (metis i that atMost_atLeast0 atMost_iff diff_add finite_atLeastAtMost prod_zero_iff)
    1.14 +  have "(\<lambda>n. \<Prod>i\<le>n. f (i + m)) \<longlonglongrightarrow> 0"
    1.15 +    by (rule LIMSEQ_offset [where k = "i-m"]) (simp add: eq0)
    1.16 +    with p show ?thesis
    1.17 +      unfolding gen_has_prod_def
    1.18 +    using LIMSEQ_unique by blast
    1.19 +qed
    1.20 +
    1.21  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.22    by (simp add: has_prod_def)
    1.23 +      
    1.24 +lemma has_prod_unique2: 
    1.25 +  fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}"
    1.26 +  assumes "f has_prod a" "f has_prod b" shows "a = b"
    1.27 +  using assms
    1.28 +  by (auto simp: has_prod_def gen_has_prod_eq_0) (meson gen_has_prod_def sequentially_bot tendsto_unique)
    1.29 +
    1.30 +lemma has_prod_unique:
    1.31 +  fixes f :: "nat \<Rightarrow> 'a :: {idom,t2_space}"
    1.32 +  shows "f has_prod s \<Longrightarrow> s = prodinf f"
    1.33 +  by (simp add: has_prod_unique2 prodinf_def the_equality)
    1.34  
    1.35  lemma convergent_prod_altdef:
    1.36    fixes f :: "nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}"
    1.37 @@ -385,7 +410,14 @@
    1.38      unfolding prod_defs by blast
    1.39  qed
    1.40  
    1.41 -lemma abs_convergent_prod_ignore_initial_segment:
    1.42 +corollary convergent_prod_ignore_nonzero_segment:
    1.43 +  fixes f :: "nat \<Rightarrow> 'a :: real_normed_field"
    1.44 +  assumes f: "convergent_prod f" and nz: "\<And>i. i \<ge> M \<Longrightarrow> f i \<noteq> 0"
    1.45 +  shows "\<exists>p. gen_has_prod f M p"
    1.46 +  using convergent_prod_ignore_initial_segment [OF f]
    1.47 +  by (metis convergent_LIMSEQ_iff convergent_prod_iff_convergent le_add_same_cancel2 nz prod_defs(1) zero_order(1))
    1.48 +
    1.49 +corollary abs_convergent_prod_ignore_initial_segment:
    1.50    assumes "abs_convergent_prod f"
    1.51    shows   "abs_convergent_prod (\<lambda>n. f (n + m))"
    1.52    using assms unfolding abs_convergent_prod_def 
    1.53 @@ -519,15 +551,13 @@
    1.54    with L show ?thesis by (auto simp: prod_defs)
    1.55  qed
    1.56  
    1.57 -lemma convergent_prod_offset_0:
    1.58 +lemma gen_has_prod_cases:
    1.59    fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"
    1.60 -  assumes "convergent_prod f" "\<And>i. f i \<noteq> 0"
    1.61 -  shows "\<exists>p. gen_has_prod f 0 p"
    1.62 -  using assms
    1.63 -  unfolding convergent_prod_def
    1.64 -proof (clarsimp simp: prod_defs)
    1.65 -  fix M p
    1.66 -  assume "(\<lambda>n. \<Prod>i\<le>n. f (i + M)) \<longlonglongrightarrow> p" "p \<noteq> 0"
    1.67 +  assumes "gen_has_prod f M p"
    1.68 +  obtains i where "i<M" "f i = 0" | p where "gen_has_prod f 0 p"
    1.69 +proof -
    1.70 +  have "(\<lambda>n. \<Prod>i\<le>n. f (i + M)) \<longlonglongrightarrow> p" "p \<noteq> 0"
    1.71 +    using assms unfolding gen_has_prod_def by blast+
    1.72    then have "(\<lambda>n. prod f {..<M} * (\<Prod>i\<le>n. f (i + M))) \<longlonglongrightarrow> prod f {..<M} * p"
    1.73      by (metis tendsto_mult_left)
    1.74    moreover have "prod f {..<M} * (\<Prod>i\<le>n. f (i + M)) = prod f {..n+M}" for n
    1.75 @@ -542,11 +572,18 @@
    1.76    qed
    1.77    ultimately have "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> prod f {..<M} * p"
    1.78      by (auto intro: LIMSEQ_offset [where k=M])
    1.79 -  then show "\<exists>p. (\<lambda>n. prod f {..n}) \<longlonglongrightarrow> p \<and> p \<noteq> 0"
    1.80 -    using \<open>p \<noteq> 0\<close> assms
    1.81 -    by (rule_tac x="prod f {..<M} * p" in exI) auto
    1.82 +  then have "gen_has_prod f 0 (prod f {..<M} * p)" if "\<forall>i<M. f i \<noteq> 0"
    1.83 +    using \<open>p \<noteq> 0\<close> assms that by (auto simp: gen_has_prod_def)
    1.84 +  then show thesis
    1.85 +    using that by blast
    1.86  qed
    1.87  
    1.88 +corollary convergent_prod_offset_0:
    1.89 +  fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"
    1.90 +  assumes "convergent_prod f" "\<And>i. f i \<noteq> 0"
    1.91 +  shows "\<exists>p. gen_has_prod f 0 p"
    1.92 +  using assms convergent_prod_def gen_has_prod_cases by blast
    1.93 +
    1.94  lemma prodinf_eq_lim:
    1.95    fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"
    1.96    assumes "convergent_prod f" "\<And>i. f i \<noteq> 0"
    1.97 @@ -714,5 +751,71 @@
    1.98    shows "(\<lambda>r. if r = i then f r else 1) has_prod f i"
    1.99    using has_prod_If_finite[of "\<lambda>r. r = i"] by simp
   1.100  
   1.101 +context
   1.102 +  fixes f :: "nat \<Rightarrow> 'a :: real_normed_field"
   1.103 +begin
   1.104 +
   1.105 +lemma convergent_prod_imp_has_prod: 
   1.106 +  assumes "convergent_prod f"
   1.107 +  shows "\<exists>p. f has_prod p"
   1.108 +proof -
   1.109 +  obtain M p where p: "gen_has_prod f M p"
   1.110 +    using assms convergent_prod_def by blast
   1.111 +  then have "p \<noteq> 0"
   1.112 +    using gen_has_prod_nonzero by blast
   1.113 +  with p have fnz: "f i \<noteq> 0" if "i \<ge> M" for i
   1.114 +    using gen_has_prod_eq_0 that by blast
   1.115 +  define C where "C = (\<Prod>n<M. f n)"
   1.116 +  show ?thesis
   1.117 +  proof (cases "\<forall>n\<le>M. f n \<noteq> 0")
   1.118 +    case True
   1.119 +    then have "C \<noteq> 0"
   1.120 +      by (simp add: C_def)
   1.121 +    then show ?thesis
   1.122 +      by (meson True assms convergent_prod_offset_0 fnz has_prod_def nat_le_linear)
   1.123 +  next
   1.124 +    case False
   1.125 +    let ?N = "GREATEST n. f n = 0"
   1.126 +    have 0: "f ?N = 0"
   1.127 +      using fnz False
   1.128 +      by (metis (mono_tags, lifting) GreatestI_ex_nat nat_le_linear)
   1.129 +    have "f i \<noteq> 0" if "i > ?N" for i
   1.130 +      by (metis (mono_tags, lifting) Greatest_le_nat fnz leD linear that)
   1.131 +    then have "\<exists>p. gen_has_prod f (Suc ?N) p"
   1.132 +      using assms by (auto simp: intro!: convergent_prod_ignore_nonzero_segment)
   1.133 +    then show ?thesis
   1.134 +      unfolding has_prod_def using 0 by blast
   1.135 +  qed
   1.136 +qed
   1.137 +
   1.138 +lemma convergent_prod_has_prod [intro]:
   1.139 +  shows "convergent_prod f \<Longrightarrow> f has_prod (prodinf f)"
   1.140 +  unfolding prodinf_def
   1.141 +  by (metis convergent_prod_imp_has_prod has_prod_unique theI')
   1.142 +
   1.143 +lemma convergent_prod_LIMSEQ:
   1.144 +  shows "convergent_prod f \<Longrightarrow> (\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> prodinf f"
   1.145 +  by (metis convergent_LIMSEQ_iff convergent_prod_has_prod convergent_prod_imp_convergent 
   1.146 +      convergent_prod_to_zero_iff gen_has_prod_eq_0 has_prod_def prodinf_eq_lim zero_le)
   1.147 +
   1.148 +lemma has_prod_iff: "f has_prod x \<longleftrightarrow> convergent_prod f \<and> prodinf f = x"
   1.149 +proof
   1.150 +  assume "f has_prod x"
   1.151 +  then show "convergent_prod f \<and> prodinf f = x"
   1.152 +    apply safe
   1.153 +    using convergent_prod_def has_prod_def apply blast
   1.154 +    using has_prod_unique by blast
   1.155 +qed auto
   1.156 +
   1.157 +lemma convergent_prod_has_prod_iff: "convergent_prod f \<longleftrightarrow> f has_prod prodinf f"
   1.158 +  by (auto simp: has_prod_iff convergent_prod_has_prod)
   1.159 +
   1.160 +lemma prodinf_finite:
   1.161 +  assumes N: "finite N"
   1.162 +    and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 1"
   1.163 +  shows "prodinf f = (\<Prod>n\<in>N. f n)"
   1.164 +  using has_prod_finite[OF assms, THEN has_prod_unique] by simp
   1.165  
   1.166  end
   1.167 +
   1.168 +end