| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Isabelle/HOL/ex/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 10 kB |
|
Quelle HarmonicSeries.thy Sprache: Isabelle |
|||||||||
|
(* Title: HOL/ex/HarmonicSeries.thy
Author: Benjamin Porter, 2006 *) section \<open>Divergence of the Harmonic Series\<close> theory HarmonicSeries imports Complex_Main begin subsection \<open>Abstract\<close> text \<open>The following document presents a proof of the Divergence of Harmonic Series theorem formalised in the Isabelle/Isar theorem proving system. {\em Theorem:} The series $\sum_{n=1}^{\infty} \frac{1}{n}$ does not converge 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} \fra \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. \<close> subsection \<open>Formal Proof\<close> lemma two_pow_sub: "0 < m \ by (induct m) auto text \<open>We first prove the following auxillary lemma. This lemma simply 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}$ etc. are all greater than or equal to $\frac{1}{2}$. We do this by observing that each term in the sum is greater than or equal to the last 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}$.\<close> lemma harmonic_aux: "\ (is "\ proof fix m::nat obtain tm where tmdef: "tm = (2::nat)^m" by simp { assume mgt0: "0 < m" have "\ proof - fix x::nat assume xs: "x\ have xgt0: "x>0" proof - from xs have "x \ moreover from mgt0 have "2^(m - 1) + 1 \ ultimately have "x \ thus ?thesis by simp qed moreover from xs have "x \ ultimately have "inverse (real x) \ moreover from xgt0 have "real x \ then have "inverse (real x) = 1 / (real x)" by (rule nonzero_inverse_eq_divide) moreover from mgt0 have "real tm \ then have "inverse (real tm) = 1 / (real tm)" by (rule nonzero_inverse_eq_divide) ultimately show "1/(real x) \ qed then have "(\ by (rule sum_mono) moreover have "(\ proof - have "(\ (1/(real tm))*(\<Sum>n\<in>(?S m). 1)" by simp also have "\ by (simp add: real_of_card) also have "\ by (simp add: tmdef) also from mgt0 have "\ using tmdef two_pow_sub by presburger also have "\ by (simp add: tmdef) also from mgt0 have "\ by auto also have "\ finally show ?thesis . qed ultimately have "(\ by - (erule subst) } thus "0 < m \ qed text \<open>We then show that the sum of a finite number of terms from the harmonic series can be regrouped in increasing powers of 2. For example: $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})$.\<close> lemma harmonic_aux2 [rule_format]: "0 (1 + (\<Sum>m\<in>{1..M}. \<Sum>n\<in>{(2::nat)^(m - 1)+1..2^m}. 1/real n))" (is "0 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 \<comment> \<open>show that LHS = c and RHS = c, and thus LHS = RHS\<close> assume mz: "M=0" { then have "?LHS (Suc M) = ?LHS 1" by simp also have "\ also have "\ by (subst sum.head) (auto simp: atLeastSucAtMost_greaterThanAtMost) also have "\ by (simp add: eval_nat_numeral) also have "\ finally have "?LHS (Suc M) = 1/2 + 1" by simp } moreover { from mz have "?RHS (Suc M) = ?RHS 1" by simp also have "\ by simp also have "\ by (auto simp: atLeastAtMost_singleton') also have "\ 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\ then have mgtz: "M>0" by simp with Suc have suc: "(?LHS M) = (?RHS M)" by blast have "(?LHS (Suc M)) = ((?LHS M) + (\<Sum>n\<in>{(2::nat)^M+1..2^(Suc M)}. 1 / real n))" proof - have "{1..(2::nat)^(Suc M)} = {1..(2::nat)^M}\<union>{(2::nat)^M+1..(2::nat)^(Suc M)}" by auto moreover have "{1..(2::nat)^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 + (\<Sum>m\<in>{1..M}. \<Sum>n\<in>{(2::nat)^(m - 1)+1..2^m}. 1/real n) + (\<Sum>n\<in>{(2::nat)^(Suc M - 1)+1..2^(Suc M)}. 1/real n))" by simp also have "\ by simp also from suc have "\ by simp finally have "(?RHS (Suc M)) = \ } ultimately show "?LHS (Suc M) = ?RHS (Suc M)" by simp qed } thus ?case by simp qed text \<open>Using @{thm [source] harmonic_aux} and @{thm [source] harmonic_aux2} we now show that each group sum is greater than or equal to $\frac{1}{2}$ and thus the finite sum is bounded below by a value proportional to the number of elements we choose.\<close> lemma harmonic_aux3 [rule_format]: shows "\ (is "\ proof (rule allI, cases) fix M::nat assume "M=0" then show "?P M \ next fix M::nat assume "M\ then have "M > 0" by simp then have "(?P M) = (1 + (\<Sum>m\<in>{1..M}. \<Sum>n\<in>{(2::nat)^(m - 1)+1..2^m}. 1/real n))" by (rule harmonic_aux2) also have "\ proof - let ?f = "(\ let ?g = "(\ from harmonic_aux have "\ then have "(\ thus ?thesis by simp qed finally have "(?P M) \ moreover { have "(\ by auto also have "\ by (simp only: real_of_card[symmetric]) also have "\ also have "\ finally have "(\ } ultimately show "(?P M) \ qed text \<open>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 the sum converges, the lemma @{thm [source] sum_less_suminf} ( @{thm sum_less_suminf} ) states that each sum is bounded above by the series' limit. This contradicts our first statement and thus we prove that the harmonic series is divergent.\<close> theorem DivergenceOfHarmonicSeries: shows "\ (is "\ proof \<comment> \<open>by contradiction\<close> let ?s = "suminf ?f" \<comment> \<open>let ?s equal the sum of the harmonic series\<close> assume sf: "summable ?f" then obtain n::nat where ndef: "n = nat \ then have ngt: "1 + real n/2 > ?s" by linarith define j where "j = (2::nat)^n" have "(\ using sf by (simp add: sum_less_suminf) then have "(\ unfolding sum.shift_bounds_Suc_ivl by (simp add: atLeast0LessThan) with j_def have "(\ then have "(\ by (simp only: atLeastLessThanSuc_atLeastAtMost) moreover from harmonic_aux3 have "(\ moreover from ngt have "1 + real n/2 > ?s" by simp ultimately show False by simp qed end ¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28