the last of the infinite product proofs
authorpaulson <lp15@cam.ac.uk>
Mon Jun 11 14:34:17 2018 +0100 (11 months ago)
changeset 6842402e5a44ffe7d
parent 68411 d8363de26567
child 68425 32f445237d36
the last of the infinite product proofs
src/HOL/Analysis/Infinite_Products.thy
     1.1 --- a/src/HOL/Analysis/Infinite_Products.thy	Mon Jun 11 08:15:43 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Infinite_Products.thy	Mon Jun 11 14:34:17 2018 +0100
     1.3 @@ -6,9 +6,11 @@
     1.4  *)
     1.5  section \<open>Infinite Products\<close>
     1.6  theory Infinite_Products
     1.7 -  imports Complex_Main
     1.8 +  imports Topology_Euclidean_Space
     1.9  begin
    1.10 -    
    1.11 +
    1.12 +subsection\<open>Preliminaries\<close>
    1.13 +
    1.14  lemma sum_le_prod:
    1.15    fixes f :: "'a \<Rightarrow> 'b :: linordered_semidom"
    1.16    assumes "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> 0"
    1.17 @@ -50,6 +52,8 @@
    1.18      by (rule tendsto_eq_intros refl | simp)+
    1.19  qed auto
    1.20  
    1.21 +subsection\<open>Definitions and basic properties\<close>
    1.22 +
    1.23  definition raw_has_prod :: "[nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}, nat, 'a] \<Rightarrow> bool" 
    1.24    where "raw_has_prod f M p \<equiv> (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> p \<and> p \<noteq> 0"
    1.25  
    1.26 @@ -135,6 +139,9 @@
    1.27      by blast
    1.28  qed (auto simp: prod_defs)
    1.29  
    1.30 +
    1.31 +subsection\<open>Absolutely convergent products\<close>
    1.32 +
    1.33  definition abs_convergent_prod :: "(nat \<Rightarrow> _) \<Rightarrow> bool" where
    1.34    "abs_convergent_prod f \<longleftrightarrow> convergent_prod (\<lambda>i. 1 + norm (f i - 1))"
    1.35  
    1.36 @@ -383,6 +390,8 @@
    1.37    shows   "abs_convergent_prod f"
    1.38    using assms unfolding abs_convergent_prod_def by (rule convergent_prod_offset)
    1.39  
    1.40 +subsection\<open>Ignoring initial segments\<close>
    1.41 +
    1.42  lemma raw_has_prod_ignore_initial_segment:
    1.43    fixes f :: "nat \<Rightarrow> 'a :: real_normed_field"
    1.44    assumes "raw_has_prod f M p" "N \<ge> M"
    1.45 @@ -569,6 +578,8 @@
    1.46    with L show ?thesis by (auto simp: prod_defs)
    1.47  qed
    1.48  
    1.49 +subsection\<open>More elementary properties\<close>
    1.50 +
    1.51  lemma raw_has_prod_cases:
    1.52    fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}"
    1.53    assumes "raw_has_prod f M p"
    1.54 @@ -1040,7 +1051,7 @@
    1.55    using convergent_prod_def raw_has_prodI_bounded [OF assms] by blast
    1.56  
    1.57  
    1.58 -subsection \<open>Infinite products on topological monoids\<close>
    1.59 +subsection \<open>Infinite products on topological spaces\<close>
    1.60  
    1.61  context
    1.62    fixes f g :: "nat \<Rightarrow> 'a::{t2_space,topological_semigroup_mult,idom}"
    1.63 @@ -1141,7 +1152,7 @@
    1.64  
    1.65  end
    1.66  
    1.67 -subsection \<open>Infinite summability on real normed vector spaces\<close>
    1.68 +subsection \<open>Infinite summability on real normed fields\<close>
    1.69  
    1.70  context
    1.71    fixes f :: "nat \<Rightarrow> 'a::real_normed_field"
    1.72 @@ -1224,7 +1235,7 @@
    1.73  
    1.74  end
    1.75  
    1.76 -context (* Separate contexts are necessary to allow general use of the results above, here. *)
    1.77 +context 
    1.78    fixes f :: "nat \<Rightarrow> 'a::real_normed_field"
    1.79  begin
    1.80  
    1.81 @@ -1298,7 +1309,7 @@
    1.82  
    1.83  end
    1.84  
    1.85 -context (* Separate contexts are necessary to allow general use of the results above, here. *)
    1.86 +context 
    1.87    fixes f :: "nat \<Rightarrow> 'a::real_normed_field"
    1.88  begin
    1.89  
    1.90 @@ -1329,4 +1340,128 @@
    1.91  
    1.92  end
    1.93  
    1.94 +
    1.95 +subsection\<open>Exponentials and logarithms\<close>
    1.96 +
    1.97 +context 
    1.98 +  fixes f :: "nat \<Rightarrow> 'a::{real_normed_field,banach}"
    1.99 +begin
   1.100 +
   1.101 +lemma sums_imp_has_prod_exp: 
   1.102 +  assumes "f sums s"
   1.103 +  shows "raw_has_prod (\<lambda>i. exp (f i)) 0 (exp s)"
   1.104 +  using assms continuous_on_exp [of UNIV "\<lambda>x::'a. x"]
   1.105 +  using continuous_on_tendsto_compose [of UNIV exp "(\<lambda>n. sum f {..n})" s]
   1.106 +  by (simp add: prod_defs sums_def_le exp_sum)
   1.107 +
   1.108 +lemma convergent_prod_exp: 
   1.109 +  assumes "summable f"
   1.110 +  shows "convergent_prod (\<lambda>i. exp (f i))"
   1.111 +  using sums_imp_has_prod_exp assms unfolding summable_def convergent_prod_def  by blast
   1.112 +
   1.113 +lemma prodinf_exp: 
   1.114 +  assumes "summable f"
   1.115 +  shows "prodinf (\<lambda>i. exp (f i)) = exp (suminf f)"
   1.116 +proof -
   1.117 +  have "f sums suminf f"
   1.118 +    using assms by blast
   1.119 +  then have "(\<lambda>i. exp (f i)) has_prod exp (suminf f)"
   1.120 +    by (simp add: has_prod_def sums_imp_has_prod_exp)
   1.121 +  then show ?thesis
   1.122 +    by (rule has_prod_unique [symmetric])
   1.123 +qed
   1.124 +
   1.125  end
   1.126 +
   1.127 +lemma has_prod_imp_sums_ln_real: 
   1.128 +  fixes f :: "nat \<Rightarrow> real"
   1.129 +  assumes "raw_has_prod f 0 p" and 0: "\<And>x. f x > 0"
   1.130 +  shows "(\<lambda>i. ln (f i)) sums (ln p)"
   1.131 +proof -
   1.132 +  have "p > 0"
   1.133 +    using assms unfolding prod_defs by (metis LIMSEQ_prod_nonneg less_eq_real_def)
   1.134 +  then show ?thesis
   1.135 +  using assms continuous_on_ln [of "{0<..}" "\<lambda>x. x"]
   1.136 +  using continuous_on_tendsto_compose [of "{0<..}" ln "(\<lambda>n. prod f {..n})" p]
   1.137 +  by (auto simp: prod_defs sums_def_le ln_prod order_tendstoD)
   1.138 +qed
   1.139 +
   1.140 +lemma summable_ln_real: 
   1.141 +  fixes f :: "nat \<Rightarrow> real"
   1.142 +  assumes f: "convergent_prod f" and 0: "\<And>x. f x > 0"
   1.143 +  shows "summable (\<lambda>i. ln (f i))"
   1.144 +proof -
   1.145 +  obtain M p where "raw_has_prod f M p"
   1.146 +    using f convergent_prod_def by blast
   1.147 +  then consider i where "i<M" "f i = 0" | p where "raw_has_prod f 0 p"
   1.148 +    using raw_has_prod_cases by blast
   1.149 +  then show ?thesis
   1.150 +  proof cases
   1.151 +    case 1
   1.152 +    with 0 show ?thesis
   1.153 +      by (metis less_irrefl)
   1.154 +  next
   1.155 +    case 2
   1.156 +    then show ?thesis
   1.157 +      using "0" has_prod_imp_sums_ln_real summable_def by blast
   1.158 +  qed
   1.159 +qed
   1.160 +
   1.161 +lemma suminf_ln_real: 
   1.162 +  fixes f :: "nat \<Rightarrow> real"
   1.163 +  assumes f: "convergent_prod f" and 0: "\<And>x. f x > 0"
   1.164 +  shows "suminf (\<lambda>i. ln (f i)) = ln (prodinf f)"
   1.165 +proof -
   1.166 +  have "f has_prod prodinf f"
   1.167 +    by (simp add: f has_prod_iff)
   1.168 +  then have "raw_has_prod f 0 (prodinf f)"
   1.169 +    by (metis "0" has_prod_def less_irrefl)
   1.170 +  then have "(\<lambda>i. ln (f i)) sums ln (prodinf f)"
   1.171 +    using "0" has_prod_imp_sums_ln_real by blast
   1.172 +  then show ?thesis
   1.173 +    by (rule sums_unique [symmetric])
   1.174 +qed
   1.175 +
   1.176 +lemma prodinf_exp_real: 
   1.177 +  fixes f :: "nat \<Rightarrow> real"
   1.178 +  assumes f: "convergent_prod f" and 0: "\<And>x. f x > 0"
   1.179 +  shows "prodinf f = exp (suminf (\<lambda>i. ln (f i)))"
   1.180 +  by (simp add: "0" f less_0_prodinf suminf_ln_real)
   1.181 +
   1.182 +
   1.183 +subsection\<open>Embeddings from the reals into some complete real normed field\<close>
   1.184 +
   1.185 +lemma tendsto_of_real:
   1.186 +  assumes "(\<lambda>n. of_real (f n) :: 'a::{complete_space,real_normed_field}) \<longlonglongrightarrow> q"
   1.187 +  shows "q = of_real (lim f)"
   1.188 +proof -
   1.189 +  have "convergent (\<lambda>n. of_real (f n) :: 'a)"
   1.190 +    using assms convergent_def by blast 
   1.191 +  then have "convergent f"
   1.192 +    unfolding convergent_def
   1.193 +    by (simp add: convergent_eq_Cauchy Cauchy_def)
   1.194 +  then show ?thesis
   1.195 +    by (metis LIMSEQ_unique assms convergentD sequentially_bot tendsto_Lim tendsto_of_real)
   1.196 +qed
   1.197 +
   1.198 +lemma tendsto_of_real':
   1.199 +  assumes "(\<lambda>n. of_real (f n) :: 'a::{complete_space,real_normed_field}) \<longlonglongrightarrow> q"
   1.200 +  obtains r where "q = of_real r"
   1.201 +  using tendsto_of_real assms by blast
   1.202 +
   1.203 +lemma has_prod_of_real_iff:
   1.204 +  "(\<lambda>n. of_real (f n) :: 'a::{complete_space,real_normed_field}) has_prod of_real c \<longleftrightarrow> f has_prod c"
   1.205 +  (is "?lhs = ?rhs")
   1.206 +proof
   1.207 +  assume ?lhs
   1.208 +  then show ?rhs
   1.209 +    apply (auto simp: prod_defs LIMSEQ_prod_0 tendsto_of_real_iff simp flip: of_real_prod)
   1.210 +    using tendsto_of_real'
   1.211 +    by (metis of_real_0 tendsto_of_real_iff)
   1.212 +next
   1.213 +  assume ?rhs
   1.214 +  with tendsto_of_real_iff show ?lhs
   1.215 +    by (fastforce simp: prod_defs simp flip: of_real_prod)
   1.216 +qed
   1.217 +
   1.218 +end