src/HOL/Analysis/Infinite_Products.thy
 author nipkow Sat Dec 29 15:43:53 2018 +0100 (6 months ago) changeset 69529 4ab9657b3257 parent 68651 16d98ef49a2c child 69565 1daf07b65385 permissions -rw-r--r--
capitalize proper names in lemma names
 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  lp15@68585  9  imports Topology_Euclidean_Space Complex_Transcendental  eberlm@66277  10 begin  lp15@68424  11 eberlm@68651  12 subsection%unimportant \Preliminaries\  lp15@68424  13 eberlm@66277  14 lemma sum_le_prod:  eberlm@66277  15  fixes f :: "'a \ 'b :: linordered_semidom"  eberlm@66277  16  assumes "\x. x \ A \ f x \ 0"  eberlm@66277  17  shows "sum f A \ (\x\A. 1 + f x)"  eberlm@66277  18  using assms  eberlm@66277  19 proof (induction A rule: infinite_finite_induct)  eberlm@66277  20  case (insert x A)  eberlm@66277  21  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  22  by (intro add_mono insert mult_left_mono prod_mono) (auto intro: insert.prems)  eberlm@66277  23  with insert.hyps show ?case by (simp add: algebra_simps)  eberlm@66277  24 qed simp_all  eberlm@66277  25 eberlm@66277  26 lemma prod_le_exp_sum:  eberlm@66277  27  fixes f :: "'a \ real"  eberlm@66277  28  assumes "\x. x \ A \ f x \ 0"  eberlm@66277  29  shows "prod (\x. 1 + f x) A \ exp (sum f A)"  eberlm@66277  30  using assms  eberlm@66277  31 proof (induction A rule: infinite_finite_induct)  eberlm@66277  32  case (insert x A)  eberlm@66277  33  have "(1 + f x) * (\x\A. 1 + f x) \ exp (f x) * exp (sum f A)"  eberlm@66277  34  using insert.prems by (intro mult_mono insert prod_nonneg exp_ge_add_one_self) auto  eberlm@66277  35  with insert.hyps show ?case by (simp add: algebra_simps exp_add)  eberlm@66277  36 qed simp_all  eberlm@66277  37 eberlm@66277  38 lemma lim_ln_1_plus_x_over_x_at_0: "(\x::real. ln (1 + x) / x) \0\ 1"  eberlm@66277  39 proof (rule lhopital)  eberlm@66277  40  show "(\x::real. ln (1 + x)) \0\ 0"  eberlm@66277  41  by (rule tendsto_eq_intros refl | simp)+  eberlm@66277  42  have "eventually (\x::real. x \ {-1/2<..<1/2}) (nhds 0)"  eberlm@66277  43  by (rule eventually_nhds_in_open) auto  eberlm@66277  44  hence *: "eventually (\x::real. x \ {-1/2<..<1/2}) (at 0)"  eberlm@66277  45  by (rule filter_leD [rotated]) (simp_all add: at_within_def)  eberlm@66277  46  show "eventually (\x::real. ((\x. ln (1 + x)) has_field_derivative inverse (1 + x)) (at x)) (at 0)"  eberlm@66277  47  using * by eventually_elim (auto intro!: derivative_eq_intros simp: field_simps)  eberlm@66277  48  show "eventually (\x::real. ((\x. x) has_field_derivative 1) (at x)) (at 0)"  eberlm@66277  49  using * by eventually_elim (auto intro!: derivative_eq_intros simp: field_simps)  eberlm@66277  50  show "\\<^sub>F x in at 0. x \ 0" by (auto simp: at_within_def eventually_inf_principal)  eberlm@66277  51  show "(\x::real. inverse (1 + x) / 1) \0\ 1"  eberlm@66277  52  by (rule tendsto_eq_intros refl | simp)+  eberlm@66277  53 qed auto  eberlm@66277  54 lp15@68424  55 subsection\Definitions and basic properties\  lp15@68424  56 eberlm@68651  57 definition%important raw_has_prod :: "[nat \ 'a::{t2_space, comm_semiring_1}, nat, 'a] \ bool"  lp15@68361  58  where "raw_has_prod f M p \ (\n. \i\n. f (i+M)) \ p \ p \ 0"  lp15@68064  59 lp15@68064  60 text\The nonzero and zero cases, as in \emph{Complex Analysis} by Joseph Bak and Donald J.Newman, page 241\  eberlm@68651  61 definition%important  eberlm@68651  62  has_prod :: "(nat \ 'a::{t2_space, comm_semiring_1}) \ 'a \ bool" (infixr "has'_prod" 80)  lp15@68361  63  where "f has_prod p \ raw_has_prod f 0 p \ (\i q. p = 0 \ f i = 0 \ raw_has_prod f (Suc i) q)"  lp15@68064  64 eberlm@68651  65 definition%important convergent_prod :: "(nat \ 'a :: {t2_space,comm_semiring_1}) \ bool" where  lp15@68361  66  "convergent_prod f \ \M p. raw_has_prod f M p"  lp15@68064  67 eberlm@68651  68 definition%important prodinf :: "(nat \ 'a::{t2_space, comm_semiring_1}) \ 'a"  lp15@68064  69  (binder "\" 10)  lp15@68064  70  where "prodinf f = (THE p. f has_prod p)"  lp15@68064  71 lp15@68361  72 lemmas prod_defs = raw_has_prod_def has_prod_def convergent_prod_def prodinf_def  lp15@68064  73 lp15@68064  74 lemma has_prod_subst[trans]: "f = g \ g has_prod z \ f has_prod z"  lp15@68064  75  by simp  lp15@68064  76 lp15@68064  77 lemma has_prod_cong: "(\n. f n = g n) \ f has_prod c \ g has_prod c"  lp15@68064  78  by presburger  eberlm@66277  79 lp15@68361  80 lemma raw_has_prod_nonzero [simp]: "\ raw_has_prod f M 0"  lp15@68361  81  by (simp add: raw_has_prod_def)  lp15@68071  82 lp15@68361  83 lemma raw_has_prod_eq_0:  lp15@68361  84  fixes f :: "nat \ 'a::{semidom,t2_space}"  lp15@68361  85  assumes p: "raw_has_prod f m p" and i: "f i = 0" "i \ m"  lp15@68136  86  shows "p = 0"  lp15@68136  87 proof -  lp15@68136  88  have eq0: "(\k\n. f (k+m)) = 0" if "i - m \ n" for n  lp15@68361  89  proof -  lp15@68361  90  have "\k\n. f (k + m) = 0"  lp15@68361  91  using i that by auto  lp15@68361  92  then show ?thesis  lp15@68361  93  by auto  lp15@68361  94  qed  lp15@68136  95  have "(\n. \i\n. f (i + m)) \ 0"  lp15@68136  96  by (rule LIMSEQ_offset [where k = "i-m"]) (simp add: eq0)  lp15@68136  97  with p show ?thesis  lp15@68361  98  unfolding raw_has_prod_def  lp15@68136  99  using LIMSEQ_unique by blast  lp15@68136  100 qed  lp15@68136  101 lp15@68452  102 lemma raw_has_prod_Suc:  lp15@68452  103  "raw_has_prod f (Suc M) a \ raw_has_prod (\n. f (Suc n)) M a"  lp15@68452  104  unfolding raw_has_prod_def by auto  lp15@68452  105 lp15@68361  106 lemma has_prod_0_iff: "f has_prod 0 \ (\i. f i = 0 \ (\p. raw_has_prod f (Suc i) p))"  lp15@68071  107  by (simp add: has_prod_def)  lp15@68136  108   lp15@68136  109 lemma has_prod_unique2:  lp15@68361  110  fixes f :: "nat \ 'a::{semidom,t2_space}"  lp15@68136  111  assumes "f has_prod a" "f has_prod b" shows "a = b"  lp15@68136  112  using assms  lp15@68361  113  by (auto simp: has_prod_def raw_has_prod_eq_0) (meson raw_has_prod_def sequentially_bot tendsto_unique)  lp15@68136  114 lp15@68136  115 lemma has_prod_unique:  lp15@68361  116  fixes f :: "nat \ 'a :: {semidom,t2_space}"  lp15@68136  117  shows "f has_prod s \ s = prodinf f"  lp15@68136  118  by (simp add: has_prod_unique2 prodinf_def the_equality)  lp15@68071  119 eberlm@66277  120 lemma convergent_prod_altdef:  eberlm@66277  121  fixes f :: "nat \ 'a :: {t2_space,comm_semiring_1}"  eberlm@66277  122  shows "convergent_prod f \ (\M L. (\n\M. f n \ 0) \ (\n. \i\n. f (i+M)) \ L \ L \ 0)"  eberlm@66277  123 proof  eberlm@66277  124  assume "convergent_prod f"  eberlm@66277  125  then obtain M L where *: "(\n. \i\n. f (i+M)) \ L" "L \ 0"  lp15@68064  126  by (auto simp: prod_defs)  eberlm@66277  127  have "f i \ 0" if "i \ M" for i  eberlm@66277  128  proof  eberlm@66277  129  assume "f i = 0"  eberlm@66277  130  have **: "eventually (\n. (\i\n. f (i+M)) = 0) sequentially"  eberlm@66277  131  using eventually_ge_at_top[of "i - M"]  eberlm@66277  132  proof eventually_elim  eberlm@66277  133  case (elim n)  eberlm@66277  134  with \f i = 0\ and \i \ M\ show ?case  eberlm@66277  135  by (auto intro!: bexI[of _ "i - M"] prod_zero)  eberlm@66277  136  qed  eberlm@66277  137  have "(\n. (\i\n. f (i+M))) \ 0"  eberlm@66277  138  unfolding filterlim_iff  eberlm@66277  139  by (auto dest!: eventually_nhds_x_imp_x intro!: eventually_mono[OF **])  eberlm@66277  140  from tendsto_unique[OF _ this *(1)] and *(2)  eberlm@66277  141  show False by simp  eberlm@66277  142  qed  eberlm@66277  143  with * show "(\M L. (\n\M. f n \ 0) \ (\n. \i\n. f (i+M)) \ L \ L \ 0)"  eberlm@66277  144  by blast  lp15@68064  145 qed (auto simp: prod_defs)  eberlm@66277  146 lp15@68424  147 lp15@68424  148 subsection\Absolutely convergent products\  lp15@68424  149 eberlm@68651  150 definition%important abs_convergent_prod :: "(nat \ _) \ bool" where  eberlm@66277  151  "abs_convergent_prod f \ convergent_prod (\i. 1 + norm (f i - 1))"  eberlm@66277  152 eberlm@66277  153 lemma abs_convergent_prodI:  eberlm@66277  154  assumes "convergent (\n. \i\n. 1 + norm (f i - 1))"  eberlm@66277  155  shows "abs_convergent_prod f"  eberlm@66277  156 proof -  eberlm@66277  157  from assms obtain L where L: "(\n. \i\n. 1 + norm (f i - 1)) \ L"  eberlm@66277  158  by (auto simp: convergent_def)  eberlm@66277  159  have "L \ 1"  eberlm@66277  160  proof (rule tendsto_le)  eberlm@66277  161  show "eventually (\n. (\i\n. 1 + norm (f i - 1)) \ 1) sequentially"  eberlm@66277  162  proof (intro always_eventually allI)  eberlm@66277  163  fix n  eberlm@66277  164  have "(\i\n. 1 + norm (f i - 1)) \ (\i\n. 1)"  eberlm@66277  165  by (intro prod_mono) auto  eberlm@66277  166  thus "(\i\n. 1 + norm (f i - 1)) \ 1" by simp  eberlm@66277  167  qed  eberlm@66277  168  qed (use L in simp_all)  eberlm@66277  169  hence "L \ 0" by auto  lp15@68064  170  with L show ?thesis unfolding abs_convergent_prod_def prod_defs  eberlm@66277  171  by (intro exI[of _ "0::nat"] exI[of _ L]) auto  eberlm@66277  172 qed  eberlm@66277  173 eberlm@66277  174 lemma  lp15@68064  175  fixes f :: "nat \ 'a :: {topological_semigroup_mult,t2_space,idom}"  eberlm@66277  176  assumes "convergent_prod f"  eberlm@66277  177  shows convergent_prod_imp_convergent: "convergent (\n. \i\n. f i)"  eberlm@66277  178  and convergent_prod_to_zero_iff: "(\n. \i\n. f i) \ 0 \ (\i. f i = 0)"  eberlm@66277  179 proof -  eberlm@66277  180  from assms obtain M L  eberlm@66277  181  where M: "\n. n \ M \ f n \ 0" and "(\n. \i\n. f (i + M)) \ L" and "L \ 0"  eberlm@66277  182  by (auto simp: convergent_prod_altdef)  eberlm@66277  183  note this(2)  eberlm@66277  184  also have "(\n. \i\n. f (i + M)) = (\n. \i=M..M+n. f i)"  eberlm@66277  185  by (intro ext prod.reindex_bij_witness[of _ "\n. n - M" "\n. n + M"]) auto  eberlm@66277  186  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  189  by (subst prod.union_disjoint) auto  eberlm@66277  190  also have "(\n. {.. {M..M+n}) = (\n. {..n+M})" by auto  eberlm@66277  191  finally have lim: "(\n. prod f {..n}) \ prod f {..n. \i\n. f i)"  eberlm@66277  194  by (auto simp: convergent_def)  eberlm@66277  195 eberlm@66277  196  show "(\n. \i\n. f i) \ 0 \ (\i. f i = 0)"  eberlm@66277  197  proof  eberlm@66277  198  assume "\i. f i = 0"  eberlm@66277  199  then obtain i where "f i = 0" by auto  eberlm@66277  200  moreover with M have "i < M" by (cases "i < M") auto  eberlm@66277  201  ultimately have "(\in. \i\n. f i) \ 0" by simp  eberlm@66277  203  next  eberlm@66277  204  assume "(\n. \i\n. f i) \ 0"  eberlm@66277  205  from tendsto_unique[OF _ this lim] and \L \ 0\  eberlm@66277  206  show "\i. f i = 0" by auto  eberlm@66277  207  qed  eberlm@66277  208 qed  eberlm@66277  209 lp15@68064  210 lemma convergent_prod_iff_nz_lim:  lp15@68064  211  fixes f :: "nat \ 'a :: {topological_semigroup_mult,t2_space,idom}"  lp15@68064  212  assumes "\i. f i \ 0"  lp15@68064  213  shows "convergent_prod f \ (\L. (\n. \i\n. f i) \ L \ L \ 0)"  lp15@68064  214  (is "?lhs \ ?rhs")  lp15@68064  215 proof  lp15@68064  216  assume ?lhs then show ?rhs  lp15@68064  217  using assms convergentD convergent_prod_imp_convergent convergent_prod_to_zero_iff by blast  lp15@68064  218 next  lp15@68064  219  assume ?rhs then show ?lhs  lp15@68064  220  unfolding prod_defs  lp15@68138  221  by (rule_tac x=0 in exI) auto  lp15@68064  222 qed  lp15@68064  223 eberlm@68651  224 lemma%important convergent_prod_iff_convergent:  lp15@68064  225  fixes f :: "nat \ 'a :: {topological_semigroup_mult,t2_space,idom}"  lp15@68064  226  assumes "\i. f i \ 0"  lp15@68064  227  shows "convergent_prod f \ convergent (\n. \i\n. f i) \ lim (\n. \i\n. f i) \ 0"  lp15@68138  228  by (force simp: convergent_prod_iff_nz_lim assms convergent_def limI)  lp15@68064  229 lp15@68527  230 lemma bounded_imp_convergent_prod:  lp15@68527  231  fixes a :: "nat \ real"  lp15@68527  232  assumes 1: "\n. a n \ 1" and bounded: "\n. (\i\n. a i) \ B"  lp15@68527  233  shows "convergent_prod a"  lp15@68527  234 proof -  lp15@68527  235  have "bdd_above (range(\n. \i\n. a i))"  lp15@68527  236  by (meson bdd_aboveI2 bounded)  lp15@68527  237  moreover have "incseq (\n. \i\n. a i)"  lp15@68527  238  unfolding mono_def by (metis 1 prod_mono2 atMost_subset_iff dual_order.trans finite_atMost zero_le_one)  lp15@68527  239  ultimately obtain p where p: "(\n. \i\n. a i) \ p"  lp15@68527  240  using LIMSEQ_incseq_SUP by blast  lp15@68527  241  then have "p \ 0"  lp15@68527  242  by (metis "1" not_one_le_zero prod_ge_1 LIMSEQ_le_const)  lp15@68527  243  with 1 p show ?thesis  lp15@68527  244  by (metis convergent_prod_iff_nz_lim not_one_le_zero)  lp15@68527  245 qed  lp15@68527  246 lp15@68064  247 eberlm@66277  248 lemma abs_convergent_prod_altdef:  lp15@68064  249  fixes f :: "nat \ 'a :: {one,real_normed_vector}"  lp15@68064  250  shows "abs_convergent_prod f \ convergent (\n. \i\n. 1 + norm (f i - 1))"  eberlm@66277  251 proof  eberlm@66277  252  assume "abs_convergent_prod f"  eberlm@66277  253  thus "convergent (\n. \i\n. 1 + norm (f i - 1))"  eberlm@66277  254  by (auto simp: abs_convergent_prod_def intro!: convergent_prod_imp_convergent)  eberlm@66277  255 qed (auto intro: abs_convergent_prodI)  eberlm@66277  256 nipkow@69529  257 lemma Weierstrass_prod_ineq:  eberlm@66277  258  fixes f :: "'a \ real"  eberlm@66277  259  assumes "\x. x \ A \ f x \ {0..1}"  eberlm@66277  260  shows "1 - sum f A \ (\x\A. 1 - f x)"  eberlm@66277  261  using assms  eberlm@66277  262 proof (induction A rule: infinite_finite_induct)  eberlm@66277  263  case (insert x A)  eberlm@66277  264  from insert.hyps and insert.prems  eberlm@66277  265  have "1 - sum f A + f x * (\x\A. 1 - f x) \ (\x\A. 1 - f x) + f x * (\x\A. 1)"  eberlm@66277  266  by (intro insert.IH add_mono mult_left_mono prod_mono) auto  eberlm@66277  267  with insert.hyps show ?case by (simp add: algebra_simps)  eberlm@66277  268 qed simp_all  eberlm@66277  269 eberlm@66277  270 lemma norm_prod_minus1_le_prod_minus1:  eberlm@66277  271  fixes f :: "nat \ 'a :: {real_normed_div_algebra,comm_ring_1}"  eberlm@66277  272  shows "norm (prod (\n. 1 + f n) A - 1) \ prod (\n. 1 + norm (f n)) A - 1"  eberlm@66277  273 proof (induction A rule: infinite_finite_induct)  eberlm@66277  274  case (insert x A)  eberlm@66277  275  from insert.hyps have  eberlm@66277  276  "norm ((\n\insert x A. 1 + f n) - 1) =  eberlm@66277  277  norm ((\n\A. 1 + f n) - 1 + f x * (\n\A. 1 + f n))"  eberlm@66277  278  by (simp add: algebra_simps)  eberlm@66277  279  also have "\ \ norm ((\n\A. 1 + f n) - 1) + norm (f x * (\n\A. 1 + f n))"  eberlm@66277  280  by (rule norm_triangle_ineq)  eberlm@66277  281  also have "norm (f x * (\n\A. 1 + f n)) = norm (f x) * (\x\A. norm (1 + f x))"  eberlm@66277  282  by (simp add: prod_norm norm_mult)  eberlm@66277  283  also have "(\x\A. norm (1 + f x)) \ (\x\A. norm (1::'a) + norm (f x))"  eberlm@66277  284  by (intro prod_mono norm_triangle_ineq ballI conjI) auto  eberlm@66277  285  also have "norm (1::'a) = 1" by simp  eberlm@66277  286  also note insert.IH  eberlm@66277  287  also have "(\n\A. 1 + norm (f n)) - 1 + norm (f x) * (\x\A. 1 + norm (f x)) =  lp15@68064  288  (\n\insert x A. 1 + norm (f n)) - 1"  eberlm@66277  289  using insert.hyps by (simp add: algebra_simps)  eberlm@66277  290  finally show ?case by - (simp_all add: mult_left_mono)  eberlm@66277  291 qed simp_all  eberlm@66277  292 eberlm@66277  293 lemma convergent_prod_imp_ev_nonzero:  eberlm@66277  294  fixes f :: "nat \ 'a :: {t2_space,comm_semiring_1}"  eberlm@66277  295  assumes "convergent_prod f"  eberlm@66277  296  shows "eventually (\n. f n \ 0) sequentially"  eberlm@66277  297  using assms by (auto simp: eventually_at_top_linorder convergent_prod_altdef)  eberlm@66277  298 eberlm@66277  299 lemma convergent_prod_imp_LIMSEQ:  eberlm@66277  300  fixes f :: "nat \ 'a :: {real_normed_field}"  eberlm@66277  301  assumes "convergent_prod f"  eberlm@66277  302  shows "f \ 1"  eberlm@66277  303 proof -  eberlm@66277  304  from assms obtain M L where L: "(\n. \i\n. f (i+M)) \ L" "\n. n \ M \ f n \ 0" "L \ 0"  eberlm@66277  305  by (auto simp: convergent_prod_altdef)  eberlm@66277  306  hence L': "(\n. \i\Suc n. f (i+M)) \ L" by (subst filterlim_sequentially_Suc)  eberlm@66277  307  have "(\n. (\i\Suc n. f (i+M)) / (\i\n. f (i+M))) \ L / L"  eberlm@66277  308  using L L' by (intro tendsto_divide) simp_all  eberlm@66277  309  also from L have "L / L = 1" by simp  eberlm@66277  310  also have "(\n. (\i\Suc n. f (i+M)) / (\i\n. f (i+M))) = (\n. f (n + Suc M))"  eberlm@66277  311  using assms L by (auto simp: fun_eq_iff atMost_Suc)  eberlm@66277  312  finally show ?thesis by (rule LIMSEQ_offset)  eberlm@66277  313 qed  eberlm@66277  314 eberlm@66277  315 lemma abs_convergent_prod_imp_summable:  eberlm@66277  316  fixes f :: "nat \ 'a :: real_normed_div_algebra"  eberlm@66277  317  assumes "abs_convergent_prod f"  eberlm@66277  318  shows "summable (\i. norm (f i - 1))"  eberlm@66277  319 proof -  eberlm@66277  320  from assms have "convergent (\n. \i\n. 1 + norm (f i - 1))"  eberlm@66277  321  unfolding abs_convergent_prod_def by (rule convergent_prod_imp_convergent)  eberlm@66277  322  then obtain L where L: "(\n. \i\n. 1 + norm (f i - 1)) \ L"  eberlm@66277  323  unfolding convergent_def by blast  eberlm@66277  324  have "convergent (\n. \i\n. norm (f i - 1))"  eberlm@66277  325  proof (rule Bseq_monoseq_convergent)  eberlm@66277  326  have "eventually (\n. (\i\n. 1 + norm (f i - 1)) < L + 1) sequentially"  eberlm@66277  327  using L(1) by (rule order_tendstoD) simp_all  eberlm@66277  328  hence "\\<^sub>F x in sequentially. norm (\i\x. norm (f i - 1)) \ L + 1"  eberlm@66277  329  proof eventually_elim  eberlm@66277  330  case (elim n)  eberlm@66277  331  have "norm (\i\n. norm (f i - 1)) = (\i\n. norm (f i - 1))"  eberlm@66277  332  unfolding real_norm_def by (intro abs_of_nonneg sum_nonneg) simp_all  eberlm@66277  333  also have "\ \ (\i\n. 1 + norm (f i - 1))" by (rule sum_le_prod) auto  eberlm@66277  334  also have "\ < L + 1" by (rule elim)  eberlm@66277  335  finally show ?case by simp  eberlm@66277  336  qed  eberlm@66277  337  thus "Bseq (\n. \i\n. norm (f i - 1))" by (rule BfunI)  eberlm@66277  338  next  eberlm@66277  339  show "monoseq (\n. \i\n. norm (f i - 1))"  eberlm@66277  340  by (rule mono_SucI1) auto  eberlm@66277  341  qed  eberlm@66277  342  thus "summable (\i. norm (f i - 1))" by (simp add: summable_iff_convergent')  eberlm@66277  343 qed  eberlm@66277  344 eberlm@66277  345 lemma summable_imp_abs_convergent_prod:  eberlm@66277  346  fixes f :: "nat \ 'a :: real_normed_div_algebra"  eberlm@66277  347  assumes "summable (\i. norm (f i - 1))"  eberlm@66277  348  shows "abs_convergent_prod f"  eberlm@66277  349 proof (intro abs_convergent_prodI Bseq_monoseq_convergent)  eberlm@66277  350  show "monoseq (\n. \i\n. 1 + norm (f i - 1))"  eberlm@66277  351  by (intro mono_SucI1)  eberlm@66277  352  (auto simp: atMost_Suc algebra_simps intro!: mult_nonneg_nonneg prod_nonneg)  eberlm@66277  353 next  eberlm@66277  354  show "Bseq (\n. \i\n. 1 + norm (f i - 1))"  eberlm@66277  355  proof (rule Bseq_eventually_mono)  eberlm@66277  356  show "eventually (\n. norm (\i\n. 1 + norm (f i - 1)) \  eberlm@66277  357  norm (exp (\i\n. norm (f i - 1)))) sequentially"  eberlm@66277  358  by (intro always_eventually allI) (auto simp: abs_prod exp_sum intro!: prod_mono)  eberlm@66277  359  next  eberlm@66277  360  from assms have "(\n. \i\n. norm (f i - 1)) \ (\i. norm (f i - 1))"  eberlm@66277  361  using sums_def_le by blast  eberlm@66277  362  hence "(\n. exp (\i\n. norm (f i - 1))) \ exp (\i. norm (f i - 1))"  eberlm@66277  363  by (rule tendsto_exp)  eberlm@66277  364  hence "convergent (\n. exp (\i\n. norm (f i - 1)))"  eberlm@66277  365  by (rule convergentI)  eberlm@66277  366  thus "Bseq (\n. exp (\i\n. norm (f i - 1)))"  eberlm@66277  367  by (rule convergent_imp_Bseq)  eberlm@66277  368  qed  eberlm@66277  369 qed  eberlm@66277  370 eberlm@68651  371 theorem abs_convergent_prod_conv_summable:  eberlm@66277  372  fixes f :: "nat \ 'a :: real_normed_div_algebra"  eberlm@66277  373  shows "abs_convergent_prod f \ summable (\i. norm (f i - 1))"  eberlm@66277  374  by (blast intro: abs_convergent_prod_imp_summable summable_imp_abs_convergent_prod)  eberlm@66277  375 eberlm@66277  376 lemma abs_convergent_prod_imp_LIMSEQ:  eberlm@66277  377  fixes f :: "nat \ 'a :: {comm_ring_1,real_normed_div_algebra}"  eberlm@66277  378  assumes "abs_convergent_prod f"  eberlm@66277  379  shows "f \ 1"  eberlm@66277  380 proof -  eberlm@66277  381  from assms have "summable (\n. norm (f n - 1))"  eberlm@66277  382  by (rule abs_convergent_prod_imp_summable)  eberlm@66277  383  from summable_LIMSEQ_zero[OF this] have "(\n. f n - 1) \ 0"  eberlm@66277  384  by (simp add: tendsto_norm_zero_iff)  eberlm@66277  385  from tendsto_add[OF this tendsto_const[of 1]] show ?thesis by simp  eberlm@66277  386 qed  eberlm@66277  387 eberlm@66277  388 lemma abs_convergent_prod_imp_ev_nonzero:  eberlm@66277  389  fixes f :: "nat \ 'a :: {comm_ring_1,real_normed_div_algebra}"  eberlm@66277  390  assumes "abs_convergent_prod f"  eberlm@66277  391  shows "eventually (\n. f n \ 0) sequentially"  eberlm@66277  392 proof -  eberlm@66277  393  from assms have "f \ 1"  eberlm@66277  394  by (rule abs_convergent_prod_imp_LIMSEQ)  eberlm@66277  395  hence "eventually (\n. dist (f n) 1 < 1) at_top"  eberlm@66277  396  by (auto simp: tendsto_iff)  eberlm@66277  397  thus ?thesis by eventually_elim auto  eberlm@66277  398 qed  eberlm@66277  399 eberlm@68651  400 subsection%unimportant \Ignoring initial segments\  eberlm@68651  401 eberlm@66277  402 lemma convergent_prod_offset:  eberlm@66277  403  assumes "convergent_prod (\n. f (n + m))"  eberlm@66277  404  shows "convergent_prod f"  eberlm@66277  405 proof -  eberlm@66277  406  from assms obtain M L where "(\n. \k\n. f (k + (M + m))) \ L" "L \ 0"  lp15@68064  407  by (auto simp: prod_defs add.assoc)  lp15@68064  408  thus "convergent_prod f"  lp15@68064  409  unfolding prod_defs by blast  eberlm@66277  410 qed  eberlm@66277  411 eberlm@66277  412 lemma abs_convergent_prod_offset:  eberlm@66277  413  assumes "abs_convergent_prod (\n. f (n + m))"  eberlm@66277  414  shows "abs_convergent_prod f"  eberlm@66277  415  using assms unfolding abs_convergent_prod_def by (rule convergent_prod_offset)  eberlm@66277  416 lp15@68424  417 lp15@68361  418 lemma raw_has_prod_ignore_initial_segment:  lp15@68361  419  fixes f :: "nat \ 'a :: real_normed_field"  lp15@68361  420  assumes "raw_has_prod f M p" "N \ M"  lp15@68361  421  obtains q where "raw_has_prod f N q"  eberlm@66277  422 proof -  lp15@68361  423  have p: "(\n. \k\n. f (k + M)) \ p" and "p \ 0"  lp15@68361  424  using assms by (auto simp: raw_has_prod_def)  lp15@68361  425  then have nz: "\n. n \ M \ f n \ 0"  lp15@68361  426  using assms by (auto simp: raw_has_prod_eq_0)  lp15@68361  427  define C where "C = (\k 0"  eberlm@66277  429  by (auto simp: C_def)  eberlm@66277  430 lp15@68361  431  from p have "(\i. \k\i + (N-M). f (k + M)) \ p"  eberlm@66277  432  by (rule LIMSEQ_ignore_initial_segment)  lp15@68361  433  also have "(\i. \k\i + (N-M). f (k + M)) = (\n. C * (\k\n. f (k + N)))"  eberlm@66277  434  proof (rule ext, goal_cases)  eberlm@66277  435  case (1 n)  lp15@68361  436  have "{..n+(N-M)} = {..<(N-M)} \ {(N-M)..n+(N-M)}" by auto  lp15@68361  437  also have "(\k\\. f (k + M)) = C * (\k=(N-M)..n+(N-M). f (k + M))"  eberlm@66277  438  unfolding C_def by (rule prod.union_disjoint) auto  lp15@68361  439  also have "(\k=(N-M)..n+(N-M). f (k + M)) = (\k\n. f (k + (N-M) + M))"  lp15@68361  440  by (intro ext prod.reindex_bij_witness[of _ "\k. k + (N-M)" "\k. k - (N-M)"]) auto  lp15@68361  441  finally show ?case  lp15@68361  442  using \N \ M\ by (simp add: add_ac)  eberlm@66277  443  qed  lp15@68361  444  finally have "(\n. C * (\k\n. f (k + N)) / C) \ p / C"  eberlm@66277  445  by (intro tendsto_divide tendsto_const) auto  lp15@68361  446  hence "(\n. \k\n. f (k + N)) \ p / C" by simp  lp15@68361  447  moreover from \p \ 0\ have "p / C \ 0" by simp  lp15@68361  448  ultimately show ?thesis  lp15@68361  449  using raw_has_prod_def that by blast  eberlm@66277  450 qed  eberlm@66277  451 eberlm@68651  452 corollary%unimportant convergent_prod_ignore_initial_segment:  lp15@68361  453  fixes f :: "nat \ 'a :: real_normed_field"  lp15@68361  454  assumes "convergent_prod f"  lp15@68361  455  shows "convergent_prod (\n. f (n + m))"  lp15@68361  456  using assms  lp15@68361  457  unfolding convergent_prod_def  lp15@68361  458  apply clarify  lp15@68361  459  apply (erule_tac N="M+m" in raw_has_prod_ignore_initial_segment)  lp15@68361  460  apply (auto simp add: raw_has_prod_def add_ac)  lp15@68361  461  done  lp15@68361  462 eberlm@68651  463 corollary%unimportant convergent_prod_ignore_nonzero_segment:  lp15@68136  464  fixes f :: "nat \ 'a :: real_normed_field"  lp15@68136  465  assumes f: "convergent_prod f" and nz: "\i. i \ M \ f i \ 0"  lp15@68361  466  shows "\p. raw_has_prod f M p"  lp15@68136  467  using convergent_prod_ignore_initial_segment [OF f]  lp15@68136  468  by (metis convergent_LIMSEQ_iff convergent_prod_iff_convergent le_add_same_cancel2 nz prod_defs(1) zero_order(1))  lp15@68136  469 eberlm@68651  470 corollary%unimportant abs_convergent_prod_ignore_initial_segment:  eberlm@66277  471  assumes "abs_convergent_prod f"  eberlm@66277  472  shows "abs_convergent_prod (\n. f (n + m))"  eberlm@66277  473  using assms unfolding abs_convergent_prod_def  eberlm@66277  474  by (rule convergent_prod_ignore_initial_segment)  eberlm@66277  475 eberlm@68651  476 subsection\More elementary properties\  eberlm@68651  477 eberlm@68651  478 theorem abs_convergent_prod_imp_convergent_prod:  eberlm@66277  479  fixes f :: "nat \ 'a :: {real_normed_div_algebra,complete_space,comm_ring_1}"  eberlm@66277  480  assumes "abs_convergent_prod f"  eberlm@66277  481  shows "convergent_prod f"  eberlm@66277  482 proof -  eberlm@66277  483  from assms have "eventually (\n. f n \ 0) sequentially"  eberlm@66277  484  by (rule abs_convergent_prod_imp_ev_nonzero)  eberlm@66277  485  then obtain N where N: "f n \ 0" if "n \ N" for n  eberlm@66277  486  by (auto simp: eventually_at_top_linorder)  eberlm@66277  487  let ?P = "\n. \i\n. f (i + N)" and ?Q = "\n. \i\n. 1 + norm (f (i + N) - 1)"  eberlm@66277  488 eberlm@66277  489  have "Cauchy ?P"  eberlm@66277  490  proof (rule CauchyI', goal_cases)  eberlm@66277  491  case (1 \)  eberlm@66277  492  from assms have "abs_convergent_prod (\n. f (n + N))"  eberlm@66277  493  by (rule abs_convergent_prod_ignore_initial_segment)  eberlm@66277  494  hence "Cauchy ?Q"  eberlm@66277  495  unfolding abs_convergent_prod_def  eberlm@66277  496  by (intro convergent_Cauchy convergent_prod_imp_convergent)  eberlm@66277  497  from CauchyD[OF this 1] obtain M where M: "norm (?Q m - ?Q n) < \" if "m \ M" "n \ M" for m n  eberlm@66277  498  by blast  eberlm@66277  499  show ?case  eberlm@66277  500  proof (rule exI[of _ M], safe, goal_cases)  eberlm@66277  501  case (1 m n)  eberlm@66277  502  have "dist (?P m) (?P n) = norm (?P n - ?P m)"  eberlm@66277  503  by (simp add: dist_norm norm_minus_commute)  eberlm@66277  504  also from 1 have "{..n} = {..m} \ {m<..n}" by auto  eberlm@66277  505  hence "norm (?P n - ?P m) = norm (?P m * (\k\{m<..n}. f (k + N)) - ?P m)"  eberlm@66277  506  by (subst prod.union_disjoint [symmetric]) (auto simp: algebra_simps)  eberlm@66277  507  also have "\ = norm (?P m * ((\k\{m<..n}. f (k + N)) - 1))"  eberlm@66277  508  by (simp add: algebra_simps)  eberlm@66277  509  also have "\ = (\k\m. norm (f (k + N))) * norm ((\k\{m<..n}. f (k + N)) - 1)"  eberlm@66277  510  by (simp add: norm_mult prod_norm)  eberlm@66277  511  also have "\ \ ?Q m * ((\k\{m<..n}. 1 + norm (f (k + N) - 1)) - 1)"  eberlm@66277  512  using norm_prod_minus1_le_prod_minus1[of "\k. f (k + N) - 1" "{m<..n}"]  eberlm@66277  513  norm_triangle_ineq[of 1 "f k - 1" for k]  eberlm@66277  514  by (intro mult_mono prod_mono ballI conjI norm_prod_minus1_le_prod_minus1 prod_nonneg) auto  eberlm@66277  515  also have "\ = ?Q m * (\k\{m<..n}. 1 + norm (f (k + N) - 1)) - ?Q m"  eberlm@66277  516  by (simp add: algebra_simps)  eberlm@66277  517  also have "?Q m * (\k\{m<..n}. 1 + norm (f (k + N) - 1)) =  eberlm@66277  518  (\k\{..m}\{m<..n}. 1 + norm (f (k + N) - 1))"  eberlm@66277  519  by (rule prod.union_disjoint [symmetric]) auto  eberlm@66277  520  also from 1 have "{..m}\{m<..n} = {..n}" by auto  eberlm@66277  521  also have "?Q n - ?Q m \ norm (?Q n - ?Q m)" by simp  eberlm@66277  522  also from 1 have "\ < \" by (intro M) auto  eberlm@66277  523  finally show ?case .  eberlm@66277  524  qed  eberlm@66277  525  qed  eberlm@66277  526  hence conv: "convergent ?P" by (rule Cauchy_convergent)  eberlm@66277  527  then obtain L where L: "?P \ L"  eberlm@66277  528  by (auto simp: convergent_def)  eberlm@66277  529 eberlm@66277  530  have "L \ 0"  eberlm@66277  531  proof  eberlm@66277  532  assume [simp]: "L = 0"  eberlm@66277  533  from tendsto_norm[OF L] have limit: "(\n. \k\n. norm (f (k + N))) \ 0"  eberlm@66277  534  by (simp add: prod_norm)  eberlm@66277  535 eberlm@66277  536  from assms have "(\n. f (n + N)) \ 1"  eberlm@66277  537  by (intro abs_convergent_prod_imp_LIMSEQ abs_convergent_prod_ignore_initial_segment)  eberlm@66277  538  hence "eventually (\n. norm (f (n + N) - 1) < 1) sequentially"  eberlm@66277  539  by (auto simp: tendsto_iff dist_norm)  eberlm@66277  540  then obtain M0 where M0: "norm (f (n + N) - 1) < 1" if "n \ M0" for n  eberlm@66277  541  by (auto simp: eventually_at_top_linorder)  eberlm@66277  542 eberlm@66277  543  {  eberlm@66277  544  fix M assume M: "M \ M0"  eberlm@66277  545  with M0 have M: "norm (f (n + N) - 1) < 1" if "n \ M" for n using that by simp  eberlm@66277  546 eberlm@66277  547  have "(\n. \k\n. 1 - norm (f (k+M+N) - 1)) \ 0"  eberlm@66277  548  proof (rule tendsto_sandwich)  eberlm@66277  549  show "eventually (\n. (\k\n. 1 - norm (f (k+M+N) - 1)) \ 0) sequentially"  eberlm@66277  550  using M by (intro always_eventually prod_nonneg allI ballI) (auto intro: less_imp_le)  eberlm@66277  551  have "norm (1::'a) - norm (f (i + M + N) - 1) \ norm (f (i + M + N))" for i  eberlm@66277  552  using norm_triangle_ineq3[of "f (i + M + N)" 1] by simp  eberlm@66277  553  thus "eventually (\n. (\k\n. 1 - norm (f (k+M+N) - 1)) \ (\k\n. norm (f (k+M+N)))) at_top"  eberlm@66277  554  using M by (intro always_eventually allI prod_mono ballI conjI) (auto intro: less_imp_le)  eberlm@66277  555   eberlm@66277  556  define C where "C = (\k 0" by (auto simp: C_def)  eberlm@66277  558  from L have "(\n. norm (\k\n+M. f (k + N))) \ 0"  eberlm@66277  559  by (intro LIMSEQ_ignore_initial_segment) (simp add: tendsto_norm_zero_iff)  eberlm@66277  560  also have "(\n. norm (\k\n+M. f (k + N))) = (\n. C * (\k\n. norm (f (k + M + N))))"  eberlm@66277  561  proof (rule ext, goal_cases)  eberlm@66277  562  case (1 n)  eberlm@66277  563  have "{..n+M} = {.. {M..n+M}" by auto  eberlm@66277  564  also have "norm (\k\\. f (k + N)) = C * norm (\k=M..n+M. f (k + N))"  eberlm@66277  565  unfolding C_def by (subst prod.union_disjoint) (auto simp: norm_mult prod_norm)  eberlm@66277  566  also have "(\k=M..n+M. f (k + N)) = (\k\n. f (k + N + M))"  eberlm@66277  567  by (intro prod.reindex_bij_witness[of _ "\i. i + M" "\i. i - M"]) auto  eberlm@66277  568  finally show ?case by (simp add: add_ac prod_norm)  eberlm@66277  569  qed  eberlm@66277  570  finally have "(\n. C * (\k\n. norm (f (k + M + N))) / C) \ 0 / C"  eberlm@66277  571  by (intro tendsto_divide tendsto_const) auto  eberlm@66277  572  thus "(\n. \k\n. norm (f (k + M + N))) \ 0" by simp  eberlm@66277  573  qed simp_all  eberlm@66277  574 eberlm@66277  575  have "1 - (\i. norm (f (i + M + N) - 1)) \ 0"  eberlm@66277  576  proof (rule tendsto_le)  eberlm@66277  577  show "eventually (\n. 1 - (\k\n. norm (f (k+M+N) - 1)) \  eberlm@66277  578  (\k\n. 1 - norm (f (k+M+N) - 1))) at_top"  nipkow@69529  579  using M by (intro always_eventually allI Weierstrass_prod_ineq) (auto intro: less_imp_le)  eberlm@66277  580  show "(\n. \k\n. 1 - norm (f (k+M+N) - 1)) \ 0" by fact  eberlm@66277  581  show "(\n. 1 - (\k\n. norm (f (k + M + N) - 1)))  eberlm@66277  582  \ 1 - (\i. norm (f (i + M + N) - 1))"  eberlm@66277  583  by (intro tendsto_intros summable_LIMSEQ' summable_ignore_initial_segment  eberlm@66277  584  abs_convergent_prod_imp_summable assms)  eberlm@66277  585  qed simp_all  eberlm@66277  586  hence "(\i. norm (f (i + M + N) - 1)) \ 1" by simp  eberlm@66277  587  also have "\ + (\ii. norm (f (i + N) - 1))"  eberlm@66277  588  by (intro suminf_split_initial_segment [symmetric] summable_ignore_initial_segment  eberlm@66277  589  abs_convergent_prod_imp_summable assms)  eberlm@66277  590  finally have "1 + (\i (\i. norm (f (i + N) - 1))" by simp  eberlm@66277  591  } note * = this  eberlm@66277  592 eberlm@66277  593  have "1 + (\i. norm (f (i + N) - 1)) \ (\i. norm (f (i + N) - 1))"  eberlm@66277  594  proof (rule tendsto_le)  eberlm@66277  595  show "(\M. 1 + (\i 1 + (\i. norm (f (i + N) - 1))"  eberlm@66277  596  by (intro tendsto_intros summable_LIMSEQ summable_ignore_initial_segment  eberlm@66277  597  abs_convergent_prod_imp_summable assms)  eberlm@66277  598  show "eventually (\M. 1 + (\i (\i. norm (f (i + N) - 1))) at_top"  eberlm@66277  599  using eventually_ge_at_top[of M0] by eventually_elim (use * in auto)  eberlm@66277  600  qed simp_all  eberlm@66277  601  thus False by simp  eberlm@66277  602  qed  lp15@68064  603  with L show ?thesis by (auto simp: prod_defs)  lp15@68064  604 qed  lp15@68064  605 lp15@68361  606 lemma raw_has_prod_cases:  lp15@68064  607  fixes f :: "nat \ 'a :: {idom,topological_semigroup_mult,t2_space}"  lp15@68361  608  assumes "raw_has_prod f M p"  lp15@68361  609  obtains i where "in. \i\n. f (i + M)) \ p" "p \ 0"  lp15@68361  612  using assms unfolding raw_has_prod_def by blast+  lp15@68064  613  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  616  proof -  lp15@68064  617  have "{..n+M} = {.. {M..n+M}"  lp15@68064  618  by auto  lp15@68064  619  then have "prod f {..n+M} = prod f {.. = prod f {..i\n. f (i + M))"  lp15@68064  622  by (metis (mono_tags, lifting) add.left_neutral atMost_atLeast0 prod_shift_bounds_cl_nat_ivl)  lp15@68064  623  finally show ?thesis by metis  lp15@68064  624  qed  lp15@68064  625  ultimately have "(\n. prod f {..n}) \ prod f {..i 0"  lp15@68361  628  using \p \ 0\ assms that by (auto simp: raw_has_prod_def)  lp15@68136  629  then show thesis  lp15@68136  630  using that by blast  lp15@68064  631 qed  lp15@68064  632 lp15@68136  633 corollary convergent_prod_offset_0:  lp15@68136  634  fixes f :: "nat \ 'a :: {idom,topological_semigroup_mult,t2_space}"  lp15@68136  635  assumes "convergent_prod f" "\i. f i \ 0"  lp15@68361  636  shows "\p. raw_has_prod f 0 p"  lp15@68361  637  using assms convergent_prod_def raw_has_prod_cases by blast  lp15@68136  638 lp15@68064  639 lemma prodinf_eq_lim:  lp15@68064  640  fixes f :: "nat \ 'a :: {idom,topological_semigroup_mult,t2_space}"  lp15@68064  641  assumes "convergent_prod f" "\i. f i \ 0"  lp15@68064  642  shows "prodinf f = lim (\n. \i\n. f i)"  lp15@68064  643  using assms convergent_prod_offset_0 [OF assms]  lp15@68064  644  by (simp add: prod_defs lim_def) (metis (no_types) assms(1) convergent_prod_to_zero_iff)  lp15@68064  645 lp15@68064  646 lemma has_prod_one[simp, intro]: "(\n. 1) has_prod 1"  lp15@68064  647  unfolding prod_defs by auto  lp15@68064  648 lp15@68064  649 lemma convergent_prod_one[simp, intro]: "convergent_prod (\n. 1)"  lp15@68064  650  unfolding prod_defs by auto  lp15@68064  651 lp15@68064  652 lemma prodinf_cong: "(\n. f n = g n) \ prodinf f = prodinf g"  lp15@68064  653  by presburger  lp15@68064  654 lp15@68064  655 lemma convergent_prod_cong:  lp15@68064  656  fixes f g :: "nat \ 'a::{field,topological_semigroup_mult,t2_space}"  lp15@68064  657  assumes ev: "eventually (\x. f x = g x) sequentially" and f: "\i. f i \ 0" and g: "\i. g i \ 0"  lp15@68064  658  shows "convergent_prod f = convergent_prod g"  lp15@68064  659 proof -  lp15@68064  660  from assms obtain N where N: "\n\N. f n = g n"  lp15@68064  661  by (auto simp: eventually_at_top_linorder)  lp15@68064  662  define C where "C = (\k 0"  lp15@68064  664  by (simp add: f)  lp15@68064  665  have *: "eventually (\n. prod f {..n} = C * prod g {..n}) sequentially"  lp15@68064  666  using eventually_ge_at_top[of N]  lp15@68064  667  proof eventually_elim  lp15@68064  668  case (elim n)  lp15@68064  669  then have "{..n} = {.. {N..n}"  lp15@68064  670  by auto  lp15@68138  671  also have "prod f \ = prod f {.. {N..n})"  lp15@68064  678  by (intro prod.union_disjoint [symmetric]) auto  lp15@68064  679  also from elim have "{.. {N..n} = {..n}"  lp15@68064  680  by auto  lp15@68064  681  finally show "prod f {..n} = C * prod g {..n}" .  lp15@68064  682  qed  lp15@68064  683  then have cong: "convergent (\n. prod f {..n}) = convergent (\n. C * prod g {..n})"  lp15@68064  684  by (rule convergent_cong)  lp15@68064  685  show ?thesis  lp15@68064  686  proof  lp15@68064  687  assume cf: "convergent_prod f"  lp15@68064  688  then have "\ (\n. prod g {..n}) \ 0"  lp15@68064  689  using tendsto_mult_left * convergent_prod_to_zero_iff f filterlim_cong by fastforce  lp15@68064  690  then show "convergent_prod g"  lp15@68064  691  by (metis convergent_mult_const_iff \C \ 0\ cong cf convergent_LIMSEQ_iff convergent_prod_iff_convergent convergent_prod_imp_convergent g)  lp15@68064  692  next  lp15@68064  693  assume cg: "convergent_prod g"  lp15@68064  694  have "\a. C * a \ 0 \ (\n. prod g {..n}) \ a"  lp15@68064  695  by (metis (no_types) \C \ 0\ cg convergent_prod_iff_nz_lim divide_eq_0_iff g nonzero_mult_div_cancel_right)  lp15@68064  696  then show "convergent_prod f"  lp15@68064  697  using "*" tendsto_mult_left filterlim_cong  lp15@68064  698  by (fastforce simp add: convergent_prod_iff_nz_lim f)  lp15@68064  699  qed  eberlm@66277  700 qed  eberlm@66277  701 lp15@68071  702 lemma has_prod_finite:  lp15@68361  703  fixes f :: "nat \ 'a::{semidom,t2_space}"  lp15@68071  704  assumes [simp]: "finite N"  lp15@68071  705  and f: "\n. n \ N \ f n = 1"  lp15@68071  706  shows "f has_prod (\n\N. f n)"  lp15@68071  707 proof -  lp15@68071  708  have eq: "prod f {..n + Suc (Max N)} = prod f N" for n  lp15@68071  709  proof (rule prod.mono_neutral_right)  lp15@68071  710  show "N \ {..n + Suc (Max N)}"  lp15@68138  711  by (auto simp: le_Suc_eq trans_le_add2)  lp15@68071  712  show "\i\{..n + Suc (Max N)} - N. f i = 1"  lp15@68071  713  using f by blast  lp15@68071  714  qed auto  lp15@68071  715  show ?thesis  lp15@68071  716  proof (cases "\n\N. f n \ 0")  lp15@68071  717  case True  lp15@68071  718  then have "prod f N \ 0"  lp15@68071  719  by simp  lp15@68071  720  moreover have "(\n. prod f {..n}) \ prod f N"  lp15@68071  721  by (rule LIMSEQ_offset[of _ "Suc (Max N)"]) (simp add: eq atLeast0LessThan del: add_Suc_right)  lp15@68071  722  ultimately show ?thesis  lp15@68361  723  by (simp add: raw_has_prod_def has_prod_def)  lp15@68071  724  next  lp15@68071  725  case False  lp15@68071  726  then obtain k where "k \ N" "f k = 0"  lp15@68071  727  by auto  lp15@68071  728  let ?Z = "{n \ N. f n = 0}"  lp15@68071  729  have maxge: "Max ?Z \ n" if "f n = 0" for n  lp15@68071  730  using Max_ge [of ?Z] \finite N\ \f n = 0\  lp15@68071  731  by (metis (mono_tags) Collect_mem_eq f finite_Collect_conjI mem_Collect_eq zero_neq_one)  lp15@68071  732  let ?q = "prod f {Suc (Max ?Z)..Max N}"  lp15@68071  733  have [simp]: "?q \ 0"  lp15@68071  734  using maxge Suc_n_not_le_n le_trans by force  lp15@68076  735  have eq: "(\i\n + Max N. f (Suc (i + Max ?Z))) = ?q" for n  lp15@68076  736  proof -  lp15@68076  737  have "(\i\n + Max N. f (Suc (i + Max ?Z))) = prod f {Suc (Max ?Z)..n + Max N + Suc (Max ?Z)}"  lp15@68076  738  proof (rule prod.reindex_cong [where l = "\i. i + Suc (Max ?Z)", THEN sym])  lp15@68076  739  show "{Suc (Max ?Z)..n + Max N + Suc (Max ?Z)} = (\i. i + Suc (Max ?Z))  {..n + Max N}"  lp15@68076  740  using le_Suc_ex by fastforce  lp15@68076  741  qed (auto simp: inj_on_def)  lp15@68138  742  also have "\ = ?q"  lp15@68076  743  by (rule prod.mono_neutral_right)  lp15@68076  744  (use Max.coboundedI [OF \finite N\] f in \force+\)  lp15@68076  745  finally show ?thesis .  lp15@68076  746  qed  lp15@68361  747  have q: "raw_has_prod f (Suc (Max ?Z)) ?q"  lp15@68361  748  proof (simp add: raw_has_prod_def)  lp15@68076  749  show "(\n. \i\n. f (Suc (i + Max ?Z))) \ ?q"  lp15@68076  750  by (rule LIMSEQ_offset[of _ "(Max N)"]) (simp add: eq)  lp15@68076  751  qed  lp15@68071  752  show ?thesis  lp15@68071  753  unfolding has_prod_def  lp15@68071  754  proof (intro disjI2 exI conjI)  lp15@68071  755  show "prod f N = 0"  lp15@68071  756  using \f k = 0\ \k \ N\ \finite N\ prod_zero by blast  lp15@68071  757  show "f (Max ?Z) = 0"  lp15@68071  758  using Max_in [of ?Z] \finite N\ \f k = 0\ \k \ N\ by auto  lp15@68071  759  qed (use q in auto)  lp15@68071  760  qed  lp15@68071  761 qed  lp15@68071  762 eberlm@68651  763 corollary%unimportant has_prod_0:  lp15@68361  764  fixes f :: "nat \ 'a::{semidom,t2_space}"  lp15@68071  765  assumes "\n. f n = 1"  lp15@68071  766  shows "f has_prod 1"  lp15@68071  767  by (simp add: assms has_prod_cong)  lp15@68071  768 lp15@68361  769 lemma prodinf_zero[simp]: "prodinf (\n. 1::'a::real_normed_field) = 1"  lp15@68361  770  using has_prod_unique by force  lp15@68361  771 lp15@68071  772 lemma convergent_prod_finite:  lp15@68071  773  fixes f :: "nat \ 'a::{idom,t2_space}"  lp15@68071  774  assumes "finite N" "\n. n \ N \ f n = 1"  lp15@68071  775  shows "convergent_prod f"  lp15@68071  776 proof -  lp15@68361  777  have "\n p. raw_has_prod f n p"  lp15@68071  778  using assms has_prod_def has_prod_finite by blast  lp15@68071  779  then show ?thesis  lp15@68071  780  by (simp add: convergent_prod_def)  lp15@68071  781 qed  lp15@68071  782 lp15@68127  783 lemma has_prod_If_finite_set:  lp15@68127  784  fixes f :: "nat \ 'a::{idom,t2_space}"  lp15@68127  785  shows "finite A \ (\r. if r \ A then f r else 1) has_prod (\r\A. f r)"  lp15@68127  786  using has_prod_finite[of A "(\r. if r \ A then f r else 1)"]  lp15@68127  787  by simp  lp15@68127  788 lp15@68127  789 lemma has_prod_If_finite:  lp15@68127  790  fixes f :: "nat \ 'a::{idom,t2_space}"  lp15@68127  791  shows "finite {r. P r} \ (\r. if P r then f r else 1) has_prod (\r | P r. f r)"  lp15@68127  792  using has_prod_If_finite_set[of "{r. P r}"] by simp  lp15@68127  793 lp15@68127  794 lemma convergent_prod_If_finite_set[simp, intro]:  lp15@68127  795  fixes f :: "nat \ 'a::{idom,t2_space}"  lp15@68127  796  shows "finite A \ convergent_prod (\r. if r \ A then f r else 1)"  lp15@68127  797  by (simp add: convergent_prod_finite)  lp15@68127  798 lp15@68127  799 lemma convergent_prod_If_finite[simp, intro]:  lp15@68127  800  fixes f :: "nat \ 'a::{idom,t2_space}"  lp15@68127  801  shows "finite {r. P r} \ convergent_prod (\r. if P r then f r else 1)"  lp15@68127  802  using convergent_prod_def has_prod_If_finite has_prod_def by fastforce  lp15@68127  803 lp15@68127  804 lemma has_prod_single:  lp15@68127  805  fixes f :: "nat \ 'a::{idom,t2_space}"  lp15@68127  806  shows "(\r. if r = i then f r else 1) has_prod f i"  lp15@68127  807  using has_prod_If_finite[of "\r. r = i"] by simp  lp15@68127  808 lp15@68136  809 context  lp15@68136  810  fixes f :: "nat \ 'a :: real_normed_field"  lp15@68136  811 begin  lp15@68136  812 lp15@68136  813 lemma convergent_prod_imp_has_prod:  lp15@68136  814  assumes "convergent_prod f"  lp15@68136  815  shows "\p. f has_prod p"  lp15@68136  816 proof -  lp15@68361  817  obtain M p where p: "raw_has_prod f M p"  lp15@68136  818  using assms convergent_prod_def by blast  lp15@68136  819  then have "p \ 0"  lp15@68361  820  using raw_has_prod_nonzero by blast  lp15@68136  821  with p have fnz: "f i \ 0" if "i \ M" for i  lp15@68361  822  using raw_has_prod_eq_0 that by blast  lp15@68136  823  define C where "C = (\nn\M. f n \ 0")  lp15@68136  826  case True  lp15@68136  827  then have "C \ 0"  lp15@68136  828  by (simp add: C_def)  lp15@68136  829  then show ?thesis  lp15@68136  830  by (meson True assms convergent_prod_offset_0 fnz has_prod_def nat_le_linear)  lp15@68136  831  next  lp15@68136  832  case False  lp15@68136  833  let ?N = "GREATEST n. f n = 0"  lp15@68136  834  have 0: "f ?N = 0"  lp15@68136  835  using fnz False  lp15@68136  836  by (metis (mono_tags, lifting) GreatestI_ex_nat nat_le_linear)  lp15@68136  837  have "f i \ 0" if "i > ?N" for i  lp15@68136  838  by (metis (mono_tags, lifting) Greatest_le_nat fnz leD linear that)  lp15@68361  839  then have "\p. raw_has_prod f (Suc ?N) p"  lp15@68136  840  using assms by (auto simp: intro!: convergent_prod_ignore_nonzero_segment)  lp15@68136  841  then show ?thesis  lp15@68136  842  unfolding has_prod_def using 0 by blast  lp15@68136  843  qed  lp15@68136  844 qed  lp15@68136  845 lp15@68136  846 lemma convergent_prod_has_prod [intro]:  lp15@68136  847  shows "convergent_prod f \ f has_prod (prodinf f)"  lp15@68136  848  unfolding prodinf_def  lp15@68136  849  by (metis convergent_prod_imp_has_prod has_prod_unique theI')  lp15@68136  850 lp15@68136  851 lemma convergent_prod_LIMSEQ:  lp15@68136  852  shows "convergent_prod f \ (\n. \i\n. f i) \ prodinf f"  lp15@68136  853  by (metis convergent_LIMSEQ_iff convergent_prod_has_prod convergent_prod_imp_convergent  lp15@68361  854  convergent_prod_to_zero_iff raw_has_prod_eq_0 has_prod_def prodinf_eq_lim zero_le)  lp15@68136  855 eberlm@68651  856 theorem has_prod_iff: "f has_prod x \ convergent_prod f \ prodinf f = x"  lp15@68136  857 proof  lp15@68136  858  assume "f has_prod x"  lp15@68136  859  then show "convergent_prod f \ prodinf f = x"  lp15@68136  860  apply safe  lp15@68136  861  using convergent_prod_def has_prod_def apply blast  lp15@68136  862  using has_prod_unique by blast  lp15@68136  863 qed auto  lp15@68136  864 lp15@68136  865 lemma convergent_prod_has_prod_iff: "convergent_prod f \ f has_prod prodinf f"  lp15@68136  866  by (auto simp: has_prod_iff convergent_prod_has_prod)  lp15@68136  867 lp15@68136  868 lemma prodinf_finite:  lp15@68136  869  assumes N: "finite N"  lp15@68136  870  and f: "\n. n \ N \ f n = 1"  lp15@68136  871  shows "prodinf f = (\n\N. f n)"  lp15@68136  872  using has_prod_finite[OF assms, THEN has_prod_unique] by simp  lp15@68127  873 eberlm@66277  874 end  lp15@68136  875 eberlm@68651  876 subsection%unimportant \Infinite products on ordered topological monoids\  lp15@68361  877 lp15@68361  878 lemma LIMSEQ_prod_0:  lp15@68361  879  fixes f :: "nat \ 'a::{semidom,topological_space}"  lp15@68361  880  assumes "f i = 0"  lp15@68361  881  shows "(\n. prod f {..n}) \ 0"  lp15@68361  882 proof (subst tendsto_cong)  lp15@68361  883  show "\\<^sub>F n in sequentially. prod f {..n} = 0"  lp15@68361  884  proof  lp15@68361  885  show "prod f {..n} = 0" if "n \ i" for n  lp15@68361  886  using that assms by auto  lp15@68361  887  qed  lp15@68361  888 qed auto  lp15@68361  889 lp15@68361  890 lemma LIMSEQ_prod_nonneg:  lp15@68361  891  fixes f :: "nat \ 'a::{linordered_semidom,linorder_topology}"  lp15@68361  892  assumes 0: "\n. 0 \ f n" and a: "(\n. prod f {..n}) \ a"  lp15@68361  893  shows "a \ 0"  lp15@68361  894  by (simp add: "0" prod_nonneg LIMSEQ_le_const [OF a])  lp15@68361  895 lp15@68361  896 lp15@68361  897 context  lp15@68361  898  fixes f :: "nat \ 'a::{linordered_semidom,linorder_topology}"  lp15@68361  899 begin  lp15@68361  900 lp15@68361  901 lemma has_prod_le:  lp15@68361  902  assumes f: "f has_prod a" and g: "g has_prod b" and le: "\n. 0 \ f n \ f n \ g n"  lp15@68361  903  shows "a \ b"  lp15@68361  904 proof (cases "a=0 \ b=0")  lp15@68361  905  case True  lp15@68361  906  then show ?thesis  lp15@68361  907  proof  lp15@68361  908  assume [simp]: "a=0"  lp15@68361  909  have "b \ 0"  lp15@68361  910  proof (rule LIMSEQ_prod_nonneg)  lp15@68361  911  show "(\n. prod g {..n}) \ b"  lp15@68361  912  using g by (auto simp: has_prod_def raw_has_prod_def LIMSEQ_prod_0)  lp15@68361  913  qed (use le order_trans in auto)  lp15@68361  914  then show ?thesis  lp15@68361  915  by auto  lp15@68361  916  next  lp15@68361  917  assume [simp]: "b=0"  lp15@68361  918  then obtain i where "g i = 0"  lp15@68361  919  using g by (auto simp: prod_defs)  lp15@68361  920  then have "f i = 0"  lp15@68361  921  using antisym le by force  lp15@68361  922  then have "a=0"  lp15@68361  923  using f by (auto simp: prod_defs LIMSEQ_prod_0 LIMSEQ_unique)  lp15@68361  924  then show ?thesis  lp15@68361  925  by auto  lp15@68361  926  qed  lp15@68361  927 next  lp15@68361  928  case False  lp15@68361  929  then show ?thesis  lp15@68361  930  using assms  lp15@68361  931  unfolding has_prod_def raw_has_prod_def  lp15@68361  932  by (force simp: LIMSEQ_prod_0 intro!: LIMSEQ_le prod_mono)  lp15@68361  933 qed  lp15@68361  934 lp15@68361  935 lemma prodinf_le:  lp15@68361  936  assumes f: "f has_prod a" and g: "g has_prod b" and le: "\n. 0 \ f n \ f n \ g n"  lp15@68361  937  shows "prodinf f \ prodinf g"  lp15@68361  938  using has_prod_le [OF assms] has_prod_unique f g by blast  lp15@68361  939 lp15@68136  940 end  lp15@68361  941 lp15@68361  942 lp15@68361  943 lemma prod_le_prodinf:  lp15@68361  944  fixes f :: "nat \ 'a::{linordered_idom,linorder_topology}"  lp15@68361  945  assumes "f has_prod a" "\i. 0 \ f i" "\i. i\n \ 1 \ f i"  lp15@68361  946  shows "prod f {.. prodinf f"  lp15@68361  947  by(rule has_prod_le[OF has_prod_If_finite_set]) (use assms has_prod_unique in auto)  lp15@68361  948 lp15@68361  949 lemma prodinf_nonneg:  lp15@68361  950  fixes f :: "nat \ 'a::{linordered_idom,linorder_topology}"  lp15@68361  951  assumes "f has_prod a" "\i. 1 \ f i"  lp15@68361  952  shows "1 \ prodinf f"  lp15@68361  953  using prod_le_prodinf[of f a 0] assms  lp15@68361  954  by (metis order_trans prod_ge_1 zero_le_one)  lp15@68361  955 lp15@68361  956 lemma prodinf_le_const:  lp15@68361  957  fixes f :: "nat \ real"  lp15@68361  958  assumes "convergent_prod f" "\n. prod f {.. x"  lp15@68361  959  shows "prodinf f \ x"  lp15@68361  960  by (metis lessThan_Suc_atMost assms convergent_prod_LIMSEQ LIMSEQ_le_const2)  lp15@68361  961 lp15@68361  962 lemma prodinf_eq_one_iff:  lp15@68361  963  fixes f :: "nat \ real"  lp15@68361  964  assumes f: "convergent_prod f" and ge1: "\n. 1 \ f n"  lp15@68361  965  shows "prodinf f = 1 \ (\n. f n = 1)"  lp15@68361  966 proof  lp15@68361  967  assume "prodinf f = 1"  lp15@68361  968  then have "(\n. \i 1"  lp15@68361  969  using convergent_prod_LIMSEQ[of f] assms by (simp add: LIMSEQ_lessThan_iff_atMost)  lp15@68361  970  then have "\i. (\n\{i}. f n) \ 1"  lp15@68361  971  proof (rule LIMSEQ_le_const)  lp15@68361  972  have "1 \ prod f n" for n  lp15@68361  973  by (simp add: ge1 prod_ge_1)  lp15@68361  974  have "prod f {..\n. 1 \ prod f n\ \prodinf f = 1\ antisym f convergent_prod_has_prod ge1 order_trans prod_le_prodinf zero_le_one)  lp15@68361  976  then have "(\n\{i}. f n) \ prod f {.. Suc i" for i n  lp15@68361  977  by (metis mult.left_neutral order_refl prod.cong prod.neutral_const prod_lessThan_Suc)  lp15@68361  978  then show "\N. \n\N. (\n\{i}. f n) \ prod f {..n. f n = 1"  lp15@68361  982  by (auto intro!: antisym)  lp15@68361  983 qed (metis prodinf_zero fun_eq_iff)  lp15@68361  984 lp15@68361  985 lemma prodinf_pos_iff:  lp15@68361  986  fixes f :: "nat \ real"  lp15@68361  987  assumes "convergent_prod f" "\n. 1 \ f n"  lp15@68361  988  shows "1 < prodinf f \ (\i. 1 < f i)"  lp15@68361  989  using prod_le_prodinf[of f 1] prodinf_eq_one_iff  lp15@68361  990  by (metis convergent_prod_has_prod assms less_le prodinf_nonneg)  lp15@68361  991 lp15@68361  992 lemma less_1_prodinf2:  lp15@68361  993  fixes f :: "nat \ real"  lp15@68361  994  assumes "convergent_prod f" "\n. 1 \ f n" "1 < f i"  lp15@68361  995  shows "1 < prodinf f"  lp15@68361  996 proof -  lp15@68361  997  have "1 < (\n \ prodinf f"  lp15@68361  1000  by (intro prod_le_prodinf) (use assms order_trans zero_le_one in \blast+\)  lp15@68361  1001  finally show ?thesis .  lp15@68361  1002 qed  lp15@68361  1003 lp15@68361  1004 lemma less_1_prodinf:  lp15@68361  1005  fixes f :: "nat \ real"  lp15@68361  1006  shows "\convergent_prod f; \n. 1 < f n\ \ 1 < prodinf f"  lp15@68361  1007  by (intro less_1_prodinf2[where i=1]) (auto intro: less_imp_le)  lp15@68361  1008 lp15@68361  1009 lemma prodinf_nonzero:  lp15@68361  1010  fixes f :: "nat \ 'a :: {idom,topological_semigroup_mult,t2_space}"  lp15@68361  1011  assumes "convergent_prod f" "\i. f i \ 0"  lp15@68361  1012  shows "prodinf f \ 0"  lp15@68361  1013  by (metis assms convergent_prod_offset_0 has_prod_unique raw_has_prod_def has_prod_def)  lp15@68361  1014 lp15@68361  1015 lemma less_0_prodinf:  lp15@68361  1016  fixes f :: "nat \ real"  lp15@68361  1017  assumes f: "convergent_prod f" and 0: "\i. f i > 0"  lp15@68361  1018  shows "0 < prodinf f"  lp15@68361  1019 proof -  lp15@68361  1020  have "prodinf f \ 0"  lp15@68361  1021  by (metis assms less_irrefl prodinf_nonzero)  lp15@68361  1022  moreover have "0 < (\n 0"  lp15@68361  1025  using convergent_prod_LIMSEQ [OF f] LIMSEQ_prod_nonneg 0 less_le by blast  lp15@68361  1026  ultimately show ?thesis  lp15@68361  1027  by auto  lp15@68361  1028 qed  lp15@68361  1029 lp15@68361  1030 lemma prod_less_prodinf2:  lp15@68361  1031  fixes f :: "nat \ real"  lp15@68361  1032  assumes f: "convergent_prod f" and 1: "\m. m\n \ 1 \ f m" and 0: "\m. 0 < f m" and i: "n \ i" "1 < f i"  lp15@68361  1033  shows "prod f {.. prod f {.. prodinf f"  lp15@68361  1041  using prod_le_prodinf[of f _ "Suc i"]  lp15@68361  1042  by (meson "0" "1" Suc_leD convergent_prod_has_prod f \n \ i\ le_trans less_eq_real_def)  lp15@68361  1043  ultimately show ?thesis  lp15@68361  1044  by (metis le_less_trans mult.commute not_le prod_lessThan_Suc)  lp15@68361  1045 qed  lp15@68361  1046 lp15@68361  1047 lemma prod_less_prodinf:  lp15@68361  1048  fixes f :: "nat \ real"  lp15@68361  1049  assumes f: "convergent_prod f" and 1: "\m. m\n \ 1 < f m" and 0: "\m. 0 < f m"  lp15@68361  1050  shows "prod f {.. real"  lp15@68361  1055  assumes pos: "\n. 1 \ f n"  lp15@68361  1056  and le: "\n. (\i x"  lp15@68361  1057  shows "\p. raw_has_prod f 0 p"  lp15@68361  1058  unfolding raw_has_prod_def add_0_right  lp15@68361  1059 proof (rule exI LIMSEQ_incseq_SUP conjI)+  lp15@68361  1060  show "bdd_above (range (\n. prod f {..n}))"  lp15@68361  1061  by (metis bdd_aboveI2 le lessThan_Suc_atMost)  lp15@68361  1062  then have "(SUP i. prod f {..i}) > 0"  lp15@68361  1063  by (metis UNIV_I cSUP_upper less_le_trans pos prod_pos zero_less_one)  lp15@68361  1064  then show "(SUP i. prod f {..i}) \ 0"  lp15@68361  1065  by auto  lp15@68361  1066  show "incseq (\n. prod f {..n})"  lp15@68361  1067  using pos order_trans [OF zero_le_one] by (auto simp: mono_def intro!: prod_mono2)  lp15@68361  1068 qed  lp15@68361  1069 lp15@68361  1070 lemma convergent_prodI_nonneg_bounded:  lp15@68361  1071  fixes f :: "nat \ real"  lp15@68361  1072  assumes "\n. 1 \ f n" "\n. (\i x"  lp15@68361  1073  shows "convergent_prod f"  lp15@68361  1074  using convergent_prod_def raw_has_prodI_bounded [OF assms] by blast  lp15@68361  1075 lp15@68361  1076 eberlm@68651  1077 subsection%unimportant \Infinite products on topological spaces\  lp15@68361  1078 lp15@68361  1079 context  lp15@68361  1080  fixes f g :: "nat \ 'a::{t2_space,topological_semigroup_mult,idom}"  lp15@68361  1081 begin  lp15@68361  1082 lp15@68361  1083 lemma raw_has_prod_mult: "\raw_has_prod f M a; raw_has_prod g M b\ \ raw_has_prod (\n. f n * g n) M (a * b)"  lp15@68361  1084  by (force simp add: prod.distrib tendsto_mult raw_has_prod_def)  lp15@68361  1085 lp15@68361  1086 lemma has_prod_mult_nz: "\f has_prod a; g has_prod b; a \ 0; b \ 0\ \ (\n. f n * g n) has_prod (a * b)"  lp15@68361  1087  by (simp add: raw_has_prod_mult has_prod_def)  lp15@68361  1088 lp15@68361  1089 end  lp15@68361  1090 lp15@68361  1091 lp15@68361  1092 context  lp15@68361  1093  fixes f g :: "nat \ 'a::real_normed_field"  lp15@68361  1094 begin  lp15@68361  1095 lp15@68361  1096 lemma has_prod_mult:  lp15@68361  1097  assumes f: "f has_prod a" and g: "g has_prod b"  lp15@68361  1098  shows "(\n. f n * g n) has_prod (a * b)"  lp15@68361  1099  using f [unfolded has_prod_def]  lp15@68361  1100 proof (elim disjE exE conjE)  lp15@68361  1101  assume f0: "raw_has_prod f 0 a"  lp15@68361  1102  show ?thesis  lp15@68361  1103  using g [unfolded has_prod_def]  lp15@68361  1104  proof (elim disjE exE conjE)  lp15@68361  1105  assume g0: "raw_has_prod g 0 b"  lp15@68361  1106  with f0 show ?thesis  lp15@68361  1107  by (force simp add: has_prod_def prod.distrib tendsto_mult raw_has_prod_def)  lp15@68361  1108  next  lp15@68361  1109  fix j q  lp15@68361  1110  assume "b = 0" and "g j = 0" and q: "raw_has_prod g (Suc j) q"  lp15@68361  1111  obtain p where p: "raw_has_prod f (Suc j) p"  lp15@68361  1112  using f0 raw_has_prod_ignore_initial_segment by blast  lp15@68361  1113  then have "Ex (raw_has_prod (\n. f n * g n) (Suc j))"  lp15@68361  1114  using q raw_has_prod_mult by blast  lp15@68361  1115  then show ?thesis  lp15@68361  1116  using \b = 0\ \g j = 0\ has_prod_0_iff by fastforce  lp15@68361  1117  qed  lp15@68361  1118 next  lp15@68361  1119  fix i p  lp15@68361  1120  assume "a = 0" and "f i = 0" and p: "raw_has_prod f (Suc i) p"  lp15@68361  1121  show ?thesis  lp15@68361  1122  using g [unfolded has_prod_def]  lp15@68361  1123  proof (elim disjE exE conjE)  lp15@68361  1124  assume g0: "raw_has_prod g 0 b"  lp15@68361  1125  obtain q where q: "raw_has_prod g (Suc i) q"  lp15@68361  1126  using g0 raw_has_prod_ignore_initial_segment by blast  lp15@68361  1127  then have "Ex (raw_has_prod (\n. f n * g n) (Suc i))"  lp15@68361  1128  using raw_has_prod_mult p by blast  lp15@68361  1129  then show ?thesis  lp15@68361  1130  using \a = 0\ \f i = 0\ has_prod_0_iff by fastforce  lp15@68361  1131  next  lp15@68361  1132  fix j q  lp15@68361  1133  assume "b = 0" and "g j = 0" and q: "raw_has_prod g (Suc j) q"  lp15@68361  1134  obtain p' where p': "raw_has_prod f (Suc (max i j)) p'"  lp15@68361  1135  by (metis raw_has_prod_ignore_initial_segment max_Suc_Suc max_def p)  lp15@68361  1136  moreover  lp15@68361  1137  obtain q' where q': "raw_has_prod g (Suc (max i j)) q'"  lp15@68361  1138  by (metis raw_has_prod_ignore_initial_segment max.cobounded2 max_Suc_Suc q)  lp15@68361  1139  ultimately show ?thesis  lp15@68361  1140  using \b = 0\ by (simp add: has_prod_def) (metis \f i = 0\ \g j = 0\ raw_has_prod_mult max_def)  lp15@68361  1141  qed  lp15@68361  1142 qed  lp15@68361  1143 lp15@68361  1144 lemma convergent_prod_mult:  lp15@68361  1145  assumes f: "convergent_prod f" and g: "convergent_prod g"  lp15@68361  1146  shows "convergent_prod (\n. f n * g n)"  lp15@68361  1147  unfolding convergent_prod_def  lp15@68361  1148 proof -  lp15@68361  1149  obtain M p N q where p: "raw_has_prod f M p" and q: "raw_has_prod g N q"  lp15@68361  1150  using convergent_prod_def f g by blast+  lp15@68361  1151  then obtain p' q' where p': "raw_has_prod f (max M N) p'" and q': "raw_has_prod g (max M N) q'"  lp15@68361  1152  by (meson raw_has_prod_ignore_initial_segment max.cobounded1 max.cobounded2)  lp15@68361  1153  then show "\M p. raw_has_prod (\n. f n * g n) M p"  lp15@68361  1154  using raw_has_prod_mult by blast  lp15@68361  1155 qed  lp15@68361  1156 lp15@68361  1157 lemma prodinf_mult: "convergent_prod f \ convergent_prod g \ prodinf f * prodinf g = (\n. f n * g n)"  lp15@68361  1158  by (intro has_prod_unique has_prod_mult convergent_prod_has_prod)  lp15@68361  1159 lp15@68361  1160 end  lp15@68361  1161 lp15@68361  1162 context  lp15@68361  1163  fixes f :: "'i \ nat \ 'a::real_normed_field"  lp15@68361  1164  and I :: "'i set"  lp15@68361  1165 begin  lp15@68361  1166 lp15@68361  1167 lemma has_prod_prod: "(\i. i \ I \ (f i) has_prod (x i)) \ (\n. \i\I. f i n) has_prod (\i\I. x i)"  lp15@68361  1168  by (induct I rule: infinite_finite_induct) (auto intro!: has_prod_mult)  lp15@68361  1169 lp15@68361  1170 lemma prodinf_prod: "(\i. i \ I \ convergent_prod (f i)) \ (\n. \i\I. f i n) = (\i\I. \n. f i n)"  lp15@68361  1171  using has_prod_unique[OF has_prod_prod, OF convergent_prod_has_prod] by simp  lp15@68361  1172 lp15@68361  1173 lemma convergent_prod_prod: "(\i. i \ I \ convergent_prod (f i)) \ convergent_prod (\n. \i\I. f i n)"  lp15@68361  1174  using convergent_prod_has_prod_iff has_prod_prod prodinf_prod by force  lp15@68361  1175 lp15@68361  1176 end  lp15@68361  1177 eberlm@68651  1178 subsection%unimportant \Infinite summability on real normed fields\  lp15@68361  1179 lp15@68361  1180 context  lp15@68361  1181  fixes f :: "nat \ 'a::real_normed_field"  lp15@68361  1182 begin  lp15@68361  1183 lp15@68361  1184 lemma raw_has_prod_Suc_iff: "raw_has_prod f M (a * f M) \ raw_has_prod (\n. f (Suc n)) M a \ f M \ 0"  lp15@68361  1185 proof -  lp15@68361  1186  have "raw_has_prod f M (a * f M) \ (\i. \j\Suc i. f (j+M)) \ a * f M \ a * f M \ 0"  lp15@68361  1187  by (subst LIMSEQ_Suc_iff) (simp add: raw_has_prod_def)  lp15@68361  1188  also have "\ \ (\i. (\j\i. f (Suc j + M)) * f M) \ a * f M \ a * f M \ 0"  lp15@68361  1189  by (simp add: ac_simps atMost_Suc_eq_insert_0 image_Suc_atMost prod_atLeast1_atMost_eq lessThan_Suc_atMost)  lp15@68361  1190  also have "\ \ raw_has_prod (\n. f (Suc n)) M a \ f M \ 0"  lp15@68361  1191  proof safe  lp15@68361  1192  assume tends: "(\i. (\j\i. f (Suc j + M)) * f M) \ a * f M" and 0: "a * f M \ 0"  lp15@68361  1193  with tendsto_divide[OF tends tendsto_const, of "f M"]  lp15@68361  1194  show "raw_has_prod (\n. f (Suc n)) M a"  lp15@68361  1195  by (simp add: raw_has_prod_def)  lp15@68361  1196  qed (auto intro: tendsto_mult_right simp: raw_has_prod_def)  lp15@68361  1197  finally show ?thesis .  lp15@68361  1198 qed  lp15@68361  1199 lp15@68361  1200 lemma has_prod_Suc_iff:  lp15@68361  1201  assumes "f 0 \ 0" shows "(\n. f (Suc n)) has_prod a \ f has_prod (a * f 0)"  lp15@68361  1202 proof (cases "a = 0")  lp15@68361  1203  case True  lp15@68361  1204  then show ?thesis  lp15@68361  1205  proof (simp add: has_prod_def, safe)  lp15@68361  1206  fix i x  lp15@68361  1207  assume "f (Suc i) = 0" and "raw_has_prod (\n. f (Suc n)) (Suc i) x"  lp15@68361  1208  then obtain y where "raw_has_prod f (Suc (Suc i)) y"  lp15@68361  1209  by (metis (no_types) raw_has_prod_eq_0 Suc_n_not_le_n raw_has_prod_Suc_iff raw_has_prod_ignore_initial_segment raw_has_prod_nonzero linear)  lp15@68361  1210  then show "\i. f i = 0 \ Ex (raw_has_prod f (Suc i))"  lp15@68361  1211  using \f (Suc i) = 0\ by blast  lp15@68361  1212  next  lp15@68361  1213  fix i x  lp15@68361  1214  assume "f i = 0" and x: "raw_has_prod f (Suc i) x"  lp15@68361  1215  then obtain j where j: "i = Suc j"  lp15@68361  1216  by (metis assms not0_implies_Suc)  lp15@68361  1217  moreover have "\ y. raw_has_prod (\n. f (Suc n)) i y"  lp15@68361  1218  using x by (auto simp: raw_has_prod_def)  lp15@68361  1219  then show "\i. f (Suc i) = 0 \ Ex (raw_has_prod (\n. f (Suc n)) (Suc i))"  lp15@68361  1220  using \f i = 0\ j by blast  lp15@68361  1221  qed  lp15@68361  1222 next  lp15@68361  1223  case False  lp15@68361  1224  then show ?thesis  lp15@68361  1225  by (auto simp: has_prod_def raw_has_prod_Suc_iff assms)  lp15@68361  1226 qed  lp15@68361  1227 lp15@68361  1228 lemma convergent_prod_Suc_iff:  lp15@68452  1229  shows "convergent_prod (\n. f (Suc n)) = convergent_prod f"  lp15@68361  1230 proof  lp15@68361  1231  assume "convergent_prod f"  lp15@68452  1232  then obtain M L where M_nz:"\n\M. f n \ 0" and  lp15@68452  1233  M_L:"(\n. \i\n. f (i + M)) \ L" and "L \ 0"  lp15@68452  1234  unfolding convergent_prod_altdef by auto  lp15@68452  1235  have "(\n. \i\n. f (Suc (i + M))) \ L / f M"  lp15@68452  1236  proof -  lp15@68452  1237  have "(\n. \i\{0..Suc n}. f (i + M)) \ L"  lp15@68452  1238  using M_L  lp15@68452  1239  apply (subst (asm) LIMSEQ_Suc_iff[symmetric])  lp15@68452  1240  using atLeast0AtMost by auto  lp15@68452  1241  then have "(\n. f M * (\i\{0..n}. f (Suc (i + M)))) \ L"  lp15@68452  1242  apply (subst (asm) prod.atLeast0_atMost_Suc_shift)  lp15@68452  1243  by simp  lp15@68452  1244  then have "(\n. (\i\{0..n}. f (Suc (i + M)))) \ L/f M"  lp15@68452  1245  apply (drule_tac tendsto_divide)  lp15@68452  1246  using M_nz[rule_format,of M,simplified] by auto  lp15@68452  1247  then show ?thesis unfolding atLeast0AtMost .  lp15@68452  1248  qed  lp15@68452  1249  then show "convergent_prod (\n. f (Suc n))" unfolding convergent_prod_altdef  lp15@68452  1250  apply (rule_tac exI[where x=M])  lp15@68452  1251  apply (rule_tac exI[where x="L/f M"])  lp15@68452  1252  using M_nz \L\0\ by auto  lp15@68361  1253 next  lp15@68361  1254  assume "convergent_prod (\n. f (Suc n))"  lp15@68452  1255  then obtain M where "\L. (\n\M. f (Suc n) \ 0) \ (\n. \i\n. f (Suc (i + M))) \ L \ L \ 0"  lp15@68452  1256  unfolding convergent_prod_altdef by auto  lp15@68452  1257  then show "convergent_prod f" unfolding convergent_prod_altdef  lp15@68452  1258  apply (rule_tac exI[where x="Suc M"])  lp15@68452  1259  using Suc_le_D by auto  lp15@68361  1260 qed  lp15@68361  1261 lp15@68361  1262 lemma raw_has_prod_inverse:  lp15@68361  1263  assumes "raw_has_prod f M a" shows "raw_has_prod (\n. inverse (f n)) M (inverse a)"  lp15@68361  1264  using assms unfolding raw_has_prod_def by (auto dest: tendsto_inverse simp: prod_inversef [symmetric])  lp15@68361  1265 lp15@68361  1266 lemma has_prod_inverse:  lp15@68361  1267  assumes "f has_prod a" shows "(\n. inverse (f n)) has_prod (inverse a)"  lp15@68361  1268 using assms raw_has_prod_inverse unfolding has_prod_def by auto  lp15@68361  1269 lp15@68361  1270 lemma convergent_prod_inverse:  lp15@68361  1271  assumes "convergent_prod f"  lp15@68361  1272  shows "convergent_prod (\n. inverse (f n))"  lp15@68361  1273  using assms unfolding convergent_prod_def by (blast intro: raw_has_prod_inverse elim: )  lp15@68361  1274 lp15@68361  1275 end  lp15@68361  1276 lp15@68424  1277 context  lp15@68361  1278  fixes f :: "nat \ 'a::real_normed_field"  lp15@68361  1279 begin  lp15@68361  1280 lp15@68361  1281 lemma raw_has_prod_Suc_iff': "raw_has_prod f M a \ raw_has_prod (\n. f (Suc n)) M (a / f M) \ f M \ 0"  lp15@68361  1282  by (metis raw_has_prod_eq_0 add.commute add.left_neutral raw_has_prod_Suc_iff raw_has_prod_nonzero le_add1 nonzero_mult_div_cancel_right times_divide_eq_left)  lp15@68361  1283 lp15@68361  1284 lemma has_prod_divide: "f has_prod a \ g has_prod b \ (\n. f n / g n) has_prod (a / b)"  lp15@68361  1285  unfolding divide_inverse by (intro has_prod_inverse has_prod_mult)  lp15@68361  1286 lp15@68361  1287 lemma convergent_prod_divide:  lp15@68361  1288  assumes f: "convergent_prod f" and g: "convergent_prod g"  lp15@68361  1289  shows "convergent_prod (\n. f n / g n)"  lp15@68361  1290  using f g has_prod_divide has_prod_iff by blast  lp15@68361  1291 lp15@68361  1292 lemma prodinf_divide: "convergent_prod f \ convergent_prod g \ prodinf f / prodinf g = (\n. f n / g n)"  lp15@68361  1293  by (intro has_prod_unique has_prod_divide convergent_prod_has_prod)  lp15@68361  1294 lp15@68361  1295 lemma prodinf_inverse: "convergent_prod f \ (\n. inverse (f n)) = inverse (\n. f n)"  lp15@68361  1296  by (intro has_prod_unique [symmetric] has_prod_inverse convergent_prod_has_prod)  lp15@68361  1297 lp15@68452  1298 lemma has_prod_Suc_imp:  lp15@68452  1299  assumes "(\n. f (Suc n)) has_prod a"  lp15@68452  1300  shows "f has_prod (a * f 0)"  lp15@68452  1301 proof -  lp15@68452  1302  have "f has_prod (a * f 0)" when "raw_has_prod (\n. f (Suc n)) 0 a"  lp15@68452  1303  apply (cases "f 0=0")  lp15@68452  1304  using that unfolding has_prod_def raw_has_prod_Suc  lp15@68452  1305  by (auto simp add: raw_has_prod_Suc_iff)  lp15@68452  1306  moreover have "f has_prod (a * f 0)" when  lp15@68452  1307  "(\i q. a = 0 \ f (Suc i) = 0 \ raw_has_prod (\n. f (Suc n)) (Suc i) q)"  lp15@68452  1308  proof -  lp15@68452  1309  from that  lp15@68452  1310  obtain i q where "a = 0" "f (Suc i) = 0" "raw_has_prod (\n. f (Suc n)) (Suc i) q"  lp15@68452  1311  by auto  lp15@68452  1312  then show ?thesis unfolding has_prod_def  lp15@68452  1313  by (auto intro!:exI[where x="Suc i"] simp:raw_has_prod_Suc)  lp15@68452  1314  qed  lp15@68452  1315  ultimately show "f has_prod (a * f 0)" using assms unfolding has_prod_def by auto  lp15@68452  1316 qed  lp15@68452  1317 lp15@68361  1318 lemma has_prod_iff_shift:  lp15@68361  1319  assumes "\i. i < n \ f i \ 0"  lp15@68361  1320  shows "(\i. f (i + n)) has_prod a \ f has_prod (a * (\ii. f (Suc i + n)) has_prod a \ (\i. f (i + n)) has_prod (a * f n)"  lp15@68361  1328  by (subst has_prod_Suc_iff) auto  lp15@68361  1329  with Suc show ?case  lp15@68361  1330  by (simp add: ac_simps)  lp15@68361  1331 qed  lp15@68361  1332 eberlm@68651  1333 corollary%unimportant has_prod_iff_shift':  lp15@68361  1334  assumes "\i. i < n \ f i \ 0"  lp15@68361  1335  shows "(\i. f (i + n)) has_prod (a / (\i f has_prod a"  lp15@68361  1336  by (simp add: assms has_prod_iff_shift)  lp15@68361  1337 lp15@68361  1338 lemma has_prod_one_iff_shift:  lp15@68361  1339  assumes "\i. i < n \ f i = 1"  lp15@68361  1340  shows "(\i. f (i+n)) has_prod a \ (\i. f i) has_prod a"  lp15@68361  1341  by (simp add: assms has_prod_iff_shift)  lp15@68361  1342 lp15@68361  1343 lemma convergent_prod_iff_shift:  lp15@68361  1344  shows "convergent_prod (\i. f (i + n)) \ convergent_prod f"  lp15@68361  1345  apply safe  lp15@68361  1346  using convergent_prod_offset apply blast  lp15@68361  1347  using convergent_prod_ignore_initial_segment convergent_prod_def by blast  lp15@68361  1348 lp15@68361  1349 lemma has_prod_split_initial_segment:  lp15@68361  1350  assumes "f has_prod a" "\i. i < n \ f i \ 0"  lp15@68361  1351  shows "(\i. f (i + n)) has_prod (a / (\ii. i < n \ f i \ 0"  lp15@68361  1356  shows "(\i. f (i + n)) = (\i. f i) / (\ii. i < n \ f i \ 0"  lp15@68361  1361  shows "prodinf f = (\i. f (i + n)) * (\i 0"  lp15@68361  1366  shows "(\n. f (Suc n)) = prodinf f / f 0"  lp15@68361  1367  using prodinf_split_initial_segment[of 1] assms by simp  lp15@68361  1368 lp15@68361  1369 end  lp15@68361  1370 lp15@68424  1371 context  lp15@68361  1372  fixes f :: "nat \ 'a::real_normed_field"  lp15@68361  1373 begin  lp15@68361  1374 lp15@68361  1375 lemma convergent_prod_inverse_iff: "convergent_prod (\n. inverse (f n)) \ convergent_prod f"  lp15@68361  1376  by (auto dest: convergent_prod_inverse)  lp15@68361  1377 lp15@68361  1378 lemma convergent_prod_const_iff:  lp15@68361  1379  fixes c :: "'a :: {real_normed_field}"  lp15@68361  1380  shows "convergent_prod (\_. c) \ c = 1"  lp15@68361  1381 proof  lp15@68361  1382  assume "convergent_prod (\_. c)"  lp15@68361  1383  then show "c = 1"  lp15@68361  1384  using convergent_prod_imp_LIMSEQ LIMSEQ_unique by blast  lp15@68361  1385 next  lp15@68361  1386  assume "c = 1"  lp15@68361  1387  then show "convergent_prod (\_. c)"  lp15@68361  1388  by auto  lp15@68361  1389 qed  lp15@68361  1390 lp15@68361  1391 lemma has_prod_power: "f has_prod a \ (\i. f i ^ n) has_prod (a ^ n)"  lp15@68361  1392  by (induction n) (auto simp: has_prod_mult)  lp15@68361  1393 lp15@68361  1394 lemma convergent_prod_power: "convergent_prod f \ convergent_prod (\i. f i ^ n)"  lp15@68361  1395  by (induction n) (auto simp: convergent_prod_mult)  lp15@68361  1396 lp15@68361  1397 lemma prodinf_power: "convergent_prod f \ prodinf (\i. f i ^ n) = prodinf f ^ n"  lp15@68361  1398  by (metis has_prod_unique convergent_prod_imp_has_prod has_prod_power)  lp15@68361  1399 lp15@68361  1400 end  lp15@68361  1401 lp15@68424  1402 lp15@68424  1403 subsection\Exponentials and logarithms\  lp15@68424  1404 lp15@68424  1405 context  lp15@68424  1406  fixes f :: "nat \ 'a::{real_normed_field,banach}"  lp15@68424  1407 begin  lp15@68424  1408 lp15@68424  1409 lemma sums_imp_has_prod_exp:  lp15@68424  1410  assumes "f sums s"  lp15@68424  1411  shows "raw_has_prod (\i. exp (f i)) 0 (exp s)"  lp15@68424  1412  using assms continuous_on_exp [of UNIV "\x::'a. x"]  lp15@68424  1413  using continuous_on_tendsto_compose [of UNIV exp "(\n. sum f {..n})" s]  lp15@68424  1414  by (simp add: prod_defs sums_def_le exp_sum)  lp15@68424  1415 lp15@68424  1416 lemma convergent_prod_exp:  lp15@68424  1417  assumes "summable f"  lp15@68424  1418  shows "convergent_prod (\i. exp (f i))"  lp15@68424  1419  using sums_imp_has_prod_exp assms unfolding summable_def convergent_prod_def by blast  lp15@68424  1420 lp15@68424  1421 lemma prodinf_exp:  lp15@68424  1422  assumes "summable f"  lp15@68424  1423  shows "prodinf (\i. exp (f i)) = exp (suminf f)"  lp15@68424  1424 proof -  lp15@68424  1425  have "f sums suminf f"  lp15@68424  1426  using assms by blast  lp15@68424  1427  then have "(\i. exp (f i)) has_prod exp (suminf f)"  lp15@68424  1428  by (simp add: has_prod_def sums_imp_has_prod_exp)  lp15@68424  1429  then show ?thesis  lp15@68424  1430  by (rule has_prod_unique [symmetric])  lp15@68424  1431 qed  lp15@68424  1432 lp15@68361  1433 end  lp15@68424  1434 eberlm@68651  1435 theorem convergent_prod_iff_summable_real:  lp15@68585  1436  fixes a :: "nat \ real"  lp15@68585  1437  assumes "\n. a n > 0"  lp15@68585  1438  shows "convergent_prod (\k. 1 + a k) \ summable a" (is "?lhs = ?rhs")  lp15@68585  1439 proof  lp15@68585  1440  assume ?lhs  lp15@68585  1441  then obtain p where "raw_has_prod (\k. 1 + a k) 0 p"  lp15@68585  1442  by (metis assms add_less_same_cancel2 convergent_prod_offset_0 not_one_less_zero)  lp15@68585  1443  then have to_p: "(\n. \k\n. 1 + a k) \ p"  lp15@68585  1444  by (auto simp: raw_has_prod_def)  lp15@68585  1445  moreover have le: "(\k\n. a k) \ (\k\n. 1 + a k)" for n  lp15@68585  1446  by (rule sum_le_prod) (use assms less_le in force)  lp15@68585  1447  have "(\k\n. 1 + a k) \ p" for n  lp15@68585  1448  proof (rule incseq_le [OF _ to_p])  lp15@68585  1449  show "incseq (\n. \k\n. 1 + a k)"  lp15@68585  1450  using assms by (auto simp: mono_def order.strict_implies_order intro!: prod_mono2)  lp15@68585  1451  qed  lp15@68585  1452  with le have "(\k\n. a k) \ p" for n  lp15@68585  1453  by (metis order_trans)  lp15@68585  1454  with assms bounded_imp_summable show ?rhs  lp15@68585  1455  by (metis not_less order.asym)  lp15@68585  1456 next  lp15@68585  1457  assume R: ?rhs  lp15@68585  1458  have "(\k\n. 1 + a k) \ exp (suminf a)" for n  lp15@68585  1459  proof -  lp15@68585  1460  have "(\k\n. 1 + a k) \ exp (\k\n. a k)" for n  lp15@68585  1461  by (rule prod_le_exp_sum) (use assms less_le in force)  lp15@68585  1462  moreover have "exp (\k\n. a k) \ exp (suminf a)" for n  lp15@68585  1463  unfolding exp_le_cancel_iff  lp15@68585  1464  by (meson sum_le_suminf R assms finite_atMost less_eq_real_def)  lp15@68585  1465  ultimately show ?thesis  lp15@68585  1466  by (meson order_trans)  lp15@68585  1467  qed  lp15@68585  1468  then obtain L where L: "(\n. \k\n. 1 + a k) \ L"  lp15@68585  1469  by (metis assms bounded_imp_convergent_prod convergent_prod_iff_nz_lim le_add_same_cancel1 le_add_same_cancel2 less_le not_le zero_le_one)  lp15@68585  1470  moreover have "L \ 0"  lp15@68585  1471  proof  lp15@68585  1472  assume "L = 0"  lp15@68585  1473  with L have "(\n. \k\n. 1 + a k) \ 0"  lp15@68585  1474  by simp  lp15@68585  1475  moreover have "(\k\n. 1 + a k) > 1" for n  lp15@68585  1476  by (simp add: assms less_1_prod)  lp15@68585  1477  ultimately show False  lp15@68585  1478  by (meson Lim_bounded2 not_one_le_zero less_imp_le)  lp15@68585  1479  qed  lp15@68585  1480  ultimately show ?lhs  lp15@68585  1481  using assms convergent_prod_iff_nz_lim  lp15@68585  1482  by (metis add_less_same_cancel1 less_le not_le zero_less_one)  lp15@68585  1483 qed  lp15@68585  1484 lp15@68452  1485 lemma exp_suminf_prodinf_real:  lp15@68452  1486  fixes f :: "nat \ real"  lp15@68452  1487  assumes ge0:"\n. f n \ 0" and ac: "abs_convergent_prod (\n. exp (f n))"  lp15@68452  1488  shows "prodinf (\i. exp (f i)) = exp (suminf f)"  lp15@68452  1489 proof -  lp15@68517  1490  have "summable f"  lp15@68452  1491  using ac unfolding abs_convergent_prod_conv_summable  lp15@68452  1492  proof (elim summable_comparison_test')  lp15@68452  1493  fix n  lp15@68517  1494  have "\f n\ = f n"  lp15@68517  1495  by (simp add: ge0)  lp15@68517  1496  also have "\ \ exp (f n) - 1"  lp15@68517  1497  by (metis diff_diff_add exp_ge_add_one_self ge_iff_diff_ge_0)  lp15@68517  1498  finally show "norm (f n) \ norm (exp (f n) - 1)"  lp15@68517  1499  by simp  lp15@68452  1500  qed  lp15@68452  1501  then show ?thesis  lp15@68452  1502  by (simp add: prodinf_exp)  lp15@68452  1503 qed  lp15@68452  1504 lp15@68424  1505 lemma has_prod_imp_sums_ln_real:  lp15@68424  1506  fixes f :: "nat \ real"  lp15@68424  1507  assumes "raw_has_prod f 0 p" and 0: "\x. f x > 0"  lp15@68424  1508  shows "(\i. ln (f i)) sums (ln p)"  lp15@68424  1509 proof -  lp15@68424  1510  have "p > 0"  lp15@68424  1511  using assms unfolding prod_defs by (metis LIMSEQ_prod_nonneg less_eq_real_def)  lp15@68424  1512  then show ?thesis  lp15@68424  1513  using assms continuous_on_ln [of "{0<..}" "\x. x"]  lp15@68424  1514  using continuous_on_tendsto_compose [of "{0<..}" ln "(\n. prod f {..n})" p]  lp15@68424  1515  by (auto simp: prod_defs sums_def_le ln_prod order_tendstoD)  lp15@68424  1516 qed  lp15@68424  1517 lp15@68424  1518 lemma summable_ln_real:  lp15@68424  1519  fixes f :: "nat \ real"  lp15@68424  1520  assumes f: "convergent_prod f" and 0: "\x. f x > 0"  lp15@68424  1521  shows "summable (\i. ln (f i))"  lp15@68424  1522 proof -  lp15@68424  1523  obtain M p where "raw_has_prod f M p"  lp15@68424  1524  using f convergent_prod_def by blast  lp15@68424  1525  then consider i where "i real"  lp15@68424  1541  assumes f: "convergent_prod f" and 0: "\x. f x > 0"  lp15@68424  1542  shows "suminf (\i. ln (f i)) = ln (prodinf f)"  lp15@68424  1543 proof -  lp15@68424  1544  have "f has_prod prodinf f"  lp15@68424  1545  by (simp add: f has_prod_iff)  lp15@68424  1546  then have "raw_has_prod f 0 (prodinf f)"  lp15@68424  1547  by (metis "0" has_prod_def less_irrefl)  lp15@68424  1548  then have "(\i. ln (f i)) sums ln (prodinf f)"  lp15@68424  1549  using "0" has_prod_imp_sums_ln_real by blast  lp15@68424  1550  then show ?thesis  lp15@68424  1551  by (rule sums_unique [symmetric])  lp15@68424  1552 qed  lp15@68424  1553 lp15@68424  1554 lemma prodinf_exp_real:  lp15@68424  1555  fixes f :: "nat \ real"  lp15@68424  1556  assumes f: "convergent_prod f" and 0: "\x. f x > 0"  lp15@68424  1557  shows "prodinf f = exp (suminf (\i. ln (f i)))"  lp15@68424  1558  by (simp add: "0" f less_0_prodinf suminf_ln_real)  lp15@68424  1559 lp15@68424  1560 eberlm@68651  1561 theorem Ln_prodinf_complex:  lp15@68585  1562  fixes z :: "nat \ complex"  lp15@68585  1563  assumes z: "\j. z j \ 0" and \: "\ \ 0"  lp15@68585  1564  shows "((\n. \j\n. z j) \ \) \ (\k. (\n. (\j\n. Ln (z j))) \ Ln \ + of_int k * (of_real(2*pi) * \))" (is "?lhs = ?rhs")  lp15@68585  1565 proof  lp15@68585  1566  assume L: ?lhs  lp15@68585  1567  have pnz: "(\j\n. z j) \ 0" for n  lp15@68585  1568  using z by auto  lp15@68585  1569  define \ where "\ \ Arg \ + 2*pi"  lp15@68585  1570  then have "\ > pi"  lp15@68585  1571  using Arg_def mpi_less_Im_Ln by fastforce  lp15@68585  1572  have \_eq: "\ = cmod \ * exp (\ * \)"  lp15@68585  1573  using Arg_def Arg_eq \ unfolding \_def by (simp add: algebra_simps exp_add)  lp15@68585  1574  define \ where "\ \ \n. THE t. is_Arg (\j\n. z j) t \ t \ {\-pi<..\+pi}"  lp15@68585  1575  have uniq: "\!s. is_Arg (\j\n. z j) s \ s \ {\-pi<..\+pi}" for n  lp15@68585  1576  using Argument_exists_unique [OF pnz] by metis  lp15@68585  1577  have \: "is_Arg (\j\n. z j) (\ n)" and \_interval: "\ n \ {\-pi<..\+pi}" for n  lp15@68585  1578  unfolding \_def  lp15@68585  1579  using theI' [OF uniq] by metis+  lp15@68585  1580  have \_pos: "\j. \ j > 0"  lp15@68585  1581  using \_interval \\ > pi\ by simp (meson diff_gt_0_iff_gt less_trans)  lp15@68585  1582  have "(\j\n. z j) = cmod (\j\n. z j) * exp (\ * \ n)" for n  lp15@68585  1583  using \ by (auto simp: is_Arg_def)  lp15@68585  1584  then have eq: "(\n. \j\n. z j) = (\n. cmod (\j\n. z j) * exp (\ * \ n))"  lp15@68585  1585  by simp  lp15@68585  1586  then have "(\n. (cmod (\j\n. z j)) * exp (\ * (\ n))) \ \"  lp15@68585  1587  using L by force  lp15@68585  1588  then obtain k where k: "(\j. \ j - of_int (k j) * (2 * pi)) \ \"  lp15@68585  1589  using L by (subst (asm) \_eq) (auto simp add: eq z \ polar_convergence)  lp15@68585  1590  moreover have "\\<^sub>F n in sequentially. k n = 0"  lp15@68585  1591  proof -  lp15@68585  1592  have *: "kj = 0" if "dist (vj - real_of_int kj * 2) V < 1" "vj \ {V - 1<..V + 1}" for kj vj V  lp15@68585  1593  using that by (auto simp: dist_norm)  lp15@68585  1594  have "\\<^sub>F j in sequentially. dist (\ j - of_int (k j) * (2 * pi)) \ < pi"  lp15@68585  1595  using tendstoD [OF k] pi_gt_zero by blast  lp15@68585  1596  then show ?thesis  lp15@68585  1597  proof (rule eventually_mono)  lp15@68585  1598  fix j  lp15@68585  1599  assume d: "dist (\ j - real_of_int (k j) * (2 * pi)) \ < pi"  lp15@68585  1600  show "k j = 0"  lp15@68585  1601  by (rule * [of "\ j/pi" _ "\/pi"])  lp15@68585  1602  (use \_interval [of j] d in \simp_all add: divide_simps dist_norm\)  lp15@68585  1603  qed  lp15@68585  1604  qed  lp15@68585  1605  ultimately have \to\: "\ \ \"  lp15@68585  1606  apply (simp only: tendsto_def)  lp15@68585  1607  apply (erule all_forward imp_forward asm_rl)+  lp15@68585  1608  apply (drule (1) eventually_conj)  lp15@68585  1609  apply (auto elim: eventually_mono)  lp15@68585  1610  done  lp15@68585  1611  then have to0: "(\n. \\ (Suc n) - \ n\) \ 0"  lp15@68585  1612  by (metis (full_types) diff_self filterlim_sequentially_Suc tendsto_diff tendsto_rabs_zero)  lp15@68585  1613  have "\k. Im (\j\n. Ln (z j)) - of_int k * (2*pi) = \ n" for n  lp15@68585  1614  proof (rule is_Arg_exp_diff_2pi)  lp15@68585  1615  show "is_Arg (exp (\j\n. Ln (z j))) (\ n)"  lp15@68585  1616  using pnz \ by (simp add: is_Arg_def exp_sum prod_norm)  lp15@68585  1617  qed  lp15@68585  1618  then have "\k. (\j\n. Im (Ln (z j))) = \ n + of_int k * (2*pi)" for n  lp15@68585  1619  by (simp add: algebra_simps)  lp15@68585  1620  then obtain k where k: "\n. (\j\n. Im (Ln (z j))) = \ n + of_int (k n) * (2*pi)"  lp15@68585  1621  by metis  lp15@68585  1622  obtain K where "\\<^sub>F n in sequentially. k n = K"  lp15@68585  1623  proof -  lp15@68585  1624  have k_le: "(2*pi) * \k (Suc n) - k n\ \ \\ (Suc n) - \ n\ + \Im (Ln (z (Suc n)))\" for n  lp15@68585  1625  proof -  lp15@68585  1626  have "(\j\Suc n. Im (Ln (z j))) - (\j\n. Im (Ln (z j))) = Im (Ln (z (Suc n)))"  lp15@68585  1627  by simp  lp15@68585  1628  then show ?thesis  lp15@68585  1629  using k [of "Suc n"] k [of n] by (auto simp: abs_if algebra_simps)  lp15@68585  1630  qed  lp15@68585  1631  have "z \ 1"  lp15@68585  1632  using L \ convergent_prod_iff_nz_lim z by (blast intro: convergent_prod_imp_LIMSEQ)  lp15@68585  1633  with z have "(\n. Ln (z n)) \ Ln 1"  lp15@68585  1634  using isCont_tendsto_compose [OF continuous_at_Ln] nonpos_Reals_one_I by blast  lp15@68585  1635  then have "(\n. Ln (z n)) \ 0"  lp15@68585  1636  by simp  lp15@68585  1637  then have "(\n. \Im (Ln (z (Suc n)))\) \ 0"  lp15@68585  1638  by (metis LIMSEQ_unique \z \ 1\ continuous_at_Ln filterlim_sequentially_Suc isCont_tendsto_compose nonpos_Reals_one_I tendsto_Im tendsto_rabs_zero_iff zero_complex.simps(2))  lp15@68585  1639  then have "\\<^sub>F n in sequentially. \Im (Ln (z (Suc n)))\ < 1"  lp15@68585  1640  by (simp add: order_tendsto_iff)  lp15@68585  1641  moreover have "\\<^sub>F n in sequentially. \\ (Suc n) - \ n\ < 1"  lp15@68585  1642  using to0 by (simp add: order_tendsto_iff)  lp15@68585  1643  ultimately have "\\<^sub>F n in sequentially. (2*pi) * \k (Suc n) - k n\ < 1 + 1"  lp15@68585  1644  proof (rule eventually_elim2)  lp15@68585  1645  fix n  lp15@68585  1646  assume "\Im (Ln (z (Suc n)))\ < 1" and "\\ (Suc n) - \ n\ < 1"  lp15@68585  1647  with k_le [of n] show "2 * pi * real_of_int \k (Suc n) - k n\ < 1 + 1"  lp15@68585  1648  by linarith  lp15@68585  1649  qed  lp15@68585  1650  then have "\\<^sub>F n in sequentially. real_of_int\k (Suc n) - k n\ < 1"  lp15@68585  1651  proof (rule eventually_mono)  lp15@68585  1652  fix n :: "nat"  lp15@68585  1653  assume "2 * pi * \k (Suc n) - k n\ < 1 + 1"  lp15@68585  1654  then have "\k (Suc n) - k n\ < 2 / (2*pi)"  lp15@68585  1655  by (simp add: field_simps)  lp15@68585  1656  also have "... < 1"  lp15@68585  1657  using pi_ge_two by auto  lp15@68585  1658  finally show "real_of_int \k (Suc n) - k n\ < 1" .  lp15@68585  1659  qed  lp15@68585  1660  then obtain N where N: "\n. n\N \ \k (Suc n) - k n\ = 0"  lp15@68585  1661  using eventually_sequentially less_irrefl of_int_abs by fastforce  lp15@68585  1662  have "k (N+i) = k N" for i  lp15@68585  1663  proof (induction i)  lp15@68585  1664  case (Suc i)  lp15@68585  1665  with N [of "N+i"] show ?case  lp15@68585  1666  by auto  lp15@68585  1667  qed simp  lp15@68585  1668  then have "\n. n\N \ k n = k N"  lp15@68585  1669  using le_Suc_ex by auto  lp15@68585  1670  then show ?thesis  lp15@68585  1671  by (force simp add: eventually_sequentially intro: that)  lp15@68585  1672  qed  lp15@68585  1673  with \to\ have "(\n. (\j\n. Im (Ln (z j)))) \ \ + of_int K * (2*pi)"  lp15@68585  1674  by (simp add: k tendsto_add tendsto_mult Lim_eventually)  lp15@68585  1675  moreover have "(\n. (\k\n. Re (Ln (z k)))) \ Re (Ln \)"  lp15@68585  1676  using assms continuous_imp_tendsto [OF isCont_ln tendsto_norm [OF L]]  lp15@68585  1677  by (simp add: o_def flip: prod_norm ln_prod)  lp15@68585  1678  ultimately show ?rhs  lp15@68585  1679  by (rule_tac x="K+1" in exI) (auto simp: tendsto_complex_iff \_def Arg_def assms algebra_simps)  lp15@68585  1680 next  lp15@68585  1681  assume ?rhs  lp15@68585  1682  then obtain r where r: "(\n. (\k\n. Ln (z k))) \ Ln \ + of_int r * (of_real(2*pi) * \)" ..  lp15@68585  1683  have "(\n. exp (\k\n. Ln (z k))) \ \"  lp15@68585  1684  using assms continuous_imp_tendsto [OF isCont_exp r] exp_integer_2pi [of r]  lp15@68585  1685  by (simp add: o_def exp_add algebra_simps)  lp15@68585  1686  moreover have "exp (\k\n. Ln (z k)) = (\k\n. z k)" for n  lp15@68585  1687  by (simp add: exp_sum add_eq_0_iff assms)  lp15@68585  1688  ultimately show ?lhs  lp15@68585  1689  by auto  lp15@68585  1690 qed  lp15@68585  1691 lp15@68585  1692 text\Prop 17.2 of Bak and Newman, Complex Analysis, p.242\  lp15@68585  1693 proposition convergent_prod_iff_summable_complex:  lp15@68585  1694  fixes z :: "nat \ complex"  lp15@68585  1695  assumes "\k. z k \ 0"  lp15@68585  1696  shows "convergent_prod (\k. z k) \ summable (\k. Ln (z k))" (is "?lhs = ?rhs")  lp15@68585  1697 proof  lp15@68585  1698  assume ?lhs  lp15@68585  1699  then obtain p where p: "(\n. \k\n. z k) \ p" and "p \ 0"  lp15@68585  1700  using convergent_prod_LIMSEQ prodinf_nonzero add_eq_0_iff assms by fastforce  lp15@68585  1701  then show ?rhs  lp15@68585  1702  using Ln_prodinf_complex assms  lp15@68585  1703  by (auto simp: prodinf_nonzero summable_def sums_def_le)  lp15@68585  1704 next  lp15@68585  1705  assume R: ?rhs  lp15@68585  1706  have "(\k\n. z k) = exp (\k\n. Ln (z k))" for n  lp15@68585  1707  by (simp add: exp_sum add_eq_0_iff assms)  lp15@68585  1708  then have "(\n. \k\n. z k) \ exp (suminf (\k. Ln (z k)))"  lp15@68585  1709  using continuous_imp_tendsto [OF isCont_exp summable_LIMSEQ' [OF R]] by (simp add: o_def)  lp15@68585  1710  then show ?lhs  lp15@68585  1711  by (subst convergent_prod_iff_convergent) (auto simp: convergent_def tendsto_Lim assms add_eq_0_iff)  lp15@68585  1712 qed  lp15@68585  1713 lp15@68586  1714 text\Prop 17.3 of Bak and Newman, Complex Analysis\  lp15@68586  1715 proposition summable_imp_convergent_prod_complex:  lp15@68586  1716  fixes z :: "nat \ complex"  lp15@68586  1717  assumes z: "summable (\k. norm (z k))" and non0: "\k. z k \ -1"  lp15@68586  1718  shows "convergent_prod (\k. 1 + z k)"  lp15@68586  1719 proof -  lp15@68586  1720  note if_cong [cong] power_Suc [simp del]  lp15@68586  1721  obtain N where N: "\k. k\N \ norm (z k) < 1/2"  lp15@68586  1722  using summable_LIMSEQ_zero [OF z]  lp15@68586  1723  by (metis diff_zero dist_norm half_gt_zero_iff less_numeral_extra(1) lim_sequentially tendsto_norm_zero_iff)  lp15@68586  1724  have "norm (Ln (1 + z k)) \ 2 * norm (z k)" if "k \ N" for k  lp15@68586  1725  proof (cases "z k = 0")  lp15@68586  1726  case False  lp15@68586  1727  let ?f = "\i. cmod ((- 1) ^ i * z k ^ i / of_nat (Suc i))"  lp15@68586  1728  have normf: "norm (?f n) \ (1 / 2) ^ n" for n  lp15@68586  1729  proof -  lp15@68586  1730  have "norm (?f n) = cmod (z k) ^ n / cmod (1 + of_nat n)"  lp15@68586  1731  by (auto simp: norm_divide norm_mult norm_power)  lp15@68586  1732  also have "\ \ cmod (z k) ^ n"  lp15@68586  1733  by (auto simp: divide_simps mult_le_cancel_left1 in_Reals_norm)  lp15@68586  1734  also have "\ \ (1 / 2) ^ n"  lp15@68586  1735  using N [OF that] by (simp add: power_mono)  lp15@68586  1736  finally show "norm (?f n) \ (1 / 2) ^ n" .  lp15@68586  1737  qed  lp15@68586  1738  have summablef: "summable ?f"  lp15@68586  1739  by (intro normf summable_comparison_test' [OF summable_geometric [of "1/2"]]) auto  lp15@68586  1740  have "(\n. (- 1) ^ Suc n / of_nat n * z k ^ n) sums Ln (1 + z k)"  lp15@68586  1741  using Ln_series [of "z k"] N that by fastforce  lp15@68586  1742  then have *: "(\i. z k * (((- 1) ^ i * z k ^ i) / (Suc i))) sums Ln (1 + z k)"  lp15@68586  1743  using sums_split_initial_segment [where n= 1] by (force simp: power_Suc mult_ac)  lp15@68586  1744  then have "norm (Ln (1 + z k)) = norm (suminf (\i. z k * (((- 1) ^ i * z k ^ i) / (Suc i))))"  lp15@68586  1745  using sums_unique by force  lp15@68586  1746  also have "\ = norm (z k * suminf (\i. ((- 1) ^ i * z k ^ i) / (Suc i)))"  lp15@68586  1747  apply (subst suminf_mult)  lp15@68586  1748  using * False  lp15@68586  1749  by (auto simp: sums_summable intro: summable_mult_D [of "z k"])  lp15@68586  1750  also have "\ = norm (z k) * norm (suminf (\i. ((- 1) ^ i * z k ^ i) / (Suc i)))"  lp15@68586  1751  by (simp add: norm_mult)  lp15@68586  1752  also have "\ \ norm (z k) * suminf (\i. norm (((- 1) ^ i * z k ^ i) / (Suc i)))"  lp15@68586  1753  by (intro mult_left_mono summable_norm summablef) auto  lp15@68586  1754  also have "\ \ norm (z k) * suminf (\i. (1/2) ^ i)"  lp15@68586  1755  by (intro mult_left_mono suminf_le) (use summable_geometric [of "1/2"] summablef normf in auto)  lp15@68586  1756  also have "\ \ norm (z k) * 2"  lp15@68586  1757  using suminf_geometric [of "1/2::real"] by simp  lp15@68586  1758  finally show ?thesis  lp15@68586  1759  by (simp add: mult_ac)  lp15@68586  1760  qed simp  lp15@68586  1761  then have "summable (\k. Ln (1 + z k))"  lp15@68586  1762  by (metis summable_comparison_test summable_mult z)  lp15@68586  1763  with non0 show ?thesis  lp15@68586  1764  by (simp add: add_eq_0_iff convergent_prod_iff_summable_complex)  lp15@68586  1765 qed  lp15@68586  1766 lp15@68616  1767 lemma summable_Ln_complex:  lp15@68616  1768  fixes z :: "nat \ complex"  lp15@68616  1769  assumes "convergent_prod z" "\k. z k \ 0"  lp15@68616  1770  shows "summable (\k. Ln (z k))"  lp15@68616  1771  using convergent_prod_def assms convergent_prod_iff_summable_complex by blast  lp15@68616  1772 lp15@68586  1773 eberlm@68651  1774 subsection%unimportant \Embeddings from the reals into some complete real normed field\  lp15@68424  1775 lp15@68426  1776 lemma tendsto_eq_of_real_lim:  lp15@68424  1777  assumes "(\n. of_real (f n) :: 'a::{complete_space,real_normed_field}) \ q"  lp15@68424  1778  shows "q = of_real (lim f)"  lp15@68424  1779 proof -  lp15@68424  1780  have "convergent (\n. of_real (f n) :: 'a)"  lp15@68424  1781  using assms convergent_def by blast  lp15@68424  1782  then have "convergent f"  lp15@68424  1783  unfolding convergent_def  lp15@68424  1784  by (simp add: convergent_eq_Cauchy Cauchy_def)  lp15@68424  1785  then show ?thesis  lp15@68424  1786  by (metis LIMSEQ_unique assms convergentD sequentially_bot tendsto_Lim tendsto_of_real)  lp15@68424  1787 qed  lp15@68424  1788 lp15@68426  1789 lemma tendsto_eq_of_real:  lp15@68424  1790  assumes "(\n. of_real (f n) :: 'a::{complete_space,real_normed_field}) \ q"  lp15@68424  1791  obtains r where "q = of_real r"  lp15@68426  1792  using tendsto_eq_of_real_lim assms by blast  lp15@68424  1793 lp15@68424  1794 lemma has_prod_of_real_iff:  lp15@68424  1795  "(\n. of_real (f n) :: 'a::{complete_space,real_normed_field}) has_prod of_real c \ f has_prod c"  lp15@68424  1796  (is "?lhs = ?rhs")  lp15@68424  1797 proof  lp15@68424  1798  assume ?lhs  lp15@68424  1799  then show ?rhs  lp15@68424  1800  apply (auto simp: prod_defs LIMSEQ_prod_0 tendsto_of_real_iff simp flip: of_real_prod)  lp15@68426  1801  using tendsto_eq_of_real  lp15@68424  1802  by (metis of_real_0 tendsto_of_real_iff)  lp15@68424  1803 next  lp15@68424  1804  assume ?rhs  lp15@68424  1805  with tendsto_of_real_iff show ?lhs  lp15@68424  1806  by (fastforce simp: prod_defs simp flip: of_real_prod)  lp15@68424  1807 qed  lp15@68424  1808 lp15@68424  1809 end `