Quelle  HarmonicSeries.thy

(*  Title:      HOL/ex/HarmonicSeries.thy
    Author:     Benjamin Porter, 2006
*)

section ‹Divergence of the Harmonic Series›

theory HarmonicSeries
imports Complex_Main
begin

subsection ‹Abstract›

text ‹The following document presents a proof of the Divergence of
  Series theorem formalised in the Isabelle/Isar theorem
  system.

 \em Theorem:} The series $\sum_{n=1}^{\infty} \frac{1}{n}$ does not
  to any number.

 \em Informal Proof:}
 The informal proof is based on the following auxillary lemmas:
 \begin{itemize}
 \item{aux: $\sum_{n=2^m-1}^{2^m} \frac{1}{n} \geq \frac{1}{2}$}
 \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}$}
 \end{itemize}

 From {\em aux} and {\em aux2} we can deduce that $\sum_{n=1}^{2^M}
 \frac{1}{n} \geq 1 + \frac{M}{2}$ for all $M$.
 Now for contradiction, assume that $\sum_{n=1}^{\infty} \frac{1}{n}
 = s$ for some $s$. Because $\forall n. \frac{1}{n} > 0$ all the
 partial sums in the series must be less than $s$. However with our
 deduction above we can choose $N > 2*s - 2$ and thus
 $\sum_{n=1}^{2^N} \frac{1}{n} > s$. This leads to a contradiction
 and hence $\sum_{n=1}^{\infty} \frac{1}{n}$ is not summable.
 QED.
 ›

subsection ‹Formal Proof›

lemma two_pow_sub:
  "0 < m ==> (2::nat)^m - 2^(m - 1) = 2^(m - 1)"
  by (induct m) auto

text ‹We first prove the following auxillary lemma. This lemma
  states that the finite sums: $\frac{1}{2}$, $\frac{1}{3} +
 frac{1}{4}$, $\frac{1}{5} + \frac{1}{6} + \frac{1}{7} + \frac{1}{8}$
 . are all greater than or equal to $\frac{1}{2}$. We do this by
  that each term in the sum is greater than or equal to the
  term, e.g. $\frac{1}{3} > \frac{1}{4}$ and thus $\frac{1}{3} +
 frac{1}{4} > \frac{1}{4} + \frac{1}{4} = \frac{1}{2}$.›

lemma harmonic_aux:
  "∀m>0. (∑n∈{(2::nat)^(m - 1)+1..2^m}. 1/real n) ≥ 1/2"
  (is "∀m>0. (∑n∈(?S m). 1/real n) ≥ 1/2")
proof
  fix m::nat
  obtain tm where tmdef: "tm = (2::nat)^m" by simp
  {
    assume mgt0: "0 < m"
    have "∧x. x∈(?S m) ==> 1/(real x) ≥ 1/(real tm)"
    proof -
      fix x::nat
      assume xs: "x∈(?S m)"
      have xgt0: "x>0"
      proof -
        from xs have
          "x ≥ 2^(m - 1) + 1" by auto
        moreover from mgt0 have
          "2^(m - 1) + 1 ≥ (1::nat)" by auto
        ultimately have
          "x ≥ 1" by (rule xtrans)
        thus ?thesis by simp
      qed
      moreover from xs have "x ≤ 2^m" by auto
      ultimately have "inverse (real x) ≥ inverse (real ((2::nat)^m))" by simp
      moreover
      from xgt0 have "real x ≠ 0" by simp
      then have
        "inverse (real x) = 1 / (real x)"
        by (rule nonzero_inverse_eq_divide)
      moreover from mgt0 have "real tm ≠ 0" by (simp add: tmdef)
      then have
        "inverse (real tm) = 1 / (real tm)"
        by (rule nonzero_inverse_eq_divide)
      ultimately show
        "1/(real x) ≥ 1/(real tm)" by (auto simp add: tmdef)
    qed
    then have
      "(∑n∈(?S m). 1 / real n) ≥ (∑n∈(?S m). 1/(real tm))"
      by (rule sum_mono)
    moreover have
      "(∑n∈(?S m). 1/(real tm)) = 1/2"
    proof -
      have
        "(∑n∈(?S m). 1/(real tm)) =
         (1/(real tm))*(∑n∈(?S m). 1)"
        by simp
      also have
        "… = ((1/(real tm)) * real (card (?S m)))"
        by (simp add: real_of_card)
      also have
        "… = ((1/(real tm)) * real (tm - (2^(m - 1))))"
        by (simp add: tmdef)
      also from mgt0 have
        "… = ((1/(real tm)) * real ((2::nat)^(m - 1)))"
        using tmdef two_pow_sub by presburger
      also have
        "… = (real (2::nat))^(m - 1) / (real (2::nat))^m"
        by (simp add: tmdef)
      also from mgt0 have
        "… = (real (2::nat))^(m - 1) / (real (2::nat))^((m - 1) + 1)"
        by auto
      also have "… = 1/2" by simp
      finally show ?thesis .
    qed
    ultimately have
      "(∑n∈(?S m). 1 / real n) ≥ 1/2"
      by - (erule subst)
  }
  thus "0 < m ⟶ 1 / 2 ≤ (∑n∈(?S m). 1 / real n)" by simp
qed

text ‹We then show that the sum of a finite number of terms from the
  series can be regrouped in increasing powers of 2. For
 : $1 + \frac{1}{2} + \frac{1}{3} + \frac{1}{4} + \frac{1}{5} +
 frac{1}{6} + \frac{1}{7} + \frac{1}{8} = 1 + (\frac{1}{2}) +
 \frac{1}{3} + \frac{1}{4}) + (\frac{1}{5} + \frac{1}{6} + \frac{1}{7}
  \frac{1}{8})$.›

lemma harmonic_aux2 [rule_format]:
  "0<M ==> (∑n∈{1..(2::nat)^M}. 1/real n) =
   (1 + (∑m∈{1..M}. ∑n∈{(2::nat)^(m - 1)+1..2^m}. 1/real n))"
  (is "0<M ==> ?LHS M = ?RHS M")
proof (induct M)
  case 0 show ?case by simp
next
  case (Suc M)
  have ant: "0 < Suc M" by fact
  {
    have suc: "?LHS (Suc M) = ?RHS (Suc M)"
    proof cases ― ‹show that LHS = c and RHS = c, and thus LHS = RHS›
      assume mz: "M=0"
      {
        then have
          "?LHS (Suc M) = ?LHS 1" by simp
        also have
          "… = (∑n∈{(1::nat)..2}. 1/real n)" by simp
        also have
          "… = ((∑n∈{Suc 1..2}. 1/real n) + 1/(real (1::nat)))"
          by (subst sum.head)
             (auto simp: atLeastSucAtMost_greaterThanAtMost)
        also have
          "… = ((∑n∈{2..2::nat}. 1/real n) + 1/(real (1::nat)))"
          by (simp add: eval_nat_numeral)
        also have
          "… = 1/(real (2::nat)) + 1/(real (1::nat))" by simp
        finally have
          "?LHS (Suc M) = 1/2 + 1" by simp
      }
      moreover
      {
        from mz have
          "?RHS (Suc M) = ?RHS 1" by simp
        also have
          "… = (∑n∈{((2::nat)^0)+1..2^1}. 1/real n) + 1"
          by simp
        also have
          "… = (∑n∈{2::nat..2}. 1/real n) + 1"
          by (auto simp: atLeastAtMost_singleton')
        also have
          "… = 1/2 + 1"
          by simp
        finally have
          "?RHS (Suc M) = 1/2 + 1" by simp
      }
      ultimately show "?LHS (Suc M) = ?RHS (Suc M)" by simp
    next
      assume mnz: "M≠0"
      then have mgtz: "M>0" by simp
      with Suc have suc:
        "(?LHS M) = (?RHS M)" by blast
      have
        "(?LHS (Suc M)) =
         ((?LHS M) + (∑n∈{(2::nat)^M+1..2^(Suc M)}. 1 / real n))"
      proof -
        have
          "{1..(2::nat)^(Suc M)} =
           {1..(2::nat)^M}∪{(2::nat)^M+1..(2::nat)^(Suc M)}"
          by auto
        moreover have
          "{1..(2::nat)^M}∩{(2::nat)^M+1..(2::nat)^(Suc M)} = {}"
          by auto
        moreover have
          "finite {1..(2::nat)^M}" and "finite {(2::nat)^M+1..(2::nat)^(Suc M)}"
          by auto
        ultimately show ?thesis
          by (auto intro: sum.union_disjoint)
      qed
      moreover
      {
        have
          "(?RHS (Suc M)) =
           (1 + (∑m∈{1..M}. ∑n∈{(2::nat)^(m - 1)+1..2^m}. 1/real n) +
           (∑n∈{(2::nat)^(Suc M - 1)+1..2^(Suc M)}. 1/real n))" by simp
        also have
          "… = (?RHS M) + (∑n∈{(2::nat)^M+1..2^(Suc M)}. 1/real n)"
          by simp
        also from suc have
          "… = (?LHS M) + (∑n∈{(2::nat)^M+1..2^(Suc M)}. 1/real n)"
          by simp
        finally have
          "(?RHS (Suc M)) = …" by simp
      }
      ultimately show "?LHS (Suc M) = ?RHS (Suc M)" by simp
    qed
  }
  thus ?case by simp
qed

text ‹Using @{thm [source] harmonic_aux} and @{thm [source] harmonic_aux2} we now show
  each group sum is greater than or equal to $\frac{1}{2}$ and thus
  finite sum is bounded below by a value proportional to the number
  elements we choose.›

lemma harmonic_aux3 [rule_format]:
  shows "∀(M::nat). (∑n∈{1..(2::nat)^M}. 1 / real n) ≥ 1 + (real M)/2"
  (is "∀M. ?P M ≥ _")
proof (rule allI, cases)
  fix M::nat
  assume "M=0"
  then show "?P M ≥ 1 + (real M)/2" by simp
next
  fix M::nat
  assume "M≠0"
  then have "M > 0" by simp
  then have
    "(?P M) =
     (1 + (∑m∈{1..M}. ∑n∈{(2::nat)^(m - 1)+1..2^m}. 1/real n))"
    by (rule harmonic_aux2)
  also have
    "… ≥ (1 + (∑m∈{1..M}. 1/2))"
  proof -
    let ?f = "(λx. 1/2)"
    let ?g = "(λx. (∑n∈{(2::nat)^(x - 1)+1..2^x}. 1/real n))"
    from harmonic_aux have "∧x. x∈{1..M} ==> ?f x ≤ ?g x" by simp
    then have "(∑m∈{1..M}. ?g m) ≥ (∑m∈{1..M}. ?f m)" by (rule sum_mono)
    thus ?thesis by simp
  qed
  finally have "(?P M) ≥ (1 + (∑m∈{1..M}. 1/2))" .
  moreover
  {
    have
      "(∑m∈{1..M}. (1::real)/2) = 1/2 * (∑m∈{1..M}. 1)"
      by auto
    also have
      "… = 1/2*(real (card {1..M}))"
      by (simp only: real_of_card[symmetric])
    also have
      "… = 1/2*(real M)" by simp
    also have
      "… = (real M)/2" by simp
    finally have "(∑m∈{1..M}. (1::real)/2) = (real M)/2" .
  }
  ultimately show "(?P M) ≥ (1 + (real M)/2)" by simp
qed

text ‹The final theorem shows that as we take more and more elements
 see @{thm [source] harmonic_aux3}) we get an ever increasing sum. By assuming
  sum converges, the lemma @{thm [source] sum_less_suminf} ( @{thm
 } ) states that each sum is bounded above by the
 ' limit. This contradicts our first statement and thus we prove
  the harmonic series is divergent.›

theorem DivergenceOfHarmonicSeries:
  shows "¬summable (λn. 1/real (Suc n))"
  (is "¬summable ?f")
proof ― ‹by contradiction›
  let ?s = "suminf ?f" ― ‹let ?s equal the sum of the harmonic series›
  assume sf: "summable ?f"
  then obtain n::nat where ndef: "n = nat ⌈2 * ?s⌉" by simp
  then have ngt: "1 + real n/2 > ?s" by linarith
  define j where "j = (2::nat)^n"
  have "(∑i<j. ?f i) < ?s" 
    using sf by (simp add: sum_less_suminf)
  then have "(∑i∈{Suc 0..<Suc j}. 1/(real i)) < ?s"
    unfolding sum.shift_bounds_Suc_ivl by (simp add: atLeast0LessThan)
  with j_def have
    "(∑i∈{1..< Suc ((2::nat)^n)}. 1 / (real i)) < ?s" by simp
  then have
    "(∑i∈{1..(2::nat)^n}. 1 / (real i)) < ?s"
    by (simp only: atLeastLessThanSuc_atLeastAtMost)
  moreover from harmonic_aux3 have
    "(∑i∈{1..(2::nat)^n}. 1 / (real i)) ≥ 1 + real n/2" by simp
  moreover from ngt have "1 + real n/2 > ?s" by simp
  ultimately show False by simp
qed

end