:: CONVFUN1 semantic presentation

definition
let c1, c2 be non empty RLSStruct ;
func Add_in_Prod_of_RLS c1,c2 -> BinOp of [:the carrier of a1,the carrier of a2:] means :Def1: :: CONVFUN1:def 1
for b1, b2 being Element of [:the carrier of a1,the carrier of a2:]
for b3, b4 being VECTOR of a1
for b5, b6 being VECTOR of a2 st b1 = [b3,b5] & b2 = [b4,b6] holds
a3 . b1,b2 = [(the add of a1 . [b3,b4]),(the add of a2 . [b5,b6])];
existence
ex b1 being BinOp of [:the carrier of c1,the carrier of c2:] st
for b2, b3 being Element of [:the carrier of c1,the carrier of c2:]
for b4, b5 being VECTOR of c1
for b6, b7 being VECTOR of c2 st b2 = [b4,b6] & b3 = [b5,b7] holds
b1 . b2,b3 = [(the add of c1 . [b4,b5]),(the add of c2 . [b6,b7])]
proof end;
uniqueness
for b1, b2 being BinOp of [:the carrier of c1,the carrier of c2:] st ( for b3, b4 being Element of [:the carrier of c1,the carrier of c2:]
for b5, b6 being VECTOR of c1
for b7, b8 being VECTOR of c2 st b3 = [b5,b7] & b4 = [b6,b8] holds
b1 . b3,b4 = [(the add of c1 . [b5,b6]),(the add of c2 . [b7,b8])] ) & ( for b3, b4 being Element of [:the carrier of c1,the carrier of c2:]
for b5, b6 being VECTOR of c1
for b7, b8 being VECTOR of c2 st b3 = [b5,b7] & b4 = [b6,b8] holds
b2 . b3,b4 = [(the add of c1 . [b5,b6]),(the add of c2 . [b7,b8])] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Add_in_Prod_of_RLS CONVFUN1:def 1 :
for b1, b2 being non empty RLSStruct
for b3 being BinOp of [:the carrier of b1,the carrier of b2:] holds
( b3 = Add_in_Prod_of_RLS b1,b2 iff for b4, b5 being Element of [:the carrier of b1,the carrier of b2:]
for b6, b7 being VECTOR of b1
for b8, b9 being VECTOR of b2 st b4 = [b6,b8] & b5 = [b7,b9] holds
b3 . b4,b5 = [(the add of b1 . [b6,b7]),(the add of b2 . [b8,b9])] );

definition
let c1, c2 be non empty RLSStruct ;
func Mult_in_Prod_of_RLS c1,c2 -> Function of [:REAL ,[:the carrier of a1,the carrier of a2:]:],[:the carrier of a1,the carrier of a2:] means :Def2: :: CONVFUN1:def 2
for b1 being Real
for b2 being Element of [:the carrier of a1,the carrier of a2:]
for b3 being VECTOR of a1
for b4 being VECTOR of a2 st b2 = [b3,b4] holds
a3 . [b1,b2] = [(the Mult of a1 . [b1,b3]),(the Mult of a2 . [b1,b4])];
existence
ex b1 being Function of [:REAL ,[:the carrier of c1,the carrier of c2:]:],[:the carrier of c1,the carrier of c2:] st
for b2 being Real
for b3 being Element of [:the carrier of c1,the carrier of c2:]
for b4 being VECTOR of c1
for b5 being VECTOR of c2 st b3 = [b4,b5] holds
b1 . [b2,b3] = [(the Mult of c1 . [b2,b4]),(the Mult of c2 . [b2,b5])]
proof end;
uniqueness
for b1, b2 being Function of [:REAL ,[:the carrier of c1,the carrier of c2:]:],[:the carrier of c1,the carrier of c2:] st ( for b3 being Real
for b4 being Element of [:the carrier of c1,the carrier of c2:]
for b5 being VECTOR of c1
for b6 being VECTOR of c2 st b4 = [b5,b6] holds
b1 . [b3,b4] = [(the Mult of c1 . [b3,b5]),(the Mult of c2 . [b3,b6])] ) & ( for b3 being Real
for b4 being Element of [:the carrier of c1,the carrier of c2:]
for b5 being VECTOR of c1
for b6 being VECTOR of c2 st b4 = [b5,b6] holds
b2 . [b3,b4] = [(the Mult of c1 . [b3,b5]),(the Mult of c2 . [b3,b6])] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Mult_in_Prod_of_RLS CONVFUN1:def 2 :
for b1, b2 being non empty RLSStruct
for b3 being Function of [:REAL ,[:the carrier of b1,the carrier of b2:]:],[:the carrier of b1,the carrier of b2:] holds
( b3 = Mult_in_Prod_of_RLS b1,b2 iff for b4 being Real
for b5 being Element of [:the carrier of b1,the carrier of b2:]
for b6 being VECTOR of b1
for b7 being VECTOR of b2 st b5 = [b6,b7] holds
b3 . [b4,b5] = [(the Mult of b1 . [b4,b6]),(the Mult of b2 . [b4,b7])] );

definition
let c1, c2 be non empty RLSStruct ;
func Prod_of_RLS c1,c2 -> RLSStruct equals :: CONVFUN1:def 3
 RLSStruct(# [:the carrier of a1,the carrier of a2:],[(0. a1),(0. a2)],(Add_in_Prod_of_RLS a1,a2),(Mult_in_Prod_of_RLS a1,a2) #);
correctness
coherence
RLSStruct(# [:the carrier of c1,the carrier of c2:],[(0. c1),(0. c2)],(Add_in_Prod_of_RLS c1,c2),(Mult_in_Prod_of_RLS c1,c2) #) is RLSStruct ;
;
end;

:: deftheorem Def3 defines Prod_of_RLS CONVFUN1:def 3 :
for b1, b2 being non empty RLSStruct holds Prod_of_RLS b1,b2 = RLSStruct(# [:the carrier of b1,the carrier of b2:],[(0. b1),(0. b2)],(Add_in_Prod_of_RLS b1,b2),(Mult_in_Prod_of_RLS b1,b2) #);

registration
let c1, c2 be non empty RLSStruct ;
cluster Prod_of_RLS a1,a2 -> non empty ;
coherence
not Prod_of_RLS c1,c2 is empty ;
end;

theorem Th1: :: CONVFUN1:1
for b1, b2 being non empty RLSStruct
for b3 being VECTOR of b1
for b4 being VECTOR of b2
for b5 being VECTOR of (Prod_of_RLS b1,b2)
for b6 being Real st b5 = [b3,b4] holds
b6 * b5 = [(b6 * b3),(b6 * b4)]
proof end;

theorem Th2: :: CONVFUN1:2
for b1, b2 being non empty RLSStruct
for b3, b4 being VECTOR of b1
for b5, b6 being VECTOR of b2
for b7, b8 being VECTOR of (Prod_of_RLS b1,b2) st b7 = [b3,b5] & b8 = [b4,b6] holds
b7 + b8 = [(b3 + b4),(b5 + b6)]
proof end;

Lemma5: for b1, b2 being non empty RLSStruct holds 0. (Prod_of_RLS b1,b2) = [(0. b1),(0. b2)]
by RLVECT_1:def 2;

registration
let c1, c2 be non empty Abelian RLSStruct ;
cluster Prod_of_RLS a1,a2 -> non empty Abelian ;
coherence
Prod_of_RLS c1,c2 is Abelian
proof end;
end;

registration
let c1, c2 be non empty add-associative RLSStruct ;
cluster Prod_of_RLS a1,a2 -> non empty add-associative ;
coherence
Prod_of_RLS c1,c2 is add-associative
proof end;
end;

registration
let c1, c2 be non empty right_zeroed RLSStruct ;
cluster Prod_of_RLS a1,a2 -> non empty right_zeroed ;
coherence
Prod_of_RLS c1,c2 is right_zeroed
proof end;
end;

registration
let c1, c2 be non empty right_complementable RLSStruct ;
cluster Prod_of_RLS a1,a2 -> non empty right_complementable ;
coherence
Prod_of_RLS c1,c2 is right_complementable
proof end;
end;

registration
let c1, c2 be non empty RealLinearSpace-like RLSStruct ;
cluster Prod_of_RLS a1,a2 -> non empty RealLinearSpace-like ;
coherence
Prod_of_RLS c1,c2 is RealLinearSpace-like
proof end;
end;

theorem Th3: :: CONVFUN1:3
for b1, b2 being RealLinearSpace
for b3 being Nat
for b4 being FinSequence of the carrier of b1
for b5 being FinSequence of the carrier of b2
for b6 being FinSequence of the carrier of (Prod_of_RLS b1,b2) st len b4 = b3 & len b5 = b3 & len b6 = b3 & ( for b7 being Nat st b7 in Seg b3 holds
b6 . b7 = [(b4 . b7),(b5 . b7)] ) holds
Sum b6 = [(Sum b4),(Sum b5)]
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 Def4 defines RLS_Real CONVFUN1:def 4 :
RLS_Real = RLSStruct(# REAL ,0,addreal ,multreal #);

Lemma7: for b1 being VECTOR of RLS_Real
for b2, b3 being Real st b1 = b2 holds
b3 * b1 = b3 * b2
proof end;

Lemma8: for b1, b2 being VECTOR of RLS_Real
for b3, b4 being Real st b1 = b3 & b2 = b4 holds
b1 + b2 = b3 + b4
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;

Lemma9: for b1 being non empty RLSStruct
for b2 being VECTOR of b1
for b3 being VECTOR of (Prod_of_RLS b1,RLS_Real )
for b4, b5 being Real st b3 = [b2,b5] holds
b4 * b3 = [(b4 * b2),(b4 * b5)]
proof end;

Lemma10: for b1 being non empty RLSStruct
for b2, b3 being VECTOR of b1
for b4, b5 being Real
for b6, b7 being VECTOR of (Prod_of_RLS b1,RLS_Real ) st b6 = [b2,b4] & b7 = [b3,b5] holds
b6 + b7 = [(b2 + b3),(b4 + b5)]
proof end;

Lemma11: for b1 being FinSequence of the carrier of RLS_Real
for b2 being FinSequence of REAL st len b1 = len b2 & ( for b3 being Nat st b3 in dom b1 holds
b1 . b3 = b2 . b3 ) holds
Sum b1 = Sum b2
proof end;

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

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

theorem Th4: :: CONVFUN1:4
Sum (<*> ExtREAL ) = 0.
proof end;

theorem Th5: :: CONVFUN1:5
for b1 being R_eal holds Sum <*b1*> = b1
proof end;

Lemma15: for b1 being FinSequence of ExtREAL
for b2 being Element of ExtREAL holds Sum (b1 ^ <*b2*>) = (Sum b1) + b2
proof end;

theorem Th6: :: CONVFUN1:6
for b1, b2 being R_eal holds Sum <*b1,b2*> = b1 + b2
proof end;

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

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

Lemma19: for b1 being FinSequence of ExtREAL
for b2 being FinSequence of REAL st len b1 = len b2 & ( for b3 being Nat st b3 in dom b1 holds
b1 . b3 = b2 . b3 ) holds
Sum b1 = Sum b2
proof end;

Lemma20: for b1 being Nat
for b2 being FinSequence of ExtREAL
for b3 being FinSequence of the carrier of RLS_Real st len b2 = b1 & len b3 = b1 & ( for b4 being Nat st b4 in Seg b1 holds
b2 . b4 = b3 . b4 ) holds
Sum b2 = Sum b3
proof end;

theorem Th7: :: CONVFUN1:7
for b1, b2 being FinSequence of ExtREAL st not -infty in rng b1 & not -infty in rng b2 holds
Sum (b1 ^ b2) = (Sum b1) + (Sum b2)
proof end;

Lemma22: for b1, b2 being Nat st b2 in Seg (b1 + 1) holds
ex b3 being Permutation of Seg (b1 + 1) st
for b4 being Nat st b4 in Seg (b1 + 1) holds
( ( b4 < b2 implies b3 . b4 = b4 ) & ( b4 = b2 implies b3 . b4 = b1 + 1 ) & ( b4 > b2 implies b3 . b4 = b4 - 1 ) )
proof end;

Lemma23: for b1, b2 being Nat
for b3, b4 being Permutation of Seg (b1 + 1)
for b5 being FinSequence of Seg (b1 + 1) st b5 = b3 & b2 = b3 . (b1 + 1) & ( for b6 being Nat st b6 in Seg (b1 + 1) holds
( ( b6 < b2 implies b4 . b6 = b6 ) & ( b6 = b2 implies b4 . b6 = b1 + 1 ) & ( b6 > b2 implies b4 . b6 = b6 - 1 ) ) ) holds
b4 * (b5 | b1) is Permutation of Seg b1
proof end;

Lemma24: for b1, b2 being Nat
for b3 being Permutation of Seg (b1 + 1)
for b4, b5 being FinSequence of ExtREAL st b4 = b5 * b3 & b2 in Seg (b1 + 1) & len b5 = b1 + 1 & not -infty in rng b5 & ( for b6 being Nat st b6 in Seg (b1 + 1) holds
( ( b6 < b2 implies b3 . b6 = b6 ) & ( b6 = b2 implies b3 . b6 = b1 + 1 ) & ( b6 > b2 implies b3 . b6 = b6 - 1 ) ) ) holds
Sum b4 = Sum b5
proof end;

theorem Th8: :: CONVFUN1:8
for b1, b2 being FinSequence of ExtREAL
for b3 being Permutation of dom b1 st b2 = b1 * b3 & not -infty in rng b1 holds
Sum b1 = Sum b2
proof end;

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

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

Lemma28: for b1 being RealLinearSpace
for b2 being FinSequence of the carrier of b1 st rng b2 c= {(0. b1)} holds
Sum b2 = 0. b1
proof end;

definition
let c1 be non empty RLSStruct ;
let c2 be Function of the carrier of c1, ExtREAL ;
func epigraph c2 -> Subset of (Prod_of_RLS a1,RLS_Real ) equals :: CONVFUN1:def 6
{ [b1,b2] where B is Element of a1, B is Element of REAL : a2 . b1 <=' R_EAL b2 } ;
coherence
{ [b1,b2] where B is Element of c1, B is Element of REAL : c2 . b1 <=' R_EAL b2 } is Subset of (Prod_of_RLS c1,RLS_Real )
proof end;
end;

:: deftheorem Def6 defines epigraph CONVFUN1:def 6 :
for b1 being non empty RLSStruct
for b2 being Function of the carrier of b1, ExtREAL holds epigraph b2 = { [b3,b4] where B is Element of b1, B is Element of REAL : b2 . b3 <=' R_EAL b4 } ;

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

:: deftheorem Def7 defines convex CONVFUN1:def 7 :
for b1 being non empty RLSStruct
for b2 being Function of the carrier of b1, ExtREAL holds
( b2 is convex iff epigraph b2 is convex );

Lemma30: for b1 being R_eal
for b2, b3 being Real st b1 = b2 holds
b3 * b2 = (R_EAL b3) * b1
proof end;

Lemma31: for b1, b2 being R_eal
for b3, b4, b5, b6 being Real st b1 = b3 & b2 = b4 holds
(b5 * b3) + (b6 * b4) = ((R_EAL b5) * b1) + ((R_EAL b6) * b2)
proof end;

theorem Th9: :: CONVFUN1:9
for b1 being non empty RLSStruct
for b2 being Function of the carrier of b1, ExtREAL st ( for b3 being VECTOR of b1 holds b2 . b3 <> -infty ) holds
( b2 is convex iff for b3, b4 being VECTOR of b1
for b5 being Real st 0 < b5 & b5 < 1 holds
b2 . ((b5 * b3) + ((1 - b5) * b4)) <=' ((R_EAL b5) * (b2 . b3)) + ((R_EAL (1 - b5)) * (b2 . b4)) )
proof end;

theorem Th10: :: CONVFUN1:10
for b1 being RealLinearSpace
for b2 being Function of the carrier of b1, ExtREAL st ( for b3 being VECTOR of b1 holds b2 . b3 <> -infty ) holds
( b2 is convex iff for b3, b4 being VECTOR of b1
for b5 being Real st 0 <= b5 & b5 <= 1 holds
b2 . ((b5 * b3) + ((1 - b5) * b4)) <=' ((R_EAL b5) * (b2 . b3)) + ((R_EAL (1 - b5)) * (b2 . b4)) )
proof end;

theorem Th11: :: CONVFUN1:11
for b1 being PartFunc of REAL , REAL
for b2 being Function of the carrier of RLS_Real , ExtREAL
for b3 being Subset of RLS_Real st b3 c= dom b1 & ( for b4 being Real holds
( ( b4 in b3 implies b2 . b4 = b1 . b4 ) & ( not b4 in b3 implies b2 . b4 = +infty ) ) ) holds
( b2 is convex iff ( b1 is_convex_on b3 & b3 is convex ) )
proof end;

theorem Th12: :: CONVFUN1:12
for b1 being RealLinearSpace
for b2 being Subset of b1 holds
( b2 is convex iff for b3 being non empty Nat
for b4 being FinSequence of REAL
for b5, b6 being FinSequence of the carrier of b1 st len b4 = b3 & len b5 = b3 & len b6 = b3 & Sum b4 = 1 & ( for b7 being Nat st b7 in Seg b3 holds
( b4 . b7 > 0 & b6 . b7 = (b4 . b7) * (b5 /. b7) & b5 /. b7 in b2 ) ) holds
Sum b6 in b2 )
proof end;

Lemma34: for b1 being RealLinearSpace
for b2 being Function of the carrier of b1, ExtREAL
for b3 being non empty Nat
for b4 being FinSequence of REAL
for b5 being FinSequence of ExtREAL
for b6 being FinSequence of the carrier of b1 st len b4 = b3 & len b5 = b3 & len b6 = b3 & ( for b7 being VECTOR of b1 holds b2 . b7 <> -infty ) & ( for b7 being Nat st b7 in Seg b3 holds
( b4 . b7 >= 0 & b5 . b7 = (R_EAL (b4 . b7)) * (b2 . (b6 /. b7)) ) ) holds
not -infty in rng b5
proof end;

theorem Th13: :: CONVFUN1:13
for b1 being RealLinearSpace
for b2 being Function of the carrier of b1, ExtREAL st ( for b3 being VECTOR of b1 holds b2 . b3 <> -infty ) holds
( b2 is convex iff for b3 being non empty Nat
for b4 being FinSequence of REAL
for b5 being FinSequence of ExtREAL
for b6, b7 being FinSequence of the carrier of b1 st len b4 = b3 & len b5 = b3 & len b6 = b3 & len b7 = b3 & Sum b4 = 1 & ( for b8 being Nat st b8 in Seg b3 holds
( b4 . b8 > 0 & b7 . b8 = (b4 . b8) * (b6 /. b8) & b5 . b8 = (R_EAL (b4 . b8)) * (b2 . (b6 /. b8)) ) ) holds
b2 . (Sum b7) <=' Sum b5 )
proof end;

Lemma36: for b1 being FinSequence of REAL ex b2 being Permutation of dom b1ex b3 being Nat st
for b4 being Nat st b4 in dom b1 holds
( b4 in Seg b3 iff b1 . (b2 . b4) <> 0 )
proof end;

theorem Th14: :: CONVFUN1:14
for b1 being RealLinearSpace
for b2 being Function of the carrier of b1, ExtREAL st ( for b3 being VECTOR of b1 holds b2 . b3 <> -infty ) holds
( b2 is convex iff for b3 being non empty Nat
for b4 being FinSequence of REAL
for b5 being FinSequence of ExtREAL
for b6, b7 being FinSequence of the carrier of b1 st len b4 = b3 & len b5 = b3 & len b6 = b3 & len b7 = b3 & Sum b4 = 1 & ( for b8 being Nat st b8 in Seg b3 holds
( b4 . b8 >= 0 & b7 . b8 = (b4 . b8) * (b6 /. b8) & b5 . b8 = (R_EAL (b4 . b8)) * (b2 . (b6 /. b8)) ) ) holds
b2 . (Sum b7) <=' Sum b5 )
proof end;