:: Definition of Convex Function and {J}ensen's Inequality
::  by Grigory E. Ivanov
::
:: Received July 17, 2003
:: Copyright (c) 2003-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, XBOOLE_0, RLVECT_1, BINOP_1, ZFMISC_1, STRUCT_0,
      SUBSET_1, FUNCT_1, ALGSTR_0, REAL_1, SUPINF_2, RELAT_1, ARYTM_3,
      FINSEQ_1, CARD_3, CARD_1, XXREAL_0, TARSKI, PARTFUN1, ORDINAL4, BINOP_2,
      ARYTM_1, SUPINF_1, NAT_1, FUNCT_2, RFINSEQ, CONVEX1, RFUNCT_3, FINSET_1,
      CLASSES1, CONVFUN1, FUNCT_7, XCMPLX_0;
 notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XXREAL_0,
      XXREAL_3, XCMPLX_0, XREAL_0, REAL_1, FUNCT_1, RELSET_1, PARTFUN1,
      SUPINF_1, ZFMISC_1, MEASURE6, BINOP_1, FUNCT_2, SUPINF_2, DOMAIN_1,
      BINOP_2, FINSET_1, CLASSES1, RFINSEQ, RFUNCT_3, NAT_1, RVSUM_1, EXTREAL1,
      FINSEQ_1, FINSEQ_4, STRUCT_0, ALGSTR_0, RLVECT_1, CONVEX1;
 constructors BINOP_1, DOMAIN_1, REAL_1, FINSEQ_4, FINSOP_1, RVSUM_1, SUPINF_2,
      RFINSEQ, RFUNCT_3, MEASURE6, EXTREAL1, CONVEX1, BINOP_2, SUPINF_1,
      CLASSES1, RELSET_1;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS,
      XXREAL_0, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, STRUCT_0, RLVECT_1,
      VALUED_0, ALGSTR_0, CARD_1, XXREAL_3, INT_1, ORDINAL1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Product of Two Real Linear Spaces

definition
  let X,Y be non empty RLSStruct;
  func Add_in_Prod_of_RLS(X,Y) -> BinOp of [:the carrier of X, the carrier of
  Y:] means
:: CONVFUN1:def 1

  for z1, z2 being Element of [:the carrier of X, the carrier of
Y:], x1, x2 being VECTOR of X, y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 =
  [x2,y2] holds it.(z1,z2) = [(the addF of X).[x1,x2],(the addF of Y).[y1,y2]];
end;

definition
  let X,Y be non empty RLSStruct;
  func Mult_in_Prod_of_RLS(X,Y) -> Function of [:REAL, [:the carrier of X, the
  carrier of Y:]:], [:the carrier of X, the carrier of Y:] means
:: CONVFUN1:def 2

  for a being Real,
      z being Element of [:the carrier of X, the carrier of Y:], x being
VECTOR of X, y being VECTOR of Y st z = [x,y] holds it.(a,z) = [(the Mult of X)
  .[a,x],(the Mult of Y).[a,y]];
end;

definition
  let X,Y be non empty RLSStruct;
  func Prod_of_RLS(X,Y) -> RLSStruct equals
:: CONVFUN1:def 3
  RLSStruct(# [:the carrier of X,
the carrier of Y:], [0.X,0.Y], Add_in_Prod_of_RLS(X,Y), Mult_in_Prod_of_RLS(X,Y
    ) #);
end;

registration
  let X,Y be non empty RLSStruct;
  cluster Prod_of_RLS(X,Y) -> non empty;
end;

theorem :: CONVFUN1:1
  for X,Y being non empty RLSStruct, x being VECTOR of X, y being VECTOR
of Y, u being VECTOR of Prod_of_RLS(X,Y), p being Real st u = [x,y] holds p*u =
  [p*x,p*y];

theorem :: CONVFUN1:2
  for X,Y being non empty RLSStruct, x1, x2 being VECTOR of X, y1,
y2 being VECTOR of Y, u1, u2 being VECTOR of Prod_of_RLS(X,Y) st u1 = [x1,y1] &
  u2 = [x2,y2] holds u1+u2 = [x1+x2,y1+y2];

registration
  let X,Y be Abelian non empty RLSStruct;
  cluster Prod_of_RLS(X,Y) -> Abelian;
end;

registration
  let X,Y be add-associative non empty RLSStruct;
  cluster Prod_of_RLS(X,Y) -> add-associative;
end;

registration
  let X,Y be right_zeroed non empty RLSStruct;
  cluster Prod_of_RLS(X,Y) -> right_zeroed;
end;

registration
  let X,Y be right_complementable non empty RLSStruct;
  cluster Prod_of_RLS(X,Y) -> right_complementable;
end;

registration
  let X,Y be vector-distributive scalar-distributive scalar-associative
  scalar-unital
  non empty RLSStruct;
  cluster Prod_of_RLS(X,Y) -> vector-distributive scalar-distributive
  scalar-associative scalar-unital;
end;

theorem :: CONVFUN1:3
  for X,Y being RealLinearSpace, n being Nat, x being
  FinSequence of the carrier of X, y being FinSequence of the carrier of Y, z
being FinSequence of the carrier of Prod_of_RLS(X,Y) st len x = n & len y = n &
  len z = n & (for i being Nat st i in Seg n holds z.i = [x.i,y.i])
  holds Sum z = [Sum x, Sum y];

begin :: Real Linear Space of Real Numbers

definition
  func RLS_Real -> non empty RLSStruct equals
:: CONVFUN1:def 4
  RLSStruct(# REAL,In(0,REAL),addreal,multreal #);
end;

registration
  cluster RLS_Real -> Abelian add-associative right_zeroed
    right_complementable vector-distributive
    scalar-distributive scalar-associative scalar-unital;
end;

begin

begin :: Definition of Convex Function

definition
  let X be non empty RLSStruct, f be Function of the carrier of X,ExtREAL;
  func epigraph f -> Subset of Prod_of_RLS(X,RLS_Real) equals
:: CONVFUN1:def 5
  {[x,y] where x is Element of X, y is Element of REAL: f.x <= (y)};
end;

definition
  let X be non empty RLSStruct, f be Function of the carrier of X,ExtREAL;
  attr f is convex means
:: CONVFUN1:def 6

  epigraph f is convex;
end;

theorem :: CONVFUN1:4
  for X being non empty RLSStruct, f being Function of the carrier
of X,ExtREAL st (for x being VECTOR of X holds f.x <> -infty) holds f is convex
iff for x1, x2 being VECTOR of X,
   p being Real st 0<p & p<1 holds f.(p*x1+(1-p)
  *x2) <= (p)*f.x1+(1-p)*f.x2;

theorem :: CONVFUN1:5
  for X being RealLinearSpace, f being Function of the carrier of X,
ExtREAL st (for x being VECTOR of X holds f.x <> -infty) holds f is convex iff
for x1, x2 being VECTOR of X,
   p being Real st 0<=p & p<=1 holds f.(p*x1+(1-p)*
  x2) <= (p)*f.x1+(1-p)*f.x2;

begin :: Relation between notions "function is convex" and "function is convex on set"

theorem :: CONVFUN1:6
  for f being PartFunc of REAL,REAL, g being Function of the carrier of
  RLS_Real,ExtREAL, X being Subset of RLS_Real st X c= dom f & for x being Real
  holds (x in X implies g.x=f.x) & (not x in X implies g.x=+infty) holds g is
  convex iff f is_convex_on X & X is convex;

begin :: CONVEX2:6 in other words

theorem :: CONVFUN1:7
  for X being RealLinearSpace, M being Subset of X holds M is
  convex iff for n being non zero Nat, p being FinSequence of REAL, y,z being
FinSequence of the carrier of X st len p = n & len y = n & len z = n & Sum p =
  1 & (for i being Nat st i in Seg n holds p.i>0 & z.i=p.i*y/.i & y/.i in M)
  holds Sum(z) in M;

begin

theorem :: CONVFUN1:8
  for X being RealLinearSpace, f being Function of the carrier of
  X,ExtREAL st (for x being VECTOR of X holds f.x <> -infty) holds f is convex
iff for n being non zero Element of NAT, p being FinSequence of REAL, F being
FinSequence of ExtREAL, y,z being FinSequence of the carrier of X st len p = n
  & len F = n & len y = n & len z = n & Sum p = 1 & (for i being Element of NAT
st i in Seg n holds p.i>0 & z.i=p.i*y/.i & F.i = (p.i)*f.(y/.i)) holds f.
  Sum(z) <= Sum F;

theorem :: CONVFUN1:9
  for X being RealLinearSpace, f being Function of the carrier of X,
ExtREAL st (for x being VECTOR of X holds f.x <> -infty) holds f is convex iff
  for n being non zero Element of NAT, p being FinSequence of REAL, F being
FinSequence of ExtREAL, y,z being FinSequence of the carrier of X st len p = n
  & len F = n & len y = n & len z = n & Sum p = 1 & (for i being Element of NAT
st i in Seg n holds p.i>=0 & z.i=p.i*y/.i & F.i = (p.i)*f.(y/.i)) holds f.
  Sum(z) <= Sum F;