REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: http://hdl.handle.net/11320/3712
Pełny rekord metadanych
Pole DCWartośćJęzyk
dc.contributor.authorGrabowski, Adam-
dc.date.accessioned2015-12-09T20:40:51Z-
dc.date.available2015-12-09T20:40:51Z-
dc.date.issued2014-
dc.identifier.citationFormalized Mathematics, Volume 22, Issue 2, 2014, Pages 157-166-
dc.identifier.issn1426-2630-
dc.identifier.issn1898-9934-
dc.identifier.urihttp://hdl.handle.net/11320/3712-
dc.description.abstractThe 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/.-
dc.language.isoen-
dc.publisherDe Gruyter Open-
dc.subjectgeometric mean-
dc.subjectarithmetic mean-
dc.subjectAM-GM inequality-
dc.subjectCauchy mean theorem-
dc.titleCauchy Mean Theorem-
dc.typeArticle-
dc.identifier.doi10.2478/forma-2014-0016-
dc.description.AffiliationInstitute of Informatics University of Białystok Akademicka 2, 15-267 Białystok Poland-
dc.description.referencesGrzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990.-
dc.description.referencesGrzegorz Bancerek. Tarski’s classes and ranks. Formalized Mathematics, 1(3):563–567, 1990.-
dc.description.referencesGrzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.-
dc.description.referencesGrzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990.-
dc.description.referencesGrzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.-
dc.description.referencesGrzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. Formalized Mathematics, 5(4):485–492, 1996.-
dc.description.referencesCzesław Byliński. The complex numbers. Formalized Mathematics, 1(3):507–513, 1990.-
dc.description.referencesCzesław Byliński. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529–536, 1990.-
dc.description.referencesCzesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55–65, 1990.-
dc.description.referencesCzesław Byliński. The sum and product of finite sequences of real numbers. Formalized Mathematics, 1(4):661–668, 1990.-
dc.description.referencesCzesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990.-
dc.description.referencesAgata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990.-
dc.description.referencesFuguo Ge and Xiquan Liang. On the partial product of series and related basic inequalities. Formalized Mathematics, 13(3):413–416, 2005.-
dc.description.referencesAndrzej Kondracki. Basic properties of rational numbers. Formalized Mathematics, 1(5):841–845, 1990.-
dc.description.referencesArtur Korniłowicz. On the real valued functions. Formalized Mathematics, 13(1):181–187, 2005.-
dc.description.referencesJarosław Kotowicz. Functions and finite sequences of real numbers. Formalized Mathematics, 3(2):275–278, 1992.-
dc.description.referencesRafał Kwiatek. Factorial and Newton coefficients. Formalized Mathematics, 1(5):887–890, 1990.-
dc.description.referencesBenjamin 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.-
dc.description.referencesKonrad Raczkowski and Andrzej Nędzusiak. Real exponents and logarithms. Formalized Mathematics, 2(2):213–216, 1991.-
dc.description.referencesAndrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1(2):329–334, 1990.-
dc.description.referencesAndrzej Trybulec. On the sets inhabited by numbers. Formalized Mathematics, 11(4):341–347, 2003.-
dc.description.referencesAndrzej Trybulec and Czesław Byliński. Some properties of real numbers. Formalized Mathematics, 1(3):445–449, 1990.-
dc.description.referencesMichał J. Trybulec. Integers. Formalized Mathematics, 1(3):501–505, 1990.-
dc.description.referencesWojciech A. Trybulec. Non-contiguous substrings and one-to-one finite sequences. Formalized Mathematics, 1(3):569–573, 1990.-
dc.description.referencesZinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.-
dc.description.referencesEdmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990.-
Występuje w kolekcji(ach):Artykuły naukowe (WMiI)
Formalized Mathematics, 2014, Volume 22, Issue 2

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
forma-2014-0016.pdf331,66 kBAdobe PDFOtwórz
Pokaż uproszczony widok rekordu Zobacz statystyki


Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL Creative Commons