@MISC{RVSUM_3.MIZ,
  AUTHOR = {Grabowski, Adam},
  TITLE = {Cauchy Mean Theorem},
  SECTION1 = {Preliminaries},
  SECTION2 = {Arithmetic Mean and Geometric Mean},
  SECTION3 = {Heterogeneity of a Finite Sequence},
  SECTION4 = {Auxiliary Replacement Function},
  SECTION5 = {Homogenization of a Finite Sequence},
  SECTION6 = {Cauchy Mean Theorem},
  DAY = {13},
  MONTH = {June},
  YEAR = {2014},
  ADDRESS1 = {Institute of Computer Science\\University of Bia{\l}ystok\\Akademicka 2, 15-267 Bia{\l}ystok\\Poland},
  SUMMARY = {The main aim of the article was to prove formally
  another item from Freek Wiedijk's ``Top 100 mathematical theorems"
  \cite{Freek-100-theorems}.
  We concentrate on \#38, called ``Arithmetic Mean/Geometric Mean" --
  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.
  \par
  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 \cite{SERIES_3.ABS}). 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.
  \par
  The proof follows similar lines as that written in Isabelle
  \cite{Cauchy-AFP}; 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.}}

@article{Cauchy-AFP,
  author  = {Benjamin Porter},
  title   = {Cauchy's Mean Theorem and the Cauchy-Schwarz Inequality},
  journal = {Archive of Formal Proofs},
  month   = mar,
  year    = 2006,
  note    = {\url{http://afp.sf.net/entries/Cauchy.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}


