Cauchy Mean Theorem

Adam Grabowski

Formalized Mathematics (2014)

  • Volume: 22, Issue: 2, page 157-166
  • ISSN: 1426-2630

Abstract

top
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/.

How to cite

top

Adam Grabowski. "Cauchy Mean Theorem." Formalized Mathematics 22.2 (2014): 157-166. <http://eudml.org/doc/268819>.

@article{AdamGrabowski2014,
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/.},
author = {Adam Grabowski},
journal = {Formalized Mathematics},
keywords = {geometric mean; arithmetic mean; AM-GM inequality; Cauchy mean theorem},
language = {eng},
number = {2},
pages = {157-166},
title = {Cauchy Mean Theorem},
url = {http://eudml.org/doc/268819},
volume = {22},
year = {2014},
}

TY - JOUR
AU - Adam Grabowski
TI - Cauchy Mean Theorem
JO - Formalized Mathematics
PY - 2014
VL - 22
IS - 2
SP - 157
EP - 166
AB - 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/.
LA - eng
KW - geometric mean; arithmetic mean; AM-GM inequality; Cauchy mean theorem
UR - http://eudml.org/doc/268819
ER -

References

top
  1. [1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990. 
  2. [2] Grzegorz Bancerek. Tarski’s classes and ranks. Formalized Mathematics, 1(3):563–567, 1990. 
  3. [3] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990. Zbl06213858
  4. [4] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990. 
  5. [5] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990. 
  6. [6] Grzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. Formalized Mathematics, 5(4):485–492, 1996. 
  7. [7] Czesław Byliński. The complex numbers. Formalized Mathematics, 1(3):507–513, 1990. 
  8. [8] Czesław Byliński. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529–536, 1990. 
  9. [9] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55–65, 1990. 
  10. [10] Czesław Byliński. The sum and product of finite sequences of real numbers. Formalized Mathematics, 1(4):661–668, 1990. 
  11. [11] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990. 
  12. [12] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990. 
  13. [13] Fuguo Ge and Xiquan Liang. On the partial product of series and related basic inequalities. Formalized Mathematics, 13(3):413–416, 2005. 
  14. [14] Andrzej Kondracki. Basic properties of rational numbers. Formalized Mathematics, 1(5):841–845, 1990. 
  15. [15] Artur Korniłowicz. On the real valued functions. Formalized Mathematics, 13(1):181–187, 2005. 
  16. [16] Jarosław Kotowicz. Functions and finite sequences of real numbers. Formalized Mathematics, 3(2):275–278, 1992. 
  17. [17] Rafał Kwiatek. Factorial and Newton coefficients. Formalized Mathematics, 1(5):887–890, 1990. 
  18. [18] Benjamin Porter. Cauchy’s mean theorem and the Cauchy-Schwarz inequality. Archive of Formal Proofs, March 2006. ISSN 2150-914x. http://afp.sf.net/entries/Cauchy. shtml, Formal proof development. 
  19. [19] Konrad Raczkowski and Andrzej Nędzusiak. Real exponents and logarithms. Formalized Mathematics, 2(2):213–216, 1991. 
  20. [20] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1(2):329–334, 1990. 
  21. [21] Andrzej Trybulec. On the sets inhabited by numbers. Formalized Mathematics, 11(4):341–347, 2003. 
  22. [22] Andrzej Trybulec and Czesław Byliński. Some properties of real numbers. Formalized Mathematics, 1(3):445–449, 1990. 
  23. [23] Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501–505, 1990. 
  24. [24] Wojciech A. Trybulec. Non-contiguous substrings and one-to-one finite sequences. Formalized Mathematics, 1(3):569–573, 1990. 
  25. [25] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990. 
  26. [26] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.