src/HOL/Analysis/Infinite_Products.thy
 author eberlm Sat Jul 15 14:33:56 2017 +0100 (2017-07-15) changeset 66277 512b0dc09061 child 68064 b249fab48c76 permissions -rw-r--r--
HOL-Analysis: Infinite products
 eberlm@66277 ` 1` ```(* ``` eberlm@66277 ` 2` ``` File: HOL/Analysis/Infinite_Product.thy ``` eberlm@66277 ` 3` ``` Author: Manuel Eberl ``` eberlm@66277 ` 4` eberlm@66277 ` 5` ``` Basic results about convergence and absolute convergence of infinite products ``` eberlm@66277 ` 6` ``` and their connection to summability. ``` eberlm@66277 ` 7` ```*) ``` eberlm@66277 ` 8` ```section \Infinite Products\ ``` eberlm@66277 ` 9` ```theory Infinite_Products ``` eberlm@66277 ` 10` ``` imports Complex_Main ``` eberlm@66277 ` 11` ```begin ``` eberlm@66277 ` 12` eberlm@66277 ` 13` ```lemma sum_le_prod: ``` eberlm@66277 ` 14` ``` fixes f :: "'a \ 'b :: linordered_semidom" ``` eberlm@66277 ` 15` ``` assumes "\x. x \ A \ f x \ 0" ``` eberlm@66277 ` 16` ``` shows "sum f A \ (\x\A. 1 + f x)" ``` eberlm@66277 ` 17` ``` using assms ``` eberlm@66277 ` 18` ```proof (induction A rule: infinite_finite_induct) ``` eberlm@66277 ` 19` ``` case (insert x A) ``` eberlm@66277 ` 20` ``` from insert.hyps have "sum f A + f x * (\x\A. 1) \ (\x\A. 1 + f x) + f x * (\x\A. 1 + f x)" ``` eberlm@66277 ` 21` ``` by (intro add_mono insert mult_left_mono prod_mono) (auto intro: insert.prems) ``` eberlm@66277 ` 22` ``` with insert.hyps show ?case by (simp add: algebra_simps) ``` eberlm@66277 ` 23` ```qed simp_all ``` eberlm@66277 ` 24` eberlm@66277 ` 25` ```lemma prod_le_exp_sum: ``` eberlm@66277 ` 26` ``` fixes f :: "'a \ real" ``` eberlm@66277 ` 27` ``` assumes "\x. x \ A \ f x \ 0" ``` eberlm@66277 ` 28` ``` shows "prod (\x. 1 + f x) A \ exp (sum f A)" ``` eberlm@66277 ` 29` ``` using assms ``` eberlm@66277 ` 30` ```proof (induction A rule: infinite_finite_induct) ``` eberlm@66277 ` 31` ``` case (insert x A) ``` eberlm@66277 ` 32` ``` have "(1 + f x) * (\x\A. 1 + f x) \ exp (f x) * exp (sum f A)" ``` eberlm@66277 ` 33` ``` using insert.prems by (intro mult_mono insert prod_nonneg exp_ge_add_one_self) auto ``` eberlm@66277 ` 34` ``` with insert.hyps show ?case by (simp add: algebra_simps exp_add) ``` eberlm@66277 ` 35` ```qed simp_all ``` eberlm@66277 ` 36` eberlm@66277 ` 37` ```lemma lim_ln_1_plus_x_over_x_at_0: "(\x::real. ln (1 + x) / x) \0\ 1" ``` eberlm@66277 ` 38` ```proof (rule lhopital) ``` eberlm@66277 ` 39` ``` show "(\x::real. ln (1 + x)) \0\ 0" ``` eberlm@66277 ` 40` ``` by (rule tendsto_eq_intros refl | simp)+ ``` eberlm@66277 ` 41` ``` have "eventually (\x::real. x \ {-1/2<..<1/2}) (nhds 0)" ``` eberlm@66277 ` 42` ``` by (rule eventually_nhds_in_open) auto ``` eberlm@66277 ` 43` ``` hence *: "eventually (\x::real. x \ {-1/2<..<1/2}) (at 0)" ``` eberlm@66277 ` 44` ``` by (rule filter_leD [rotated]) (simp_all add: at_within_def) ``` eberlm@66277 ` 45` ``` show "eventually (\x::real. ((\x. ln (1 + x)) has_field_derivative inverse (1 + x)) (at x)) (at 0)" ``` eberlm@66277 ` 46` ``` using * by eventually_elim (auto intro!: derivative_eq_intros simp: field_simps) ``` eberlm@66277 ` 47` ``` show "eventually (\x::real. ((\x. x) has_field_derivative 1) (at x)) (at 0)" ``` eberlm@66277 ` 48` ``` using * by eventually_elim (auto intro!: derivative_eq_intros simp: field_simps) ``` eberlm@66277 ` 49` ``` show "\\<^sub>F x in at 0. x \ 0" by (auto simp: at_within_def eventually_inf_principal) ``` eberlm@66277 ` 50` ``` show "(\x::real. inverse (1 + x) / 1) \0\ 1" ``` eberlm@66277 ` 51` ``` by (rule tendsto_eq_intros refl | simp)+ ``` eberlm@66277 ` 52` ```qed auto ``` eberlm@66277 ` 53` eberlm@66277 ` 54` ```definition convergent_prod :: "(nat \ 'a :: {t2_space,comm_semiring_1}) \ bool" where ``` eberlm@66277 ` 55` ``` "convergent_prod f \ (\M L. (\n. \i\n. f (i+M)) \ L \ L \ 0)" ``` eberlm@66277 ` 56` eberlm@66277 ` 57` ```lemma convergent_prod_altdef: ``` eberlm@66277 ` 58` ``` fixes f :: "nat \ 'a :: {t2_space,comm_semiring_1}" ``` eberlm@66277 ` 59` ``` shows "convergent_prod f \ (\M L. (\n\M. f n \ 0) \ (\n. \i\n. f (i+M)) \ L \ L \ 0)" ``` eberlm@66277 ` 60` ```proof ``` eberlm@66277 ` 61` ``` assume "convergent_prod f" ``` eberlm@66277 ` 62` ``` then obtain M L where *: "(\n. \i\n. f (i+M)) \ L" "L \ 0" ``` eberlm@66277 ` 63` ``` by (auto simp: convergent_prod_def) ``` eberlm@66277 ` 64` ``` have "f i \ 0" if "i \ M" for i ``` eberlm@66277 ` 65` ``` proof ``` eberlm@66277 ` 66` ``` assume "f i = 0" ``` eberlm@66277 ` 67` ``` have **: "eventually (\n. (\i\n. f (i+M)) = 0) sequentially" ``` eberlm@66277 ` 68` ``` using eventually_ge_at_top[of "i - M"] ``` eberlm@66277 ` 69` ``` proof eventually_elim ``` eberlm@66277 ` 70` ``` case (elim n) ``` eberlm@66277 ` 71` ``` with \f i = 0\ and \i \ M\ show ?case ``` eberlm@66277 ` 72` ``` by (auto intro!: bexI[of _ "i - M"] prod_zero) ``` eberlm@66277 ` 73` ``` qed ``` eberlm@66277 ` 74` ``` have "(\n. (\i\n. f (i+M))) \ 0" ``` eberlm@66277 ` 75` ``` unfolding filterlim_iff ``` eberlm@66277 ` 76` ``` by (auto dest!: eventually_nhds_x_imp_x intro!: eventually_mono[OF **]) ``` eberlm@66277 ` 77` ``` from tendsto_unique[OF _ this *(1)] and *(2) ``` eberlm@66277 ` 78` ``` show False by simp ``` eberlm@66277 ` 79` ``` qed ``` eberlm@66277 ` 80` ``` with * show "(\M L. (\n\M. f n \ 0) \ (\n. \i\n. f (i+M)) \ L \ L \ 0)" ``` eberlm@66277 ` 81` ``` by blast ``` eberlm@66277 ` 82` ```qed (auto simp: convergent_prod_def) ``` eberlm@66277 ` 83` eberlm@66277 ` 84` ```definition abs_convergent_prod :: "(nat \ _) \ bool" where ``` eberlm@66277 ` 85` ``` "abs_convergent_prod f \ convergent_prod (\i. 1 + norm (f i - 1))" ``` eberlm@66277 ` 86` eberlm@66277 ` 87` ```lemma abs_convergent_prodI: ``` eberlm@66277 ` 88` ``` assumes "convergent (\n. \i\n. 1 + norm (f i - 1))" ``` eberlm@66277 ` 89` ``` shows "abs_convergent_prod f" ``` eberlm@66277 ` 90` ```proof - ``` eberlm@66277 ` 91` ``` from assms obtain L where L: "(\n. \i\n. 1 + norm (f i - 1)) \ L" ``` eberlm@66277 ` 92` ``` by (auto simp: convergent_def) ``` eberlm@66277 ` 93` ``` have "L \ 1" ``` eberlm@66277 ` 94` ``` proof (rule tendsto_le) ``` eberlm@66277 ` 95` ``` show "eventually (\n. (\i\n. 1 + norm (f i - 1)) \ 1) sequentially" ``` eberlm@66277 ` 96` ``` proof (intro always_eventually allI) ``` eberlm@66277 ` 97` ``` fix n ``` eberlm@66277 ` 98` ``` have "(\i\n. 1 + norm (f i - 1)) \ (\i\n. 1)" ``` eberlm@66277 ` 99` ``` by (intro prod_mono) auto ``` eberlm@66277 ` 100` ``` thus "(\i\n. 1 + norm (f i - 1)) \ 1" by simp ``` eberlm@66277 ` 101` ``` qed ``` eberlm@66277 ` 102` ``` qed (use L in simp_all) ``` eberlm@66277 ` 103` ``` hence "L \ 0" by auto ``` eberlm@66277 ` 104` ``` with L show ?thesis unfolding abs_convergent_prod_def convergent_prod_def ``` eberlm@66277 ` 105` ``` by (intro exI[of _ "0::nat"] exI[of _ L]) auto ``` eberlm@66277 ` 106` ```qed ``` eberlm@66277 ` 107` eberlm@66277 ` 108` ```lemma ``` eberlm@66277 ` 109` ``` fixes f :: "nat \ 'a :: {real_normed_div_algebra,idom}" ``` eberlm@66277 ` 110` ``` assumes "convergent_prod f" ``` eberlm@66277 ` 111` ``` shows convergent_prod_imp_convergent: "convergent (\n. \i\n. f i)" ``` eberlm@66277 ` 112` ``` and convergent_prod_to_zero_iff: "(\n. \i\n. f i) \ 0 \ (\i. f i = 0)" ``` eberlm@66277 ` 113` ```proof - ``` eberlm@66277 ` 114` ``` from assms obtain M L ``` eberlm@66277 ` 115` ``` where M: "\n. n \ M \ f n \ 0" and "(\n. \i\n. f (i + M)) \ L" and "L \ 0" ``` eberlm@66277 ` 116` ``` by (auto simp: convergent_prod_altdef) ``` eberlm@66277 ` 117` ``` note this(2) ``` eberlm@66277 ` 118` ``` also have "(\n. \i\n. f (i + M)) = (\n. \i=M..M+n. f i)" ``` eberlm@66277 ` 119` ``` by (intro ext prod.reindex_bij_witness[of _ "\n. n - M" "\n. n + M"]) auto ``` eberlm@66277 ` 120` ``` finally have "(\n. (\ii=M..M+n. f i)) \ (\in. (\ii=M..M+n. f i)) = (\n. (\i\{..{M..M+n}. f i))" ``` eberlm@66277 ` 123` ``` by (subst prod.union_disjoint) auto ``` eberlm@66277 ` 124` ``` also have "(\n. {.. {M..M+n}) = (\n. {..n+M})" by auto ``` eberlm@66277 ` 125` ``` finally have lim: "(\n. prod f {..n}) \ prod f {..n. \i\n. f i)" ``` eberlm@66277 ` 128` ``` by (auto simp: convergent_def) ``` eberlm@66277 ` 129` eberlm@66277 ` 130` ``` show "(\n. \i\n. f i) \ 0 \ (\i. f i = 0)" ``` eberlm@66277 ` 131` ``` proof ``` eberlm@66277 ` 132` ``` assume "\i. f i = 0" ``` eberlm@66277 ` 133` ``` then obtain i where "f i = 0" by auto ``` eberlm@66277 ` 134` ``` moreover with M have "i < M" by (cases "i < M") auto ``` eberlm@66277 ` 135` ``` ultimately have "(\in. \i\n. f i) \ 0" by simp ``` eberlm@66277 ` 137` ``` next ``` eberlm@66277 ` 138` ``` assume "(\n. \i\n. f i) \ 0" ``` eberlm@66277 ` 139` ``` from tendsto_unique[OF _ this lim] and \L \ 0\ ``` eberlm@66277 ` 140` ``` show "\i. f i = 0" by auto ``` eberlm@66277 ` 141` ``` qed ``` eberlm@66277 ` 142` ```qed ``` eberlm@66277 ` 143` eberlm@66277 ` 144` ```lemma abs_convergent_prod_altdef: ``` eberlm@66277 ` 145` ``` "abs_convergent_prod f \ convergent (\n. \i\n. 1 + norm (f i - 1))" ``` eberlm@66277 ` 146` ```proof ``` eberlm@66277 ` 147` ``` assume "abs_convergent_prod f" ``` eberlm@66277 ` 148` ``` thus "convergent (\n. \i\n. 1 + norm (f i - 1))" ``` eberlm@66277 ` 149` ``` by (auto simp: abs_convergent_prod_def intro!: convergent_prod_imp_convergent) ``` eberlm@66277 ` 150` ```qed (auto intro: abs_convergent_prodI) ``` eberlm@66277 ` 151` eberlm@66277 ` 152` ```lemma weierstrass_prod_ineq: ``` eberlm@66277 ` 153` ``` fixes f :: "'a \ real" ``` eberlm@66277 ` 154` ``` assumes "\x. x \ A \ f x \ {0..1}" ``` eberlm@66277 ` 155` ``` shows "1 - sum f A \ (\x\A. 1 - f x)" ``` eberlm@66277 ` 156` ``` using assms ``` eberlm@66277 ` 157` ```proof (induction A rule: infinite_finite_induct) ``` eberlm@66277 ` 158` ``` case (insert x A) ``` eberlm@66277 ` 159` ``` from insert.hyps and insert.prems ``` eberlm@66277 ` 160` ``` have "1 - sum f A + f x * (\x\A. 1 - f x) \ (\x\A. 1 - f x) + f x * (\x\A. 1)" ``` eberlm@66277 ` 161` ``` by (intro insert.IH add_mono mult_left_mono prod_mono) auto ``` eberlm@66277 ` 162` ``` with insert.hyps show ?case by (simp add: algebra_simps) ``` eberlm@66277 ` 163` ```qed simp_all ``` eberlm@66277 ` 164` eberlm@66277 ` 165` ```lemma norm_prod_minus1_le_prod_minus1: ``` eberlm@66277 ` 166` ``` fixes f :: "nat \ 'a :: {real_normed_div_algebra,comm_ring_1}" ``` eberlm@66277 ` 167` ``` shows "norm (prod (\n. 1 + f n) A - 1) \ prod (\n. 1 + norm (f n)) A - 1" ``` eberlm@66277 ` 168` ```proof (induction A rule: infinite_finite_induct) ``` eberlm@66277 ` 169` ``` case (insert x A) ``` eberlm@66277 ` 170` ``` from insert.hyps have ``` eberlm@66277 ` 171` ``` "norm ((\n\insert x A. 1 + f n) - 1) = ``` eberlm@66277 ` 172` ``` norm ((\n\A. 1 + f n) - 1 + f x * (\n\A. 1 + f n))" ``` eberlm@66277 ` 173` ``` by (simp add: algebra_simps) ``` eberlm@66277 ` 174` ``` also have "\ \ norm ((\n\A. 1 + f n) - 1) + norm (f x * (\n\A. 1 + f n))" ``` eberlm@66277 ` 175` ``` by (rule norm_triangle_ineq) ``` eberlm@66277 ` 176` ``` also have "norm (f x * (\n\A. 1 + f n)) = norm (f x) * (\x\A. norm (1 + f x))" ``` eberlm@66277 ` 177` ``` by (simp add: prod_norm norm_mult) ``` eberlm@66277 ` 178` ``` also have "(\x\A. norm (1 + f x)) \ (\x\A. norm (1::'a) + norm (f x))" ``` eberlm@66277 ` 179` ``` by (intro prod_mono norm_triangle_ineq ballI conjI) auto ``` eberlm@66277 ` 180` ``` also have "norm (1::'a) = 1" by simp ``` eberlm@66277 ` 181` ``` also note insert.IH ``` eberlm@66277 ` 182` ``` also have "(\n\A. 1 + norm (f n)) - 1 + norm (f x) * (\x\A. 1 + norm (f x)) = ``` eberlm@66277 ` 183` ``` (\n\insert x A. 1 + norm (f n)) - 1" ``` eberlm@66277 ` 184` ``` using insert.hyps by (simp add: algebra_simps) ``` eberlm@66277 ` 185` ``` finally show ?case by - (simp_all add: mult_left_mono) ``` eberlm@66277 ` 186` ```qed simp_all ``` eberlm@66277 ` 187` eberlm@66277 ` 188` ```lemma convergent_prod_imp_ev_nonzero: ``` eberlm@66277 ` 189` ``` fixes f :: "nat \ 'a :: {t2_space,comm_semiring_1}" ``` eberlm@66277 ` 190` ``` assumes "convergent_prod f" ``` eberlm@66277 ` 191` ``` shows "eventually (\n. f n \ 0) sequentially" ``` eberlm@66277 ` 192` ``` using assms by (auto simp: eventually_at_top_linorder convergent_prod_altdef) ``` eberlm@66277 ` 193` eberlm@66277 ` 194` ```lemma convergent_prod_imp_LIMSEQ: ``` eberlm@66277 ` 195` ``` fixes f :: "nat \ 'a :: {real_normed_field}" ``` eberlm@66277 ` 196` ``` assumes "convergent_prod f" ``` eberlm@66277 ` 197` ``` shows "f \ 1" ``` eberlm@66277 ` 198` ```proof - ``` eberlm@66277 ` 199` ``` from assms obtain M L where L: "(\n. \i\n. f (i+M)) \ L" "\n. n \ M \ f n \ 0" "L \ 0" ``` eberlm@66277 ` 200` ``` by (auto simp: convergent_prod_altdef) ``` eberlm@66277 ` 201` ``` hence L': "(\n. \i\Suc n. f (i+M)) \ L" by (subst filterlim_sequentially_Suc) ``` eberlm@66277 ` 202` ``` have "(\n. (\i\Suc n. f (i+M)) / (\i\n. f (i+M))) \ L / L" ``` eberlm@66277 ` 203` ``` using L L' by (intro tendsto_divide) simp_all ``` eberlm@66277 ` 204` ``` also from L have "L / L = 1" by simp ``` eberlm@66277 ` 205` ``` also have "(\n. (\i\Suc n. f (i+M)) / (\i\n. f (i+M))) = (\n. f (n + Suc M))" ``` eberlm@66277 ` 206` ``` using assms L by (auto simp: fun_eq_iff atMost_Suc) ``` eberlm@66277 ` 207` ``` finally show ?thesis by (rule LIMSEQ_offset) ``` eberlm@66277 ` 208` ```qed ``` eberlm@66277 ` 209` eberlm@66277 ` 210` ```lemma abs_convergent_prod_imp_summable: ``` eberlm@66277 ` 211` ``` fixes f :: "nat \ 'a :: real_normed_div_algebra" ``` eberlm@66277 ` 212` ``` assumes "abs_convergent_prod f" ``` eberlm@66277 ` 213` ``` shows "summable (\i. norm (f i - 1))" ``` eberlm@66277 ` 214` ```proof - ``` eberlm@66277 ` 215` ``` from assms have "convergent (\n. \i\n. 1 + norm (f i - 1))" ``` eberlm@66277 ` 216` ``` unfolding abs_convergent_prod_def by (rule convergent_prod_imp_convergent) ``` eberlm@66277 ` 217` ``` then obtain L where L: "(\n. \i\n. 1 + norm (f i - 1)) \ L" ``` eberlm@66277 ` 218` ``` unfolding convergent_def by blast ``` eberlm@66277 ` 219` ``` have "convergent (\n. \i\n. norm (f i - 1))" ``` eberlm@66277 ` 220` ``` proof (rule Bseq_monoseq_convergent) ``` eberlm@66277 ` 221` ``` have "eventually (\n. (\i\n. 1 + norm (f i - 1)) < L + 1) sequentially" ``` eberlm@66277 ` 222` ``` using L(1) by (rule order_tendstoD) simp_all ``` eberlm@66277 ` 223` ``` hence "\\<^sub>F x in sequentially. norm (\i\x. norm (f i - 1)) \ L + 1" ``` eberlm@66277 ` 224` ``` proof eventually_elim ``` eberlm@66277 ` 225` ``` case (elim n) ``` eberlm@66277 ` 226` ``` have "norm (\i\n. norm (f i - 1)) = (\i\n. norm (f i - 1))" ``` eberlm@66277 ` 227` ``` unfolding real_norm_def by (intro abs_of_nonneg sum_nonneg) simp_all ``` eberlm@66277 ` 228` ``` also have "\ \ (\i\n. 1 + norm (f i - 1))" by (rule sum_le_prod) auto ``` eberlm@66277 ` 229` ``` also have "\ < L + 1" by (rule elim) ``` eberlm@66277 ` 230` ``` finally show ?case by simp ``` eberlm@66277 ` 231` ``` qed ``` eberlm@66277 ` 232` ``` thus "Bseq (\n. \i\n. norm (f i - 1))" by (rule BfunI) ``` eberlm@66277 ` 233` ``` next ``` eberlm@66277 ` 234` ``` show "monoseq (\n. \i\n. norm (f i - 1))" ``` eberlm@66277 ` 235` ``` by (rule mono_SucI1) auto ``` eberlm@66277 ` 236` ``` qed ``` eberlm@66277 ` 237` ``` thus "summable (\i. norm (f i - 1))" by (simp add: summable_iff_convergent') ``` eberlm@66277 ` 238` ```qed ``` eberlm@66277 ` 239` eberlm@66277 ` 240` ```lemma summable_imp_abs_convergent_prod: ``` eberlm@66277 ` 241` ``` fixes f :: "nat \ 'a :: real_normed_div_algebra" ``` eberlm@66277 ` 242` ``` assumes "summable (\i. norm (f i - 1))" ``` eberlm@66277 ` 243` ``` shows "abs_convergent_prod f" ``` eberlm@66277 ` 244` ```proof (intro abs_convergent_prodI Bseq_monoseq_convergent) ``` eberlm@66277 ` 245` ``` show "monoseq (\n. \i\n. 1 + norm (f i - 1))" ``` eberlm@66277 ` 246` ``` by (intro mono_SucI1) ``` eberlm@66277 ` 247` ``` (auto simp: atMost_Suc algebra_simps intro!: mult_nonneg_nonneg prod_nonneg) ``` eberlm@66277 ` 248` ```next ``` eberlm@66277 ` 249` ``` show "Bseq (\n. \i\n. 1 + norm (f i - 1))" ``` eberlm@66277 ` 250` ``` proof (rule Bseq_eventually_mono) ``` eberlm@66277 ` 251` ``` show "eventually (\n. norm (\i\n. 1 + norm (f i - 1)) \ ``` eberlm@66277 ` 252` ``` norm (exp (\i\n. norm (f i - 1)))) sequentially" ``` eberlm@66277 ` 253` ``` by (intro always_eventually allI) (auto simp: abs_prod exp_sum intro!: prod_mono) ``` eberlm@66277 ` 254` ``` next ``` eberlm@66277 ` 255` ``` from assms have "(\n. \i\n. norm (f i - 1)) \ (\i. norm (f i - 1))" ``` eberlm@66277 ` 256` ``` using sums_def_le by blast ``` eberlm@66277 ` 257` ``` hence "(\n. exp (\i\n. norm (f i - 1))) \ exp (\i. norm (f i - 1))" ``` eberlm@66277 ` 258` ``` by (rule tendsto_exp) ``` eberlm@66277 ` 259` ``` hence "convergent (\n. exp (\i\n. norm (f i - 1)))" ``` eberlm@66277 ` 260` ``` by (rule convergentI) ``` eberlm@66277 ` 261` ``` thus "Bseq (\n. exp (\i\n. norm (f i - 1)))" ``` eberlm@66277 ` 262` ``` by (rule convergent_imp_Bseq) ``` eberlm@66277 ` 263` ``` qed ``` eberlm@66277 ` 264` ```qed ``` eberlm@66277 ` 265` eberlm@66277 ` 266` ```lemma abs_convergent_prod_conv_summable: ``` eberlm@66277 ` 267` ``` fixes f :: "nat \ 'a :: real_normed_div_algebra" ``` eberlm@66277 ` 268` ``` shows "abs_convergent_prod f \ summable (\i. norm (f i - 1))" ``` eberlm@66277 ` 269` ``` by (blast intro: abs_convergent_prod_imp_summable summable_imp_abs_convergent_prod) ``` eberlm@66277 ` 270` eberlm@66277 ` 271` ```lemma abs_convergent_prod_imp_LIMSEQ: ``` eberlm@66277 ` 272` ``` fixes f :: "nat \ 'a :: {comm_ring_1,real_normed_div_algebra}" ``` eberlm@66277 ` 273` ``` assumes "abs_convergent_prod f" ``` eberlm@66277 ` 274` ``` shows "f \ 1" ``` eberlm@66277 ` 275` ```proof - ``` eberlm@66277 ` 276` ``` from assms have "summable (\n. norm (f n - 1))" ``` eberlm@66277 ` 277` ``` by (rule abs_convergent_prod_imp_summable) ``` eberlm@66277 ` 278` ``` from summable_LIMSEQ_zero[OF this] have "(\n. f n - 1) \ 0" ``` eberlm@66277 ` 279` ``` by (simp add: tendsto_norm_zero_iff) ``` eberlm@66277 ` 280` ``` from tendsto_add[OF this tendsto_const[of 1]] show ?thesis by simp ``` eberlm@66277 ` 281` ```qed ``` eberlm@66277 ` 282` eberlm@66277 ` 283` ```lemma abs_convergent_prod_imp_ev_nonzero: ``` eberlm@66277 ` 284` ``` fixes f :: "nat \ 'a :: {comm_ring_1,real_normed_div_algebra}" ``` eberlm@66277 ` 285` ``` assumes "abs_convergent_prod f" ``` eberlm@66277 ` 286` ``` shows "eventually (\n. f n \ 0) sequentially" ``` eberlm@66277 ` 287` ```proof - ``` eberlm@66277 ` 288` ``` from assms have "f \ 1" ``` eberlm@66277 ` 289` ``` by (rule abs_convergent_prod_imp_LIMSEQ) ``` eberlm@66277 ` 290` ``` hence "eventually (\n. dist (f n) 1 < 1) at_top" ``` eberlm@66277 ` 291` ``` by (auto simp: tendsto_iff) ``` eberlm@66277 ` 292` ``` thus ?thesis by eventually_elim auto ``` eberlm@66277 ` 293` ```qed ``` eberlm@66277 ` 294` eberlm@66277 ` 295` ```lemma convergent_prod_offset: ``` eberlm@66277 ` 296` ``` assumes "convergent_prod (\n. f (n + m))" ``` eberlm@66277 ` 297` ``` shows "convergent_prod f" ``` eberlm@66277 ` 298` ```proof - ``` eberlm@66277 ` 299` ``` from assms obtain M L where "(\n. \k\n. f (k + (M + m))) \ L" "L \ 0" ``` eberlm@66277 ` 300` ``` by (auto simp: convergent_prod_def add.assoc) ``` eberlm@66277 ` 301` ``` thus "convergent_prod f" unfolding convergent_prod_def by blast ``` eberlm@66277 ` 302` ```qed ``` eberlm@66277 ` 303` eberlm@66277 ` 304` ```lemma abs_convergent_prod_offset: ``` eberlm@66277 ` 305` ``` assumes "abs_convergent_prod (\n. f (n + m))" ``` eberlm@66277 ` 306` ``` shows "abs_convergent_prod f" ``` eberlm@66277 ` 307` ``` using assms unfolding abs_convergent_prod_def by (rule convergent_prod_offset) ``` eberlm@66277 ` 308` eberlm@66277 ` 309` ```lemma convergent_prod_ignore_initial_segment: ``` eberlm@66277 ` 310` ``` fixes f :: "nat \ 'a :: {real_normed_field}" ``` eberlm@66277 ` 311` ``` assumes "convergent_prod f" ``` eberlm@66277 ` 312` ``` shows "convergent_prod (\n. f (n + m))" ``` eberlm@66277 ` 313` ```proof - ``` eberlm@66277 ` 314` ``` from assms obtain M L ``` eberlm@66277 ` 315` ``` where L: "(\n. \k\n. f (k + M)) \ L" "L \ 0" and nz: "\n. n \ M \ f n \ 0" ``` eberlm@66277 ` 316` ``` by (auto simp: convergent_prod_altdef) ``` eberlm@66277 ` 317` ``` define C where "C = (\k 0" ``` eberlm@66277 ` 319` ``` by (auto simp: C_def) ``` eberlm@66277 ` 320` eberlm@66277 ` 321` ``` from L(1) have "(\n. \k\n+m. f (k + M)) \ L" ``` eberlm@66277 ` 322` ``` by (rule LIMSEQ_ignore_initial_segment) ``` eberlm@66277 ` 323` ``` also have "(\n. \k\n+m. f (k + M)) = (\n. C * (\k\n. f (k + M + m)))" ``` eberlm@66277 ` 324` ``` proof (rule ext, goal_cases) ``` eberlm@66277 ` 325` ``` case (1 n) ``` eberlm@66277 ` 326` ``` have "{..n+m} = {.. {m..n+m}" by auto ``` eberlm@66277 ` 327` ``` also have "(\k\\. f (k + M)) = C * (\k=m..n+m. f (k + M))" ``` eberlm@66277 ` 328` ``` unfolding C_def by (rule prod.union_disjoint) auto ``` eberlm@66277 ` 329` ``` also have "(\k=m..n+m. f (k + M)) = (\k\n. f (k + m + M))" ``` eberlm@66277 ` 330` ``` by (intro ext prod.reindex_bij_witness[of _ "\k. k + m" "\k. k - m"]) auto ``` eberlm@66277 ` 331` ``` finally show ?case by (simp add: add_ac) ``` eberlm@66277 ` 332` ``` qed ``` eberlm@66277 ` 333` ``` finally have "(\n. C * (\k\n. f (k + M + m)) / C) \ L / C" ``` eberlm@66277 ` 334` ``` by (intro tendsto_divide tendsto_const) auto ``` eberlm@66277 ` 335` ``` hence "(\n. \k\n. f (k + M + m)) \ L / C" by simp ``` eberlm@66277 ` 336` ``` moreover from \L \ 0\ have "L / C \ 0" by simp ``` eberlm@66277 ` 337` ``` ultimately show ?thesis unfolding convergent_prod_def by blast ``` eberlm@66277 ` 338` ```qed ``` eberlm@66277 ` 339` eberlm@66277 ` 340` ```lemma abs_convergent_prod_ignore_initial_segment: ``` eberlm@66277 ` 341` ``` assumes "abs_convergent_prod f" ``` eberlm@66277 ` 342` ``` shows "abs_convergent_prod (\n. f (n + m))" ``` eberlm@66277 ` 343` ``` using assms unfolding abs_convergent_prod_def ``` eberlm@66277 ` 344` ``` by (rule convergent_prod_ignore_initial_segment) ``` eberlm@66277 ` 345` eberlm@66277 ` 346` ```lemma summable_LIMSEQ': ``` eberlm@66277 ` 347` ``` assumes "summable (f::nat\'a::{t2_space,comm_monoid_add})" ``` eberlm@66277 ` 348` ``` shows "(\n. \i\n. f i) \ suminf f" ``` eberlm@66277 ` 349` ``` using assms sums_def_le by blast ``` eberlm@66277 ` 350` eberlm@66277 ` 351` ```lemma abs_convergent_prod_imp_convergent_prod: ``` eberlm@66277 ` 352` ``` fixes f :: "nat \ 'a :: {real_normed_div_algebra,complete_space,comm_ring_1}" ``` eberlm@66277 ` 353` ``` assumes "abs_convergent_prod f" ``` eberlm@66277 ` 354` ``` shows "convergent_prod f" ``` eberlm@66277 ` 355` ```proof - ``` eberlm@66277 ` 356` ``` from assms have "eventually (\n. f n \ 0) sequentially" ``` eberlm@66277 ` 357` ``` by (rule abs_convergent_prod_imp_ev_nonzero) ``` eberlm@66277 ` 358` ``` then obtain N where N: "f n \ 0" if "n \ N" for n ``` eberlm@66277 ` 359` ``` by (auto simp: eventually_at_top_linorder) ``` eberlm@66277 ` 360` ``` let ?P = "\n. \i\n. f (i + N)" and ?Q = "\n. \i\n. 1 + norm (f (i + N) - 1)" ``` eberlm@66277 ` 361` eberlm@66277 ` 362` ``` have "Cauchy ?P" ``` eberlm@66277 ` 363` ``` proof (rule CauchyI', goal_cases) ``` eberlm@66277 ` 364` ``` case (1 \) ``` eberlm@66277 ` 365` ``` from assms have "abs_convergent_prod (\n. f (n + N))" ``` eberlm@66277 ` 366` ``` by (rule abs_convergent_prod_ignore_initial_segment) ``` eberlm@66277 ` 367` ``` hence "Cauchy ?Q" ``` eberlm@66277 ` 368` ``` unfolding abs_convergent_prod_def ``` eberlm@66277 ` 369` ``` by (intro convergent_Cauchy convergent_prod_imp_convergent) ``` eberlm@66277 ` 370` ``` from CauchyD[OF this 1] obtain M where M: "norm (?Q m - ?Q n) < \" if "m \ M" "n \ M" for m n ``` eberlm@66277 ` 371` ``` by blast ``` eberlm@66277 ` 372` ``` show ?case ``` eberlm@66277 ` 373` ``` proof (rule exI[of _ M], safe, goal_cases) ``` eberlm@66277 ` 374` ``` case (1 m n) ``` eberlm@66277 ` 375` ``` have "dist (?P m) (?P n) = norm (?P n - ?P m)" ``` eberlm@66277 ` 376` ``` by (simp add: dist_norm norm_minus_commute) ``` eberlm@66277 ` 377` ``` also from 1 have "{..n} = {..m} \ {m<..n}" by auto ``` eberlm@66277 ` 378` ``` hence "norm (?P n - ?P m) = norm (?P m * (\k\{m<..n}. f (k + N)) - ?P m)" ``` eberlm@66277 ` 379` ``` by (subst prod.union_disjoint [symmetric]) (auto simp: algebra_simps) ``` eberlm@66277 ` 380` ``` also have "\ = norm (?P m * ((\k\{m<..n}. f (k + N)) - 1))" ``` eberlm@66277 ` 381` ``` by (simp add: algebra_simps) ``` eberlm@66277 ` 382` ``` also have "\ = (\k\m. norm (f (k + N))) * norm ((\k\{m<..n}. f (k + N)) - 1)" ``` eberlm@66277 ` 383` ``` by (simp add: norm_mult prod_norm) ``` eberlm@66277 ` 384` ``` also have "\ \ ?Q m * ((\k\{m<..n}. 1 + norm (f (k + N) - 1)) - 1)" ``` eberlm@66277 ` 385` ``` using norm_prod_minus1_le_prod_minus1[of "\k. f (k + N) - 1" "{m<..n}"] ``` eberlm@66277 ` 386` ``` norm_triangle_ineq[of 1 "f k - 1" for k] ``` eberlm@66277 ` 387` ``` by (intro mult_mono prod_mono ballI conjI norm_prod_minus1_le_prod_minus1 prod_nonneg) auto ``` eberlm@66277 ` 388` ``` also have "\ = ?Q m * (\k\{m<..n}. 1 + norm (f (k + N) - 1)) - ?Q m" ``` eberlm@66277 ` 389` ``` by (simp add: algebra_simps) ``` eberlm@66277 ` 390` ``` also have "?Q m * (\k\{m<..n}. 1 + norm (f (k + N) - 1)) = ``` eberlm@66277 ` 391` ``` (\k\{..m}\{m<..n}. 1 + norm (f (k + N) - 1))" ``` eberlm@66277 ` 392` ``` by (rule prod.union_disjoint [symmetric]) auto ``` eberlm@66277 ` 393` ``` also from 1 have "{..m}\{m<..n} = {..n}" by auto ``` eberlm@66277 ` 394` ``` also have "?Q n - ?Q m \ norm (?Q n - ?Q m)" by simp ``` eberlm@66277 ` 395` ``` also from 1 have "\ < \" by (intro M) auto ``` eberlm@66277 ` 396` ``` finally show ?case . ``` eberlm@66277 ` 397` ``` qed ``` eberlm@66277 ` 398` ``` qed ``` eberlm@66277 ` 399` ``` hence conv: "convergent ?P" by (rule Cauchy_convergent) ``` eberlm@66277 ` 400` ``` then obtain L where L: "?P \ L" ``` eberlm@66277 ` 401` ``` by (auto simp: convergent_def) ``` eberlm@66277 ` 402` eberlm@66277 ` 403` ``` have "L \ 0" ``` eberlm@66277 ` 404` ``` proof ``` eberlm@66277 ` 405` ``` assume [simp]: "L = 0" ``` eberlm@66277 ` 406` ``` from tendsto_norm[OF L] have limit: "(\n. \k\n. norm (f (k + N))) \ 0" ``` eberlm@66277 ` 407` ``` by (simp add: prod_norm) ``` eberlm@66277 ` 408` eberlm@66277 ` 409` ``` from assms have "(\n. f (n + N)) \ 1" ``` eberlm@66277 ` 410` ``` by (intro abs_convergent_prod_imp_LIMSEQ abs_convergent_prod_ignore_initial_segment) ``` eberlm@66277 ` 411` ``` hence "eventually (\n. norm (f (n + N) - 1) < 1) sequentially" ``` eberlm@66277 ` 412` ``` by (auto simp: tendsto_iff dist_norm) ``` eberlm@66277 ` 413` ``` then obtain M0 where M0: "norm (f (n + N) - 1) < 1" if "n \ M0" for n ``` eberlm@66277 ` 414` ``` by (auto simp: eventually_at_top_linorder) ``` eberlm@66277 ` 415` eberlm@66277 ` 416` ``` { ``` eberlm@66277 ` 417` ``` fix M assume M: "M \ M0" ``` eberlm@66277 ` 418` ``` with M0 have M: "norm (f (n + N) - 1) < 1" if "n \ M" for n using that by simp ``` eberlm@66277 ` 419` eberlm@66277 ` 420` ``` have "(\n. \k\n. 1 - norm (f (k+M+N) - 1)) \ 0" ``` eberlm@66277 ` 421` ``` proof (rule tendsto_sandwich) ``` eberlm@66277 ` 422` ``` show "eventually (\n. (\k\n. 1 - norm (f (k+M+N) - 1)) \ 0) sequentially" ``` eberlm@66277 ` 423` ``` using M by (intro always_eventually prod_nonneg allI ballI) (auto intro: less_imp_le) ``` eberlm@66277 ` 424` ``` have "norm (1::'a) - norm (f (i + M + N) - 1) \ norm (f (i + M + N))" for i ``` eberlm@66277 ` 425` ``` using norm_triangle_ineq3[of "f (i + M + N)" 1] by simp ``` eberlm@66277 ` 426` ``` thus "eventually (\n. (\k\n. 1 - norm (f (k+M+N) - 1)) \ (\k\n. norm (f (k+M+N)))) at_top" ``` eberlm@66277 ` 427` ``` using M by (intro always_eventually allI prod_mono ballI conjI) (auto intro: less_imp_le) ``` eberlm@66277 ` 428` ``` ``` eberlm@66277 ` 429` ``` define C where "C = (\k 0" by (auto simp: C_def) ``` eberlm@66277 ` 431` ``` from L have "(\n. norm (\k\n+M. f (k + N))) \ 0" ``` eberlm@66277 ` 432` ``` by (intro LIMSEQ_ignore_initial_segment) (simp add: tendsto_norm_zero_iff) ``` eberlm@66277 ` 433` ``` also have "(\n. norm (\k\n+M. f (k + N))) = (\n. C * (\k\n. norm (f (k + M + N))))" ``` eberlm@66277 ` 434` ``` proof (rule ext, goal_cases) ``` eberlm@66277 ` 435` ``` case (1 n) ``` eberlm@66277 ` 436` ``` have "{..n+M} = {.. {M..n+M}" by auto ``` eberlm@66277 ` 437` ``` also have "norm (\k\\. f (k + N)) = C * norm (\k=M..n+M. f (k + N))" ``` eberlm@66277 ` 438` ``` unfolding C_def by (subst prod.union_disjoint) (auto simp: norm_mult prod_norm) ``` eberlm@66277 ` 439` ``` also have "(\k=M..n+M. f (k + N)) = (\k\n. f (k + N + M))" ``` eberlm@66277 ` 440` ``` by (intro prod.reindex_bij_witness[of _ "\i. i + M" "\i. i - M"]) auto ``` eberlm@66277 ` 441` ``` finally show ?case by (simp add: add_ac prod_norm) ``` eberlm@66277 ` 442` ``` qed ``` eberlm@66277 ` 443` ``` finally have "(\n. C * (\k\n. norm (f (k + M + N))) / C) \ 0 / C" ``` eberlm@66277 ` 444` ``` by (intro tendsto_divide tendsto_const) auto ``` eberlm@66277 ` 445` ``` thus "(\n. \k\n. norm (f (k + M + N))) \ 0" by simp ``` eberlm@66277 ` 446` ``` qed simp_all ``` eberlm@66277 ` 447` eberlm@66277 ` 448` ``` have "1 - (\i. norm (f (i + M + N) - 1)) \ 0" ``` eberlm@66277 ` 449` ``` proof (rule tendsto_le) ``` eberlm@66277 ` 450` ``` show "eventually (\n. 1 - (\k\n. norm (f (k+M+N) - 1)) \ ``` eberlm@66277 ` 451` ``` (\k\n. 1 - norm (f (k+M+N) - 1))) at_top" ``` eberlm@66277 ` 452` ``` using M by (intro always_eventually allI weierstrass_prod_ineq) (auto intro: less_imp_le) ``` eberlm@66277 ` 453` ``` show "(\n. \k\n. 1 - norm (f (k+M+N) - 1)) \ 0" by fact ``` eberlm@66277 ` 454` ``` show "(\n. 1 - (\k\n. norm (f (k + M + N) - 1))) ``` eberlm@66277 ` 455` ``` \ 1 - (\i. norm (f (i + M + N) - 1))" ``` eberlm@66277 ` 456` ``` by (intro tendsto_intros summable_LIMSEQ' summable_ignore_initial_segment ``` eberlm@66277 ` 457` ``` abs_convergent_prod_imp_summable assms) ``` eberlm@66277 ` 458` ``` qed simp_all ``` eberlm@66277 ` 459` ``` hence "(\i. norm (f (i + M + N) - 1)) \ 1" by simp ``` eberlm@66277 ` 460` ``` also have "\ + (\ii. norm (f (i + N) - 1))" ``` eberlm@66277 ` 461` ``` by (intro suminf_split_initial_segment [symmetric] summable_ignore_initial_segment ``` eberlm@66277 ` 462` ``` abs_convergent_prod_imp_summable assms) ``` eberlm@66277 ` 463` ``` finally have "1 + (\i (\i. norm (f (i + N) - 1))" by simp ``` eberlm@66277 ` 464` ``` } note * = this ``` eberlm@66277 ` 465` eberlm@66277 ` 466` ``` have "1 + (\i. norm (f (i + N) - 1)) \ (\i. norm (f (i + N) - 1))" ``` eberlm@66277 ` 467` ``` proof (rule tendsto_le) ``` eberlm@66277 ` 468` ``` show "(\M. 1 + (\i 1 + (\i. norm (f (i + N) - 1))" ``` eberlm@66277 ` 469` ``` by (intro tendsto_intros summable_LIMSEQ summable_ignore_initial_segment ``` eberlm@66277 ` 470` ``` abs_convergent_prod_imp_summable assms) ``` eberlm@66277 ` 471` ``` show "eventually (\M. 1 + (\i (\i. norm (f (i + N) - 1))) at_top" ``` eberlm@66277 ` 472` ``` using eventually_ge_at_top[of M0] by eventually_elim (use * in auto) ``` eberlm@66277 ` 473` ``` qed simp_all ``` eberlm@66277 ` 474` ``` thus False by simp ``` eberlm@66277 ` 475` ``` qed ``` eberlm@66277 ` 476` ``` with L show ?thesis by (auto simp: convergent_prod_def) ``` eberlm@66277 ` 477` ```qed ``` eberlm@66277 ` 478` eberlm@66277 ` 479` ```end ```