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