:: by Grigory E. Ivanov

::

:: Received July 17, 2003

:: Copyright (c) 2003-2016 Association of Mizar Users

definition

let X, Y be non empty RLSStruct ;

ex b_{1} 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_{1} . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])]

for b_{1}, b_{2} 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_{1} . (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_{2} . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] ) holds

b_{1} = b_{2}

end;
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 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])];

ex b

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

proof end;

uniqueness for b

for x1, x2 being VECTOR of X

for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds

b

for x1, x2 being VECTOR of X

for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds

b

b

proof end;

:: deftheorem Def1 defines Add_in_Prod_of_RLS CONVFUN1:def 1 :

for X, Y being non empty RLSStruct

for b_{3} being BinOp of [: the carrier of X, the carrier of Y:] holds

( b_{3} = 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_{3} . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] );

for X, Y being non empty RLSStruct

for b

( b

for x1, x2 being VECTOR of X

for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds

b

definition

let X, Y be non empty RLSStruct ;

ex b_{1} 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_{1} . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])]

for b_{1}, b_{2} 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_{1} . (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_{2} . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] ) holds

b_{1} = b_{2}

end;
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 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])];

ex b

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

proof end;

uniqueness for b

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

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

b

proof end;

:: deftheorem Def2 defines Mult_in_Prod_of_RLS CONVFUN1:def 2 :

for X, Y being non empty RLSStruct

for b_{3} being Function of [:REAL,[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:] holds

( b_{3} = 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_{3} . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] );

for X, Y being non empty RLSStruct

for b

( b

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

definition

let X, Y be non empty RLSStruct ;

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;
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 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)) #);

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 ;

;

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

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)) #);

theorem :: CONVFUN1:1

registration
end;

registration

let X, Y be non empty add-associative RLSStruct ;

coherence

Prod_of_RLS (X,Y) is add-associative

end;
coherence

Prod_of_RLS (X,Y) is add-associative

proof end;

registration

let X, Y be non empty right_zeroed RLSStruct ;

coherence

Prod_of_RLS (X,Y) is right_zeroed

end;
coherence

Prod_of_RLS (X,Y) is right_zeroed

proof end;

registration

let X, Y be non empty right_complementable RLSStruct ;

coherence

Prod_of_RLS (X,Y) is right_complementable

end;
coherence

Prod_of_RLS (X,Y) is right_complementable

proof end;

registration

let X, Y be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ;

( 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 )

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

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)]

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

coherence

RLSStruct(# REAL,(In (0,REAL)),addreal,multreal #) is non empty RLSStruct ;

;

end;

func RLS_Real -> non empty RLSStruct equals :: CONVFUN1:def 4

RLSStruct(# REAL,(In (0,REAL)),addreal,multreal #);

correctness RLSStruct(# REAL,(In (0,REAL)),addreal,multreal #);

coherence

RLSStruct(# REAL,(In (0,REAL)),addreal,multreal #) is non empty RLSStruct ;

;

:: deftheorem defines RLS_Real CONVFUN1:def 4 :

RLS_Real = RLSStruct(# REAL,(In (0,REAL)),addreal,multreal #);

RLS_Real = RLSStruct(# REAL,(In (0,REAL)),addreal,multreal #);

registration

( 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 )
end;

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;

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;

{ [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))

end;
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 } ;

{ [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;

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

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

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

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

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

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

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 )

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 )

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 )

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;