:: Definition of Convex Function and {J}ensen's Inequality
:: by Grigory E. Ivanov
::
:: Copyright (c) 2003-2021 Association of Mizar Users

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 :Def1: :: CONVFUN1:def 1
for z1, z2 being Element of [: the carrier of X, the carrier of Y:]
for x1, x2 being VECTOR of X
for 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])];
existence
ex b1 being BinOp of [: the carrier of X, the carrier of Y:] st
for z1, z2 being Element of [: the carrier of X, the carrier of Y:]
for x1, x2 being VECTOR of X
for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds
b1 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])]
proof end;
uniqueness
for b1, b2 being BinOp of [: the carrier of X, the carrier of Y:] st ( for z1, z2 being Element of [: the carrier of X, the carrier of Y:]
for x1, x2 being VECTOR of X
for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds
b1 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] ) & ( for z1, z2 being Element of [: the carrier of X, the carrier of Y:]
for x1, x2 being VECTOR of X
for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds
b2 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Add_in_Prod_of_RLS CONVFUN1:def 1 :
for X, Y being non empty RLSStruct
for b3 being BinOp of [: the carrier of X, the carrier of Y:] holds
( b3 = Add_in_Prod_of_RLS (X,Y) iff for z1, z2 being Element of [: the carrier of X, the carrier of Y:]
for x1, x2 being VECTOR of X
for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds
b3 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] );

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 :Def2: :: CONVFUN1:def 2
for a being Real
for z being Element of [: the carrier of X, the carrier of Y:]
for x being VECTOR of X
for 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])];
existence
ex b1 being Function of [:REAL,[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:] st
for a being Real
for z being Element of [: the carrier of X, the carrier of Y:]
for x being VECTOR of X
for y being VECTOR of Y st z = [x,y] holds
b1 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])]
proof end;
uniqueness
for b1, b2 being Function of [:REAL,[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:] st ( for a being Real
for z being Element of [: the carrier of X, the carrier of Y:]
for x being VECTOR of X
for y being VECTOR of Y st z = [x,y] holds
b1 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] ) & ( for a being Real
for z being Element of [: the carrier of X, the carrier of Y:]
for x being VECTOR of X
for y being VECTOR of Y st z = [x,y] holds
b2 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Mult_in_Prod_of_RLS CONVFUN1:def 2 :
for X, Y being non empty RLSStruct
for b3 being Function of [:REAL,[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:] holds
( b3 = Mult_in_Prod_of_RLS (X,Y) iff for a being Real
for z being Element of [: the carrier of X, the carrier of Y:]
for x being VECTOR of X
for y being VECTOR of Y st z = [x,y] holds
b3 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] );

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)) #);
correctness
coherence
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)) #) is RLSStruct
;
;
end;

:: deftheorem defines Prod_of_RLS CONVFUN1:def 3 :
for X, Y being non empty RLSStruct holds Prod_of_RLS (X,Y) = 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)) #);

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

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

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

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

registration
let X, Y be non empty add-associative RLSStruct ;
coherence
proof end;
end;

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

registration
let X, Y be non empty right_complementable RLSStruct ;
coherence
Prod_of_RLS (X,Y) is right_complementable
proof end;
end;

registration
let X, Y be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ;
coherence
( Prod_of_RLS (X,Y) is vector-distributive & Prod_of_RLS (X,Y) is scalar-distributive & Prod_of_RLS (X,Y) is scalar-associative & Prod_of_RLS (X,Y) is scalar-unital )
proof end;
end;

theorem Th3: :: CONVFUN1:3
for X, Y being RealLinearSpace
for n being Nat
for x being FinSequence of the carrier of X
for y being FinSequence of the carrier of Y
for 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)]
proof end;

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

:: deftheorem defines RLS_Real CONVFUN1:def 4 :
RLS_Real = RLSStruct(# REAL,(In (0,REAL)),addreal,multreal #);

registration
coherence
proof end;
end;

Lm1: for X being non empty RLSStruct
for x being VECTOR of X
for u being VECTOR of ()
for p, w being Real st u = [x,w] holds
p * u = [(p * x),(p * w)]

proof end;

Lm2: for X being non empty RLSStruct
for x1, x2 being VECTOR of X
for w1, w2 being Real
for u1, u2 being VECTOR of () st u1 = [x1,w1] & u2 = [x2,w2] holds
u1 + u2 = [(x1 + x2),(w1 + w2)]

proof end;

Lm3: for a being FinSequence of the carrier of RLS_Real
for b being FinSequence of REAL st len a = len b & ( for i being Element of NAT st i in dom a holds
a . i = b . i ) holds
Sum a = Sum b

proof end;

Lm4: for F being FinSequence of ExtREAL
for x being Element of ExtREAL holds Sum (F ^ <*x*>) = (Sum F) + x

proof end;

Lm5: for F being FinSequence of ExtREAL st not -infty in rng F holds
Sum F <> -infty

proof end;

Lm6: for F being FinSequence of ExtREAL st +infty in rng F & not -infty in rng F holds
Sum F = +infty

proof end;

Lm7: for a being FinSequence of ExtREAL
for b being FinSequence of REAL st len a = len b & ( for i being Element of NAT st i in dom a holds
a . i = b . i ) holds
Sum a = Sum b

proof end;

Lm8: for n being Element of NAT
for a being FinSequence of ExtREAL
for b being FinSequence of the carrier of RLS_Real st len a = n & len b = n & ( for i being Element of NAT st i in Seg n holds
a . i = b . i ) holds
Sum a = Sum b

proof end;

Lm9: for F being FinSequence of ExtREAL st rng F c= holds
Sum F = 0.

proof end;

Lm10: for F being FinSequence of REAL st rng F c= holds
Sum F = 0

proof end;

Lm11: for X being RealLinearSpace
for F being FinSequence of the carrier of X st rng F c= {(0. X)} holds
Sum F = 0. X

proof end;

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

:: deftheorem defines epigraph CONVFUN1:def 5 :
for X being non empty RLSStruct
for f being Function of the carrier of X,ExtREAL holds epigraph f = { [x,y] where x is Element of X, y is Element of REAL : f . x <= y } ;

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

:: deftheorem defines convex CONVFUN1:def 6 :
for X being non empty RLSStruct
for f being Function of the carrier of X,ExtREAL holds
( f is convex iff epigraph f is convex );

Lm12: for w1, w2 being R_eal
for wr1, wr2, p1, p2 being Real st w1 = wr1 & w2 = wr2 holds
(p1 * wr1) + (p2 * wr2) = (p1 * w1) + (p2 * w2)

proof end;

theorem Th4: :: CONVFUN1:4
for X being non empty RLSStruct
for 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
for p being Real st 0 < p & p < 1 holds
f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) )
proof end;

theorem :: CONVFUN1:5
for X being RealLinearSpace
for 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
for p being Real st 0 <= p & p <= 1 holds
f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) )
proof end;

theorem :: CONVFUN1:6
for f being PartFunc of REAL,REAL
for g being Function of the carrier of RLS_Real,ExtREAL
for 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 ) )
proof end;

theorem Th7: :: CONVFUN1:7
for X being RealLinearSpace
for M being Subset of X holds
( M is convex iff for n being non zero Nat
for p being FinSequence of REAL
for 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 )
proof end;

Lm13: for X being RealLinearSpace
for f being Function of the carrier of X,ExtREAL
for n being non zero Element of NAT
for p being FinSequence of REAL
for F being FinSequence of ExtREAL
for y being FinSequence of the carrier of X st len F = n & ( for x being VECTOR of X holds f . x <> -infty ) & ( for i being Element of NAT st i in Seg n holds
( p . i >= 0 & F . i = (p . i) * (f . (y /. i)) ) ) holds
not -infty in rng F

proof end;

theorem Th8: :: CONVFUN1:8
for X being RealLinearSpace
for 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
for p being FinSequence of REAL
for F being FinSequence of ExtREAL
for 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 )
proof end;

Lm14: for F being FinSequence of REAL ex s being Permutation of (dom F) ex n being Element of NAT st
for i being Element of NAT st i in dom F holds
( i in Seg n iff F . (s . i) <> 0 )

proof end;

theorem :: CONVFUN1:9
for X being RealLinearSpace
for 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
for p being FinSequence of REAL
for F being FinSequence of ExtREAL
for 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 )
proof end;