:: 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 -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;