src/HOL/ex/HarmonicSeries.thy
 author bulwahn Fri Oct 21 11:17:14 2011 +0200 (2011-10-21) changeset 45231 d85a2fdc586c parent 40077 c8a9eaaa2f59 child 53374 a14d2a854c02 permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
1 (*  Title:      HOL/ex/HarmonicSeries.thy
2     Author:     Benjamin Porter, 2006
3 *)
5 header {* Divergence of the Harmonic Series *}
7 theory HarmonicSeries
8 imports Complex_Main
9 begin
11 subsection {* Abstract *}
13 text {* The following document presents a proof of the Divergence of
14 Harmonic Series theorem formalised in the Isabelle/Isar theorem
15 proving system.
17 {\em Theorem:} The series $\sum_{n=1}^{\infty} \frac{1}{n}$ does not
18 converge to any number.
20 {\em Informal Proof:}
21   The informal proof is based on the following auxillary lemmas:
22   \begin{itemize}
23   \item{aux: $\sum_{n=2^m-1}^{2^m} \frac{1}{n} \geq \frac{1}{2}$}
24   \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}$}
25   \end{itemize}
27   From {\em aux} and {\em aux2} we can deduce that $\sum_{n=1}^{2^M} 28 \frac{1}{n} \geq 1 + \frac{M}{2}$ for all $M$.
29   Now for contradiction, assume that $\sum_{n=1}^{\infty} \frac{1}{n} 30 = s$ for some $s$. Because $\forall n. \frac{1}{n} > 0$ all the
31   partial sums in the series must be less than $s$. However with our
32   deduction above we can choose $N > 2*s - 2$ and thus
33   $\sum_{n=1}^{2^N} \frac{1}{n} > s$. This leads to a contradiction
34   and hence $\sum_{n=1}^{\infty} \frac{1}{n}$ is not summable.
35   QED.
36 *}
38 subsection {* Formal Proof *}
40 lemma two_pow_sub:
41   "0 < m \<Longrightarrow> (2::nat)^m - 2^(m - 1) = 2^(m - 1)"
42   by (induct m) auto
44 text {* We first prove the following auxillary lemma. This lemma
45 simply states that the finite sums: $\frac{1}{2}$, $\frac{1}{3} + 46 \frac{1}{4}$, $\frac{1}{5} + \frac{1}{6} + \frac{1}{7} + \frac{1}{8}$
47 etc. are all greater than or equal to $\frac{1}{2}$. We do this by
48 observing that each term in the sum is greater than or equal to the
49 last term, e.g. $\frac{1}{3} > \frac{1}{4}$ and thus $\frac{1}{3} + 50 \frac{1}{4} > \frac{1}{4} + \frac{1}{4} = \frac{1}{2}$. *}
52 lemma harmonic_aux:
53   "\<forall>m>0. (\<Sum>n\<in>{(2::nat)^(m - 1)+1..2^m}. 1/real n) \<ge> 1/2"
54   (is "\<forall>m>0. (\<Sum>n\<in>(?S m). 1/real n) \<ge> 1/2")
55 proof
56   fix m::nat
57   obtain tm where tmdef: "tm = (2::nat)^m" by simp
58   {
59     assume mgt0: "0 < m"
60     have "\<And>x. x\<in>(?S m) \<Longrightarrow> 1/(real x) \<ge> 1/(real tm)"
61     proof -
62       fix x::nat
63       assume xs: "x\<in>(?S m)"
64       have xgt0: "x>0"
65       proof -
66         from xs have
67           "x \<ge> 2^(m - 1) + 1" by auto
68         moreover with mgt0 have
69           "2^(m - 1) + 1 \<ge> (1::nat)" by auto
70         ultimately have
71           "x \<ge> 1" by (rule xtrans)
72         thus ?thesis by simp
73       qed
74       moreover from xs have "x \<le> 2^m" by auto
75       ultimately have
76         "inverse (real x) \<ge> inverse (real ((2::nat)^m))"
77         by (simp del: real_of_nat_power)
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)
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
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})$. *}
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" by fact
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: eval_nat_numeral)
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           by (auto simp: atLeastAtMost_singleton')
172         also have
173           "\<dots> = 1/2 + 1"
174           by simp
175         finally have
176           "?RHS (Suc M) = 1/2 + 1" by simp
177       }
178       ultimately show "?LHS (Suc M) = ?RHS (Suc M)" by simp
179     next
180       assume mnz: "M\<noteq>0"
181       then have mgtz: "M>0" by simp
182       with Suc have suc:
183         "(?LHS M) = (?RHS M)" by blast
184       have
185         "(?LHS (Suc M)) =
186          ((?LHS M) + (\<Sum>n\<in>{(2::nat)^M+1..2^(Suc M)}. 1 / real n))"
187       proof -
188         have
189           "{1..(2::nat)^(Suc M)} =
190            {1..(2::nat)^M}\<union>{(2::nat)^M+1..(2::nat)^(Suc M)}"
191           by auto
192         moreover have
193           "{1..(2::nat)^M}\<inter>{(2::nat)^M+1..(2::nat)^(Suc M)} = {}"
194           by auto
195         moreover have
196           "finite {1..(2::nat)^M}" and "finite {(2::nat)^M+1..(2::nat)^(Suc M)}"
197           by auto
198         ultimately show ?thesis
199           by (auto intro: setsum_Un_disjoint)
200       qed
201       moreover
202       {
203         have
204           "(?RHS (Suc M)) =
205            (1 + (\<Sum>m\<in>{1..M}.  \<Sum>n\<in>{(2::nat)^(m - 1)+1..2^m}. 1/real n) +
206            (\<Sum>n\<in>{(2::nat)^(Suc M - 1)+1..2^(Suc M)}. 1/real n))" by simp
207         also have
208           "\<dots> = (?RHS M) + (\<Sum>n\<in>{(2::nat)^M+1..2^(Suc M)}. 1/real n)"
209           by simp
210         also from suc have
211           "\<dots> = (?LHS M) +  (\<Sum>n\<in>{(2::nat)^M+1..2^(Suc M)}. 1/real n)"
212           by simp
213         finally have
214           "(?RHS (Suc M)) = \<dots>" by simp
215       }
216       ultimately show "?LHS (Suc M) = ?RHS (Suc M)" by simp
217     qed
218   }
219   thus ?case by simp
220 qed
222 text {* Using @{thm [source] harmonic_aux} and @{thm [source] harmonic_aux2} we now show
223 that each group sum is greater than or equal to $\frac{1}{2}$ and thus
224 the finite sum is bounded below by a value proportional to the number
225 of elements we choose. *}
227 lemma harmonic_aux3 [rule_format]:
228   shows "\<forall>(M::nat). (\<Sum>n\<in>{1..(2::nat)^M}. 1 / real n) \<ge> 1 + (real M)/2"
229   (is "\<forall>M. ?P M \<ge> _")
230 proof (rule allI, cases)
231   fix M::nat
232   assume "M=0"
233   then show "?P M \<ge> 1 + (real M)/2" by simp
234 next
235   fix M::nat
236   assume "M\<noteq>0"
237   then have "M > 0" by simp
238   then have
239     "(?P M) =
240      (1 + (\<Sum>m\<in>{1..M}. \<Sum>n\<in>{(2::nat)^(m - 1)+1..2^m}. 1/real n))"
241     by (rule harmonic_aux2)
242   also have
243     "\<dots> \<ge> (1 + (\<Sum>m\<in>{1..M}. 1/2))"
244   proof -
245     let ?f = "(\<lambda>x. 1/2)"
246     let ?g = "(\<lambda>x. (\<Sum>n\<in>{(2::nat)^(x - 1)+1..2^x}. 1/real n))"
247     from harmonic_aux have "\<And>x. x\<in>{1..M} \<Longrightarrow> ?f x \<le> ?g x" by simp
248     then have "(\<Sum>m\<in>{1..M}. ?g m) \<ge> (\<Sum>m\<in>{1..M}. ?f m)" by (rule setsum_mono)
249     thus ?thesis by simp
250   qed
251   finally have "(?P M) \<ge> (1 + (\<Sum>m\<in>{1..M}. 1/2))" .
252   moreover
253   {
254     have
255       "(\<Sum>m\<in>{1..M}. (1::real)/2) = 1/2 * (\<Sum>m\<in>{1..M}. 1)"
256       by auto
257     also have
258       "\<dots> = 1/2*(real (card {1..M}))"
259       by (simp only: real_of_card[symmetric])
260     also have
261       "\<dots> = 1/2*(real M)" by simp
262     also have
263       "\<dots> = (real M)/2" by simp
264     finally have "(\<Sum>m\<in>{1..M}. (1::real)/2) = (real M)/2" .
265   }
266   ultimately show "(?P M) \<ge> (1 + (real M)/2)" by simp
267 qed
269 text {* The final theorem shows that as we take more and more elements
270 (see @{thm [source] harmonic_aux3}) we get an ever increasing sum. By assuming
271 the sum converges, the lemma @{thm [source] series_pos_less} ( @{thm
272 series_pos_less} ) states that each sum is bounded above by the
273 series' limit. This contradicts our first statement and thus we prove
274 that the harmonic series is divergent. *}
276 theorem DivergenceOfHarmonicSeries:
277   shows "\<not>summable (\<lambda>n. 1/real (Suc n))"
278   (is "\<not>summable ?f")
279 proof -- "by contradiction"
280   let ?s = "suminf ?f" -- "let ?s equal the sum of the harmonic series"
281   assume sf: "summable ?f"
282   then obtain n::nat where ndef: "n = nat \<lceil>2 * ?s\<rceil>" by simp
283   then have ngt: "1 + real n/2 > ?s"
284   proof -
285     have "\<forall>n. 0 \<le> ?f n" by simp
286     with sf have "?s \<ge> 0"
287       by - (rule suminf_0_le, simp_all)
288     then have cgt0: "\<lceil>2*?s\<rceil> \<ge> 0" by simp
290     from ndef have "n = nat \<lceil>(2*?s)\<rceil>" .
291     then have "real n = real (nat \<lceil>2*?s\<rceil>)" by simp
292     with cgt0 have "real n = real \<lceil>2*?s\<rceil>"
293       by (auto dest: real_nat_eq_real)
294     then have "real n \<ge> 2*(?s)" by simp
295     then have "real n/2 \<ge> (?s)" by simp
296     then show "1 + real n/2 > (?s)" by simp
297   qed
299   obtain j where jdef: "j = (2::nat)^n" by simp
300   have "\<forall>m\<ge>j. 0 < ?f m" by simp
301   with sf have "(\<Sum>i\<in>{0..<j}. ?f i) < ?s" by (rule series_pos_less)
302   then have "(\<Sum>i\<in>{1..<Suc j}. 1/(real i)) < ?s"
303     apply -
304     apply (subst(asm) setsum_shift_bounds_Suc_ivl [symmetric])
305     by simp
306   with jdef have
307     "(\<Sum>i\<in>{1..< Suc ((2::nat)^n)}. 1 / (real i)) < ?s" by simp
308   then have
309     "(\<Sum>i\<in>{1..(2::nat)^n}. 1 / (real i)) < ?s"
310     by (simp only: atLeastLessThanSuc_atLeastAtMost)
311   moreover from harmonic_aux3 have
312     "(\<Sum>i\<in>{1..(2::nat)^n}. 1 / (real i)) \<ge> 1 + real n/2" by simp
313   moreover from ngt have "1 + real n/2 > ?s" by simp
314   ultimately show False by simp
315 qed
317 end