# HG changeset patch # User kleing # Date 1140351692 -3600 # Node ID 6e6b5b1fdc06a9bb4a5af4958f4bcc63232688e0 # Parent 3aabd46340e03f2cef73af398f64da83289789cd * added Library/ASeries (sum of arithmetic series with instantiation to nat and int) * added Complex/ex/ASeries_Complex (instantiation of the above for reals) * added Complex/ex/HarmonicSeries (should really be in something like Complex/Library) (these are contributions by Benjamin Porter, numbers 68 and 34 of http://www.cs.ru.nl/~freek/100/) diff -r 3aabd46340e0 -r 6e6b5b1fdc06 src/HOL/Complex/ex/ASeries_Complex.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Complex/ex/ASeries_Complex.thy Sun Feb 19 13:21:32 2006 +0100 @@ -0,0 +1,24 @@ +(* Title: HOL/Library/ASeries.thy + ID: $Id$ + Author: Benjamin Porter, 2006 +*) + + +header {* Arithmetic Series for Reals *} + +theory ASeries_Complex +imports Complex_Main ASeries +begin + +lemma arith_series_real: + "(2::real) * (\i\{..i\{.. 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. +*} + +section {* 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 +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}$. *} + +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 with 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 setsum_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 real_of_nat_def) + 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)))" + by (auto simp: tmdef dest: two_pow_sub) + also have + "\ = (real (2::nat))^(m - 1) / (real (2::nat))^m" + by (simp add: tmdef realpow_real_of_nat [symmetric]) + 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 +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})$. *} + +lemma harmonic_aux2 [rule_format]: + "0 (\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 ?LHS M = ?RHS M") +proof (induct M) + case 0 show ?case by simp +next + case (Suc M) + have ant: "0 < Suc M" . + { + 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 setsum_head) + (auto simp: atLeastSucAtMost_greaterThanAtMost) + also have + "\ = ((\n\{2..2::nat}. 1/real n) + 1/(real (1::nat)))" + by (simp add: nat_number) + 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" + proof - + have "(2::nat)^0 = 1" by simp + then have "(2::nat)^0+1 = 2" by simp + moreover have "(2::nat)^1 = 2" by simp + ultimately have "{((2::nat)^0)+1..2^1} = {2::nat..2}" by auto + thus ?thesis by simp + qed + 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: setsum_Un_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 +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. *} + +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 setsum_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 +the sum converges, the lemma @{thm [source] series_pos_less} ( @{thm +series_pos_less} ) 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. *} + +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" + proof - + have "\n. 0 \ ?f n" by simp + with sf have "?s \ 0" + by - (rule suminf_0_le, simp_all) + then have cgt0: "\2*?s\ \ 0" by simp + + from ndef have "n = nat \(2*?s)\" . + then have "real n = real (nat \2*?s\)" by simp + with cgt0 have "real n = real \2*?s\" + by (auto dest: real_nat_eq_real) + then have "real n \ 2*(?s)" by simp + then have "real n/2 \ (?s)" by simp + then show "1 + real n/2 > (?s)" by simp + qed + + obtain j where jdef: "j = (2::nat)^n" by simp + have "\m\j. 0 < ?f m" by simp + with sf have "(\i\{0..i\{1..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 \ No newline at end of file diff -r 3aabd46340e0 -r 6e6b5b1fdc06 src/HOL/Complex/ex/ROOT.ML --- a/src/HOL/Complex/ex/ROOT.ML Sun Feb 19 02:11:27 2006 +0100 +++ b/src/HOL/Complex/ex/ROOT.ML Sun Feb 19 13:21:32 2006 +0100 @@ -14,3 +14,6 @@ no_document use_thy "BigO"; use_thy "BigO_Complex"; + +use_thy "ASeries_Complex"; +use_thy "HarmonicSeries"; diff -r 3aabd46340e0 -r 6e6b5b1fdc06 src/HOL/Hyperreal/Series.thy --- a/src/HOL/Hyperreal/Series.thy Sun Feb 19 02:11:27 2006 +0100 +++ b/src/HOL/Hyperreal/Series.thy Sun Feb 19 13:21:32 2006 +0100 @@ -280,7 +280,6 @@ apply simp done - lemma sumr_pos_lt_pair: "[|summable f; \d. 0 < (f(n + (Suc(Suc 0) * d))) + f(n + ((Suc(Suc 0) * d) + 1))|] @@ -409,6 +408,21 @@ apply (simp add: abs_le_interval_iff) done +(* specialisation for the common 0 case *) +lemma suminf_0_le: + fixes f::"nat\real" + assumes gt0: "\n. 0 \ f n" and sm: "summable f" + shows "0 \ suminf f" +proof - + let ?g = "(\n. (0::real))" + from gt0 have "\n. ?g n \ f n" by simp + moreover have "summable ?g" by (rule summable_zero) + moreover from sm have "summable f" . + ultimately have "suminf ?g \ suminf f" by (rule summable_le) + then show "0 \ suminf f" by (simp add: suminf_zero) +qed + + text{*Absolute convergence imples normal convergence*} lemma summable_rabs_cancel: "summable (%n. abs (f n)) ==> summable f" apply (auto simp add: summable_Cauchy) diff -r 3aabd46340e0 -r 6e6b5b1fdc06 src/HOL/Library/ASeries.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/ASeries.thy Sun Feb 19 13:21:32 2006 +0100 @@ -0,0 +1,114 @@ +(* Title: HOL/Library/ASeries.thy + ID: $Id$ + Author: Benjamin Porter, 2006 +*) + + +header {* Arithmetic Series *} + +theory ASeries +imports Main +begin + +section {* Abstract *} + +text {* The following document presents a proof of the Arithmetic +Series Sum formalised in Isabelle/Isar. + +{\em Theorem:} The series $\sum_{i=1}^{n} a_i$ where $a_{i+1} = a_i + +d$ for some constant $d$ has the sum $\frac{n}{2} (a_1 + a_n)$ +(i.e. $n$ multiplied by the arithmetic mean of the first and last +element). + +{\em Informal Proof:} (from +"http://mathworld.wolfram.com/ArithmeticSeries.html") + The proof is a simple forward proof. Let $S$ equal the sum above and + $a$ the first element, then we have +\begin{align} +\nonumber S &= a + (a+d) + (a+2d) + ... a_n \\ +\nonumber &= n*a + d (0 + 1 + 2 + ... n-1) \\ +\nonumber &= n*a + d (\frac{1}{2} * (n-1) * n) \mbox{..using a simple sum identity} \\ +\nonumber &= \frac{n}{2} (2a + d(n-1)) \\ +\nonumber & \mbox{..but $(a+a_n = a + (a + d(n-1)) = 2a + d(n-1))$ so} \\ +\nonumber S &= \frac{n}{2} (a + a_n) +\end{align} +*} + +section {* Formal Proof *} + +text {* We present a proof for the abstract case of a commutative ring, +we then instantiate for three common types nats, ints and reals. The +function @{text "of_nat"} maps the natural numbers into any +commutative ring. +*} + +lemmas comm_simp [simp] = left_distrib right_distrib add_assoc mult_ac + +text {* Next we prove the following simple summation law $\sum_{i=1}^n +i = \frac {n * (n+1)}{2}$. *} + +lemma sum_ident: + "((1::'a::comm_semiring_1_cancel) + 1)*(\i\{1..n}. of_nat i) = + of_nat n*((of_nat n)+1)" +proof (induct n) + case 0 + show ?case by simp +next + case (Suc n) + then show ?case by simp +qed + +text {* The abstract theorem follows. Note that $2$ is displayed as +$1+1$ to keep the structure as abstract as possible. *} + +theorem arith_series_general: + "((1::'a::comm_semiring_1_cancel) + 1) * (\i\{.. 1" + let ?I = "\i. of_nat i" and ?n = "of_nat n" + have + "(\i\{..i\{..i\{.. = ?n*a + (\i\{.. = (?n*a + d*(\i\{1.. = (1+1)*?n*a + d*(1+1)*(\i\{1..i\{1..n - 1}. ?I i) = ((1+1)*?n*a + d*?I (n - 1)*?I n)" + by (simp only: mult_ac sum_ident [of "n - 1"]) (simp add: of_nat_Suc [symmetric]) + finally show ?thesis by simp +next + assume "\(n > 1)" + hence "n = 1 \ n = 0" by auto + thus ?thesis by auto +qed + +subsection {* Instantiation *} + +lemma arith_series_nat: + "(2::nat) * (\i\{..i\{..i\{..i\{..*) diff -r 3aabd46340e0 -r 6e6b5b1fdc06 src/HOL/SetInterval.thy --- a/src/HOL/SetInterval.thy Sun Feb 19 02:11:27 2006 +0100 +++ b/src/HOL/SetInterval.thy Sun Feb 19 13:21:32 2006 +0100 @@ -715,24 +715,39 @@ "setsum f {Suc m..x\{m..n}. P x) = P m + (\x\{m<..n}. P x)" (is "?lhs = ?rhs") +proof - + from mn + have "{m..n} = {m} \ {m<..n}" + by (auto intro: ivl_disj_un_singleton) + hence "?lhs = (\x\{m} \ {m<..n}. P x)" + by (simp add: atLeast0LessThan) + also have "\ = ?rhs" by simp + finally show ?thesis . +qed + +lemma setsum_head_upt: fixes m::nat assumes m: "0 < m" - shows "P 0 + (\x\{1..xxx\{1.. {0<..xx\{0.. = (\x\{0..m - 1}. P x)" + by (cases m) (auto simp add: atLeastLessThanSuc_atLeastAtMost) + also + have "\ = P 0 + (\x\{0<..m - 1}. P x)" + by (simp add: setsum_head) + also + from m + have "{0<..m - 1} = {1.. = (\xx