Cauchy Mean Theorem

Pole DC	Wartość	Język
dc.contributor.author	Grabowski, Adam	-
dc.date.accessioned	2015-12-09T20:40:51Z	-
dc.date.available	2015-12-09T20:40:51Z	-
dc.date.issued	2014	-
dc.identifier.citation	Formalized Mathematics, Volume 22, Issue 2, 2014, Pages 157-166	-
dc.identifier.issn	1426-2630	-
dc.identifier.issn	1898-9934	-
dc.identifier.uri	http://hdl.handle.net/11320/3712	-
dc.description.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/.	-
dc.language.iso	en	-
dc.publisher	De Gruyter Open	-
dc.subject	geometric mean	-
dc.subject	arithmetic mean	-
dc.subject	AM-GM inequality	-
dc.subject	Cauchy mean theorem	-
dc.title	Cauchy Mean Theorem	-
dc.type	Article	-
dc.identifier.doi	10.2478/forma-2014-0016	-
dc.description.Affiliation	Institute of Informatics University of Białystok Akademicka 2, 15-267 Białystok Poland	-
dc.description.references	Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990.	-
dc.description.references	Grzegorz Bancerek. Tarski’s classes and ranks. Formalized Mathematics, 1(3):563–567, 1990.	-
dc.description.references	Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.	-
dc.description.references	Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990.	-
dc.description.references	Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.	-
dc.description.references	Grzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. Formalized Mathematics, 5(4):485–492, 1996.	-
dc.description.references	Czesław Byliński. The complex numbers. Formalized Mathematics, 1(3):507–513, 1990.	-
dc.description.references	Czesław Byliński. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529–536, 1990.	-
dc.description.references	Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55–65, 1990.	-
dc.description.references	Czesław Byliński. The sum and product of finite sequences of real numbers. Formalized Mathematics, 1(4):661–668, 1990.	-
dc.description.references	Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990.	-
dc.description.references	Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990.	-
dc.description.references	Fuguo Ge and Xiquan Liang. On the partial product of series and related basic inequalities. Formalized Mathematics, 13(3):413–416, 2005.	-
dc.description.references	Andrzej Kondracki. Basic properties of rational numbers. Formalized Mathematics, 1(5):841–845, 1990.	-
dc.description.references	Artur Korniłowicz. On the real valued functions. Formalized Mathematics, 13(1):181–187, 2005.	-
dc.description.references	Jarosław Kotowicz. Functions and finite sequences of real numbers. Formalized Mathematics, 3(2):275–278, 1992.	-
dc.description.references	Rafał Kwiatek. Factorial and Newton coefficients. Formalized Mathematics, 1(5):887–890, 1990.	-
dc.description.references	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.	-
dc.description.references	Konrad Raczkowski and Andrzej Nędzusiak. Real exponents and logarithms. Formalized Mathematics, 2(2):213–216, 1991.	-
dc.description.references	Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1(2):329–334, 1990.	-
dc.description.references	Andrzej Trybulec. On the sets inhabited by numbers. Formalized Mathematics, 11(4):341–347, 2003.	-
dc.description.references	Andrzej Trybulec and Czesław Byliński. Some properties of real numbers. Formalized Mathematics, 1(3):445–449, 1990.	-
dc.description.references	Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501–505, 1990.	-
dc.description.references	Wojciech A. Trybulec. Non-contiguous substrings and one-to-one finite sequences. Formalized Mathematics, 1(3):569–573, 1990.	-
dc.description.references	Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990.	-
dc.description.references	Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990.	-
Występuje w kolekcji(ach):	Artykuły naukowe (WInf) Formalized Mathematics, 2014, Volume 22, Issue 2

Pliki w tej pozycji:

Plik	Opis	Rozmiar	Format
forma-2014-0016.pdf		331,66 kB	Adobe PDF	Otwórz

Pokaż uproszczony widok rekordu Zobacz statystyki

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