1 theory SeriesPlus |
|
2 imports Complex_Main Nat_Bijection |
|
3 begin |
|
4 |
|
5 text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*} |
|
6 |
|
7 lemma choice2: "(!!x. \<exists>y z. Q x y z) ==> \<exists>f g. \<forall>x. Q x (f x) (g x)" |
|
8 by metis |
|
9 |
|
10 lemma range_subsetD: "range f \<subseteq> B \<Longrightarrow> f i \<in> B" |
|
11 by blast |
|
12 |
|
13 |
|
14 lemma suminf_2dimen: |
|
15 fixes f:: "nat * nat \<Rightarrow> real" |
|
16 assumes f_nneg: "!!m n. 0 \<le> f(m,n)" |
|
17 and fsums: "!!m. (\<lambda>n. f (m,n)) sums (g m)" |
|
18 and sumg: "summable g" |
|
19 shows "(f o prod_decode) sums suminf g" |
|
20 proof (simp add: sums_def) |
|
21 { |
|
22 fix x |
|
23 have "0 \<le> f x" |
|
24 by (cases x) (simp add: f_nneg) |
|
25 } note [iff] = this |
|
26 have g_nneg: "!!m. 0 \<le> g m" |
|
27 proof - |
|
28 fix m |
|
29 have "0 \<le> suminf (\<lambda>n. f (m,n))" |
|
30 by (rule suminf_0_le, simp add: f_nneg, metis fsums sums_iff) |
|
31 thus "0 \<le> g m" using fsums [of m] |
|
32 by (auto simp add: sums_iff) |
|
33 qed |
|
34 show "(\<lambda>n. \<Sum>x = 0..<n. f (prod_decode x)) ----> suminf g" |
|
35 proof (rule increasing_LIMSEQ, simp add: f_nneg) |
|
36 fix n |
|
37 def i \<equiv> "Max (Domain (prod_decode ` {0..<n}))" |
|
38 def j \<equiv> "Max (Range (prod_decode ` {0..<n}))" |
|
39 have ij: "prod_decode ` {0..<n} \<subseteq> ({0..i} \<times> {0..j})" |
|
40 by (force simp add: i_def j_def |
|
41 intro: finite_imageI Max_ge finite_Domain finite_Range) |
|
42 have "(\<Sum>x = 0..<n. f (prod_decode x)) = setsum f (prod_decode ` {0..<n})" |
|
43 using setsum_reindex [of prod_decode "{0..<n}" f] |
|
44 by (simp add: o_def) |
|
45 (metis inj_prod_decode inj_prod_decode) |
|
46 also have "... \<le> setsum f ({0..i} \<times> {0..j})" |
|
47 by (rule setsum_mono2) (auto simp add: ij) |
|
48 also have "... = setsum (\<lambda>m. setsum (\<lambda>n. f (m,n)) {0..j}) {0..<Suc i}" |
|
49 by (metis atLeast0AtMost atLeast0LessThan lessThan_Suc_atMost |
|
50 setsum_cartesian_product split_eta) |
|
51 also have "... \<le> setsum g {0..<Suc i}" |
|
52 proof (rule setsum_mono, simp add: less_Suc_eq_le) |
|
53 fix m |
|
54 assume m: "m \<le> i" |
|
55 thus " (\<Sum>n = 0..j. f (m, n)) \<le> g m" using fsums [of m] |
|
56 by (auto simp add: sums_iff) |
|
57 (metis atLeastLessThanSuc_atLeastAtMost f_nneg series_pos_le f_nneg) |
|
58 qed |
|
59 finally have "(\<Sum>x = 0..<n. f (prod_decode x)) \<le> setsum g {0..<Suc i}" . |
|
60 also have "... \<le> suminf g" |
|
61 by (rule series_pos_le [OF sumg]) (simp add: g_nneg) |
|
62 finally show "(\<Sum>x = 0..<n. f (prod_decode x)) \<le> suminf g" . |
|
63 next |
|
64 fix e :: real |
|
65 assume e: "0 < e" |
|
66 with summable_sums [OF sumg] |
|
67 obtain N where "\<bar>setsum g {0..<N} - suminf g\<bar> < e/2" and nz: "N>0" |
|
68 by (simp add: sums_def LIMSEQ_iff_nz dist_real_def) |
|
69 (metis e half_gt_zero le_refl that) |
|
70 hence gless: "suminf g < setsum g {0..<N} + e/2" using series_pos_le [OF sumg] |
|
71 by (simp add: g_nneg) |
|
72 { fix m |
|
73 assume m: "m<N" |
|
74 hence enneg: "0 < e / (2 * real N)" using e |
|
75 by (simp add: zero_less_divide_iff) |
|
76 hence "\<exists>j. \<bar>(\<Sum>n = 0..<j. f (m, n)) - g m\<bar> < e/(2 * real N)" |
|
77 using fsums [of m] m |
|
78 by (force simp add: sums_def LIMSEQ_def dist_real_def) |
|
79 hence "\<exists>j. g m < setsum (\<lambda>n. f (m,n)) {0..<j} + e/(2 * real N)" |
|
80 using fsums [of m] |
|
81 by (auto simp add: sums_iff) |
|
82 (metis abs_diff_less_iff add_less_cancel_right eq_diff_eq') |
|
83 } |
|
84 hence "\<exists>jj. \<forall>m. m<N \<longrightarrow> g m < (\<Sum>n = 0..<jj m. f (m, n)) + e/(2 * real N)" |
|
85 by (force intro: choice) |
|
86 then obtain jj where jj: |
|
87 "!!m. m<N \<Longrightarrow> g m < (\<Sum>n = 0..<jj m. f (m, n)) + e/(2 * real N)" |
|
88 by auto |
|
89 def IJ \<equiv> "SIGMA i : {0..<N}. {0..<jj i}" |
|
90 have "setsum g {0..<N} < |
|
91 (\<Sum>m = 0..<N. (\<Sum>n = 0..<jj m. f (m, n)) + e/(2 * real N))" |
|
92 by (auto simp add: nz jj intro: setsum_strict_mono) |
|
93 also have "... = (\<Sum>m = 0..<N. \<Sum>n = 0..<jj m. f (m, n)) + e/2" using nz |
|
94 by (auto simp add: setsum_addf real_of_nat_def) |
|
95 also have "... = setsum f IJ + e/2" |
|
96 by (simp add: IJ_def setsum_Sigma) |
|
97 finally have "setsum g {0..<N} < setsum f IJ + e/2" . |
|
98 hence glessf: "suminf g < setsum f IJ + e" using gless |
|
99 by auto |
|
100 have finite_IJ: "finite IJ" |
|
101 by (simp add: IJ_def) |
|
102 def NIJ \<equiv> "Max (prod_decode -` IJ)" |
|
103 have IJsb: "IJ \<subseteq> prod_decode ` {0..NIJ}" |
|
104 proof (auto simp add: NIJ_def) |
|
105 fix i j |
|
106 assume ij:"(i,j) \<in> IJ" |
|
107 hence "(i,j) = prod_decode (prod_encode (i,j))" |
|
108 by simp |
|
109 thus "(i,j) \<in> prod_decode ` {0..Max (prod_decode -` IJ)}" |
|
110 by (rule image_eqI) |
|
111 (simp add: ij finite_vimageI [OF finite_IJ inj_prod_decode]) |
|
112 qed |
|
113 have "setsum f IJ \<le> setsum f (prod_decode `{0..NIJ})" |
|
114 by (rule setsum_mono2) (auto simp add: IJsb) |
|
115 also have "... = (\<Sum>k = 0..NIJ. f (prod_decode k))" |
|
116 by (simp add: setsum_reindex inj_prod_decode) |
|
117 also have "... = (\<Sum>k = 0..<Suc NIJ. f (prod_decode k))" |
|
118 by (metis atLeast0AtMost atLeast0LessThan lessThan_Suc_atMost) |
|
119 finally have "setsum f IJ \<le> (\<Sum>k = 0..<Suc NIJ. f (prod_decode k))" . |
|
120 thus "\<exists>n. suminf g \<le> (\<Sum>x = 0..<n. f (prod_decode x)) + e" using glessf |
|
121 by (metis add_right_mono local.glessf not_leE order_le_less_trans less_asym) |
|
122 qed |
|
123 qed |
|
124 |
|
125 end |
|