*To*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] 4 new AFP entries*From*: Gerwin Klein <Gerwin.Klein at nicta.com.au>*Date*: Tue, 5 Jan 2016 23:12:24 +0000*Accept-language*: en-AU, en-US*Thread-index*: AQHRSA6JVnOFuC1lqUCHdqHY9SzhYQ==*Thread-topic*: 4 new AFP entries

We have 4 new AFP entries online at [http://afp.sfp.net], all by Manuel Eberl: 1. The Divergence of the Prime Harmonic Series Abstract: In this work, we prove the lower bound ln (H_n) - ln(5/3) for the partial sum of the Prime Harmonic series and, based on this, the divergence of the Prime Harmonic Series â [p prime] Â 1/p. The proof relies on the unique squarefree decomposition of natural numbers. This is similar to Euler's original proof (which was highly informal and morally questionable). Its advantage over proofs by contradiction, like the famous one by Paul ErdÅs, is that it provides a relatively good lower bound for the partial sums. 2. Descartes' Rule of Signs Abstract: Descartes' Rule of Signs relates the number of positive real roots of a polynomial with the number of sign changes in its coefficient sequence. Our proof follows the simple inductive proof given by Rob Arthan, which was also used by John Harrison in his HOL Light formalisation. We proved most of the lemmas for arbitrary linearly-ordered integrity domains (e.g. integers, rationals, reals); the main result, however, requires the intermediate value theorem and was therefore only proven for real polynomials. 3. Basic Geometric Properties of Triangles Abstract: This entry contains a definition of angles between vectors and between three points. Building on this, we prove basic geometric properties of triangles, such as the Isosceles Triangle Theorem, the Law of Sines and the Law of Cosines, that the sum of the angles of a triangle is Ï, and the congruence theorems for triangles. The definitions and proofs were developed following those by John Harrison in HOL Light. However, due to Isabelle's type class system, all definitions and theorems in the Isabelle formalisation hold for all real inner product spaces. 4. Liouville numbers Abstract: Liouville numbers are a class of transcendental numbers that can be approximated particularly well with rational numbers. Historically, they were the first numbers whose transcendence was proven. In this entry, we define the concept of Liouville numbers as well as the standard construction to obtain Liouville numbers (including Liouville's constant) and we prove their most important properties: irrationality and transcendence. The proof is very elementary and requires only standard arithmetic, the Mean Value Theorem for polynomials, and the boundedness of polynomials on compact intervals. Enjoy! Gerwin ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

- Previous by Date: Re: [isabelle] Isabelle2016-RC0 - does not exit on Linux
- Next by Date: [isabelle] Isabelle2016-RC0: Windows bootstrapping
- Previous by Thread: Re: [isabelle] Deep embedding of natural deduction?
- Next by Thread: [isabelle] Isabelle2016-RC0: Windows bootstrapping
- Cl-isabelle-users January 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list