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

src/HOL/ex/HarmonicSeries.thy

author | wenzelm |

Wed Jun 22 10:09:20 2016 +0200 (2016-06-22) | |

changeset 63343 | fb5d8a50c641 |

parent 63040 | eb4ddd18d635 |

child 64267 | b9a1486e79be |

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

bundle lifting_syntax;

1 (* Title: HOL/ex/HarmonicSeries.thy

2 Author: Benjamin Porter, 2006

3 *)

5 section \<open>Divergence of the Harmonic Series\<close>

7 theory HarmonicSeries

8 imports Complex_Main

9 begin

11 subsection \<open>Abstract\<close>

13 text \<open>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 \<close>

38 subsection \<open>Formal Proof\<close>

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 \<open>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}$.\<close>

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 "inverse (real x) \<ge> inverse (real ((2::nat)^m))" by simp

76 moreover

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

78 then have

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

80 by (rule nonzero_inverse_eq_divide)

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

82 then have

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

84 by (rule nonzero_inverse_eq_divide)

85 ultimately show

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

87 qed

88 then have

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

90 by (rule setsum_mono)

91 moreover have

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

93 proof -

94 have

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

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

97 by simp

98 also have

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

100 by (simp add: real_of_card)

101 also have

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

103 by (simp add: tmdef)

104 also from mgt0 have

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

106 by (auto simp: tmdef dest: two_pow_sub)

107 also have

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

109 by (simp add: tmdef)

110 also from mgt0 have

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

112 by auto

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

114 finally show ?thesis .

115 qed

116 ultimately have

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

118 by - (erule subst)

119 }

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

121 qed

123 text \<open>We then show that the sum of a finite number of terms from the

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

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

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

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

128 + \frac{1}{8})$.\<close>

130 lemma harmonic_aux2 [rule_format]:

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

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

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

134 proof (induct M)

135 case 0 show ?case by simp

136 next

137 case (Suc M)

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

139 {

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

141 proof cases \<comment> "show that LHS = c and RHS = c, and thus LHS = RHS"

142 assume mz: "M=0"

143 {

144 then have

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

146 also have

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

148 also have

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

150 by (subst setsum_head)

151 (auto simp: atLeastSucAtMost_greaterThanAtMost)

152 also have

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

154 by (simp add: eval_nat_numeral)

155 also have

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

157 finally have

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

159 }

160 moreover

161 {

162 from mz have

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

164 also have

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

166 by simp

167 also have

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

169 by (auto simp: atLeastAtMost_singleton')

170 also have

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

172 by simp

173 finally have

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

175 }

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

177 next

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

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

180 with Suc have suc:

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

182 have

183 "(?LHS (Suc M)) =

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

185 proof -

186 have

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

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

189 by auto

190 moreover have

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

192 by auto

193 moreover have

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

195 by auto

196 ultimately show ?thesis

197 by (auto intro: setsum.union_disjoint)

198 qed

199 moreover

200 {

201 have

202 "(?RHS (Suc M)) =

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

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

205 also have

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

207 by simp

208 also from suc have

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

210 by simp

211 finally have

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

213 }

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

215 qed

216 }

217 thus ?case by simp

218 qed

220 text \<open>Using @{thm [source] harmonic_aux} and @{thm [source] harmonic_aux2} we now show

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

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

223 of elements we choose.\<close>

225 lemma harmonic_aux3 [rule_format]:

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

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

228 proof (rule allI, cases)

229 fix M::nat

230 assume "M=0"

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

232 next

233 fix M::nat

234 assume "M\<noteq>0"

235 then have "M > 0" by simp

236 then have

237 "(?P M) =

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

239 by (rule harmonic_aux2)

240 also have

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

242 proof -

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

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

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

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

247 thus ?thesis by simp

248 qed

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

250 moreover

251 {

252 have

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

254 by auto

255 also have

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

257 by (simp only: real_of_card[symmetric])

258 also have

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

260 also have

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

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

263 }

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

265 qed

267 text \<open>The final theorem shows that as we take more and more elements

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

269 the sum converges, the lemma @{thm [source] setsum_less_suminf} ( @{thm

270 setsum_less_suminf} ) states that each sum is bounded above by the

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

272 that the harmonic series is divergent.\<close>

274 theorem DivergenceOfHarmonicSeries:

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

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

277 proof \<comment> "by contradiction"

278 let ?s = "suminf ?f" \<comment> "let ?s equal the sum of the harmonic series"

279 assume sf: "summable ?f"

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

281 then have ngt: "1 + real n/2 > ?s" by linarith

282 define j where "j = (2::nat)^n"

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

284 with sf have "(\<Sum>i<j. ?f i) < ?s" by (rule setsum_less_suminf)

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

286 unfolding setsum_shift_bounds_Suc_ivl by (simp add: atLeast0LessThan)

287 with j_def have

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

289 then have

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

291 by (simp only: atLeastLessThanSuc_atLeastAtMost)

292 moreover from harmonic_aux3 have

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

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

295 ultimately show False by simp

296 qed

298 end