src/HOL/Analysis/Infinite_Products.thy
 changeset 68136 f022083489d0 parent 68127 137d5d0112bb child 68138 c738f40e88d4
```     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.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.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
```