wenzelm@56788: (*  Title:      HOL/ex/HarmonicSeries.thy
wenzelm@56788:     Author:     Benjamin Porter, 2006
wenzelm@56788: *)
wenzelm@56788: 
wenzelm@58889: section {* Divergence of the Harmonic Series *}
wenzelm@56788: 
wenzelm@56788: theory HarmonicSeries
wenzelm@56788: imports Complex_Main
wenzelm@56788: begin
wenzelm@56788: 
wenzelm@56788: subsection {* Abstract *}
wenzelm@56788: 
wenzelm@56788: text {* The following document presents a proof of the Divergence of
wenzelm@56788: Harmonic Series theorem formalised in the Isabelle/Isar theorem
wenzelm@56788: proving system.
wenzelm@56788: 
wenzelm@56788: {\em Theorem:} The series $\sum_{n=1}^{\infty} \frac{1}{n}$ does not
wenzelm@56788: converge to any number.
wenzelm@56788: 
wenzelm@56788: {\em Informal Proof:}
wenzelm@56788:   The informal proof is based on the following auxillary lemmas:
wenzelm@56788:   \begin{itemize}
wenzelm@56788:   \item{aux: $\sum_{n=2^m-1}^{2^m} \frac{1}{n} \geq \frac{1}{2}$}
wenzelm@56788:   \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:   \end{itemize}
wenzelm@56788: 
wenzelm@56788:   From {\em aux} and {\em aux2} we can deduce that $\sum_{n=1}^{2^M}
wenzelm@56788:   \frac{1}{n} \geq 1 + \frac{M}{2}$ for all $M$.
wenzelm@56788:   Now for contradiction, assume that $\sum_{n=1}^{\infty} \frac{1}{n}
wenzelm@56788:   = s$ for some $s$. Because $\forall n. \frac{1}{n} > 0$ all the
wenzelm@56788:   partial sums in the series must be less than $s$. However with our
wenzelm@56788:   deduction above we can choose $N > 2*s - 2$ and thus
wenzelm@56788:   $\sum_{n=1}^{2^N} \frac{1}{n} > s$. This leads to a contradiction
wenzelm@56788:   and hence $\sum_{n=1}^{\infty} \frac{1}{n}$ is not summable.
wenzelm@56788:   QED.
wenzelm@56788: *}
wenzelm@56788: 
wenzelm@56788: subsection {* Formal Proof *}
wenzelm@56788: 
wenzelm@56788: lemma two_pow_sub:
wenzelm@56788:   "0 < m \<Longrightarrow> (2::nat)^m - 2^(m - 1) = 2^(m - 1)"
wenzelm@56788:   by (induct m) auto
wenzelm@56788: 
wenzelm@56788: text {* We first prove the following auxillary lemma. This lemma
wenzelm@56788: simply states that the finite sums: $\frac{1}{2}$, $\frac{1}{3} +
wenzelm@56788: \frac{1}{4}$, $\frac{1}{5} + \frac{1}{6} + \frac{1}{7} + \frac{1}{8}$
wenzelm@56788: etc. are all greater than or equal to $\frac{1}{2}$. We do this by
wenzelm@56788: observing that each term in the sum is greater than or equal to the
wenzelm@56788: last term, e.g. $\frac{1}{3} > \frac{1}{4}$ and thus $\frac{1}{3} +
wenzelm@56788: \frac{1}{4} > \frac{1}{4} + \frac{1}{4} = \frac{1}{2}$. *}
wenzelm@56788: 
wenzelm@56788: lemma harmonic_aux:
wenzelm@56788:   "\<forall>m>0. (\<Sum>n\<in>{(2::nat)^(m - 1)+1..2^m}. 1/real n) \<ge> 1/2"
wenzelm@56788:   (is "\<forall>m>0. (\<Sum>n\<in>(?S m). 1/real n) \<ge> 1/2")
wenzelm@56788: proof
wenzelm@56788:   fix m::nat
wenzelm@56788:   obtain tm where tmdef: "tm = (2::nat)^m" by simp
wenzelm@56788:   {
wenzelm@56788:     assume mgt0: "0 < m"
wenzelm@56788:     have "\<And>x. x\<in>(?S m) \<Longrightarrow> 1/(real x) \<ge> 1/(real tm)"
wenzelm@56788:     proof -
wenzelm@56788:       fix x::nat
wenzelm@56788:       assume xs: "x\<in>(?S m)"
wenzelm@56788:       have xgt0: "x>0"
wenzelm@56788:       proof -
wenzelm@56788:         from xs have
wenzelm@56788:           "x \<ge> 2^(m - 1) + 1" by auto
wenzelm@56788:         moreover from mgt0 have
wenzelm@56788:           "2^(m - 1) + 1 \<ge> (1::nat)" by auto
wenzelm@56788:         ultimately have
wenzelm@56788:           "x \<ge> 1" by (rule xtrans)
wenzelm@56788:         thus ?thesis by simp
wenzelm@56788:       qed
wenzelm@56788:       moreover from xs have "x \<le> 2^m" by auto
wenzelm@56788:       ultimately have
wenzelm@56788:         "inverse (real x) \<ge> inverse (real ((2::nat)^m))"
wenzelm@56788:         by (simp del: real_of_nat_power)
wenzelm@56788:       moreover
wenzelm@56788:       from xgt0 have "real x \<noteq> 0" by simp
wenzelm@56788:       then have
wenzelm@56788:         "inverse (real x) = 1 / (real x)"
wenzelm@56788:         by (rule nonzero_inverse_eq_divide)
wenzelm@56788:       moreover from mgt0 have "real tm \<noteq> 0" by (simp add: tmdef)
wenzelm@56788:       then have
wenzelm@56788:         "inverse (real tm) = 1 / (real tm)"
wenzelm@56788:         by (rule nonzero_inverse_eq_divide)
wenzelm@56788:       ultimately show
wenzelm@56788:         "1/(real x) \<ge> 1/(real tm)" by (auto simp add: tmdef)
wenzelm@56788:     qed
wenzelm@56788:     then have
wenzelm@56788:       "(\<Sum>n\<in>(?S m). 1 / real n) \<ge> (\<Sum>n\<in>(?S m). 1/(real tm))"
wenzelm@56788:       by (rule setsum_mono)
wenzelm@56788:     moreover have
wenzelm@56788:       "(\<Sum>n\<in>(?S m). 1/(real tm)) = 1/2"
wenzelm@56788:     proof -
wenzelm@56788:       have
wenzelm@56788:         "(\<Sum>n\<in>(?S m). 1/(real tm)) =
wenzelm@56788:          (1/(real tm))*(\<Sum>n\<in>(?S m). 1)"
wenzelm@56788:         by simp
wenzelm@56788:       also have
wenzelm@56788:         "\<dots> = ((1/(real tm)) * real (card (?S m)))"
wenzelm@56788:         by (simp add: real_of_card real_of_nat_def)
wenzelm@56788:       also have
wenzelm@56788:         "\<dots> = ((1/(real tm)) * real (tm - (2^(m - 1))))"
wenzelm@56788:         by (simp add: tmdef)
wenzelm@56788:       also from mgt0 have
wenzelm@56788:         "\<dots> = ((1/(real tm)) * real ((2::nat)^(m - 1)))"
wenzelm@56788:         by (auto simp: tmdef dest: two_pow_sub)
wenzelm@56788:       also have
wenzelm@56788:         "\<dots> = (real (2::nat))^(m - 1) / (real (2::nat))^m"
wenzelm@56788:         by (simp add: tmdef)
wenzelm@56788:       also from mgt0 have
wenzelm@56788:         "\<dots> = (real (2::nat))^(m - 1) / (real (2::nat))^((m - 1) + 1)"
wenzelm@56788:         by auto
wenzelm@56788:       also have "\<dots> = 1/2" by simp
wenzelm@56788:       finally show ?thesis .
wenzelm@56788:     qed
wenzelm@56788:     ultimately have
wenzelm@56788:       "(\<Sum>n\<in>(?S m). 1 / real n) \<ge> 1/2"
wenzelm@56788:       by - (erule subst)
wenzelm@56788:   }
wenzelm@56788:   thus "0 < m \<longrightarrow> 1 / 2 \<le> (\<Sum>n\<in>(?S m). 1 / real n)" by simp
wenzelm@56788: qed
wenzelm@56788: 
wenzelm@56788: text {* We then show that the sum of a finite number of terms from the
wenzelm@56788: harmonic series can be regrouped in increasing powers of 2. For
wenzelm@56788: example: $1 + \frac{1}{2} + \frac{1}{3} + \frac{1}{4} + \frac{1}{5} +
wenzelm@56788: \frac{1}{6} + \frac{1}{7} + \frac{1}{8} = 1 + (\frac{1}{2}) +
wenzelm@56788: (\frac{1}{3} + \frac{1}{4}) + (\frac{1}{5} + \frac{1}{6} + \frac{1}{7}
wenzelm@56788: + \frac{1}{8})$. *}
wenzelm@56788: 
wenzelm@56788: lemma harmonic_aux2 [rule_format]:
wenzelm@56788:   "0<M \<Longrightarrow> (\<Sum>n\<in>{1..(2::nat)^M}. 1/real n) =
wenzelm@56788:    (1 + (\<Sum>m\<in>{1..M}. \<Sum>n\<in>{(2::nat)^(m - 1)+1..2^m}. 1/real n))"
wenzelm@56788:   (is "0<M \<Longrightarrow> ?LHS M = ?RHS M")
wenzelm@56788: proof (induct M)
wenzelm@56788:   case 0 show ?case by simp
wenzelm@56788: next
wenzelm@56788:   case (Suc M)
wenzelm@56788:   have ant: "0 < Suc M" by fact
wenzelm@56788:   {
wenzelm@56788:     have suc: "?LHS (Suc M) = ?RHS (Suc M)"
wenzelm@56788:     proof cases -- "show that LHS = c and RHS = c, and thus LHS = RHS"
wenzelm@56788:       assume mz: "M=0"
wenzelm@56788:       {
wenzelm@56788:         then have
wenzelm@56788:           "?LHS (Suc M) = ?LHS 1" by simp
wenzelm@56788:         also have
wenzelm@56788:           "\<dots> = (\<Sum>n\<in>{(1::nat)..2}. 1/real n)" by simp
wenzelm@56788:         also have
wenzelm@56788:           "\<dots> = ((\<Sum>n\<in>{Suc 1..2}. 1/real n) + 1/(real (1::nat)))"
wenzelm@56788:           by (subst setsum_head)
wenzelm@56788:              (auto simp: atLeastSucAtMost_greaterThanAtMost)
wenzelm@56788:         also have
wenzelm@56788:           "\<dots> = ((\<Sum>n\<in>{2..2::nat}. 1/real n) + 1/(real (1::nat)))"
wenzelm@56788:           by (simp add: eval_nat_numeral)
wenzelm@56788:         also have
wenzelm@56788:           "\<dots> =  1/(real (2::nat)) + 1/(real (1::nat))" by simp
wenzelm@56788:         finally have
wenzelm@56788:           "?LHS (Suc M) = 1/2 + 1" by simp
wenzelm@56788:       }
wenzelm@56788:       moreover
wenzelm@56788:       {
wenzelm@56788:         from mz have
wenzelm@56788:           "?RHS (Suc M) = ?RHS 1" by simp
wenzelm@56788:         also have
wenzelm@56788:           "\<dots> = (\<Sum>n\<in>{((2::nat)^0)+1..2^1}. 1/real n) + 1"
wenzelm@56788:           by simp
wenzelm@56788:         also have
wenzelm@56788:           "\<dots> = (\<Sum>n\<in>{2::nat..2}. 1/real n) + 1"
wenzelm@56788:           by (auto simp: atLeastAtMost_singleton')
wenzelm@56788:         also have
wenzelm@56788:           "\<dots> = 1/2 + 1"
wenzelm@56788:           by simp
wenzelm@56788:         finally have
wenzelm@56788:           "?RHS (Suc M) = 1/2 + 1" by simp
wenzelm@56788:       }
wenzelm@56788:       ultimately show "?LHS (Suc M) = ?RHS (Suc M)" by simp
wenzelm@56788:     next
wenzelm@56788:       assume mnz: "M\<noteq>0"
wenzelm@56788:       then have mgtz: "M>0" by simp
wenzelm@56788:       with Suc have suc:
wenzelm@56788:         "(?LHS M) = (?RHS M)" by blast
wenzelm@56788:       have
wenzelm@56788:         "(?LHS (Suc M)) =
wenzelm@56788:          ((?LHS M) + (\<Sum>n\<in>{(2::nat)^M+1..2^(Suc M)}. 1 / real n))"
wenzelm@56788:       proof -
wenzelm@56788:         have
wenzelm@56788:           "{1..(2::nat)^(Suc M)} =
wenzelm@56788:            {1..(2::nat)^M}\<union>{(2::nat)^M+1..(2::nat)^(Suc M)}"
wenzelm@56788:           by auto
wenzelm@56788:         moreover have
wenzelm@56788:           "{1..(2::nat)^M}\<inter>{(2::nat)^M+1..(2::nat)^(Suc M)} = {}"
wenzelm@56788:           by auto
wenzelm@56788:         moreover have
wenzelm@56788:           "finite {1..(2::nat)^M}" and "finite {(2::nat)^M+1..(2::nat)^(Suc M)}"
wenzelm@56788:           by auto
wenzelm@56788:         ultimately show ?thesis
haftmann@57418:           by (auto intro: setsum.union_disjoint)
wenzelm@56788:       qed
wenzelm@56788:       moreover
wenzelm@56788:       {
wenzelm@56788:         have
wenzelm@56788:           "(?RHS (Suc M)) =
wenzelm@56788:            (1 + (\<Sum>m\<in>{1..M}.  \<Sum>n\<in>{(2::nat)^(m - 1)+1..2^m}. 1/real n) +
wenzelm@56788:            (\<Sum>n\<in>{(2::nat)^(Suc M - 1)+1..2^(Suc M)}. 1/real n))" by simp
wenzelm@56788:         also have
wenzelm@56788:           "\<dots> = (?RHS M) + (\<Sum>n\<in>{(2::nat)^M+1..2^(Suc M)}. 1/real n)"
wenzelm@56788:           by simp
wenzelm@56788:         also from suc have
wenzelm@56788:           "\<dots> = (?LHS M) +  (\<Sum>n\<in>{(2::nat)^M+1..2^(Suc M)}. 1/real n)"
wenzelm@56788:           by simp
wenzelm@56788:         finally have
wenzelm@56788:           "(?RHS (Suc M)) = \<dots>" by simp
wenzelm@56788:       }
wenzelm@56788:       ultimately show "?LHS (Suc M) = ?RHS (Suc M)" by simp
wenzelm@56788:     qed
wenzelm@56788:   }
wenzelm@56788:   thus ?case by simp
wenzelm@56788: qed
wenzelm@56788: 
wenzelm@56788: text {* Using @{thm [source] harmonic_aux} and @{thm [source] harmonic_aux2} we now show
wenzelm@56788: that each group sum is greater than or equal to $\frac{1}{2}$ and thus
wenzelm@56788: the finite sum is bounded below by a value proportional to the number
wenzelm@56788: of elements we choose. *}
wenzelm@56788: 
wenzelm@56788: lemma harmonic_aux3 [rule_format]:
wenzelm@56788:   shows "\<forall>(M::nat). (\<Sum>n\<in>{1..(2::nat)^M}. 1 / real n) \<ge> 1 + (real M)/2"
wenzelm@56788:   (is "\<forall>M. ?P M \<ge> _")
wenzelm@56788: proof (rule allI, cases)
wenzelm@56788:   fix M::nat
wenzelm@56788:   assume "M=0"
wenzelm@56788:   then show "?P M \<ge> 1 + (real M)/2" by simp
wenzelm@56788: next
wenzelm@56788:   fix M::nat
wenzelm@56788:   assume "M\<noteq>0"
wenzelm@56788:   then have "M > 0" by simp
wenzelm@56788:   then have
wenzelm@56788:     "(?P M) =
wenzelm@56788:      (1 + (\<Sum>m\<in>{1..M}. \<Sum>n\<in>{(2::nat)^(m - 1)+1..2^m}. 1/real n))"
wenzelm@56788:     by (rule harmonic_aux2)
wenzelm@56788:   also have
wenzelm@56788:     "\<dots> \<ge> (1 + (\<Sum>m\<in>{1..M}. 1/2))"
wenzelm@56788:   proof -
wenzelm@56788:     let ?f = "(\<lambda>x. 1/2)"
wenzelm@56788:     let ?g = "(\<lambda>x. (\<Sum>n\<in>{(2::nat)^(x - 1)+1..2^x}. 1/real n))"
wenzelm@56788:     from harmonic_aux have "\<And>x. x\<in>{1..M} \<Longrightarrow> ?f x \<le> ?g x" by simp
wenzelm@56788:     then have "(\<Sum>m\<in>{1..M}. ?g m) \<ge> (\<Sum>m\<in>{1..M}. ?f m)" by (rule setsum_mono)
wenzelm@56788:     thus ?thesis by simp
wenzelm@56788:   qed
wenzelm@56788:   finally have "(?P M) \<ge> (1 + (\<Sum>m\<in>{1..M}. 1/2))" .
wenzelm@56788:   moreover
wenzelm@56788:   {
wenzelm@56788:     have
wenzelm@56788:       "(\<Sum>m\<in>{1..M}. (1::real)/2) = 1/2 * (\<Sum>m\<in>{1..M}. 1)"
wenzelm@56788:       by auto
wenzelm@56788:     also have
wenzelm@56788:       "\<dots> = 1/2*(real (card {1..M}))"
wenzelm@56788:       by (simp only: real_of_card[symmetric])
wenzelm@56788:     also have
wenzelm@56788:       "\<dots> = 1/2*(real M)" by simp
wenzelm@56788:     also have
wenzelm@56788:       "\<dots> = (real M)/2" by simp
wenzelm@56788:     finally have "(\<Sum>m\<in>{1..M}. (1::real)/2) = (real M)/2" .
wenzelm@56788:   }
wenzelm@56788:   ultimately show "(?P M) \<ge> (1 + (real M)/2)" by simp
wenzelm@56788: qed
wenzelm@56788: 
wenzelm@56788: text {* The final theorem shows that as we take more and more elements
wenzelm@56788: (see @{thm [source] harmonic_aux3}) we get an ever increasing sum. By assuming
wenzelm@56788: the sum converges, the lemma @{thm [source] setsum_less_suminf} ( @{thm
wenzelm@56788: setsum_less_suminf} ) states that each sum is bounded above by the
wenzelm@56788: series' limit. This contradicts our first statement and thus we prove
wenzelm@56788: that the harmonic series is divergent. *}
wenzelm@56788: 
wenzelm@56788: theorem DivergenceOfHarmonicSeries:
wenzelm@56788:   shows "\<not>summable (\<lambda>n. 1/real (Suc n))"
wenzelm@56788:   (is "\<not>summable ?f")
wenzelm@56788: proof -- "by contradiction"
wenzelm@56788:   let ?s = "suminf ?f" -- "let ?s equal the sum of the harmonic series"
wenzelm@56788:   assume sf: "summable ?f"
wenzelm@56788:   then obtain n::nat where ndef: "n = nat \<lceil>2 * ?s\<rceil>" by simp
wenzelm@56788:   then have ngt: "1 + real n/2 > ?s"
wenzelm@56788:   proof -
wenzelm@56788:     have "\<forall>n. 0 \<le> ?f n" by simp
wenzelm@56788:     with sf have "?s \<ge> 0"
wenzelm@56788:       by (rule suminf_nonneg)
wenzelm@56788:     then have cgt0: "\<lceil>2*?s\<rceil> \<ge> 0" by simp
wenzelm@56788: 
wenzelm@56788:     from ndef have "n = nat \<lceil>(2*?s)\<rceil>" .
wenzelm@56788:     then have "real n = real (nat \<lceil>2*?s\<rceil>)" by simp
wenzelm@56788:     with cgt0 have "real n = real \<lceil>2*?s\<rceil>"
wenzelm@56788:       by (auto dest: real_nat_eq_real)
wenzelm@56788:     then have "real n \<ge> 2*(?s)" by simp
wenzelm@56788:     then have "real n/2 \<ge> (?s)" by simp
wenzelm@56788:     then show "1 + real n/2 > (?s)" by simp
wenzelm@56788:   qed
wenzelm@56788: 
wenzelm@56788:   obtain j where jdef: "j = (2::nat)^n" by simp
wenzelm@56788:   have "\<forall>m\<ge>j. 0 < ?f m" by simp
wenzelm@56788:   with sf have "(\<Sum>i<j. ?f i) < ?s" by (rule setsum_less_suminf)
wenzelm@56788:   then have "(\<Sum>i\<in>{Suc 0..<Suc j}. 1/(real i)) < ?s"
wenzelm@56788:     unfolding setsum_shift_bounds_Suc_ivl by (simp add: atLeast0LessThan)
wenzelm@56788:   with jdef have
wenzelm@56788:     "(\<Sum>i\<in>{1..< Suc ((2::nat)^n)}. 1 / (real i)) < ?s" by simp
wenzelm@56788:   then have
wenzelm@56788:     "(\<Sum>i\<in>{1..(2::nat)^n}. 1 / (real i)) < ?s"
wenzelm@56788:     by (simp only: atLeastLessThanSuc_atLeastAtMost)
wenzelm@56788:   moreover from harmonic_aux3 have
wenzelm@56788:     "(\<Sum>i\<in>{1..(2::nat)^n}. 1 / (real i)) \<ge> 1 + real n/2" by simp
wenzelm@56788:   moreover from ngt have "1 + real n/2 > ?s" by simp
wenzelm@56788:   ultimately show False by simp
wenzelm@56788: qed
wenzelm@56788: 
wenzelm@56788: end