<abstract xmlns="http://www.w3.org/1999/xhtml">The purpose of this paper was to prove formally, using the Mizar language, Arithmetic Mean/Geometric Mean theorem known maybe better under the name of AM-GM inequality or Cauchy mean theorem. It states that the arithmetic mean of a list of a non-negative real numbers is greater than or equal to the geometric mean of the same list.The formalization was tempting for at least two reasons: one of them, perhaps the strongest, was that the proof of this theorem seemed to be relatively easy to formalize (e.g. the weaker variant of this was proven in [13]). Also Jensen’s inequality is already present in the Mizar Mathematical Library. We were impressed by the beauty and elegance of the simple proof by induction and so we decided to follow this specific way.The proof follows similar lines as that written in Isabelle [18]; the comparison of both could be really interesting as it seems that in both systems the number of lines needed to prove this are really close.This theorem is item #38 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/.</abstract>

The purpose of this paper was to prove formally, using the Mizar language, Arithmetic Mean/Geometric Mean theorem known maybe better under the name of AM-GM inequality or Cauchy mean theorem. It states that the arithmetic mean of a list of a non-negative real numbers is greater than or equal to the geometric mean of the same list.The formalization was tempting for at least two reasons: one of them, perhaps the strongest, was that the proof of this theorem seemed to be relatively easy to formalize (e.g. the weaker variant of this was proven in [13]). Also Jensen’s inequality is already present in the Mizar Mathematical Library. We were impressed by the beauty and elegance of the simple proof by induction and so we decided to follow this specific way.The proof follows similar lines as that written in Isabelle [18]; the comparison of both could be really interesting as it seems that in both systems the number of lines needed to prove this are really close.This theorem is item #38 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/.

Cauchy Mean Theorem

Institute of Informatics University of Białystok Akademicka 2, 15-267 Białystok Poland

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License. (CC BY-SA 3.0)

{"article-title":"Cauchy Mean Theorem"}

The purpose of this paper was to prove formally, using the Mizar language, Arithmetic Mean/Geometric Mean theorem known maybe better under the name of AM-GM...

Cauchy Mean Theorem

Data publikacji: 30 cze 2014

Zakres stron: 157 - 166

Otrzymano: 13 cze 2014

DOI: https://doi.org/10.2478/forma-2014-0016

Słowa kluczowe
geometric mean, arithmetic mean, AM-GM inequality, Cauchy mean theorem

© 2014 Adam Grabowski

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License. (CC BY-SA 3.0)

Cauchy Mean Theorem

Data publikacji: 30 cze 2014

Zakres stron: 157 - 166

Otrzymano: 13 cze 2014

DOI: https://doi.org/10.2478/forma-2014-0016

Słowa kluczowegeometric mean, arithmetic mean, AM-GM inequality, Cauchy mean theorem

© 2014 Adam Grabowski

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 License. (CC BY-SA 3.0)

Słowa kluczowe
geometric mean, arithmetic mean, AM-GM inequality, Cauchy mean theorem