src/HOL/ex/HarmonicSeries.thy
 author haftmann Fri Oct 10 19:55:32 2014 +0200 (2014-10-10) changeset 58646 cd63a4b12a33 parent 57418 6ab1c7cb0b8d child 58889 5b7a9633cfa8 permissions -rw-r--r--
specialized specification: avoid trivial instances
     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 subsection {* 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 subsection {* 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 from mgt0 have

    69           "2^(m - 1) + 1 \<ge> (1::nat)" by auto

    70         ultimately have

    71           "x \<ge> 1" by (rule xtrans)

    72         thus ?thesis by simp

    73       qed

    74       moreover from xs have "x \<le> 2^m" by auto

    75       ultimately have

    76         "inverse (real x) \<ge> inverse (real ((2::nat)^m))"

    77         by (simp del: real_of_nat_power)

    78       moreover

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

    80       then have

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

    82         by (rule nonzero_inverse_eq_divide)

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

    84       then have

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

    86         by (rule nonzero_inverse_eq_divide)

    87       ultimately show

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

    89     qed

    90     then have

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

    92       by (rule setsum_mono)

    93     moreover have

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

    95     proof -

    96       have

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

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

    99         by simp

   100       also have

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

   102         by (simp add: real_of_card real_of_nat_def)

   103       also have

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

   105         by (simp add: tmdef)

   106       also from mgt0 have

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

   108         by (auto simp: tmdef dest: two_pow_sub)

   109       also have

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

   111         by (simp add: tmdef)

   112       also from mgt0 have

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

   114         by auto

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

   116       finally show ?thesis .

   117     qed

   118     ultimately have

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

   120       by - (erule subst)

   121   }

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

   123 qed

   124

   125 text {* We then show that the sum of a finite number of terms from the

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

   127 example: $1 + \frac{1}{2} + \frac{1}{3} + \frac{1}{4} + \frac{1}{5} +   128 \frac{1}{6} + \frac{1}{7} + \frac{1}{8} = 1 + (\frac{1}{2}) +   129 (\frac{1}{3} + \frac{1}{4}) + (\frac{1}{5} + \frac{1}{6} + \frac{1}{7}   130 + \frac{1}{8})$. *}

   131

   132 lemma harmonic_aux2 [rule_format]:

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

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

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

   136 proof (induct M)

   137   case 0 show ?case by simp

   138 next

   139   case (Suc M)

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

   141   {

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

   143     proof cases -- "show that LHS = c and RHS = c, and thus LHS = RHS"

   144       assume mz: "M=0"

   145       {

   146         then have

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

   148         also have

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

   150         also have

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

   152           by (subst setsum_head)

   153              (auto simp: atLeastSucAtMost_greaterThanAtMost)

   154         also have

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

   156           by (simp add: eval_nat_numeral)

   157         also have

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

   159         finally have

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

   161       }

   162       moreover

   163       {

   164         from mz have

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

   166         also have

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

   168           by simp

   169         also have

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

   171           by (auto simp: atLeastAtMost_singleton')

   172         also have

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

   174           by simp

   175         finally have

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

   177       }

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

   179     next

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

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

   182       with Suc have suc:

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

   184       have

   185         "(?LHS (Suc M)) =

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

   187       proof -

   188         have

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

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

   191           by auto

   192         moreover have

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

   194           by auto

   195         moreover have

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

   197           by auto

   198         ultimately show ?thesis

   199           by (auto intro: setsum.union_disjoint)

   200       qed

   201       moreover

   202       {

   203         have

   204           "(?RHS (Suc M)) =

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

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

   207         also have

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

   209           by simp

   210         also from suc have

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

   212           by simp

   213         finally have

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

   215       }

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

   217     qed

   218   }

   219   thus ?case by simp

   220 qed

   221

   222 text {* Using @{thm [source] harmonic_aux} and @{thm [source] harmonic_aux2} we now show

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

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

   225 of elements we choose. *}

   226

   227 lemma harmonic_aux3 [rule_format]:

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

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

   230 proof (rule allI, cases)

   231   fix M::nat

   232   assume "M=0"

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

   234 next

   235   fix M::nat

   236   assume "M\<noteq>0"

   237   then have "M > 0" by simp

   238   then have

   239     "(?P M) =

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

   241     by (rule harmonic_aux2)

   242   also have

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

   244   proof -

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

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

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

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

   249     thus ?thesis by simp

   250   qed

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

   252   moreover

   253   {

   254     have

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

   256       by auto

   257     also have

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

   259       by (simp only: real_of_card[symmetric])

   260     also have

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

   262     also have

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

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

   265   }

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

   267 qed

   268

   269 text {* The final theorem shows that as we take more and more elements

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

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

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

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

   274 that the harmonic series is divergent. *}

   275

   276 theorem DivergenceOfHarmonicSeries:

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

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

   279 proof -- "by contradiction"

   280   let ?s = "suminf ?f" -- "let ?s equal the sum of the harmonic series"

   281   assume sf: "summable ?f"

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

   283   then have ngt: "1 + real n/2 > ?s"

   284   proof -

   285     have "\<forall>n. 0 \<le> ?f n" by simp

   286     with sf have "?s \<ge> 0"

   287       by (rule suminf_nonneg)

   288     then have cgt0: "\<lceil>2*?s\<rceil> \<ge> 0" by simp

   289

   290     from ndef have "n = nat \<lceil>(2*?s)\<rceil>" .

   291     then have "real n = real (nat \<lceil>2*?s\<rceil>)" by simp

   292     with cgt0 have "real n = real \<lceil>2*?s\<rceil>"

   293       by (auto dest: real_nat_eq_real)

   294     then have "real n \<ge> 2*(?s)" by simp

   295     then have "real n/2 \<ge> (?s)" by simp

   296     then show "1 + real n/2 > (?s)" by simp

   297   qed

   298

   299   obtain j where jdef: "j = (2::nat)^n" by simp

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

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

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

   303     unfolding setsum_shift_bounds_Suc_ivl by (simp add: atLeast0LessThan)

   304   with jdef have

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

   306   then have

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

   308     by (simp only: atLeastLessThanSuc_atLeastAtMost)

   309   moreover from harmonic_aux3 have

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

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

   312   ultimately show False by simp

   313 qed

   314

   315 end