48 show "\<forall>\<^sub>F x in at 0. x \<noteq> 0" by (auto simp: at_within_def eventually_inf_principal) |
48 show "\<forall>\<^sub>F x in at 0. x \<noteq> 0" by (auto simp: at_within_def eventually_inf_principal) |
49 show "(\<lambda>x::real. inverse (1 + x) / 1) \<midarrow>0\<rightarrow> 1" |
49 show "(\<lambda>x::real. inverse (1 + x) / 1) \<midarrow>0\<rightarrow> 1" |
50 by (rule tendsto_eq_intros refl | simp)+ |
50 by (rule tendsto_eq_intros refl | simp)+ |
51 qed auto |
51 qed auto |
52 |
52 |
53 definition gen_has_prod :: "[nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}, nat, 'a] \<Rightarrow> bool" |
53 definition raw_has_prod :: "[nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}, nat, 'a] \<Rightarrow> bool" |
54 where "gen_has_prod f M p \<equiv> (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> p \<and> p \<noteq> 0" |
54 where "raw_has_prod f M p \<equiv> (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> p \<and> p \<noteq> 0" |
55 |
55 |
56 text\<open>The nonzero and zero cases, as in \emph{Complex Analysis} by Joseph Bak and Donald J.Newman, page 241\<close> |
56 text\<open>The nonzero and zero cases, as in \emph{Complex Analysis} by Joseph Bak and Donald J.Newman, page 241\<close> |
57 definition has_prod :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "has'_prod" 80) |
57 definition has_prod :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "has'_prod" 80) |
58 where "f has_prod p \<equiv> gen_has_prod f 0 p \<or> (\<exists>i q. p = 0 \<and> f i = 0 \<and> gen_has_prod f (Suc i) q)" |
58 where "f has_prod p \<equiv> raw_has_prod f 0 p \<or> (\<exists>i q. p = 0 \<and> f i = 0 \<and> raw_has_prod f (Suc i) q)" |
59 |
59 |
60 definition convergent_prod :: "(nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}) \<Rightarrow> bool" where |
60 definition convergent_prod :: "(nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}) \<Rightarrow> bool" where |
61 "convergent_prod f \<equiv> \<exists>M p. gen_has_prod f M p" |
61 "convergent_prod f \<equiv> \<exists>M p. raw_has_prod f M p" |
62 |
62 |
63 definition prodinf :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a" |
63 definition prodinf :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a" |
64 (binder "\<Prod>" 10) |
64 (binder "\<Prod>" 10) |
65 where "prodinf f = (THE p. f has_prod p)" |
65 where "prodinf f = (THE p. f has_prod p)" |
66 |
66 |
67 lemmas prod_defs = gen_has_prod_def has_prod_def convergent_prod_def prodinf_def |
67 lemmas prod_defs = raw_has_prod_def has_prod_def convergent_prod_def prodinf_def |
68 |
68 |
69 lemma has_prod_subst[trans]: "f = g \<Longrightarrow> g has_prod z \<Longrightarrow> f has_prod z" |
69 lemma has_prod_subst[trans]: "f = g \<Longrightarrow> g has_prod z \<Longrightarrow> f has_prod z" |
70 by simp |
70 by simp |
71 |
71 |
72 lemma has_prod_cong: "(\<And>n. f n = g n) \<Longrightarrow> f has_prod c \<longleftrightarrow> g has_prod c" |
72 lemma has_prod_cong: "(\<And>n. f n = g n) \<Longrightarrow> f has_prod c \<longleftrightarrow> g has_prod c" |
73 by presburger |
73 by presburger |
74 |
74 |
75 lemma gen_has_prod_nonzero [simp]: "\<not> gen_has_prod f M 0" |
75 lemma raw_has_prod_nonzero [simp]: "\<not> raw_has_prod f M 0" |
76 by (simp add: gen_has_prod_def) |
76 by (simp add: raw_has_prod_def) |
77 |
77 |
78 lemma gen_has_prod_eq_0: |
78 lemma raw_has_prod_eq_0: |
79 fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}" |
79 fixes f :: "nat \<Rightarrow> 'a::{semidom,t2_space}" |
80 assumes p: "gen_has_prod f m p" and i: "f i = 0" "i \<ge> m" |
80 assumes p: "raw_has_prod f m p" and i: "f i = 0" "i \<ge> m" |
81 shows "p = 0" |
81 shows "p = 0" |
82 proof - |
82 proof - |
83 have eq0: "(\<Prod>k\<le>n. f (k+m)) = 0" if "i - m \<le> n" for n |
83 have eq0: "(\<Prod>k\<le>n. f (k+m)) = 0" if "i - m \<le> n" for n |
84 by (metis i that atMost_atLeast0 atMost_iff diff_add finite_atLeastAtMost prod_zero_iff) |
84 proof - |
|
85 have "\<exists>k\<le>n. f (k + m) = 0" |
|
86 using i that by auto |
|
87 then show ?thesis |
|
88 by auto |
|
89 qed |
85 have "(\<lambda>n. \<Prod>i\<le>n. f (i + m)) \<longlonglongrightarrow> 0" |
90 have "(\<lambda>n. \<Prod>i\<le>n. f (i + m)) \<longlonglongrightarrow> 0" |
86 by (rule LIMSEQ_offset [where k = "i-m"]) (simp add: eq0) |
91 by (rule LIMSEQ_offset [where k = "i-m"]) (simp add: eq0) |
87 with p show ?thesis |
92 with p show ?thesis |
88 unfolding gen_has_prod_def |
93 unfolding raw_has_prod_def |
89 using LIMSEQ_unique by blast |
94 using LIMSEQ_unique by blast |
90 qed |
95 qed |
91 |
96 |
92 lemma has_prod_0_iff: "f has_prod 0 \<longleftrightarrow> (\<exists>i. f i = 0 \<and> (\<exists>p. gen_has_prod f (Suc i) p))" |
97 lemma has_prod_0_iff: "f has_prod 0 \<longleftrightarrow> (\<exists>i. f i = 0 \<and> (\<exists>p. raw_has_prod f (Suc i) p))" |
93 by (simp add: has_prod_def) |
98 by (simp add: has_prod_def) |
94 |
99 |
95 lemma has_prod_unique2: |
100 lemma has_prod_unique2: |
96 fixes f :: "nat \<Rightarrow> 'a::{idom,t2_space}" |
101 fixes f :: "nat \<Rightarrow> 'a::{semidom,t2_space}" |
97 assumes "f has_prod a" "f has_prod b" shows "a = b" |
102 assumes "f has_prod a" "f has_prod b" shows "a = b" |
98 using assms |
103 using assms |
99 by (auto simp: has_prod_def gen_has_prod_eq_0) (meson gen_has_prod_def sequentially_bot tendsto_unique) |
104 by (auto simp: has_prod_def raw_has_prod_eq_0) (meson raw_has_prod_def sequentially_bot tendsto_unique) |
100 |
105 |
101 lemma has_prod_unique: |
106 lemma has_prod_unique: |
102 fixes f :: "nat \<Rightarrow> 'a :: {idom,t2_space}" |
107 fixes f :: "nat \<Rightarrow> 'a :: {semidom,t2_space}" |
103 shows "f has_prod s \<Longrightarrow> s = prodinf f" |
108 shows "f has_prod s \<Longrightarrow> s = prodinf f" |
104 by (simp add: has_prod_unique2 prodinf_def the_equality) |
109 by (simp add: has_prod_unique2 prodinf_def the_equality) |
105 |
110 |
106 lemma convergent_prod_altdef: |
111 lemma convergent_prod_altdef: |
107 fixes f :: "nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}" |
112 fixes f :: "nat \<Rightarrow> 'a :: {t2_space,comm_semiring_1}" |
376 lemma abs_convergent_prod_offset: |
381 lemma abs_convergent_prod_offset: |
377 assumes "abs_convergent_prod (\<lambda>n. f (n + m))" |
382 assumes "abs_convergent_prod (\<lambda>n. f (n + m))" |
378 shows "abs_convergent_prod f" |
383 shows "abs_convergent_prod f" |
379 using assms unfolding abs_convergent_prod_def by (rule convergent_prod_offset) |
384 using assms unfolding abs_convergent_prod_def by (rule convergent_prod_offset) |
380 |
385 |
381 lemma convergent_prod_ignore_initial_segment: |
386 lemma raw_has_prod_ignore_initial_segment: |
382 fixes f :: "nat \<Rightarrow> 'a :: {real_normed_field}" |
387 fixes f :: "nat \<Rightarrow> 'a :: real_normed_field" |
|
388 assumes "raw_has_prod f M p" "N \<ge> M" |
|
389 obtains q where "raw_has_prod f N q" |
|
390 proof - |
|
391 have p: "(\<lambda>n. \<Prod>k\<le>n. f (k + M)) \<longlonglongrightarrow> p" and "p \<noteq> 0" |
|
392 using assms by (auto simp: raw_has_prod_def) |
|
393 then have nz: "\<And>n. n \<ge> M \<Longrightarrow> f n \<noteq> 0" |
|
394 using assms by (auto simp: raw_has_prod_eq_0) |
|
395 define C where "C = (\<Prod>k<N-M. f (k + M))" |
|
396 from nz have [simp]: "C \<noteq> 0" |
|
397 by (auto simp: C_def) |
|
398 |
|
399 from p have "(\<lambda>i. \<Prod>k\<le>i + (N-M). f (k + M)) \<longlonglongrightarrow> p" |
|
400 by (rule LIMSEQ_ignore_initial_segment) |
|
401 also have "(\<lambda>i. \<Prod>k\<le>i + (N-M). f (k + M)) = (\<lambda>n. C * (\<Prod>k\<le>n. f (k + N)))" |
|
402 proof (rule ext, goal_cases) |
|
403 case (1 n) |
|
404 have "{..n+(N-M)} = {..<(N-M)} \<union> {(N-M)..n+(N-M)}" by auto |
|
405 also have "(\<Prod>k\<in>\<dots>. f (k + M)) = C * (\<Prod>k=(N-M)..n+(N-M). f (k + M))" |
|
406 unfolding C_def by (rule prod.union_disjoint) auto |
|
407 also have "(\<Prod>k=(N-M)..n+(N-M). f (k + M)) = (\<Prod>k\<le>n. f (k + (N-M) + M))" |
|
408 by (intro ext prod.reindex_bij_witness[of _ "\<lambda>k. k + (N-M)" "\<lambda>k. k - (N-M)"]) auto |
|
409 finally show ?case |
|
410 using \<open>N \<ge> M\<close> by (simp add: add_ac) |
|
411 qed |
|
412 finally have "(\<lambda>n. C * (\<Prod>k\<le>n. f (k + N)) / C) \<longlonglongrightarrow> p / C" |
|
413 by (intro tendsto_divide tendsto_const) auto |
|
414 hence "(\<lambda>n. \<Prod>k\<le>n. f (k + N)) \<longlonglongrightarrow> p / C" by simp |
|
415 moreover from \<open>p \<noteq> 0\<close> have "p / C \<noteq> 0" by simp |
|
416 ultimately show ?thesis |
|
417 using raw_has_prod_def that by blast |
|
418 qed |
|
419 |
|
420 corollary convergent_prod_ignore_initial_segment: |
|
421 fixes f :: "nat \<Rightarrow> 'a :: real_normed_field" |
383 assumes "convergent_prod f" |
422 assumes "convergent_prod f" |
384 shows "convergent_prod (\<lambda>n. f (n + m))" |
423 shows "convergent_prod (\<lambda>n. f (n + m))" |
385 proof - |
424 using assms |
386 from assms obtain M L |
425 unfolding convergent_prod_def |
387 where L: "(\<lambda>n. \<Prod>k\<le>n. f (k + M)) \<longlonglongrightarrow> L" "L \<noteq> 0" and nz: "\<And>n. n \<ge> M \<Longrightarrow> f n \<noteq> 0" |
426 apply clarify |
388 by (auto simp: convergent_prod_altdef) |
427 apply (erule_tac N="M+m" in raw_has_prod_ignore_initial_segment) |
389 define C where "C = (\<Prod>k<m. f (k + M))" |
428 apply (auto simp add: raw_has_prod_def add_ac) |
390 from nz have [simp]: "C \<noteq> 0" |
429 done |
391 by (auto simp: C_def) |
|
392 |
|
393 from L(1) have "(\<lambda>n. \<Prod>k\<le>n+m. f (k + M)) \<longlonglongrightarrow> L" |
|
394 by (rule LIMSEQ_ignore_initial_segment) |
|
395 also have "(\<lambda>n. \<Prod>k\<le>n+m. f (k + M)) = (\<lambda>n. C * (\<Prod>k\<le>n. f (k + M + m)))" |
|
396 proof (rule ext, goal_cases) |
|
397 case (1 n) |
|
398 have "{..n+m} = {..<m} \<union> {m..n+m}" by auto |
|
399 also have "(\<Prod>k\<in>\<dots>. f (k + M)) = C * (\<Prod>k=m..n+m. f (k + M))" |
|
400 unfolding C_def by (rule prod.union_disjoint) auto |
|
401 also have "(\<Prod>k=m..n+m. f (k + M)) = (\<Prod>k\<le>n. f (k + m + M))" |
|
402 by (intro ext prod.reindex_bij_witness[of _ "\<lambda>k. k + m" "\<lambda>k. k - m"]) auto |
|
403 finally show ?case by (simp add: add_ac) |
|
404 qed |
|
405 finally have "(\<lambda>n. C * (\<Prod>k\<le>n. f (k + M + m)) / C) \<longlonglongrightarrow> L / C" |
|
406 by (intro tendsto_divide tendsto_const) auto |
|
407 hence "(\<lambda>n. \<Prod>k\<le>n. f (k + M + m)) \<longlonglongrightarrow> L / C" by simp |
|
408 moreover from \<open>L \<noteq> 0\<close> have "L / C \<noteq> 0" by simp |
|
409 ultimately show ?thesis |
|
410 unfolding prod_defs by blast |
|
411 qed |
|
412 |
430 |
413 corollary convergent_prod_ignore_nonzero_segment: |
431 corollary convergent_prod_ignore_nonzero_segment: |
414 fixes f :: "nat \<Rightarrow> 'a :: real_normed_field" |
432 fixes f :: "nat \<Rightarrow> 'a :: real_normed_field" |
415 assumes f: "convergent_prod f" and nz: "\<And>i. i \<ge> M \<Longrightarrow> f i \<noteq> 0" |
433 assumes f: "convergent_prod f" and nz: "\<And>i. i \<ge> M \<Longrightarrow> f i \<noteq> 0" |
416 shows "\<exists>p. gen_has_prod f M p" |
434 shows "\<exists>p. raw_has_prod f M p" |
417 using convergent_prod_ignore_initial_segment [OF f] |
435 using convergent_prod_ignore_initial_segment [OF f] |
418 by (metis convergent_LIMSEQ_iff convergent_prod_iff_convergent le_add_same_cancel2 nz prod_defs(1) zero_order(1)) |
436 by (metis convergent_LIMSEQ_iff convergent_prod_iff_convergent le_add_same_cancel2 nz prod_defs(1) zero_order(1)) |
419 |
437 |
420 corollary abs_convergent_prod_ignore_initial_segment: |
438 corollary abs_convergent_prod_ignore_initial_segment: |
421 assumes "abs_convergent_prod f" |
439 assumes "abs_convergent_prod f" |
816 shows "prodinf f = (\<Prod>n\<in>N. f n)" |
837 shows "prodinf f = (\<Prod>n\<in>N. f n)" |
817 using has_prod_finite[OF assms, THEN has_prod_unique] by simp |
838 using has_prod_finite[OF assms, THEN has_prod_unique] by simp |
818 |
839 |
819 end |
840 end |
820 |
841 |
|
842 subsection \<open>Infinite products on ordered, topological monoids\<close> |
|
843 |
|
844 lemma LIMSEQ_prod_0: |
|
845 fixes f :: "nat \<Rightarrow> 'a::{semidom,topological_space}" |
|
846 assumes "f i = 0" |
|
847 shows "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> 0" |
|
848 proof (subst tendsto_cong) |
|
849 show "\<forall>\<^sub>F n in sequentially. prod f {..n} = 0" |
|
850 proof |
|
851 show "prod f {..n} = 0" if "n \<ge> i" for n |
|
852 using that assms by auto |
|
853 qed |
|
854 qed auto |
|
855 |
|
856 lemma LIMSEQ_prod_nonneg: |
|
857 fixes f :: "nat \<Rightarrow> 'a::{linordered_semidom,linorder_topology}" |
|
858 assumes 0: "\<And>n. 0 \<le> f n" and a: "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> a" |
|
859 shows "a \<ge> 0" |
|
860 by (simp add: "0" prod_nonneg LIMSEQ_le_const [OF a]) |
|
861 |
|
862 |
|
863 context |
|
864 fixes f :: "nat \<Rightarrow> 'a::{linordered_semidom,linorder_topology}" |
|
865 begin |
|
866 |
|
867 lemma has_prod_le: |
|
868 assumes f: "f has_prod a" and g: "g has_prod b" and le: "\<And>n. 0 \<le> f n \<and> f n \<le> g n" |
|
869 shows "a \<le> b" |
|
870 proof (cases "a=0 \<or> b=0") |
|
871 case True |
|
872 then show ?thesis |
|
873 proof |
|
874 assume [simp]: "a=0" |
|
875 have "b \<ge> 0" |
|
876 proof (rule LIMSEQ_prod_nonneg) |
|
877 show "(\<lambda>n. prod g {..n}) \<longlonglongrightarrow> b" |
|
878 using g by (auto simp: has_prod_def raw_has_prod_def LIMSEQ_prod_0) |
|
879 qed (use le order_trans in auto) |
|
880 then show ?thesis |
|
881 by auto |
|
882 next |
|
883 assume [simp]: "b=0" |
|
884 then obtain i where "g i = 0" |
|
885 using g by (auto simp: prod_defs) |
|
886 then have "f i = 0" |
|
887 using antisym le by force |
|
888 then have "a=0" |
|
889 using f by (auto simp: prod_defs LIMSEQ_prod_0 LIMSEQ_unique) |
|
890 then show ?thesis |
|
891 by auto |
|
892 qed |
|
893 next |
|
894 case False |
|
895 then show ?thesis |
|
896 using assms |
|
897 unfolding has_prod_def raw_has_prod_def |
|
898 by (force simp: LIMSEQ_prod_0 intro!: LIMSEQ_le prod_mono) |
|
899 qed |
|
900 |
|
901 lemma prodinf_le: |
|
902 assumes f: "f has_prod a" and g: "g has_prod b" and le: "\<And>n. 0 \<le> f n \<and> f n \<le> g n" |
|
903 shows "prodinf f \<le> prodinf g" |
|
904 using has_prod_le [OF assms] has_prod_unique f g by blast |
|
905 |
821 end |
906 end |
|
907 |
|
908 |
|
909 lemma prod_le_prodinf: |
|
910 fixes f :: "nat \<Rightarrow> 'a::{linordered_idom,linorder_topology}" |
|
911 assumes "f has_prod a" "\<And>i. 0 \<le> f i" "\<And>i. i\<ge>n \<Longrightarrow> 1 \<le> f i" |
|
912 shows "prod f {..<n} \<le> prodinf f" |
|
913 by(rule has_prod_le[OF has_prod_If_finite_set]) (use assms has_prod_unique in auto) |
|
914 |
|
915 lemma prodinf_nonneg: |
|
916 fixes f :: "nat \<Rightarrow> 'a::{linordered_idom,linorder_topology}" |
|
917 assumes "f has_prod a" "\<And>i. 1 \<le> f i" |
|
918 shows "1 \<le> prodinf f" |
|
919 using prod_le_prodinf[of f a 0] assms |
|
920 by (metis order_trans prod_ge_1 zero_le_one) |
|
921 |
|
922 lemma prodinf_le_const: |
|
923 fixes f :: "nat \<Rightarrow> real" |
|
924 assumes "convergent_prod f" "\<And>n. prod f {..<n} \<le> x" |
|
925 shows "prodinf f \<le> x" |
|
926 by (metis lessThan_Suc_atMost assms convergent_prod_LIMSEQ LIMSEQ_le_const2) |
|
927 |
|
928 lemma prodinf_eq_one_iff: |
|
929 fixes f :: "nat \<Rightarrow> real" |
|
930 assumes f: "convergent_prod f" and ge1: "\<And>n. 1 \<le> f n" |
|
931 shows "prodinf f = 1 \<longleftrightarrow> (\<forall>n. f n = 1)" |
|
932 proof |
|
933 assume "prodinf f = 1" |
|
934 then have "(\<lambda>n. \<Prod>i<n. f i) \<longlonglongrightarrow> 1" |
|
935 using convergent_prod_LIMSEQ[of f] assms by (simp add: LIMSEQ_lessThan_iff_atMost) |
|
936 then have "\<And>i. (\<Prod>n\<in>{i}. f n) \<le> 1" |
|
937 proof (rule LIMSEQ_le_const) |
|
938 have "1 \<le> prod f n" for n |
|
939 by (simp add: ge1 prod_ge_1) |
|
940 have "prod f {..<n} = 1" for n |
|
941 by (metis \<open>\<And>n. 1 \<le> prod f n\<close> \<open>prodinf f = 1\<close> antisym f convergent_prod_has_prod ge1 order_trans prod_le_prodinf zero_le_one) |
|
942 then have "(\<Prod>n\<in>{i}. f n) \<le> prod f {..<n}" if "n \<ge> Suc i" for i n |
|
943 by (metis mult.left_neutral order_refl prod.cong prod.neutral_const prod_lessThan_Suc) |
|
944 then show "\<exists>N. \<forall>n\<ge>N. (\<Prod>n\<in>{i}. f n) \<le> prod f {..<n}" for i |
|
945 by blast |
|
946 qed |
|
947 with ge1 show "\<forall>n. f n = 1" |
|
948 by (auto intro!: antisym) |
|
949 qed (metis prodinf_zero fun_eq_iff) |
|
950 |
|
951 lemma prodinf_pos_iff: |
|
952 fixes f :: "nat \<Rightarrow> real" |
|
953 assumes "convergent_prod f" "\<And>n. 1 \<le> f n" |
|
954 shows "1 < prodinf f \<longleftrightarrow> (\<exists>i. 1 < f i)" |
|
955 using prod_le_prodinf[of f 1] prodinf_eq_one_iff |
|
956 by (metis convergent_prod_has_prod assms less_le prodinf_nonneg) |
|
957 |
|
958 lemma less_1_prodinf2: |
|
959 fixes f :: "nat \<Rightarrow> real" |
|
960 assumes "convergent_prod f" "\<And>n. 1 \<le> f n" "1 < f i" |
|
961 shows "1 < prodinf f" |
|
962 proof - |
|
963 have "1 < (\<Prod>n<Suc i. f n)" |
|
964 using assms by (intro less_1_prod2[where i=i]) auto |
|
965 also have "\<dots> \<le> prodinf f" |
|
966 by (intro prod_le_prodinf) (use assms order_trans zero_le_one in \<open>blast+\<close>) |
|
967 finally show ?thesis . |
|
968 qed |
|
969 |
|
970 lemma less_1_prodinf: |
|
971 fixes f :: "nat \<Rightarrow> real" |
|
972 shows "\<lbrakk>convergent_prod f; \<And>n. 1 < f n\<rbrakk> \<Longrightarrow> 1 < prodinf f" |
|
973 by (intro less_1_prodinf2[where i=1]) (auto intro: less_imp_le) |
|
974 |
|
975 lemma prodinf_nonzero: |
|
976 fixes f :: "nat \<Rightarrow> 'a :: {idom,topological_semigroup_mult,t2_space}" |
|
977 assumes "convergent_prod f" "\<And>i. f i \<noteq> 0" |
|
978 shows "prodinf f \<noteq> 0" |
|
979 by (metis assms convergent_prod_offset_0 has_prod_unique raw_has_prod_def has_prod_def) |
|
980 |
|
981 lemma less_0_prodinf: |
|
982 fixes f :: "nat \<Rightarrow> real" |
|
983 assumes f: "convergent_prod f" and 0: "\<And>i. f i > 0" |
|
984 shows "0 < prodinf f" |
|
985 proof - |
|
986 have "prodinf f \<noteq> 0" |
|
987 by (metis assms less_irrefl prodinf_nonzero) |
|
988 moreover have "0 < (\<Prod>n<i. f n)" for i |
|
989 by (simp add: 0 prod_pos) |
|
990 then have "prodinf f \<ge> 0" |
|
991 using convergent_prod_LIMSEQ [OF f] LIMSEQ_prod_nonneg 0 less_le by blast |
|
992 ultimately show ?thesis |
|
993 by auto |
|
994 qed |
|
995 |
|
996 lemma prod_less_prodinf2: |
|
997 fixes f :: "nat \<Rightarrow> real" |
|
998 assumes f: "convergent_prod f" and 1: "\<And>m. m\<ge>n \<Longrightarrow> 1 \<le> f m" and 0: "\<And>m. 0 < f m" and i: "n \<le> i" "1 < f i" |
|
999 shows "prod f {..<n} < prodinf f" |
|
1000 proof - |
|
1001 have "prod f {..<n} \<le> prod f {..<i}" |
|
1002 by (rule prod_mono2) (use assms less_le in auto) |
|
1003 then have "prod f {..<n} < f i * prod f {..<i}" |
|
1004 using mult_less_le_imp_less[of 1 "f i" "prod f {..<n}" "prod f {..<i}"] assms |
|
1005 by (simp add: prod_pos) |
|
1006 moreover have "prod f {..<Suc i} \<le> prodinf f" |
|
1007 using prod_le_prodinf[of f _ "Suc i"] |
|
1008 by (meson "0" "1" Suc_leD convergent_prod_has_prod f \<open>n \<le> i\<close> le_trans less_eq_real_def) |
|
1009 ultimately show ?thesis |
|
1010 by (metis le_less_trans mult.commute not_le prod_lessThan_Suc) |
|
1011 qed |
|
1012 |
|
1013 lemma prod_less_prodinf: |
|
1014 fixes f :: "nat \<Rightarrow> real" |
|
1015 assumes f: "convergent_prod f" and 1: "\<And>m. m\<ge>n \<Longrightarrow> 1 < f m" and 0: "\<And>m. 0 < f m" |
|
1016 shows "prod f {..<n} < prodinf f" |
|
1017 by (meson "0" "1" f le_less prod_less_prodinf2) |
|
1018 |
|
1019 lemma raw_has_prodI_bounded: |
|
1020 fixes f :: "nat \<Rightarrow> real" |
|
1021 assumes pos: "\<And>n. 1 \<le> f n" |
|
1022 and le: "\<And>n. (\<Prod>i<n. f i) \<le> x" |
|
1023 shows "\<exists>p. raw_has_prod f 0 p" |
|
1024 unfolding raw_has_prod_def add_0_right |
|
1025 proof (rule exI LIMSEQ_incseq_SUP conjI)+ |
|
1026 show "bdd_above (range (\<lambda>n. prod f {..n}))" |
|
1027 by (metis bdd_aboveI2 le lessThan_Suc_atMost) |
|
1028 then have "(SUP i. prod f {..i}) > 0" |
|
1029 by (metis UNIV_I cSUP_upper less_le_trans pos prod_pos zero_less_one) |
|
1030 then show "(SUP i. prod f {..i}) \<noteq> 0" |
|
1031 by auto |
|
1032 show "incseq (\<lambda>n. prod f {..n})" |
|
1033 using pos order_trans [OF zero_le_one] by (auto simp: mono_def intro!: prod_mono2) |
|
1034 qed |
|
1035 |
|
1036 lemma convergent_prodI_nonneg_bounded: |
|
1037 fixes f :: "nat \<Rightarrow> real" |
|
1038 assumes "\<And>n. 1 \<le> f n" "\<And>n. (\<Prod>i<n. f i) \<le> x" |
|
1039 shows "convergent_prod f" |
|
1040 using convergent_prod_def raw_has_prodI_bounded [OF assms] by blast |
|
1041 |
|
1042 |
|
1043 subsection \<open>Infinite products on topological monoids\<close> |
|
1044 |
|
1045 context |
|
1046 fixes f g :: "nat \<Rightarrow> 'a::{t2_space,topological_semigroup_mult,idom}" |
|
1047 begin |
|
1048 |
|
1049 lemma raw_has_prod_mult: "\<lbrakk>raw_has_prod f M a; raw_has_prod g M b\<rbrakk> \<Longrightarrow> raw_has_prod (\<lambda>n. f n * g n) M (a * b)" |
|
1050 by (force simp add: prod.distrib tendsto_mult raw_has_prod_def) |
|
1051 |
|
1052 lemma has_prod_mult_nz: "\<lbrakk>f has_prod a; g has_prod b; a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>n. f n * g n) has_prod (a * b)" |
|
1053 by (simp add: raw_has_prod_mult has_prod_def) |
|
1054 |
|
1055 end |
|
1056 |
|
1057 |
|
1058 context |
|
1059 fixes f g :: "nat \<Rightarrow> 'a::real_normed_field" |
|
1060 begin |
|
1061 |
|
1062 lemma has_prod_mult: |
|
1063 assumes f: "f has_prod a" and g: "g has_prod b" |
|
1064 shows "(\<lambda>n. f n * g n) has_prod (a * b)" |
|
1065 using f [unfolded has_prod_def] |
|
1066 proof (elim disjE exE conjE) |
|
1067 assume f0: "raw_has_prod f 0 a" |
|
1068 show ?thesis |
|
1069 using g [unfolded has_prod_def] |
|
1070 proof (elim disjE exE conjE) |
|
1071 assume g0: "raw_has_prod g 0 b" |
|
1072 with f0 show ?thesis |
|
1073 by (force simp add: has_prod_def prod.distrib tendsto_mult raw_has_prod_def) |
|
1074 next |
|
1075 fix j q |
|
1076 assume "b = 0" and "g j = 0" and q: "raw_has_prod g (Suc j) q" |
|
1077 obtain p where p: "raw_has_prod f (Suc j) p" |
|
1078 using f0 raw_has_prod_ignore_initial_segment by blast |
|
1079 then have "Ex (raw_has_prod (\<lambda>n. f n * g n) (Suc j))" |
|
1080 using q raw_has_prod_mult by blast |
|
1081 then show ?thesis |
|
1082 using \<open>b = 0\<close> \<open>g j = 0\<close> has_prod_0_iff by fastforce |
|
1083 qed |
|
1084 next |
|
1085 fix i p |
|
1086 assume "a = 0" and "f i = 0" and p: "raw_has_prod f (Suc i) p" |
|
1087 show ?thesis |
|
1088 using g [unfolded has_prod_def] |
|
1089 proof (elim disjE exE conjE) |
|
1090 assume g0: "raw_has_prod g 0 b" |
|
1091 obtain q where q: "raw_has_prod g (Suc i) q" |
|
1092 using g0 raw_has_prod_ignore_initial_segment by blast |
|
1093 then have "Ex (raw_has_prod (\<lambda>n. f n * g n) (Suc i))" |
|
1094 using raw_has_prod_mult p by blast |
|
1095 then show ?thesis |
|
1096 using \<open>a = 0\<close> \<open>f i = 0\<close> has_prod_0_iff by fastforce |
|
1097 next |
|
1098 fix j q |
|
1099 assume "b = 0" and "g j = 0" and q: "raw_has_prod g (Suc j) q" |
|
1100 obtain p' where p': "raw_has_prod f (Suc (max i j)) p'" |
|
1101 by (metis raw_has_prod_ignore_initial_segment max_Suc_Suc max_def p) |
|
1102 moreover |
|
1103 obtain q' where q': "raw_has_prod g (Suc (max i j)) q'" |
|
1104 by (metis raw_has_prod_ignore_initial_segment max.cobounded2 max_Suc_Suc q) |
|
1105 ultimately show ?thesis |
|
1106 using \<open>b = 0\<close> by (simp add: has_prod_def) (metis \<open>f i = 0\<close> \<open>g j = 0\<close> raw_has_prod_mult max_def) |
|
1107 qed |
|
1108 qed |
|
1109 |
|
1110 lemma convergent_prod_mult: |
|
1111 assumes f: "convergent_prod f" and g: "convergent_prod g" |
|
1112 shows "convergent_prod (\<lambda>n. f n * g n)" |
|
1113 unfolding convergent_prod_def |
|
1114 proof - |
|
1115 obtain M p N q where p: "raw_has_prod f M p" and q: "raw_has_prod g N q" |
|
1116 using convergent_prod_def f g by blast+ |
|
1117 then obtain p' q' where p': "raw_has_prod f (max M N) p'" and q': "raw_has_prod g (max M N) q'" |
|
1118 by (meson raw_has_prod_ignore_initial_segment max.cobounded1 max.cobounded2) |
|
1119 then show "\<exists>M p. raw_has_prod (\<lambda>n. f n * g n) M p" |
|
1120 using raw_has_prod_mult by blast |
|
1121 qed |
|
1122 |
|
1123 lemma prodinf_mult: "convergent_prod f \<Longrightarrow> convergent_prod g \<Longrightarrow> prodinf f * prodinf g = (\<Prod>n. f n * g n)" |
|
1124 by (intro has_prod_unique has_prod_mult convergent_prod_has_prod) |
|
1125 |
|
1126 end |
|
1127 |
|
1128 context |
|
1129 fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::real_normed_field" |
|
1130 and I :: "'i set" |
|
1131 begin |
|
1132 |
|
1133 lemma has_prod_prod: "(\<And>i. i \<in> I \<Longrightarrow> (f i) has_prod (x i)) \<Longrightarrow> (\<lambda>n. \<Prod>i\<in>I. f i n) has_prod (\<Prod>i\<in>I. x i)" |
|
1134 by (induct I rule: infinite_finite_induct) (auto intro!: has_prod_mult) |
|
1135 |
|
1136 lemma prodinf_prod: "(\<And>i. i \<in> I \<Longrightarrow> convergent_prod (f i)) \<Longrightarrow> (\<Prod>n. \<Prod>i\<in>I. f i n) = (\<Prod>i\<in>I. \<Prod>n. f i n)" |
|
1137 using has_prod_unique[OF has_prod_prod, OF convergent_prod_has_prod] by simp |
|
1138 |
|
1139 lemma convergent_prod_prod: "(\<And>i. i \<in> I \<Longrightarrow> convergent_prod (f i)) \<Longrightarrow> convergent_prod (\<lambda>n. \<Prod>i\<in>I. f i n)" |
|
1140 using convergent_prod_has_prod_iff has_prod_prod prodinf_prod by force |
|
1141 |
|
1142 end |
|
1143 |
|
1144 subsection \<open>Infinite summability on real normed vector spaces\<close> |
|
1145 |
|
1146 context |
|
1147 fixes f :: "nat \<Rightarrow> 'a::real_normed_field" |
|
1148 begin |
|
1149 |
|
1150 lemma raw_has_prod_Suc_iff: "raw_has_prod f M (a * f M) \<longleftrightarrow> raw_has_prod (\<lambda>n. f (Suc n)) M a \<and> f M \<noteq> 0" |
|
1151 proof - |
|
1152 have "raw_has_prod f M (a * f M) \<longleftrightarrow> (\<lambda>i. \<Prod>j\<le>Suc i. f (j+M)) \<longlonglongrightarrow> a * f M \<and> a * f M \<noteq> 0" |
|
1153 by (subst LIMSEQ_Suc_iff) (simp add: raw_has_prod_def) |
|
1154 also have "\<dots> \<longleftrightarrow> (\<lambda>i. (\<Prod>j\<le>i. f (Suc j + M)) * f M) \<longlonglongrightarrow> a * f M \<and> a * f M \<noteq> 0" |
|
1155 by (simp add: ac_simps atMost_Suc_eq_insert_0 image_Suc_atMost prod_atLeast1_atMost_eq lessThan_Suc_atMost) |
|
1156 also have "\<dots> \<longleftrightarrow> raw_has_prod (\<lambda>n. f (Suc n)) M a \<and> f M \<noteq> 0" |
|
1157 proof safe |
|
1158 assume tends: "(\<lambda>i. (\<Prod>j\<le>i. f (Suc j + M)) * f M) \<longlonglongrightarrow> a * f M" and 0: "a * f M \<noteq> 0" |
|
1159 with tendsto_divide[OF tends tendsto_const, of "f M"] |
|
1160 show "raw_has_prod (\<lambda>n. f (Suc n)) M a" |
|
1161 by (simp add: raw_has_prod_def) |
|
1162 qed (auto intro: tendsto_mult_right simp: raw_has_prod_def) |
|
1163 finally show ?thesis . |
|
1164 qed |
|
1165 |
|
1166 lemma has_prod_Suc_iff: |
|
1167 assumes "f 0 \<noteq> 0" shows "(\<lambda>n. f (Suc n)) has_prod a \<longleftrightarrow> f has_prod (a * f 0)" |
|
1168 proof (cases "a = 0") |
|
1169 case True |
|
1170 then show ?thesis |
|
1171 proof (simp add: has_prod_def, safe) |
|
1172 fix i x |
|
1173 assume "f (Suc i) = 0" and "raw_has_prod (\<lambda>n. f (Suc n)) (Suc i) x" |
|
1174 then obtain y where "raw_has_prod f (Suc (Suc i)) y" |
|
1175 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) |
|
1176 then show "\<exists>i. f i = 0 \<and> Ex (raw_has_prod f (Suc i))" |
|
1177 using \<open>f (Suc i) = 0\<close> by blast |
|
1178 next |
|
1179 fix i x |
|
1180 assume "f i = 0" and x: "raw_has_prod f (Suc i) x" |
|
1181 then obtain j where j: "i = Suc j" |
|
1182 by (metis assms not0_implies_Suc) |
|
1183 moreover have "\<exists> y. raw_has_prod (\<lambda>n. f (Suc n)) i y" |
|
1184 using x by (auto simp: raw_has_prod_def) |
|
1185 then show "\<exists>i. f (Suc i) = 0 \<and> Ex (raw_has_prod (\<lambda>n. f (Suc n)) (Suc i))" |
|
1186 using \<open>f i = 0\<close> j by blast |
|
1187 qed |
|
1188 next |
|
1189 case False |
|
1190 then show ?thesis |
|
1191 by (auto simp: has_prod_def raw_has_prod_Suc_iff assms) |
|
1192 qed |
|
1193 |
|
1194 lemma convergent_prod_Suc_iff: |
|
1195 assumes "\<And>k. f k \<noteq> 0" shows "convergent_prod (\<lambda>n. f (Suc n)) = convergent_prod f" |
|
1196 proof |
|
1197 assume "convergent_prod f" |
|
1198 then have "f has_prod prodinf f" |
|
1199 by (rule convergent_prod_has_prod) |
|
1200 moreover have "prodinf f \<noteq> 0" |
|
1201 by (simp add: \<open>convergent_prod f\<close> assms prodinf_nonzero) |
|
1202 ultimately have "(\<lambda>n. f (Suc n)) has_prod (prodinf f * inverse (f 0))" |
|
1203 by (simp add: has_prod_Suc_iff inverse_eq_divide assms) |
|
1204 then show "convergent_prod (\<lambda>n. f (Suc n))" |
|
1205 using has_prod_iff by blast |
|
1206 next |
|
1207 assume "convergent_prod (\<lambda>n. f (Suc n))" |
|
1208 then show "convergent_prod f" |
|
1209 using assms convergent_prod_def raw_has_prod_Suc_iff by blast |
|
1210 qed |
|
1211 |
|
1212 lemma raw_has_prod_inverse: |
|
1213 assumes "raw_has_prod f M a" shows "raw_has_prod (\<lambda>n. inverse (f n)) M (inverse a)" |
|
1214 using assms unfolding raw_has_prod_def by (auto dest: tendsto_inverse simp: prod_inversef [symmetric]) |
|
1215 |
|
1216 lemma has_prod_inverse: |
|
1217 assumes "f has_prod a" shows "(\<lambda>n. inverse (f n)) has_prod (inverse a)" |
|
1218 using assms raw_has_prod_inverse unfolding has_prod_def by auto |
|
1219 |
|
1220 lemma convergent_prod_inverse: |
|
1221 assumes "convergent_prod f" |
|
1222 shows "convergent_prod (\<lambda>n. inverse (f n))" |
|
1223 using assms unfolding convergent_prod_def by (blast intro: raw_has_prod_inverse elim: ) |
|
1224 |
|
1225 end |
|
1226 |
|
1227 context (* Separate contexts are necessary to allow general use of the results above, here. *) |
|
1228 fixes f :: "nat \<Rightarrow> 'a::real_normed_field" |
|
1229 begin |
|
1230 |
|
1231 lemma raw_has_prod_Suc_iff': "raw_has_prod f M a \<longleftrightarrow> raw_has_prod (\<lambda>n. f (Suc n)) M (a / f M) \<and> f M \<noteq> 0" |
|
1232 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) |
|
1233 |
|
1234 lemma has_prod_divide: "f has_prod a \<Longrightarrow> g has_prod b \<Longrightarrow> (\<lambda>n. f n / g n) has_prod (a / b)" |
|
1235 unfolding divide_inverse by (intro has_prod_inverse has_prod_mult) |
|
1236 |
|
1237 lemma convergent_prod_divide: |
|
1238 assumes f: "convergent_prod f" and g: "convergent_prod g" |
|
1239 shows "convergent_prod (\<lambda>n. f n / g n)" |
|
1240 using f g has_prod_divide has_prod_iff by blast |
|
1241 |
|
1242 lemma prodinf_divide: "convergent_prod f \<Longrightarrow> convergent_prod g \<Longrightarrow> prodinf f / prodinf g = (\<Prod>n. f n / g n)" |
|
1243 by (intro has_prod_unique has_prod_divide convergent_prod_has_prod) |
|
1244 |
|
1245 lemma prodinf_inverse: "convergent_prod f \<Longrightarrow> (\<Prod>n. inverse (f n)) = inverse (\<Prod>n. f n)" |
|
1246 by (intro has_prod_unique [symmetric] has_prod_inverse convergent_prod_has_prod) |
|
1247 |
|
1248 lemma has_prod_iff_shift: |
|
1249 assumes "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0" |
|
1250 shows "(\<lambda>i. f (i + n)) has_prod a \<longleftrightarrow> f has_prod (a * (\<Prod>i<n. f i))" |
|
1251 using assms |
|
1252 proof (induct n arbitrary: a) |
|
1253 case 0 |
|
1254 then show ?case by simp |
|
1255 next |
|
1256 case (Suc n) |
|
1257 then have "(\<lambda>i. f (Suc i + n)) has_prod a \<longleftrightarrow> (\<lambda>i. f (i + n)) has_prod (a * f n)" |
|
1258 by (subst has_prod_Suc_iff) auto |
|
1259 with Suc show ?case |
|
1260 by (simp add: ac_simps) |
|
1261 qed |
|
1262 |
|
1263 corollary has_prod_iff_shift': |
|
1264 assumes "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0" |
|
1265 shows "(\<lambda>i. f (i + n)) has_prod (a / (\<Prod>i<n. f i)) \<longleftrightarrow> f has_prod a" |
|
1266 by (simp add: assms has_prod_iff_shift) |
|
1267 |
|
1268 lemma has_prod_one_iff_shift: |
|
1269 assumes "\<And>i. i < n \<Longrightarrow> f i = 1" |
|
1270 shows "(\<lambda>i. f (i+n)) has_prod a \<longleftrightarrow> (\<lambda>i. f i) has_prod a" |
|
1271 by (simp add: assms has_prod_iff_shift) |
|
1272 |
|
1273 lemma convergent_prod_iff_shift: |
|
1274 shows "convergent_prod (\<lambda>i. f (i + n)) \<longleftrightarrow> convergent_prod f" |
|
1275 apply safe |
|
1276 using convergent_prod_offset apply blast |
|
1277 using convergent_prod_ignore_initial_segment convergent_prod_def by blast |
|
1278 |
|
1279 lemma has_prod_split_initial_segment: |
|
1280 assumes "f has_prod a" "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0" |
|
1281 shows "(\<lambda>i. f (i + n)) has_prod (a / (\<Prod>i<n. f i))" |
|
1282 using assms has_prod_iff_shift' by blast |
|
1283 |
|
1284 lemma prodinf_divide_initial_segment: |
|
1285 assumes "convergent_prod f" "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0" |
|
1286 shows "(\<Prod>i. f (i + n)) = (\<Prod>i. f i) / (\<Prod>i<n. f i)" |
|
1287 by (rule has_prod_unique[symmetric]) (auto simp: assms has_prod_iff_shift) |
|
1288 |
|
1289 lemma prodinf_split_initial_segment: |
|
1290 assumes "convergent_prod f" "\<And>i. i < n \<Longrightarrow> f i \<noteq> 0" |
|
1291 shows "prodinf f = (\<Prod>i. f (i + n)) * (\<Prod>i<n. f i)" |
|
1292 by (auto simp add: assms prodinf_divide_initial_segment) |
|
1293 |
|
1294 lemma prodinf_split_head: |
|
1295 assumes "convergent_prod f" "f 0 \<noteq> 0" |
|
1296 shows "(\<Prod>n. f (Suc n)) = prodinf f / f 0" |
|
1297 using prodinf_split_initial_segment[of 1] assms by simp |
|
1298 |
|
1299 end |
|
1300 |
|
1301 context (* Separate contexts are necessary to allow general use of the results above, here. *) |
|
1302 fixes f :: "nat \<Rightarrow> 'a::real_normed_field" |
|
1303 begin |
|
1304 |
|
1305 lemma convergent_prod_inverse_iff: "convergent_prod (\<lambda>n. inverse (f n)) \<longleftrightarrow> convergent_prod f" |
|
1306 by (auto dest: convergent_prod_inverse) |
|
1307 |
|
1308 lemma convergent_prod_const_iff: |
|
1309 fixes c :: "'a :: {real_normed_field}" |
|
1310 shows "convergent_prod (\<lambda>_. c) \<longleftrightarrow> c = 1" |
|
1311 proof |
|
1312 assume "convergent_prod (\<lambda>_. c)" |
|
1313 then show "c = 1" |
|
1314 using convergent_prod_imp_LIMSEQ LIMSEQ_unique by blast |
|
1315 next |
|
1316 assume "c = 1" |
|
1317 then show "convergent_prod (\<lambda>_. c)" |
|
1318 by auto |
|
1319 qed |
|
1320 |
|
1321 lemma has_prod_power: "f has_prod a \<Longrightarrow> (\<lambda>i. f i ^ n) has_prod (a ^ n)" |
|
1322 by (induction n) (auto simp: has_prod_mult) |
|
1323 |
|
1324 lemma convergent_prod_power: "convergent_prod f \<Longrightarrow> convergent_prod (\<lambda>i. f i ^ n)" |
|
1325 by (induction n) (auto simp: convergent_prod_mult) |
|
1326 |
|
1327 lemma prodinf_power: "convergent_prod f \<Longrightarrow> prodinf (\<lambda>i. f i ^ n) = prodinf f ^ n" |
|
1328 by (metis has_prod_unique convergent_prod_imp_has_prod has_prod_power) |
|
1329 |
|
1330 end |
|
1331 |
|
1332 end |