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