src/HOL/Analysis/Infinite_Products.thy
changeset 68064 b249fab48c76
parent 66277 512b0dc09061
child 68071 c18af2b0f83e
     1.1 --- a/src/HOL/Analysis/Infinite_Products.thy	Fri Apr 27 12:43:05 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Infinite_Products.thy	Wed May 02 12:47:56 2018 +0100
     1.3 @@ -1,6 +1,5 @@
     1.4 -(*
     1.5 -  File:      HOL/Analysis/Infinite_Product.thy
     1.6 -  Author:    Manuel Eberl
     1.7 +(*File:      HOL/Analysis/Infinite_Product.thy
     1.8 +  Author:    Manuel Eberl & LC Paulson
     1.9  
    1.10    Basic results about convergence and absolute convergence of infinite products
    1.11    and their connection to summability.
    1.12 @@ -9,7 +8,7 @@
    1.13  theory Infinite_Products
    1.14    imports Complex_Main
    1.15  begin
    1.16 -
    1.17 +    
    1.18  lemma sum_le_prod:
    1.19    fixes f :: "'a \<Rightarrow> 'b :: linordered_semidom"
    1.20    assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0"
    1.21 @@ -51,8 +50,27 @@
    1.22      by (rule tendsto_eq_intros refl | simp)+
    1.23  qed auto
    1.24  
    1.25 +definition gen_has_prod :: "[nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}, nat, 'a] \<Rightarrow> bool" 
    1.26 +  where "gen_has_prod f M p \<equiv> (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> p \<and> p \<noteq> 0"
    1.27 +
    1.28 +text\<open>The nonzero and zero cases, as in \emph{Complex Analysis} by Joseph Bak and Donald J.Newman, page 241\<close>
    1.29 +definition has_prod :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "has'_prod" 80)
    1.30 +  where "f has_prod p \<equiv> gen_has_prod f 0 p \<or> (\<exists>i q. p = 0 \<and> f i = 0 \<and> gen_has_prod f (Suc i) q)"
    1.31 +
    1.32  definition convergent_prod :: "(nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}) \<Rightarrow> bool" where
    1.33 -  "convergent_prod f \<longleftrightarrow> (\<exists>M L. (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> L \<and> L \<noteq> 0)"
    1.34 +  "convergent_prod f \<equiv> \<exists>M p. gen_has_prod f M p"
    1.35 +
    1.36 +definition prodinf :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a"
    1.37 +    (binder "\<Prod>" 10)
    1.38 +  where "prodinf f = (THE p. f has_prod p)"
    1.39 +
    1.40 +lemmas prod_defs = gen_has_prod_def has_prod_def convergent_prod_def prodinf_def
    1.41 +
    1.42 +lemma has_prod_subst[trans]: "f = g \<Longrightarrow> g has_prod z \<Longrightarrow> f has_prod z"
    1.43 +  by simp
    1.44 +
    1.45 +lemma has_prod_cong: "(\<And>n. f n = g n) \<Longrightarrow> f has_prod c \<longleftrightarrow> g has_prod c"
    1.46 +  by presburger
    1.47  
    1.48  lemma convergent_prod_altdef:
    1.49    fixes f :: "nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}"
    1.50 @@ -60,7 +78,7 @@
    1.51  proof
    1.52    assume "convergent_prod f"
    1.53    then obtain M L where *: "(\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> L" "L \<noteq> 0"
    1.54 -    by (auto simp: convergent_prod_def)
    1.55 +    by (auto simp: prod_defs)
    1.56    have "f i \<noteq> 0" if "i \<ge> M" for i
    1.57    proof
    1.58      assume "f i = 0"
    1.59 @@ -79,7 +97,7 @@
    1.60    qed
    1.61    with * show "(\<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.62      by blast
    1.63 -qed (auto simp: convergent_prod_def)
    1.64 +qed (auto simp: prod_defs)
    1.65  
    1.66  definition abs_convergent_prod :: "(nat \<Rightarrow> _) \<Rightarrow> bool" where
    1.67    "abs_convergent_prod f \<longleftrightarrow> convergent_prod (\<lambda>i. 1 + norm (f i - 1))"
    1.68 @@ -101,12 +119,12 @@
    1.69      qed
    1.70    qed (use L in simp_all)
    1.71    hence "L \<noteq> 0" by auto
    1.72 -  with L show ?thesis unfolding abs_convergent_prod_def convergent_prod_def
    1.73 +  with L show ?thesis unfolding abs_convergent_prod_def prod_defs
    1.74      by (intro exI[of _ "0::nat"] exI[of _ L]) auto
    1.75  qed
    1.76  
    1.77  lemma
    1.78 -  fixes f :: "nat \<Rightarrow> 'a :: {real_normed_div_algebra,idom}"
    1.79 +  fixes f :: "nat \<Rightarrow> 'a :: {topological_semigroup_mult,t2_space,idom}"
    1.80    assumes "convergent_prod f"
    1.81    shows   convergent_prod_imp_convergent: "convergent (\<lambda>n. \<Prod>i\<le>n. f i)"
    1.82      and   convergent_prod_to_zero_iff:    "(\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> 0 \<longleftrightarrow> (\<exists>i. f i = 0)"
    1.83 @@ -141,8 +159,30 @@
    1.84    qed
    1.85  qed
    1.86  
    1.87 +lemma convergent_prod_iff_nz_lim:
    1.88 +  fixes f :: "nat \<Rightarrow> 'a :: {topological_semigroup_mult,t2_space,idom}"
    1.89 +  assumes "\<And>i. f i \<noteq> 0"
    1.90 +  shows "convergent_prod f \<longleftrightarrow> (\<exists>L. (\<lambda>n. \<Prod>i\<le>n. f i) \<longlonglongrightarrow> L \<and> L \<noteq> 0)"
    1.91 +    (is "?lhs \<longleftrightarrow> ?rhs")
    1.92 +proof
    1.93 +  assume ?lhs then show ?rhs
    1.94 +    using assms convergentD convergent_prod_imp_convergent convergent_prod_to_zero_iff by blast
    1.95 +next
    1.96 +  assume ?rhs then show ?lhs
    1.97 +    unfolding prod_defs
    1.98 +    by (rule_tac x="0" in exI) (auto simp: )
    1.99 +qed
   1.100 +
   1.101 +lemma convergent_prod_iff_convergent: 
   1.102 +  fixes f :: "nat \<Rightarrow> 'a :: {topological_semigroup_mult,t2_space,idom}"
   1.103 +  assumes "\<And>i. f i \<noteq> 0"
   1.104 +  shows "convergent_prod f \<longleftrightarrow> convergent (\<lambda>n. \<Prod>i\<le>n. f i) \<and> lim (\<lambda>n. \<Prod>i\<le>n. f i) \<noteq> 0"
   1.105 +  by (force simp add: convergent_prod_iff_nz_lim assms convergent_def limI)
   1.106 +
   1.107 +
   1.108  lemma abs_convergent_prod_altdef:
   1.109 -  "abs_convergent_prod f \<longleftrightarrow> convergent (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))"
   1.110 +  fixes f :: "nat \<Rightarrow> 'a :: {one,real_normed_vector}"
   1.111 +  shows  "abs_convergent_prod f \<longleftrightarrow> convergent (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))"
   1.112  proof
   1.113    assume "abs_convergent_prod f"
   1.114    thus "convergent (\<lambda>n. \<Prod>i\<le>n. 1 + norm (f i - 1))"
   1.115 @@ -180,7 +220,7 @@
   1.116    also have "norm (1::'a) = 1" by simp
   1.117    also note insert.IH
   1.118    also have "(\<Prod>n\<in>A. 1 + norm (f n)) - 1 + norm (f x) * (\<Prod>x\<in>A. 1 + norm (f x)) =
   1.119 -               (\<Prod>n\<in>insert x A. 1 + norm (f n)) - 1"
   1.120 +             (\<Prod>n\<in>insert x A. 1 + norm (f n)) - 1"
   1.121      using insert.hyps by (simp add: algebra_simps)
   1.122    finally show ?case by - (simp_all add: mult_left_mono)
   1.123  qed simp_all
   1.124 @@ -297,8 +337,9 @@
   1.125    shows   "convergent_prod f"
   1.126  proof -
   1.127    from assms obtain M L where "(\<lambda>n. \<Prod>k\<le>n. f (k + (M + m))) \<longlonglongrightarrow> L" "L \<noteq> 0"
   1.128 -    by (auto simp: convergent_prod_def add.assoc)
   1.129 -  thus "convergent_prod f" unfolding convergent_prod_def by blast
   1.130 +    by (auto simp: prod_defs add.assoc)
   1.131 +  thus "convergent_prod f" 
   1.132 +    unfolding prod_defs by blast
   1.133  qed
   1.134  
   1.135  lemma abs_convergent_prod_offset:
   1.136 @@ -334,7 +375,8 @@
   1.137      by (intro tendsto_divide tendsto_const) auto
   1.138    hence "(\<lambda>n. \<Prod>k\<le>n. f (k + M + m)) \<longlonglongrightarrow> L / C" by simp
   1.139    moreover from \<open>L \<noteq> 0\<close> have "L / C \<noteq> 0" by simp
   1.140 -  ultimately show ?thesis unfolding convergent_prod_def by blast
   1.141 +  ultimately show ?thesis 
   1.142 +    unfolding prod_defs by blast
   1.143  qed
   1.144  
   1.145  lemma abs_convergent_prod_ignore_initial_segment:
   1.146 @@ -343,11 +385,6 @@
   1.147    using assms unfolding abs_convergent_prod_def 
   1.148    by (rule convergent_prod_ignore_initial_segment)
   1.149  
   1.150 -lemma summable_LIMSEQ': 
   1.151 -  assumes "summable (f::nat\<Rightarrow>'a::{t2_space,comm_monoid_add})"
   1.152 -  shows   "(\<lambda>n. \<Sum>i\<le>n. f i) \<longlonglongrightarrow> suminf f"
   1.153 -  using assms sums_def_le by blast
   1.154 -
   1.155  lemma abs_convergent_prod_imp_convergent_prod:
   1.156    fixes f :: "nat \<Rightarrow> 'a :: {real_normed_div_algebra,complete_space,comm_ring_1}"
   1.157    assumes "abs_convergent_prod f"
   1.158 @@ -473,7 +510,98 @@
   1.159      qed simp_all
   1.160      thus False by simp
   1.161    qed
   1.162 -  with L show ?thesis by (auto simp: convergent_prod_def)
   1.163 +  with L show ?thesis by (auto simp: prod_defs)
   1.164 +qed
   1.165 +
   1.166 +lemma convergent_prod_offset_0:
   1.167 +  fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"
   1.168 +  assumes "convergent_prod f" "\<And>i. f i \<noteq> 0"
   1.169 +  shows "\<exists>p. gen_has_prod f 0 p"
   1.170 +  using assms
   1.171 +  unfolding convergent_prod_def
   1.172 +proof (clarsimp simp: prod_defs)
   1.173 +  fix M p
   1.174 +  assume "(\<lambda>n. \<Prod>i\<le>n. f (i + M)) \<longlonglongrightarrow> p" "p \<noteq> 0"
   1.175 +  then have "(\<lambda>n. prod f {..<M} * (\<Prod>i\<le>n. f (i + M))) \<longlonglongrightarrow> prod f {..<M} * p"
   1.176 +    by (metis tendsto_mult_left)
   1.177 +  moreover have "prod f {..<M} * (\<Prod>i\<le>n. f (i + M)) = prod f {..n+M}" for n
   1.178 +  proof -
   1.179 +    have "{..n+M} = {..<M} \<union> {M..n+M}"
   1.180 +      by auto
   1.181 +    then have "prod f {..n+M} = prod f {..<M} * prod f {M..n+M}"
   1.182 +      by simp (subst prod.union_disjoint; force)
   1.183 +    also have "... = prod f {..<M} * (\<Prod>i\<le>n. f (i + M))"
   1.184 +      by (metis (mono_tags, lifting) add.left_neutral atMost_atLeast0 prod_shift_bounds_cl_nat_ivl)
   1.185 +    finally show ?thesis by metis
   1.186 +  qed
   1.187 +  ultimately have "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> prod f {..<M} * p"
   1.188 +    by (auto intro: LIMSEQ_offset [where k=M])
   1.189 +  then show "\<exists>p. (\<lambda>n. prod f {..n}) \<longlonglongrightarrow> p \<and> p \<noteq> 0"
   1.190 +    using \<open>p \<noteq> 0\<close> assms
   1.191 +    by (rule_tac x="prod f {..<M} * p" in exI) auto
   1.192 +qed
   1.193 +
   1.194 +lemma prodinf_eq_lim:
   1.195 +  fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"
   1.196 +  assumes "convergent_prod f" "\<And>i. f i \<noteq> 0"
   1.197 +  shows "prodinf f = lim (\<lambda>n. \<Prod>i\<le>n. f i)"
   1.198 +  using assms convergent_prod_offset_0 [OF assms]
   1.199 +  by (simp add: prod_defs lim_def) (metis (no_types) assms(1) convergent_prod_to_zero_iff)
   1.200 +
   1.201 +lemma has_prod_one[simp, intro]: "(\<lambda>n. 1) has_prod 1"
   1.202 +  unfolding prod_defs by auto
   1.203 +
   1.204 +lemma convergent_prod_one[simp, intro]: "convergent_prod (\<lambda>n. 1)"
   1.205 +  unfolding prod_defs by auto
   1.206 +
   1.207 +lemma prodinf_cong: "(\<And>n. f n = g n) \<Longrightarrow> prodinf f = prodinf g"
   1.208 +  by presburger
   1.209 +
   1.210 +lemma convergent_prod_cong:
   1.211 +  fixes f g :: "nat \<Rightarrow> 'a::{field,topological_semigroup_mult,t2_space}"
   1.212 +  assumes ev: "eventually (\<lambda>x. f x = g x) sequentially" and f: "\<And>i. f i \<noteq> 0" and g: "\<And>i. g i \<noteq> 0"
   1.213 +  shows "convergent_prod f = convergent_prod g"
   1.214 +proof -
   1.215 +  from assms obtain N where N: "\<forall>n\<ge>N. f n = g n"
   1.216 +    by (auto simp: eventually_at_top_linorder)
   1.217 +  define C where "C = (\<Prod>k<N. f k / g k)"
   1.218 +  with g have "C \<noteq> 0"
   1.219 +    by (simp add: f)
   1.220 +  have *: "eventually (\<lambda>n. prod f {..n} = C * prod g {..n}) sequentially"
   1.221 +    using eventually_ge_at_top[of N]
   1.222 +  proof eventually_elim
   1.223 +    case (elim n)
   1.224 +    then have "{..n} = {..<N} \<union> {N..n}"
   1.225 +      by auto
   1.226 +    also have "prod f ... = prod f {..<N} * prod f {N..n}"
   1.227 +      by (intro prod.union_disjoint) auto
   1.228 +    also from N have "prod f {N..n} = prod g {N..n}"
   1.229 +      by (intro prod.cong) simp_all
   1.230 +    also have "prod f {..<N} * prod g {N..n} = C * (prod g {..<N} * prod g {N..n})"
   1.231 +      unfolding C_def by (simp add: g prod_dividef)
   1.232 +    also have "prod g {..<N} * prod g {N..n} = prod g ({..<N} \<union> {N..n})"
   1.233 +      by (intro prod.union_disjoint [symmetric]) auto
   1.234 +    also from elim have "{..<N} \<union> {N..n} = {..n}"
   1.235 +      by auto                                                                    
   1.236 +    finally show "prod f {..n} = C * prod g {..n}" .
   1.237 +  qed
   1.238 +  then have cong: "convergent (\<lambda>n. prod f {..n}) = convergent (\<lambda>n. C * prod g {..n})"
   1.239 +    by (rule convergent_cong)
   1.240 +  show ?thesis
   1.241 +  proof
   1.242 +    assume cf: "convergent_prod f"
   1.243 +    then have "\<not> (\<lambda>n. prod g {..n}) \<longlonglongrightarrow> 0"
   1.244 +      using tendsto_mult_left * convergent_prod_to_zero_iff f filterlim_cong by fastforce
   1.245 +    then show "convergent_prod g"
   1.246 +      by (metis convergent_mult_const_iff \<open>C \<noteq> 0\<close> cong cf convergent_LIMSEQ_iff convergent_prod_iff_convergent convergent_prod_imp_convergent g)
   1.247 +  next
   1.248 +    assume cg: "convergent_prod g"
   1.249 +    have "\<exists>a. C * a \<noteq> 0 \<and> (\<lambda>n. prod g {..n}) \<longlonglongrightarrow> a"
   1.250 +      by (metis (no_types) \<open>C \<noteq> 0\<close> cg convergent_prod_iff_nz_lim divide_eq_0_iff g nonzero_mult_div_cancel_right)
   1.251 +    then show "convergent_prod f"
   1.252 +      using "*" tendsto_mult_left filterlim_cong
   1.253 +      by (fastforce simp add: convergent_prod_iff_nz_lim f)
   1.254 +  qed
   1.255  qed
   1.256  
   1.257  end