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.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