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

src/HOL/ex/HarmonicSeries.thy

author | haftmann |

Fri Oct 10 19:55:32 2014 +0200 (2014-10-10) | |

changeset 58646 | cd63a4b12a33 |

parent 57418 | 6ab1c7cb0b8d |

child 58889 | 5b7a9633cfa8 |

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

specialized specification: avoid trivial instances

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 from 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.union_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] setsum_less_suminf} ( @{thm

272 setsum_less_suminf} ) 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_nonneg)

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<j. ?f i) < ?s" by (rule setsum_less_suminf)

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

303 unfolding setsum_shift_bounds_Suc_ivl by (simp add: atLeast0LessThan)

304 with jdef have

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

306 then have

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

308 by (simp only: atLeastLessThanSuc_atLeastAtMost)

309 moreover from harmonic_aux3 have

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

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

312 ultimately show False by simp

313 qed

315 end