:: CONVFUN1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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 add of X . [x1,x2]),(the add 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 add of X . [x1,x2]),(the add 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 add of X . [x1,x2]),(the add 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 add of X . [x1,x2]),(the add 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 add of X . [x1,x2]),(the add 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 Th1: :: CONVFUN1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)]
proof end;

theorem Th2: :: CONVFUN1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)]
proof end;

Lm1: for X, Y being non empty RLSStruct holds 0. (Prod_of_RLS X,Y) = [(0. X),(0. Y)]
by RLVECT_1:def 2;

registration
let X, Y be non empty Abelian RLSStruct ;
cluster Prod_of_RLS X,Y -> non empty 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 -> non empty 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 -> non empty 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 -> non empty right_complementable ;
coherence
Prod_of_RLS X,Y is right_complementable
proof end;
end;

registration
let X, Y be non empty RealLinearSpace-like RLSStruct ;
cluster Prod_of_RLS X,Y -> non empty RealLinearSpace-like ;
coherence
Prod_of_RLS X,Y is RealLinearSpace-like
proof end;
end;

theorem Th3: :: CONVFUN1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ,0,addreal ,multreal #);
correctness
coherence
RLSStruct(# REAL ,0,addreal ,multreal #) is non empty RLSStruct ;
;
end;

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

Lm2: for v being VECTOR of RLS_Real
for x, p being Real st v = x holds
p * v = p * x
proof end;

Lm3: for v1, v2 being VECTOR of RLS_Real
for x1, x2 being Real st v1 = x1 & v2 = x2 holds
v1 + v2 = x1 + x2
proof end;

registration
cluster RLS_Real -> non empty Abelian add-associative right_zeroed right_complementable RealLinearSpace-like ;
coherence
( RLS_Real is Abelian & RLS_Real is add-associative & RLS_Real is right_zeroed & RLS_Real is right_complementable & RLS_Real is RealLinearSpace-like )
proof end;
end;

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

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

Lm6: for a being FinSequence of the carrier of RLS_Real
for b being FinSequence of REAL st len a = len b & ( for i being Nat st i in dom a holds
a . i = b . i ) holds
Sum a = Sum b
proof end;

definition
let F be FinSequence of ExtREAL ;
func Sum F -> R_eal means :Def5: :: CONVFUN1:def 5
 ex f being Function of NAT , ExtREAL st
( it = f . (len F) & f . 0 = 0. & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) );
existence
ex b1 being R_eal ex f being Function of NAT , ExtREAL st
( b1 = f . (len F) & f . 0 = 0. & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) )
proof end;
uniqueness
for b1, b2 being R_eal st ex f being Function of NAT , ExtREAL st
( b1 = f . (len F) & f . 0 = 0. & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) & ex f being Function of NAT , ExtREAL st
( b2 = f . (len F) & f . 0 = 0. & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines Sum CONVFUN1:def 5 :
for F being FinSequence of ExtREAL
for b2 being R_eal holds
( b2 = Sum F iff ex f being Function of NAT , ExtREAL st
( b2 = f . (len F) & f . 0 = 0. & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) );

theorem Th4: :: CONVFUN1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Sum (<*> ExtREAL ) = 0.
proof end;

theorem Th5: :: CONVFUN1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being R_eal holds Sum <*a*> = a
proof end;

Lm7: for F being FinSequence of ExtREAL
for x being Element of ExtREAL holds Sum (F ^ <*x*>) = (Sum F) + x
proof end;

theorem Th6: :: CONVFUN1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being R_eal holds Sum <*a,b*> = a + b
proof end;

Lm8: for F being FinSequence of ExtREAL st not -infty in rng F holds
Sum F <> -infty
proof end;

Lm9: for F being FinSequence of ExtREAL st +infty in rng F & not -infty in rng F holds
Sum F = +infty
proof end;

Lm10: for a being FinSequence of ExtREAL
for b being FinSequence of REAL st len a = len b & ( for i being Nat st i in dom a holds
a . i = b . i ) holds
Sum a = Sum b
proof end;

Lm11: for n being 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 Nat st i in Seg n holds
a . i = b . i ) holds
Sum a = Sum b
proof end;

theorem Th7: :: CONVFUN1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G being FinSequence of ExtREAL st not -infty in rng F & not -infty in rng G holds
Sum (F ^ G) = (Sum F) + (Sum G)
proof end;

Lm12: for n, q being Nat st q in Seg (n + 1) holds
ex p being Permutation of Seg (n + 1) st
for i being Nat st i in Seg (n + 1) holds
( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) )
proof end;

Lm13: for n, q being Nat
for s, p being Permutation of Seg (n + 1)
for s' being FinSequence of Seg (n + 1) st s' = s & q = s . (n + 1) & ( for i being Nat st i in Seg (n + 1) holds
( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) ) holds
p * (s' | n) is Permutation of Seg n
proof end;

Lm14: for n, q being Nat
for p being Permutation of Seg (n + 1)
for F, H being FinSequence of ExtREAL st F = H * p & q in Seg (n + 1) & len H = n + 1 & not -infty in rng H & ( for i being Nat st i in Seg (n + 1) holds
( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) ) holds
Sum F = Sum H
proof end;

theorem Th8: :: CONVFUN1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G being FinSequence of ExtREAL
for s being Permutation of dom F st G = F * s & not -infty in rng F holds
Sum F = Sum G
proof end;

Lm15: for F being FinSequence of ExtREAL st rng F c= {0. } holds
Sum F = 0.
proof end;

Lm16: for F being FinSequence of REAL st rng F c= {0} holds
Sum F = 0
proof end;

Lm17: 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 6
{ [x,y] where x is Element of X, y is Element of REAL : f . x <=' R_EAL y } ;
coherence
{ [x,y] where x is Element of X, y is Element of REAL : f . x <=' R_EAL y } is Subset of (Prod_of_RLS X,RLS_Real )
proof end;
end;

:: deftheorem defines epigraph CONVFUN1:def 6 :
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 <=' R_EAL y } ;

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

:: deftheorem Def7 defines convex CONVFUN1:def 7 :
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 );

Lm18: for w being R_eal
for wr, p being Real st w = wr holds
p * wr = (R_EAL p) * w
proof end;

Lm19: for w1, w2 being R_eal
for wr1, wr2, p1, p2 being Real st w1 = wr1 & w2 = wr2 holds
(p1 * wr1) + (p2 * wr2) = ((R_EAL p1) * w1) + ((R_EAL p2) * w2)
proof end;

theorem Th9: :: CONVFUN1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)) <=' ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) )
proof end;

theorem :: CONVFUN1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)) <=' ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) )
proof end;

theorem :: CONVFUN1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th12: :: CONVFUN1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being RealLinearSpace
for M being Subset of X holds
( M is convex iff for n being non empty 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;

Lm20: for X being RealLinearSpace
for f being Function of the carrier of X, ExtREAL
for n being non empty Nat
for p being FinSequence of REAL
for F being FinSequence of ExtREAL
for y being FinSequence of the carrier of X st len p = n & len F = n & len y = n & ( for x being VECTOR of X holds f . x <> -infty ) & ( for i being Nat st i in Seg n holds
( p . i >= 0 & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
not -infty in rng F
proof end;

theorem Th13: :: CONVFUN1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 empty 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 Nat st i in Seg n holds
( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <=' Sum F )
proof end;

Lm21: for F being FinSequence of REAL ex s being Permutation of dom F ex n being Nat st
for i being Nat st i in dom F holds
( i in Seg n iff F . (s . i) <> 0 )
proof end;

theorem :: CONVFUN1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 empty 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 Nat st i in Seg n holds
( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <=' Sum F )
proof end;