summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/ex/HarmonicSeries.thy

author | nipkow |

Fri Mar 06 17:38:47 2009 +0100 (2009-03-06) | |

changeset 30313 | b2441b0c8d38 |

parent 28952 | 15a4b2cf8c34 |

child 33509 | 29e4cf2c4ea3 |

permissions | -rw-r--r-- |

added lemmas

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 section {* 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 section {* 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))" by simp

77 moreover

78 from xgt0 have "real x \<noteq> 0" by simp

79 then have

80 "inverse (real x) = 1 / (real x)"

81 by (rule nonzero_inverse_eq_divide)

82 moreover from mgt0 have "real tm \<noteq> 0" by (simp add: tmdef)

83 then have

84 "inverse (real tm) = 1 / (real tm)"

85 by (rule nonzero_inverse_eq_divide)

86 ultimately show

87 "1/(real x) \<ge> 1/(real tm)" by (auto simp add: tmdef)

88 qed

89 then have

90 "(\<Sum>n\<in>(?S m). 1 / real n) \<ge> (\<Sum>n\<in>(?S m). 1/(real tm))"

91 by (rule setsum_mono)

92 moreover have

93 "(\<Sum>n\<in>(?S m). 1/(real tm)) = 1/2"

94 proof -

95 have

96 "(\<Sum>n\<in>(?S m). 1/(real tm)) =

97 (1/(real tm))*(\<Sum>n\<in>(?S m). 1)"

98 by simp

99 also have

100 "\<dots> = ((1/(real tm)) * real (card (?S m)))"

101 by (simp add: real_of_card real_of_nat_def)

102 also have

103 "\<dots> = ((1/(real tm)) * real (tm - (2^(m - 1))))"

104 by (simp add: tmdef)

105 also from mgt0 have

106 "\<dots> = ((1/(real tm)) * real ((2::nat)^(m - 1)))"

107 by (auto simp: tmdef dest: two_pow_sub)

108 also have

109 "\<dots> = (real (2::nat))^(m - 1) / (real (2::nat))^m"

110 by (simp add: tmdef realpow_real_of_nat [symmetric])

111 also from mgt0 have

112 "\<dots> = (real (2::nat))^(m - 1) / (real (2::nat))^((m - 1) + 1)"

113 by auto

114 also have "\<dots> = 1/2" by simp

115 finally show ?thesis .

116 qed

117 ultimately have

118 "(\<Sum>n\<in>(?S m). 1 / real n) \<ge> 1/2"

119 by - (erule subst)

120 }

121 thus "0 < m \<longrightarrow> 1 / 2 \<le> (\<Sum>n\<in>(?S m). 1 / real n)" by simp

122 qed

124 text {* We then show that the sum of a finite number of terms from the

125 harmonic series can be regrouped in increasing powers of 2. For

126 example: $1 + \frac{1}{2} + \frac{1}{3} + \frac{1}{4} + \frac{1}{5} +

127 \frac{1}{6} + \frac{1}{7} + \frac{1}{8} = 1 + (\frac{1}{2}) +

128 (\frac{1}{3} + \frac{1}{4}) + (\frac{1}{5} + \frac{1}{6} + \frac{1}{7}

129 + \frac{1}{8})$. *}

131 lemma harmonic_aux2 [rule_format]:

132 "0<M \<Longrightarrow> (\<Sum>n\<in>{1..(2::nat)^M}. 1/real n) =

133 (1 + (\<Sum>m\<in>{1..M}. \<Sum>n\<in>{(2::nat)^(m - 1)+1..2^m}. 1/real n))"

134 (is "0<M \<Longrightarrow> ?LHS M = ?RHS M")

135 proof (induct M)

136 case 0 show ?case by simp

137 next

138 case (Suc M)

139 have ant: "0 < Suc M" by fact

140 {

141 have suc: "?LHS (Suc M) = ?RHS (Suc M)"

142 proof cases -- "show that LHS = c and RHS = c, and thus LHS = RHS"

143 assume mz: "M=0"

144 {

145 then have

146 "?LHS (Suc M) = ?LHS 1" by simp

147 also have

148 "\<dots> = (\<Sum>n\<in>{(1::nat)..2}. 1/real n)" by simp

149 also have

150 "\<dots> = ((\<Sum>n\<in>{Suc 1..2}. 1/real n) + 1/(real (1::nat)))"

151 by (subst setsum_head)

152 (auto simp: atLeastSucAtMost_greaterThanAtMost)

153 also have

154 "\<dots> = ((\<Sum>n\<in>{2..2::nat}. 1/real n) + 1/(real (1::nat)))"

155 by (simp add: nat_number)

156 also have

157 "\<dots> = 1/(real (2::nat)) + 1/(real (1::nat))" by simp

158 finally have

159 "?LHS (Suc M) = 1/2 + 1" by simp

160 }

161 moreover

162 {

163 from mz have

164 "?RHS (Suc M) = ?RHS 1" by simp

165 also have

166 "\<dots> = (\<Sum>n\<in>{((2::nat)^0)+1..2^1}. 1/real n) + 1"

167 by simp

168 also have

169 "\<dots> = (\<Sum>n\<in>{2::nat..2}. 1/real n) + 1"

170 proof -

171 have "(2::nat)^0 = 1" by simp

172 then have "(2::nat)^0+1 = 2" by simp

173 moreover have "(2::nat)^1 = 2" by simp

174 ultimately have "{((2::nat)^0)+1..2^1} = {2::nat..2}" by auto

175 thus ?thesis by simp

176 qed

177 also have

178 "\<dots> = 1/2 + 1"

179 by simp

180 finally have

181 "?RHS (Suc M) = 1/2 + 1" by simp

182 }

183 ultimately show "?LHS (Suc M) = ?RHS (Suc M)" by simp

184 next

185 assume mnz: "M\<noteq>0"

186 then have mgtz: "M>0" by simp

187 with Suc have suc:

188 "(?LHS M) = (?RHS M)" by blast

189 have

190 "(?LHS (Suc M)) =

191 ((?LHS M) + (\<Sum>n\<in>{(2::nat)^M+1..2^(Suc M)}. 1 / real n))"

192 proof -

193 have

194 "{1..(2::nat)^(Suc M)} =

195 {1..(2::nat)^M}\<union>{(2::nat)^M+1..(2::nat)^(Suc M)}"

196 by auto

197 moreover have

198 "{1..(2::nat)^M}\<inter>{(2::nat)^M+1..(2::nat)^(Suc M)} = {}"

199 by auto

200 moreover have

201 "finite {1..(2::nat)^M}" and "finite {(2::nat)^M+1..(2::nat)^(Suc M)}"

202 by auto

203 ultimately show ?thesis

204 by (auto intro: setsum_Un_disjoint)

205 qed

206 moreover

207 {

208 have

209 "(?RHS (Suc M)) =

210 (1 + (\<Sum>m\<in>{1..M}. \<Sum>n\<in>{(2::nat)^(m - 1)+1..2^m}. 1/real n) +

211 (\<Sum>n\<in>{(2::nat)^(Suc M - 1)+1..2^(Suc M)}. 1/real n))" by simp

212 also have

213 "\<dots> = (?RHS M) + (\<Sum>n\<in>{(2::nat)^M+1..2^(Suc M)}. 1/real n)"

214 by simp

215 also from suc have

216 "\<dots> = (?LHS M) + (\<Sum>n\<in>{(2::nat)^M+1..2^(Suc M)}. 1/real n)"

217 by simp

218 finally have

219 "(?RHS (Suc M)) = \<dots>" by simp

220 }

221 ultimately show "?LHS (Suc M) = ?RHS (Suc M)" by simp

222 qed

223 }

224 thus ?case by simp

225 qed

227 text {* Using @{thm [source] harmonic_aux} and @{thm [source] harmonic_aux2} we now show

228 that each group sum is greater than or equal to $\frac{1}{2}$ and thus

229 the finite sum is bounded below by a value proportional to the number

230 of elements we choose. *}

232 lemma harmonic_aux3 [rule_format]:

233 shows "\<forall>(M::nat). (\<Sum>n\<in>{1..(2::nat)^M}. 1 / real n) \<ge> 1 + (real M)/2"

234 (is "\<forall>M. ?P M \<ge> _")

235 proof (rule allI, cases)

236 fix M::nat

237 assume "M=0"

238 then show "?P M \<ge> 1 + (real M)/2" by simp

239 next

240 fix M::nat

241 assume "M\<noteq>0"

242 then have "M > 0" by simp

243 then have

244 "(?P M) =

245 (1 + (\<Sum>m\<in>{1..M}. \<Sum>n\<in>{(2::nat)^(m - 1)+1..2^m}. 1/real n))"

246 by (rule harmonic_aux2)

247 also have

248 "\<dots> \<ge> (1 + (\<Sum>m\<in>{1..M}. 1/2))"

249 proof -

250 let ?f = "(\<lambda>x. 1/2)"

251 let ?g = "(\<lambda>x. (\<Sum>n\<in>{(2::nat)^(x - 1)+1..2^x}. 1/real n))"

252 from harmonic_aux have "\<And>x. x\<in>{1..M} \<Longrightarrow> ?f x \<le> ?g x" by simp

253 then have "(\<Sum>m\<in>{1..M}. ?g m) \<ge> (\<Sum>m\<in>{1..M}. ?f m)" by (rule setsum_mono)

254 thus ?thesis by simp

255 qed

256 finally have "(?P M) \<ge> (1 + (\<Sum>m\<in>{1..M}. 1/2))" .

257 moreover

258 {

259 have

260 "(\<Sum>m\<in>{1..M}. (1::real)/2) = 1/2 * (\<Sum>m\<in>{1..M}. 1)"

261 by auto

262 also have

263 "\<dots> = 1/2*(real (card {1..M}))"

264 by (simp only: real_of_card[symmetric])

265 also have

266 "\<dots> = 1/2*(real M)" by simp

267 also have

268 "\<dots> = (real M)/2" by simp

269 finally have "(\<Sum>m\<in>{1..M}. (1::real)/2) = (real M)/2" .

270 }

271 ultimately show "(?P M) \<ge> (1 + (real M)/2)" by simp

272 qed

274 text {* The final theorem shows that as we take more and more elements

275 (see @{thm [source] harmonic_aux3}) we get an ever increasing sum. By assuming

276 the sum converges, the lemma @{thm [source] series_pos_less} ( @{thm

277 series_pos_less} ) states that each sum is bounded above by the

278 series' limit. This contradicts our first statement and thus we prove

279 that the harmonic series is divergent. *}

281 theorem DivergenceOfHarmonicSeries:

282 shows "\<not>summable (\<lambda>n. 1/real (Suc n))"

283 (is "\<not>summable ?f")

284 proof -- "by contradiction"

285 let ?s = "suminf ?f" -- "let ?s equal the sum of the harmonic series"

286 assume sf: "summable ?f"

287 then obtain n::nat where ndef: "n = nat \<lceil>2 * ?s\<rceil>" by simp

288 then have ngt: "1 + real n/2 > ?s"

289 proof -

290 have "\<forall>n. 0 \<le> ?f n" by simp

291 with sf have "?s \<ge> 0"

292 by - (rule suminf_0_le, simp_all)

293 then have cgt0: "\<lceil>2*?s\<rceil> \<ge> 0" by simp

295 from ndef have "n = nat \<lceil>(2*?s)\<rceil>" .

296 then have "real n = real (nat \<lceil>2*?s\<rceil>)" by simp

297 with cgt0 have "real n = real \<lceil>2*?s\<rceil>"

298 by (auto dest: real_nat_eq_real)

299 then have "real n \<ge> 2*(?s)" by simp

300 then have "real n/2 \<ge> (?s)" by simp

301 then show "1 + real n/2 > (?s)" by simp

302 qed

304 obtain j where jdef: "j = (2::nat)^n" by simp

305 have "\<forall>m\<ge>j. 0 < ?f m" by simp

306 with sf have "(\<Sum>i\<in>{0..<j}. ?f i) < ?s" by (rule series_pos_less)

307 then have "(\<Sum>i\<in>{1..<Suc j}. 1/(real i)) < ?s"

308 apply -

309 apply (subst(asm) setsum_shift_bounds_Suc_ivl [symmetric])

310 by simp

311 with jdef have

312 "(\<Sum>i\<in>{1..< Suc ((2::nat)^n)}. 1 / (real i)) < ?s" by simp

313 then have

314 "(\<Sum>i\<in>{1..(2::nat)^n}. 1 / (real i)) < ?s"

315 by (simp only: atLeastLessThanSuc_atLeastAtMost)

316 moreover from harmonic_aux3 have

317 "(\<Sum>i\<in>{1..(2::nat)^n}. 1 / (real i)) \<ge> 1 + real n/2" by simp

318 moreover from ngt have "1 + real n/2 > ?s" by simp

319 ultimately show False by simp

320 qed

322 end