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