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