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

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 b₁ 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
b₁ . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])]

proof end;

uniqueness
for b₁, b₂ 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
b₁ . (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
b₂ . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines Add_in_Prod_of_RLS CONVFUN1:def 1 :
for X, Y being non empty RLSStruct
for b₃ being BinOp of [: the carrier of X, the carrier of Y:] holds
( b₃ = 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
b₃ . (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 b₁ 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
b₁ . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])]

proof end;

uniqueness
for b₁, b₂ 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
b₁ . (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
b₂ . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines Mult_in_Prod_of_RLS CONVFUN1:def 2 :
for X, Y being non empty RLSStruct
for b₃ being Function of [:REAL,[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:] holds
( b₃ = 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
b₃ . (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 ;

cluster Prod_of_RLS (X,Y) -> add-associative ;

coherence
Prod_of_RLS (X,Y) is add-associative

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 ;

cluster Prod_of_RLS (X,Y) -> right_complementable ;

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 ;

cluster Prod_of_RLS (X,Y) -> vector-distributive scalar-distributive scalar-associative scalar-unital ;

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
RLSStruct(# REAL,(In (0,REAL)),addreal,multreal #);

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

cluster RLS_Real -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence
( RLS_Real is Abelian & RLS_Real is add-associative & RLS_Real is right_zeroed & RLS_Real is right_complementable & RLS_Real is vector-distributive & RLS_Real is scalar-distributive & RLS_Real is scalar-associative & RLS_Real is scalar-unital )

proof end;

end;

Lm1: for X being non empty RLSStruct
for x being VECTOR of X
for u being VECTOR of (Prod_of_RLS (X,RLS_Real))
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 (Prod_of_RLS (X,RLS_Real)) 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= {0.} holds
Sum F = 0.

proof end;

Lm10: for F being FinSequence of REAL st rng F c= {0} 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 (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 } ;

coherence
{ [x,y] where x is Element of X, y is Element of REAL : f . x <= y } is Subset of (Prod_of_RLS (X,RLS_Real))

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;