diff --git a/src/HOL/Analysis/Infinite_Products.thy b/src/HOL/Analysis/Infinite_Products.thy --- a/src/HOL/Analysis/Infinite_Products.thy +++ b/src/HOL/Analysis/Infinite_Products.thy @@ -1,1813 +1,1837 @@ (*File: HOL/Analysis/Infinite_Product.thy Author: Manuel Eberl & LC Paulson Basic results about convergence and absolute convergence of infinite products and their connection to summability. *) section \Infinite Products\ theory Infinite_Products imports Topology_Euclidean_Space Complex_Transcendental begin subsection\<^marker>\tag unimportant\ \Preliminaries\ lemma sum_le_prod: fixes f :: "'a \ 'b :: linordered_semidom" assumes "\x. x \ A \ f x \ 0" shows "sum f A \ (\x\A. 1 + f x)" using assms proof (induction A rule: infinite_finite_induct) case (insert x A) from insert.hyps have "sum f A + f x * (\x\A. 1) \ (\x\A. 1 + f x) + f x * (\x\A. 1 + f x)" by (intro add_mono insert mult_left_mono prod_mono) (auto intro: insert.prems) with insert.hyps show ?case by (simp add: algebra_simps) qed simp_all lemma prod_le_exp_sum: fixes f :: "'a \ real" assumes "\x. x \ A \ f x \ 0" shows "prod (\x. 1 + f x) A \ exp (sum f A)" using assms proof (induction A rule: infinite_finite_induct) case (insert x A) have "(1 + f x) * (\x\A. 1 + f x) \ exp (f x) * exp (sum f A)" using insert.prems by (intro mult_mono insert prod_nonneg exp_ge_add_one_self) auto with insert.hyps show ?case by (simp add: algebra_simps exp_add) qed simp_all lemma lim_ln_1_plus_x_over_x_at_0: "(\x::real. ln (1 + x) / x) \0\ 1" proof (rule lhopital) show "(\x::real. ln (1 + x)) \0\ 0" by (rule tendsto_eq_intros refl | simp)+ have "eventually (\x::real. x \ {-1/2<..<1/2}) (nhds 0)" by (rule eventually_nhds_in_open) auto hence *: "eventually (\x::real. x \ {-1/2<..<1/2}) (at 0)" by (rule filter_leD [rotated]) (simp_all add: at_within_def) show "eventually (\x::real. ((\x. ln (1 + x)) has_field_derivative inverse (1 + x)) (at x)) (at 0)" using * by eventually_elim (auto intro!: derivative_eq_intros simp: field_simps) show "eventually (\x::real. ((\x. x) has_field_derivative 1) (at x)) (at 0)" using * by eventually_elim (auto intro!: derivative_eq_intros simp: field_simps) show "\\<^sub>F x in at 0. x \ 0" by (auto simp: at_within_def eventually_inf_principal) show "(\x::real. inverse (1 + x) / 1) \0\ 1" by (rule tendsto_eq_intros refl | simp)+ qed auto subsection\Definitions and basic properties\ definition\<^marker>\tag important\ raw_has_prod :: "[nat \ 'a::{t2_space, comm_semiring_1}, nat, 'a] \ bool" where "raw_has_prod f M p \ (\n. \i\n. f (i+M)) \ p \ p \ 0" text\The nonzero and zero cases, as in \emph{Complex Analysis} by Joseph Bak and Donald J.Newman, page 241\ text\<^marker>\tag important\ \%whitespace\ definition\<^marker>\tag important\ has_prod :: "(nat \ 'a::{t2_space, comm_semiring_1}) \ 'a \ bool" (infixr "has'_prod" 80) 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)" definition\<^marker>\tag important\ convergent_prod :: "(nat \ 'a :: {t2_space,comm_semiring_1}) \ bool" where "convergent_prod f \ \M p. raw_has_prod f M p" definition\<^marker>\tag important\ prodinf :: "(nat \ 'a::{t2_space, comm_semiring_1}) \ 'a" (binder "\" 10) where "prodinf f = (THE p. f has_prod p)" lemmas prod_defs = raw_has_prod_def has_prod_def convergent_prod_def prodinf_def lemma has_prod_subst[trans]: "f = g \ g has_prod z \ f has_prod z" by simp lemma has_prod_cong: "(\n. f n = g n) \ f has_prod c \ g has_prod c" by presburger lemma raw_has_prod_nonzero [simp]: "\ raw_has_prod f M 0" by (simp add: raw_has_prod_def) lemma raw_has_prod_eq_0: fixes f :: "nat \ 'a::{semidom,t2_space}" assumes p: "raw_has_prod f m p" and i: "f i = 0" "i \ m" shows "p = 0" proof - have eq0: "(\k\n. f (k+m)) = 0" if "i - m \ n" for n proof - have "\k\n. f (k + m) = 0" using i that by auto then show ?thesis by auto qed have "(\n. \i\n. f (i + m)) \ 0" by (rule LIMSEQ_offset [where k = "i-m"]) (simp add: eq0) with p show ?thesis unfolding raw_has_prod_def using LIMSEQ_unique by blast qed lemma raw_has_prod_Suc: "raw_has_prod f (Suc M) a \ raw_has_prod (\n. f (Suc n)) M a" unfolding raw_has_prod_def by auto lemma has_prod_0_iff: "f has_prod 0 \ (\i. f i = 0 \ (\p. raw_has_prod f (Suc i) p))" by (simp add: has_prod_def) lemma has_prod_unique2: fixes f :: "nat \ 'a::{semidom,t2_space}" assumes "f has_prod a" "f has_prod b" shows "a = b" using assms by (auto simp: has_prod_def raw_has_prod_eq_0) (meson raw_has_prod_def sequentially_bot tendsto_unique) lemma has_prod_unique: fixes f :: "nat \ 'a :: {semidom,t2_space}" shows "f has_prod s \ s = prodinf f" by (simp add: has_prod_unique2 prodinf_def the_equality) lemma convergent_prod_altdef: fixes f :: "nat \ 'a :: {t2_space,comm_semiring_1}" shows "convergent_prod f \ (\M L. (\n\M. f n \ 0) \ (\n. \i\n. f (i+M)) \ L \ L \ 0)" proof assume "convergent_prod f" then obtain M L where *: "(\n. \i\n. f (i+M)) \ L" "L \ 0" by (auto simp: prod_defs) have "f i \ 0" if "i \ M" for i proof assume "f i = 0" have **: "eventually (\n. (\i\n. f (i+M)) = 0) sequentially" using eventually_ge_at_top[of "i - M"] proof eventually_elim case (elim n) with \f i = 0\ and \i \ M\ show ?case by (auto intro!: bexI[of _ "i - M"] prod_zero) qed have "(\n. (\i\n. f (i+M))) \ 0" unfolding filterlim_iff by (auto dest!: eventually_nhds_x_imp_x intro!: eventually_mono[OF **]) from tendsto_unique[OF _ this *(1)] and *(2) show False by simp qed with * show "(\M L. (\n\M. f n \ 0) \ (\n. \i\n. f (i+M)) \ L \ L \ 0)" by blast qed (auto simp: prod_defs) +lemma raw_has_prod_norm: + fixes a :: "'a ::real_normed_field" + assumes "raw_has_prod f M a" + shows "raw_has_prod (\n. norm (f n)) M (norm a)" + using assms by (auto simp: raw_has_prod_def prod_norm tendsto_norm) + +lemma has_prod_norm: + fixes a :: "'a ::real_normed_field" + assumes f: "f has_prod a" + shows "(\n. norm (f n)) has_prod (norm a)" + using f [unfolded has_prod_def] +proof (elim disjE exE conjE) + assume f0: "raw_has_prod f 0 a" + then show "(\n. norm (f n)) has_prod norm a" + using has_prod_def raw_has_prod_norm by blast +next + fix i p + assume "a = 0" and "f i = 0" and p: "raw_has_prod f (Suc i) p" + then have "Ex (raw_has_prod (\n. norm (f n)) (Suc i))" + using raw_has_prod_norm by blast + then show ?thesis + by (metis \a = 0\ \f i = 0\ has_prod_0_iff norm_zero) +qed + subsection\Absolutely convergent products\ definition\<^marker>\tag important\ abs_convergent_prod :: "(nat \ _) \ bool" where "abs_convergent_prod f \ convergent_prod (\i. 1 + norm (f i - 1))" lemma abs_convergent_prodI: assumes "convergent (\n. \i\n. 1 + norm (f i - 1))" shows "abs_convergent_prod f" proof - from assms obtain L where L: "(\n. \i\n. 1 + norm (f i - 1)) \ L" by (auto simp: convergent_def) have "L \ 1" proof (rule tendsto_le) show "eventually (\n. (\i\n. 1 + norm (f i - 1)) \ 1) sequentially" proof (intro always_eventually allI) fix n have "(\i\n. 1 + norm (f i - 1)) \ (\i\n. 1)" by (intro prod_mono) auto thus "(\i\n. 1 + norm (f i - 1)) \ 1" by simp qed qed (use L in simp_all) hence "L \ 0" by auto with L show ?thesis unfolding abs_convergent_prod_def prod_defs by (intro exI[of _ "0::nat"] exI[of _ L]) auto qed lemma fixes f :: "nat \ 'a :: {topological_semigroup_mult,t2_space,idom}" assumes "convergent_prod f" shows convergent_prod_imp_convergent: "convergent (\n. \i\n. f i)" and convergent_prod_to_zero_iff [simp]: "(\n. \i\n. f i) \ 0 \ (\i. f i = 0)" proof - from assms obtain M L where M: "\n. n \ M \ f n \ 0" and "(\n. \i\n. f (i + M)) \ L" and "L \ 0" by (auto simp: convergent_prod_altdef) note this(2) also have "(\n. \i\n. f (i + M)) = (\n. \i=M..M+n. f i)" by (intro ext prod.reindex_bij_witness[of _ "\n. n - M" "\n. n + M"]) auto finally have "(\n. (\ii=M..M+n. f i)) \ (\in. (\ii=M..M+n. f i)) = (\n. (\i\{..{M..M+n}. f i))" by (subst prod.union_disjoint) auto also have "(\n. {.. {M..M+n}) = (\n. {..n+M})" by auto finally have lim: "(\n. prod f {..n}) \ prod f {..n. \i\n. f i)" by (auto simp: convergent_def) show "(\n. \i\n. f i) \ 0 \ (\i. f i = 0)" proof assume "\i. f i = 0" then obtain i where "f i = 0" by auto moreover with M have "i < M" by (cases "i < M") auto ultimately have "(\in. \i\n. f i) \ 0" by simp next assume "(\n. \i\n. f i) \ 0" from tendsto_unique[OF _ this lim] and \L \ 0\ show "\i. f i = 0" by auto qed qed lemma convergent_prod_iff_nz_lim: fixes f :: "nat \ 'a :: {topological_semigroup_mult,t2_space,idom}" assumes "\i. f i \ 0" shows "convergent_prod f \ (\L. (\n. \i\n. f i) \ L \ L \ 0)" (is "?lhs \ ?rhs") proof assume ?lhs then show ?rhs using assms convergentD convergent_prod_imp_convergent convergent_prod_to_zero_iff by blast next assume ?rhs then show ?lhs unfolding prod_defs by (rule_tac x=0 in exI) auto qed lemma\<^marker>\tag important\ convergent_prod_iff_convergent: fixes f :: "nat \ 'a :: {topological_semigroup_mult,t2_space,idom}" assumes "\i. f i \ 0" shows "convergent_prod f \ convergent (\n. \i\n. f i) \ lim (\n. \i\n. f i) \ 0" by (force simp: convergent_prod_iff_nz_lim assms convergent_def limI) lemma bounded_imp_convergent_prod: fixes a :: "nat \ real" assumes 1: "\n. a n \ 1" and bounded: "\n. (\i\n. a i) \ B" shows "convergent_prod a" proof - have "bdd_above (range(\n. \i\n. a i))" by (meson bdd_aboveI2 bounded) moreover have "incseq (\n. \i\n. a i)" unfolding mono_def by (metis 1 prod_mono2 atMost_subset_iff dual_order.trans finite_atMost zero_le_one) ultimately obtain p where p: "(\n. \i\n. a i) \ p" using LIMSEQ_incseq_SUP by blast then have "p \ 0" by (metis "1" not_one_le_zero prod_ge_1 LIMSEQ_le_const) with 1 p show ?thesis by (metis convergent_prod_iff_nz_lim not_one_le_zero) qed lemma abs_convergent_prod_altdef: fixes f :: "nat \ 'a :: {one,real_normed_vector}" shows "abs_convergent_prod f \ convergent (\n. \i\n. 1 + norm (f i - 1))" proof assume "abs_convergent_prod f" thus "convergent (\n. \i\n. 1 + norm (f i - 1))" by (auto simp: abs_convergent_prod_def intro!: convergent_prod_imp_convergent) qed (auto intro: abs_convergent_prodI) lemma Weierstrass_prod_ineq: fixes f :: "'a \ real" assumes "\x. x \ A \ f x \ {0..1}" shows "1 - sum f A \ (\x\A. 1 - f x)" using assms proof (induction A rule: infinite_finite_induct) case (insert x A) from insert.hyps and insert.prems have "1 - sum f A + f x * (\x\A. 1 - f x) \ (\x\A. 1 - f x) + f x * (\x\A. 1)" by (intro insert.IH add_mono mult_left_mono prod_mono) auto with insert.hyps show ?case by (simp add: algebra_simps) qed simp_all lemma norm_prod_minus1_le_prod_minus1: fixes f :: "nat \ 'a :: {real_normed_div_algebra,comm_ring_1}" shows "norm (prod (\n. 1 + f n) A - 1) \ prod (\n. 1 + norm (f n)) A - 1" proof (induction A rule: infinite_finite_induct) case (insert x A) from insert.hyps have "norm ((\n\insert x A. 1 + f n) - 1) = norm ((\n\A. 1 + f n) - 1 + f x * (\n\A. 1 + f n))" by (simp add: algebra_simps) also have "\ \ norm ((\n\A. 1 + f n) - 1) + norm (f x * (\n\A. 1 + f n))" by (rule norm_triangle_ineq) also have "norm (f x * (\n\A. 1 + f n)) = norm (f x) * (\x\A. norm (1 + f x))" by (simp add: prod_norm norm_mult) also have "(\x\A. norm (1 + f x)) \ (\x\A. norm (1::'a) + norm (f x))" by (intro prod_mono norm_triangle_ineq ballI conjI) auto also have "norm (1::'a) = 1" by simp also note insert.IH also have "(\n\A. 1 + norm (f n)) - 1 + norm (f x) * (\x\A. 1 + norm (f x)) = (\n\insert x A. 1 + norm (f n)) - 1" using insert.hyps by (simp add: algebra_simps) finally show ?case by - (simp_all add: mult_left_mono) qed simp_all lemma convergent_prod_imp_ev_nonzero: fixes f :: "nat \ 'a :: {t2_space,comm_semiring_1}" assumes "convergent_prod f" shows "eventually (\n. f n \ 0) sequentially" using assms by (auto simp: eventually_at_top_linorder convergent_prod_altdef) lemma convergent_prod_imp_LIMSEQ: fixes f :: "nat \ 'a :: {real_normed_field}" assumes "convergent_prod f" shows "f \ 1" proof - from assms obtain M L where L: "(\n. \i\n. f (i+M)) \ L" "\n. n \ M \ f n \ 0" "L \ 0" by (auto simp: convergent_prod_altdef) hence L': "(\n. \i\Suc n. f (i+M)) \ L" by (subst filterlim_sequentially_Suc) have "(\n. (\i\Suc n. f (i+M)) / (\i\n. f (i+M))) \ L / L" using L L' by (intro tendsto_divide) simp_all also from L have "L / L = 1" by simp also have "(\n. (\i\Suc n. f (i+M)) / (\i\n. f (i+M))) = (\n. f (n + Suc M))" using assms L by (auto simp: fun_eq_iff atMost_Suc) finally show ?thesis by (rule LIMSEQ_offset) qed lemma abs_convergent_prod_imp_summable: fixes f :: "nat \ 'a :: real_normed_div_algebra" assumes "abs_convergent_prod f" shows "summable (\i. norm (f i - 1))" proof - from assms have "convergent (\n. \i\n. 1 + norm (f i - 1))" unfolding abs_convergent_prod_def by (rule convergent_prod_imp_convergent) then obtain L where L: "(\n. \i\n. 1 + norm (f i - 1)) \ L" unfolding convergent_def by blast have "convergent (\n. \i\n. norm (f i - 1))" proof (rule Bseq_monoseq_convergent) have "eventually (\n. (\i\n. 1 + norm (f i - 1)) < L + 1) sequentially" using L(1) by (rule order_tendstoD) simp_all hence "\\<^sub>F x in sequentially. norm (\i\x. norm (f i - 1)) \ L + 1" proof eventually_elim case (elim n) have "norm (\i\n. norm (f i - 1)) = (\i\n. norm (f i - 1))" unfolding real_norm_def by (intro abs_of_nonneg sum_nonneg) simp_all also have "\ \ (\i\n. 1 + norm (f i - 1))" by (rule sum_le_prod) auto also have "\ < L + 1" by (rule elim) finally show ?case by simp qed thus "Bseq (\n. \i\n. norm (f i - 1))" by (rule BfunI) next show "monoseq (\n. \i\n. norm (f i - 1))" by (rule mono_SucI1) auto qed thus "summable (\i. norm (f i - 1))" by (simp add: summable_iff_convergent') qed lemma summable_imp_abs_convergent_prod: fixes f :: "nat \ 'a :: real_normed_div_algebra" assumes "summable (\i. norm (f i - 1))" shows "abs_convergent_prod f" proof (intro abs_convergent_prodI Bseq_monoseq_convergent) show "monoseq (\n. \i\n. 1 + norm (f i - 1))" by (intro mono_SucI1) (auto simp: atMost_Suc algebra_simps intro!: mult_nonneg_nonneg prod_nonneg) next show "Bseq (\n. \i\n. 1 + norm (f i - 1))" proof (rule Bseq_eventually_mono) show "eventually (\n. norm (\i\n. 1 + norm (f i - 1)) \ norm (exp (\i\n. norm (f i - 1)))) sequentially" by (intro always_eventually allI) (auto simp: abs_prod exp_sum intro!: prod_mono) next from assms have "(\n. \i\n. norm (f i - 1)) \ (\i. norm (f i - 1))" using sums_def_le by blast hence "(\n. exp (\i\n. norm (f i - 1))) \ exp (\i. norm (f i - 1))" by (rule tendsto_exp) hence "convergent (\n. exp (\i\n. norm (f i - 1)))" by (rule convergentI) thus "Bseq (\n. exp (\i\n. norm (f i - 1)))" by (rule convergent_imp_Bseq) qed qed theorem abs_convergent_prod_conv_summable: fixes f :: "nat \ 'a :: real_normed_div_algebra" shows "abs_convergent_prod f \ summable (\i. norm (f i - 1))" by (blast intro: abs_convergent_prod_imp_summable summable_imp_abs_convergent_prod) lemma abs_convergent_prod_imp_LIMSEQ: fixes f :: "nat \ 'a :: {comm_ring_1,real_normed_div_algebra}" assumes "abs_convergent_prod f" shows "f \ 1" proof - from assms have "summable (\n. norm (f n - 1))" by (rule abs_convergent_prod_imp_summable) from summable_LIMSEQ_zero[OF this] have "(\n. f n - 1) \ 0" by (simp add: tendsto_norm_zero_iff) from tendsto_add[OF this tendsto_const[of 1]] show ?thesis by simp qed lemma abs_convergent_prod_imp_ev_nonzero: fixes f :: "nat \ 'a :: {comm_ring_1,real_normed_div_algebra}" assumes "abs_convergent_prod f" shows "eventually (\n. f n \ 0) sequentially" proof - from assms have "f \ 1" by (rule abs_convergent_prod_imp_LIMSEQ) hence "eventually (\n. dist (f n) 1 < 1) at_top" by (auto simp: tendsto_iff) thus ?thesis by eventually_elim auto qed subsection\<^marker>\tag unimportant\ \Ignoring initial segments\ lemma convergent_prod_offset: assumes "convergent_prod (\n. f (n + m))" shows "convergent_prod f" proof - from assms obtain M L where "(\n. \k\n. f (k + (M + m))) \ L" "L \ 0" by (auto simp: prod_defs add.assoc) thus "convergent_prod f" unfolding prod_defs by blast qed lemma abs_convergent_prod_offset: assumes "abs_convergent_prod (\n. f (n + m))" shows "abs_convergent_prod f" using assms unfolding abs_convergent_prod_def by (rule convergent_prod_offset) lemma raw_has_prod_ignore_initial_segment: fixes f :: "nat \ 'a :: real_normed_field" assumes "raw_has_prod f M p" "N \ M" obtains q where "raw_has_prod f N q" proof - have p: "(\n. \k\n. f (k + M)) \ p" and "p \ 0" using assms by (auto simp: raw_has_prod_def) then have nz: "\n. n \ M \ f n \ 0" using assms by (auto simp: raw_has_prod_eq_0) define C where "C = (\k 0" by (auto simp: C_def) from p have "(\i. \k\i + (N-M). f (k + M)) \ p" by (rule LIMSEQ_ignore_initial_segment) also have "(\i. \k\i + (N-M). f (k + M)) = (\n. C * (\k\n. f (k + N)))" proof (rule ext, goal_cases) case (1 n) have "{..n+(N-M)} = {..<(N-M)} \ {(N-M)..n+(N-M)}" by auto also have "(\k\\. f (k + M)) = C * (\k=(N-M)..n+(N-M). f (k + M))" unfolding C_def by (rule prod.union_disjoint) auto also have "(\k=(N-M)..n+(N-M). f (k + M)) = (\k\n. f (k + (N-M) + M))" by (intro ext prod.reindex_bij_witness[of _ "\k. k + (N-M)" "\k. k - (N-M)"]) auto finally show ?case using \N \ M\ by (simp add: add_ac) qed finally have "(\n. C * (\k\n. f (k + N)) / C) \ p / C" by (intro tendsto_divide tendsto_const) auto hence "(\n. \k\n. f (k + N)) \ p / C" by simp moreover from \p \ 0\ have "p / C \ 0" by simp ultimately show ?thesis using raw_has_prod_def that by blast qed corollary\<^marker>\tag unimportant\ convergent_prod_ignore_initial_segment: fixes f :: "nat \ 'a :: real_normed_field" assumes "convergent_prod f" shows "convergent_prod (\n. f (n + m))" using assms unfolding convergent_prod_def apply clarify apply (erule_tac N="M+m" in raw_has_prod_ignore_initial_segment) apply (auto simp add: raw_has_prod_def add_ac) done corollary\<^marker>\tag unimportant\ convergent_prod_ignore_nonzero_segment: fixes f :: "nat \ 'a :: real_normed_field" assumes f: "convergent_prod f" and nz: "\i. i \ M \ f i \ 0" shows "\p. raw_has_prod f M p" using convergent_prod_ignore_initial_segment [OF f] by (metis convergent_LIMSEQ_iff convergent_prod_iff_convergent le_add_same_cancel2 nz prod_defs(1) zero_order(1)) corollary\<^marker>\tag unimportant\ abs_convergent_prod_ignore_initial_segment: assumes "abs_convergent_prod f" shows "abs_convergent_prod (\n. f (n + m))" using assms unfolding abs_convergent_prod_def by (rule convergent_prod_ignore_initial_segment) subsection\More elementary properties\ theorem abs_convergent_prod_imp_convergent_prod: fixes f :: "nat \ 'a :: {real_normed_div_algebra,complete_space,comm_ring_1}" assumes "abs_convergent_prod f" shows "convergent_prod f" proof - from assms have "eventually (\n. f n \ 0) sequentially" by (rule abs_convergent_prod_imp_ev_nonzero) then obtain N where N: "f n \ 0" if "n \ N" for n by (auto simp: eventually_at_top_linorder) let ?P = "\n. \i\n. f (i + N)" and ?Q = "\n. \i\n. 1 + norm (f (i + N) - 1)" have "Cauchy ?P" proof (rule CauchyI', goal_cases) case (1 \) from assms have "abs_convergent_prod (\n. f (n + N))" by (rule abs_convergent_prod_ignore_initial_segment) hence "Cauchy ?Q" unfolding abs_convergent_prod_def by (intro convergent_Cauchy convergent_prod_imp_convergent) from CauchyD[OF this 1] obtain M where M: "norm (?Q m - ?Q n) < \" if "m \ M" "n \ M" for m n by blast show ?case proof (rule exI[of _ M], safe, goal_cases) case (1 m n) have "dist (?P m) (?P n) = norm (?P n - ?P m)" by (simp add: dist_norm norm_minus_commute) also from 1 have "{..n} = {..m} \ {m<..n}" by auto hence "norm (?P n - ?P m) = norm (?P m * (\k\{m<..n}. f (k + N)) - ?P m)" by (subst prod.union_disjoint [symmetric]) (auto simp: algebra_simps) also have "\ = norm (?P m * ((\k\{m<..n}. f (k + N)) - 1))" by (simp add: algebra_simps) also have "\ = (\k\m. norm (f (k + N))) * norm ((\k\{m<..n}. f (k + N)) - 1)" by (simp add: norm_mult prod_norm) also have "\ \ ?Q m * ((\k\{m<..n}. 1 + norm (f (k + N) - 1)) - 1)" using norm_prod_minus1_le_prod_minus1[of "\k. f (k + N) - 1" "{m<..n}"] norm_triangle_ineq[of 1 "f k - 1" for k] by (intro mult_mono prod_mono ballI conjI norm_prod_minus1_le_prod_minus1 prod_nonneg) auto also have "\ = ?Q m * (\k\{m<..n}. 1 + norm (f (k + N) - 1)) - ?Q m" by (simp add: algebra_simps) also have "?Q m * (\k\{m<..n}. 1 + norm (f (k + N) - 1)) = (\k\{..m}\{m<..n}. 1 + norm (f (k + N) - 1))" by (rule prod.union_disjoint [symmetric]) auto also from 1 have "{..m}\{m<..n} = {..n}" by auto also have "?Q n - ?Q m \ norm (?Q n - ?Q m)" by simp also from 1 have "\ < \" by (intro M) auto finally show ?case . qed qed hence conv: "convergent ?P" by (rule Cauchy_convergent) then obtain L where L: "?P \ L" by (auto simp: convergent_def) have "L \ 0" proof assume [simp]: "L = 0" from tendsto_norm[OF L] have limit: "(\n. \k\n. norm (f (k + N))) \ 0" by (simp add: prod_norm) from assms have "(\n. f (n + N)) \ 1" by (intro abs_convergent_prod_imp_LIMSEQ abs_convergent_prod_ignore_initial_segment) hence "eventually (\n. norm (f (n + N) - 1) < 1) sequentially" by (auto simp: tendsto_iff dist_norm) then obtain M0 where M0: "norm (f (n + N) - 1) < 1" if "n \ M0" for n by (auto simp: eventually_at_top_linorder) { fix M assume M: "M \ M0" with M0 have M: "norm (f (n + N) - 1) < 1" if "n \ M" for n using that by simp have "(\n. \k\n. 1 - norm (f (k+M+N) - 1)) \ 0" proof (rule tendsto_sandwich) show "eventually (\n. (\k\n. 1 - norm (f (k+M+N) - 1)) \ 0) sequentially" using M by (intro always_eventually prod_nonneg allI ballI) (auto intro: less_imp_le) have "norm (1::'a) - norm (f (i + M + N) - 1) \ norm (f (i + M + N))" for i using norm_triangle_ineq3[of "f (i + M + N)" 1] by simp thus "eventually (\n. (\k\n. 1 - norm (f (k+M+N) - 1)) \ (\k\n. norm (f (k+M+N)))) at_top" using M by (intro always_eventually allI prod_mono ballI conjI) (auto intro: less_imp_le) define C where "C = (\k 0" by (auto simp: C_def) from L have "(\n. norm (\k\n+M. f (k + N))) \ 0" by (intro LIMSEQ_ignore_initial_segment) (simp add: tendsto_norm_zero_iff) also have "(\n. norm (\k\n+M. f (k + N))) = (\n. C * (\k\n. norm (f (k + M + N))))" proof (rule ext, goal_cases) case (1 n) have "{..n+M} = {.. {M..n+M}" by auto also have "norm (\k\\. f (k + N)) = C * norm (\k=M..n+M. f (k + N))" unfolding C_def by (subst prod.union_disjoint) (auto simp: norm_mult prod_norm) also have "(\k=M..n+M. f (k + N)) = (\k\n. f (k + N + M))" by (intro prod.reindex_bij_witness[of _ "\i. i + M" "\i. i - M"]) auto finally show ?case by (simp add: add_ac prod_norm) qed finally have "(\n. C * (\k\n. norm (f (k + M + N))) / C) \ 0 / C" by (intro tendsto_divide tendsto_const) auto thus "(\n. \k\n. norm (f (k + M + N))) \ 0" by simp qed simp_all have "1 - (\i. norm (f (i + M + N) - 1)) \ 0" proof (rule tendsto_le) show "eventually (\n. 1 - (\k\n. norm (f (k+M+N) - 1)) \ (\k\n. 1 - norm (f (k+M+N) - 1))) at_top" using M by (intro always_eventually allI Weierstrass_prod_ineq) (auto intro: less_imp_le) show "(\n. \k\n. 1 - norm (f (k+M+N) - 1)) \ 0" by fact show "(\n. 1 - (\k\n. norm (f (k + M + N) - 1))) \ 1 - (\i. norm (f (i + M + N) - 1))" by (intro tendsto_intros summable_LIMSEQ' summable_ignore_initial_segment abs_convergent_prod_imp_summable assms) qed simp_all hence "(\i. norm (f (i + M + N) - 1)) \ 1" by simp also have "\ + (\ii. norm (f (i + N) - 1))" by (intro suminf_split_initial_segment [symmetric] summable_ignore_initial_segment abs_convergent_prod_imp_summable assms) finally have "1 + (\i (\i. norm (f (i + N) - 1))" by simp } note * = this have "1 + (\i. norm (f (i + N) - 1)) \ (\i. norm (f (i + N) - 1))" proof (rule tendsto_le) show "(\M. 1 + (\i 1 + (\i. norm (f (i + N) - 1))" by (intro tendsto_intros summable_LIMSEQ summable_ignore_initial_segment abs_convergent_prod_imp_summable assms) show "eventually (\M. 1 + (\i (\i. norm (f (i + N) - 1))) at_top" using eventually_ge_at_top[of M0] by eventually_elim (use * in auto) qed simp_all thus False by simp qed with L show ?thesis by (auto simp: prod_defs) qed lemma raw_has_prod_cases: fixes f :: "nat \ 'a :: {idom,topological_semigroup_mult,t2_space}" assumes "raw_has_prod f M p" obtains i where "in. \i\n. f (i + M)) \ p" "p \ 0" using assms unfolding raw_has_prod_def by blast+ then have "(\n. prod f {..i\n. f (i + M))) \ prod f {..i\n. f (i + M)) = prod f {..n+M}" for n proof - have "{..n+M} = {.. {M..n+M}" by auto then have "prod f {..n+M} = prod f {.. = prod f {..i\n. f (i + M))" by (metis (mono_tags, lifting) add.left_neutral atMost_atLeast0 prod.shift_bounds_cl_nat_ivl) finally show ?thesis by metis qed ultimately have "(\n. prod f {..n}) \ prod f {..i 0" using \p \ 0\ assms that by (auto simp: raw_has_prod_def) then show thesis using that by blast qed corollary convergent_prod_offset_0: fixes f :: "nat \ 'a :: {idom,topological_semigroup_mult,t2_space}" assumes "convergent_prod f" "\i. f i \ 0" shows "\p. raw_has_prod f 0 p" using assms convergent_prod_def raw_has_prod_cases by blast lemma prodinf_eq_lim: fixes f :: "nat \ 'a :: {idom,topological_semigroup_mult,t2_space}" assumes "convergent_prod f" "\i. f i \ 0" shows "prodinf f = lim (\n. \i\n. f i)" using assms convergent_prod_offset_0 [OF assms] by (simp add: prod_defs lim_def) (metis (no_types) assms(1) convergent_prod_to_zero_iff) lemma has_prod_one[simp, intro]: "(\n. 1) has_prod 1" unfolding prod_defs by auto lemma convergent_prod_one[simp, intro]: "convergent_prod (\n. 1)" unfolding prod_defs by auto lemma prodinf_cong: "(\n. f n = g n) \ prodinf f = prodinf g" by presburger lemma convergent_prod_cong: fixes f g :: "nat \ 'a::{field,topological_semigroup_mult,t2_space}" assumes ev: "eventually (\x. f x = g x) sequentially" and f: "\i. f i \ 0" and g: "\i. g i \ 0" shows "convergent_prod f = convergent_prod g" proof - from assms obtain N where N: "\n\N. f n = g n" by (auto simp: eventually_at_top_linorder) define C where "C = (\k 0" by (simp add: f) have *: "eventually (\n. prod f {..n} = C * prod g {..n}) sequentially" using eventually_ge_at_top[of N] proof eventually_elim case (elim n) then have "{..n} = {.. {N..n}" by auto also have "prod f \ = prod f {.. {N..n})" by (intro prod.union_disjoint [symmetric]) auto also from elim have "{.. {N..n} = {..n}" by auto finally show "prod f {..n} = C * prod g {..n}" . qed then have cong: "convergent (\n. prod f {..n}) = convergent (\n. C * prod g {..n})" by (rule convergent_cong) show ?thesis proof assume cf: "convergent_prod f" with f have "\ (\n. prod f {..n}) \ 0" by simp then have "\ (\n. prod g {..n}) \ 0" using * \C \ 0\ filterlim_cong by fastforce then show "convergent_prod g" by (metis convergent_mult_const_iff \C \ 0\ cong cf convergent_LIMSEQ_iff convergent_prod_iff_convergent convergent_prod_imp_convergent g) next assume cg: "convergent_prod g" have "\a. C * a \ 0 \ (\n. prod g {..n}) \ a" by (metis (no_types) \C \ 0\ cg convergent_prod_iff_nz_lim divide_eq_0_iff g nonzero_mult_div_cancel_right) then show "convergent_prod f" using "*" tendsto_mult_left filterlim_cong by (fastforce simp add: convergent_prod_iff_nz_lim f) qed qed lemma has_prod_finite: fixes f :: "nat \ 'a::{semidom,t2_space}" assumes [simp]: "finite N" and f: "\n. n \ N \ f n = 1" shows "f has_prod (\n\N. f n)" proof - have eq: "prod f {..n + Suc (Max N)} = prod f N" for n proof (rule prod.mono_neutral_right) show "N \ {..n + Suc (Max N)}" by (auto simp: le_Suc_eq trans_le_add2) show "\i\{..n + Suc (Max N)} - N. f i = 1" using f by blast qed auto show ?thesis proof (cases "\n\N. f n \ 0") case True then have "prod f N \ 0" by simp moreover have "(\n. prod f {..n}) \ prod f N" by (rule LIMSEQ_offset[of _ "Suc (Max N)"]) (simp add: eq atLeast0LessThan del: add_Suc_right) ultimately show ?thesis by (simp add: raw_has_prod_def has_prod_def) next case False then obtain k where "k \ N" "f k = 0" by auto let ?Z = "{n \ N. f n = 0}" have maxge: "Max ?Z \ n" if "f n = 0" for n using Max_ge [of ?Z] \finite N\ \f n = 0\ by (metis (mono_tags) Collect_mem_eq f finite_Collect_conjI mem_Collect_eq zero_neq_one) let ?q = "prod f {Suc (Max ?Z)..Max N}" have [simp]: "?q \ 0" using maxge Suc_n_not_le_n le_trans by force have eq: "(\i\n + Max N. f (Suc (i + Max ?Z))) = ?q" for n proof - have "(\i\n + Max N. f (Suc (i + Max ?Z))) = prod f {Suc (Max ?Z)..n + Max N + Suc (Max ?Z)}" proof (rule prod.reindex_cong [where l = "\i. i + Suc (Max ?Z)", THEN sym]) show "{Suc (Max ?Z)..n + Max N + Suc (Max ?Z)} = (\i. i + Suc (Max ?Z))  {..n + Max N}" using le_Suc_ex by fastforce qed (auto simp: inj_on_def) also have "\ = ?q" by (rule prod.mono_neutral_right) (use Max.coboundedI [OF \finite N\] f in \force+\) finally show ?thesis . qed have q: "raw_has_prod f (Suc (Max ?Z)) ?q" proof (simp add: raw_has_prod_def) show "(\n. \i\n. f (Suc (i + Max ?Z))) \ ?q" by (rule LIMSEQ_offset[of _ "(Max N)"]) (simp add: eq) qed show ?thesis unfolding has_prod_def proof (intro disjI2 exI conjI) show "prod f N = 0" using \f k = 0\ \k \ N\ \finite N\ prod_zero by blast show "f (Max ?Z) = 0" using Max_in [of ?Z] \finite N\ \f k = 0\ \k \ N\ by auto qed (use q in auto) qed qed corollary\<^marker>\tag unimportant\ has_prod_0: fixes f :: "nat \ 'a::{semidom,t2_space}" assumes "\n. f n = 1" shows "f has_prod 1" by (simp add: assms has_prod_cong) lemma prodinf_zero[simp]: "prodinf (\n. 1::'a::real_normed_field) = 1" using has_prod_unique by force lemma convergent_prod_finite: fixes f :: "nat \ 'a::{idom,t2_space}" assumes "finite N" "\n. n \ N \ f n = 1" shows "convergent_prod f" proof - have "\n p. raw_has_prod f n p" using assms has_prod_def has_prod_finite by blast then show ?thesis by (simp add: convergent_prod_def) qed lemma has_prod_If_finite_set: fixes f :: "nat \ 'a::{idom,t2_space}" shows "finite A \ (\r. if r \ A then f r else 1) has_prod (\r\A. f r)" using has_prod_finite[of A "(\r. if r \ A then f r else 1)"] by simp lemma has_prod_If_finite: fixes f :: "nat \ 'a::{idom,t2_space}" shows "finite {r. P r} \ (\r. if P r then f r else 1) has_prod (\r | P r. f r)" using has_prod_If_finite_set[of "{r. P r}"] by simp lemma convergent_prod_If_finite_set[simp, intro]: fixes f :: "nat \ 'a::{idom,t2_space}" shows "finite A \ convergent_prod (\r. if r \ A then f r else 1)" by (simp add: convergent_prod_finite) lemma convergent_prod_If_finite[simp, intro]: fixes f :: "nat \ 'a::{idom,t2_space}" shows "finite {r. P r} \ convergent_prod (\r. if P r then f r else 1)" using convergent_prod_def has_prod_If_finite has_prod_def by fastforce lemma has_prod_single: fixes f :: "nat \ 'a::{idom,t2_space}" shows "(\r. if r = i then f r else 1) has_prod f i" using has_prod_If_finite[of "\r. r = i"] by simp context fixes f :: "nat \ 'a :: real_normed_field" begin lemma convergent_prod_imp_has_prod: assumes "convergent_prod f" shows "\p. f has_prod p" proof - obtain M p where p: "raw_has_prod f M p" using assms convergent_prod_def by blast then have "p \ 0" using raw_has_prod_nonzero by blast with p have fnz: "f i \ 0" if "i \ M" for i using raw_has_prod_eq_0 that by blast define C where "C = (\nn\M. f n \ 0") case True then have "C \ 0" by (simp add: C_def) then show ?thesis by (meson True assms convergent_prod_offset_0 fnz has_prod_def nat_le_linear) next case False let ?N = "GREATEST n. f n = 0" have 0: "f ?N = 0" using fnz False by (metis (mono_tags, lifting) GreatestI_ex_nat nat_le_linear) have "f i \ 0" if "i > ?N" for i by (metis (mono_tags, lifting) Greatest_le_nat fnz leD linear that) then have "\p. raw_has_prod f (Suc ?N) p" using assms by (auto simp: intro!: convergent_prod_ignore_nonzero_segment) then show ?thesis unfolding has_prod_def using 0 by blast qed qed lemma convergent_prod_has_prod [intro]: shows "convergent_prod f \ f has_prod (prodinf f)" unfolding prodinf_def by (metis convergent_prod_imp_has_prod has_prod_unique theI') lemma convergent_prod_LIMSEQ: shows "convergent_prod f \ (\n. \i\n. f i) \ prodinf f" by (metis convergent_LIMSEQ_iff convergent_prod_has_prod convergent_prod_imp_convergent convergent_prod_to_zero_iff raw_has_prod_eq_0 has_prod_def prodinf_eq_lim zero_le) theorem has_prod_iff: "f has_prod x \ convergent_prod f \ prodinf f = x" proof assume "f has_prod x" then show "convergent_prod f \ prodinf f = x" apply safe using convergent_prod_def has_prod_def apply blast using has_prod_unique by blast qed auto lemma convergent_prod_has_prod_iff: "convergent_prod f \ f has_prod prodinf f" by (auto simp: has_prod_iff convergent_prod_has_prod) lemma prodinf_finite: assumes N: "finite N" and f: "\n. n \ N \ f n = 1" shows "prodinf f = (\n\N. f n)" using has_prod_finite[OF assms, THEN has_prod_unique] by simp end subsection\<^marker>\tag unimportant\ \Infinite products on ordered topological monoids\ lemma LIMSEQ_prod_0: fixes f :: "nat \ 'a::{semidom,topological_space}" assumes "f i = 0" shows "(\n. prod f {..n}) \ 0" proof (subst tendsto_cong) show "\\<^sub>F n in sequentially. prod f {..n} = 0" proof show "prod f {..n} = 0" if "n \ i" for n using that assms by auto qed qed auto lemma LIMSEQ_prod_nonneg: fixes f :: "nat \ 'a::{linordered_semidom,linorder_topology}" assumes 0: "\n. 0 \ f n" and a: "(\n. prod f {..n}) \ a" shows "a \ 0" by (simp add: "0" prod_nonneg LIMSEQ_le_const [OF a]) context fixes f :: "nat \ 'a::{linordered_semidom,linorder_topology}" begin lemma has_prod_le: assumes f: "f has_prod a" and g: "g has_prod b" and le: "\n. 0 \ f n \ f n \ g n" shows "a \ b" proof (cases "a=0 \ b=0") case True then show ?thesis proof assume [simp]: "a=0" have "b \ 0" proof (rule LIMSEQ_prod_nonneg) show "(\n. prod g {..n}) \ b" using g by (auto simp: has_prod_def raw_has_prod_def LIMSEQ_prod_0) qed (use le order_trans in auto) then show ?thesis by auto next assume [simp]: "b=0" then obtain i where "g i = 0" using g by (auto simp: prod_defs) then have "f i = 0" using antisym le by force then have "a=0" using f by (auto simp: prod_defs LIMSEQ_prod_0 LIMSEQ_unique) then show ?thesis by auto qed next case False then show ?thesis using assms unfolding has_prod_def raw_has_prod_def by (force simp: LIMSEQ_prod_0 intro!: LIMSEQ_le prod_mono) qed lemma prodinf_le: assumes f: "f has_prod a" and g: "g has_prod b" and le: "\n. 0 \ f n \ f n \ g n" shows "prodinf f \ prodinf g" using has_prod_le [OF assms] has_prod_unique f g by blast end lemma prod_le_prodinf: fixes f :: "nat \ 'a::{linordered_idom,linorder_topology}" assumes "f has_prod a" "\i. 0 \ f i" "\i. i\n \ 1 \ f i" shows "prod f {.. prodinf f" by(rule has_prod_le[OF has_prod_If_finite_set]) (use assms has_prod_unique in auto) lemma prodinf_nonneg: fixes f :: "nat \ 'a::{linordered_idom,linorder_topology}" assumes "f has_prod a" "\i. 1 \ f i" shows "1 \ prodinf f" using prod_le_prodinf[of f a 0] assms by (metis order_trans prod_ge_1 zero_le_one) lemma prodinf_le_const: fixes f :: "nat \ real" assumes "convergent_prod f" "\n. prod f {.. x" shows "prodinf f \ x" by (metis lessThan_Suc_atMost assms convergent_prod_LIMSEQ LIMSEQ_le_const2) lemma prodinf_eq_one_iff [simp]: fixes f :: "nat \ real" assumes f: "convergent_prod f" and ge1: "\n. 1 \ f n" shows "prodinf f = 1 \ (\n. f n = 1)" proof assume "prodinf f = 1" then have "(\n. \i 1" using convergent_prod_LIMSEQ[of f] assms by (simp add: LIMSEQ_lessThan_iff_atMost) then have "\i. (\n\{i}. f n) \ 1" proof (rule LIMSEQ_le_const) have "1 \ prod f n" for n by (simp add: ge1 prod_ge_1) 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) then have "(\n\{i}. f n) \ prod f {.. Suc i" for i n by (metis mult.left_neutral order_refl prod.cong prod.neutral_const prod.lessThan_Suc) then show "\N. \n\N. (\n\{i}. f n) \ prod f {..n. f n = 1" by (auto intro!: antisym) qed (metis prodinf_zero fun_eq_iff) lemma prodinf_pos_iff: fixes f :: "nat \ real" assumes "convergent_prod f" "\n. 1 \ f n" shows "1 < prodinf f \ (\i. 1 < f i)" using prod_le_prodinf[of f 1] prodinf_eq_one_iff by (metis convergent_prod_has_prod assms less_le prodinf_nonneg) lemma less_1_prodinf2: fixes f :: "nat \ real" assumes "convergent_prod f" "\n. 1 \ f n" "1 < f i" shows "1 < prodinf f" proof - have "1 < (\n \ prodinf f" by (intro prod_le_prodinf) (use assms order_trans zero_le_one in \blast+\) finally show ?thesis . qed lemma less_1_prodinf: fixes f :: "nat \ real" shows "\convergent_prod f; \n. 1 < f n\ \ 1 < prodinf f" by (intro less_1_prodinf2[where i=1]) (auto intro: less_imp_le) lemma prodinf_nonzero: fixes f :: "nat \ 'a :: {idom,topological_semigroup_mult,t2_space}" assumes "convergent_prod f" "\i. f i \ 0" shows "prodinf f \ 0" by (metis assms convergent_prod_offset_0 has_prod_unique raw_has_prod_def has_prod_def) lemma less_0_prodinf: fixes f :: "nat \ real" assumes f: "convergent_prod f" and 0: "\i. f i > 0" shows "0 < prodinf f" proof - have "prodinf f \ 0" by (metis assms less_irrefl prodinf_nonzero) moreover have "0 < (\n 0" using convergent_prod_LIMSEQ [OF f] LIMSEQ_prod_nonneg 0 less_le by blast ultimately show ?thesis by auto qed lemma prod_less_prodinf2: fixes f :: "nat \ real" 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" shows "prod f {.. prod f {.. prodinf f" using prod_le_prodinf[of f _ "Suc i"] by (meson "0" "1" Suc_leD convergent_prod_has_prod f \n \ i\ le_trans less_eq_real_def) ultimately show ?thesis by (metis le_less_trans mult.commute not_le prod.lessThan_Suc) qed lemma prod_less_prodinf: fixes f :: "nat \ real" assumes f: "convergent_prod f" and 1: "\m. m\n \ 1 < f m" and 0: "\m. 0 < f m" shows "prod f {.. real" assumes pos: "\n. 1 \ f n" and le: "\n. (\i x" shows "\p. raw_has_prod f 0 p" unfolding raw_has_prod_def add_0_right proof (rule exI LIMSEQ_incseq_SUP conjI)+ show "bdd_above (range (\n. prod f {..n}))" by (metis bdd_aboveI2 le lessThan_Suc_atMost) then have "(SUP i. prod f {..i}) > 0" by (metis UNIV_I cSUP_upper less_le_trans pos prod_pos zero_less_one) then show "(SUP i. prod f {..i}) \ 0" by auto show "incseq (\n. prod f {..n})" using pos order_trans [OF zero_le_one] by (auto simp: mono_def intro!: prod_mono2) qed lemma convergent_prodI_nonneg_bounded: fixes f :: "nat \ real" assumes "\n. 1 \ f n" "\n. (\i x" shows "convergent_prod f" using convergent_prod_def raw_has_prodI_bounded [OF assms] by blast subsection\<^marker>\tag unimportant\ \Infinite products on topological spaces\ context fixes f g :: "nat \ 'a::{t2_space,topological_semigroup_mult,idom}" begin 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)" by (force simp add: prod.distrib tendsto_mult raw_has_prod_def) 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)" by (simp add: raw_has_prod_mult has_prod_def) end context fixes f g :: "nat \ 'a::real_normed_field" begin lemma has_prod_mult: assumes f: "f has_prod a" and g: "g has_prod b" shows "(\n. f n * g n) has_prod (a * b)" using f [unfolded has_prod_def] proof (elim disjE exE conjE) assume f0: "raw_has_prod f 0 a" show ?thesis using g [unfolded has_prod_def] proof (elim disjE exE conjE) assume g0: "raw_has_prod g 0 b" with f0 show ?thesis by (force simp add: has_prod_def prod.distrib tendsto_mult raw_has_prod_def) next fix j q assume "b = 0" and "g j = 0" and q: "raw_has_prod g (Suc j) q" obtain p where p: "raw_has_prod f (Suc j) p" using f0 raw_has_prod_ignore_initial_segment by blast then have "Ex (raw_has_prod (\n. f n * g n) (Suc j))" using q raw_has_prod_mult by blast then show ?thesis using \b = 0\ \g j = 0\ has_prod_0_iff by fastforce qed next fix i p assume "a = 0" and "f i = 0" and p: "raw_has_prod f (Suc i) p" show ?thesis using g [unfolded has_prod_def] proof (elim disjE exE conjE) assume g0: "raw_has_prod g 0 b" obtain q where q: "raw_has_prod g (Suc i) q" using g0 raw_has_prod_ignore_initial_segment by blast then have "Ex (raw_has_prod (\n. f n * g n) (Suc i))" using raw_has_prod_mult p by blast then show ?thesis using \a = 0\ \f i = 0\ has_prod_0_iff by fastforce next fix j q assume "b = 0" and "g j = 0" and q: "raw_has_prod g (Suc j) q" obtain p' where p': "raw_has_prod f (Suc (max i j)) p'" by (metis raw_has_prod_ignore_initial_segment max_Suc_Suc max_def p) moreover obtain q' where q': "raw_has_prod g (Suc (max i j)) q'" by (metis raw_has_prod_ignore_initial_segment max.cobounded2 max_Suc_Suc q) ultimately show ?thesis using \b = 0\ by (simp add: has_prod_def) (metis \f i = 0\ \g j = 0\ raw_has_prod_mult max_def) qed qed lemma convergent_prod_mult: assumes f: "convergent_prod f" and g: "convergent_prod g" shows "convergent_prod (\n. f n * g n)" unfolding convergent_prod_def proof - obtain M p N q where p: "raw_has_prod f M p" and q: "raw_has_prod g N q" using convergent_prod_def f g by blast+ then obtain p' q' where p': "raw_has_prod f (max M N) p'" and q': "raw_has_prod g (max M N) q'" by (meson raw_has_prod_ignore_initial_segment max.cobounded1 max.cobounded2) then show "\M p. raw_has_prod (\n. f n * g n) M p" using raw_has_prod_mult by blast qed lemma prodinf_mult: "convergent_prod f \ convergent_prod g \ prodinf f * prodinf g = (\n. f n * g n)" by (intro has_prod_unique has_prod_mult convergent_prod_has_prod) end context fixes f :: "'i \ nat \ 'a::real_normed_field" and I :: "'i set" begin 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)" by (induct I rule: infinite_finite_induct) (auto intro!: has_prod_mult) lemma prodinf_prod: "(\i. i \ I \ convergent_prod (f i)) \ (\n. \i\I. f i n) = (\i\I. \n. f i n)" using has_prod_unique[OF has_prod_prod, OF convergent_prod_has_prod] by simp lemma convergent_prod_prod: "(\i. i \ I \ convergent_prod (f i)) \ convergent_prod (\n. \i\I. f i n)" using convergent_prod_has_prod_iff has_prod_prod prodinf_prod by force end subsection\<^marker>\tag unimportant\ \Infinite summability on real normed fields\ context fixes f :: "nat \ 'a::real_normed_field" begin 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" proof - have "raw_has_prod f M (a * f M) \ (\i. \j\Suc i. f (j+M)) \ a * f M \ a * f M \ 0" by (subst filterlim_sequentially_Suc) (simp add: raw_has_prod_def) also have "\ \ (\i. (\j\i. f (Suc j + M)) * f M) \ a * f M \ a * f M \ 0" by (simp add: ac_simps atMost_Suc_eq_insert_0 image_Suc_atMost prod.atLeast1_atMost_eq lessThan_Suc_atMost del: prod.cl_ivl_Suc) also have "\ \ raw_has_prod (\n. f (Suc n)) M a \ f M \ 0" proof safe assume tends: "(\i. (\j\i. f (Suc j + M)) * f M) \ a * f M" and 0: "a * f M \ 0" with tendsto_divide[OF tends tendsto_const, of "f M"] show "raw_has_prod (\n. f (Suc n)) M a" by (simp add: raw_has_prod_def) qed (auto intro: tendsto_mult_right simp: raw_has_prod_def) finally show ?thesis . qed lemma has_prod_Suc_iff: assumes "f 0 \ 0" shows "(\n. f (Suc n)) has_prod a \ f has_prod (a * f 0)" proof (cases "a = 0") case True then show ?thesis proof (simp add: has_prod_def, safe) fix i x assume "f (Suc i) = 0" and "raw_has_prod (\n. f (Suc n)) (Suc i) x" then obtain y where "raw_has_prod f (Suc (Suc i)) y" 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) then show "\i. f i = 0 \ Ex (raw_has_prod f (Suc i))" using \f (Suc i) = 0\ by blast next fix i x assume "f i = 0" and x: "raw_has_prod f (Suc i) x" then obtain j where j: "i = Suc j" by (metis assms not0_implies_Suc) moreover have "\ y. raw_has_prod (\n. f (Suc n)) i y" using x by (auto simp: raw_has_prod_def) then show "\i. f (Suc i) = 0 \ Ex (raw_has_prod (\n. f (Suc n)) (Suc i))" using \f i = 0\ j by blast qed next case False then show ?thesis by (auto simp: has_prod_def raw_has_prod_Suc_iff assms) qed lemma convergent_prod_Suc_iff [simp]: shows "convergent_prod (\n. f (Suc n)) = convergent_prod f" proof assume "convergent_prod f" then obtain M L where M_nz:"\n\M. f n \ 0" and M_L:"(\n. \i\n. f (i + M)) \ L" and "L \ 0" unfolding convergent_prod_altdef by auto have "(\n. \i\n. f (Suc (i + M))) \ L / f M" proof - have "(\n. \i\{0..Suc n}. f (i + M)) \ L" using M_L apply (subst (asm) filterlim_sequentially_Suc[symmetric]) using atLeast0AtMost by auto then have "(\n. f M * (\i\{0..n}. f (Suc (i + M)))) \ L" apply (subst (asm) prod.atLeast0_atMost_Suc_shift) by simp then have "(\n. (\i\{0..n}. f (Suc (i + M)))) \ L/f M" apply (drule_tac tendsto_divide) using M_nz[rule_format,of M,simplified] by auto then show ?thesis unfolding atLeast0AtMost . qed then show "convergent_prod (\n. f (Suc n))" unfolding convergent_prod_altdef apply (rule_tac exI[where x=M]) apply (rule_tac exI[where x="L/f M"]) using M_nz \L\0\ by auto next assume "convergent_prod (\n. f (Suc n))" then obtain M where "\L. (\n\M. f (Suc n) \ 0) \ (\n. \i\n. f (Suc (i + M))) \ L \ L \ 0" unfolding convergent_prod_altdef by auto then show "convergent_prod f" unfolding convergent_prod_altdef apply (rule_tac exI[where x="Suc M"]) using Suc_le_D by auto qed lemma raw_has_prod_inverse: assumes "raw_has_prod f M a" shows "raw_has_prod (\n. inverse (f n)) M (inverse a)" using assms unfolding raw_has_prod_def by (auto dest: tendsto_inverse simp: prod_inversef [symmetric]) lemma has_prod_inverse: assumes "f has_prod a" shows "(\n. inverse (f n)) has_prod (inverse a)" using assms raw_has_prod_inverse unfolding has_prod_def by auto lemma convergent_prod_inverse: assumes "convergent_prod f" shows "convergent_prod (\n. inverse (f n))" using assms unfolding convergent_prod_def by (blast intro: raw_has_prod_inverse elim: ) end context fixes f :: "nat \ 'a::real_normed_field" begin 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" 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) lemma has_prod_divide: "f has_prod a \ g has_prod b \ (\n. f n / g n) has_prod (a / b)" unfolding divide_inverse by (intro has_prod_inverse has_prod_mult) lemma convergent_prod_divide: assumes f: "convergent_prod f" and g: "convergent_prod g" shows "convergent_prod (\n. f n / g n)" using f g has_prod_divide has_prod_iff by blast lemma prodinf_divide: "convergent_prod f \ convergent_prod g \ prodinf f / prodinf g = (\n. f n / g n)" by (intro has_prod_unique has_prod_divide convergent_prod_has_prod) lemma prodinf_inverse: "convergent_prod f \ (\n. inverse (f n)) = inverse (\n. f n)" by (intro has_prod_unique [symmetric] has_prod_inverse convergent_prod_has_prod) lemma has_prod_Suc_imp: assumes "(\n. f (Suc n)) has_prod a" shows "f has_prod (a * f 0)" proof - have "f has_prod (a * f 0)" when "raw_has_prod (\n. f (Suc n)) 0 a" apply (cases "f 0=0") using that unfolding has_prod_def raw_has_prod_Suc by (auto simp add: raw_has_prod_Suc_iff) moreover have "f has_prod (a * f 0)" when "(\i q. a = 0 \ f (Suc i) = 0 \ raw_has_prod (\n. f (Suc n)) (Suc i) q)" proof - from that obtain i q where "a = 0" "f (Suc i) = 0" "raw_has_prod (\n. f (Suc n)) (Suc i) q" by auto then show ?thesis unfolding has_prod_def by (auto intro!:exI[where x="Suc i"] simp:raw_has_prod_Suc) qed ultimately show "f has_prod (a * f 0)" using assms unfolding has_prod_def by auto qed lemma has_prod_iff_shift: assumes "\i. i < n \ f i \ 0" 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)" by (subst has_prod_Suc_iff) auto with Suc show ?case by (simp add: ac_simps) qed corollary\<^marker>\tag unimportant\ has_prod_iff_shift': assumes "\i. i < n \ f i \ 0" shows "(\i. f (i + n)) has_prod (a / (\i f has_prod a" by (simp add: assms has_prod_iff_shift) lemma has_prod_one_iff_shift: assumes "\i. i < n \ f i = 1" shows "(\i. f (i+n)) has_prod a \ (\i. f i) has_prod a" by (simp add: assms has_prod_iff_shift) lemma convergent_prod_iff_shift [simp]: shows "convergent_prod (\i. f (i + n)) \ convergent_prod f" apply safe using convergent_prod_offset apply blast using convergent_prod_ignore_initial_segment convergent_prod_def by blast lemma has_prod_split_initial_segment: assumes "f has_prod a" "\i. i < n \ f i \ 0" shows "(\i. f (i + n)) has_prod (a / (\ii. i < n \ f i \ 0" shows "(\i. f (i + n)) = (\i. f i) / (\ii. i < n \ f i \ 0" shows "prodinf f = (\i. f (i + n)) * (\i 0" shows "(\n. f (Suc n)) = prodinf f / f 0" using prodinf_split_initial_segment[of 1] assms by simp end context fixes f :: "nat \ 'a::real_normed_field" begin lemma convergent_prod_inverse_iff [simp]: "convergent_prod (\n. inverse (f n)) \ convergent_prod f" by (auto dest: convergent_prod_inverse) lemma convergent_prod_const_iff [simp]: fixes c :: "'a :: {real_normed_field}" shows "convergent_prod (\_. c) \ c = 1" proof assume "convergent_prod (\_. c)" then show "c = 1" using convergent_prod_imp_LIMSEQ LIMSEQ_unique by blast next assume "c = 1" then show "convergent_prod (\_. c)" by auto qed lemma has_prod_power: "f has_prod a \ (\i. f i ^ n) has_prod (a ^ n)" by (induction n) (auto simp: has_prod_mult) lemma convergent_prod_power: "convergent_prod f \ convergent_prod (\i. f i ^ n)" by (induction n) (auto simp: convergent_prod_mult) lemma prodinf_power: "convergent_prod f \ prodinf (\i. f i ^ n) = prodinf f ^ n" by (metis has_prod_unique convergent_prod_imp_has_prod has_prod_power) end subsection\Exponentials and logarithms\ context fixes f :: "nat \ 'a::{real_normed_field,banach}" begin lemma sums_imp_has_prod_exp: assumes "f sums s" shows "raw_has_prod (\i. exp (f i)) 0 (exp s)" using assms continuous_on_exp [of UNIV "\x::'a. x"] using continuous_on_tendsto_compose [of UNIV exp "(\n. sum f {..n})" s] by (simp add: prod_defs sums_def_le exp_sum) lemma convergent_prod_exp: assumes "summable f" shows "convergent_prod (\i. exp (f i))" using sums_imp_has_prod_exp assms unfolding summable_def convergent_prod_def by blast lemma prodinf_exp: assumes "summable f" shows "prodinf (\i. exp (f i)) = exp (suminf f)" proof - have "f sums suminf f" using assms by blast then have "(\i. exp (f i)) has_prod exp (suminf f)" by (simp add: has_prod_def sums_imp_has_prod_exp) then show ?thesis by (rule has_prod_unique [symmetric]) qed end theorem convergent_prod_iff_summable_real: fixes a :: "nat \ real" assumes "\n. a n > 0" shows "convergent_prod (\k. 1 + a k) \ summable a" (is "?lhs = ?rhs") proof assume ?lhs then obtain p where "raw_has_prod (\k. 1 + a k) 0 p" by (metis assms add_less_same_cancel2 convergent_prod_offset_0 not_one_less_zero) then have to_p: "(\n. \k\n. 1 + a k) \ p" by (auto simp: raw_has_prod_def) moreover have le: "(\k\n. a k) \ (\k\n. 1 + a k)" for n by (rule sum_le_prod) (use assms less_le in force) have "(\k\n. 1 + a k) \ p" for n proof (rule incseq_le [OF _ to_p]) show "incseq (\n. \k\n. 1 + a k)" using assms by (auto simp: mono_def order.strict_implies_order intro!: prod_mono2) qed with le have "(\k\n. a k) \ p" for n by (metis order_trans) with assms bounded_imp_summable show ?rhs by (metis not_less order.asym) next assume R: ?rhs have "(\k\n. 1 + a k) \ exp (suminf a)" for n proof - have "(\k\n. 1 + a k) \ exp (\k\n. a k)" for n by (rule prod_le_exp_sum) (use assms less_le in force) moreover have "exp (\k\n. a k) \ exp (suminf a)" for n unfolding exp_le_cancel_iff by (meson sum_le_suminf R assms finite_atMost less_eq_real_def) ultimately show ?thesis by (meson order_trans) qed then obtain L where L: "(\n. \k\n. 1 + a k) \ L" 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) moreover have "L \ 0" proof assume "L = 0" with L have "(\n. \k\n. 1 + a k) \ 0" by simp moreover have "(\k\n. 1 + a k) > 1" for n by (simp add: assms less_1_prod) ultimately show False by (meson Lim_bounded2 not_one_le_zero less_imp_le) qed ultimately show ?lhs using assms convergent_prod_iff_nz_lim by (metis add_less_same_cancel1 less_le not_le zero_less_one) qed lemma exp_suminf_prodinf_real: fixes f :: "nat \ real" assumes ge0:"\n. f n \ 0" and ac: "abs_convergent_prod (\n. exp (f n))" shows "prodinf (\i. exp (f i)) = exp (suminf f)" proof - have "summable f" using ac unfolding abs_convergent_prod_conv_summable proof (elim summable_comparison_test') fix n have "\f n\ = f n" by (simp add: ge0) also have "\ \ exp (f n) - 1" by (metis diff_diff_add exp_ge_add_one_self ge_iff_diff_ge_0) finally show "norm (f n) \ norm (exp (f n) - 1)" by simp qed then show ?thesis by (simp add: prodinf_exp) qed lemma has_prod_imp_sums_ln_real: fixes f :: "nat \ real" assumes "raw_has_prod f 0 p" and 0: "\x. f x > 0" shows "(\i. ln (f i)) sums (ln p)" proof - have "p > 0" using assms unfolding prod_defs by (metis LIMSEQ_prod_nonneg less_eq_real_def) then show ?thesis using assms continuous_on_ln [of "{0<..}" "\x. x"] using continuous_on_tendsto_compose [of "{0<..}" ln "(\n. prod f {..n})" p] by (auto simp: prod_defs sums_def_le ln_prod order_tendstoD) qed lemma summable_ln_real: fixes f :: "nat \ real" assumes f: "convergent_prod f" and 0: "\x. f x > 0" shows "summable (\i. ln (f i))" proof - obtain M p where "raw_has_prod f M p" using f convergent_prod_def by blast then consider i where "i real" assumes f: "convergent_prod f" and 0: "\x. f x > 0" shows "suminf (\i. ln (f i)) = ln (prodinf f)" proof - have "f has_prod prodinf f" by (simp add: f has_prod_iff) then have "raw_has_prod f 0 (prodinf f)" by (metis "0" has_prod_def less_irrefl) then have "(\i. ln (f i)) sums ln (prodinf f)" using "0" has_prod_imp_sums_ln_real by blast then show ?thesis by (rule sums_unique [symmetric]) qed lemma prodinf_exp_real: fixes f :: "nat \ real" assumes f: "convergent_prod f" and 0: "\x. f x > 0" shows "prodinf f = exp (suminf (\i. ln (f i)))" by (simp add: "0" f less_0_prodinf suminf_ln_real) theorem Ln_prodinf_complex: fixes z :: "nat \ complex" assumes z: "\j. z j \ 0" and \: "\ \ 0" shows "((\n. \j\n. z j) \ \) \ (\k. (\n. (\j\n. Ln (z j))) \ Ln \ + of_int k * (of_real(2*pi) * \))" (is "?lhs = ?rhs") proof assume L: ?lhs have pnz: "(\j\n. z j) \ 0" for n using z by auto define \ where "\ \ Arg \ + 2*pi" then have "\ > pi" using Arg_def mpi_less_Im_Ln by fastforce have \_eq: "\ = cmod \ * exp (\ * \)" using Arg_def Arg_eq \ unfolding \_def by (simp add: algebra_simps exp_add) define \ where "\ \ \n. THE t. is_Arg (\j\n. z j) t \ t \ {\-pi<..\+pi}" have uniq: "\!s. is_Arg (\j\n. z j) s \ s \ {\-pi<..\+pi}" for n using Argument_exists_unique [OF pnz] by metis have \: "is_Arg (\j\n. z j) (\ n)" and \_interval: "\ n \ {\-pi<..\+pi}" for n unfolding \_def using theI' [OF uniq] by metis+ have \_pos: "\j. \ j > 0" using \_interval \\ > pi\ by simp (meson diff_gt_0_iff_gt less_trans) have "(\j\n. z j) = cmod (\j\n. z j) * exp (\ * \ n)" for n using \ by (auto simp: is_Arg_def) then have eq: "(\n. \j\n. z j) = (\n. cmod (\j\n. z j) * exp (\ * \ n))" by simp then have "(\n. (cmod (\j\n. z j)) * exp (\ * (\ n))) \ \" using L by force then obtain k where k: "(\j. \ j - of_int (k j) * (2 * pi)) \ \" using L by (subst (asm) \_eq) (auto simp add: eq z \ polar_convergence) moreover have "\\<^sub>F n in sequentially. k n = 0" proof - have *: "kj = 0" if "dist (vj - real_of_int kj * 2) V < 1" "vj \ {V - 1<..V + 1}" for kj vj V using that by (auto simp: dist_norm) have "\\<^sub>F j in sequentially. dist (\ j - of_int (k j) * (2 * pi)) \ < pi" using tendstoD [OF k] pi_gt_zero by blast then show ?thesis proof (rule eventually_mono) fix j assume d: "dist (\ j - real_of_int (k j) * (2 * pi)) \ < pi" show "k j = 0" by (rule * [of "\ j/pi" _ "\/pi"]) (use \_interval [of j] d in \simp_all add: divide_simps dist_norm\) qed qed ultimately have \to\: "\ \ \" apply (simp only: tendsto_def) apply (erule all_forward imp_forward asm_rl)+ apply (drule (1) eventually_conj) apply (auto elim: eventually_mono) done then have to0: "(\n. \\ (Suc n) - \ n\) \ 0" by (metis (full_types) diff_self filterlim_sequentially_Suc tendsto_diff tendsto_rabs_zero) have "\k. Im (\j\n. Ln (z j)) - of_int k * (2*pi) = \ n" for n proof (rule is_Arg_exp_diff_2pi) show "is_Arg (exp (\j\n. Ln (z j))) (\ n)" using pnz \ by (simp add: is_Arg_def exp_sum prod_norm) qed then have "\k. (\j\n. Im (Ln (z j))) = \ n + of_int k * (2*pi)" for n by (simp add: algebra_simps) then obtain k where k: "\n. (\j\n. Im (Ln (z j))) = \ n + of_int (k n) * (2*pi)" by metis obtain K where "\\<^sub>F n in sequentially. k n = K" proof - have k_le: "(2*pi) * \k (Suc n) - k n\ \ \\ (Suc n) - \ n\ + \Im (Ln (z (Suc n)))\" for n proof - have "(\j\Suc n. Im (Ln (z j))) - (\j\n. Im (Ln (z j))) = Im (Ln (z (Suc n)))" by simp then show ?thesis using k [of "Suc n"] k [of n] by (auto simp: abs_if algebra_simps) qed have "z \ 1" using L \ convergent_prod_iff_nz_lim z by (blast intro: convergent_prod_imp_LIMSEQ) with z have "(\n. Ln (z n)) \ Ln 1" using isCont_tendsto_compose [OF continuous_at_Ln] nonpos_Reals_one_I by blast then have "(\n. Ln (z n)) \ 0" by simp then have "(\n. \Im (Ln (z (Suc n)))\) \ 0" 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)) then have "\\<^sub>F n in sequentially. \Im (Ln (z (Suc n)))\ < 1" by (simp add: order_tendsto_iff) moreover have "\\<^sub>F n in sequentially. \\ (Suc n) - \ n\ < 1" using to0 by (simp add: order_tendsto_iff) ultimately have "\\<^sub>F n in sequentially. (2*pi) * \k (Suc n) - k n\ < 1 + 1" proof (rule eventually_elim2) fix n assume "\Im (Ln (z (Suc n)))\ < 1" and "\\ (Suc n) - \ n\ < 1" with k_le [of n] show "2 * pi * real_of_int \k (Suc n) - k n\ < 1 + 1" by linarith qed then have "\\<^sub>F n in sequentially. real_of_int\k (Suc n) - k n\ < 1" proof (rule eventually_mono) fix n :: "nat" assume "2 * pi * \k (Suc n) - k n\ < 1 + 1" then have "\k (Suc n) - k n\ < 2 / (2*pi)" by (simp add: field_simps) also have "... < 1" using pi_ge_two by auto finally show "real_of_int \k (Suc n) - k n\ < 1" . qed then obtain N where N: "\n. n\N \ \k (Suc n) - k n\ = 0" using eventually_sequentially less_irrefl of_int_abs by fastforce have "k (N+i) = k N" for i proof (induction i) case (Suc i) with N [of "N+i"] show ?case by auto qed simp then have "\n. n\N \ k n = k N" using le_Suc_ex by auto then show ?thesis by (force simp add: eventually_sequentially intro: that) qed with \to\ have "(\n. (\j\n. Im (Ln (z j)))) \ \ + of_int K * (2*pi)" by (simp add: k tendsto_add tendsto_mult tendsto_eventually) moreover have "(\n. (\k\n. Re (Ln (z k)))) \ Re (Ln \)" using assms continuous_imp_tendsto [OF isCont_ln tendsto_norm [OF L]] by (simp add: o_def flip: prod_norm ln_prod) ultimately show ?rhs by (rule_tac x="K+1" in exI) (auto simp: tendsto_complex_iff \_def Arg_def assms algebra_simps) next assume ?rhs then obtain r where r: "(\n. (\k\n. Ln (z k))) \ Ln \ + of_int r * (of_real(2*pi) * \)" .. have "(\n. exp (\k\n. Ln (z k))) \ \" using assms continuous_imp_tendsto [OF isCont_exp r] exp_integer_2pi [of r] by (simp add: o_def exp_add algebra_simps) moreover have "exp (\k\n. Ln (z k)) = (\k\n. z k)" for n by (simp add: exp_sum add_eq_0_iff assms) ultimately show ?lhs by auto qed text\Prop 17.2 of Bak and Newman, Complex Analysis, p.242\ proposition convergent_prod_iff_summable_complex: fixes z :: "nat \ complex" assumes "\k. z k \ 0" shows "convergent_prod (\k. z k) \ summable (\k. Ln (z k))" (is "?lhs = ?rhs") proof assume ?lhs then obtain p where p: "(\n. \k\n. z k) \ p" and "p \ 0" using convergent_prod_LIMSEQ prodinf_nonzero add_eq_0_iff assms by fastforce then show ?rhs using Ln_prodinf_complex assms by (auto simp: prodinf_nonzero summable_def sums_def_le) next assume R: ?rhs have "(\k\n. z k) = exp (\k\n. Ln (z k))" for n by (simp add: exp_sum add_eq_0_iff assms) then have "(\n. \k\n. z k) \ exp (suminf (\k. Ln (z k)))" using continuous_imp_tendsto [OF isCont_exp summable_LIMSEQ' [OF R]] by (simp add: o_def) then show ?lhs by (subst convergent_prod_iff_convergent) (auto simp: convergent_def tendsto_Lim assms add_eq_0_iff) qed text\Prop 17.3 of Bak and Newman, Complex Analysis\ proposition summable_imp_convergent_prod_complex: fixes z :: "nat \ complex" assumes z: "summable (\k. norm (z k))" and non0: "\k. z k \ -1" shows "convergent_prod (\k. 1 + z k)" proof - note if_cong [cong] power_Suc [simp del] obtain N where N: "\k. k\N \ norm (z k) < 1/2" using summable_LIMSEQ_zero [OF z] by (metis diff_zero dist_norm half_gt_zero_iff less_numeral_extra(1) lim_sequentially tendsto_norm_zero_iff) have "norm (Ln (1 + z k)) \ 2 * norm (z k)" if "k \ N" for k proof (cases "z k = 0") case False let ?f = "\i. cmod ((- 1) ^ i * z k ^ i / of_nat (Suc i))" have normf: "norm (?f n) \ (1 / 2) ^ n" for n proof - have "norm (?f n) = cmod (z k) ^ n / cmod (1 + of_nat n)" by (auto simp: norm_divide norm_mult norm_power) also have "\ \ cmod (z k) ^ n" by (auto simp: field_split_simps mult_le_cancel_left1 in_Reals_norm) also have "\ \ (1 / 2) ^ n" using N [OF that] by (simp add: power_mono) finally show "norm (?f n) \ (1 / 2) ^ n" . qed have summablef: "summable ?f" by (intro normf summable_comparison_test' [OF summable_geometric [of "1/2"]]) auto have "(\n. (- 1) ^ Suc n / of_nat n * z k ^ n) sums Ln (1 + z k)" using Ln_series [of "z k"] N that by fastforce then have *: "(\i. z k * (((- 1) ^ i * z k ^ i) / (Suc i))) sums Ln (1 + z k)" using sums_split_initial_segment [where n= 1] by (force simp: power_Suc mult_ac) then have "norm (Ln (1 + z k)) = norm (suminf (\i. z k * (((- 1) ^ i * z k ^ i) / (Suc i))))" using sums_unique by force also have "\ = norm (z k * suminf (\i. ((- 1) ^ i * z k ^ i) / (Suc i)))" apply (subst suminf_mult) using * False by (auto simp: sums_summable intro: summable_mult_D [of "z k"]) also have "\ = norm (z k) * norm (suminf (\i. ((- 1) ^ i * z k ^ i) / (Suc i)))" by (simp add: norm_mult) also have "\ \ norm (z k) * suminf (\i. norm (((- 1) ^ i * z k ^ i) / (Suc i)))" by (intro mult_left_mono summable_norm summablef) auto also have "\ \ norm (z k) * suminf (\i. (1/2) ^ i)" by (intro mult_left_mono suminf_le) (use summable_geometric [of "1/2"] summablef normf in auto) also have "\ \ norm (z k) * 2" using suminf_geometric [of "1/2::real"] by simp finally show ?thesis by (simp add: mult_ac) qed simp then have "summable (\k. Ln (1 + z k))" by (metis summable_comparison_test summable_mult z) with non0 show ?thesis by (simp add: add_eq_0_iff convergent_prod_iff_summable_complex) qed lemma summable_Ln_complex: fixes z :: "nat \ complex" assumes "convergent_prod z" "\k. z k \ 0" shows "summable (\k. Ln (z k))" using convergent_prod_def assms convergent_prod_iff_summable_complex by blast subsection\<^marker>\tag unimportant\ \Embeddings from the reals into some complete real normed field\ lemma tendsto_eq_of_real_lim: assumes "(\n. of_real (f n) :: 'a::{complete_space,real_normed_field}) \ q" shows "q = of_real (lim f)" proof - have "convergent (\n. of_real (f n) :: 'a)" using assms convergent_def by blast then have "convergent f" unfolding convergent_def by (simp add: convergent_eq_Cauchy Cauchy_def) then show ?thesis by (metis LIMSEQ_unique assms convergentD sequentially_bot tendsto_Lim tendsto_of_real) qed lemma tendsto_eq_of_real: assumes "(\n. of_real (f n) :: 'a::{complete_space,real_normed_field}) \ q" obtains r where "q = of_real r" using tendsto_eq_of_real_lim assms by blast lemma has_prod_of_real_iff [simp]: "(\n. of_real (f n) :: 'a::{complete_space,real_normed_field}) has_prod of_real c \ f has_prod c" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs apply (auto simp: prod_defs LIMSEQ_prod_0 tendsto_of_real_iff simp flip: of_real_prod) using tendsto_eq_of_real by (metis of_real_0 tendsto_of_real_iff) next assume ?rhs with tendsto_of_real_iff show ?lhs by (fastforce simp: prod_defs simp flip: of_real_prod) qed end diff --git a/src/HOL/Library/Infinite_Set.thy b/src/HOL/Library/Infinite_Set.thy --- a/src/HOL/Library/Infinite_Set.thy +++ b/src/HOL/Library/Infinite_Set.thy @@ -1,614 +1,618 @@ (* Title: HOL/Library/Infinite_Set.thy Author: Stephan Merz *) section \Infinite Sets and Related Concepts\ theory Infinite_Set imports Main begin subsection \The set of natural numbers is infinite\ lemma infinite_nat_iff_unbounded_le: "infinite S \ (\m. \n\m. n \ S)" for S :: "nat set" using frequently_cofinite[of "\x. x \ S"] by (simp add: cofinite_eq_sequentially frequently_def eventually_sequentially) lemma infinite_nat_iff_unbounded: "infinite S \ (\m. \n>m. n \ S)" for S :: "nat set" using frequently_cofinite[of "\x. x \ S"] by (simp add: cofinite_eq_sequentially frequently_def eventually_at_top_dense) lemma finite_nat_iff_bounded: "finite S \ (\k. S \ {.. (\k. S \ {.. k})" for S :: "nat set" using infinite_nat_iff_unbounded[of S] by (simp add: subset_eq) (metis not_le) lemma finite_nat_bounded: "finite S \ \k. S \ {.. For a set of natural numbers to be infinite, it is enough to know that for any number larger than some \k\, there is some larger number that is an element of the set. \ lemma unbounded_k_infinite: "\m>k. \n>m. n \ S \ infinite (S::nat set)" apply (clarsimp simp add: finite_nat_set_iff_bounded) apply (drule_tac x="Suc (max m k)" in spec) using less_Suc_eq apply fastforce done lemma nat_not_finite: "finite (UNIV::nat set) \ R" by simp lemma range_inj_infinite: fixes f :: "nat \ 'a" assumes "inj f" shows "infinite (range f)" proof assume "finite (range f)" from this assms have "finite (UNIV::nat set)" by (rule finite_imageD) then show False by simp qed subsection \The set of integers is also infinite\ lemma infinite_int_iff_infinite_nat_abs: "infinite S \ infinite ((nat \ abs)  S)" for S :: "int set" proof (unfold Not_eq_iff, rule iffI) assume "finite ((nat \ abs)  S)" then have "finite (nat  (abs  S))" by (simp add: image_image cong: image_cong) moreover have "inj_on nat (abs  S)" by (rule inj_onI) auto ultimately have "finite (abs  S)" by (rule finite_imageD) then show "finite S" by (rule finite_image_absD) qed simp proposition infinite_int_iff_unbounded_le: "infinite S \ (\m. \n. \n\ \ m \ n \ S)" for S :: "int set" by (simp add: infinite_int_iff_infinite_nat_abs infinite_nat_iff_unbounded_le o_def image_def) (metis abs_ge_zero nat_le_eq_zle le_nat_iff) proposition infinite_int_iff_unbounded: "infinite S \ (\m. \n. \n\ > m \ n \ S)" for S :: "int set" by (simp add: infinite_int_iff_infinite_nat_abs infinite_nat_iff_unbounded o_def image_def) (metis (full_types) nat_le_iff nat_mono not_le) proposition finite_int_iff_bounded: "finite S \ (\k. abs  S \ {.. (\k. abs ` S \ {.. k})" for S :: "int set" using infinite_int_iff_unbounded[of S] by (simp add: subset_eq) (metis not_le) subsection \Infinitely Many and Almost All\ text \ We often need to reason about the existence of infinitely many (resp., all but finitely many) objects satisfying some predicate, so we introduce corresponding binders and their proof rules. \ lemma not_INFM [simp]: "\ (INFM x. P x) \ (MOST x. \ P x)" by (rule not_frequently) lemma not_MOST [simp]: "\ (MOST x. P x) \ (INFM x. \ P x)" by (rule not_eventually) lemma INFM_const [simp]: "(INFM x::'a. P) \ P \ infinite (UNIV::'a set)" by (simp add: frequently_const_iff) lemma MOST_const [simp]: "(MOST x::'a. P) \ P \ finite (UNIV::'a set)" by (simp add: eventually_const_iff) lemma INFM_imp_distrib: "(INFM x. P x \ Q x) \ ((MOST x. P x) \ (INFM x. Q x))" by (rule frequently_imp_iff) lemma MOST_imp_iff: "MOST x. P x \ (MOST x. P x \ Q x) \ (MOST x. Q x)" by (auto intro: eventually_rev_mp eventually_mono) lemma INFM_conjI: "INFM x. P x \ MOST x. Q x \ INFM x. P x \ Q x" by (rule frequently_rev_mp[of P]) (auto elim: eventually_mono) text \Properties of quantifiers with injective functions.\ lemma INFM_inj: "INFM x. P (f x) \ inj f \ INFM x. P x" using finite_vimageI[of "{x. P x}" f] by (auto simp: frequently_cofinite) lemma MOST_inj: "MOST x. P x \ inj f \ MOST x. P (f x)" using finite_vimageI[of "{x. \ P x}" f] by (auto simp: eventually_cofinite) text \Properties of quantifiers with singletons.\ lemma not_INFM_eq [simp]: "\ (INFM x. x = a)" "\ (INFM x. a = x)" unfolding frequently_cofinite by simp_all lemma MOST_neq [simp]: "MOST x. x \ a" "MOST x. a \ x" unfolding eventually_cofinite by simp_all lemma INFM_neq [simp]: "(INFM x::'a. x \ a) \ infinite (UNIV::'a set)" "(INFM x::'a. a \ x) \ infinite (UNIV::'a set)" unfolding frequently_cofinite by simp_all lemma MOST_eq [simp]: "(MOST x::'a. x = a) \ finite (UNIV::'a set)" "(MOST x::'a. a = x) \ finite (UNIV::'a set)" unfolding eventually_cofinite by simp_all lemma MOST_eq_imp: "MOST x. x = a \ P x" "MOST x. a = x \ P x" unfolding eventually_cofinite by simp_all text \Properties of quantifiers over the naturals.\ lemma MOST_nat: "(\\<^sub>\n. P n) \ (\m. \n>m. P n)" for P :: "nat \ bool" by (auto simp add: eventually_cofinite finite_nat_iff_bounded_le subset_eq simp flip: not_le) lemma MOST_nat_le: "(\\<^sub>\n. P n) \ (\m. \n\m. P n)" for P :: "nat \ bool" by (auto simp add: eventually_cofinite finite_nat_iff_bounded subset_eq simp flip: not_le) lemma INFM_nat: "(\\<^sub>\n. P n) \ (\m. \n>m. P n)" for P :: "nat \ bool" by (simp add: frequently_cofinite infinite_nat_iff_unbounded) lemma INFM_nat_le: "(\\<^sub>\n. P n) \ (\m. \n\m. P n)" for P :: "nat \ bool" by (simp add: frequently_cofinite infinite_nat_iff_unbounded_le) lemma MOST_INFM: "infinite (UNIV::'a set) \ MOST x::'a. P x \ INFM x::'a. P x" by (simp add: eventually_frequently) lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \ (MOST n. P n)" by (simp add: cofinite_eq_sequentially) lemma MOST_SucI: "MOST n. P n \ MOST n. P (Suc n)" and MOST_SucD: "MOST n. P (Suc n) \ MOST n. P n" by (simp_all add: MOST_Suc_iff) lemma MOST_ge_nat: "MOST n::nat. m \ n" by (simp add: cofinite_eq_sequentially) \ \legacy names\ lemma Inf_many_def: "Inf_many P \ infinite {x. P x}" by (fact frequently_cofinite) lemma Alm_all_def: "Alm_all P \ \ (INFM x. \ P x)" by simp lemma INFM_iff_infinite: "(INFM x. P x) \ infinite {x. P x}" by (fact frequently_cofinite) lemma MOST_iff_cofinite: "(MOST x. P x) \ finite {x. \ P x}" by (fact eventually_cofinite) lemma INFM_EX: "(\\<^sub>\x. P x) \ (\x. P x)" by (fact frequently_ex) lemma ALL_MOST: "\x. P x \ \\<^sub>\x. P x" by (fact always_eventually) lemma INFM_mono: "\\<^sub>\x. P x \ (\x. P x \ Q x) \ \\<^sub>\x. Q x" by (fact frequently_elim1) lemma MOST_mono: "\\<^sub>\x. P x \ (\x. P x \ Q x) \ \\<^sub>\x. Q x" by (fact eventually_mono) lemma INFM_disj_distrib: "(\\<^sub>\x. P x \ Q x) \ (\\<^sub>\x. P x) \ (\\<^sub>\x. Q x)" by (fact frequently_disj_iff) lemma MOST_rev_mp: "\\<^sub>\x. P x \ \\<^sub>\x. P x \ Q x \ \\<^sub>\x. Q x" by (fact eventually_rev_mp) lemma MOST_conj_distrib: "(\\<^sub>\x. P x \ Q x) \ (\\<^sub>\x. P x) \ (\\<^sub>\x. Q x)" by (fact eventually_conj_iff) lemma MOST_conjI: "MOST x. P x \ MOST x. Q x \ MOST x. P x \ Q x" by (fact eventually_conj) lemma INFM_finite_Bex_distrib: "finite A \ (INFM y. \x\A. P x y) \ (\x\A. INFM y. P x y)" by (fact frequently_bex_finite_distrib) lemma MOST_finite_Ball_distrib: "finite A \ (MOST y. \x\A. P x y) \ (\x\A. MOST y. P x y)" by (fact eventually_ball_finite_distrib) lemma INFM_E: "INFM x. P x \ (\x. P x \ thesis) \ thesis" by (fact frequentlyE) lemma MOST_I: "(\x. P x) \ MOST x. P x" by (rule eventuallyI) lemmas MOST_iff_finiteNeg = MOST_iff_cofinite subsection \Enumeration of an Infinite Set\ text \The set's element type must be wellordered (e.g. the natural numbers).\ text \ Could be generalized to \<^prop>\enumerate' S n = (SOME t. t \ s \ finite {s\S. s < t} \ card {s\S. s < t} = n)\. \ primrec (in wellorder) enumerate :: "'a set \ nat \ 'a" where enumerate_0: "enumerate S 0 = (LEAST n. n \ S)" | enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \ S}) n" lemma enumerate_Suc': "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n" by simp lemma enumerate_in_set: "infinite S \ enumerate S n \ S" proof (induct n arbitrary: S) case 0 then show ?case by (fastforce intro: LeastI dest!: infinite_imp_nonempty) next case (Suc n) then show ?case by simp (metis DiffE infinite_remove) qed declare enumerate_0 [simp del] enumerate_Suc [simp del] lemma enumerate_step: "infinite S \ enumerate S n < enumerate S (Suc n)" proof (induction n arbitrary: S) case 0 then have "enumerate S 0 \ enumerate S (Suc 0)" by (simp add: enumerate_0 Least_le enumerate_in_set) moreover have "enumerate (S - {enumerate S 0}) 0 \ S - {enumerate S 0}" by (meson "0.prems" enumerate_in_set infinite_remove) then have "enumerate S 0 \ enumerate (S - {enumerate S 0}) 0" by auto ultimately show ?case by (simp add: enumerate_Suc') next case (Suc n) then show ?case by (simp add: enumerate_Suc') qed lemma enumerate_mono: "m < n \ infinite S \ enumerate S m < enumerate S n" by (induct m n rule: less_Suc_induct) (auto intro: enumerate_step) lemma enumerate_mono_iff [simp]: "infinite S \ enumerate S m < enumerate S n \ m < n" by (metis enumerate_mono less_asym less_linear) +lemma enumerate_mono_le_iff [simp]: + "infinite S \ enumerate S m \ enumerate S n \ m \ n" + by (meson enumerate_mono_iff not_le) + lemma le_enumerate: assumes S: "infinite S" shows "n \ enumerate S n" using S proof (induct n) case 0 then show ?case by simp next case (Suc n) then have "n \ enumerate S n" by simp also note enumerate_mono[of n "Suc n", OF _ \infinite S\] finally show ?case by simp qed lemma infinite_enumerate: assumes fS: "infinite S" shows "\r::nat\nat. strict_mono r \ (\n. r n \ S)" unfolding strict_mono_def using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by blast lemma enumerate_Suc'': fixes S :: "'a::wellorder set" assumes "infinite S" shows "enumerate S (Suc n) = (LEAST s. s \ S \ enumerate S n < s)" using assms proof (induct n arbitrary: S) case 0 then have "\s \ S. enumerate S 0 \ s" by (auto simp: enumerate.simps intro: Least_le) then show ?case unfolding enumerate_Suc' enumerate_0[of "S - {enumerate S 0}"] by (intro arg_cong[where f = Least] ext) auto next case (Suc n S) show ?case using enumerate_mono[OF zero_less_Suc \infinite S\, of n] \infinite S\ apply (subst (1 2) enumerate_Suc') apply (subst Suc) apply (use \infinite S\ in simp) apply (intro arg_cong[where f = Least] ext) apply (auto simp flip: enumerate_Suc') done qed lemma enumerate_Ex: fixes S :: "nat set" assumes S: "infinite S" and s: "s \ S" shows "\n. enumerate S n = s" using s proof (induct s rule: less_induct) case (less s) show ?case proof (cases "\y\S. y < s") case True let ?y = "Max {s'\S. s' < s}" from True have y: "\x. ?y < x \ (\s'\S. s' < s \ s' < x)" by (subst Max_less_iff) auto then have y_in: "?y \ {s'\S. s' < s}" by (intro Max_in) auto with less.hyps[of ?y] obtain n where "enumerate S n = ?y" by auto with S have "enumerate S (Suc n) = s" by (auto simp: y less enumerate_Suc'' intro!: Least_equality) then show ?thesis by auto next case False then have "\t\S. s \ t" by auto with \s \ S\ show ?thesis by (auto intro!: exI[of _ 0] Least_equality simp: enumerate_0) qed qed lemma inj_enumerate: fixes S :: "'a::wellorder set" assumes S: "infinite S" shows "inj (enumerate S)" unfolding inj_on_def proof clarsimp show "\x y. enumerate S x = enumerate S y \ x = y" by (metis neq_iff enumerate_mono[OF _ \infinite S\]) qed text \To generalise this, we'd need a condition that all initial segments were finite\ lemma bij_enumerate: fixes S :: "nat set" assumes S: "infinite S" shows "bij_betw (enumerate S) UNIV S" proof - have "\s \ S. \i. enumerate S i = s" using enumerate_Ex[OF S] by auto moreover note \infinite S\ inj_enumerate ultimately show ?thesis unfolding bij_betw_def by (auto intro: enumerate_in_set) qed lemma fixes S :: "nat set" assumes S: "infinite S" shows range_enumerate: "range (enumerate S) = S" and strict_mono_enumerate: "strict_mono (enumerate S)" by (auto simp add: bij_betw_imp_surj_on bij_enumerate assms strict_mono_def) text \A pair of weird and wonderful lemmas from HOL Light.\ lemma finite_transitivity_chain: assumes "finite A" and R: "\x. \ R x x" "\x y z. \R x y; R y z\ \ R x z" and A: "\x. x \ A \ \y. y \ A \ R x y" shows "A = {}" using \finite A\ A proof (induct A) case empty then show ?case by simp next case (insert a A) have False using R(1)[of a] R(2)[of _ a] insert(3,4) by blast thus ?case .. qed corollary Union_maximal_sets: assumes "finite \" shows "\{T \ \. \U\\. \ T \ U} = \\" (is "?lhs = ?rhs") proof show "?lhs \ ?rhs" by force show "?rhs \ ?lhs" proof (rule Union_subsetI) fix S assume "S \ \" have "{T \ \. S \ T} = {}" if "\ (\y. y \ {T \ \. \U\\. \ T \ U} \ S \ y)" proof - have \
: "\x. x \ \ \ S \ x \ \y. y \ \ \ S \ y \ x \ y" using that by (blast intro: dual_order.trans psubset_imp_subset) show ?thesis proof (rule finite_transitivity_chain [of _ "\T U. S \ T \ T \ U"]) qed (use assms in \auto intro: \
\) qed with \S \ \\ show "\y. y \ {T \ \. \U\\. \ T \ U} \ S \ y" by blast qed qed subsection \Properties of @{term enumerate} on finite sets\ lemma finite_enumerate_in_set: "\finite S; n < card S\ \ enumerate S n \ S" proof (induction n arbitrary: S) case 0 then show ?case by (metis all_not_in_conv card.empty enumerate.simps(1) not_less0 wellorder_Least_lemma(1)) next case (Suc n) show ?case using Suc.prems Suc.IH [of "S - {LEAST n. n \ S}"] apply (simp add: enumerate.simps) by (metis Diff_empty Diff_insert0 Suc_lessD card.remove less_Suc_eq) qed lemma finite_enumerate_step: "\finite S; Suc n < card S\ \ enumerate S n < enumerate S (Suc n)" proof (induction n arbitrary: S) case 0 then have "enumerate S 0 \ enumerate S (Suc 0)" by (simp add: Least_le enumerate.simps(1) finite_enumerate_in_set) moreover have "enumerate (S - {enumerate S 0}) 0 \ S - {enumerate S 0}" by (metis 0 Suc_lessD Suc_less_eq card_Suc_Diff1 enumerate_in_set finite_enumerate_in_set) then have "enumerate S 0 \ enumerate (S - {enumerate S 0}) 0" by auto ultimately show ?case by (simp add: enumerate_Suc') next case (Suc n) then show ?case by (simp add: enumerate_Suc' finite_enumerate_in_set) qed lemma finite_enumerate_mono: "\m < n; finite S; n < card S\ \ enumerate S m < enumerate S n" by (induct m n rule: less_Suc_induct) (auto intro: finite_enumerate_step) lemma finite_enumerate_mono_iff [simp]: "\finite S; m < card S; n < card S\ \ enumerate S m < enumerate S n \ m < n" by (metis finite_enumerate_mono less_asym less_linear) lemma finite_le_enumerate: assumes "finite S" "n < card S" shows "n \ enumerate S n" using assms proof (induction n) case 0 then show ?case by simp next case (Suc n) then have "n \ enumerate S n" by simp also note finite_enumerate_mono[of n "Suc n", OF _ \finite S\] finally show ?case using Suc.prems(2) Suc_leI by blast qed lemma finite_enumerate: assumes fS: "finite S" shows "\r::nat\nat. strict_mono_on {.. (\n S)" unfolding strict_mono_def using finite_enumerate_in_set[OF fS] finite_enumerate_mono[of _ _ S] fS by (metis lessThan_iff strict_mono_on_def) lemma finite_enumerate_Suc'': fixes S :: "'a::wellorder set" assumes "finite S" "Suc n < card S" shows "enumerate S (Suc n) = (LEAST s. s \ S \ enumerate S n < s)" using assms proof (induction n arbitrary: S) case 0 then have "\s \ S. enumerate S 0 \ s" by (auto simp: enumerate.simps intro: Least_le) then show ?case unfolding enumerate_Suc' enumerate_0[of "S - {enumerate S 0}"] by (metis Diff_iff dual_order.strict_iff_order singletonD singletonI) next case (Suc n S) then have "Suc n < card (S - {enumerate S 0})" using Suc.prems(2) finite_enumerate_in_set by force then show ?case apply (subst (1 2) enumerate_Suc') apply (simp add: Suc) apply (intro arg_cong[where f = Least] HOL.ext) using finite_enumerate_mono[OF zero_less_Suc \finite S\, of n] Suc.prems by (auto simp flip: enumerate_Suc') qed lemma finite_enumerate_initial_segment: fixes S :: "'a::wellorder set" assumes "finite S" and n: "n < card (S \ {.. {.. S \ n < s) = (LEAST n. n \ S)" proof (rule Least_equality) have "\t. t \ S \ t < s" by (metis "0" card_gt_0_iff disjoint_iff_not_equal lessThan_iff) then show "(LEAST n. n \ S) \ S \ (LEAST n. n \ S) < s" by (meson LeastI Least_le le_less_trans) qed (simp add: Least_le) then show ?case by (auto simp: enumerate_0) next case (Suc n) then have less_card: "Suc n < card S" by (meson assms(1) card_mono inf_sup_ord(1) leD le_less_linear order.trans) obtain T where T: "T \ {s \ S. enumerate S n < s}" by (metis Infinite_Set.enumerate_step enumerate_in_set finite_enumerate_in_set finite_enumerate_step less_card mem_Collect_eq) have "(LEAST x. x \ S \ x < s \ enumerate S n < x) = (LEAST x. x \ S \ enumerate S n < x)" (is "_ = ?r") proof (intro Least_equality conjI) show "?r \ S" by (metis (mono_tags, lifting) LeastI mem_Collect_eq T) have "\ s \ ?r" using not_less_Least [of _ "\x. x \ S \ enumerate S n < x"] Suc assms by (metis (mono_tags, lifting) Int_Collect Suc_lessD finite_Int finite_enumerate_in_set finite_enumerate_step lessThan_def less_le_trans) then show "?r < s" by auto show "enumerate S n < ?r" by (metis (no_types, lifting) LeastI mem_Collect_eq T) qed (auto simp: Least_le) then show ?case using Suc assms by (simp add: finite_enumerate_Suc'' less_card) qed lemma finite_enumerate_Ex: fixes S :: "'a::wellorder set" assumes S: "finite S" and s: "s \ S" shows "\ny\S. y < s") case True let ?T = "S \ {..finite S\]) from True have y: "\x. Max ?T < x \ (\s'\S. s' < s \ s' < x)" by (subst Max_less_iff) (auto simp: \finite ?T\) then have y_in: "Max ?T \ {s'\S. s' < s}" using Max_in \finite ?T\ by fastforce with less.IH[of "Max ?T" ?T] obtain n where n: "enumerate ?T n = Max ?T" "n < card ?T" using \finite ?T\ by blast then have "Suc n < card S" using TS less_trans_Suc by blast with S n have "enumerate S (Suc n) = s" by (subst finite_enumerate_Suc'') (auto simp: y finite_enumerate_initial_segment less finite_enumerate_Suc'' intro!: Least_equality) then show ?thesis using \Suc n < card S\ by blast next case False then have "\t\S. s \ t" by auto moreover have "0 < card S" using card_0_eq less.prems by blast ultimately show ?thesis using \s \ S\ by (auto intro!: exI[of _ 0] Least_equality simp: enumerate_0) qed qed lemma finite_enum_subset: assumes "\i. i < card X \ enumerate X i = enumerate Y i" and "finite X" "finite Y" "card X \ card Y" shows "X \ Y" by (metis assms finite_enumerate_Ex finite_enumerate_in_set less_le_trans subsetI) lemma finite_enum_ext: assumes "\i. i < card X \ enumerate X i = enumerate Y i" and "finite X" "finite Y" "card X = card Y" shows "X = Y" by (intro antisym finite_enum_subset) (auto simp: assms) lemma finite_bij_enumerate: fixes S :: "'a::wellorder set" assumes S: "finite S" shows "bij_betw (enumerate S) {..n m. \n \ m; n < card S; m < card S\ \ enumerate S n \ enumerate S m" using finite_enumerate_mono[OF _ \finite S\] by (auto simp: neq_iff) then have "inj_on (enumerate S) {..s \ S. \ifinite S\ ultimately show ?thesis unfolding bij_betw_def by (auto intro: finite_enumerate_in_set) qed lemma ex_bij_betw_strict_mono_card: fixes M :: "'a::wellorder set" assumes "finite M" obtains h where "bij_betw h {..