src/HOL/Analysis/Infinite_Products.thy
 author paulson Wed May 02 12:47:56 2018 +0100 (14 months ago) changeset 68064 b249fab48c76 parent 66277 512b0dc09061 child 68071 c18af2b0f83e permissions -rw-r--r--
type class generalisations; some work on infinite products
 lp15@68064  1 (*File: HOL/Analysis/Infinite_Product.thy  lp15@68064  2  Author: Manuel Eberl & LC Paulson  eberlm@66277  3 eberlm@66277  4  Basic results about convergence and absolute convergence of infinite products  eberlm@66277  5  and their connection to summability.  eberlm@66277  6 *)  eberlm@66277  7 section \Infinite Products\  eberlm@66277  8 theory Infinite_Products  eberlm@66277  9  imports Complex_Main  eberlm@66277  10 begin  lp15@68064  11   eberlm@66277  12 lemma sum_le_prod:  eberlm@66277  13  fixes f :: "'a \ 'b :: linordered_semidom"  eberlm@66277  14  assumes "\x. x \ A \ f x \ 0"  eberlm@66277  15  shows "sum f A \ (\x\A. 1 + f x)"  eberlm@66277  16  using assms  eberlm@66277  17 proof (induction A rule: infinite_finite_induct)  eberlm@66277  18  case (insert x A)  eberlm@66277  19  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  20  by (intro add_mono insert mult_left_mono prod_mono) (auto intro: insert.prems)  eberlm@66277  21  with insert.hyps show ?case by (simp add: algebra_simps)  eberlm@66277  22 qed simp_all  eberlm@66277  23 eberlm@66277  24 lemma prod_le_exp_sum:  eberlm@66277  25  fixes f :: "'a \ real"  eberlm@66277  26  assumes "\x. x \ A \ f x \ 0"  eberlm@66277  27  shows "prod (\x. 1 + f x) A \ exp (sum f A)"  eberlm@66277  28  using assms  eberlm@66277  29 proof (induction A rule: infinite_finite_induct)  eberlm@66277  30  case (insert x A)  eberlm@66277  31  have "(1 + f x) * (\x\A. 1 + f x) \ exp (f x) * exp (sum f A)"  eberlm@66277  32  using insert.prems by (intro mult_mono insert prod_nonneg exp_ge_add_one_self) auto  eberlm@66277  33  with insert.hyps show ?case by (simp add: algebra_simps exp_add)  eberlm@66277  34 qed simp_all  eberlm@66277  35 eberlm@66277  36 lemma lim_ln_1_plus_x_over_x_at_0: "(\x::real. ln (1 + x) / x) \0\ 1"  eberlm@66277  37 proof (rule lhopital)  eberlm@66277  38  show "(\x::real. ln (1 + x)) \0\ 0"  eberlm@66277  39  by (rule tendsto_eq_intros refl | simp)+  eberlm@66277  40  have "eventually (\x::real. x \ {-1/2<..<1/2}) (nhds 0)"  eberlm@66277  41  by (rule eventually_nhds_in_open) auto  eberlm@66277  42  hence *: "eventually (\x::real. x \ {-1/2<..<1/2}) (at 0)"  eberlm@66277  43  by (rule filter_leD [rotated]) (simp_all add: at_within_def)  eberlm@66277  44  show "eventually (\x::real. ((\x. ln (1 + x)) has_field_derivative inverse (1 + x)) (at x)) (at 0)"  eberlm@66277  45  using * by eventually_elim (auto intro!: derivative_eq_intros simp: field_simps)  eberlm@66277  46  show "eventually (\x::real. ((\x. x) has_field_derivative 1) (at x)) (at 0)"  eberlm@66277  47  using * by eventually_elim (auto intro!: derivative_eq_intros simp: field_simps)  eberlm@66277  48  show "\\<^sub>F x in at 0. x \ 0" by (auto simp: at_within_def eventually_inf_principal)  eberlm@66277  49  show "(\x::real. inverse (1 + x) / 1) \0\ 1"  eberlm@66277  50  by (rule tendsto_eq_intros refl | simp)+  eberlm@66277  51 qed auto  eberlm@66277  52 lp15@68064  53 definition gen_has_prod :: "[nat \ 'a::{t2_space, comm_semiring_1}, nat, 'a] \ bool"  lp15@68064  54  where "gen_has_prod f M p \ (\n. \i\n. f (i+M)) \ p \ p \ 0"  lp15@68064  55 lp15@68064  56 text\The nonzero and zero cases, as in \emph{Complex Analysis} by Joseph Bak and Donald J.Newman, page 241\  lp15@68064  57 definition has_prod :: "(nat \ 'a::{t2_space, comm_semiring_1}) \ 'a \ bool" (infixr "has'_prod" 80)  lp15@68064  58  where "f has_prod p \ gen_has_prod f 0 p \ (\i q. p = 0 \ f i = 0 \ gen_has_prod f (Suc i) q)"  lp15@68064  59 eberlm@66277  60 definition convergent_prod :: "(nat \ 'a :: {t2_space,comm_semiring_1}) \ bool" where  lp15@68064  61  "convergent_prod f \ \M p. gen_has_prod f M p"  lp15@68064  62 lp15@68064  63 definition prodinf :: "(nat \ 'a::{t2_space, comm_semiring_1}) \ 'a"  lp15@68064  64  (binder "\" 10)  lp15@68064  65  where "prodinf f = (THE p. f has_prod p)"  lp15@68064  66 lp15@68064  67 lemmas prod_defs = gen_has_prod_def has_prod_def convergent_prod_def prodinf_def  lp15@68064  68 lp15@68064  69 lemma has_prod_subst[trans]: "f = g \ g has_prod z \ f has_prod z"  lp15@68064  70  by simp  lp15@68064  71 lp15@68064  72 lemma has_prod_cong: "(\n. f n = g n) \ f has_prod c \ g has_prod c"  lp15@68064  73  by presburger  eberlm@66277  74 eberlm@66277  75 lemma convergent_prod_altdef:  eberlm@66277  76  fixes f :: "nat \ 'a :: {t2_space,comm_semiring_1}"  eberlm@66277  77  shows "convergent_prod f \ (\M L. (\n\M. f n \ 0) \ (\n. \i\n. f (i+M)) \ L \ L \ 0)"  eberlm@66277  78 proof  eberlm@66277  79  assume "convergent_prod f"  eberlm@66277  80  then obtain M L where *: "(\n. \i\n. f (i+M)) \ L" "L \ 0"  lp15@68064  81  by (auto simp: prod_defs)  eberlm@66277  82  have "f i \ 0" if "i \ M" for i  eberlm@66277  83  proof  eberlm@66277  84  assume "f i = 0"  eberlm@66277  85  have **: "eventually (\n. (\i\n. f (i+M)) = 0) sequentially"  eberlm@66277  86  using eventually_ge_at_top[of "i - M"]  eberlm@66277  87  proof eventually_elim  eberlm@66277  88  case (elim n)  eberlm@66277  89  with \f i = 0\ and \i \ M\ show ?case  eberlm@66277  90  by (auto intro!: bexI[of _ "i - M"] prod_zero)  eberlm@66277  91  qed  eberlm@66277  92  have "(\n. (\i\n. f (i+M))) \ 0"  eberlm@66277  93  unfolding filterlim_iff  eberlm@66277  94  by (auto dest!: eventually_nhds_x_imp_x intro!: eventually_mono[OF **])  eberlm@66277  95  from tendsto_unique[OF _ this *(1)] and *(2)  eberlm@66277  96  show False by simp  eberlm@66277  97  qed  eberlm@66277  98  with * show "(\M L. (\n\M. f n \ 0) \ (\n. \i\n. f (i+M)) \ L \ L \ 0)"  eberlm@66277  99  by blast  lp15@68064  100 qed (auto simp: prod_defs)  eberlm@66277  101 eberlm@66277  102 definition abs_convergent_prod :: "(nat \ _) \ bool" where  eberlm@66277  103  "abs_convergent_prod f \ convergent_prod (\i. 1 + norm (f i - 1))"  eberlm@66277  104 eberlm@66277  105 lemma abs_convergent_prodI:  eberlm@66277  106  assumes "convergent (\n. \i\n. 1 + norm (f i - 1))"  eberlm@66277  107  shows "abs_convergent_prod f"  eberlm@66277  108 proof -  eberlm@66277  109  from assms obtain L where L: "(\n. \i\n. 1 + norm (f i - 1)) \ L"  eberlm@66277  110  by (auto simp: convergent_def)  eberlm@66277  111  have "L \ 1"  eberlm@66277  112  proof (rule tendsto_le)  eberlm@66277  113  show "eventually (\n. (\i\n. 1 + norm (f i - 1)) \ 1) sequentially"  eberlm@66277  114  proof (intro always_eventually allI)  eberlm@66277  115  fix n  eberlm@66277  116  have "(\i\n. 1 + norm (f i - 1)) \ (\i\n. 1)"  eberlm@66277  117  by (intro prod_mono) auto  eberlm@66277  118  thus "(\i\n. 1 + norm (f i - 1)) \ 1" by simp  eberlm@66277  119  qed  eberlm@66277  120  qed (use L in simp_all)  eberlm@66277  121  hence "L \ 0" by auto  lp15@68064  122  with L show ?thesis unfolding abs_convergent_prod_def prod_defs  eberlm@66277  123  by (intro exI[of _ "0::nat"] exI[of _ L]) auto  eberlm@66277  124 qed  eberlm@66277  125 eberlm@66277  126 lemma  lp15@68064  127  fixes f :: "nat \ 'a :: {topological_semigroup_mult,t2_space,idom}"  eberlm@66277  128  assumes "convergent_prod f"  eberlm@66277  129  shows convergent_prod_imp_convergent: "convergent (\n. \i\n. f i)"  eberlm@66277  130  and convergent_prod_to_zero_iff: "(\n. \i\n. f i) \ 0 \ (\i. f i = 0)"  eberlm@66277  131 proof -  eberlm@66277  132  from assms obtain M L  eberlm@66277  133  where M: "\n. n \ M \ f n \ 0" and "(\n. \i\n. f (i + M)) \ L" and "L \ 0"  eberlm@66277  134  by (auto simp: convergent_prod_altdef)  eberlm@66277  135  note this(2)  eberlm@66277  136  also have "(\n. \i\n. f (i + M)) = (\n. \i=M..M+n. f i)"  eberlm@66277  137  by (intro ext prod.reindex_bij_witness[of _ "\n. n - M" "\n. n + M"]) auto  eberlm@66277  138  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  141  by (subst prod.union_disjoint) auto  eberlm@66277  142  also have "(\n. {.. {M..M+n}) = (\n. {..n+M})" by auto  eberlm@66277  143  finally have lim: "(\n. prod f {..n}) \ prod f {..n. \i\n. f i)"  eberlm@66277  146  by (auto simp: convergent_def)  eberlm@66277  147 eberlm@66277  148  show "(\n. \i\n. f i) \ 0 \ (\i. f i = 0)"  eberlm@66277  149  proof  eberlm@66277  150  assume "\i. f i = 0"  eberlm@66277  151  then obtain i where "f i = 0" by auto  eberlm@66277  152  moreover with M have "i < M" by (cases "i < M") auto  eberlm@66277  153  ultimately have "(\in. \i\n. f i) \ 0" by simp  eberlm@66277  155  next  eberlm@66277  156  assume "(\n. \i\n. f i) \ 0"  eberlm@66277  157  from tendsto_unique[OF _ this lim] and \L \ 0\  eberlm@66277  158  show "\i. f i = 0" by auto  eberlm@66277  159  qed  eberlm@66277  160 qed  eberlm@66277  161 lp15@68064  162 lemma convergent_prod_iff_nz_lim:  lp15@68064  163  fixes f :: "nat \ 'a :: {topological_semigroup_mult,t2_space,idom}"  lp15@68064  164  assumes "\i. f i \ 0"  lp15@68064  165  shows "convergent_prod f \ (\L. (\n. \i\n. f i) \ L \ L \ 0)"  lp15@68064  166  (is "?lhs \ ?rhs")  lp15@68064  167 proof  lp15@68064  168  assume ?lhs then show ?rhs  lp15@68064  169  using assms convergentD convergent_prod_imp_convergent convergent_prod_to_zero_iff by blast  lp15@68064  170 next  lp15@68064  171  assume ?rhs then show ?lhs  lp15@68064  172  unfolding prod_defs  lp15@68064  173  by (rule_tac x="0" in exI) (auto simp: )  lp15@68064  174 qed  lp15@68064  175 lp15@68064  176 lemma convergent_prod_iff_convergent:  lp15@68064  177  fixes f :: "nat \ 'a :: {topological_semigroup_mult,t2_space,idom}"  lp15@68064  178  assumes "\i. f i \ 0"  lp15@68064  179  shows "convergent_prod f \ convergent (\n. \i\n. f i) \ lim (\n. \i\n. f i) \ 0"  lp15@68064  180  by (force simp add: convergent_prod_iff_nz_lim assms convergent_def limI)  lp15@68064  181 lp15@68064  182 eberlm@66277  183 lemma abs_convergent_prod_altdef:  lp15@68064  184  fixes f :: "nat \ 'a :: {one,real_normed_vector}"  lp15@68064  185  shows "abs_convergent_prod f \ convergent (\n. \i\n. 1 + norm (f i - 1))"  eberlm@66277  186 proof  eberlm@66277  187  assume "abs_convergent_prod f"  eberlm@66277  188  thus "convergent (\n. \i\n. 1 + norm (f i - 1))"  eberlm@66277  189  by (auto simp: abs_convergent_prod_def intro!: convergent_prod_imp_convergent)  eberlm@66277  190 qed (auto intro: abs_convergent_prodI)  eberlm@66277  191 eberlm@66277  192 lemma weierstrass_prod_ineq:  eberlm@66277  193  fixes f :: "'a \ real"  eberlm@66277  194  assumes "\x. x \ A \ f x \ {0..1}"  eberlm@66277  195  shows "1 - sum f A \ (\x\A. 1 - f x)"  eberlm@66277  196  using assms  eberlm@66277  197 proof (induction A rule: infinite_finite_induct)  eberlm@66277  198  case (insert x A)  eberlm@66277  199  from insert.hyps and insert.prems  eberlm@66277  200  have "1 - sum f A + f x * (\x\A. 1 - f x) \ (\x\A. 1 - f x) + f x * (\x\A. 1)"  eberlm@66277  201  by (intro insert.IH add_mono mult_left_mono prod_mono) auto  eberlm@66277  202  with insert.hyps show ?case by (simp add: algebra_simps)  eberlm@66277  203 qed simp_all  eberlm@66277  204 eberlm@66277  205 lemma norm_prod_minus1_le_prod_minus1:  eberlm@66277  206  fixes f :: "nat \ 'a :: {real_normed_div_algebra,comm_ring_1}"  eberlm@66277  207  shows "norm (prod (\n. 1 + f n) A - 1) \ prod (\n. 1 + norm (f n)) A - 1"  eberlm@66277  208 proof (induction A rule: infinite_finite_induct)  eberlm@66277  209  case (insert x A)  eberlm@66277  210  from insert.hyps have  eberlm@66277  211  "norm ((\n\insert x A. 1 + f n) - 1) =  eberlm@66277  212  norm ((\n\A. 1 + f n) - 1 + f x * (\n\A. 1 + f n))"  eberlm@66277  213  by (simp add: algebra_simps)  eberlm@66277  214  also have "\ \ norm ((\n\A. 1 + f n) - 1) + norm (f x * (\n\A. 1 + f n))"  eberlm@66277  215  by (rule norm_triangle_ineq)  eberlm@66277  216  also have "norm (f x * (\n\A. 1 + f n)) = norm (f x) * (\x\A. norm (1 + f x))"  eberlm@66277  217  by (simp add: prod_norm norm_mult)  eberlm@66277  218  also have "(\x\A. norm (1 + f x)) \ (\x\A. norm (1::'a) + norm (f x))"  eberlm@66277  219  by (intro prod_mono norm_triangle_ineq ballI conjI) auto  eberlm@66277  220  also have "norm (1::'a) = 1" by simp  eberlm@66277  221  also note insert.IH  eberlm@66277  222  also have "(\n\A. 1 + norm (f n)) - 1 + norm (f x) * (\x\A. 1 + norm (f x)) =  lp15@68064  223  (\n\insert x A. 1 + norm (f n)) - 1"  eberlm@66277  224  using insert.hyps by (simp add: algebra_simps)  eberlm@66277  225  finally show ?case by - (simp_all add: mult_left_mono)  eberlm@66277  226 qed simp_all  eberlm@66277  227 eberlm@66277  228 lemma convergent_prod_imp_ev_nonzero:  eberlm@66277  229  fixes f :: "nat \ 'a :: {t2_space,comm_semiring_1}"  eberlm@66277  230  assumes "convergent_prod f"  eberlm@66277  231  shows "eventually (\n. f n \ 0) sequentially"  eberlm@66277  232  using assms by (auto simp: eventually_at_top_linorder convergent_prod_altdef)  eberlm@66277  233 eberlm@66277  234 lemma convergent_prod_imp_LIMSEQ:  eberlm@66277  235  fixes f :: "nat \ 'a :: {real_normed_field}"  eberlm@66277  236  assumes "convergent_prod f"  eberlm@66277  237  shows "f \ 1"  eberlm@66277  238 proof -  eberlm@66277  239  from assms obtain M L where L: "(\n. \i\n. f (i+M)) \ L" "\n. n \ M \ f n \ 0" "L \ 0"  eberlm@66277  240  by (auto simp: convergent_prod_altdef)  eberlm@66277  241  hence L': "(\n. \i\Suc n. f (i+M)) \ L" by (subst filterlim_sequentially_Suc)  eberlm@66277  242  have "(\n. (\i\Suc n. f (i+M)) / (\i\n. f (i+M))) \ L / L"  eberlm@66277  243  using L L' by (intro tendsto_divide) simp_all  eberlm@66277  244  also from L have "L / L = 1" by simp  eberlm@66277  245  also have "(\n. (\i\Suc n. f (i+M)) / (\i\n. f (i+M))) = (\n. f (n + Suc M))"  eberlm@66277  246  using assms L by (auto simp: fun_eq_iff atMost_Suc)  eberlm@66277  247  finally show ?thesis by (rule LIMSEQ_offset)  eberlm@66277  248 qed  eberlm@66277  249 eberlm@66277  250 lemma abs_convergent_prod_imp_summable:  eberlm@66277  251  fixes f :: "nat \ 'a :: real_normed_div_algebra"  eberlm@66277  252  assumes "abs_convergent_prod f"  eberlm@66277  253  shows "summable (\i. norm (f i - 1))"  eberlm@66277  254 proof -  eberlm@66277  255  from assms have "convergent (\n. \i\n. 1 + norm (f i - 1))"  eberlm@66277  256  unfolding abs_convergent_prod_def by (rule convergent_prod_imp_convergent)  eberlm@66277  257  then obtain L where L: "(\n. \i\n. 1 + norm (f i - 1)) \ L"  eberlm@66277  258  unfolding convergent_def by blast  eberlm@66277  259  have "convergent (\n. \i\n. norm (f i - 1))"  eberlm@66277  260  proof (rule Bseq_monoseq_convergent)  eberlm@66277  261  have "eventually (\n. (\i\n. 1 + norm (f i - 1)) < L + 1) sequentially"  eberlm@66277  262  using L(1) by (rule order_tendstoD) simp_all  eberlm@66277  263  hence "\\<^sub>F x in sequentially. norm (\i\x. norm (f i - 1)) \ L + 1"  eberlm@66277  264  proof eventually_elim  eberlm@66277  265  case (elim n)  eberlm@66277  266  have "norm (\i\n. norm (f i - 1)) = (\i\n. norm (f i - 1))"  eberlm@66277  267  unfolding real_norm_def by (intro abs_of_nonneg sum_nonneg) simp_all  eberlm@66277  268  also have "\ \ (\i\n. 1 + norm (f i - 1))" by (rule sum_le_prod) auto  eberlm@66277  269  also have "\ < L + 1" by (rule elim)  eberlm@66277  270  finally show ?case by simp  eberlm@66277  271  qed  eberlm@66277  272  thus "Bseq (\n. \i\n. norm (f i - 1))" by (rule BfunI)  eberlm@66277  273  next  eberlm@66277  274  show "monoseq (\n. \i\n. norm (f i - 1))"  eberlm@66277  275  by (rule mono_SucI1) auto  eberlm@66277  276  qed  eberlm@66277  277  thus "summable (\i. norm (f i - 1))" by (simp add: summable_iff_convergent')  eberlm@66277  278 qed  eberlm@66277  279 eberlm@66277  280 lemma summable_imp_abs_convergent_prod:  eberlm@66277  281  fixes f :: "nat \ 'a :: real_normed_div_algebra"  eberlm@66277  282  assumes "summable (\i. norm (f i - 1))"  eberlm@66277  283  shows "abs_convergent_prod f"  eberlm@66277  284 proof (intro abs_convergent_prodI Bseq_monoseq_convergent)  eberlm@66277  285  show "monoseq (\n. \i\n. 1 + norm (f i - 1))"  eberlm@66277  286  by (intro mono_SucI1)  eberlm@66277  287  (auto simp: atMost_Suc algebra_simps intro!: mult_nonneg_nonneg prod_nonneg)  eberlm@66277  288 next  eberlm@66277  289  show "Bseq (\n. \i\n. 1 + norm (f i - 1))"  eberlm@66277  290  proof (rule Bseq_eventually_mono)  eberlm@66277  291  show "eventually (\n. norm (\i\n. 1 + norm (f i - 1)) \  eberlm@66277  292  norm (exp (\i\n. norm (f i - 1)))) sequentially"  eberlm@66277  293  by (intro always_eventually allI) (auto simp: abs_prod exp_sum intro!: prod_mono)  eberlm@66277  294  next  eberlm@66277  295  from assms have "(\n. \i\n. norm (f i - 1)) \ (\i. norm (f i - 1))"  eberlm@66277  296  using sums_def_le by blast  eberlm@66277  297  hence "(\n. exp (\i\n. norm (f i - 1))) \ exp (\i. norm (f i - 1))"  eberlm@66277  298  by (rule tendsto_exp)  eberlm@66277  299  hence "convergent (\n. exp (\i\n. norm (f i - 1)))"  eberlm@66277  300  by (rule convergentI)  eberlm@66277  301  thus "Bseq (\n. exp (\i\n. norm (f i - 1)))"  eberlm@66277  302  by (rule convergent_imp_Bseq)  eberlm@66277  303  qed  eberlm@66277  304 qed  eberlm@66277  305 eberlm@66277  306 lemma abs_convergent_prod_conv_summable:  eberlm@66277  307  fixes f :: "nat \ 'a :: real_normed_div_algebra"  eberlm@66277  308  shows "abs_convergent_prod f \ summable (\i. norm (f i - 1))"  eberlm@66277  309  by (blast intro: abs_convergent_prod_imp_summable summable_imp_abs_convergent_prod)  eberlm@66277  310 eberlm@66277  311 lemma abs_convergent_prod_imp_LIMSEQ:  eberlm@66277  312  fixes f :: "nat \ 'a :: {comm_ring_1,real_normed_div_algebra}"  eberlm@66277  313  assumes "abs_convergent_prod f"  eberlm@66277  314  shows "f \ 1"  eberlm@66277  315 proof -  eberlm@66277  316  from assms have "summable (\n. norm (f n - 1))"  eberlm@66277  317  by (rule abs_convergent_prod_imp_summable)  eberlm@66277  318  from summable_LIMSEQ_zero[OF this] have "(\n. f n - 1) \ 0"  eberlm@66277  319  by (simp add: tendsto_norm_zero_iff)  eberlm@66277  320  from tendsto_add[OF this tendsto_const[of 1]] show ?thesis by simp  eberlm@66277  321 qed  eberlm@66277  322 eberlm@66277  323 lemma abs_convergent_prod_imp_ev_nonzero:  eberlm@66277  324  fixes f :: "nat \ 'a :: {comm_ring_1,real_normed_div_algebra}"  eberlm@66277  325  assumes "abs_convergent_prod f"  eberlm@66277  326  shows "eventually (\n. f n \ 0) sequentially"  eberlm@66277  327 proof -  eberlm@66277  328  from assms have "f \ 1"  eberlm@66277  329  by (rule abs_convergent_prod_imp_LIMSEQ)  eberlm@66277  330  hence "eventually (\n. dist (f n) 1 < 1) at_top"  eberlm@66277  331  by (auto simp: tendsto_iff)  eberlm@66277  332  thus ?thesis by eventually_elim auto  eberlm@66277  333 qed  eberlm@66277  334 eberlm@66277  335 lemma convergent_prod_offset:  eberlm@66277  336  assumes "convergent_prod (\n. f (n + m))"  eberlm@66277  337  shows "convergent_prod f"  eberlm@66277  338 proof -  eberlm@66277  339  from assms obtain M L where "(\n. \k\n. f (k + (M + m))) \ L" "L \ 0"  lp15@68064  340  by (auto simp: prod_defs add.assoc)  lp15@68064  341  thus "convergent_prod f"  lp15@68064  342  unfolding prod_defs by blast  eberlm@66277  343 qed  eberlm@66277  344 eberlm@66277  345 lemma abs_convergent_prod_offset:  eberlm@66277  346  assumes "abs_convergent_prod (\n. f (n + m))"  eberlm@66277  347  shows "abs_convergent_prod f"  eberlm@66277  348  using assms unfolding abs_convergent_prod_def by (rule convergent_prod_offset)  eberlm@66277  349 eberlm@66277  350 lemma convergent_prod_ignore_initial_segment:  eberlm@66277  351  fixes f :: "nat \ 'a :: {real_normed_field}"  eberlm@66277  352  assumes "convergent_prod f"  eberlm@66277  353  shows "convergent_prod (\n. f (n + m))"  eberlm@66277  354 proof -  eberlm@66277  355  from assms obtain M L  eberlm@66277  356  where L: "(\n. \k\n. f (k + M)) \ L" "L \ 0" and nz: "\n. n \ M \ f n \ 0"  eberlm@66277  357  by (auto simp: convergent_prod_altdef)  eberlm@66277  358  define C where "C = (\k 0"  eberlm@66277  360  by (auto simp: C_def)  eberlm@66277  361 eberlm@66277  362  from L(1) have "(\n. \k\n+m. f (k + M)) \ L"  eberlm@66277  363  by (rule LIMSEQ_ignore_initial_segment)  eberlm@66277  364  also have "(\n. \k\n+m. f (k + M)) = (\n. C * (\k\n. f (k + M + m)))"  eberlm@66277  365  proof (rule ext, goal_cases)  eberlm@66277  366  case (1 n)  eberlm@66277  367  have "{..n+m} = {.. {m..n+m}" by auto  eberlm@66277  368  also have "(\k\\. f (k + M)) = C * (\k=m..n+m. f (k + M))"  eberlm@66277  369  unfolding C_def by (rule prod.union_disjoint) auto  eberlm@66277  370  also have "(\k=m..n+m. f (k + M)) = (\k\n. f (k + m + M))"  eberlm@66277  371  by (intro ext prod.reindex_bij_witness[of _ "\k. k + m" "\k. k - m"]) auto  eberlm@66277  372  finally show ?case by (simp add: add_ac)  eberlm@66277  373  qed  eberlm@66277  374  finally have "(\n. C * (\k\n. f (k + M + m)) / C) \ L / C"  eberlm@66277  375  by (intro tendsto_divide tendsto_const) auto  eberlm@66277  376  hence "(\n. \k\n. f (k + M + m)) \ L / C" by simp  eberlm@66277  377  moreover from \L \ 0\ have "L / C \ 0" by simp  lp15@68064  378  ultimately show ?thesis  lp15@68064  379  unfolding prod_defs by blast  eberlm@66277  380 qed  eberlm@66277  381 eberlm@66277  382 lemma abs_convergent_prod_ignore_initial_segment:  eberlm@66277  383  assumes "abs_convergent_prod f"  eberlm@66277  384  shows "abs_convergent_prod (\n. f (n + m))"  eberlm@66277  385  using assms unfolding abs_convergent_prod_def  eberlm@66277  386  by (rule convergent_prod_ignore_initial_segment)  eberlm@66277  387 eberlm@66277  388 lemma abs_convergent_prod_imp_convergent_prod:  eberlm@66277  389  fixes f :: "nat \ 'a :: {real_normed_div_algebra,complete_space,comm_ring_1}"  eberlm@66277  390  assumes "abs_convergent_prod f"  eberlm@66277  391  shows "convergent_prod f"  eberlm@66277  392 proof -  eberlm@66277  393  from assms have "eventually (\n. f n \ 0) sequentially"  eberlm@66277  394  by (rule abs_convergent_prod_imp_ev_nonzero)  eberlm@66277  395  then obtain N where N: "f n \ 0" if "n \ N" for n  eberlm@66277  396  by (auto simp: eventually_at_top_linorder)  eberlm@66277  397  let ?P = "\n. \i\n. f (i + N)" and ?Q = "\n. \i\n. 1 + norm (f (i + N) - 1)"  eberlm@66277  398 eberlm@66277  399  have "Cauchy ?P"  eberlm@66277  400  proof (rule CauchyI', goal_cases)  eberlm@66277  401  case (1 \)  eberlm@66277  402  from assms have "abs_convergent_prod (\n. f (n + N))"  eberlm@66277  403  by (rule abs_convergent_prod_ignore_initial_segment)  eberlm@66277  404  hence "Cauchy ?Q"  eberlm@66277  405  unfolding abs_convergent_prod_def  eberlm@66277  406  by (intro convergent_Cauchy convergent_prod_imp_convergent)  eberlm@66277  407  from CauchyD[OF this 1] obtain M where M: "norm (?Q m - ?Q n) < \" if "m \ M" "n \ M" for m n  eberlm@66277  408  by blast  eberlm@66277  409  show ?case  eberlm@66277  410  proof (rule exI[of _ M], safe, goal_cases)  eberlm@66277  411  case (1 m n)  eberlm@66277  412  have "dist (?P m) (?P n) = norm (?P n - ?P m)"  eberlm@66277  413  by (simp add: dist_norm norm_minus_commute)  eberlm@66277  414  also from 1 have "{..n} = {..m} \ {m<..n}" by auto  eberlm@66277  415  hence "norm (?P n - ?P m) = norm (?P m * (\k\{m<..n}. f (k + N)) - ?P m)"  eberlm@66277  416  by (subst prod.union_disjoint [symmetric]) (auto simp: algebra_simps)  eberlm@66277  417  also have "\ = norm (?P m * ((\k\{m<..n}. f (k + N)) - 1))"  eberlm@66277  418  by (simp add: algebra_simps)  eberlm@66277  419  also have "\ = (\k\m. norm (f (k + N))) * norm ((\k\{m<..n}. f (k + N)) - 1)"  eberlm@66277  420  by (simp add: norm_mult prod_norm)  eberlm@66277  421  also have "\ \ ?Q m * ((\k\{m<..n}. 1 + norm (f (k + N) - 1)) - 1)"  eberlm@66277  422  using norm_prod_minus1_le_prod_minus1[of "\k. f (k + N) - 1" "{m<..n}"]  eberlm@66277  423  norm_triangle_ineq[of 1 "f k - 1" for k]  eberlm@66277  424  by (intro mult_mono prod_mono ballI conjI norm_prod_minus1_le_prod_minus1 prod_nonneg) auto  eberlm@66277  425  also have "\ = ?Q m * (\k\{m<..n}. 1 + norm (f (k + N) - 1)) - ?Q m"  eberlm@66277  426  by (simp add: algebra_simps)  eberlm@66277  427  also have "?Q m * (\k\{m<..n}. 1 + norm (f (k + N) - 1)) =  eberlm@66277  428  (\k\{..m}\{m<..n}. 1 + norm (f (k + N) - 1))"  eberlm@66277  429  by (rule prod.union_disjoint [symmetric]) auto  eberlm@66277  430  also from 1 have "{..m}\{m<..n} = {..n}" by auto  eberlm@66277  431  also have "?Q n - ?Q m \ norm (?Q n - ?Q m)" by simp  eberlm@66277  432  also from 1 have "\ < \" by (intro M) auto  eberlm@66277  433  finally show ?case .  eberlm@66277  434  qed  eberlm@66277  435  qed  eberlm@66277  436  hence conv: "convergent ?P" by (rule Cauchy_convergent)  eberlm@66277  437  then obtain L where L: "?P \ L"  eberlm@66277  438  by (auto simp: convergent_def)  eberlm@66277  439 eberlm@66277  440  have "L \ 0"  eberlm@66277  441  proof  eberlm@66277  442  assume [simp]: "L = 0"  eberlm@66277  443  from tendsto_norm[OF L] have limit: "(\n. \k\n. norm (f (k + N))) \ 0"  eberlm@66277  444  by (simp add: prod_norm)  eberlm@66277  445 eberlm@66277  446  from assms have "(\n. f (n + N)) \ 1"  eberlm@66277  447  by (intro abs_convergent_prod_imp_LIMSEQ abs_convergent_prod_ignore_initial_segment)  eberlm@66277  448  hence "eventually (\n. norm (f (n + N) - 1) < 1) sequentially"  eberlm@66277  449  by (auto simp: tendsto_iff dist_norm)  eberlm@66277  450  then obtain M0 where M0: "norm (f (n + N) - 1) < 1" if "n \ M0" for n  eberlm@66277  451  by (auto simp: eventually_at_top_linorder)  eberlm@66277  452 eberlm@66277  453  {  eberlm@66277  454  fix M assume M: "M \ M0"  eberlm@66277  455  with M0 have M: "norm (f (n + N) - 1) < 1" if "n \ M" for n using that by simp  eberlm@66277  456 eberlm@66277  457  have "(\n. \k\n. 1 - norm (f (k+M+N) - 1)) \ 0"  eberlm@66277  458  proof (rule tendsto_sandwich)  eberlm@66277  459  show "eventually (\n. (\k\n. 1 - norm (f (k+M+N) - 1)) \ 0) sequentially"  eberlm@66277  460  using M by (intro always_eventually prod_nonneg allI ballI) (auto intro: less_imp_le)  eberlm@66277  461  have "norm (1::'a) - norm (f (i + M + N) - 1) \ norm (f (i + M + N))" for i  eberlm@66277  462  using norm_triangle_ineq3[of "f (i + M + N)" 1] by simp  eberlm@66277  463  thus "eventually (\n. (\k\n. 1 - norm (f (k+M+N) - 1)) \ (\k\n. norm (f (k+M+N)))) at_top"  eberlm@66277  464  using M by (intro always_eventually allI prod_mono ballI conjI) (auto intro: less_imp_le)  eberlm@66277  465   eberlm@66277  466  define C where "C = (\k 0" by (auto simp: C_def)  eberlm@66277  468  from L have "(\n. norm (\k\n+M. f (k + N))) \ 0"  eberlm@66277  469  by (intro LIMSEQ_ignore_initial_segment) (simp add: tendsto_norm_zero_iff)  eberlm@66277  470  also have "(\n. norm (\k\n+M. f (k + N))) = (\n. C * (\k\n. norm (f (k + M + N))))"  eberlm@66277  471  proof (rule ext, goal_cases)  eberlm@66277  472  case (1 n)  eberlm@66277  473  have "{..n+M} = {.. {M..n+M}" by auto  eberlm@66277  474  also have "norm (\k\\. f (k + N)) = C * norm (\k=M..n+M. f (k + N))"  eberlm@66277  475  unfolding C_def by (subst prod.union_disjoint) (auto simp: norm_mult prod_norm)  eberlm@66277  476  also have "(\k=M..n+M. f (k + N)) = (\k\n. f (k + N + M))"  eberlm@66277  477  by (intro prod.reindex_bij_witness[of _ "\i. i + M" "\i. i - M"]) auto  eberlm@66277  478  finally show ?case by (simp add: add_ac prod_norm)  eberlm@66277  479  qed  eberlm@66277  480  finally have "(\n. C * (\k\n. norm (f (k + M + N))) / C) \ 0 / C"  eberlm@66277  481  by (intro tendsto_divide tendsto_const) auto  eberlm@66277  482  thus "(\n. \k\n. norm (f (k + M + N))) \ 0" by simp  eberlm@66277  483  qed simp_all  eberlm@66277  484 eberlm@66277  485  have "1 - (\i. norm (f (i + M + N) - 1)) \ 0"  eberlm@66277  486  proof (rule tendsto_le)  eberlm@66277  487  show "eventually (\n. 1 - (\k\n. norm (f (k+M+N) - 1)) \  eberlm@66277  488  (\k\n. 1 - norm (f (k+M+N) - 1))) at_top"  eberlm@66277  489  using M by (intro always_eventually allI weierstrass_prod_ineq) (auto intro: less_imp_le)  eberlm@66277  490  show "(\n. \k\n. 1 - norm (f (k+M+N) - 1)) \ 0" by fact  eberlm@66277  491  show "(\n. 1 - (\k\n. norm (f (k + M + N) - 1)))  eberlm@66277  492  \ 1 - (\i. norm (f (i + M + N) - 1))"  eberlm@66277  493  by (intro tendsto_intros summable_LIMSEQ' summable_ignore_initial_segment  eberlm@66277  494  abs_convergent_prod_imp_summable assms)  eberlm@66277  495  qed simp_all  eberlm@66277  496  hence "(\i. norm (f (i + M + N) - 1)) \ 1" by simp  eberlm@66277  497  also have "\ + (\ii. norm (f (i + N) - 1))"  eberlm@66277  498  by (intro suminf_split_initial_segment [symmetric] summable_ignore_initial_segment  eberlm@66277  499  abs_convergent_prod_imp_summable assms)  eberlm@66277  500  finally have "1 + (\i (\i. norm (f (i + N) - 1))" by simp  eberlm@66277  501  } note * = this  eberlm@66277  502 eberlm@66277  503  have "1 + (\i. norm (f (i + N) - 1)) \ (\i. norm (f (i + N) - 1))"  eberlm@66277  504  proof (rule tendsto_le)  eberlm@66277  505  show "(\M. 1 + (\i 1 + (\i. norm (f (i + N) - 1))"  eberlm@66277  506  by (intro tendsto_intros summable_LIMSEQ summable_ignore_initial_segment  eberlm@66277  507  abs_convergent_prod_imp_summable assms)  eberlm@66277  508  show "eventually (\M. 1 + (\i (\i. norm (f (i + N) - 1))) at_top"  eberlm@66277  509  using eventually_ge_at_top[of M0] by eventually_elim (use * in auto)  eberlm@66277  510  qed simp_all  eberlm@66277  511  thus False by simp  eberlm@66277  512  qed  lp15@68064  513  with L show ?thesis by (auto simp: prod_defs)  lp15@68064  514 qed  lp15@68064  515 lp15@68064  516 lemma convergent_prod_offset_0:  lp15@68064  517  fixes f :: "nat \ 'a :: {idom,topological_semigroup_mult,t2_space}"  lp15@68064  518  assumes "convergent_prod f" "\i. f i \ 0"  lp15@68064  519  shows "\p. gen_has_prod f 0 p"  lp15@68064  520  using assms  lp15@68064  521  unfolding convergent_prod_def  lp15@68064  522 proof (clarsimp simp: prod_defs)  lp15@68064  523  fix M p  lp15@68064  524  assume "(\n. \i\n. f (i + M)) \ p" "p \ 0"  lp15@68064  525  then have "(\n. prod f {..i\n. f (i + M))) \ prod f {..i\n. f (i + M)) = prod f {..n+M}" for n  lp15@68064  528  proof -  lp15@68064  529  have "{..n+M} = {.. {M..n+M}"  lp15@68064  530  by auto  lp15@68064  531  then have "prod f {..n+M} = prod f {..i\n. f (i + M))"  lp15@68064  534  by (metis (mono_tags, lifting) add.left_neutral atMost_atLeast0 prod_shift_bounds_cl_nat_ivl)  lp15@68064  535  finally show ?thesis by metis  lp15@68064  536  qed  lp15@68064  537  ultimately have "(\n. prod f {..n}) \ prod f {..p. (\n. prod f {..n}) \ p \ p \ 0"  lp15@68064  540  using \p \ 0\ assms  lp15@68064  541  by (rule_tac x="prod f {.. 'a :: {idom,topological_semigroup_mult,t2_space}"  lp15@68064  546  assumes "convergent_prod f" "\i. f i \ 0"  lp15@68064  547  shows "prodinf f = lim (\n. \i\n. f i)"  lp15@68064  548  using assms convergent_prod_offset_0 [OF assms]  lp15@68064  549  by (simp add: prod_defs lim_def) (metis (no_types) assms(1) convergent_prod_to_zero_iff)  lp15@68064  550 lp15@68064  551 lemma has_prod_one[simp, intro]: "(\n. 1) has_prod 1"  lp15@68064  552  unfolding prod_defs by auto  lp15@68064  553 lp15@68064  554 lemma convergent_prod_one[simp, intro]: "convergent_prod (\n. 1)"  lp15@68064  555  unfolding prod_defs by auto  lp15@68064  556 lp15@68064  557 lemma prodinf_cong: "(\n. f n = g n) \ prodinf f = prodinf g"  lp15@68064  558  by presburger  lp15@68064  559 lp15@68064  560 lemma convergent_prod_cong:  lp15@68064  561  fixes f g :: "nat \ 'a::{field,topological_semigroup_mult,t2_space}"  lp15@68064  562  assumes ev: "eventually (\x. f x = g x) sequentially" and f: "\i. f i \ 0" and g: "\i. g i \ 0"  lp15@68064  563  shows "convergent_prod f = convergent_prod g"  lp15@68064  564 proof -  lp15@68064  565  from assms obtain N where N: "\n\N. f n = g n"  lp15@68064  566  by (auto simp: eventually_at_top_linorder)  lp15@68064  567  define C where "C = (\k 0"  lp15@68064  569  by (simp add: f)  lp15@68064  570  have *: "eventually (\n. prod f {..n} = C * prod g {..n}) sequentially"  lp15@68064  571  using eventually_ge_at_top[of N]  lp15@68064  572  proof eventually_elim  lp15@68064  573  case (elim n)  lp15@68064  574  then have "{..n} = {.. {N..n}"  lp15@68064  575  by auto  lp15@68064  576  also have "prod f ... = prod f {.. {N..n})"  lp15@68064  583  by (intro prod.union_disjoint [symmetric]) auto  lp15@68064  584  also from elim have "{.. {N..n} = {..n}"  lp15@68064  585  by auto  lp15@68064  586  finally show "prod f {..n} = C * prod g {..n}" .  lp15@68064  587  qed  lp15@68064  588  then have cong: "convergent (\n. prod f {..n}) = convergent (\n. C * prod g {..n})"  lp15@68064  589  by (rule convergent_cong)  lp15@68064  590  show ?thesis  lp15@68064  591  proof  lp15@68064  592  assume cf: "convergent_prod f"  lp15@68064  593  then have "\ (\n. prod g {..n}) \ 0"  lp15@68064  594  using tendsto_mult_left * convergent_prod_to_zero_iff f filterlim_cong by fastforce  lp15@68064  595  then show "convergent_prod g"  lp15@68064  596  by (metis convergent_mult_const_iff \C \ 0\ cong cf convergent_LIMSEQ_iff convergent_prod_iff_convergent convergent_prod_imp_convergent g)  lp15@68064  597  next  lp15@68064  598  assume cg: "convergent_prod g"  lp15@68064  599  have "\a. C * a \ 0 \ (\n. prod g {..n}) \ a"  lp15@68064  600  by (metis (no_types) \C \ 0\ cg convergent_prod_iff_nz_lim divide_eq_0_iff g nonzero_mult_div_cancel_right)  lp15@68064  601  then show "convergent_prod f"  lp15@68064  602  using "*" tendsto_mult_left filterlim_cong  lp15@68064  603  by (fastforce simp add: convergent_prod_iff_nz_lim f)  lp15@68064  604  qed  eberlm@66277  605 qed  eberlm@66277  606 eberlm@66277  607 end