src/HOL/Analysis/Infinite_Products.thy
 author paulson Thu May 10 15:41:34 2018 +0100 (14 months ago) changeset 68136 f022083489d0 parent 68127 137d5d0112bb child 68138 c738f40e88d4 permissions -rw-r--r--
more 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 lp15@68071  75 lemma gen_has_prod_nonzero [simp]: "\ gen_has_prod f M 0"  lp15@68071  76  by (simp add: gen_has_prod_def)  lp15@68071  77 lp15@68136  78 lemma gen_has_prod_eq_0:  lp15@68136  79  fixes f :: "nat \ 'a::{idom,t2_space}"  lp15@68136  80  assumes p: "gen_has_prod f m p" and i: "f i = 0" "i \ m"  lp15@68136  81  shows "p = 0"  lp15@68136  82 proof -  lp15@68136  83  have eq0: "(\k\n. f (k+m)) = 0" if "i - m \ n" for n  lp15@68136  84  by (metis i that atMost_atLeast0 atMost_iff diff_add finite_atLeastAtMost prod_zero_iff)  lp15@68136  85  have "(\n. \i\n. f (i + m)) \ 0"  lp15@68136  86  by (rule LIMSEQ_offset [where k = "i-m"]) (simp add: eq0)  lp15@68136  87  with p show ?thesis  lp15@68136  88  unfolding gen_has_prod_def  lp15@68136  89  using LIMSEQ_unique by blast  lp15@68136  90 qed  lp15@68136  91 lp15@68071  92 lemma has_prod_0_iff: "f has_prod 0 \ (\i. f i = 0 \ (\p. gen_has_prod f (Suc i) p))"  lp15@68071  93  by (simp add: has_prod_def)  lp15@68136  94   lp15@68136  95 lemma has_prod_unique2:  lp15@68136  96  fixes f :: "nat \ 'a::{idom,t2_space}"  lp15@68136  97  assumes "f has_prod a" "f has_prod b" shows "a = b"  lp15@68136  98  using assms  lp15@68136  99  by (auto simp: has_prod_def gen_has_prod_eq_0) (meson gen_has_prod_def sequentially_bot tendsto_unique)  lp15@68136  100 lp15@68136  101 lemma has_prod_unique:  lp15@68136  102  fixes f :: "nat \ 'a :: {idom,t2_space}"  lp15@68136  103  shows "f has_prod s \ s = prodinf f"  lp15@68136  104  by (simp add: has_prod_unique2 prodinf_def the_equality)  lp15@68071  105 eberlm@66277  106 lemma convergent_prod_altdef:  eberlm@66277  107  fixes f :: "nat \ 'a :: {t2_space,comm_semiring_1}"  eberlm@66277  108  shows "convergent_prod f \ (\M L. (\n\M. f n \ 0) \ (\n. \i\n. f (i+M)) \ L \ L \ 0)"  eberlm@66277  109 proof  eberlm@66277  110  assume "convergent_prod f"  eberlm@66277  111  then obtain M L where *: "(\n. \i\n. f (i+M)) \ L" "L \ 0"  lp15@68064  112  by (auto simp: prod_defs)  eberlm@66277  113  have "f i \ 0" if "i \ M" for i  eberlm@66277  114  proof  eberlm@66277  115  assume "f i = 0"  eberlm@66277  116  have **: "eventually (\n. (\i\n. f (i+M)) = 0) sequentially"  eberlm@66277  117  using eventually_ge_at_top[of "i - M"]  eberlm@66277  118  proof eventually_elim  eberlm@66277  119  case (elim n)  eberlm@66277  120  with \f i = 0\ and \i \ M\ show ?case  eberlm@66277  121  by (auto intro!: bexI[of _ "i - M"] prod_zero)  eberlm@66277  122  qed  eberlm@66277  123  have "(\n. (\i\n. f (i+M))) \ 0"  eberlm@66277  124  unfolding filterlim_iff  eberlm@66277  125  by (auto dest!: eventually_nhds_x_imp_x intro!: eventually_mono[OF **])  eberlm@66277  126  from tendsto_unique[OF _ this *(1)] and *(2)  eberlm@66277  127  show False by simp  eberlm@66277  128  qed  eberlm@66277  129  with * show "(\M L. (\n\M. f n \ 0) \ (\n. \i\n. f (i+M)) \ L \ L \ 0)"  eberlm@66277  130  by blast  lp15@68064  131 qed (auto simp: prod_defs)  eberlm@66277  132 eberlm@66277  133 definition abs_convergent_prod :: "(nat \ _) \ bool" where  eberlm@66277  134  "abs_convergent_prod f \ convergent_prod (\i. 1 + norm (f i - 1))"  eberlm@66277  135 eberlm@66277  136 lemma abs_convergent_prodI:  eberlm@66277  137  assumes "convergent (\n. \i\n. 1 + norm (f i - 1))"  eberlm@66277  138  shows "abs_convergent_prod f"  eberlm@66277  139 proof -  eberlm@66277  140  from assms obtain L where L: "(\n. \i\n. 1 + norm (f i - 1)) \ L"  eberlm@66277  141  by (auto simp: convergent_def)  eberlm@66277  142  have "L \ 1"  eberlm@66277  143  proof (rule tendsto_le)  eberlm@66277  144  show "eventually (\n. (\i\n. 1 + norm (f i - 1)) \ 1) sequentially"  eberlm@66277  145  proof (intro always_eventually allI)  eberlm@66277  146  fix n  eberlm@66277  147  have "(\i\n. 1 + norm (f i - 1)) \ (\i\n. 1)"  eberlm@66277  148  by (intro prod_mono) auto  eberlm@66277  149  thus "(\i\n. 1 + norm (f i - 1)) \ 1" by simp  eberlm@66277  150  qed  eberlm@66277  151  qed (use L in simp_all)  eberlm@66277  152  hence "L \ 0" by auto  lp15@68064  153  with L show ?thesis unfolding abs_convergent_prod_def prod_defs  eberlm@66277  154  by (intro exI[of _ "0::nat"] exI[of _ L]) auto  eberlm@66277  155 qed  eberlm@66277  156 eberlm@66277  157 lemma  lp15@68064  158  fixes f :: "nat \ 'a :: {topological_semigroup_mult,t2_space,idom}"  eberlm@66277  159  assumes "convergent_prod f"  eberlm@66277  160  shows convergent_prod_imp_convergent: "convergent (\n. \i\n. f i)"  eberlm@66277  161  and convergent_prod_to_zero_iff: "(\n. \i\n. f i) \ 0 \ (\i. f i = 0)"  eberlm@66277  162 proof -  eberlm@66277  163  from assms obtain M L  eberlm@66277  164  where M: "\n. n \ M \ f n \ 0" and "(\n. \i\n. f (i + M)) \ L" and "L \ 0"  eberlm@66277  165  by (auto simp: convergent_prod_altdef)  eberlm@66277  166  note this(2)  eberlm@66277  167  also have "(\n. \i\n. f (i + M)) = (\n. \i=M..M+n. f i)"  eberlm@66277  168  by (intro ext prod.reindex_bij_witness[of _ "\n. n - M" "\n. n + M"]) auto  eberlm@66277  169  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  172  by (subst prod.union_disjoint) auto  eberlm@66277  173  also have "(\n. {.. {M..M+n}) = (\n. {..n+M})" by auto  eberlm@66277  174  finally have lim: "(\n. prod f {..n}) \ prod f {..n. \i\n. f i)"  eberlm@66277  177  by (auto simp: convergent_def)  eberlm@66277  178 eberlm@66277  179  show "(\n. \i\n. f i) \ 0 \ (\i. f i = 0)"  eberlm@66277  180  proof  eberlm@66277  181  assume "\i. f i = 0"  eberlm@66277  182  then obtain i where "f i = 0" by auto  eberlm@66277  183  moreover with M have "i < M" by (cases "i < M") auto  eberlm@66277  184  ultimately have "(\in. \i\n. f i) \ 0" by simp  eberlm@66277  186  next  eberlm@66277  187  assume "(\n. \i\n. f i) \ 0"  eberlm@66277  188  from tendsto_unique[OF _ this lim] and \L \ 0\  eberlm@66277  189  show "\i. f i = 0" by auto  eberlm@66277  190  qed  eberlm@66277  191 qed  eberlm@66277  192 lp15@68064  193 lemma convergent_prod_iff_nz_lim:  lp15@68064  194  fixes f :: "nat \ 'a :: {topological_semigroup_mult,t2_space,idom}"  lp15@68064  195  assumes "\i. f i \ 0"  lp15@68064  196  shows "convergent_prod f \ (\L. (\n. \i\n. f i) \ L \ L \ 0)"  lp15@68064  197  (is "?lhs \ ?rhs")  lp15@68064  198 proof  lp15@68064  199  assume ?lhs then show ?rhs  lp15@68064  200  using assms convergentD convergent_prod_imp_convergent convergent_prod_to_zero_iff by blast  lp15@68064  201 next  lp15@68064  202  assume ?rhs then show ?lhs  lp15@68064  203  unfolding prod_defs  lp15@68064  204  by (rule_tac x="0" in exI) (auto simp: )  lp15@68064  205 qed  lp15@68064  206 lp15@68064  207 lemma convergent_prod_iff_convergent:  lp15@68064  208  fixes f :: "nat \ 'a :: {topological_semigroup_mult,t2_space,idom}"  lp15@68064  209  assumes "\i. f i \ 0"  lp15@68064  210  shows "convergent_prod f \ convergent (\n. \i\n. f i) \ lim (\n. \i\n. f i) \ 0"  lp15@68064  211  by (force simp add: convergent_prod_iff_nz_lim assms convergent_def limI)  lp15@68064  212 lp15@68064  213 eberlm@66277  214 lemma abs_convergent_prod_altdef:  lp15@68064  215  fixes f :: "nat \ 'a :: {one,real_normed_vector}"  lp15@68064  216  shows "abs_convergent_prod f \ convergent (\n. \i\n. 1 + norm (f i - 1))"  eberlm@66277  217 proof  eberlm@66277  218  assume "abs_convergent_prod f"  eberlm@66277  219  thus "convergent (\n. \i\n. 1 + norm (f i - 1))"  eberlm@66277  220  by (auto simp: abs_convergent_prod_def intro!: convergent_prod_imp_convergent)  eberlm@66277  221 qed (auto intro: abs_convergent_prodI)  eberlm@66277  222 eberlm@66277  223 lemma weierstrass_prod_ineq:  eberlm@66277  224  fixes f :: "'a \ real"  eberlm@66277  225  assumes "\x. x \ A \ f x \ {0..1}"  eberlm@66277  226  shows "1 - sum f A \ (\x\A. 1 - f x)"  eberlm@66277  227  using assms  eberlm@66277  228 proof (induction A rule: infinite_finite_induct)  eberlm@66277  229  case (insert x A)  eberlm@66277  230  from insert.hyps and insert.prems  eberlm@66277  231  have "1 - sum f A + f x * (\x\A. 1 - f x) \ (\x\A. 1 - f x) + f x * (\x\A. 1)"  eberlm@66277  232  by (intro insert.IH add_mono mult_left_mono prod_mono) auto  eberlm@66277  233  with insert.hyps show ?case by (simp add: algebra_simps)  eberlm@66277  234 qed simp_all  eberlm@66277  235 eberlm@66277  236 lemma norm_prod_minus1_le_prod_minus1:  eberlm@66277  237  fixes f :: "nat \ 'a :: {real_normed_div_algebra,comm_ring_1}"  eberlm@66277  238  shows "norm (prod (\n. 1 + f n) A - 1) \ prod (\n. 1 + norm (f n)) A - 1"  eberlm@66277  239 proof (induction A rule: infinite_finite_induct)  eberlm@66277  240  case (insert x A)  eberlm@66277  241  from insert.hyps have  eberlm@66277  242  "norm ((\n\insert x A. 1 + f n) - 1) =  eberlm@66277  243  norm ((\n\A. 1 + f n) - 1 + f x * (\n\A. 1 + f n))"  eberlm@66277  244  by (simp add: algebra_simps)  eberlm@66277  245  also have "\ \ norm ((\n\A. 1 + f n) - 1) + norm (f x * (\n\A. 1 + f n))"  eberlm@66277  246  by (rule norm_triangle_ineq)  eberlm@66277  247  also have "norm (f x * (\n\A. 1 + f n)) = norm (f x) * (\x\A. norm (1 + f x))"  eberlm@66277  248  by (simp add: prod_norm norm_mult)  eberlm@66277  249  also have "(\x\A. norm (1 + f x)) \ (\x\A. norm (1::'a) + norm (f x))"  eberlm@66277  250  by (intro prod_mono norm_triangle_ineq ballI conjI) auto  eberlm@66277  251  also have "norm (1::'a) = 1" by simp  eberlm@66277  252  also note insert.IH  eberlm@66277  253  also have "(\n\A. 1 + norm (f n)) - 1 + norm (f x) * (\x\A. 1 + norm (f x)) =  lp15@68064  254  (\n\insert x A. 1 + norm (f n)) - 1"  eberlm@66277  255  using insert.hyps by (simp add: algebra_simps)  eberlm@66277  256  finally show ?case by - (simp_all add: mult_left_mono)  eberlm@66277  257 qed simp_all  eberlm@66277  258 eberlm@66277  259 lemma convergent_prod_imp_ev_nonzero:  eberlm@66277  260  fixes f :: "nat \ 'a :: {t2_space,comm_semiring_1}"  eberlm@66277  261  assumes "convergent_prod f"  eberlm@66277  262  shows "eventually (\n. f n \ 0) sequentially"  eberlm@66277  263  using assms by (auto simp: eventually_at_top_linorder convergent_prod_altdef)  eberlm@66277  264 eberlm@66277  265 lemma convergent_prod_imp_LIMSEQ:  eberlm@66277  266  fixes f :: "nat \ 'a :: {real_normed_field}"  eberlm@66277  267  assumes "convergent_prod f"  eberlm@66277  268  shows "f \ 1"  eberlm@66277  269 proof -  eberlm@66277  270  from assms obtain M L where L: "(\n. \i\n. f (i+M)) \ L" "\n. n \ M \ f n \ 0" "L \ 0"  eberlm@66277  271  by (auto simp: convergent_prod_altdef)  eberlm@66277  272  hence L': "(\n. \i\Suc n. f (i+M)) \ L" by (subst filterlim_sequentially_Suc)  eberlm@66277  273  have "(\n. (\i\Suc n. f (i+M)) / (\i\n. f (i+M))) \ L / L"  eberlm@66277  274  using L L' by (intro tendsto_divide) simp_all  eberlm@66277  275  also from L have "L / L = 1" by simp  eberlm@66277  276  also have "(\n. (\i\Suc n. f (i+M)) / (\i\n. f (i+M))) = (\n. f (n + Suc M))"  eberlm@66277  277  using assms L by (auto simp: fun_eq_iff atMost_Suc)  eberlm@66277  278  finally show ?thesis by (rule LIMSEQ_offset)  eberlm@66277  279 qed  eberlm@66277  280 eberlm@66277  281 lemma abs_convergent_prod_imp_summable:  eberlm@66277  282  fixes f :: "nat \ 'a :: real_normed_div_algebra"  eberlm@66277  283  assumes "abs_convergent_prod f"  eberlm@66277  284  shows "summable (\i. norm (f i - 1))"  eberlm@66277  285 proof -  eberlm@66277  286  from assms have "convergent (\n. \i\n. 1 + norm (f i - 1))"  eberlm@66277  287  unfolding abs_convergent_prod_def by (rule convergent_prod_imp_convergent)  eberlm@66277  288  then obtain L where L: "(\n. \i\n. 1 + norm (f i - 1)) \ L"  eberlm@66277  289  unfolding convergent_def by blast  eberlm@66277  290  have "convergent (\n. \i\n. norm (f i - 1))"  eberlm@66277  291  proof (rule Bseq_monoseq_convergent)  eberlm@66277  292  have "eventually (\n. (\i\n. 1 + norm (f i - 1)) < L + 1) sequentially"  eberlm@66277  293  using L(1) by (rule order_tendstoD) simp_all  eberlm@66277  294  hence "\\<^sub>F x in sequentially. norm (\i\x. norm (f i - 1)) \ L + 1"  eberlm@66277  295  proof eventually_elim  eberlm@66277  296  case (elim n)  eberlm@66277  297  have "norm (\i\n. norm (f i - 1)) = (\i\n. norm (f i - 1))"  eberlm@66277  298  unfolding real_norm_def by (intro abs_of_nonneg sum_nonneg) simp_all  eberlm@66277  299  also have "\ \ (\i\n. 1 + norm (f i - 1))" by (rule sum_le_prod) auto  eberlm@66277  300  also have "\ < L + 1" by (rule elim)  eberlm@66277  301  finally show ?case by simp  eberlm@66277  302  qed  eberlm@66277  303  thus "Bseq (\n. \i\n. norm (f i - 1))" by (rule BfunI)  eberlm@66277  304  next  eberlm@66277  305  show "monoseq (\n. \i\n. norm (f i - 1))"  eberlm@66277  306  by (rule mono_SucI1) auto  eberlm@66277  307  qed  eberlm@66277  308  thus "summable (\i. norm (f i - 1))" by (simp add: summable_iff_convergent')  eberlm@66277  309 qed  eberlm@66277  310 eberlm@66277  311 lemma summable_imp_abs_convergent_prod:  eberlm@66277  312  fixes f :: "nat \ 'a :: real_normed_div_algebra"  eberlm@66277  313  assumes "summable (\i. norm (f i - 1))"  eberlm@66277  314  shows "abs_convergent_prod f"  eberlm@66277  315 proof (intro abs_convergent_prodI Bseq_monoseq_convergent)  eberlm@66277  316  show "monoseq (\n. \i\n. 1 + norm (f i - 1))"  eberlm@66277  317  by (intro mono_SucI1)  eberlm@66277  318  (auto simp: atMost_Suc algebra_simps intro!: mult_nonneg_nonneg prod_nonneg)  eberlm@66277  319 next  eberlm@66277  320  show "Bseq (\n. \i\n. 1 + norm (f i - 1))"  eberlm@66277  321  proof (rule Bseq_eventually_mono)  eberlm@66277  322  show "eventually (\n. norm (\i\n. 1 + norm (f i - 1)) \  eberlm@66277  323  norm (exp (\i\n. norm (f i - 1)))) sequentially"  eberlm@66277  324  by (intro always_eventually allI) (auto simp: abs_prod exp_sum intro!: prod_mono)  eberlm@66277  325  next  eberlm@66277  326  from assms have "(\n. \i\n. norm (f i - 1)) \ (\i. norm (f i - 1))"  eberlm@66277  327  using sums_def_le by blast  eberlm@66277  328  hence "(\n. exp (\i\n. norm (f i - 1))) \ exp (\i. norm (f i - 1))"  eberlm@66277  329  by (rule tendsto_exp)  eberlm@66277  330  hence "convergent (\n. exp (\i\n. norm (f i - 1)))"  eberlm@66277  331  by (rule convergentI)  eberlm@66277  332  thus "Bseq (\n. exp (\i\n. norm (f i - 1)))"  eberlm@66277  333  by (rule convergent_imp_Bseq)  eberlm@66277  334  qed  eberlm@66277  335 qed  eberlm@66277  336 eberlm@66277  337 lemma abs_convergent_prod_conv_summable:  eberlm@66277  338  fixes f :: "nat \ 'a :: real_normed_div_algebra"  eberlm@66277  339  shows "abs_convergent_prod f \ summable (\i. norm (f i - 1))"  eberlm@66277  340  by (blast intro: abs_convergent_prod_imp_summable summable_imp_abs_convergent_prod)  eberlm@66277  341 eberlm@66277  342 lemma abs_convergent_prod_imp_LIMSEQ:  eberlm@66277  343  fixes f :: "nat \ 'a :: {comm_ring_1,real_normed_div_algebra}"  eberlm@66277  344  assumes "abs_convergent_prod f"  eberlm@66277  345  shows "f \ 1"  eberlm@66277  346 proof -  eberlm@66277  347  from assms have "summable (\n. norm (f n - 1))"  eberlm@66277  348  by (rule abs_convergent_prod_imp_summable)  eberlm@66277  349  from summable_LIMSEQ_zero[OF this] have "(\n. f n - 1) \ 0"  eberlm@66277  350  by (simp add: tendsto_norm_zero_iff)  eberlm@66277  351  from tendsto_add[OF this tendsto_const[of 1]] show ?thesis by simp  eberlm@66277  352 qed  eberlm@66277  353 eberlm@66277  354 lemma abs_convergent_prod_imp_ev_nonzero:  eberlm@66277  355  fixes f :: "nat \ 'a :: {comm_ring_1,real_normed_div_algebra}"  eberlm@66277  356  assumes "abs_convergent_prod f"  eberlm@66277  357  shows "eventually (\n. f n \ 0) sequentially"  eberlm@66277  358 proof -  eberlm@66277  359  from assms have "f \ 1"  eberlm@66277  360  by (rule abs_convergent_prod_imp_LIMSEQ)  eberlm@66277  361  hence "eventually (\n. dist (f n) 1 < 1) at_top"  eberlm@66277  362  by (auto simp: tendsto_iff)  eberlm@66277  363  thus ?thesis by eventually_elim auto  eberlm@66277  364 qed  eberlm@66277  365 eberlm@66277  366 lemma convergent_prod_offset:  eberlm@66277  367  assumes "convergent_prod (\n. f (n + m))"  eberlm@66277  368  shows "convergent_prod f"  eberlm@66277  369 proof -  eberlm@66277  370  from assms obtain M L where "(\n. \k\n. f (k + (M + m))) \ L" "L \ 0"  lp15@68064  371  by (auto simp: prod_defs add.assoc)  lp15@68064  372  thus "convergent_prod f"  lp15@68064  373  unfolding prod_defs by blast  eberlm@66277  374 qed  eberlm@66277  375 eberlm@66277  376 lemma abs_convergent_prod_offset:  eberlm@66277  377  assumes "abs_convergent_prod (\n. f (n + m))"  eberlm@66277  378  shows "abs_convergent_prod f"  eberlm@66277  379  using assms unfolding abs_convergent_prod_def by (rule convergent_prod_offset)  eberlm@66277  380 eberlm@66277  381 lemma convergent_prod_ignore_initial_segment:  eberlm@66277  382  fixes f :: "nat \ 'a :: {real_normed_field}"  eberlm@66277  383  assumes "convergent_prod f"  eberlm@66277  384  shows "convergent_prod (\n. f (n + m))"  eberlm@66277  385 proof -  eberlm@66277  386  from assms obtain M L  eberlm@66277  387  where L: "(\n. \k\n. f (k + M)) \ L" "L \ 0" and nz: "\n. n \ M \ f n \ 0"  eberlm@66277  388  by (auto simp: convergent_prod_altdef)  eberlm@66277  389  define C where "C = (\k 0"  eberlm@66277  391  by (auto simp: C_def)  eberlm@66277  392 eberlm@66277  393  from L(1) have "(\n. \k\n+m. f (k + M)) \ L"  eberlm@66277  394  by (rule LIMSEQ_ignore_initial_segment)  eberlm@66277  395  also have "(\n. \k\n+m. f (k + M)) = (\n. C * (\k\n. f (k + M + m)))"  eberlm@66277  396  proof (rule ext, goal_cases)  eberlm@66277  397  case (1 n)  eberlm@66277  398  have "{..n+m} = {.. {m..n+m}" by auto  eberlm@66277  399  also have "(\k\\. f (k + M)) = C * (\k=m..n+m. f (k + M))"  eberlm@66277  400  unfolding C_def by (rule prod.union_disjoint) auto  eberlm@66277  401  also have "(\k=m..n+m. f (k + M)) = (\k\n. f (k + m + M))"  eberlm@66277  402  by (intro ext prod.reindex_bij_witness[of _ "\k. k + m" "\k. k - m"]) auto  eberlm@66277  403  finally show ?case by (simp add: add_ac)  eberlm@66277  404  qed  eberlm@66277  405  finally have "(\n. C * (\k\n. f (k + M + m)) / C) \ L / C"  eberlm@66277  406  by (intro tendsto_divide tendsto_const) auto  eberlm@66277  407  hence "(\n. \k\n. f (k + M + m)) \ L / C" by simp  eberlm@66277  408  moreover from \L \ 0\ have "L / C \ 0" by simp  lp15@68064  409  ultimately show ?thesis  lp15@68064  410  unfolding prod_defs by blast  eberlm@66277  411 qed  eberlm@66277  412 lp15@68136  413 corollary convergent_prod_ignore_nonzero_segment:  lp15@68136  414  fixes f :: "nat \ 'a :: real_normed_field"  lp15@68136  415  assumes f: "convergent_prod f" and nz: "\i. i \ M \ f i \ 0"  lp15@68136  416  shows "\p. gen_has_prod f M p"  lp15@68136  417  using convergent_prod_ignore_initial_segment [OF f]  lp15@68136  418  by (metis convergent_LIMSEQ_iff convergent_prod_iff_convergent le_add_same_cancel2 nz prod_defs(1) zero_order(1))  lp15@68136  419 lp15@68136  420 corollary abs_convergent_prod_ignore_initial_segment:  eberlm@66277  421  assumes "abs_convergent_prod f"  eberlm@66277  422  shows "abs_convergent_prod (\n. f (n + m))"  eberlm@66277  423  using assms unfolding abs_convergent_prod_def  eberlm@66277  424  by (rule convergent_prod_ignore_initial_segment)  eberlm@66277  425 eberlm@66277  426 lemma abs_convergent_prod_imp_convergent_prod:  eberlm@66277  427  fixes f :: "nat \ 'a :: {real_normed_div_algebra,complete_space,comm_ring_1}"  eberlm@66277  428  assumes "abs_convergent_prod f"  eberlm@66277  429  shows "convergent_prod f"  eberlm@66277  430 proof -  eberlm@66277  431  from assms have "eventually (\n. f n \ 0) sequentially"  eberlm@66277  432  by (rule abs_convergent_prod_imp_ev_nonzero)  eberlm@66277  433  then obtain N where N: "f n \ 0" if "n \ N" for n  eberlm@66277  434  by (auto simp: eventually_at_top_linorder)  eberlm@66277  435  let ?P = "\n. \i\n. f (i + N)" and ?Q = "\n. \i\n. 1 + norm (f (i + N) - 1)"  eberlm@66277  436 eberlm@66277  437  have "Cauchy ?P"  eberlm@66277  438  proof (rule CauchyI', goal_cases)  eberlm@66277  439  case (1 \)  eberlm@66277  440  from assms have "abs_convergent_prod (\n. f (n + N))"  eberlm@66277  441  by (rule abs_convergent_prod_ignore_initial_segment)  eberlm@66277  442  hence "Cauchy ?Q"  eberlm@66277  443  unfolding abs_convergent_prod_def  eberlm@66277  444  by (intro convergent_Cauchy convergent_prod_imp_convergent)  eberlm@66277  445  from CauchyD[OF this 1] obtain M where M: "norm (?Q m - ?Q n) < \" if "m \ M" "n \ M" for m n  eberlm@66277  446  by blast  eberlm@66277  447  show ?case  eberlm@66277  448  proof (rule exI[of _ M], safe, goal_cases)  eberlm@66277  449  case (1 m n)  eberlm@66277  450  have "dist (?P m) (?P n) = norm (?P n - ?P m)"  eberlm@66277  451  by (simp add: dist_norm norm_minus_commute)  eberlm@66277  452  also from 1 have "{..n} = {..m} \ {m<..n}" by auto  eberlm@66277  453  hence "norm (?P n - ?P m) = norm (?P m * (\k\{m<..n}. f (k + N)) - ?P m)"  eberlm@66277  454  by (subst prod.union_disjoint [symmetric]) (auto simp: algebra_simps)  eberlm@66277  455  also have "\ = norm (?P m * ((\k\{m<..n}. f (k + N)) - 1))"  eberlm@66277  456  by (simp add: algebra_simps)  eberlm@66277  457  also have "\ = (\k\m. norm (f (k + N))) * norm ((\k\{m<..n}. f (k + N)) - 1)"  eberlm@66277  458  by (simp add: norm_mult prod_norm)  eberlm@66277  459  also have "\ \ ?Q m * ((\k\{m<..n}. 1 + norm (f (k + N) - 1)) - 1)"  eberlm@66277  460  using norm_prod_minus1_le_prod_minus1[of "\k. f (k + N) - 1" "{m<..n}"]  eberlm@66277  461  norm_triangle_ineq[of 1 "f k - 1" for k]  eberlm@66277  462  by (intro mult_mono prod_mono ballI conjI norm_prod_minus1_le_prod_minus1 prod_nonneg) auto  eberlm@66277  463  also have "\ = ?Q m * (\k\{m<..n}. 1 + norm (f (k + N) - 1)) - ?Q m"  eberlm@66277  464  by (simp add: algebra_simps)  eberlm@66277  465  also have "?Q m * (\k\{m<..n}. 1 + norm (f (k + N) - 1)) =  eberlm@66277  466  (\k\{..m}\{m<..n}. 1 + norm (f (k + N) - 1))"  eberlm@66277  467  by (rule prod.union_disjoint [symmetric]) auto  eberlm@66277  468  also from 1 have "{..m}\{m<..n} = {..n}" by auto  eberlm@66277  469  also have "?Q n - ?Q m \ norm (?Q n - ?Q m)" by simp  eberlm@66277  470  also from 1 have "\ < \" by (intro M) auto  eberlm@66277  471  finally show ?case .  eberlm@66277  472  qed  eberlm@66277  473  qed  eberlm@66277  474  hence conv: "convergent ?P" by (rule Cauchy_convergent)  eberlm@66277  475  then obtain L where L: "?P \ L"  eberlm@66277  476  by (auto simp: convergent_def)  eberlm@66277  477 eberlm@66277  478  have "L \ 0"  eberlm@66277  479  proof  eberlm@66277  480  assume [simp]: "L = 0"  eberlm@66277  481  from tendsto_norm[OF L] have limit: "(\n. \k\n. norm (f (k + N))) \ 0"  eberlm@66277  482  by (simp add: prod_norm)  eberlm@66277  483 eberlm@66277  484  from assms have "(\n. f (n + N)) \ 1"  eberlm@66277  485  by (intro abs_convergent_prod_imp_LIMSEQ abs_convergent_prod_ignore_initial_segment)  eberlm@66277  486  hence "eventually (\n. norm (f (n + N) - 1) < 1) sequentially"  eberlm@66277  487  by (auto simp: tendsto_iff dist_norm)  eberlm@66277  488  then obtain M0 where M0: "norm (f (n + N) - 1) < 1" if "n \ M0" for n  eberlm@66277  489  by (auto simp: eventually_at_top_linorder)  eberlm@66277  490 eberlm@66277  491  {  eberlm@66277  492  fix M assume M: "M \ M0"  eberlm@66277  493  with M0 have M: "norm (f (n + N) - 1) < 1" if "n \ M" for n using that by simp  eberlm@66277  494 eberlm@66277  495  have "(\n. \k\n. 1 - norm (f (k+M+N) - 1)) \ 0"  eberlm@66277  496  proof (rule tendsto_sandwich)  eberlm@66277  497  show "eventually (\n. (\k\n. 1 - norm (f (k+M+N) - 1)) \ 0) sequentially"  eberlm@66277  498  using M by (intro always_eventually prod_nonneg allI ballI) (auto intro: less_imp_le)  eberlm@66277  499  have "norm (1::'a) - norm (f (i + M + N) - 1) \ norm (f (i + M + N))" for i  eberlm@66277  500  using norm_triangle_ineq3[of "f (i + M + N)" 1] by simp  eberlm@66277  501  thus "eventually (\n. (\k\n. 1 - norm (f (k+M+N) - 1)) \ (\k\n. norm (f (k+M+N)))) at_top"  eberlm@66277  502  using M by (intro always_eventually allI prod_mono ballI conjI) (auto intro: less_imp_le)  eberlm@66277  503   eberlm@66277  504  define C where "C = (\k 0" by (auto simp: C_def)  eberlm@66277  506  from L have "(\n. norm (\k\n+M. f (k + N))) \ 0"  eberlm@66277  507  by (intro LIMSEQ_ignore_initial_segment) (simp add: tendsto_norm_zero_iff)  eberlm@66277  508  also have "(\n. norm (\k\n+M. f (k + N))) = (\n. C * (\k\n. norm (f (k + M + N))))"  eberlm@66277  509  proof (rule ext, goal_cases)  eberlm@66277  510  case (1 n)  eberlm@66277  511  have "{..n+M} = {.. {M..n+M}" by auto  eberlm@66277  512  also have "norm (\k\\. f (k + N)) = C * norm (\k=M..n+M. f (k + N))"  eberlm@66277  513  unfolding C_def by (subst prod.union_disjoint) (auto simp: norm_mult prod_norm)  eberlm@66277  514  also have "(\k=M..n+M. f (k + N)) = (\k\n. f (k + N + M))"  eberlm@66277  515  by (intro prod.reindex_bij_witness[of _ "\i. i + M" "\i. i - M"]) auto  eberlm@66277  516  finally show ?case by (simp add: add_ac prod_norm)  eberlm@66277  517  qed  eberlm@66277  518  finally have "(\n. C * (\k\n. norm (f (k + M + N))) / C) \ 0 / C"  eberlm@66277  519  by (intro tendsto_divide tendsto_const) auto  eberlm@66277  520  thus "(\n. \k\n. norm (f (k + M + N))) \ 0" by simp  eberlm@66277  521  qed simp_all  eberlm@66277  522 eberlm@66277  523  have "1 - (\i. norm (f (i + M + N) - 1)) \ 0"  eberlm@66277  524  proof (rule tendsto_le)  eberlm@66277  525  show "eventually (\n. 1 - (\k\n. norm (f (k+M+N) - 1)) \  eberlm@66277  526  (\k\n. 1 - norm (f (k+M+N) - 1))) at_top"  eberlm@66277  527  using M by (intro always_eventually allI weierstrass_prod_ineq) (auto intro: less_imp_le)  eberlm@66277  528  show "(\n. \k\n. 1 - norm (f (k+M+N) - 1)) \ 0" by fact  eberlm@66277  529  show "(\n. 1 - (\k\n. norm (f (k + M + N) - 1)))  eberlm@66277  530  \ 1 - (\i. norm (f (i + M + N) - 1))"  eberlm@66277  531  by (intro tendsto_intros summable_LIMSEQ' summable_ignore_initial_segment  eberlm@66277  532  abs_convergent_prod_imp_summable assms)  eberlm@66277  533  qed simp_all  eberlm@66277  534  hence "(\i. norm (f (i + M + N) - 1)) \ 1" by simp  eberlm@66277  535  also have "\ + (\ii. norm (f (i + N) - 1))"  eberlm@66277  536  by (intro suminf_split_initial_segment [symmetric] summable_ignore_initial_segment  eberlm@66277  537  abs_convergent_prod_imp_summable assms)  eberlm@66277  538  finally have "1 + (\i (\i. norm (f (i + N) - 1))" by simp  eberlm@66277  539  } note * = this  eberlm@66277  540 eberlm@66277  541  have "1 + (\i. norm (f (i + N) - 1)) \ (\i. norm (f (i + N) - 1))"  eberlm@66277  542  proof (rule tendsto_le)  eberlm@66277  543  show "(\M. 1 + (\i 1 + (\i. norm (f (i + N) - 1))"  eberlm@66277  544  by (intro tendsto_intros summable_LIMSEQ summable_ignore_initial_segment  eberlm@66277  545  abs_convergent_prod_imp_summable assms)  eberlm@66277  546  show "eventually (\M. 1 + (\i (\i. norm (f (i + N) - 1))) at_top"  eberlm@66277  547  using eventually_ge_at_top[of M0] by eventually_elim (use * in auto)  eberlm@66277  548  qed simp_all  eberlm@66277  549  thus False by simp  eberlm@66277  550  qed  lp15@68064  551  with L show ?thesis by (auto simp: prod_defs)  lp15@68064  552 qed  lp15@68064  553 lp15@68136  554 lemma gen_has_prod_cases:  lp15@68064  555  fixes f :: "nat \ 'a :: {idom,topological_semigroup_mult,t2_space}"  lp15@68136  556  assumes "gen_has_prod f M p"  lp15@68136  557  obtains i where "in. \i\n. f (i + M)) \ p" "p \ 0"  lp15@68136  560  using assms unfolding gen_has_prod_def by blast+  lp15@68064  561  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  564  proof -  lp15@68064  565  have "{..n+M} = {.. {M..n+M}"  lp15@68064  566  by auto  lp15@68064  567  then have "prod f {..n+M} = prod f {..i\n. f (i + M))"  lp15@68064  570  by (metis (mono_tags, lifting) add.left_neutral atMost_atLeast0 prod_shift_bounds_cl_nat_ivl)  lp15@68064  571  finally show ?thesis by metis  lp15@68064  572  qed  lp15@68064  573  ultimately have "(\n. prod f {..n}) \ prod f {..i 0"  lp15@68136  576  using \p \ 0\ assms that by (auto simp: gen_has_prod_def)  lp15@68136  577  then show thesis  lp15@68136  578  using that by blast  lp15@68064  579 qed  lp15@68064  580 lp15@68136  581 corollary convergent_prod_offset_0:  lp15@68136  582  fixes f :: "nat \ 'a :: {idom,topological_semigroup_mult,t2_space}"  lp15@68136  583  assumes "convergent_prod f" "\i. f i \ 0"  lp15@68136  584  shows "\p. gen_has_prod f 0 p"  lp15@68136  585  using assms convergent_prod_def gen_has_prod_cases by blast  lp15@68136  586 lp15@68064  587 lemma prodinf_eq_lim:  lp15@68064  588  fixes f :: "nat \ 'a :: {idom,topological_semigroup_mult,t2_space}"  lp15@68064  589  assumes "convergent_prod f" "\i. f i \ 0"  lp15@68064  590  shows "prodinf f = lim (\n. \i\n. f i)"  lp15@68064  591  using assms convergent_prod_offset_0 [OF assms]  lp15@68064  592  by (simp add: prod_defs lim_def) (metis (no_types) assms(1) convergent_prod_to_zero_iff)  lp15@68064  593 lp15@68064  594 lemma has_prod_one[simp, intro]: "(\n. 1) has_prod 1"  lp15@68064  595  unfolding prod_defs by auto  lp15@68064  596 lp15@68064  597 lemma convergent_prod_one[simp, intro]: "convergent_prod (\n. 1)"  lp15@68064  598  unfolding prod_defs by auto  lp15@68064  599 lp15@68064  600 lemma prodinf_cong: "(\n. f n = g n) \ prodinf f = prodinf g"  lp15@68064  601  by presburger  lp15@68064  602 lp15@68064  603 lemma convergent_prod_cong:  lp15@68064  604  fixes f g :: "nat \ 'a::{field,topological_semigroup_mult,t2_space}"  lp15@68064  605  assumes ev: "eventually (\x. f x = g x) sequentially" and f: "\i. f i \ 0" and g: "\i. g i \ 0"  lp15@68064  606  shows "convergent_prod f = convergent_prod g"  lp15@68064  607 proof -  lp15@68064  608  from assms obtain N where N: "\n\N. f n = g n"  lp15@68064  609  by (auto simp: eventually_at_top_linorder)  lp15@68064  610  define C where "C = (\k 0"  lp15@68064  612  by (simp add: f)  lp15@68064  613  have *: "eventually (\n. prod f {..n} = C * prod g {..n}) sequentially"  lp15@68064  614  using eventually_ge_at_top[of N]  lp15@68064  615  proof eventually_elim  lp15@68064  616  case (elim n)  lp15@68064  617  then have "{..n} = {.. {N..n}"  lp15@68064  618  by auto  lp15@68064  619  also have "prod f ... = prod f {.. {N..n})"  lp15@68064  626  by (intro prod.union_disjoint [symmetric]) auto  lp15@68064  627  also from elim have "{.. {N..n} = {..n}"  lp15@68064  628  by auto  lp15@68064  629  finally show "prod f {..n} = C * prod g {..n}" .  lp15@68064  630  qed  lp15@68064  631  then have cong: "convergent (\n. prod f {..n}) = convergent (\n. C * prod g {..n})"  lp15@68064  632  by (rule convergent_cong)  lp15@68064  633  show ?thesis  lp15@68064  634  proof  lp15@68064  635  assume cf: "convergent_prod f"  lp15@68064  636  then have "\ (\n. prod g {..n}) \ 0"  lp15@68064  637  using tendsto_mult_left * convergent_prod_to_zero_iff f filterlim_cong by fastforce  lp15@68064  638  then show "convergent_prod g"  lp15@68064  639  by (metis convergent_mult_const_iff \C \ 0\ cong cf convergent_LIMSEQ_iff convergent_prod_iff_convergent convergent_prod_imp_convergent g)  lp15@68064  640  next  lp15@68064  641  assume cg: "convergent_prod g"  lp15@68064  642  have "\a. C * a \ 0 \ (\n. prod g {..n}) \ a"  lp15@68064  643  by (metis (no_types) \C \ 0\ cg convergent_prod_iff_nz_lim divide_eq_0_iff g nonzero_mult_div_cancel_right)  lp15@68064  644  then show "convergent_prod f"  lp15@68064  645  using "*" tendsto_mult_left filterlim_cong  lp15@68064  646  by (fastforce simp add: convergent_prod_iff_nz_lim f)  lp15@68064  647  qed  eberlm@66277  648 qed  eberlm@66277  649 lp15@68071  650 lemma has_prod_finite:  lp15@68071  651  fixes f :: "nat \ 'a::{idom,t2_space}"  lp15@68071  652  assumes [simp]: "finite N"  lp15@68071  653  and f: "\n. n \ N \ f n = 1"  lp15@68071  654  shows "f has_prod (\n\N. f n)"  lp15@68071  655 proof -  lp15@68071  656  have eq: "prod f {..n + Suc (Max N)} = prod f N" for n  lp15@68071  657  proof (rule prod.mono_neutral_right)  lp15@68071  658  show "N \ {..n + Suc (Max N)}"  lp15@68071  659  by (auto simp add: le_Suc_eq trans_le_add2)  lp15@68071  660  show "\i\{..n + Suc (Max N)} - N. f i = 1"  lp15@68071  661  using f by blast  lp15@68071  662  qed auto  lp15@68071  663  show ?thesis  lp15@68071  664  proof (cases "\n\N. f n \ 0")  lp15@68071  665  case True  lp15@68071  666  then have "prod f N \ 0"  lp15@68071  667  by simp  lp15@68071  668  moreover have "(\n. prod f {..n}) \ prod f N"  lp15@68071  669  by (rule LIMSEQ_offset[of _ "Suc (Max N)"]) (simp add: eq atLeast0LessThan del: add_Suc_right)  lp15@68071  670  ultimately show ?thesis  lp15@68071  671  by (simp add: gen_has_prod_def has_prod_def)  lp15@68071  672  next  lp15@68071  673  case False  lp15@68071  674  then obtain k where "k \ N" "f k = 0"  lp15@68071  675  by auto  lp15@68071  676  let ?Z = "{n \ N. f n = 0}"  lp15@68071  677  have maxge: "Max ?Z \ n" if "f n = 0" for n  lp15@68071  678  using Max_ge [of ?Z] \finite N\ \f n = 0\  lp15@68071  679  by (metis (mono_tags) Collect_mem_eq f finite_Collect_conjI mem_Collect_eq zero_neq_one)  lp15@68071  680  let ?q = "prod f {Suc (Max ?Z)..Max N}"  lp15@68071  681  have [simp]: "?q \ 0"  lp15@68071  682  using maxge Suc_n_not_le_n le_trans by force  lp15@68076  683  have eq: "(\i\n + Max N. f (Suc (i + Max ?Z))) = ?q" for n  lp15@68076  684  proof -  lp15@68076  685  have "(\i\n + Max N. f (Suc (i + Max ?Z))) = prod f {Suc (Max ?Z)..n + Max N + Suc (Max ?Z)}"  lp15@68076  686  proof (rule prod.reindex_cong [where l = "\i. i + Suc (Max ?Z)", THEN sym])  lp15@68076  687  show "{Suc (Max ?Z)..n + Max N + Suc (Max ?Z)} = (\i. i + Suc (Max ?Z))  {..n + Max N}"  lp15@68076  688  using le_Suc_ex by fastforce  lp15@68076  689  qed (auto simp: inj_on_def)  lp15@68076  690  also have "... = ?q"  lp15@68076  691  by (rule prod.mono_neutral_right)  lp15@68076  692  (use Max.coboundedI [OF \finite N\] f in \force+\)  lp15@68076  693  finally show ?thesis .  lp15@68076  694  qed  lp15@68071  695  have q: "gen_has_prod f (Suc (Max ?Z)) ?q"  lp15@68076  696  proof (simp add: gen_has_prod_def)  lp15@68076  697  show "(\n. \i\n. f (Suc (i + Max ?Z))) \ ?q"  lp15@68076  698  by (rule LIMSEQ_offset[of _ "(Max N)"]) (simp add: eq)  lp15@68076  699  qed  lp15@68071  700  show ?thesis  lp15@68071  701  unfolding has_prod_def  lp15@68071  702  proof (intro disjI2 exI conjI)  lp15@68071  703  show "prod f N = 0"  lp15@68071  704  using \f k = 0\ \k \ N\ \finite N\ prod_zero by blast  lp15@68071  705  show "f (Max ?Z) = 0"  lp15@68071  706  using Max_in [of ?Z] \finite N\ \f k = 0\ \k \ N\ by auto  lp15@68071  707  qed (use q in auto)  lp15@68071  708  qed  lp15@68071  709 qed  lp15@68071  710 lp15@68071  711 corollary has_prod_0:  lp15@68071  712  fixes f :: "nat \ 'a::{idom,t2_space}"  lp15@68071  713  assumes "\n. f n = 1"  lp15@68071  714  shows "f has_prod 1"  lp15@68071  715  by (simp add: assms has_prod_cong)  lp15@68071  716 lp15@68071  717 lemma convergent_prod_finite:  lp15@68071  718  fixes f :: "nat \ 'a::{idom,t2_space}"  lp15@68071  719  assumes "finite N" "\n. n \ N \ f n = 1"  lp15@68071  720  shows "convergent_prod f"  lp15@68071  721 proof -  lp15@68071  722  have "\n p. gen_has_prod f n p"  lp15@68071  723  using assms has_prod_def has_prod_finite by blast  lp15@68071  724  then show ?thesis  lp15@68071  725  by (simp add: convergent_prod_def)  lp15@68071  726 qed  lp15@68071  727 lp15@68127  728 lemma has_prod_If_finite_set:  lp15@68127  729  fixes f :: "nat \ 'a::{idom,t2_space}"  lp15@68127  730  shows "finite A \ (\r. if r \ A then f r else 1) has_prod (\r\A. f r)"  lp15@68127  731  using has_prod_finite[of A "(\r. if r \ A then f r else 1)"]  lp15@68127  732  by simp  lp15@68127  733 lp15@68127  734 lemma has_prod_If_finite:  lp15@68127  735  fixes f :: "nat \ 'a::{idom,t2_space}"  lp15@68127  736  shows "finite {r. P r} \ (\r. if P r then f r else 1) has_prod (\r | P r. f r)"  lp15@68127  737  using has_prod_If_finite_set[of "{r. P r}"] by simp  lp15@68127  738 lp15@68127  739 lemma convergent_prod_If_finite_set[simp, intro]:  lp15@68127  740  fixes f :: "nat \ 'a::{idom,t2_space}"  lp15@68127  741  shows "finite A \ convergent_prod (\r. if r \ A then f r else 1)"  lp15@68127  742  by (simp add: convergent_prod_finite)  lp15@68127  743 lp15@68127  744 lemma convergent_prod_If_finite[simp, intro]:  lp15@68127  745  fixes f :: "nat \ 'a::{idom,t2_space}"  lp15@68127  746  shows "finite {r. P r} \ convergent_prod (\r. if P r then f r else 1)"  lp15@68127  747  using convergent_prod_def has_prod_If_finite has_prod_def by fastforce  lp15@68127  748 lp15@68127  749 lemma has_prod_single:  lp15@68127  750  fixes f :: "nat \ 'a::{idom,t2_space}"  lp15@68127  751  shows "(\r. if r = i then f r else 1) has_prod f i"  lp15@68127  752  using has_prod_If_finite[of "\r. r = i"] by simp  lp15@68127  753 lp15@68136  754 context  lp15@68136  755  fixes f :: "nat \ 'a :: real_normed_field"  lp15@68136  756 begin  lp15@68136  757 lp15@68136  758 lemma convergent_prod_imp_has_prod:  lp15@68136  759  assumes "convergent_prod f"  lp15@68136  760  shows "\p. f has_prod p"  lp15@68136  761 proof -  lp15@68136  762  obtain M p where p: "gen_has_prod f M p"  lp15@68136  763  using assms convergent_prod_def by blast  lp15@68136  764  then have "p \ 0"  lp15@68136  765  using gen_has_prod_nonzero by blast  lp15@68136  766  with p have fnz: "f i \ 0" if "i \ M" for i  lp15@68136  767  using gen_has_prod_eq_0 that by blast  lp15@68136  768  define C where "C = (\nn\M. f n \ 0")  lp15@68136  771  case True  lp15@68136  772  then have "C \ 0"  lp15@68136  773  by (simp add: C_def)  lp15@68136  774  then show ?thesis  lp15@68136  775  by (meson True assms convergent_prod_offset_0 fnz has_prod_def nat_le_linear)  lp15@68136  776  next  lp15@68136  777  case False  lp15@68136  778  let ?N = "GREATEST n. f n = 0"  lp15@68136  779  have 0: "f ?N = 0"  lp15@68136  780  using fnz False  lp15@68136  781  by (metis (mono_tags, lifting) GreatestI_ex_nat nat_le_linear)  lp15@68136  782  have "f i \ 0" if "i > ?N" for i  lp15@68136  783  by (metis (mono_tags, lifting) Greatest_le_nat fnz leD linear that)  lp15@68136  784  then have "\p. gen_has_prod f (Suc ?N) p"  lp15@68136  785  using assms by (auto simp: intro!: convergent_prod_ignore_nonzero_segment)  lp15@68136  786  then show ?thesis  lp15@68136  787  unfolding has_prod_def using 0 by blast  lp15@68136  788  qed  lp15@68136  789 qed  lp15@68136  790 lp15@68136  791 lemma convergent_prod_has_prod [intro]:  lp15@68136  792  shows "convergent_prod f \ f has_prod (prodinf f)"  lp15@68136  793  unfolding prodinf_def  lp15@68136  794  by (metis convergent_prod_imp_has_prod has_prod_unique theI')  lp15@68136  795 lp15@68136  796 lemma convergent_prod_LIMSEQ:  lp15@68136  797  shows "convergent_prod f \ (\n. \i\n. f i) \ prodinf f"  lp15@68136  798  by (metis convergent_LIMSEQ_iff convergent_prod_has_prod convergent_prod_imp_convergent  lp15@68136  799  convergent_prod_to_zero_iff gen_has_prod_eq_0 has_prod_def prodinf_eq_lim zero_le)  lp15@68136  800 lp15@68136  801 lemma has_prod_iff: "f has_prod x \ convergent_prod f \ prodinf f = x"  lp15@68136  802 proof  lp15@68136  803  assume "f has_prod x"  lp15@68136  804  then show "convergent_prod f \ prodinf f = x"  lp15@68136  805  apply safe  lp15@68136  806  using convergent_prod_def has_prod_def apply blast  lp15@68136  807  using has_prod_unique by blast  lp15@68136  808 qed auto  lp15@68136  809 lp15@68136  810 lemma convergent_prod_has_prod_iff: "convergent_prod f \ f has_prod prodinf f"  lp15@68136  811  by (auto simp: has_prod_iff convergent_prod_has_prod)  lp15@68136  812 lp15@68136  813 lemma prodinf_finite:  lp15@68136  814  assumes N: "finite N"  lp15@68136  815  and f: "\n. n \ N \ f n = 1"  lp15@68136  816  shows "prodinf f = (\n\N. f n)"  lp15@68136  817  using has_prod_finite[OF assms, THEN has_prod_unique] by simp  lp15@68127  818 eberlm@66277  819 end  lp15@68136  820 lp15@68136  821 end `