@MISC{CONVFUN1.MIZ,
  AUTHOR = {Ivanov, Grigory E.},
  TITLE = {Definition of Convex Function and {J}ensen's Inequality},
  ACKNOWLEDGEMENT = {I thank Andrzej Trybulec for teaching me Mizar.},
  SECTION1 = {Product of Two Real Linear Spaces},
  SECTION2 = {Real Linear Space of Real Numbers},
  SECTION3 = {Sum of Finite Sequence of Extended Real Numbers},
  SECTION4 = {Definition of Convex Function},
  SECTION5 = {Relation between notions ``function is convex'' \\
  and ``function is convex on set''},
  SECTION6 = {CONVEX2:6 in other words},
  SECTION7 = {Jensen's Inequality},
  DAY = {17},
  MONTH = {July},
  YEAR = {2003},
  ADDRESS1 = {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.}}

