Definition of Convex Function and Jensen's Inequality

Grigory E. Ivanov

Moscow Institute for Physics and Technology

Summary.

Convexity of a function in a real linear space is defined as convexity of its epigraph according to ``Convex analysis'' by R. Tyrrell Rockafellar. The epigraph of a function is a subset of the product of the function's domain space and the space of real numbers. Therefore the product of two real linear spaces should be defined. The values of the functions under consideration are extended real numbers. We define the sum of a finite sequence of extended real numbers and get some properties of the sum. The relation between notions ``function is convex'' and ``function is convex on set'' (see RFUNCT\_3:def 13) is established. We obtain another version of the criterion for a set to be convex (see CONVEX2:6 to compare) that may be more suitable in some cases. Finally we prove Jensen's inequality (both strict and not strict) as criteria for functions to be convex.

MML Identifier: CONVFUN1

Contents (PDF format)

1. Product of Two Real Linear Spaces
2. Real Linear Space of Real Numbers
3. Sum of Finite Sequence of Extended Real Numbers
4. Definition of Convex Function
5. Relation between notions ``function is convex'' \\ and ``function is convex on set''
6. CONVEX2:6 in other words
7. Jensen's Inequality

Acknowledgments

Bibliography

[1] Grzegorz Bancerek. Cardinal numbers. Journal of Formalized Mathematics, 1, 1989.

[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.

[3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.

[4] Jozef Bialas. Infimum and supremum of the set of real numbers. Measure theory. Journal of Formalized Mathematics, 2, 1990.

[5] Jozef Bialas. Series of positive real numbers. Measure theory. Journal of Formalized Mathematics, 2, 1990.

[6] Jozef Bialas. Some properties of the intervals. Journal of Formalized Mathematics, 6, 1994.

[7] Czeslaw Bylinski. Binary operations. Journal of Formalized Mathematics, 1, 1989.

[8] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[9] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.

[10] Czeslaw Bylinski. Partial functions. Journal of Formalized Mathematics, 1, 1989.

[11] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.

[12] Czeslaw Bylinski. The sum and product of finite sequences of real numbers. Journal of Formalized Mathematics, 2, 1990.

[13] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.

[14] Noboru Endou, Takashi Mitsuishi, and Yasunari Shidama. Convex sets and convex combinations. Journal of Formalized Mathematics, 14, 2002.

[15] Noboru Endou, Katsumi Wasaki, and Yasunari Shidama. Basic properties of extended real numbers. Journal of Formalized Mathematics, 12, 2000.

[16] Noboru Endou, Katsumi Wasaki, and Yasunari Shidama. Definitions and basic properties of measurable functions. Journal of Formalized Mathematics, 12, 2000.

[17] Krzysztof Hryniewiecki. Basic properties of real numbers. Journal of Formalized Mathematics, 1, 1989.

[18] Jaroslaw Kotowicz. Real sequences and basic operations on them. Journal of Formalized Mathematics, 1, 1989.

[19] Jaroslaw Kotowicz. Functions and finite sequences of real numbers. Journal of Formalized Mathematics, 5, 1993.

[20] Jaroslaw Kotowicz and Yuji Sakai. Properties of partial functions from a domain to the set of real numbers. Journal of Formalized Mathematics, 5, 1993.

[21] Eugeniusz Kusak, Wojciech Leonczuk, and Michal Muzalewski. Abelian groups, fields and vector spaces. Journal of Formalized Mathematics, 1, 1989.

[22] Takaya Nishiyama and Yasuho Mizuhara. Binary arithmetics. Journal of Formalized Mathematics, 5, 1993.

[23] Andrzej Trybulec. Domains and their Cartesian products. Journal of Formalized Mathematics, 1, 1989.

[24] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[25] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

[26] Wojciech A. Trybulec. Vectors in real linear space. Journal of Formalized Mathematics, 1, 1989.

[27] Wojciech A. Trybulec. Pigeon hole principle. Journal of Formalized Mathematics, 2, 1990.

[28] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

[29] Edmund Woronowicz. Relations defined on sets. Journal of Formalized Mathematics, 1, 1989.