|
1 (* Title: HOL/Library/HarmonicSeries.thy |
|
2 ID: $Id$ |
|
3 Author: Benjamin Porter, 2006 |
|
4 *) |
|
5 |
|
6 header {* Divergence of the Harmonic Series *} |
|
7 |
|
8 theory HarmonicSeries |
|
9 imports Complex_Main |
|
10 begin |
|
11 |
|
12 section {* Abstract *} |
|
13 |
|
14 text {* The following document presents a proof of the Divergence of |
|
15 Harmonic Series theorem formalised in the Isabelle/Isar theorem |
|
16 proving system. |
|
17 |
|
18 {\em Theorem:} The series $\sum_{n=1}^{\infty} \frac{1}{n}$ does not |
|
19 converge to any number. |
|
20 |
|
21 {\em Informal Proof:} |
|
22 The informal proof is based on the following auxillary lemmas: |
|
23 \begin{itemize} |
|
24 \item{aux: $\sum_{n=2^m-1}^{2^m} \frac{1}{n} \geq \frac{1}{2}$} |
|
25 \item{aux2: $\sum_{n=1}^{2^M} \frac{1}{n} = 1 + \sum_{m=1}^{M} \sum_{n=2^m-1}^{2^m} \frac{1}{n}$} |
|
26 \end{itemize} |
|
27 |
|
28 From {\em aux} and {\em aux2} we can deduce that $\sum_{n=1}^{2^M} |
|
29 \frac{1}{n} \geq 1 + \frac{M}{2}$ for all $M$. |
|
30 Now for contradiction, assume that $\sum_{n=1}^{\infty} \frac{1}{n} |
|
31 = s$ for some $s$. Because $\forall n. \frac{1}{n} > 0$ all the |
|
32 partial sums in the series must be less than $s$. However with our |
|
33 deduction above we can choose $N > 2*s - 2$ and thus |
|
34 $\sum_{n=1}^{2^N} \frac{1}{n} > s$. This leads to a contradiction |
|
35 and hence $\sum_{n=1}^{\infty} \frac{1}{n}$ is not summable. |
|
36 QED. |
|
37 *} |
|
38 |
|
39 section {* Formal Proof *} |
|
40 |
|
41 lemma two_pow_sub: |
|
42 "0 < m \<Longrightarrow> (2::nat)^m - 2^(m - 1) = 2^(m - 1)" |
|
43 by (induct m) auto |
|
44 |
|
45 text {* We first prove the following auxillary lemma. This lemma |
|
46 simply states that the finite sums: $\frac{1}{2}$, $\frac{1}{3} + |
|
47 \frac{1}{4}$, $\frac{1}{5} + \frac{1}{6} + \frac{1}{7} + \frac{1}{8}$ |
|
48 etc. are all greater than or equal to $\frac{1}{2}$. We do this by |
|
49 observing that each term in the sum is greater than or equal to the |
|
50 last term, e.g. $\frac{1}{3} > \frac{1}{4}$ and thus $\frac{1}{3} + |
|
51 \frac{1}{4} > \frac{1}{4} + \frac{1}{4} = \frac{1}{2}$. *} |
|
52 |
|
53 lemma harmonic_aux: |
|
54 "\<forall>m>0. (\<Sum>n\<in>{(2::nat)^(m - 1)+1..2^m}. 1/real n) \<ge> 1/2" |
|
55 (is "\<forall>m>0. (\<Sum>n\<in>(?S m). 1/real n) \<ge> 1/2") |
|
56 proof |
|
57 fix m::nat |
|
58 obtain tm where tmdef: "tm = (2::nat)^m" by simp |
|
59 { |
|
60 assume mgt0: "0 < m" |
|
61 have "\<And>x. x\<in>(?S m) \<Longrightarrow> 1/(real x) \<ge> 1/(real tm)" |
|
62 proof - |
|
63 fix x::nat |
|
64 assume xs: "x\<in>(?S m)" |
|
65 have xgt0: "x>0" |
|
66 proof - |
|
67 from xs have |
|
68 "x \<ge> 2^(m - 1) + 1" by auto |
|
69 moreover with mgt0 have |
|
70 "2^(m - 1) + 1 \<ge> (1::nat)" by auto |
|
71 ultimately have |
|
72 "x \<ge> 1" by (rule xtrans) |
|
73 thus ?thesis by simp |
|
74 qed |
|
75 moreover from xs have "x \<le> 2^m" by auto |
|
76 ultimately have |
|
77 "inverse (real x) \<ge> inverse (real ((2::nat)^m))" by simp |
|
78 moreover |
|
79 from xgt0 have "real x \<noteq> 0" by simp |
|
80 then have |
|
81 "inverse (real x) = 1 / (real x)" |
|
82 by (rule nonzero_inverse_eq_divide) |
|
83 moreover from mgt0 have "real tm \<noteq> 0" by (simp add: tmdef) |
|
84 then have |
|
85 "inverse (real tm) = 1 / (real tm)" |
|
86 by (rule nonzero_inverse_eq_divide) |
|
87 ultimately show |
|
88 "1/(real x) \<ge> 1/(real tm)" by (auto simp add: tmdef) |
|
89 qed |
|
90 then have |
|
91 "(\<Sum>n\<in>(?S m). 1 / real n) \<ge> (\<Sum>n\<in>(?S m). 1/(real tm))" |
|
92 by (rule setsum_mono) |
|
93 moreover have |
|
94 "(\<Sum>n\<in>(?S m). 1/(real tm)) = 1/2" |
|
95 proof - |
|
96 have |
|
97 "(\<Sum>n\<in>(?S m). 1/(real tm)) = |
|
98 (1/(real tm))*(\<Sum>n\<in>(?S m). 1)" |
|
99 by simp |
|
100 also have |
|
101 "\<dots> = ((1/(real tm)) * real (card (?S m)))" |
|
102 by (simp add: real_of_card real_of_nat_def) |
|
103 also have |
|
104 "\<dots> = ((1/(real tm)) * real (tm - (2^(m - 1))))" |
|
105 by (simp add: tmdef) |
|
106 also from mgt0 have |
|
107 "\<dots> = ((1/(real tm)) * real ((2::nat)^(m - 1)))" |
|
108 by (auto simp: tmdef dest: two_pow_sub) |
|
109 also have |
|
110 "\<dots> = (real (2::nat))^(m - 1) / (real (2::nat))^m" |
|
111 by (simp add: tmdef realpow_real_of_nat [symmetric]) |
|
112 also from mgt0 have |
|
113 "\<dots> = (real (2::nat))^(m - 1) / (real (2::nat))^((m - 1) + 1)" |
|
114 by auto |
|
115 also have "\<dots> = 1/2" by simp |
|
116 finally show ?thesis . |
|
117 qed |
|
118 ultimately have |
|
119 "(\<Sum>n\<in>(?S m). 1 / real n) \<ge> 1/2" |
|
120 by - (erule subst) |
|
121 } |
|
122 thus "0 < m \<longrightarrow> 1 / 2 \<le> (\<Sum>n\<in>(?S m). 1 / real n)" by simp |
|
123 qed |
|
124 |
|
125 text {* We then show that the sum of a finite number of terms from the |
|
126 harmonic series can be regrouped in increasing powers of 2. For |
|
127 example: $1 + \frac{1}{2} + \frac{1}{3} + \frac{1}{4} + \frac{1}{5} + |
|
128 \frac{1}{6} + \frac{1}{7} + \frac{1}{8} = 1 + (\frac{1}{2}) + |
|
129 (\frac{1}{3} + \frac{1}{4}) + (\frac{1}{5} + \frac{1}{6} + \frac{1}{7} |
|
130 + \frac{1}{8})$. *} |
|
131 |
|
132 lemma harmonic_aux2 [rule_format]: |
|
133 "0<M \<Longrightarrow> (\<Sum>n\<in>{1..(2::nat)^M}. 1/real n) = |
|
134 (1 + (\<Sum>m\<in>{1..M}. \<Sum>n\<in>{(2::nat)^(m - 1)+1..2^m}. 1/real n))" |
|
135 (is "0<M \<Longrightarrow> ?LHS M = ?RHS M") |
|
136 proof (induct M) |
|
137 case 0 show ?case by simp |
|
138 next |
|
139 case (Suc M) |
|
140 have ant: "0 < Suc M" . |
|
141 { |
|
142 have suc: "?LHS (Suc M) = ?RHS (Suc M)" |
|
143 proof cases -- "show that LHS = c and RHS = c, and thus LHS = RHS" |
|
144 assume mz: "M=0" |
|
145 { |
|
146 then have |
|
147 "?LHS (Suc M) = ?LHS 1" by simp |
|
148 also have |
|
149 "\<dots> = (\<Sum>n\<in>{(1::nat)..2}. 1/real n)" by simp |
|
150 also have |
|
151 "\<dots> = ((\<Sum>n\<in>{Suc 1..2}. 1/real n) + 1/(real (1::nat)))" |
|
152 by (subst setsum_head) |
|
153 (auto simp: atLeastSucAtMost_greaterThanAtMost) |
|
154 also have |
|
155 "\<dots> = ((\<Sum>n\<in>{2..2::nat}. 1/real n) + 1/(real (1::nat)))" |
|
156 by (simp add: nat_number) |
|
157 also have |
|
158 "\<dots> = 1/(real (2::nat)) + 1/(real (1::nat))" by simp |
|
159 finally have |
|
160 "?LHS (Suc M) = 1/2 + 1" by simp |
|
161 } |
|
162 moreover |
|
163 { |
|
164 from mz have |
|
165 "?RHS (Suc M) = ?RHS 1" by simp |
|
166 also have |
|
167 "\<dots> = (\<Sum>n\<in>{((2::nat)^0)+1..2^1}. 1/real n) + 1" |
|
168 by simp |
|
169 also have |
|
170 "\<dots> = (\<Sum>n\<in>{2::nat..2}. 1/real n) + 1" |
|
171 proof - |
|
172 have "(2::nat)^0 = 1" by simp |
|
173 then have "(2::nat)^0+1 = 2" by simp |
|
174 moreover have "(2::nat)^1 = 2" by simp |
|
175 ultimately have "{((2::nat)^0)+1..2^1} = {2::nat..2}" by auto |
|
176 thus ?thesis by simp |
|
177 qed |
|
178 also have |
|
179 "\<dots> = 1/2 + 1" |
|
180 by simp |
|
181 finally have |
|
182 "?RHS (Suc M) = 1/2 + 1" by simp |
|
183 } |
|
184 ultimately show "?LHS (Suc M) = ?RHS (Suc M)" by simp |
|
185 next |
|
186 assume mnz: "M\<noteq>0" |
|
187 then have mgtz: "M>0" by simp |
|
188 with Suc have suc: |
|
189 "(?LHS M) = (?RHS M)" by blast |
|
190 have |
|
191 "(?LHS (Suc M)) = |
|
192 ((?LHS M) + (\<Sum>n\<in>{(2::nat)^M+1..2^(Suc M)}. 1 / real n))" |
|
193 proof - |
|
194 have |
|
195 "{1..(2::nat)^(Suc M)} = |
|
196 {1..(2::nat)^M}\<union>{(2::nat)^M+1..(2::nat)^(Suc M)}" |
|
197 by auto |
|
198 moreover have |
|
199 "{1..(2::nat)^M}\<inter>{(2::nat)^M+1..(2::nat)^(Suc M)} = {}" |
|
200 by auto |
|
201 moreover have |
|
202 "finite {1..(2::nat)^M}" and "finite {(2::nat)^M+1..(2::nat)^(Suc M)}" |
|
203 by auto |
|
204 ultimately show ?thesis |
|
205 by (auto intro: setsum_Un_disjoint) |
|
206 qed |
|
207 moreover |
|
208 { |
|
209 have |
|
210 "(?RHS (Suc M)) = |
|
211 (1 + (\<Sum>m\<in>{1..M}. \<Sum>n\<in>{(2::nat)^(m - 1)+1..2^m}. 1/real n) + |
|
212 (\<Sum>n\<in>{(2::nat)^(Suc M - 1)+1..2^(Suc M)}. 1/real n))" by simp |
|
213 also have |
|
214 "\<dots> = (?RHS M) + (\<Sum>n\<in>{(2::nat)^M+1..2^(Suc M)}. 1/real n)" |
|
215 by simp |
|
216 also from suc have |
|
217 "\<dots> = (?LHS M) + (\<Sum>n\<in>{(2::nat)^M+1..2^(Suc M)}. 1/real n)" |
|
218 by simp |
|
219 finally have |
|
220 "(?RHS (Suc M)) = \<dots>" by simp |
|
221 } |
|
222 ultimately show "?LHS (Suc M) = ?RHS (Suc M)" by simp |
|
223 qed |
|
224 } |
|
225 thus ?case by simp |
|
226 qed |
|
227 |
|
228 text {* Using @{thm [source] harmonic_aux} and @{thm [source] harmonic_aux2} we now show |
|
229 that each group sum is greater than or equal to $\frac{1}{2}$ and thus |
|
230 the finite sum is bounded below by a value proportional to the number |
|
231 of elements we choose. *} |
|
232 |
|
233 lemma harmonic_aux3 [rule_format]: |
|
234 shows "\<forall>(M::nat). (\<Sum>n\<in>{1..(2::nat)^M}. 1 / real n) \<ge> 1 + (real M)/2" |
|
235 (is "\<forall>M. ?P M \<ge> _") |
|
236 proof (rule allI, cases) |
|
237 fix M::nat |
|
238 assume "M=0" |
|
239 then show "?P M \<ge> 1 + (real M)/2" by simp |
|
240 next |
|
241 fix M::nat |
|
242 assume "M\<noteq>0" |
|
243 then have "M > 0" by simp |
|
244 then have |
|
245 "(?P M) = |
|
246 (1 + (\<Sum>m\<in>{1..M}. \<Sum>n\<in>{(2::nat)^(m - 1)+1..2^m}. 1/real n))" |
|
247 by (rule harmonic_aux2) |
|
248 also have |
|
249 "\<dots> \<ge> (1 + (\<Sum>m\<in>{1..M}. 1/2))" |
|
250 proof - |
|
251 let ?f = "(\<lambda>x. 1/2)" |
|
252 let ?g = "(\<lambda>x. (\<Sum>n\<in>{(2::nat)^(x - 1)+1..2^x}. 1/real n))" |
|
253 from harmonic_aux have "\<And>x. x\<in>{1..M} \<Longrightarrow> ?f x \<le> ?g x" by simp |
|
254 then have "(\<Sum>m\<in>{1..M}. ?g m) \<ge> (\<Sum>m\<in>{1..M}. ?f m)" by (rule setsum_mono) |
|
255 thus ?thesis by simp |
|
256 qed |
|
257 finally have "(?P M) \<ge> (1 + (\<Sum>m\<in>{1..M}. 1/2))" . |
|
258 moreover |
|
259 { |
|
260 have |
|
261 "(\<Sum>m\<in>{1..M}. (1::real)/2) = 1/2 * (\<Sum>m\<in>{1..M}. 1)" |
|
262 by auto |
|
263 also have |
|
264 "\<dots> = 1/2*(real (card {1..M}))" |
|
265 by (simp only: real_of_card[symmetric]) |
|
266 also have |
|
267 "\<dots> = 1/2*(real M)" by simp |
|
268 also have |
|
269 "\<dots> = (real M)/2" by simp |
|
270 finally have "(\<Sum>m\<in>{1..M}. (1::real)/2) = (real M)/2" . |
|
271 } |
|
272 ultimately show "(?P M) \<ge> (1 + (real M)/2)" by simp |
|
273 qed |
|
274 |
|
275 text {* The final theorem shows that as we take more and more elements |
|
276 (see @{thm [source] harmonic_aux3}) we get an ever increasing sum. By assuming |
|
277 the sum converges, the lemma @{thm [source] series_pos_less} ( @{thm |
|
278 series_pos_less} ) states that each sum is bounded above by the |
|
279 series' limit. This contradicts our first statement and thus we prove |
|
280 that the harmonic series is divergent. *} |
|
281 |
|
282 theorem DivergenceOfHarmonicSeries: |
|
283 shows "\<not>summable (\<lambda>n. 1/real (Suc n))" |
|
284 (is "\<not>summable ?f") |
|
285 proof -- "by contradiction" |
|
286 let ?s = "suminf ?f" -- "let ?s equal the sum of the harmonic series" |
|
287 assume sf: "summable ?f" |
|
288 then obtain n::nat where ndef: "n = nat \<lceil>2 * ?s\<rceil>" by simp |
|
289 then have ngt: "1 + real n/2 > ?s" |
|
290 proof - |
|
291 have "\<forall>n. 0 \<le> ?f n" by simp |
|
292 with sf have "?s \<ge> 0" |
|
293 by - (rule suminf_0_le, simp_all) |
|
294 then have cgt0: "\<lceil>2*?s\<rceil> \<ge> 0" by simp |
|
295 |
|
296 from ndef have "n = nat \<lceil>(2*?s)\<rceil>" . |
|
297 then have "real n = real (nat \<lceil>2*?s\<rceil>)" by simp |
|
298 with cgt0 have "real n = real \<lceil>2*?s\<rceil>" |
|
299 by (auto dest: real_nat_eq_real) |
|
300 then have "real n \<ge> 2*(?s)" by simp |
|
301 then have "real n/2 \<ge> (?s)" by simp |
|
302 then show "1 + real n/2 > (?s)" by simp |
|
303 qed |
|
304 |
|
305 obtain j where jdef: "j = (2::nat)^n" by simp |
|
306 have "\<forall>m\<ge>j. 0 < ?f m" by simp |
|
307 with sf have "(\<Sum>i\<in>{0..<j}. ?f i) < ?s" by (rule series_pos_less) |
|
308 then have "(\<Sum>i\<in>{1..<Suc j}. 1/(real i)) < ?s" |
|
309 apply - |
|
310 apply (subst(asm) setsum_shift_bounds_Suc_ivl [symmetric]) |
|
311 by simp |
|
312 with jdef have |
|
313 "(\<Sum>i\<in>{1..< Suc ((2::nat)^n)}. 1 / (real i)) < ?s" by simp |
|
314 then have |
|
315 "(\<Sum>i\<in>{1..(2::nat)^n}. 1 / (real i)) < ?s" |
|
316 by (simp only: atLeastLessThanSuc_atLeastAtMost) |
|
317 moreover from harmonic_aux3 have |
|
318 "(\<Sum>i\<in>{1..(2::nat)^n}. 1 / (real i)) \<ge> 1 + real n/2" by simp |
|
319 moreover from ngt have "1 + real n/2 > ?s" by simp |
|
320 ultimately show False by simp |
|
321 qed |
|
322 |
|
323 end |