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