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