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
wenzelm@56788
     1
(*  Title:      HOL/ex/HarmonicSeries.thy
wenzelm@56788
     2
    Author:     Benjamin Porter, 2006
wenzelm@56788
     3
*)
wenzelm@56788
     4
wenzelm@56788
     5
header {* 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 \<Longrightarrow> (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
  "\<forall>m>0. (\<Sum>n\<in>{(2::nat)^(m - 1)+1..2^m}. 1/real n) \<ge> 1/2"
wenzelm@56788
    54
  (is "\<forall>m>0. (\<Sum>n\<in>(?S m). 1/real n) \<ge> 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 "\<And>x. x\<in>(?S m) \<Longrightarrow> 1/(real x) \<ge> 1/(real tm)"
wenzelm@56788
    61
    proof -
wenzelm@56788
    62
      fix x::nat
wenzelm@56788
    63
      assume xs: "x\<in>(?S m)"
wenzelm@56788
    64
      have xgt0: "x>0"
wenzelm@56788
    65
      proof -
wenzelm@56788
    66
        from xs have
wenzelm@56788
    67
          "x \<ge> 2^(m - 1) + 1" by auto
wenzelm@56788
    68
        moreover from mgt0 have
wenzelm@56788
    69
          "2^(m - 1) + 1 \<ge> (1::nat)" by auto
wenzelm@56788
    70
        ultimately have
wenzelm@56788
    71
          "x \<ge> 1" by (rule xtrans)
wenzelm@56788
    72
        thus ?thesis by simp
wenzelm@56788
    73
      qed
wenzelm@56788
    74
      moreover from xs have "x \<le> 2^m" by auto
wenzelm@56788
    75
      ultimately have
wenzelm@56788
    76
        "inverse (real x) \<ge> 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 \<noteq> 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 \<noteq> 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) \<ge> 1/(real tm)" by (auto simp add: tmdef)
wenzelm@56788
    89
    qed
wenzelm@56788
    90
    then have
wenzelm@56788
    91
      "(\<Sum>n\<in>(?S m). 1 / real n) \<ge> (\<Sum>n\<in>(?S m). 1/(real tm))"
wenzelm@56788
    92
      by (rule setsum_mono)
wenzelm@56788
    93
    moreover have
wenzelm@56788
    94
      "(\<Sum>n\<in>(?S m). 1/(real tm)) = 1/2"
wenzelm@56788
    95
    proof -
wenzelm@56788
    96
      have
wenzelm@56788
    97
        "(\<Sum>n\<in>(?S m). 1/(real tm)) =
wenzelm@56788
    98
         (1/(real tm))*(\<Sum>n\<in>(?S m). 1)"
wenzelm@56788
    99
        by simp
wenzelm@56788
   100
      also have
wenzelm@56788
   101
        "\<dots> = ((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
        "\<dots> = ((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
        "\<dots> = ((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
        "\<dots> = (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
        "\<dots> = (real (2::nat))^(m - 1) / (real (2::nat))^((m - 1) + 1)"
wenzelm@56788
   114
        by auto
wenzelm@56788
   115
      also have "\<dots> = 1/2" by simp
wenzelm@56788
   116
      finally show ?thesis .
wenzelm@56788
   117
    qed
wenzelm@56788
   118
    ultimately have
wenzelm@56788
   119
      "(\<Sum>n\<in>(?S m). 1 / real n) \<ge> 1/2"
wenzelm@56788
   120
      by - (erule subst)
wenzelm@56788
   121
  }
wenzelm@56788
   122
  thus "0 < m \<longrightarrow> 1 / 2 \<le> (\<Sum>n\<in>(?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<M \<Longrightarrow> (\<Sum>n\<in>{1..(2::nat)^M}. 1/real n) =
wenzelm@56788
   134
   (1 + (\<Sum>m\<in>{1..M}. \<Sum>n\<in>{(2::nat)^(m - 1)+1..2^m}. 1/real n))"
wenzelm@56788
   135
  (is "0<M \<Longrightarrow> ?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
          "\<dots> = (\<Sum>n\<in>{(1::nat)..2}. 1/real n)" by simp
wenzelm@56788
   150
        also have
wenzelm@56788
   151
          "\<dots> = ((\<Sum>n\<in>{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
          "\<dots> = ((\<Sum>n\<in>{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
          "\<dots> =  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
          "\<dots> = (\<Sum>n\<in>{((2::nat)^0)+1..2^1}. 1/real n) + 1"
wenzelm@56788
   168
          by simp
wenzelm@56788
   169
        also have
wenzelm@56788
   170
          "\<dots> = (\<Sum>n\<in>{2::nat..2}. 1/real n) + 1"
wenzelm@56788
   171
          by (auto simp: atLeastAtMost_singleton')
wenzelm@56788
   172
        also have
wenzelm@56788
   173
          "\<dots> = 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\<noteq>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) + (\<Sum>n\<in>{(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}\<union>{(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}\<inter>{(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 + (\<Sum>m\<in>{1..M}.  \<Sum>n\<in>{(2::nat)^(m - 1)+1..2^m}. 1/real n) +
wenzelm@56788
   206
           (\<Sum>n\<in>{(2::nat)^(Suc M - 1)+1..2^(Suc M)}. 1/real n))" by simp
wenzelm@56788
   207
        also have
wenzelm@56788
   208
          "\<dots> = (?RHS M) + (\<Sum>n\<in>{(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
          "\<dots> = (?LHS M) +  (\<Sum>n\<in>{(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)) = \<dots>" 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 "\<forall>(M::nat). (\<Sum>n\<in>{1..(2::nat)^M}. 1 / real n) \<ge> 1 + (real M)/2"
wenzelm@56788
   229
  (is "\<forall>M. ?P M \<ge> _")
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 \<ge> 1 + (real M)/2" by simp
wenzelm@56788
   234
next
wenzelm@56788
   235
  fix M::nat
wenzelm@56788
   236
  assume "M\<noteq>0"
wenzelm@56788
   237
  then have "M > 0" by simp
wenzelm@56788
   238
  then have
wenzelm@56788
   239
    "(?P M) =
wenzelm@56788
   240
     (1 + (\<Sum>m\<in>{1..M}. \<Sum>n\<in>{(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
    "\<dots> \<ge> (1 + (\<Sum>m\<in>{1..M}. 1/2))"
wenzelm@56788
   244
  proof -
wenzelm@56788
   245
    let ?f = "(\<lambda>x. 1/2)"
wenzelm@56788
   246
    let ?g = "(\<lambda>x. (\<Sum>n\<in>{(2::nat)^(x - 1)+1..2^x}. 1/real n))"
wenzelm@56788
   247
    from harmonic_aux have "\<And>x. x\<in>{1..M} \<Longrightarrow> ?f x \<le> ?g x" by simp
wenzelm@56788
   248
    then have "(\<Sum>m\<in>{1..M}. ?g m) \<ge> (\<Sum>m\<in>{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) \<ge> (1 + (\<Sum>m\<in>{1..M}. 1/2))" .
wenzelm@56788
   252
  moreover
wenzelm@56788
   253
  {
wenzelm@56788
   254
    have
wenzelm@56788
   255
      "(\<Sum>m\<in>{1..M}. (1::real)/2) = 1/2 * (\<Sum>m\<in>{1..M}. 1)"
wenzelm@56788
   256
      by auto
wenzelm@56788
   257
    also have
wenzelm@56788
   258
      "\<dots> = 1/2*(real (card {1..M}))"
wenzelm@56788
   259
      by (simp only: real_of_card[symmetric])
wenzelm@56788
   260
    also have
wenzelm@56788
   261
      "\<dots> = 1/2*(real M)" by simp
wenzelm@56788
   262
    also have
wenzelm@56788
   263
      "\<dots> = (real M)/2" by simp
wenzelm@56788
   264
    finally have "(\<Sum>m\<in>{1..M}. (1::real)/2) = (real M)/2" .
wenzelm@56788
   265
  }
wenzelm@56788
   266
  ultimately show "(?P M) \<ge> (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 "\<not>summable (\<lambda>n. 1/real (Suc n))"
wenzelm@56788
   278
  (is "\<not>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 \<lceil>2 * ?s\<rceil>" by simp
wenzelm@56788
   283
  then have ngt: "1 + real n/2 > ?s"
wenzelm@56788
   284
  proof -
wenzelm@56788
   285
    have "\<forall>n. 0 \<le> ?f n" by simp
wenzelm@56788
   286
    with sf have "?s \<ge> 0"
wenzelm@56788
   287
      by (rule suminf_nonneg)
wenzelm@56788
   288
    then have cgt0: "\<lceil>2*?s\<rceil> \<ge> 0" by simp
wenzelm@56788
   289
wenzelm@56788
   290
    from ndef have "n = nat \<lceil>(2*?s)\<rceil>" .
wenzelm@56788
   291
    then have "real n = real (nat \<lceil>2*?s\<rceil>)" by simp
wenzelm@56788
   292
    with cgt0 have "real n = real \<lceil>2*?s\<rceil>"
wenzelm@56788
   293
      by (auto dest: real_nat_eq_real)
wenzelm@56788
   294
    then have "real n \<ge> 2*(?s)" by simp
wenzelm@56788
   295
    then have "real n/2 \<ge> (?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 "\<forall>m\<ge>j. 0 < ?f m" by simp
wenzelm@56788
   301
  with sf have "(\<Sum>i<j. ?f i) < ?s" by (rule setsum_less_suminf)
wenzelm@56788
   302
  then have "(\<Sum>i\<in>{Suc 0..<Suc j}. 1/(real i)) < ?s"
wenzelm@56788
   303
    unfolding setsum_shift_bounds_Suc_ivl by (simp add: atLeast0LessThan)
wenzelm@56788
   304
  with jdef have
wenzelm@56788
   305
    "(\<Sum>i\<in>{1..< Suc ((2::nat)^n)}. 1 / (real i)) < ?s" by simp
wenzelm@56788
   306
  then have
wenzelm@56788
   307
    "(\<Sum>i\<in>{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
    "(\<Sum>i\<in>{1..(2::nat)^n}. 1 / (real i)) \<ge> 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