:: CONVFUN1 semantic presentation
begin
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
defpred S1[ set , set , set ] means for x1, x2 being VECTOR of X
for y1, y2 being VECTOR of Y st $1 = [x1,y1] & $2 = [x2,y2] holds
$3 = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])];
set A = [: the carrier of X, the carrier of Y:];
A1: for z1, z2 being Element of [: the carrier of X, the carrier of Y:] ex z3 being Element of [: the carrier of X, the carrier of Y:] st S1[z1,z2,z3]
proof
let z1, z2 be Element of [: the carrier of X, the carrier of Y:]; ::_thesis: ex z3 being Element of [: the carrier of X, the carrier of Y:] st S1[z1,z2,z3]
consider x19, y19 being set such that
A2: x19 in the carrier of X and
A3: y19 in the carrier of Y and
A4: z1 = [x19,y19] by ZFMISC_1:def_2;
consider x29, y29 being set such that
A5: x29 in the carrier of X and
A6: y29 in the carrier of Y and
A7: z2 = [x29,y29] by ZFMISC_1:def_2;
reconsider y19 = y19, y29 = y29 as VECTOR of Y by A3, A6;
reconsider x19 = x19, x29 = x29 as VECTOR of X by A2, A5;
reconsider z3 = [( the addF of X . [x19,x29]),( the addF of Y . [y19,y29])] as Element of [: the carrier of X, the carrier of Y:] ;
take z3 ; ::_thesis: S1[z1,z2,z3]
let x1, x2 be VECTOR of X; ::_thesis: for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds
z3 = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])]
let y1, y2 be VECTOR of Y; ::_thesis: ( z1 = [x1,y1] & z2 = [x2,y2] implies z3 = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] )
assume that
A8: z1 = [x1,y1] and
A9: z2 = [x2,y2] ; ::_thesis: z3 = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])]
A10: x2 = x29 by A7, A9, XTUPLE_0:1;
A11: y1 = y19 by A4, A8, XTUPLE_0:1;
x1 = x19 by A4, A8, XTUPLE_0:1;
hence z3 = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] by A7, A9, A10, A11, XTUPLE_0:1; ::_thesis: verum
end;
thus ex o being BinOp of [: the carrier of X, the carrier of Y:] st
for a, b being Element of [: the carrier of X, the carrier of Y:] holds S1[a,b,o . (a,b)] from BINOP_1:sch_3(A1); ::_thesis: verum
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
let A1, A2 be BinOp of [: the carrier of X, the carrier of Y:]; ::_thesis: ( ( 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
A1 . (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
A2 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] ) implies A1 = A2 )
assume A12: 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
A1 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] ; ::_thesis: ( ex z1, z2 being Element of [: the carrier of X, the carrier of Y:] ex x1, x2 being VECTOR of X ex y1, y2 being VECTOR of Y st
( z1 = [x1,y1] & z2 = [x2,y2] & not A2 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] ) or A1 = A2 )
assume A13: 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
A2 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] ; ::_thesis: A1 = A2
for z1, z2 being Element of [: the carrier of X, the carrier of Y:] holds A1 . (z1,z2) = A2 . (z1,z2)
proof
let z1, z2 be Element of [: the carrier of X, the carrier of Y:]; ::_thesis: A1 . (z1,z2) = A2 . (z1,z2)
consider x1, y1 being set such that
A14: x1 in the carrier of X and
A15: y1 in the carrier of Y and
A16: z1 = [x1,y1] by ZFMISC_1:def_2;
consider x2, y2 being set such that
A17: x2 in the carrier of X and
A18: y2 in the carrier of Y and
A19: z2 = [x2,y2] by ZFMISC_1:def_2;
reconsider y1 = y1, y2 = y2 as VECTOR of Y by A15, A18;
reconsider x1 = x1, x2 = x2 as VECTOR of X by A14, A17;
A1 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] by A12, A16, A19;
hence A1 . (z1,z2) = A2 . (z1,z2) by A13, A16, A19; ::_thesis: verum
end;
hence A1 = A2 by BINOP_1:2; ::_thesis: verum
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
defpred S1[ set , set , set ] means for x being VECTOR of X
for y being VECTOR of Y st $2 = [x,y] holds
$3 = [( the Mult of X . [$1,x]),( the Mult of Y . [$1,y])];
A1: for a1 being Element of REAL
for z being Element of [: the carrier of X, the carrier of Y:] ex w being Element of [: the carrier of X, the carrier of Y:] st S1[a1,z,w]
proof
let a1 be Element of REAL ; ::_thesis: for z being Element of [: the carrier of X, the carrier of Y:] ex w being Element of [: the carrier of X, the carrier of Y:] st S1[a1,z,w]
let z be Element of [: the carrier of X, the carrier of Y:]; ::_thesis: ex w being Element of [: the carrier of X, the carrier of Y:] st S1[a1,z,w]
consider x9, y9 being set such that
A2: x9 in the carrier of X and
A3: y9 in the carrier of Y and
A4: z = [x9,y9] by ZFMISC_1:def_2;
reconsider y9 = y9 as VECTOR of Y by A3;
reconsider x9 = x9 as VECTOR of X by A2;
reconsider w = [( the Mult of X . [a1,x9]),( the Mult of Y . [a1,y9])] as Element of [: the carrier of X, the carrier of Y:] ;
take w ; ::_thesis: S1[a1,z,w]
for x being VECTOR of X
for y being VECTOR of Y st z = [x,y] holds
w = [( the Mult of X . [a1,x]),( the Mult of Y . [a1,y])]
proof
let x be VECTOR of X; ::_thesis: for y being VECTOR of Y st z = [x,y] holds
w = [( the Mult of X . [a1,x]),( the Mult of Y . [a1,y])]
let y be VECTOR of Y; ::_thesis: ( z = [x,y] implies w = [( the Mult of X . [a1,x]),( the Mult of Y . [a1,y])] )
assume A5: z = [x,y] ; ::_thesis: w = [( the Mult of X . [a1,x]),( the Mult of Y . [a1,y])]
then x = x9 by A4, XTUPLE_0:1;
hence w = [( the Mult of X . [a1,x]),( the Mult of Y . [a1,y])] by A4, A5, XTUPLE_0:1; ::_thesis: verum
end;
hence S1[a1,z,w] ; ::_thesis: verum
end;
consider g being Function of [:REAL,[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:] such that
A6: for a being Element of REAL
for z being Element of [: the carrier of X, the carrier of Y:] holds S1[a,z,g . (a,z)] from BINOP_1:sch_3(A1);
take g ; ::_thesis: 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
g . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])]
let a be Real; ::_thesis: 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
g . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])]
let z be Element of [: the carrier of X, the carrier of Y:]; ::_thesis: for x being VECTOR of X
for y being VECTOR of Y st z = [x,y] holds
g . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])]
thus for x being VECTOR of X
for y being VECTOR of Y st z = [x,y] holds
g . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] by A6; ::_thesis: verum
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
let g1, g2 be Function of [:REAL,[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:]; ::_thesis: ( ( 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
g1 . (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
g2 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] ) implies g1 = g2 )
assume A7: 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
g1 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] ; ::_thesis: ( ex a being Real ex z being Element of [: the carrier of X, the carrier of Y:] ex x being VECTOR of X ex y being VECTOR of Y st
( z = [x,y] & not g2 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] ) or g1 = g2 )
assume A8: 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
g2 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] ; ::_thesis: g1 = g2
for a being Real
for z being Element of [: the carrier of X, the carrier of Y:] holds g1 . (a,z) = g2 . (a,z)
proof
let a be Real; ::_thesis: for z being Element of [: the carrier of X, the carrier of Y:] holds g1 . (a,z) = g2 . (a,z)
let z be Element of [: the carrier of X, the carrier of Y:]; ::_thesis: g1 . (a,z) = g2 . (a,z)
consider x, y being set such that
A9: x in the carrier of X and
A10: y in the carrier of Y and
A11: z = [x,y] by ZFMISC_1:def_2;
reconsider y = y as VECTOR of Y by A10;
reconsider x = x as VECTOR of X by A9;
g1 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] by A7, A11;
hence g1 . (a,z) = g2 . (a,z) by A8, A11; ::_thesis: verum
end;
hence g1 = g2 by BINOP_1:2; ::_thesis: verum
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
for u1, u2 being Element of (Prod_of_RLS (X,Y)) holds u1 + u2 = u2 + u1
proof
let u1, u2 be Element of (Prod_of_RLS (X,Y)); ::_thesis: u1 + u2 = u2 + u1
consider x1, y1 being set such that
A1: x1 in the carrier of X and
A2: y1 in the carrier of Y and
A3: u1 = [x1,y1] by ZFMISC_1:def_2;
reconsider y1 = y1 as VECTOR of Y by A2;
reconsider x1 = x1 as VECTOR of X by A1;
consider x2, y2 being set such that
A4: x2 in the carrier of X and
A5: y2 in the carrier of Y and
A6: u2 = [x2,y2] by ZFMISC_1:def_2;
reconsider y2 = y2 as VECTOR of Y by A5;
reconsider x2 = x2 as VECTOR of X by A4;
u1 + u2 = [(x2 + x1),(y2 + y1)] by A3, A6, Th2;
hence u1 + u2 = u2 + u1 by A3, A6, Def1; ::_thesis: verum
end;
hence Prod_of_RLS (X,Y) is Abelian by RLVECT_1:def_2; ::_thesis: verum
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
for u1, u2, u3 being Element of (Prod_of_RLS (X,Y)) holds (u1 + u2) + u3 = u1 + (u2 + u3)
proof
let u1, u2, u3 be Element of (Prod_of_RLS (X,Y)); ::_thesis: (u1 + u2) + u3 = u1 + (u2 + u3)
consider x1, y1 being set such that
A1: x1 in the carrier of X and
A2: y1 in the carrier of Y and
A3: u1 = [x1,y1] by ZFMISC_1:def_2;
reconsider y1 = y1 as VECTOR of Y by A2;
consider x3, y3 being set such that
A4: x3 in the carrier of X and
A5: y3 in the carrier of Y and
A6: u3 = [x3,y3] by ZFMISC_1:def_2;
reconsider y3 = y3 as VECTOR of Y by A5;
reconsider x3 = x3 as VECTOR of X by A4;
reconsider x1 = x1 as VECTOR of X by A1;
consider x2, y2 being set such that
A7: x2 in the carrier of X and
A8: y2 in the carrier of Y and
A9: u2 = [x2,y2] by ZFMISC_1:def_2;
reconsider y2 = y2 as VECTOR of Y by A8;
reconsider x2 = x2 as VECTOR of X by A7;
u1 + u2 = [(x1 + x2),(y1 + y2)] by A3, A9, Def1;
then A10: (u1 + u2) + u3 = [((x1 + x2) + x3),((y1 + y2) + y3)] by A6, Def1;
u2 + u3 = [(x2 + x3),(y2 + y3)] by A9, A6, Def1;
then A11: u1 + (u2 + u3) = [(x1 + (x2 + x3)),(y1 + (y2 + y3))] by A3, Def1;
(x1 + x2) + x3 = x1 + (x2 + x3) by RLVECT_1:def_3;
hence (u1 + u2) + u3 = u1 + (u2 + u3) by A10, A11, RLVECT_1:def_3; ::_thesis: verum
end;
hence Prod_of_RLS (X,Y) is add-associative by RLVECT_1:def_3; ::_thesis: verum
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
for u being Element of (Prod_of_RLS (X,Y)) holds u + (0. (Prod_of_RLS (X,Y))) = u
proof
let u be Element of (Prod_of_RLS (X,Y)); ::_thesis: u + (0. (Prod_of_RLS (X,Y))) = u
consider x, y being set such that
A1: x in the carrier of X and
A2: y in the carrier of Y and
A3: u = [x,y] by ZFMISC_1:def_2;
reconsider y = y as VECTOR of Y by A2;
reconsider x = x as VECTOR of X by A1;
A4: y + (0. Y) = y by RLVECT_1:def_4;
x + (0. X) = x by RLVECT_1:def_4;
hence u + (0. (Prod_of_RLS (X,Y))) = u by A3, A4, Def1; ::_thesis: verum
end;
hence Prod_of_RLS (X,Y) is right_zeroed by RLVECT_1:def_4; ::_thesis: verum
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
let u be Element of (Prod_of_RLS (X,Y)); :: according to ALGSTR_0:def_16 ::_thesis: u is right_complementable
consider x, y being set such that
A1: x in the carrier of X and
A2: y in the carrier of Y and
A3: u = [x,y] by ZFMISC_1:def_2;
reconsider x = x as VECTOR of X by A1;
consider x1 being VECTOR of X such that
A4: x + x1 = 0. X by ALGSTR_0:def_11;
reconsider y = y as VECTOR of Y by A2;
consider y1 being VECTOR of Y such that
A5: y + y1 = 0. Y by ALGSTR_0:def_11;
set u1 = [x1,y1];
reconsider u1 = [x1,y1] as Element of (Prod_of_RLS (X,Y)) ;
take u1 ; :: according to ALGSTR_0:def_11 ::_thesis: u + u1 = 0. (Prod_of_RLS (X,Y))
thus u + u1 = 0. (Prod_of_RLS (X,Y)) by A3, A4, A5, Def1; ::_thesis: verum
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
A1: for a being real number
for u1, u2 being VECTOR of (Prod_of_RLS (X,Y)) holds a * (u1 + u2) = (a * u1) + (a * u2)
proof
let a be real number ; ::_thesis: for u1, u2 being VECTOR of (Prod_of_RLS (X,Y)) holds a * (u1 + u2) = (a * u1) + (a * u2)
reconsider a = a as Real by XREAL_0:def_1;
let u1, u2 be VECTOR of (Prod_of_RLS (X,Y)); ::_thesis: a * (u1 + u2) = (a * u1) + (a * u2)
consider x1, y1 being set such that
A2: x1 in the carrier of X and
A3: y1 in the carrier of Y and
A4: u1 = [x1,y1] by ZFMISC_1:def_2;
reconsider x1 = x1 as VECTOR of X by A2;
consider x2, y2 being set such that
A5: x2 in the carrier of X and
A6: y2 in the carrier of Y and
A7: u2 = [x2,y2] by ZFMISC_1:def_2;
reconsider y2 = y2 as VECTOR of Y by A6;
reconsider x2 = x2 as VECTOR of X by A5;
reconsider y1 = y1 as VECTOR of Y by A3;
A8: a * (x1 + x2) = (a * x1) + (a * x2) by RLVECT_1:def_5;
u1 + u2 = [(x1 + x2),(y1 + y2)] by A4, A7, Def1;
then A9: a * (u1 + u2) = [(a * (x1 + x2)),(a * (y1 + y2))] by Def2;
A10: a * (y1 + y2) = (a * y1) + (a * y2) by RLVECT_1:def_5;
A11: a * u2 = [(a * x2),(a * y2)] by A7, Def2;
a * u1 = [(a * x1),(a * y1)] by A4, Def2;
hence a * (u1 + u2) = (a * u1) + (a * u2) by A9, A11, A8, A10, Def1; ::_thesis: verum
end;
A12: for a, b being real number
for u being VECTOR of (Prod_of_RLS (X,Y)) holds (a * b) * u = a * (b * u)
proof
let a, b be real number ; ::_thesis: for u being VECTOR of (Prod_of_RLS (X,Y)) holds (a * b) * u = a * (b * u)
reconsider a = a, b = b as Real by XREAL_0:def_1;
let u be VECTOR of (Prod_of_RLS (X,Y)); ::_thesis: (a * b) * u = a * (b * u)
consider x, y being set such that
A13: x in the carrier of X and
A14: y in the carrier of Y and
A15: u = [x,y] by ZFMISC_1:def_2;
reconsider y = y as VECTOR of Y by A14;
reconsider x = x as VECTOR of X by A13;
b * u = [(b * x),(b * y)] by A15, Def2;
then A16: a * (b * u) = [(a * (b * x)),(a * (b * y))] by Def2;
A17: (a * b) * y = a * (b * y) by RLVECT_1:def_7;
(a * b) * x = a * (b * x) by RLVECT_1:def_7;
hence (a * b) * u = a * (b * u) by A15, A16, A17, Def2; ::_thesis: verum
end;
A18: for a, b being real number
for u being VECTOR of (Prod_of_RLS (X,Y)) holds (a + b) * u = (a * u) + (b * u)
proof
let a, b be real number ; ::_thesis: for u being VECTOR of (Prod_of_RLS (X,Y)) holds (a + b) * u = (a * u) + (b * u)
reconsider a = a, b = b as Real by XREAL_0:def_1;
let u be VECTOR of (Prod_of_RLS (X,Y)); ::_thesis: (a + b) * u = (a * u) + (b * u)
consider x, y being set such that
A19: x in the carrier of X and
A20: y in the carrier of Y and
A21: u = [x,y] by ZFMISC_1:def_2;
reconsider y = y as VECTOR of Y by A20;
reconsider x = x as VECTOR of X by A19;
A22: b * u = [(b * x),(b * y)] by A21, Def2;
a * u = [(a * x),(a * y)] by A21, Def2;
then A23: (a * u) + (b * u) = [((a * x) + (b * x)),((a * y) + (b * y))] by A22, Def1;
A24: (a + b) * y = (a * y) + (b * y) by RLVECT_1:def_6;
(a + b) * x = (a * x) + (b * x) by RLVECT_1:def_6;
hence (a + b) * u = (a * u) + (b * u) by A21, A23, A24, Def2; ::_thesis: verum
end;
for u being VECTOR of (Prod_of_RLS (X,Y)) holds 1 * u = u
proof
let u be VECTOR of (Prod_of_RLS (X,Y)); ::_thesis: 1 * u = u
consider x, y being set such that
A25: x in the carrier of X and
A26: y in the carrier of Y and
A27: u = [x,y] by ZFMISC_1:def_2;
reconsider y = y as VECTOR of Y by A26;
reconsider x = x as VECTOR of X by A25;
A28: 1 * y = y by RLVECT_1:def_8;
1 * x = x by RLVECT_1:def_8;
hence 1 * u = u by A27, A28, Def2; ::_thesis: verum
end;
hence ( 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 ) by A1, A18, A12, RLVECT_1:def_5, RLVECT_1:def_6, RLVECT_1:def_7, RLVECT_1:def_8; ::_thesis: verum
end;
end;
theorem Th3: :: CONVFUN1:3
for X, Y being RealLinearSpace
for n being Element of 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 Element of NAT st i in Seg n holds
z . i = [(x . i),(y . i)] ) holds
Sum z = [(Sum x),(Sum y)]
proof
let X, Y be RealLinearSpace; ::_thesis: for n being Element of 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 Element of NAT st i in Seg n holds
z . i = [(x . i),(y . i)] ) holds
Sum z = [(Sum x),(Sum y)]
defpred S1[ Element of NAT ] means 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 = $1 & len y = $1 & len z = $1 & ( for i being Element of NAT st i in Seg $1 holds
z . i = [(x . i),(y . i)] ) holds
Sum z = [(Sum x),(Sum y)];
A1: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
thus S1[n + 1] ::_thesis: verum
proof
let x be FinSequence of the carrier of X; ::_thesis: 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 + 1 & len y = n + 1 & len z = n + 1 & ( for i being Element of NAT st i in Seg (n + 1) holds
z . i = [(x . i),(y . i)] ) holds
Sum z = [(Sum x),(Sum y)]
let y be FinSequence of the carrier of Y; ::_thesis: for z being FinSequence of the carrier of (Prod_of_RLS (X,Y)) st len x = n + 1 & len y = n + 1 & len z = n + 1 & ( for i being Element of NAT st i in Seg (n + 1) holds
z . i = [(x . i),(y . i)] ) holds
Sum z = [(Sum x),(Sum y)]
let z be FinSequence of the carrier of (Prod_of_RLS (X,Y)); ::_thesis: ( len x = n + 1 & len y = n + 1 & len z = n + 1 & ( for i being Element of NAT st i in Seg (n + 1) holds
z . i = [(x . i),(y . i)] ) implies Sum z = [(Sum x),(Sum y)] )
assume that
A3: len x = n + 1 and
A4: len y = n + 1 and
A5: len z = n + 1 and
A6: for i being Element of NAT st i in Seg (n + 1) holds
z . i = [(x . i),(y . i)] ; ::_thesis: Sum z = [(Sum x),(Sum y)]
A7: 0 + n <= 1 + n by XREAL_1:6;
then A8: len (y | n) = n by A4, FINSEQ_1:59;
A9: Seg n c= Seg (n + 1) by A7, FINSEQ_1:5;
A10: for i being Element of NAT st i in Seg n holds
(z | n) . i = [((x | n) . i),((y | n) . i)]
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies (z | n) . i = [((x | n) . i),((y | n) . i)] )
assume A11: i in Seg n ; ::_thesis: (z | n) . i = [((x | n) . i),((y | n) . i)]
then A12: i <= n by FINSEQ_1:1;
then A13: (y | n) . i = y . i by FINSEQ_3:112;
A14: (z | n) . i = z . i by A12, FINSEQ_3:112;
(x | n) . i = x . i by A12, FINSEQ_3:112;
hence (z | n) . i = [((x | n) . i),((y | n) . i)] by A6, A9, A11, A13, A14; ::_thesis: verum
end;
A15: for i being Element of NAT st i in Seg (n + 1) holds
( x /. i = x . i & y /. i = y . i & z /. i = z . i )
proof
let i be Element of NAT ; ::_thesis: ( i in Seg (n + 1) implies ( x /. i = x . i & y /. i = y . i & z /. i = z . i ) )
assume A16: i in Seg (n + 1) ; ::_thesis: ( x /. i = x . i & y /. i = y . i & z /. i = z . i )
then A17: i <= n + 1 by FINSEQ_1:1;
1 <= i by A16, FINSEQ_1:1;
hence ( x /. i = x . i & y /. i = y . i & z /. i = z . i ) by A3, A4, A5, A17, FINSEQ_4:15; ::_thesis: verum
end;
A18: n + 1 in Seg (n + 1) by FINSEQ_1:4;
then A19: y /. (n + 1) = y . (n + 1) by A15;
z | n = z | (Seg n) by FINSEQ_1:def_15;
then z = (z | n) ^ <*(z . (n + 1))*> by A5, FINSEQ_3:55;
then z = (z | n) ^ <*(z /. (n + 1))*> by A15, A18;
then A20: Sum z = (Sum (z | n)) + (Sum <*(z /. (n + 1))*>) by RLVECT_1:41
.= (Sum (z | n)) + (z /. (n + 1)) by RLVECT_1:44 ;
y | n = y | (Seg n) by FINSEQ_1:def_15;
then y = (y | n) ^ <*(y . (n + 1))*> by A4, FINSEQ_3:55;
then y = (y | n) ^ <*(y /. (n + 1))*> by A15, A18;
then A21: Sum y = (Sum (y | n)) + (Sum <*(y /. (n + 1))*>) by RLVECT_1:41
.= (Sum (y | n)) + (y /. (n + 1)) by RLVECT_1:44 ;
x | n = x | (Seg n) by FINSEQ_1:def_15;
then x = (x | n) ^ <*(x . (n + 1))*> by A3, FINSEQ_3:55;
then x = (x | n) ^ <*(x /. (n + 1))*> by A15, A18;
then A22: Sum x = (Sum (x | n)) + (Sum <*(x /. (n + 1))*>) by RLVECT_1:41
.= (Sum (x | n)) + (x /. (n + 1)) by RLVECT_1:44 ;
A23: z /. (n + 1) = z . (n + 1) by A15, A18;
x /. (n + 1) = x . (n + 1) by A15, A18;
then A24: z /. (n + 1) = [(x /. (n + 1)),(y /. (n + 1))] by A6, A19, A23, FINSEQ_1:4;
A25: len (z | n) = n by A5, A7, FINSEQ_1:59;
len (x | n) = n by A3, A7, FINSEQ_1:59;
then Sum (z | n) = [(Sum (x | n)),(Sum (y | n))] by A2, A8, A25, A10;
hence Sum z = [(Sum x),(Sum y)] by A24, A22, A21, A20, Def1; ::_thesis: verum
end;
end;
A26: S1[ 0 ]
proof
let x be FinSequence of the carrier of X; ::_thesis: 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 = 0 & len y = 0 & len z = 0 & ( for i being Element of NAT st i in Seg 0 holds
z . i = [(x . i),(y . i)] ) holds
Sum z = [(Sum x),(Sum y)]
let y be FinSequence of the carrier of Y; ::_thesis: for z being FinSequence of the carrier of (Prod_of_RLS (X,Y)) st len x = 0 & len y = 0 & len z = 0 & ( for i being Element of NAT st i in Seg 0 holds
z . i = [(x . i),(y . i)] ) holds
Sum z = [(Sum x),(Sum y)]
let z be FinSequence of the carrier of (Prod_of_RLS (X,Y)); ::_thesis: ( len x = 0 & len y = 0 & len z = 0 & ( for i being Element of NAT st i in Seg 0 holds
z . i = [(x . i),(y . i)] ) implies Sum z = [(Sum x),(Sum y)] )
assume that
A27: len x = 0 and
A28: len y = 0 and
A29: len z = 0 and
for i being Element of NAT st i in Seg 0 holds
z . i = [(x . i),(y . i)] ; ::_thesis: Sum z = [(Sum x),(Sum y)]
x = <*> the carrier of X by A27;
then A30: Sum x = 0. X by RLVECT_1:43;
z = <*> the carrier of (Prod_of_RLS (X,Y)) by A29;
then A31: Sum z = 0. (Prod_of_RLS (X,Y)) by RLVECT_1:43;
y = <*> the carrier of Y by A28;
hence Sum z = [(Sum x),(Sum y)] by A30, A31, RLVECT_1:43; ::_thesis: verum
end;
thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A26, A1); ::_thesis: verum
end;
begin
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 #);
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
thus RLS_Real is Abelian ::_thesis: ( 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
let v, w be VECTOR of RLS_Real; :: according to RLVECT_1:def_2 ::_thesis: v + w = w + v
reconsider vr = v as Real ;
reconsider wr = w as Real ;
thus v + w = vr + wr by BINOP_2:def_9
.= w + v by BINOP_2:def_9 ; ::_thesis: verum
end;
thus RLS_Real is add-associative ::_thesis: ( 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
let u, v, w be VECTOR of RLS_Real; :: according to RLVECT_1:def_3 ::_thesis: (u + v) + w = u + (v + w)
reconsider ur = u as Real ;
reconsider vr = v as Real ;
reconsider wr = w as Real ;
v + w = vr + wr by BINOP_2:def_9;
then A1: u + (v + w) = ur + (vr + wr) by BINOP_2:def_9;
u + v = ur + vr by BINOP_2:def_9;
then (u + v) + w = (ur + vr) + wr by BINOP_2:def_9;
hence (u + v) + w = u + (v + w) by A1; ::_thesis: verum
end;
thus RLS_Real is right_zeroed ::_thesis: ( 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
let v be VECTOR of RLS_Real; :: according to RLVECT_1:def_4 ::_thesis: v + (0. RLS_Real) = v
reconsider vr = v as Real ;
thus v + (0. RLS_Real) = vr + 0 by BINOP_2:def_9
.= v ; ::_thesis: verum
end;
thus RLS_Real is right_complementable ::_thesis: ( RLS_Real is vector-distributive & RLS_Real is scalar-distributive & RLS_Real is scalar-associative & RLS_Real is scalar-unital )
proof
let v be VECTOR of RLS_Real; :: according to ALGSTR_0:def_16 ::_thesis: v is right_complementable
reconsider vr = v as Real ;
reconsider w = - vr as VECTOR of RLS_Real ;
take w ; :: according to ALGSTR_0:def_11 ::_thesis: v + w = 0. RLS_Real
thus v + w = vr + (- vr) by BINOP_2:def_9
.= 0. RLS_Real ; ::_thesis: verum
end;
thus for a being real number
for v, w being VECTOR of RLS_Real holds a * (v + w) = (a * v) + (a * w) :: according to RLVECT_1:def_5 ::_thesis: ( RLS_Real is scalar-distributive & RLS_Real is scalar-associative & RLS_Real is scalar-unital )
proof
let a be real number ; ::_thesis: for v, w being VECTOR of RLS_Real holds a * (v + w) = (a * v) + (a * w)
reconsider a = a as Real by XREAL_0:def_1;
let v, w be VECTOR of RLS_Real; ::_thesis: a * (v + w) = (a * v) + (a * w)
reconsider vr = v as Real ;
reconsider wr = w as Real ;
A2: a * v = a * vr by BINOP_2:def_11;
A3: a * w = a * wr by BINOP_2:def_11;
v + w = vr + wr by BINOP_2:def_9;
then a * (v + w) = a * (vr + wr) by BINOP_2:def_11
.= (a * vr) + (a * wr)
.= (a * v) + (a * w) by A2, A3, BINOP_2:def_9 ;
hence a * (v + w) = (a * v) + (a * w) ; ::_thesis: verum
end;
thus for a, b being real number
for v being VECTOR of RLS_Real holds (a + b) * v = (a * v) + (b * v) :: according to RLVECT_1:def_6 ::_thesis: ( RLS_Real is scalar-associative & RLS_Real is scalar-unital )
proof
let a, b be real number ; ::_thesis: for v being VECTOR of RLS_Real holds (a + b) * v = (a * v) + (b * v)
reconsider a = a, b = b as Real by XREAL_0:def_1;
let v be VECTOR of RLS_Real; ::_thesis: (a + b) * v = (a * v) + (b * v)
reconsider vr = v as Real ;
A4: b * v = b * vr by BINOP_2:def_11;
a * v = a * vr by BINOP_2:def_11;
then (a * v) + (b * v) = (a * vr) + (b * vr) by A4, BINOP_2:def_9
.= (a + b) * vr
.= (a + b) * v by BINOP_2:def_11 ;
hence (a + b) * v = (a * v) + (b * v) ; ::_thesis: verum
end;
thus for a, b being real number
for v being VECTOR of RLS_Real holds (a * b) * v = a * (b * v) :: according to RLVECT_1:def_7 ::_thesis: RLS_Real is scalar-unital
proof
let a, b be real number ; ::_thesis: for v being VECTOR of RLS_Real holds (a * b) * v = a * (b * v)
reconsider a = a, b = b as Real by XREAL_0:def_1;
let v be VECTOR of RLS_Real; ::_thesis: (a * b) * v = a * (b * v)
reconsider vr = v as Real ;
b * v = b * vr by BINOP_2:def_11;
then a * (b * v) = a * (b * vr) by BINOP_2:def_11
.= (a * b) * vr
.= (a * b) * v by BINOP_2:def_11 ;
hence (a * b) * v = a * (b * v) ; ::_thesis: verum
end;
let v be VECTOR of RLS_Real; :: according to RLVECT_1:def_8 ::_thesis: 1 * v = v
reconsider vr = v as Real ;
thus 1 * v = 1 * vr by BINOP_2:def_11
.= v ; ::_thesis: verum
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
let X be non empty RLSStruct ; ::_thesis: 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)]
let x be VECTOR of X; ::_thesis: 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)]
let u be VECTOR of (Prod_of_RLS (X,RLS_Real)); ::_thesis: for p, w being Real st u = [x,w] holds
p * u = [(p * x),(p * w)]
let p, w be Real; ::_thesis: ( u = [x,w] implies p * u = [(p * x),(p * w)] )
reconsider y = w as VECTOR of RLS_Real ;
assume A1: u = [x,w] ; ::_thesis: p * u = [(p * x),(p * w)]
p * y = p * w by BINOP_2:def_11;
hence p * u = [(p * x),(p * w)] by A1, Def2; ::_thesis: verum
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
let X be non empty RLSStruct ; ::_thesis: 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)]
let x1, x2 be VECTOR of X; ::_thesis: 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)]
let w1, w2 be Real; ::_thesis: 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)]
let u1, u2 be VECTOR of (Prod_of_RLS (X,RLS_Real)); ::_thesis: ( u1 = [x1,w1] & u2 = [x2,w2] implies u1 + u2 = [(x1 + x2),(w1 + w2)] )
reconsider y1 = w1 as VECTOR of RLS_Real ;
reconsider y2 = w2 as VECTOR of RLS_Real ;
assume that
A1: u1 = [x1,w1] and
A2: u2 = [x2,w2] ; ::_thesis: u1 + u2 = [(x1 + x2),(w1 + w2)]
y1 + y2 = w1 + w2 by BINOP_2:def_9;
hence u1 + u2 = [(x1 + x2),(w1 + w2)] by A1, A2, Def1; ::_thesis: verum
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
let a be FinSequence of the carrier of RLS_Real; ::_thesis: 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
let b be FinSequence of REAL ; ::_thesis: ( len a = len b & ( for i being Element of NAT st i in dom a holds
a . i = b . i ) implies Sum a = Sum b )
defpred S1[ Element of NAT ] means for a being FinSequence of the carrier of RLS_Real
for b being FinSequence of REAL st len a = $1 & len b = $1 & ( for i being Element of NAT st i in dom a holds
a . i = b . i ) holds
Sum a = Sum b;
A1: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
thus S1[n + 1] ::_thesis: verum
proof
let a be FinSequence of the carrier of RLS_Real; ::_thesis: for b being FinSequence of REAL st len a = n + 1 & len b = n + 1 & ( for i being Element of NAT st i in dom a holds
a . i = b . i ) holds
Sum a = Sum b
let b be FinSequence of REAL ; ::_thesis: ( len a = n + 1 & len b = n + 1 & ( for i being Element of NAT st i in dom a holds
a . i = b . i ) implies Sum a = Sum b )
assume that
A3: len a = n + 1 and
A4: len b = n + 1 and
A5: for i being Element of NAT st i in dom a holds
a . i = b . i ; ::_thesis: Sum a = Sum b
A6: 0 + n <= 1 + n by XREAL_1:6;
then A7: len (a | n) = n by A3, FINSEQ_1:59;
A8: dom a = Seg (n + 1) by A3, FINSEQ_1:def_3;
A9: for i being Element of NAT st i in Seg (n + 1) holds
( a . i = a /. i & a /. i = b . i )
proof
let i be Element of NAT ; ::_thesis: ( i in Seg (n + 1) implies ( a . i = a /. i & a /. i = b . i ) )
assume A10: i in Seg (n + 1) ; ::_thesis: ( a . i = a /. i & a /. i = b . i )
then A11: i <= n + 1 by FINSEQ_1:1;
1 <= i by A10, FINSEQ_1:1;
then a /. i = a . i by A3, A11, FINSEQ_4:15;
hence ( a . i = a /. i & a /. i = b . i ) by A5, A8, A10; ::_thesis: verum
end;
A12: Seg n c= Seg (n + 1) by A6, FINSEQ_1:5;
A13: for i being Element of NAT st i in dom (a | n) holds
(a | n) . i = (b | n) . i
proof
let i be Element of NAT ; ::_thesis: ( i in dom (a | n) implies (a | n) . i = (b | n) . i )
assume i in dom (a | n) ; ::_thesis: (a | n) . i = (b | n) . i
then A14: i in Seg n by A7, FINSEQ_1:def_3;
then A15: i <= n by FINSEQ_1:1;
then A16: (b | n) . i = b . i by FINSEQ_3:112;
(a | n) . i = a . i by A15, FINSEQ_3:112;
hence (a | n) . i = (b | n) . i by A5, A8, A12, A14, A16; ::_thesis: verum
end;
len (b | n) = n by A4, A6, FINSEQ_1:59;
then A17: Sum (a | n) = Sum (b | n) by A2, A7, A13;
b | n = b | (Seg n) by FINSEQ_1:def_15;
then A18: b = (b | n) ^ <*(b . (n + 1))*> by A4, FINSEQ_3:55;
A19: n + 1 in Seg (n + 1) by FINSEQ_1:4;
then A20: a /. (n + 1) = b . (n + 1) by A9;
a | n = a | (Seg n) by FINSEQ_1:def_15;
then a = (a | n) ^ <*(a . (n + 1))*> by A3, FINSEQ_3:55;
then a = (a | n) ^ <*(a /. (n + 1))*> by A9, A19;
then Sum a = (Sum (a | n)) + (Sum <*(a /. (n + 1))*>) by RLVECT_1:41
.= (Sum (a | n)) + (a /. (n + 1)) by RLVECT_1:44
.= (Sum (b | n)) + (b . (n + 1)) by A17, A20, BINOP_2:def_9 ;
hence Sum a = Sum b by A18, RVSUM_1:74; ::_thesis: verum
end;
end;
A21: S1[ 0 ]
proof
let a be FinSequence of the carrier of RLS_Real; ::_thesis: for b being FinSequence of REAL st len a = 0 & len b = 0 & ( for i being Element of NAT st i in dom a holds
a . i = b . i ) holds
Sum a = Sum b
let b be FinSequence of REAL ; ::_thesis: ( len a = 0 & len b = 0 & ( for i being Element of NAT st i in dom a holds
a . i = b . i ) implies Sum a = Sum b )
assume that
A22: len a = 0 and
A23: len b = 0 and
for i being Element of NAT st i in dom a holds
a . i = b . i ; ::_thesis: Sum a = Sum b
a = <*> the carrier of RLS_Real by A22;
then A24: Sum a = 0. RLS_Real by RLVECT_1:43;
b = <*> REAL by A23;
hence Sum a = Sum b by A24, RVSUM_1:72; ::_thesis: verum
end;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A21, A1);
hence ( len a = len b & ( for i being Element of NAT st i in dom a holds
a . i = b . i ) implies Sum a = Sum b ) ; ::_thesis: verum
end;
begin
Lm4: for F being FinSequence of ExtREAL
for x being Element of ExtREAL holds Sum (F ^ <*x*>) = (Sum F) + x
proof
let F be FinSequence of ExtREAL ; ::_thesis: for x being Element of ExtREAL holds Sum (F ^ <*x*>) = (Sum F) + x
let x be Element of ExtREAL ; ::_thesis: Sum (F ^ <*x*>) = (Sum F) + x
consider f being Function of NAT,ExtREAL such that
A1: Sum (F ^ <*x*>) = f . (len (F ^ <*x*>)) and
A2: f . 0 = 0. and
A3: for i being Element of NAT st i < len (F ^ <*x*>) holds
f . (i + 1) = (f . i) + ((F ^ <*x*>) . (i + 1)) by EXTREAL1:def_2;
A4: len (F ^ <*x*>) = (len F) + (len <*x*>) by FINSEQ_1:22
.= (len F) + 1 by FINSEQ_1:39 ;
for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1))
proof
let i be Element of NAT ; ::_thesis: ( i < len F implies f . (i + 1) = (f . i) + (F . (i + 1)) )
A5: 1 <= i + 1 by NAT_1:11;
assume A6: i < len F ; ::_thesis: f . (i + 1) = (f . i) + (F . (i + 1))
then i + 1 <= len F by INT_1:7;
then i + 1 in Seg (len F) by A5, FINSEQ_1:1;
then A7: i + 1 in dom F by FINSEQ_1:def_3;
i < len (F ^ <*x*>) by A4, A6, NAT_1:13;
then f . (i + 1) = (f . i) + ((F ^ <*x*>) . (i + 1)) by A3;
hence f . (i + 1) = (f . i) + (F . (i + 1)) by A7, FINSEQ_1:def_7; ::_thesis: verum
end;
then A8: Sum F = f . (len F) by A2, EXTREAL1:def_2;
len F < len (F ^ <*x*>) by A4, NAT_1:13;
then f . ((len F) + 1) = (f . (len F)) + ((F ^ <*x*>) . ((len F) + 1)) by A3;
hence Sum (F ^ <*x*>) = (Sum F) + x by A1, A4, A8, FINSEQ_1:42; ::_thesis: verum
end;
Lm5: for F being FinSequence of ExtREAL st not -infty in rng F holds
Sum F <> -infty
proof
defpred S1[ FinSequence of ExtREAL ] means ( not -infty in rng $1 implies Sum $1 <> -infty );
A1: for F being FinSequence of ExtREAL
for x being Element of ExtREAL st S1[F] holds
S1[F ^ <*x*>]
proof
let F be FinSequence of ExtREAL ; ::_thesis: for x being Element of ExtREAL st S1[F] holds
S1[F ^ <*x*>]
let x be Element of ExtREAL ; ::_thesis: ( S1[F] implies S1[F ^ <*x*>] )
assume A2: S1[F] ; ::_thesis: S1[F ^ <*x*>]
A3: Sum (F ^ <*x*>) = (Sum F) + x by Lm4;
assume not -infty in rng (F ^ <*x*>) ; ::_thesis: Sum (F ^ <*x*>) <> -infty
then A4: not -infty in (rng F) \/ (rng <*x*>) by FINSEQ_1:31;
then not -infty in rng <*x*> by XBOOLE_0:def_3;
then not -infty in {x} by FINSEQ_1:38;
then x <> -infty by TARSKI:def_1;
hence Sum (F ^ <*x*>) <> -infty by A2, A4, A3, XBOOLE_0:def_3, XXREAL_3:17; ::_thesis: verum
end;
A5: S1[ <*> ExtREAL] by EXTREAL1:7;
thus for F being FinSequence of ExtREAL holds S1[F] from FINSEQ_2:sch_2(A5, A1); ::_thesis: verum
end;
Lm6: for F being FinSequence of ExtREAL st +infty in rng F & not -infty in rng F holds
Sum F = +infty
proof
defpred S1[ FinSequence of ExtREAL ] means ( +infty in rng $1 & not -infty in rng $1 implies Sum $1 = +infty );
A1: for F being FinSequence of ExtREAL
for x being Element of ExtREAL st S1[F] holds
S1[F ^ <*x*>]
proof
let F be FinSequence of ExtREAL ; ::_thesis: for x being Element of ExtREAL st S1[F] holds
S1[F ^ <*x*>]
let x be Element of ExtREAL ; ::_thesis: ( S1[F] implies S1[F ^ <*x*>] )
assume A2: S1[F] ; ::_thesis: S1[F ^ <*x*>]
assume that
A3: +infty in rng (F ^ <*x*>) and
A4: not -infty in rng (F ^ <*x*>) ; ::_thesis: Sum (F ^ <*x*>) = +infty
A5: Sum (F ^ <*x*>) = (Sum F) + x by Lm4;
+infty in (rng F) \/ (rng <*x*>) by A3, FINSEQ_1:31;
then ( +infty in rng F or +infty in rng <*x*> ) by XBOOLE_0:def_3;
then A6: ( +infty in rng F or +infty in {x} ) by FINSEQ_1:38;
A7: not -infty in (rng F) \/ (rng <*x*>) by A4, FINSEQ_1:31;
then not -infty in rng F by XBOOLE_0:def_3;
then A8: Sum F <> -infty by Lm5;
not -infty in rng <*x*> by A7, XBOOLE_0:def_3;
then not -infty in {x} by FINSEQ_1:38;
then A9: x <> -infty by TARSKI:def_1;
percases ( +infty in rng F or +infty = x ) by A6, TARSKI:def_1;
suppose +infty in rng F ; ::_thesis: Sum (F ^ <*x*>) = +infty
hence Sum (F ^ <*x*>) = +infty by A2, A7, A9, A5, XBOOLE_0:def_3, XXREAL_3:def_2; ::_thesis: verum
end;
suppose +infty = x ; ::_thesis: Sum (F ^ <*x*>) = +infty
hence Sum (F ^ <*x*>) = +infty by A5, A8, XXREAL_3:def_2; ::_thesis: verum
end;
end;
end;
A10: S1[ <*> ExtREAL] ;
thus for F being FinSequence of ExtREAL holds S1[F] from FINSEQ_2:sch_2(A10, A1); ::_thesis: verum
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
let a be FinSequence of ExtREAL ; ::_thesis: 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
let b be FinSequence of REAL ; ::_thesis: ( len a = len b & ( for i being Element of NAT st i in dom a holds
a . i = b . i ) implies Sum a = Sum b )
defpred S1[ Element of NAT ] means for a being FinSequence of ExtREAL
for b being FinSequence of REAL st len a = $1 & len b = $1 & ( for i being Element of NAT st i in dom a holds
a . i = b . i ) holds
Sum a = Sum b;
A1: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
thus S1[n + 1] ::_thesis: verum
proof
let a be FinSequence of ExtREAL ; ::_thesis: for b being FinSequence of REAL st len a = n + 1 & len b = n + 1 & ( for i being Element of NAT st i in dom a holds
a . i = b . i ) holds
Sum a = Sum b
let b be FinSequence of REAL ; ::_thesis: ( len a = n + 1 & len b = n + 1 & ( for i being Element of NAT st i in dom a holds
a . i = b . i ) implies Sum a = Sum b )
assume that
A3: len a = n + 1 and
A4: len b = n + 1 and
A5: for i being Element of NAT st i in dom a holds
a . i = b . i ; ::_thesis: Sum a = Sum b
A6: dom a = Seg (n + 1) by A3, FINSEQ_1:def_3;
then A7: a . (n + 1) = b . (n + 1) by A5, FINSEQ_1:4;
A8: 0 + n <= 1 + n by XREAL_1:6;
then A9: len (a | n) = n by A3, FINSEQ_1:59;
A10: Seg n c= Seg (n + 1) by A8, FINSEQ_1:5;
A11: for i being Element of NAT st i in dom (a | n) holds
(a | n) . i = (b | n) . i
proof
let i be Element of NAT ; ::_thesis: ( i in dom (a | n) implies (a | n) . i = (b | n) . i )
assume i in dom (a | n) ; ::_thesis: (a | n) . i = (b | n) . i
then A12: i in Seg n by A9, FINSEQ_1:def_3;
then A13: i <= n by FINSEQ_1:1;
then A14: (b | n) . i = b . i by FINSEQ_3:112;
(a | n) . i = a . i by A13, FINSEQ_3:112;
hence (a | n) . i = (b | n) . i by A5, A6, A10, A12, A14; ::_thesis: verum
end;
len (b | n) = n by A4, A8, FINSEQ_1:59;
then A15: Sum (a | n) = Sum (b | n) by A2, A9, A11;
b | n = b | (Seg n) by FINSEQ_1:def_15;
then A16: b = (b | n) ^ <*(b . (n + 1))*> by A4, FINSEQ_3:55;
a | n = a | (Seg n) by FINSEQ_1:def_15;
then a = (a | n) ^ <*(a . (n + 1))*> by A3, FINSEQ_3:55;
then Sum a = (Sum (a | n)) + (a . (n + 1)) by Lm4
.= (Sum (b | n)) + (b . (n + 1)) by A15, A7, SUPINF_2:1 ;
hence Sum a = Sum b by A16, RVSUM_1:74; ::_thesis: verum
end;
end;
A17: S1[ 0 ]
proof
let a be FinSequence of ExtREAL ; ::_thesis: for b being FinSequence of REAL st len a = 0 & len b = 0 & ( for i being Element of NAT st i in dom a holds
a . i = b . i ) holds
Sum a = Sum b
let b be FinSequence of REAL ; ::_thesis: ( len a = 0 & len b = 0 & ( for i being Element of NAT st i in dom a holds
a . i = b . i ) implies Sum a = Sum b )
assume that
A18: len a = 0 and
A19: len b = 0 and
for i being Element of NAT st i in dom a holds
a . i = b . i ; ::_thesis: Sum a = Sum b
a = <*> ExtREAL by A18;
then A20: Sum a = 0. by EXTREAL1:7;
b = <*> ExtREAL by A19;
hence Sum a = Sum b by A20, RVSUM_1:72; ::_thesis: verum
end;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A17, A1);
hence ( len a = len b & ( for i being Element of NAT st i in dom a holds
a . i = b . i ) implies Sum a = Sum b ) ; ::_thesis: verum
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
let n be Element of NAT ; ::_thesis: 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
let a be FinSequence of ExtREAL ; ::_thesis: 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
let b be FinSequence of the carrier of RLS_Real; ::_thesis: ( len a = n & len b = n & ( for i being Element of NAT st i in Seg n holds
a . i = b . i ) implies Sum a = Sum b )
assume that
A1: len a = n and
A2: len b = n and
A3: for i being Element of NAT st i in Seg n holds
a . i = b . i ; ::_thesis: Sum a = Sum b
set c = b;
reconsider c = b as FinSequence of REAL ;
dom a = Seg n by A1, FINSEQ_1:def_3;
then A4: Sum a = Sum c by A1, A2, A3, Lm7;
A5: for i being Element of NAT st i in dom b holds
b . i = c . i ;
len b = len c ;
hence Sum a = Sum b by A4, A5, Lm3; ::_thesis: verum
end;
Lm9: for F being FinSequence of ExtREAL st rng F c= {0.} holds
Sum F = 0.
proof
let F be FinSequence of ExtREAL ; ::_thesis: ( rng F c= {0.} implies Sum F = 0. )
defpred S1[ FinSequence of ExtREAL ] means ( rng $1 c= {0.} implies Sum $1 = 0. );
assume A1: rng F c= {0.} ; ::_thesis: Sum F = 0.
A2: for F being FinSequence of ExtREAL
for x being Element of ExtREAL st S1[F] holds
S1[F ^ <*x*>]
proof
let F be FinSequence of ExtREAL ; ::_thesis: for x being Element of ExtREAL st S1[F] holds
S1[F ^ <*x*>]
let x be Element of ExtREAL ; ::_thesis: ( S1[F] implies S1[F ^ <*x*>] )
assume A3: S1[F] ; ::_thesis: S1[F ^ <*x*>]
assume rng (F ^ <*x*>) c= {0.} ; ::_thesis: Sum (F ^ <*x*>) = 0.
then A4: (rng F) \/ (rng <*x*>) c= {0.} by FINSEQ_1:31;
then rng <*x*> c= {0.} by XBOOLE_1:11;
then {x} c= {0.} by FINSEQ_1:38;
then x in {0.} by ZFMISC_1:31;
then A5: x = 0. by TARSKI:def_1;
thus Sum (F ^ <*x*>) = (Sum F) + x by Lm4
.= 0. by A3, A4, A5, XBOOLE_1:11 ; ::_thesis: verum
end;
A6: S1[ <*> ExtREAL] by EXTREAL1:7;
for F being FinSequence of ExtREAL holds S1[F] from FINSEQ_2:sch_2(A6, A2);
hence Sum F = 0. by A1; ::_thesis: verum
end;
Lm10: for F being FinSequence of REAL st rng F c= {0} holds
Sum F = 0
proof
let F be FinSequence of REAL ; ::_thesis: ( rng F c= {0} implies Sum F = 0 )
defpred S1[ FinSequence of REAL ] means ( rng $1 c= {0} implies Sum $1 = 0 );
A1: for F being FinSequence of REAL
for x being Element of REAL st S1[F] holds
S1[F ^ <*x*>]
proof
let F be FinSequence of REAL ; ::_thesis: for x being Element of REAL st S1[F] holds
S1[F ^ <*x*>]
let x be Element of REAL ; ::_thesis: ( S1[F] implies S1[F ^ <*x*>] )
assume A2: S1[F] ; ::_thesis: S1[F ^ <*x*>]
assume rng (F ^ <*x*>) c= {0} ; ::_thesis: Sum (F ^ <*x*>) = 0
then A3: (rng F) \/ (rng <*x*>) c= {0} by FINSEQ_1:31;
then rng <*x*> c= {0} by XBOOLE_1:11;
then {x} c= {0} by FINSEQ_1:38;
then A4: x in {0} by ZFMISC_1:31;
thus Sum (F ^ <*x*>) = (Sum F) + x by RVSUM_1:74
.= 0 by A2, A3, A4, TARSKI:def_1, XBOOLE_1:11 ; ::_thesis: verum
end;
assume A5: rng F c= {0} ; ::_thesis: Sum F = 0
A6: S1[ <*> REAL] by RVSUM_1:72;
for F being FinSequence of REAL holds S1[F] from FINSEQ_2:sch_2(A6, A1);
hence Sum F = 0 by A5; ::_thesis: verum
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
let X be RealLinearSpace; ::_thesis: for F being FinSequence of the carrier of X st rng F c= {(0. X)} holds
Sum F = 0. X
defpred S1[ FinSequence of the carrier of X] means ( rng $1 c= {(0. X)} implies Sum $1 = 0. X );
A1: for F being FinSequence of the carrier of X
for x being Element of X st S1[F] holds
S1[F ^ <*x*>]
proof
let F be FinSequence of the carrier of X; ::_thesis: for x being Element of X st S1[F] holds
S1[F ^ <*x*>]
let x be Element of X; ::_thesis: ( S1[F] implies S1[F ^ <*x*>] )
assume A2: S1[F] ; ::_thesis: S1[F ^ <*x*>]
assume rng (F ^ <*x*>) c= {(0. X)} ; ::_thesis: Sum (F ^ <*x*>) = 0. X
then A3: (rng F) \/ (rng <*x*>) c= {(0. X)} by FINSEQ_1:31;
then rng <*x*> c= {(0. X)} by XBOOLE_1:11;
then {x} c= {(0. X)} by FINSEQ_1:38;
then x in {(0. X)} by ZFMISC_1:31;
then A4: x = 0. X by TARSKI:def_1;
thus Sum (F ^ <*x*>) = (Sum F) + (Sum <*x*>) by RLVECT_1:41
.= (Sum F) + x by RLVECT_1:44
.= 0. X by A2, A3, A4, RLVECT_1:def_4, XBOOLE_1:11 ; ::_thesis: verum
end;
let F be FinSequence of the carrier of X; ::_thesis: ( rng F c= {(0. X)} implies Sum F = 0. X )
assume A5: rng F c= {(0. X)} ; ::_thesis: Sum F = 0. X
A6: S1[ <*> the carrier of X] by RLVECT_1:43;
for F being FinSequence of the carrier of X holds S1[F] from FINSEQ_2:sch_2(A6, A1);
hence Sum F = 0. X by A5; ::_thesis: verum
end;
begin
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 <= 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
deffunc H1( Element of X, Element of REAL ) -> Element of [: the carrier of X,REAL:] = [$1,$2];
defpred S1[ Element of X, Element of REAL ] means f . $1 <= R_EAL $2;
{ H1(x,y) where x is Element of X, y is Element of REAL : S1[x,y] } is Subset of [: the carrier of X,REAL:] from DOMAIN_1:sch_9();
hence { [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)) ; ::_thesis: verum
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 <= R_EAL y } ;
definition
let X be non empty RLSStruct ;
let f be Function of the carrier of X,ExtREAL;
attrf is convex means :Def6: :: CONVFUN1:def 6
epigraph f is convex ;
end;
:: deftheorem Def6 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) = ((R_EAL p1) * w1) + ((R_EAL p2) * w2)
proof
let w1, w2 be R_eal; ::_thesis: 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)
let wr1, wr2, p1, p2 be Real; ::_thesis: ( w1 = wr1 & w2 = wr2 implies (p1 * wr1) + (p2 * wr2) = ((R_EAL p1) * w1) + ((R_EAL p2) * w2) )
assume that
A1: w1 = wr1 and
A2: w2 = wr2 ; ::_thesis: (p1 * wr1) + (p2 * wr2) = ((R_EAL p1) * w1) + ((R_EAL p2) * w2)
A3: p2 * wr2 = (R_EAL p2) * w2 by A2, EXTREAL1:1;
p1 * wr1 = (R_EAL p1) * w1 by A1, EXTREAL1:1;
hence (p1 * wr1) + (p2 * wr2) = ((R_EAL p1) * w1) + ((R_EAL p2) * w2) by A3, SUPINF_2:1; ::_thesis: verum
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)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) )
proof
let X be non empty RLSStruct ; ::_thesis: 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)) )
let f be Function of the carrier of X,ExtREAL; ::_thesis: ( ( for x being VECTOR of X holds f . x <> -infty ) implies ( 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)) ) )
assume A1: for x being VECTOR of X holds f . x <> -infty ; ::_thesis: ( 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)) )
thus ( f is convex implies 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)) ) ::_thesis: ( ( 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)) ) implies f is convex )
proof
assume f is convex ; ::_thesis: 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))
then A2: epigraph f is convex by Def6;
let x1, x2 be VECTOR of X; ::_thesis: 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))
let p be Real; ::_thesis: ( 0 < p & p < 1 implies f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) )
assume that
A3: 0 < p and
A4: p < 1 ; ::_thesis: f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2))
set p2 = R_EAL (1 - p);
set p1 = R_EAL p;
A5: 1 - p > 0 by A4, XREAL_1:50;
percases ( ( f . x1 in REAL & f . x2 in REAL ) or ( f . x1 = +infty & f . x2 in REAL ) or ( f . x1 in REAL & f . x2 = +infty ) or ( f . x1 = +infty & f . x2 = +infty ) ) by A1, XXREAL_0:14;
supposeA6: ( f . x1 in REAL & f . x2 in REAL ) ; ::_thesis: f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2))
then reconsider w2 = f . x2 as Real ;
reconsider w1 = f . x1 as Real by A6;
reconsider u1 = [x1,w1] as VECTOR of (Prod_of_RLS (X,RLS_Real)) ;
reconsider u2 = [x2,w2] as VECTOR of (Prod_of_RLS (X,RLS_Real)) ;
f . x2 <= R_EAL w2 ;
then A7: [x2,w2] in epigraph f ;
A8: p * u1 = [(p * x1),(p * w1)] by Lm1;
A9: (1 - p) * u2 = [((1 - p) * x2),((1 - p) * w2)] by Lm1;
f . x1 <= R_EAL w1 ;
then [x1,w1] in epigraph f ;
then (p * u1) + ((1 - p) * u2) in epigraph f by A2, A3, A4, A7, CONVEX1:def_2;
then [((p * x1) + ((1 - p) * x2)),((p * w1) + ((1 - p) * w2))] in epigraph f by A8, A9, Lm2;
then consider x0 being Element of X, y0 being Element of REAL such that
A10: [((p * x1) + ((1 - p) * x2)),((p * w1) + ((1 - p) * w2))] = [x0,y0] and
A11: f . x0 <= R_EAL y0 ;
A12: y0 = (p * w1) + ((1 - p) * w2) by A10, XTUPLE_0:1;
x0 = (p * x1) + ((1 - p) * x2) by A10, XTUPLE_0:1;
hence f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by A11, A12, Lm12; ::_thesis: verum
end;
supposeA13: ( f . x1 = +infty & f . x2 in REAL ) ; ::_thesis: f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2))
A14: (R_EAL (1 - p)) * (f . x2) in REAL
proof
reconsider w2 = f . x2 as Real by A13;
(R_EAL (1 - p)) * (f . x2) = (1 - p) * w2 by EXTREAL1:1;
hence (R_EAL (1 - p)) * (f . x2) in REAL ; ::_thesis: verum
end;
(R_EAL p) * (f . x1) = +infty by A3, A13, XXREAL_3:def_5;
then ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) = +infty by A14, XXREAL_3:def_2;
hence f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by XXREAL_0:4; ::_thesis: verum
end;
supposeA15: ( f . x1 in REAL & f . x2 = +infty ) ; ::_thesis: f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2))
A16: (R_EAL p) * (f . x1) in REAL
proof
reconsider w1 = f . x1 as Real by A15;
(R_EAL p) * (f . x1) = p * w1 by EXTREAL1:1;
hence (R_EAL p) * (f . x1) in REAL ; ::_thesis: verum
end;
(R_EAL (1 - p)) * (f . x2) = +infty by A5, A15, XXREAL_3:def_5;
then ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) = +infty by A16, XXREAL_3:def_2;
hence f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by XXREAL_0:4; ::_thesis: verum
end;
supposeA17: ( f . x1 = +infty & f . x2 = +infty ) ; ::_thesis: f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2))
then (R_EAL (1 - p)) * (f . x2) = +infty by A5, XXREAL_3:def_5;
then ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) = +infty by A3, A17, XXREAL_3:def_2;
hence f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by XXREAL_0:4; ::_thesis: verum
end;
end;
end;
assume A18: 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)) ; ::_thesis: f is convex
for u1, u2 being VECTOR of (Prod_of_RLS (X,RLS_Real))
for p being Real st 0 < p & p < 1 & u1 in epigraph f & u2 in epigraph f holds
(p * u1) + ((1 - p) * u2) in epigraph f
proof
let u1, u2 be VECTOR of (Prod_of_RLS (X,RLS_Real)); ::_thesis: for p being Real st 0 < p & p < 1 & u1 in epigraph f & u2 in epigraph f holds
(p * u1) + ((1 - p) * u2) in epigraph f
let p be Real; ::_thesis: ( 0 < p & p < 1 & u1 in epigraph f & u2 in epigraph f implies (p * u1) + ((1 - p) * u2) in epigraph f )
assume that
A19: 0 < p and
A20: p < 1 and
A21: u1 in epigraph f and
A22: u2 in epigraph f ; ::_thesis: (p * u1) + ((1 - p) * u2) in epigraph f
thus (p * u1) + ((1 - p) * u2) in epigraph f ::_thesis: verum
proof
consider x2 being Element of X, y2 being Element of REAL such that
A23: u2 = [x2,y2] and
A24: f . x2 <= R_EAL y2 by A22;
A25: (1 - p) * u2 = [((1 - p) * x2),((1 - p) * y2)] by A23, Lm1;
f . x2 <> +infty by A24, XXREAL_0:9;
then reconsider w2 = f . x2 as Real by A1, XXREAL_0:14;
consider x1 being Element of X, y1 being Element of REAL such that
A26: u1 = [x1,y1] and
A27: f . x1 <= R_EAL y1 by A21;
f . x1 <> +infty by A27, XXREAL_0:9;
then reconsider w1 = f . x1 as Real by A1, XXREAL_0:14;
1 - p > 0 by A20, XREAL_1:50;
then (1 - p) * w2 <= (1 - p) * y2 by A24, XREAL_1:64;
then A28: (p * w1) + ((1 - p) * w2) <= (p * w1) + ((1 - p) * y2) by XREAL_1:6;
p * w1 <= p * y1 by A19, A27, XREAL_1:64;
then (p * w1) + ((1 - p) * y2) <= (p * y1) + ((1 - p) * y2) by XREAL_1:6;
then A29: (p * w1) + ((1 - p) * w2) <= (p * y1) + ((1 - p) * y2) by A28, XXREAL_0:2;
A30: R_EAL ((p * w1) + ((1 - p) * w2)) = ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by Lm12;
then f . ((p * x1) + ((1 - p) * x2)) <> +infty by A18, A19, A20, XXREAL_0:9;
then reconsider w = f . ((p * x1) + ((1 - p) * x2)) as Real by A1, XXREAL_0:14;
w <= (p * w1) + ((1 - p) * w2) by A18, A19, A20, A30;
then f . ((p * x1) + ((1 - p) * x2)) <= R_EAL ((p * y1) + ((1 - p) * y2)) by A29, XXREAL_0:2;
then A31: [((p * x1) + ((1 - p) * x2)),((p * y1) + ((1 - p) * y2))] in { [x,y] where x is Element of X, y is Element of REAL : f . x <= R_EAL y } ;
p * u1 = [(p * x1),(p * y1)] by A26, Lm1;
hence (p * u1) + ((1 - p) * u2) in epigraph f by A31, A25, Lm2; ::_thesis: verum
end;
end;
then epigraph f is convex by CONVEX1:def_2;
hence f is convex by Def6; ::_thesis: verum
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)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) )
proof
let X be RealLinearSpace; ::_thesis: 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)) )
let f be Function of the carrier of X,ExtREAL; ::_thesis: ( ( for x being VECTOR of X holds f . x <> -infty ) implies ( 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)) ) )
assume A1: for x being VECTOR of X holds f . x <> -infty ; ::_thesis: ( 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)) )
thus ( f is convex implies 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)) ) ::_thesis: ( ( 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)) ) implies f is convex )
proof
assume A2: f is convex ; ::_thesis: 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))
let x1, x2 be VECTOR of X; ::_thesis: 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))
let p be Real; ::_thesis: ( 0 <= p & p <= 1 implies f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) )
assume that
A3: 0 <= p and
A4: p <= 1 ; ::_thesis: f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2))
percases ( p = 0 or p = 1 or ( p <> 0 & p <> 1 ) ) ;
supposeA5: p = 0 ; ::_thesis: f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2))
then A6: (1 - p) * x2 = x2 by RLVECT_1:def_8;
p * x1 = 0. X by A5, RLVECT_1:10;
then A7: (p * x1) + ((1 - p) * x2) = x2 by A6, RLVECT_1:4;
A8: (R_EAL (1 - p)) * (f . x2) = f . x2 by A5, XXREAL_3:81;
(R_EAL p) * (f . x1) = 0. by A5;
hence f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by A7, A8, XXREAL_3:4; ::_thesis: verum
end;
supposeA9: p = 1 ; ::_thesis: f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2))
then A10: (1 - p) * x2 = 0. X by RLVECT_1:10;
p * x1 = x1 by A9, RLVECT_1:def_8;
then A11: (p * x1) + ((1 - p) * x2) = x1 by A10, RLVECT_1:4;
A12: (R_EAL p) * (f . x1) = f . x1 by A9, XXREAL_3:81;
(R_EAL (1 - p)) * (f . x2) = 0. by A9;
hence f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by A11, A12, XXREAL_3:4; ::_thesis: verum
end;
supposeA13: ( p <> 0 & p <> 1 ) ; ::_thesis: f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2))
then p < 1 by A4, XXREAL_0:1;
hence f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by A1, A2, A3, A13, Th4; ::_thesis: verum
end;
end;
end;
assume 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)) ; ::_thesis: f is convex
then 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)) ;
hence f is convex by A1, Th4; ::_thesis: verum
end;
begin
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
let f be PartFunc of REAL,REAL; ::_thesis: 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 ) )
let g be Function of the carrier of RLS_Real,ExtREAL; ::_thesis: 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 ) )
let X be Subset of RLS_Real; ::_thesis: ( 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 ) ) ) implies ( g is convex iff ( f is_convex_on X & X is convex ) ) )
assume that
A1: X c= dom f and
A2: for x being Real holds
( ( x in X implies g . x = f . x ) & ( not x in X implies g . x = +infty ) ) ; ::_thesis: ( g is convex iff ( f is_convex_on X & X is convex ) )
A3: for v being VECTOR of RLS_Real holds g . v <> -infty
proof
let v be VECTOR of RLS_Real; ::_thesis: g . v <> -infty
reconsider x = v as Real ;
f . x in REAL ;
hence g . v <> -infty by A2; ::_thesis: verum
end;
A4: for v being VECTOR of RLS_Real st v in X holds
g . v in REAL
proof
let v be VECTOR of RLS_Real; ::_thesis: ( v in X implies g . v in REAL )
reconsider x = v as Real ;
assume v in X ; ::_thesis: g . v in REAL
then g . x = f . x by A2;
hence g . v in REAL ; ::_thesis: verum
end;
thus ( g is convex implies ( f is_convex_on X & X is convex ) ) ::_thesis: ( f is_convex_on X & X is convex implies g is convex )
proof
assume A5: g is convex ; ::_thesis: ( f is_convex_on X & X is convex )
for p being Real st 0 <= p & p <= 1 holds
for x1, x2 being Real st x1 in X & x2 in X & (p * x1) + ((1 - p) * x2) in X holds
f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2))
proof
let p be Real; ::_thesis: ( 0 <= p & p <= 1 implies for x1, x2 being Real st x1 in X & x2 in X & (p * x1) + ((1 - p) * x2) in X holds
f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) )
assume that
A6: 0 <= p and
A7: p <= 1 ; ::_thesis: for x1, x2 being Real st x1 in X & x2 in X & (p * x1) + ((1 - p) * x2) in X holds
f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2))
let x1, x2 be Real; ::_thesis: ( x1 in X & x2 in X & (p * x1) + ((1 - p) * x2) in X implies f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) )
assume that
A8: x1 in X and
A9: x2 in X and
A10: (p * x1) + ((1 - p) * x2) in X ; ::_thesis: f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2))
A11: f . x1 = g . x1 by A2, A8;
A12: f . ((p * x1) + ((1 - p) * x2)) = g . ((p * x1) + ((1 - p) * x2)) by A2, A10;
A13: f . x2 = g . x2 by A2, A9;
percases ( p = 0 or p = 1 or ( p <> 0 & p <> 1 ) ) ;
suppose p = 0 ; ::_thesis: f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2))
hence f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) ; ::_thesis: verum
end;
suppose p = 1 ; ::_thesis: f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2))
hence f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) ; ::_thesis: verum
end;
supposeA14: ( p <> 0 & p <> 1 ) ; ::_thesis: f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2))
reconsider v2 = x2 as VECTOR of RLS_Real ;
reconsider v1 = x1 as VECTOR of RLS_Real ;
A15: (1 - p) * v2 = (1 - p) * x2 by BINOP_2:def_11;
p * v1 = p * x1 by BINOP_2:def_11;
then A16: g . ((p * v1) + ((1 - p) * v2)) = f . ((p * x1) + ((1 - p) * x2)) by A12, A15, BINOP_2:def_9;
A17: p < 1 by A7, A14, XXREAL_0:1;
(p * (f . v1)) + ((1 - p) * (f . v2)) = ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by A11, A13, Lm12;
hence f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) by A3, A5, A6, A14, A17, A16, Th4; ::_thesis: verum
end;
end;
end;
hence f is_convex_on X by A1, RFUNCT_3:def_12; ::_thesis: X is convex
for v1, v2 being VECTOR of RLS_Real
for p being Real st 0 < p & p < 1 & v1 in X & v2 in X holds
(p * v1) + ((1 - p) * v2) in X
proof
let v1, v2 be VECTOR of RLS_Real; ::_thesis: for p being Real st 0 < p & p < 1 & v1 in X & v2 in X holds
(p * v1) + ((1 - p) * v2) in X
let p be Real; ::_thesis: ( 0 < p & p < 1 & v1 in X & v2 in X implies (p * v1) + ((1 - p) * v2) in X )
assume that
A18: 0 < p and
A19: p < 1 and
A20: v1 in X and
A21: v2 in X ; ::_thesis: (p * v1) + ((1 - p) * v2) in X
reconsider w1 = g . v1, w2 = g . v2 as Real by A4, A20, A21;
A22: (p * w1) + ((1 - p) * w2) = ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by Lm12;
g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by A3, A5, A18, A19, Th4;
then g . ((p * v1) + ((1 - p) * v2)) <> +infty by A22, XXREAL_0:9;
hence (p * v1) + ((1 - p) * v2) in X by A2; ::_thesis: verum
end;
hence X is convex by CONVEX1:def_2; ::_thesis: verum
end;
thus ( f is_convex_on X & X is convex implies g is convex ) ::_thesis: verum
proof
assume that
A23: f is_convex_on X and
A24: X is convex ; ::_thesis: g is convex
for v1, v2 being VECTOR of RLS_Real
for p being Real st 0 < p & p < 1 holds
g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2))
proof
let v1, v2 be VECTOR of RLS_Real; ::_thesis: for p being Real st 0 < p & p < 1 holds
g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2))
let p be Real; ::_thesis: ( 0 < p & p < 1 implies g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) )
assume that
A25: 0 < p and
A26: p < 1 ; ::_thesis: g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2))
reconsider x2 = v2 as Real ;
reconsider x1 = v1 as Real ;
A27: 1 - p > 0 by A26, XREAL_1:50;
percases ( ( v1 in X & v2 in X ) or ( v1 in X & not v2 in X ) or ( not v1 in X & v2 in X ) or ( not v1 in X & not v2 in X ) ) ;
supposeA28: ( v1 in X & v2 in X ) ; ::_thesis: g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2))
then A29: f . x2 = g . v2 by A2;
f . x1 = g . v1 by A2, A28;
then A30: (p * (f . x1)) + ((1 - p) * (f . x2)) = ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by A29, Lm12;
A31: (1 - p) * v2 = (1 - p) * x2 by BINOP_2:def_11;
p * v1 = p * x1 by BINOP_2:def_11;
then A32: (p * v1) + ((1 - p) * v2) = (p * x1) + ((1 - p) * x2) by A31, BINOP_2:def_9;
A33: (p * v1) + ((1 - p) * v2) in X by A24, A25, A26, A28, CONVEX1:def_2;
then f . ((p * x1) + ((1 - p) * x2)) = g . ((p * v1) + ((1 - p) * v2)) by A2, A32;
hence g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by A23, A25, A26, A28, A33, A32, A30, RFUNCT_3:def_12; ::_thesis: verum
end;
supposeA34: ( v1 in X & not v2 in X ) ; ::_thesis: g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2))
then g . x2 = +infty by A2;
then A35: (R_EAL (1 - p)) * (g . v2) = +infty by A27, XXREAL_3:def_5;
reconsider w1 = g . x1 as Real by A4, A34;
p * w1 = (R_EAL p) * (g . v1) by EXTREAL1:1;
then ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) = +infty by A35, XXREAL_3:def_2;
hence g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by XXREAL_0:4; ::_thesis: verum
end;
supposeA36: ( not v1 in X & v2 in X ) ; ::_thesis: g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2))
then g . x1 = +infty by A2;
then A37: (R_EAL p) * (g . v1) = +infty by A25, XXREAL_3:def_5;
reconsider w2 = g . x2 as Real by A4, A36;
(1 - p) * w2 = (R_EAL (1 - p)) * (g . v2) by EXTREAL1:1;
then ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) = +infty by A37, XXREAL_3:def_2;
hence g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by XXREAL_0:4; ::_thesis: verum
end;
supposeA38: ( not v1 in X & not v2 in X ) ; ::_thesis: g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2))
then g . x2 = +infty by A2;
then A39: (R_EAL (1 - p)) * (g . v2) = +infty by A27, XXREAL_3:def_5;
g . x1 = +infty by A2, A38;
then ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) = +infty by A25, A39, XXREAL_3:def_2;
hence g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by XXREAL_0:4; ::_thesis: verum
end;
end;
end;
hence g is convex by A3, Th4; ::_thesis: verum
end;
end;
begin
theorem Th7: :: CONVFUN1:7
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
let X be RealLinearSpace; ::_thesis: 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 )
let M be Subset of X; ::_thesis: ( 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 )
thus ( M is convex implies 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 ) ::_thesis: ( ( 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 ) implies M is convex )
proof
defpred S1[ Nat] means for p being FinSequence of REAL
for y, z being FinSequence of the carrier of X st len p = $1 & len y = $1 & len z = $1 & Sum p = 1 & ( for i being Nat st i in Seg $1 holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) holds
Sum z in M;
assume A1: M is convex ; ::_thesis: 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
A2: for n being non empty Nat st S1[n] holds
S1[n + 1]
proof
let n be non empty Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A3: S1[n] ; ::_thesis: S1[n + 1]
thus for p being FinSequence of REAL
for y, z being FinSequence of the carrier of X st len p = n + 1 & len y = n + 1 & len z = n + 1 & Sum p = 1 & ( for i being Nat st i in Seg (n + 1) holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) holds
Sum z in M ::_thesis: verum
proof
let p be FinSequence of REAL ; ::_thesis: for y, z being FinSequence of the carrier of X st len p = n + 1 & len y = n + 1 & len z = n + 1 & Sum p = 1 & ( for i being Nat st i in Seg (n + 1) holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) holds
Sum z in M
let y, z be FinSequence of the carrier of X; ::_thesis: ( len p = n + 1 & len y = n + 1 & len z = n + 1 & Sum p = 1 & ( for i being Nat st i in Seg (n + 1) holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) implies Sum z in M )
assume that
A4: len p = n + 1 and
A5: len y = n + 1 and
A6: len z = n + 1 and
A7: Sum p = 1 and
A8: for i being Nat st i in Seg (n + 1) holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ; ::_thesis: Sum z in M
set q = 1 - (p . (n + 1));
A9: dom (p | n) = Seg (len (p | n)) by FINSEQ_1:def_3;
1 <= n + 1 by NAT_1:14;
then 1 in Seg (n + 1) by FINSEQ_1:1;
then p . 1 > 0 by A8;
then A10: (p | n) . 1 > 0 by FINSEQ_3:112, NAT_1:14;
p | n = p | (Seg n) by FINSEQ_1:def_15;
then p = (p | n) ^ <*(p . (n + 1))*> by A4, FINSEQ_3:55;
then A11: 1 = (Sum (p | n)) + (p . (n + 1)) by A7, RVSUM_1:74;
A12: 0 + n <= 1 + n by XREAL_1:6;
then A13: len (p | n) = n by A4, FINSEQ_1:59;
then A14: dom (p | n) = Seg n by FINSEQ_1:def_3;
A15: Seg n c= Seg (n + 1) by A12, FINSEQ_1:5;
A16: for i being Nat st i in dom (p | n) holds
0 <= (p | n) . i
proof
let i be Nat; ::_thesis: ( i in dom (p | n) implies 0 <= (p | n) . i )
assume A17: i in dom (p | n) ; ::_thesis: 0 <= (p | n) . i
then A18: i <= n by A14, FINSEQ_1:1;
p . i > 0 by A8, A14, A15, A17;
hence 0 <= (p | n) . i by A18, FINSEQ_3:112; ::_thesis: verum
end;
set y9 = y | n;
set p9 = (1 / (1 - (p . (n + 1)))) * (p | n);
deffunc H1( Nat) -> Element of the carrier of X = (((1 / (1 - (p . (n + 1)))) * (p | n)) . $1) * ((y | n) /. $1);
consider z9 being FinSequence of the carrier of X such that
A19: len z9 = n and
A20: for i being Nat st i in dom z9 holds
z9 . i = H1(i) from FINSEQ_2:sch_1();
A21: len (y | n) = n by A5, A12, FINSEQ_1:59;
then A22: dom (y | n) = Seg n by FINSEQ_1:def_3;
A23: for i being Element of NAT
for v being VECTOR of X st i in dom z9 & v = (z | n) . i holds
z9 . i = (1 / (1 - (p . (n + 1)))) * v
proof
let i be Element of NAT ; ::_thesis: for v being VECTOR of X st i in dom z9 & v = (z | n) . i holds
z9 . i = (1 / (1 - (p . (n + 1)))) * v
let v be VECTOR of X; ::_thesis: ( i in dom z9 & v = (z | n) . i implies z9 . i = (1 / (1 - (p . (n + 1)))) * v )
assume that
A24: i in dom z9 and
A25: v = (z | n) . i ; ::_thesis: z9 . i = (1 / (1 - (p . (n + 1)))) * v
A26: i in Seg n by A19, A24, FINSEQ_1:def_3;
then A27: (y | n) /. i = y /. i by A22, FINSEQ_4:70;
A28: i <= n by A26, FINSEQ_1:1;
then A29: (z | n) . i = z . i by FINSEQ_3:112;
z9 . i = (((1 / (1 - (p . (n + 1)))) * (p | n)) . i) * ((y | n) /. i) by A20, A24
.= ((1 / (1 - (p . (n + 1)))) * ((p | n) . i)) * ((y | n) /. i) by RVSUM_1:44
.= ((1 / (1 - (p . (n + 1)))) * (p . i)) * ((y | n) /. i) by A28, FINSEQ_3:112
.= (1 / (1 - (p . (n + 1)))) * ((p . i) * ((y | n) /. i)) by RLVECT_1:def_7
.= (1 / (1 - (p . (n + 1)))) * v by A8, A15, A25, A26, A29, A27 ;
hence z9 . i = (1 / (1 - (p . (n + 1)))) * v ; ::_thesis: verum
end;
1 <= n by NAT_1:14;
then 1 in Seg n by FINSEQ_1:1;
then A30: 1 - (p . (n + 1)) > 0 by A11, A14, A16, A10, RVSUM_1:85;
dom ((1 / (1 - (p . (n + 1)))) * (p | n)) = Seg (len ((1 / (1 - (p . (n + 1)))) * (p | n))) by FINSEQ_1:def_3;
then Seg (len ((1 / (1 - (p . (n + 1)))) * (p | n))) = Seg (len (p | n)) by A9, VALUED_1:def_5;
then A31: len ((1 / (1 - (p . (n + 1)))) * (p | n)) = n by A13, FINSEQ_1:6;
A32: n + 1 in Seg (n + 1) by FINSEQ_1:4;
then A33: y /. (n + 1) in M by A8;
A34: 1 - (p . (n + 1)) < 1 by A8, A32, XREAL_1:44;
z | n = z | (Seg n) by FINSEQ_1:def_15;
then A35: z = (z | n) ^ <*(z . (n + 1))*> by A6, FINSEQ_3:55;
z . (n + 1) = (p . (n + 1)) * (y /. (n + 1)) by A8, A32;
then A36: Sum z = (Sum (z | n)) + (Sum <*((p . (n + 1)) * (y /. (n + 1)))*>) by A35, RLVECT_1:41
.= (Sum (z | n)) + ((1 - (1 - (p . (n + 1)))) * (y /. (n + 1))) by RLVECT_1:44 ;
A37: dom z9 = Seg n by A19, FINSEQ_1:def_3;
A38: for i being Nat st i in Seg n holds
( ((1 / (1 - (p . (n + 1)))) * (p | n)) . i > 0 & z9 . i = (((1 / (1 - (p . (n + 1)))) * (p | n)) . i) * ((y | n) /. i) & (y | n) /. i in M )
proof
(1 - (p . (n + 1))) " > 0 by A30;
then A39: 1 / (1 - (p . (n + 1))) > 0 by XCMPLX_1:215;
let i be Nat; ::_thesis: ( i in Seg n implies ( ((1 / (1 - (p . (n + 1)))) * (p | n)) . i > 0 & z9 . i = (((1 / (1 - (p . (n + 1)))) * (p | n)) . i) * ((y | n) /. i) & (y | n) /. i in M ) )
assume A40: i in Seg n ; ::_thesis: ( ((1 / (1 - (p . (n + 1)))) * (p | n)) . i > 0 & z9 . i = (((1 / (1 - (p . (n + 1)))) * (p | n)) . i) * ((y | n) /. i) & (y | n) /. i in M )
then A41: i <= n by FINSEQ_1:1;
A42: ((1 / (1 - (p . (n + 1)))) * (p | n)) . i = (1 / (1 - (p . (n + 1)))) * ((p | n) . i) by RVSUM_1:44
.= (1 / (1 - (p . (n + 1)))) * (p . i) by A41, FINSEQ_3:112 ;
A43: Seg n c= Seg (n + 1) by A12, FINSEQ_1:5;
then p . i > 0 by A8, A40;
hence ((1 / (1 - (p . (n + 1)))) * (p | n)) . i > 0 by A39, A42, XREAL_1:129; ::_thesis: ( z9 . i = (((1 / (1 - (p . (n + 1)))) * (p | n)) . i) * ((y | n) /. i) & (y | n) /. i in M )
thus z9 . i = (((1 / (1 - (p . (n + 1)))) * (p | n)) . i) * ((y | n) /. i) by A20, A37, A40; ::_thesis: (y | n) /. i in M
y /. i in M by A8, A40, A43;
hence (y | n) /. i in M by A22, A40, FINSEQ_4:70; ::_thesis: verum
end;
len (z | n) = n by A6, A12, FINSEQ_1:59;
then A44: (1 - (p . (n + 1))) * (Sum z9) = (1 - (p . (n + 1))) * ((1 / (1 - (p . (n + 1)))) * (Sum (z | n))) by A19, A23, RLVECT_1:39
.= ((1 - (p . (n + 1))) * (1 / (1 - (p . (n + 1))))) * (Sum (z | n)) by RLVECT_1:def_7
.= 1 * (Sum (z | n)) by A30, XCMPLX_1:106
.= Sum (z | n) by RLVECT_1:def_8 ;
Sum ((1 / (1 - (p . (n + 1)))) * (p | n)) = (1 / (1 - (p . (n + 1)))) * (1 - (p . (n + 1))) by A11, RVSUM_1:87
.= 1 by A30, XCMPLX_1:106 ;
then Sum z9 in M by A3, A19, A31, A21, A38;
hence Sum z in M by A1, A33, A34, A30, A36, A44, CONVEX1:def_2; ::_thesis: verum
end;
end;
A45: S1[1]
proof
let p be FinSequence of REAL ; ::_thesis: for y, z being FinSequence of the carrier of X st len p = 1 & len y = 1 & len z = 1 & Sum p = 1 & ( for i being Nat st i in Seg 1 holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) holds
Sum z in M
let y, z be FinSequence of the carrier of X; ::_thesis: ( len p = 1 & len y = 1 & len z = 1 & Sum p = 1 & ( for i being Nat st i in Seg 1 holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) implies Sum z in M )
assume that
A46: len p = 1 and
len y = 1 and
A47: len z = 1 and
A48: Sum p = 1 and
A49: for i being Nat st i in Seg 1 holds
( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ; ::_thesis: Sum z in M
p = <*(p . 1)*> by A46, FINSEQ_1:40;
then A50: p . 1 = 1 by A48, FINSOP_1:11;
A51: 1 in Seg 1 by FINSEQ_1:2, TARSKI:def_1;
then z . 1 = (p . 1) * (y /. 1) by A49;
then A52: z . 1 = y /. 1 by A50, RLVECT_1:def_8;
A53: z = <*(z . 1)*> by A47, FINSEQ_1:40;
y /. 1 in M by A49, A51;
hence Sum z in M by A53, A52, RLVECT_1:44; ::_thesis: verum
end;
thus for n being non empty Nat holds S1[n] from NAT_1:sch_10(A45, A2); ::_thesis: verum
end;
thus ( ( 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 ) implies M is convex ) ::_thesis: verum
proof
assume A54: 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 ; ::_thesis: M is convex
for x1, x2 being VECTOR of X
for r being Real st 0 < r & r < 1 & x1 in M & x2 in M holds
(r * x1) + ((1 - r) * x2) in M
proof
let x1, x2 be VECTOR of X; ::_thesis: for r being Real st 0 < r & r < 1 & x1 in M & x2 in M holds
(r * x1) + ((1 - r) * x2) in M
let r be Real; ::_thesis: ( 0 < r & r < 1 & x1 in M & x2 in M implies (r * x1) + ((1 - r) * x2) in M )
assume that
A55: 0 < r and
A56: r < 1 and
A57: x1 in M and
A58: x2 in M ; ::_thesis: (r * x1) + ((1 - r) * x2) in M
set z = <*(r * x1),((1 - r) * x2)*>;
set y = <*x1,x2*>;
set p = <*r,(1 - r)*>;
A59: for i being Nat st i in Seg 2 holds
( <*r,(1 - r)*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,(1 - r)*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M )
proof
let i be Nat; ::_thesis: ( i in Seg 2 implies ( <*r,(1 - r)*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,(1 - r)*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M ) )
assume A60: i in Seg 2 ; ::_thesis: ( <*r,(1 - r)*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,(1 - r)*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M )
percases ( i = 1 or i = 2 ) by A60, FINSEQ_1:2, TARSKI:def_2;
supposeA61: i = 1 ; ::_thesis: ( <*r,(1 - r)*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,(1 - r)*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M )
then A62: <*x1,x2*> /. i = x1 by FINSEQ_4:17;
<*r,(1 - r)*> . i = r by A61, FINSEQ_1:44;
hence ( <*r,(1 - r)*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,(1 - r)*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M ) by A55, A57, A61, A62, FINSEQ_1:44; ::_thesis: verum
end;
supposeA63: i = 2 ; ::_thesis: ( <*r,(1 - r)*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,(1 - r)*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M )
then A64: <*x1,x2*> /. i = x2 by FINSEQ_4:17;
<*r,(1 - r)*> . i = 1 - r by A63, FINSEQ_1:44;
hence ( <*r,(1 - r)*> . i > 0 & <*(r * x1),((1 - r) * x2)*> . i = (<*r,(1 - r)*> . i) * (<*x1,x2*> /. i) & <*x1,x2*> /. i in M ) by A56, A58, A63, A64, FINSEQ_1:44, XREAL_1:50; ::_thesis: verum
end;
end;
end;
A65: len <*x1,x2*> = 2 by FINSEQ_1:44;
A66: Sum <*r,(1 - r)*> = r + (1 - r) by RVSUM_1:77
.= 1 ;
A67: len <*(r * x1),((1 - r) * x2)*> = 2 by FINSEQ_1:44;
len <*r,(1 - r)*> = 2 by FINSEQ_1:44;
then Sum <*(r * x1),((1 - r) * x2)*> in M by A54, A65, A67, A66, A59;
hence (r * x1) + ((1 - r) * x2) in M by RLVECT_1:45; ::_thesis: verum
end;
hence M is convex by CONVEX1:def_2; ::_thesis: verum
end;
end;
begin
Lm13: for X being RealLinearSpace
for f being Function of the carrier of X,ExtREAL
for n being non empty 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
not -infty in rng F
proof
let X be RealLinearSpace; ::_thesis: for f being Function of the carrier of X,ExtREAL
for n being non empty 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
not -infty in rng F
let f be Function of the carrier of X,ExtREAL; ::_thesis: for n being non empty 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
not -infty in rng F
let n be non empty Element of NAT ; ::_thesis: 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
not -infty in rng F
let p be FinSequence of REAL ; ::_thesis: 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
not -infty in rng F
let F be FinSequence of ExtREAL ; ::_thesis: 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
not -infty in rng F
let y be FinSequence of the carrier of X; ::_thesis: ( 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) implies not -infty in rng F )
assume that
A1: len F = n and
A2: for x being VECTOR of X holds f . x <> -infty and
A3: for i being Element of NAT st i in Seg n holds
( p . i >= 0 & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ; ::_thesis: not -infty in rng F
for i being set st i in dom F holds
F . i <> -infty
proof
let i be set ; ::_thesis: ( i in dom F implies F . i <> -infty )
assume A4: i in dom F ; ::_thesis: F . i <> -infty
then reconsider i = i as Element of NAT ;
A5: i in Seg n by A1, A4, FINSEQ_1:def_3;
then A6: p . i >= 0 by A3;
A7: F . i = (R_EAL (p . i)) * (f . (y /. i)) by A3, A5;
percases ( R_EAL (p . i) = 0. or f . (y /. i) <> +infty or ( R_EAL (p . i) <> 0. & f . (y /. i) = +infty ) ) ;
suppose R_EAL (p . i) = 0. ; ::_thesis: F . i <> -infty
hence F . i <> -infty by A7; ::_thesis: verum
end;
suppose f . (y /. i) <> +infty ; ::_thesis: F . i <> -infty
then reconsider w = f . (y /. i) as Real by A2, XXREAL_0:14;
F . i = (p . i) * w by A7, EXTREAL1:1;
hence F . i <> -infty ; ::_thesis: verum
end;
suppose ( R_EAL (p . i) <> 0. & f . (y /. i) = +infty ) ; ::_thesis: F . i <> -infty
hence F . i <> -infty by A6, A7; ::_thesis: verum
end;
end;
end;
hence not -infty in rng F by FUNCT_1:def_3; ::_thesis: verum
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 empty 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F )
proof
let X be RealLinearSpace; ::_thesis: 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 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F )
let f be Function of the carrier of X,ExtREAL; ::_thesis: ( ( for x being VECTOR of X holds f . x <> -infty ) implies ( f is convex iff for n being non empty 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F ) )
assume A1: for x being VECTOR of X holds f . x <> -infty ; ::_thesis: ( f is convex iff for n being non empty 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F )
thus ( f is convex implies for n being non empty 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F ) ::_thesis: ( ( for n being non empty 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F ) implies f is convex )
proof
assume A2: f is convex ; ::_thesis: for n being non empty 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F
let n be non empty Element of NAT ; ::_thesis: 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F
let p be FinSequence of REAL ; ::_thesis: 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F
let F be FinSequence of ExtREAL ; ::_thesis: 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F
let y, z be FinSequence of the carrier of X; ::_thesis: ( 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) implies f . (Sum z) <= Sum F )
assume that
A3: len p = n and
A4: len F = n and
len y = n and
A5: len z = n and
A6: Sum p = 1 and
A7: for i being Element of 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)) ) ; ::_thesis: f . (Sum z) <= Sum F
for i being Element of NAT st i in Seg n holds
( p . i >= 0 & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) by A7;
then A8: not -infty in rng F by A1, A4, Lm13;
percases ( for i being Element of NAT st i in Seg n holds
f . (y /. i) <> +infty or ex i being Element of NAT st
( i in Seg n & f . (y /. i) = +infty ) ) ;
supposeA9: for i being Element of NAT st i in Seg n holds
f . (y /. i) <> +infty ; ::_thesis: f . (Sum z) <= Sum F
defpred S1[ set , set ] means $2 = [(y /. $1),(f . (y /. $1))];
reconsider V = Prod_of_RLS (X,RLS_Real) as RealLinearSpace ;
A10: for i being Element of NAT st i in Seg n holds
f . (y /. i) in REAL
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies f . (y /. i) in REAL )
assume i in Seg n ; ::_thesis: f . (y /. i) in REAL
then f . (y /. i) <> +infty by A9;
hence f . (y /. i) in REAL by A1, XXREAL_0:14; ::_thesis: verum
end;
A11: for i being Element of NAT st i in Seg n holds
ex v being Element of V st S1[i,v]
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies ex v being Element of V st S1[i,v] )
assume i in Seg n ; ::_thesis: ex v being Element of V st S1[i,v]
then reconsider w = f . (y /. i) as Real by A10;
set v = [(y /. i),w];
reconsider v = [(y /. i),w] as Element of V ;
take v ; ::_thesis: S1[i,v]
thus S1[i,v] ; ::_thesis: verum
end;
consider g being FinSequence of the carrier of V such that
A12: dom g = Seg n and
A13: for i being Element of NAT st i in Seg n holds
S1[i,g /. i] from RECDEF_1:sch_17(A11);
A14: len g = n by A12, FINSEQ_1:def_3;
defpred S2[ set , set ] means $2 = F . $1;
A15: for i being Element of NAT st i in Seg n holds
ex w being Element of RLS_Real st S2[i,w]
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies ex w being Element of RLS_Real st S2[i,w] )
assume A16: i in Seg n ; ::_thesis: ex w being Element of RLS_Real st S2[i,w]
then reconsider a = f . (y /. i) as Real by A10;
F . i = (R_EAL (p . i)) * (f . (y /. i)) by A7, A16;
then F . i = (p . i) * a by EXTREAL1:1;
then reconsider w = F . i as Element of RLS_Real ;
take w ; ::_thesis: S2[i,w]
thus S2[i,w] ; ::_thesis: verum
end;
consider F1 being FinSequence of the carrier of RLS_Real such that
A17: dom F1 = Seg n and
A18: for i being Element of NAT st i in Seg n holds
S2[i,F1 /. i] from RECDEF_1:sch_17(A15);
A19: len F1 = n by A17, FINSEQ_1:def_3;
reconsider M = epigraph f as Subset of V ;
deffunc H1( Nat) -> Element of the carrier of V = (p . $1) * (g /. $1);
consider G being FinSequence of the carrier of V such that
A20: len G = n and
A21: for i being Nat st i in dom G holds
G . i = H1(i) from FINSEQ_2:sch_1();
A22: dom G = Seg n by A20, FINSEQ_1:def_3;
A23: for i being Nat st i in Seg n holds
( p . i > 0 & G . i = (p . i) * (g /. i) & g /. i in M )
proof
let i be Nat; ::_thesis: ( i in Seg n implies ( p . i > 0 & G . i = (p . i) * (g /. i) & g /. i in M ) )
assume A24: i in Seg n ; ::_thesis: ( p . i > 0 & G . i = (p . i) * (g /. i) & g /. i in M )
hence p . i > 0 by A7; ::_thesis: ( G . i = (p . i) * (g /. i) & g /. i in M )
thus G . i = (p . i) * (g /. i) by A21, A22, A24; ::_thesis: g /. i in M
reconsider w = f . (y /. i) as Real by A10, A24;
f . (y /. i) = R_EAL w ;
then [(y /. i),w] in { [x,a] where x is Element of X, a is Element of REAL : f . x <= R_EAL a } ;
hence g /. i in M by A13, A24; ::_thesis: verum
end;
M is convex by A2, Def6;
then A25: Sum G in M by A3, A6, A14, A20, A23, Th7;
A26: for i being Element of NAT st i in Seg n holds
F1 . i = F . i
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies F1 . i = F . i )
assume A27: i in Seg n ; ::_thesis: F1 . i = F . i
then F1 /. i = F1 . i by A17, PARTFUN1:def_6;
hence F1 . i = F . i by A18, A27; ::_thesis: verum
end;
for i being Element of NAT st i in Seg n holds
G . i = [(z . i),(F1 . i)]
proof
let i be Element of NAT ; ::_thesis: ( i in Seg n implies G . i = [(z . i),(F1 . i)] )
assume A28: i in Seg n ; ::_thesis: G . i = [(z . i),(F1 . i)]
then reconsider a = f . (y /. i) as Real by A10;
g /. i = [(y /. i),a] by A13, A28;
then (p . i) * (g /. i) = [((p . i) * (y /. i)),((p . i) * a)] by Lm1;
then G . i = [((p . i) * (y /. i)),((p . i) * a)] by A21, A22, A28;
then A29: G . i = [(z . i),((p . i) * a)] by A7, A28;
F . i = (R_EAL (p . i)) * (f . (y /. i)) by A7, A28;
then F . i = (p . i) * a by EXTREAL1:1;
hence G . i = [(z . i),(F1 . i)] by A26, A28, A29; ::_thesis: verum
end;
then Sum G = [(Sum z),(Sum F1)] by A5, A20, A19, Th3;
then [(Sum z),(Sum F)] in M by A4, A25, A26, A19, Lm8;
then consider x being Element of X, w being Element of REAL such that
A30: [(Sum z),(Sum F)] = [x,w] and
A31: f . x <= R_EAL w ;
x = Sum z by A30, XTUPLE_0:1;
hence f . (Sum z) <= Sum F by A30, A31, XTUPLE_0:1; ::_thesis: verum
end;
suppose ex i being Element of NAT st
( i in Seg n & f . (y /. i) = +infty ) ; ::_thesis: f . (Sum z) <= Sum F
then consider i being Element of NAT such that
A32: i in Seg n and
A33: f . (y /. i) = +infty ;
A34: F . i = (R_EAL (p . i)) * (f . (y /. i)) by A7, A32;
A35: i in dom F by A4, A32, FINSEQ_1:def_3;
p . i > 0 by A7, A32;
then F . i = +infty by A33, A34, XXREAL_3:def_5;
then Sum F = +infty by A8, A35, Lm6, FUNCT_1:3;
hence f . (Sum z) <= Sum F by XXREAL_0:4; ::_thesis: verum
end;
end;
end;
thus ( ( for n being non empty 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F ) implies f is convex ) ::_thesis: verum
proof
assume A36: for n being non empty 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F ; ::_thesis: f is convex
for x1, x2 being VECTOR of X
for q being Real st 0 < q & q < 1 holds
f . ((q * x1) + ((1 - q) * x2)) <= ((R_EAL q) * (f . x1)) + ((R_EAL (1 - q)) * (f . x2))
proof
set n = 2;
let x1, x2 be VECTOR of X; ::_thesis: for q being Real st 0 < q & q < 1 holds
f . ((q * x1) + ((1 - q) * x2)) <= ((R_EAL q) * (f . x1)) + ((R_EAL (1 - q)) * (f . x2))
let q be Real; ::_thesis: ( 0 < q & q < 1 implies f . ((q * x1) + ((1 - q) * x2)) <= ((R_EAL q) * (f . x1)) + ((R_EAL (1 - q)) * (f . x2)) )
assume that
A37: 0 < q and
A38: q < 1 ; ::_thesis: f . ((q * x1) + ((1 - q) * x2)) <= ((R_EAL q) * (f . x1)) + ((R_EAL (1 - q)) * (f . x2))
reconsider F = <*((R_EAL q) * (f . x1)),((R_EAL (1 - q)) * (f . x2))*> as FinSequence of ExtREAL ;
reconsider z = <*(q * x1),((1 - q) * x2)*> as FinSequence of the carrier of X ;
reconsider y = <*x1,x2*> as FinSequence of the carrier of X ;
reconsider p = <*q,(1 - q)*> as FinSequence of REAL ;
A39: for i being Element of NAT st i in Seg 2 holds
( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) )
proof
let i be Element of NAT ; ::_thesis: ( i in Seg 2 implies ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) )
assume A40: i in Seg 2 ; ::_thesis: ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) )
percases ( i = 1 or i = 2 ) by A40, FINSEQ_1:2, TARSKI:def_2;
supposeA41: i = 1 ; ::_thesis: ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) )
then A42: y /. i = x1 by FINSEQ_4:17;
p . i = q by A41, FINSEQ_1:44;
hence ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) by A37, A41, A42, FINSEQ_1:44; ::_thesis: verum
end;
supposeA43: i = 2 ; ::_thesis: ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) )
then A44: y /. i = x2 by FINSEQ_4:17;
p . i = 1 - q by A43, FINSEQ_1:44;
hence ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) by A38, A43, A44, FINSEQ_1:44, XREAL_1:50; ::_thesis: verum
end;
end;
end;
A45: len p = 2 by FINSEQ_1:44;
A46: Sum p = q + (1 - q) by RVSUM_1:77
.= 1 ;
A47: len z = 2 by FINSEQ_1:44;
A48: Sum z = (q * x1) + ((1 - q) * x2) by RLVECT_1:45;
A49: len y = 2 by FINSEQ_1:44;
A50: len F = 2 by FINSEQ_1:44;
Sum F = ((R_EAL q) * (f . x1)) + ((R_EAL (1 - q)) * (f . x2)) by EXTREAL1:9;
hence f . ((q * x1) + ((1 - q) * x2)) <= ((R_EAL q) * (f . x1)) + ((R_EAL (1 - q)) * (f . x2)) by A36, A45, A50, A49, A47, A46, A39, A48; ::_thesis: verum
end;
hence f is convex by A1, Th4; ::_thesis: verum
end;
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
deffunc H1( Nat) -> Nat = $1;
let F be FinSequence of REAL ; ::_thesis: 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 )
defpred S1[ Nat] means F . $1 <> 0 ;
defpred S2[ Nat] means F . $1 = 0 ;
set A = { H1(i) where i is Element of NAT : ( H1(i) in dom F & S1[i] ) } ;
set B = { H1(i) where i is Element of NAT : ( H1(i) in dom F & S2[i] ) } ;
set N = len F;
A1: { H1(i) where i is Element of NAT : ( H1(i) in dom F & S1[i] ) } c= dom F from FRAENKEL:sch_17();
then A2: { H1(i) where i is Element of NAT : ( H1(i) in dom F & S1[i] ) } c= Seg (len F) by FINSEQ_1:def_3;
reconsider A = { H1(i) where i is Element of NAT : ( H1(i) in dom F & S1[i] ) } as finite set by A1;
A3: rng (Sgm A) = A by A2, FINSEQ_1:def_13;
A4: { H1(i) where i is Element of NAT : ( H1(i) in dom F & S2[i] ) } c= dom F from FRAENKEL:sch_17();
then A5: { H1(i) where i is Element of NAT : ( H1(i) in dom F & S2[i] ) } c= Seg (len F) by FINSEQ_1:def_3;
reconsider B = { H1(i) where i is Element of NAT : ( H1(i) in dom F & S2[i] ) } as finite set by A4;
A6: rng (Sgm B) = B by A5, FINSEQ_1:def_13;
for x being set holds not x in A /\ B
proof
let x be set ; ::_thesis: not x in A /\ B
assume A7: x in A /\ B ; ::_thesis: contradiction
then x in B by XBOOLE_0:def_4;
then A8: ex i2 being Element of NAT st
( x = i2 & i2 in dom F & F . i2 = 0 ) ;
x in A by A7, XBOOLE_0:def_4;
then ex i1 being Element of NAT st
( x = i1 & i1 in dom F & F . i1 <> 0 ) ;
hence contradiction by A8; ::_thesis: verum
end;
then A /\ B = {} by XBOOLE_0:def_1;
then A9: A misses B by XBOOLE_0:def_7;
set s = (Sgm A) ^ (Sgm B);
A10: Sgm B is one-to-one by A5, FINSEQ_3:92;
Sgm A is one-to-one by A2, FINSEQ_3:92;
then A11: (Sgm A) ^ (Sgm B) is one-to-one by A3, A6, A9, A10, FINSEQ_3:91;
set n = len (Sgm A);
A12: len (Sgm A) = card A by A2, FINSEQ_3:39;
for x being set holds
( x in dom F iff ( x in A or x in B ) )
proof
let x be set ; ::_thesis: ( x in dom F iff ( x in A or x in B ) )
thus ( not x in dom F or x in A or x in B ) ::_thesis: ( ( x in A or x in B ) implies x in dom F )
proof
assume A13: x in dom F ; ::_thesis: ( x in A or x in B )
then reconsider x = x as Element of NAT ;
percases ( F . x <> 0 or F . x = 0 ) ;
suppose F . x <> 0 ; ::_thesis: ( x in A or x in B )
hence ( x in A or x in B ) by A13; ::_thesis: verum
end;
suppose F . x = 0 ; ::_thesis: ( x in A or x in B )
hence ( x in A or x in B ) by A13; ::_thesis: verum
end;
end;
end;
thus ( ( x in A or x in B ) implies x in dom F ) by A1, A4; ::_thesis: verum
end;
then A14: A \/ B = dom F by XBOOLE_0:def_3;
then A15: rng ((Sgm A) ^ (Sgm B)) = dom F by A3, A6, FINSEQ_1:31;
len (Sgm B) = card B by A5, FINSEQ_3:39;
then len ((Sgm A) ^ (Sgm B)) = (card A) + (card B) by A12, FINSEQ_1:22
.= card (A \/ B) by A9, CARD_2:40
.= card (Seg (len F)) by A14, FINSEQ_1:def_3 ;
then A16: len ((Sgm A) ^ (Sgm B)) = len F by FINSEQ_1:57;
then A17: dom ((Sgm A) ^ (Sgm B)) = Seg (len F) by FINSEQ_1:def_3;
A18: for x being Element of NAT st x in dom F & not x in Seg (len (Sgm A)) holds
ex k being Element of NAT st
( x = k + (len (Sgm A)) & k in dom (Sgm B) & ((Sgm A) ^ (Sgm B)) . x = (Sgm B) . k )
proof
let x be Element of NAT ; ::_thesis: ( x in dom F & not x in Seg (len (Sgm A)) implies ex k being Element of NAT st
( x = k + (len (Sgm A)) & k in dom (Sgm B) & ((Sgm A) ^ (Sgm B)) . x = (Sgm B) . k ) )
assume that
A19: x in dom F and
A20: not x in Seg (len (Sgm A)) ; ::_thesis: ex k being Element of NAT st
( x = k + (len (Sgm A)) & k in dom (Sgm B) & ((Sgm A) ^ (Sgm B)) . x = (Sgm B) . k )
A21: x in Seg (len F) by A19, FINSEQ_1:def_3;
( not 1 <= x or not x <= len (Sgm A) ) by A20, FINSEQ_1:1;
then (len (Sgm A)) + 1 <= x by A21, FINSEQ_1:1, INT_1:7;
then A22: ((len (Sgm A)) + 1) - (len (Sgm A)) <= x - (len (Sgm A)) by XREAL_1:9;
then reconsider k = x - (len (Sgm A)) as Element of NAT by INT_1:3;
take k ; ::_thesis: ( x = k + (len (Sgm A)) & k in dom (Sgm B) & ((Sgm A) ^ (Sgm B)) . x = (Sgm B) . k )
len ((Sgm A) ^ (Sgm B)) = (len (Sgm A)) + (len (Sgm B)) by FINSEQ_1:22;
then A23: (len F) - (len (Sgm A)) = len (Sgm B) by A16;
x <= len F by A21, FINSEQ_1:1;
then k <= len (Sgm B) by A23, XREAL_1:9;
then k in Seg (len (Sgm B)) by A22, FINSEQ_1:1;
then k in Seg (card B) by A5, FINSEQ_3:39;
then A24: k in dom (Sgm B) by A5, FINSEQ_3:40;
x = k + (len (Sgm A)) ;
hence ( x = k + (len (Sgm A)) & k in dom (Sgm B) & ((Sgm A) ^ (Sgm B)) . x = (Sgm B) . k ) by A24, FINSEQ_1:def_7; ::_thesis: verum
end;
dom F = Seg (len F) by FINSEQ_1:def_3;
then reconsider s = (Sgm A) ^ (Sgm B) as Function of (dom F),(dom F) by A15, A17, FUNCT_2:1;
s is onto by A15, FUNCT_2:def_3;
then reconsider s = s as Permutation of (dom F) by A11;
take s ; ::_thesis: 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 )
take len (Sgm A) ; ::_thesis: for i being Element of NAT st i in dom F holds
( i in Seg (len (Sgm A)) iff F . (s . i) <> 0 )
let i be Element of NAT ; ::_thesis: ( i in dom F implies ( i in Seg (len (Sgm A)) iff F . (s . i) <> 0 ) )
assume A25: i in dom F ; ::_thesis: ( i in Seg (len (Sgm A)) iff F . (s . i) <> 0 )
thus ( i in Seg (len (Sgm A)) implies F . (s . i) <> 0 ) ::_thesis: ( F . (s . i) <> 0 implies i in Seg (len (Sgm A)) )
proof
assume i in Seg (len (Sgm A)) ; ::_thesis: F . (s . i) <> 0
then A26: i in dom (Sgm A) by FINSEQ_1:def_3;
then s . i = (Sgm A) . i by FINSEQ_1:def_7;
then s . i in A by A3, A26, FUNCT_1:3;
then ex j being Element of NAT st
( s . i = j & j in dom F & F . j <> 0 ) ;
hence F . (s . i) <> 0 ; ::_thesis: verum
end;
thus ( F . (s . i) <> 0 implies i in Seg (len (Sgm A)) ) ::_thesis: verum
proof
assume A27: F . (s . i) <> 0 ; ::_thesis: i in Seg (len (Sgm A))
assume not i in Seg (len (Sgm A)) ; ::_thesis: contradiction
then ex k being Element of NAT st
( i = k + (len (Sgm A)) & k in dom (Sgm B) & s . i = (Sgm B) . k ) by A18, A25;
then s . i in rng (Sgm B) by FUNCT_1:3;
then ex j being Element of NAT st
( s . i = j & j in dom F & F . j = 0 ) by A6;
hence contradiction by A27; ::_thesis: verum
end;
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 empty 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F )
proof
let X be RealLinearSpace; ::_thesis: 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 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F )
let f be Function of the carrier of X,ExtREAL; ::_thesis: ( ( for x being VECTOR of X holds f . x <> -infty ) implies ( f is convex iff for n being non empty 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F ) )
assume A1: for x being VECTOR of X holds f . x <> -infty ; ::_thesis: ( f is convex iff for n being non empty 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F )
thus ( f is convex implies for n being non empty 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F ) ::_thesis: ( ( for n being non empty 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F ) implies f is convex )
proof
assume A2: f is convex ; ::_thesis: for n being non empty 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F
let n be non empty Element of NAT ; ::_thesis: 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F
let p be FinSequence of REAL ; ::_thesis: 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F
let F be FinSequence of ExtREAL ; ::_thesis: 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F
let y, z be FinSequence of the carrier of X; ::_thesis: ( 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) implies f . (Sum z) <= Sum F )
assume that
A3: len p = n and
A4: len F = n and
A5: len y = n and
A6: len z = n and
A7: Sum p = 1 and
A8: for i being Element of 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)) ) ; ::_thesis: f . (Sum z) <= Sum F
consider s being Permutation of (dom p), k being Element of NAT such that
A9: for i being Element of NAT st i in dom p holds
( i in Seg k iff p . (s . i) <> 0 ) by Lm14;
A10: dom p = Seg n by A3, FINSEQ_1:def_3;
then reconsider s1 = s as FinSequence of Seg n by FINSEQ_2:25;
A11: dom F = Seg n by A4, FINSEQ_1:def_3;
then A12: F is Function of (Seg n),ExtREAL by FINSEQ_2:26;
then reconsider F9 = F * s1 as FinSequence of ExtREAL by FINSEQ_2:32;
A13: F9 = (F9 | k) ^ (F9 /^ k) by RFINSEQ:8;
A14: for i being Element of NAT st 1 <= i & i <= n - k holds
( i + k in Seg n & p . (s . (i + k)) = 0 )
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= n - k implies ( i + k in Seg n & p . (s . (i + k)) = 0 ) )
assume that
A15: 1 <= i and
A16: i <= n - k ; ::_thesis: ( i + k in Seg n & p . (s . (i + k)) = 0 )
i <= i + k by INT_1:6;
then A17: 1 <= i + k by A15, XXREAL_0:2;
0 + k < i + k by A15, XREAL_1:6;
then A18: not i + k in Seg k by FINSEQ_1:1;
A19: i + k <= (n - k) + k by A16, XREAL_1:6;
then i + k in dom p by A10, A17, FINSEQ_1:1;
hence ( i + k in Seg n & p . (s . (i + k)) = 0 ) by A9, A19, A17, A18, FINSEQ_1:1; ::_thesis: verum
end;
A20: dom z = Seg n by A6, FINSEQ_1:def_3;
then A21: z is Function of (Seg n), the carrier of X by FINSEQ_2:26;
then reconsider z9 = z * s1 as FinSequence of the carrier of X by FINSEQ_2:32;
dom s = Seg n by A10, FUNCT_2:def_1;
then A22: len s1 = n by FINSEQ_1:def_3;
then A23: len z9 = n by A21, FINSEQ_2:33;
A24: Sum (z9 /^ k) = 0. X
proof
percases ( k >= n or k < n ) ;
suppose k >= n ; ::_thesis: Sum (z9 /^ k) = 0. X
then z9 /^ k = <*> the carrier of X by A23, FINSEQ_5:32;
hence Sum (z9 /^ k) = 0. X by RLVECT_1:43; ::_thesis: verum
end;
supposeA25: k < n ; ::_thesis: Sum (z9 /^ k) = 0. X
for w being set st w in rng (z9 /^ k) holds
w in {(0. X)}
proof
reconsider k1 = n - k as Element of NAT by A25, INT_1:5;
let w be set ; ::_thesis: ( w in rng (z9 /^ k) implies w in {(0. X)} )
assume w in rng (z9 /^ k) ; ::_thesis: w in {(0. X)}
then consider i being set such that
A26: i in dom (z9 /^ k) and
A27: (z9 /^ k) . i = w by FUNCT_1:def_3;
reconsider i = i as Element of NAT by A26;
len (z9 /^ k) = k1 by A23, A25, RFINSEQ:def_1;
then A28: i in Seg k1 by A26, FINSEQ_1:def_3;
then A29: 1 <= i by FINSEQ_1:1;
A30: i <= n - k by A28, FINSEQ_1:1;
then s . (i + k) in Seg n by A10, A14, A29, FUNCT_2:5;
then z . (s . (i + k)) = (p . (s . (i + k))) * (y /. (s . (i + k))) by A8;
then A31: z . (s . (i + k)) = 0. X by A14, A29, A30, RLVECT_1:10;
i + k in Seg n by A14, A29, A30;
then i + k in dom z9 by A23, FINSEQ_1:def_3;
then z9 . (i + k) = 0. X by A31, FUNCT_1:12;
then w = 0. X by A23, A25, A26, A27, RFINSEQ:def_1;
hence w in {(0. X)} by TARSKI:def_1; ::_thesis: verum
end;
then rng (z9 /^ k) c= {(0. X)} by TARSKI:def_3;
hence Sum (z9 /^ k) = 0. X by Lm11; ::_thesis: verum
end;
end;
end;
A32: p is Function of (Seg n),REAL by A10, FINSEQ_2:26;
then reconsider p9 = p * s1 as FinSequence of REAL by FINSEQ_2:32;
set k9 = min (k,n);
reconsider k9 = min (k,n) as Element of NAT ;
p9 = (p9 | k) ^ (p9 /^ k) by RFINSEQ:8;
then A33: Sum p9 = (Sum (p9 | k)) + (Sum (p9 /^ k)) by RVSUM_1:75;
A34: len F9 = n by A22, A12, FINSEQ_2:33;
A35: Sum (F9 /^ k) = 0.
proof
percases ( k >= n or k < n ) ;
suppose k >= n ; ::_thesis: Sum (F9 /^ k) = 0.
hence Sum (F9 /^ k) = 0. by A34, EXTREAL1:7, FINSEQ_5:32; ::_thesis: verum
end;
supposeA36: k < n ; ::_thesis: Sum (F9 /^ k) = 0.
for w being set st w in rng (F9 /^ k) holds
w in {0.}
proof
reconsider k1 = n - k as Element of NAT by A36, INT_1:5;
let w be set ; ::_thesis: ( w in rng (F9 /^ k) implies w in {0.} )
assume w in rng (F9 /^ k) ; ::_thesis: w in {0.}
then consider i being set such that
A37: i in dom (F9 /^ k) and
A38: (F9 /^ k) . i = w by FUNCT_1:def_3;
reconsider i = i as Element of NAT by A37;
len (F9 /^ k) = k1 by A34, A36, RFINSEQ:def_1;
then A39: i in Seg k1 by A37, FINSEQ_1:def_3;
then A40: 1 <= i by FINSEQ_1:1;
A41: i <= n - k by A39, FINSEQ_1:1;
then A42: p . (s . (i + k)) = 0 by A14, A40;
i + k in Seg n by A14, A40, A41;
then A43: i + k in dom F9 by A34, FINSEQ_1:def_3;
s . (i + k) in Seg n by A10, A14, A40, A41, FUNCT_2:5;
then F . (s . (i + k)) = (R_EAL 0) * (f . (y /. (s . (i + k)))) by A8, A42;
then F9 . (i + k) = 0. by A43, FUNCT_1:12;
then w = 0. by A34, A36, A37, A38, RFINSEQ:def_1;
hence w in {0.} by TARSKI:def_1; ::_thesis: verum
end;
then rng (F9 /^ k) c= {0.} by TARSKI:def_3;
hence Sum (F9 /^ k) = 0. by Lm9; ::_thesis: verum
end;
end;
end;
A44: F9 | k = F9 | (Seg k) by FINSEQ_1:def_15;
then A45: len (F9 | k) = k9 by A34, FINSEQ_2:21;
for i being Element of NAT st i in Seg n holds
( p . i >= 0 & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) by A8;
then A46: not -infty in rng F by A1, A4, Lm13;
then not -infty in rng F9 by FUNCT_1:14;
then A47: not -infty in (rng (F9 | k)) \/ (rng (F9 /^ k)) by A13, FINSEQ_1:31;
then A48: not -infty in rng (F9 /^ k) by XBOOLE_0:def_3;
A49: z9 | k = z9 | (Seg k) by FINSEQ_1:def_15;
then A50: len (z9 | k) = k9 by A23, FINSEQ_2:21;
A51: len p9 = n by A22, A32, FINSEQ_2:33;
A52: Sum (p9 /^ k) = 0
proof
percases ( k >= n or k < n ) ;
suppose k >= n ; ::_thesis: Sum (p9 /^ k) = 0
hence Sum (p9 /^ k) = 0 by A51, FINSEQ_5:32, RVSUM_1:72; ::_thesis: verum
end;
supposeA53: k < n ; ::_thesis: Sum (p9 /^ k) = 0
for w being set st w in rng (p9 /^ k) holds
w in {0}
proof
reconsider k1 = n - k as Element of NAT by A53, INT_1:5;
let w be set ; ::_thesis: ( w in rng (p9 /^ k) implies w in {0} )
assume w in rng (p9 /^ k) ; ::_thesis: w in {0}
then consider i being set such that
A54: i in dom (p9 /^ k) and
A55: (p9 /^ k) . i = w by FUNCT_1:def_3;
reconsider i = i as Element of NAT by A54;
len (p9 /^ k) = k1 by A51, A53, RFINSEQ:def_1;
then A56: i in Seg k1 by A54, FINSEQ_1:def_3;
then A57: 1 <= i by FINSEQ_1:1;
A58: i <= n - k by A56, FINSEQ_1:1;
then i + k in Seg n by A14, A57;
then A59: i + k in dom p9 by A51, FINSEQ_1:def_3;
p . (s . (i + k)) = 0 by A14, A57, A58;
then p9 . (i + k) = 0 by A59, FUNCT_1:12;
then w = 0 by A51, A53, A54, A55, RFINSEQ:def_1;
hence w in {0} by TARSKI:def_1; ::_thesis: verum
end;
then rng (p9 /^ k) c= {0} by TARSKI:def_3;
hence Sum (p9 /^ k) = 0 by Lm10; ::_thesis: verum
end;
end;
end;
A60: p9 | k = p9 | (Seg k) by FINSEQ_1:def_15;
then A61: len (p9 | k) = k9 by A51, FINSEQ_2:21;
not -infty in rng (F9 | k) by A47, XBOOLE_0:def_3;
then A62: Sum F9 = (Sum (F9 | k)) + (Sum (F9 /^ k)) by A13, A48, EXTREAL1:10;
Sum F9 = Sum F by A10, A11, A46, EXTREAL1:11;
then A63: Sum (F9 | k) = Sum F by A62, A35, XXREAL_3:4;
z9 = (z9 | k) ^ (z9 /^ k) by RFINSEQ:8;
then A64: Sum z9 = (Sum (z9 | k)) + (Sum (z9 /^ k)) by RLVECT_1:41;
Sum z9 = Sum z by A10, A20, RLVECT_2:7;
then A65: Sum (z9 | k) = Sum z by A64, A24, RLVECT_1:def_4;
A66: dom y = Seg n by A5, FINSEQ_1:def_3;
then A67: y is Function of (Seg n), the carrier of X by FINSEQ_2:26;
then reconsider y9 = y * s1 as FinSequence of the carrier of X by FINSEQ_2:32;
A68: y9 | k = y9 | (Seg k) by FINSEQ_1:def_15;
len y9 = n by A22, A67, FINSEQ_2:33;
then A69: len (y9 | k) = k9 by A68, FINSEQ_2:21;
A70: p9,p are_fiberwise_equipotent by RFINSEQ:4;
then p9 | k <> {} by A7, A33, A52, RFINSEQ:9, RVSUM_1:72;
then reconsider k9 = k9 as non empty Element of NAT by A61;
A71: for i being Element of NAT st i in Seg k9 holds
( (p9 | k) . i > 0 & (z9 | k) . i = ((p9 | k) . i) * ((y9 | k) /. i) & (F9 | k) . i = (R_EAL ((p9 | k) . i)) * (f . ((y9 | k) /. i)) )
proof
let i be Element of NAT ; ::_thesis: ( i in Seg k9 implies ( (p9 | k) . i > 0 & (z9 | k) . i = ((p9 | k) . i) * ((y9 | k) /. i) & (F9 | k) . i = (R_EAL ((p9 | k) . i)) * (f . ((y9 | k) /. i)) ) )
assume A72: i in Seg k9 ; ::_thesis: ( (p9 | k) . i > 0 & (z9 | k) . i = ((p9 | k) . i) * ((y9 | k) /. i) & (F9 | k) . i = (R_EAL ((p9 | k) . i)) * (f . ((y9 | k) /. i)) )
then A73: i in dom (p9 | k) by A61, FINSEQ_1:def_3;
then A74: (p9 | k) /. i = p9 /. i by FINSEQ_4:70;
dom (p9 | k) = (dom p9) /\ (Seg k) by A60, RELAT_1:61;
then A75: i in dom p9 by A73, XBOOLE_0:def_4;
then A76: p9 . i = p . (s . i) by FUNCT_1:12;
p9 /. i = p9 . i by A75, PARTFUN1:def_6;
then A77: (p9 | k) . i = p . (s . i) by A73, A74, A76, PARTFUN1:def_6;
A78: i in dom (y9 | k) by A69, A72, FINSEQ_1:def_3;
then A79: (y9 | k) /. i = y9 /. i by FINSEQ_4:70;
dom (y9 | k) = (dom y9) /\ (Seg k) by A68, RELAT_1:61;
then A80: i in dom y9 by A78, XBOOLE_0:def_4;
then A81: y9 . i = y . (s . i) by FUNCT_1:12;
A82: i in dom (F9 | k) by A45, A72, FINSEQ_1:def_3;
then A83: (F9 | k) /. i = F9 /. i by FINSEQ_4:70;
dom (F9 | k) = (dom F9) /\ (Seg k) by A44, RELAT_1:61;
then A84: i in dom F9 by A82, XBOOLE_0:def_4;
then A85: F9 . i = F . (s . i) by FUNCT_1:12;
F9 /. i = F9 . i by A84, PARTFUN1:def_6;
then A86: (F9 | k) . i = F . (s . i) by A82, A83, A85, PARTFUN1:def_6;
A87: i in dom (z9 | k) by A50, A72, FINSEQ_1:def_3;
then A88: (z9 | k) /. i = z9 /. i by FINSEQ_4:70;
dom (z9 | k) = (dom z9) /\ (Seg k) by A49, RELAT_1:61;
then A89: i in dom z9 by A87, XBOOLE_0:def_4;
then A90: z9 . i = z . (s . i) by FUNCT_1:12;
z9 /. i = z9 . i by A89, PARTFUN1:def_6;
then A91: (z9 | k) . i = z . (s . i) by A87, A88, A90, PARTFUN1:def_6;
A92: i in Seg n by A51, A75, FINSEQ_1:def_3;
k9 <= k by XXREAL_0:17;
then Seg k9 c= Seg k by FINSEQ_1:5;
then A93: p . (s . i) <> 0 by A9, A10, A72, A92;
y9 /. i = y9 . i by A80, PARTFUN1:def_6;
then A94: (y9 | k) /. i = y /. (s . i) by A10, A66, A79, A81, A92, FUNCT_2:5, PARTFUN1:def_6;
s . i in Seg n by A10, A92, FUNCT_2:5;
hence ( (p9 | k) . i > 0 & (z9 | k) . i = ((p9 | k) . i) * ((y9 | k) /. i) & (F9 | k) . i = (R_EAL ((p9 | k) . i)) * (f . ((y9 | k) /. i)) ) by A8, A77, A94, A91, A86, A93; ::_thesis: verum
end;
Sum (p9 | k) = 1 by A7, A33, A52, A70, RFINSEQ:9;
hence f . (Sum z) <= Sum F by A1, A2, A65, A63, A61, A69, A50, A45, A71, Th8; ::_thesis: verum
end;
thus ( ( for n being non empty 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F ) implies f is convex ) ::_thesis: verum
proof
assume A95: for n being non empty 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F ; ::_thesis: f is convex
for n being non empty 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F
proof
let n be non empty Element of NAT ; ::_thesis: 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F
let p be FinSequence of REAL ; ::_thesis: 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F
let F be FinSequence of ExtREAL ; ::_thesis: 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds
f . (Sum z) <= Sum F
let y, z be FinSequence of the carrier of X; ::_thesis: ( 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 = (R_EAL (p . i)) * (f . (y /. i)) ) ) implies f . (Sum z) <= Sum F )
assume that
A96: len p = n and
A97: len F = n and
A98: len y = n and
A99: len z = n and
A100: Sum p = 1 and
A101: for i being Element of 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)) ) ; ::_thesis: f . (Sum z) <= Sum F
for i being Element of 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)) ) by A101;
hence f . (Sum z) <= Sum F by A95, A96, A97, A98, A99, A100; ::_thesis: verum
end;
hence f is convex by A1, Th8; ::_thesis: verum
end;
end;