:: Definition of Convex Function and {J}ensen's Inequality
:: by Grigory E. Ivanov
::
:: Received July 17, 2003
:: Copyright (c) 2003-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, RLVECT_1, BINOP_1, ZFMISC_1, STRUCT_0,
SUBSET_1, FUNCT_1, ALGSTR_0, REAL_1, SUPINF_2, RELAT_1, ARYTM_3,
FINSEQ_1, CARD_3, CARD_1, XXREAL_0, TARSKI, PARTFUN1, ORDINAL4, BINOP_2,
ARYTM_1, SUPINF_1, NAT_1, FUNCT_2, RFINSEQ, CONVEX1, RFUNCT_3, FINSET_1,
CLASSES1, CONVFUN1, FUNCT_7, XCMPLX_0, NUMBER09;
notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XXREAL_0,
XXREAL_3, XCMPLX_0, XREAL_0, REAL_1, FUNCT_1, RELSET_1, PARTFUN1,
SUPINF_1, ZFMISC_1, MEASURE6, BINOP_1, FUNCT_2, SUPINF_2, DOMAIN_1,
BINOP_2, FINSET_1, CLASSES1, RFINSEQ, RFUNCT_3, NAT_1, RVSUM_1, EXTREAL1,
FINSEQ_1, FINSEQ_4, STRUCT_0, ALGSTR_0, RLVECT_1, CONVEX1;
constructors BINOP_1, DOMAIN_1, REAL_1, FINSEQ_4, FINSOP_1, RVSUM_1, SUPINF_2,
RFINSEQ, RFUNCT_3, MEASURE6, EXTREAL1, CONVEX1, BINOP_2, SUPINF_1,
CLASSES1, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS,
XXREAL_0, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, STRUCT_0, RLVECT_1,
VALUED_0, ALGSTR_0, CARD_1, XXREAL_3, INT_1, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions RLVECT_1, ALGSTR_0;
equalities BINOP_1, RLVECT_1, RVSUM_1, STRUCT_0, ALGSTR_0, XCMPLX_0;
expansions BINOP_1, RLVECT_1;
theorems ZFMISC_1, FUNCT_2, CONVEX1, SUPINF_2, EXTREAL1, RLVECT_1, RFUNCT_3,
RVSUM_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSEQ_5, NAT_1, TARSKI,
FUNCT_1, CARD_2, INT_1, XCMPLX_1, XBOOLE_0, RFINSEQ, RLVECT_2, RELAT_1,
XBOOLE_1, BINOP_2, XREAL_1, XXREAL_0, XREAL_0, FINSOP_1, PARTFUN1,
ALGSTR_0, VALUED_1, XXREAL_3, XTUPLE_0;
schemes BINOP_1, DOMAIN_1, FINSEQ_2, FRAENKEL, NAT_1, RECDEF_1;
begin :: Product of Two Real Linear Spaces
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:
for z1, z2 being Element of [:the carrier of X, the carrier of
Y:], x1, x2 being VECTOR of X, 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
proof
defpred P[set,set,set] means for x1, x2 being VECTOR of X, 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 A ex z3 being Element of A st P[z1,z2,z3]
proof
let z1,z2 being Element of A;
consider x19, y19 being object 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 object 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,y29 as VECTOR of Y by A3,A6;
reconsider x19,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 A;
take z3;
let x1, x2 be VECTOR of X, y1, y2 be VECTOR of Y;
assume that
A8: z1 = [x1,y1] and
A9: z2 = [x2,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 thesis by A7,A9,A10,A11,XTUPLE_0:1;
end;
thus ex o being BinOp of A st for a,b being Element of A holds P[a,b,o.(a,
b)] from BINOP_1:sch 3(A1);
end;
uniqueness
proof
let A1, A2 be BinOp of [:the carrier of X, the carrier of Y:];
assume
A12: for z1, z2 being Element of [:the carrier of X, the carrier of Y
:], x1, x2 being VECTOR of X, 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]];
assume
A13: for z1, z2 being Element of [:the carrier of X, the carrier of Y
:], x1, x2 being VECTOR of X, 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]];
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:];
consider x1 , y1 being object 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 object 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,y2 as VECTOR of Y by A15,A18;
reconsider x1,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 thesis by A13,A16,A19;
end;
hence thesis;
end;
end;
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:
for a being Real,
z being Element of [:the carrier of X, the carrier of Y:], x being
VECTOR of X, 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
proof
defpred P[object,object,object] means
for x being VECTOR of X, 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, 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 P[a1,z,w]
proof
let a1 being Element of REAL, z be Element of [:the carrier of X, the
carrier of Y:];
consider x9 , y9 being object 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 as VECTOR of Y by A3;
reconsider 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;
for x being VECTOR of X, 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, y be VECTOR of Y;
assume
A5: z = [x,y];
then x=x9 by A4,XTUPLE_0:1;
hence thesis by A4,A5,XTUPLE_0:1;
end;
hence thesis;
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, z being Element of [:the carrier of X
, the carrier of Y:] holds P[a,z,g.(a,z)] from BINOP_1:sch 3(A1);
A7: for a being Real, z being Element of [:the carrier of X
, the carrier of Y:] holds P[a,z,g.(a,z)]
proof let a be Real, z be Element of [:the carrier of X
, the carrier of Y:];
reconsider a as Element of REAL by XREAL_0:def 1;
P[a,z,g.(a,z)] by A6;
hence thesis;
end;
take g;
let a being Real,
z being Element of [:the carrier of X, the carrier of Y
:];
thus thesis by A7;
end;
uniqueness
proof
let g1,g2 be Function of [:REAL, [:the carrier of X, the carrier of Y:]:],
[:the carrier of X, the carrier of Y:];
assume
A8: for a being Real, z being Element of [:the carrier of X, the
carrier of Y:], x being VECTOR of X, 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]];
assume
A9: for a being Real, z being Element of [:the carrier of X, the
carrier of Y:], x being VECTOR of X, 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]];
for a being Element of REAL,
z being Element of [:the carrier of X, the carrier
of Y:] holds g1.(a,z) = g2.(a,z)
proof
let a be Element of REAL,
z be Element of [:the carrier of X, the carrier of Y:];
consider x , y being object such that
A10: x in the carrier of X and
A11: y in the carrier of Y and
A12: z = [x,y] by ZFMISC_1:def 2;
reconsider y as VECTOR of Y by A11;
reconsider x as VECTOR of X by A10;
g1.(a,z) = [(the Mult of X).[a,x],(the Mult of Y).[a,y]] by A8,A12;
hence thesis by A9,A12;
end;
hence thesis;
end;
end;
definition
let X,Y be non empty RLSStruct;
func Prod_of_RLS(X,Y) -> RLSStruct equals
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;
end;
registration
let X,Y be non empty RLSStruct;
cluster Prod_of_RLS(X,Y) -> non empty;
coherence;
end;
theorem
for X,Y being non empty RLSStruct, x being VECTOR of X, y being VECTOR
of Y, u being VECTOR of Prod_of_RLS(X,Y), p being Real st u = [x,y] holds p*u =
[p*x,p*y] by Def2;
theorem Th2:
for X,Y being non empty RLSStruct, x1, x2 being VECTOR of X, y1,
y2 being VECTOR of Y, 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 Abelian non empty RLSStruct;
cluster Prod_of_RLS(X,Y) -> Abelian;
coherence
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);
consider x1,y1 being object 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 as VECTOR of Y by A2;
reconsider x1 as VECTOR of X by A1;
consider x2,y2 being object 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 as VECTOR of Y by A5;
reconsider x2 as VECTOR of X by A4;
u1+u2 = [x2+x1,y2+y1] by A3,A6,Th2;
hence thesis by A3,A6,Def1;
end;
hence thesis;
end;
end;
registration
let X,Y be add-associative non empty RLSStruct;
cluster Prod_of_RLS(X,Y) -> add-associative;
coherence
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);
consider x1,y1 being object 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 as VECTOR of Y by A2;
consider x3,y3 being object 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 as VECTOR of Y by A5;
reconsider x3 as VECTOR of X by A4;
reconsider x1 as VECTOR of X by A1;
consider x2,y2 being object 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 as VECTOR of Y by A8;
reconsider 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 thesis by A10,A11,RLVECT_1:def 3;
end;
hence thesis;
end;
end;
registration
let X,Y be right_zeroed non empty RLSStruct;
cluster Prod_of_RLS(X,Y) -> right_zeroed;
coherence
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);
consider x,y being object 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 as VECTOR of Y by A2;
reconsider 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 thesis by A3,A4,Def1;
end;
hence thesis;
end;
end;
registration
let X,Y be right_complementable non empty RLSStruct;
cluster Prod_of_RLS(X,Y) -> right_complementable;
coherence
proof
let u be Element of Prod_of_RLS(X,Y);
consider x,y being object 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 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 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 as Element of Prod_of_RLS(X,Y);
take u1;
thus thesis by A3,A4,A5,Def1;
end;
end;
registration
let X,Y be vector-distributive scalar-distributive scalar-associative
scalar-unital
non empty RLSStruct;
cluster Prod_of_RLS(X,Y) -> vector-distributive scalar-distributive
scalar-associative scalar-unital;
coherence
proof
A1: for a being Real for u1,u2 being VECTOR of Prod_of_RLS(X,Y)
holds a*(u1+u2)=a*u1+a*u2
proof
let a be Real;
reconsider a as Real;
let u1,u2 be VECTOR of Prod_of_RLS(X,Y);
consider x1,y1 being object 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 as VECTOR of X by A2;
consider x2,y2 being object 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 as VECTOR of Y by A6;
reconsider x2 as VECTOR of X by A5;
reconsider 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 thesis by A9,A11,A8,A10,Def1;
end;
A12: for a,b being Real for u being VECTOR of Prod_of_RLS(X,Y)
holds (a*b)*u = a*(b*u)
proof
let a,b be Real;
reconsider a,b as Real;
let u be VECTOR of Prod_of_RLS(X,Y);
consider x,y being object 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 as VECTOR of Y by A14;
reconsider 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 thesis by A15,A16,A17,Def2;
end;
A18: for a,b being Real for u being VECTOR of Prod_of_RLS(X,Y)
holds (a+b)*u = a*u+b*u
proof
let a,b be Real;
reconsider a,b as Real;
let u be VECTOR of Prod_of_RLS(X,Y);
consider x,y being object 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 as VECTOR of Y by A20;
reconsider 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 thesis by A21,A23,A24,Def2;
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);
consider x,y being object 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 as VECTOR of Y by A26;
reconsider 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 thesis by A27,A28,Def2;
end;
hence thesis by A1,A18,A12;
end;
end;
theorem Th3:
for X,Y being RealLinearSpace, n being Nat, x being
FinSequence of the carrier of X, y being FinSequence of the carrier of Y, z
being FinSequence of the carrier of Prod_of_RLS(X,Y) st len x = n & len y = n &
len z = n & (for i being Nat st i in Seg n holds z.i = [x.i,y.i])
holds Sum z = [Sum x, Sum y]
proof
let X, Y be RealLinearSpace;
defpred P[Nat] means for x being FinSequence of the carrier of X,
y being FinSequence of the carrier of Y, 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 Nat st i in Seg $1 holds z.i = [x.i,y.i]
holds Sum z = [Sum x, Sum y];
A1: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A2: P[n];
thus P[n+1]
proof
let x be FinSequence of the carrier of X, y be FinSequence of the
carrier of Y, z be FinSequence of the carrier of Prod_of_RLS(X,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 Nat st i in Seg(n+1) holds z.i = [x.i,y. i];
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 Nat st i in Seg n holds (z|n).i = [(x|n).i,(y|n).i]
proof
let i be Nat;
assume
A11: i in Seg n;
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 thesis by A6,A9,A11,A13,A14;
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;
assume
A16: i in Seg(n+1);
then
A17: i<=n+1 by FINSEQ_1:1;
1<=i by A16,FINSEQ_1:1;
hence thesis by A3,A4,A5,A17,FINSEQ_4:15;
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 16;
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 16;
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 16;
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 thesis by A24,A22,A21,A20,Def1;
end;
end;
A26: P[0]
proof
let x be FinSequence of the carrier of X, y be FinSequence of the carrier
of Y, z be FinSequence of the carrier of Prod_of_RLS(X,Y);
assume that
A27: len x = 0 and
A28: len y = 0 and
A29: len z = 0 and
for i being Nat st i in Seg 0 holds z.i = [x.i,y.i];
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 thesis by A30,A31,RLVECT_1:43;
end;
thus for n being Nat holds P[n] from NAT_1:sch 2(A26,A1);
end;
begin :: Real Linear Space of Real Numbers
definition
func RLS_Real -> non empty RLSStruct equals
RLSStruct(# REAL,In(0,REAL),addreal,multreal #);
correctness;
end;
registration
cluster RLS_Real -> Abelian add-associative right_zeroed
right_complementable vector-distributive
scalar-distributive scalar-associative scalar-unital;
coherence
proof
thus RLS_Real is Abelian
proof
let v,w be VECTOR of RLS_Real;
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;
end;
thus RLS_Real is add-associative
proof
let u,v,w be VECTOR of RLS_Real;
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 thesis by A1;
end;
thus RLS_Real is right_zeroed
proof
let v be VECTOR of RLS_Real;
reconsider vr=v as Real;
thus v+0.RLS_Real = vr+0 by BINOP_2:def 9
.= v;
end;
thus RLS_Real is right_complementable
proof
let v be VECTOR of RLS_Real;
reconsider vr=v as Real;
reconsider w=-vr as VECTOR of RLS_Real by XREAL_0:def 1;
take w;
thus v+w = vr+(-vr) by BINOP_2:def 9
.= 0.RLS_Real;
end;
thus for a being Real for v,w being VECTOR of RLS_Real holds a*(v+w
) = a*v+a*w
proof
let a be Real;
reconsider a as Real;
let v,w be VECTOR of RLS_Real;
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 thesis;
end;
thus for a,b being Real for v being VECTOR of RLS_Real holds (a+b)*
v = a*v+b*v
proof
let a,b be Real;
reconsider a,b as Real;
let v be VECTOR of RLS_Real;
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 thesis;
end;
thus for a,b being Real for v being VECTOR of RLS_Real holds (a*b)*
v = a*(b*v)
proof
let a,b be Real;
reconsider a,b as Real;
let v be VECTOR of RLS_Real;
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 thesis;
end;
let v be VECTOR of RLS_Real;
reconsider vr=v as Real;
thus 1*v = 1*vr by BINOP_2:def 11
.= v;
end;
end;
Lm1: for X being non empty RLSStruct, x being VECTOR of X, u being VECTOR of
Prod_of_RLS(X,RLS_Real),
p,w being Real st u = [x,w] holds p*u = [p*x,p*w]
proof
let X be non empty RLSStruct, x be VECTOR of X, u be VECTOR of Prod_of_RLS(X
,RLS_Real), p,w be Real;
reconsider y=w as VECTOR of RLS_Real by XREAL_0:def 1;
assume
A1: u = [x,w];
p*y = p*w by BINOP_2:def 11;
hence thesis by A1,Def2;
end;
Lm2: for X being non empty RLSStruct, x1, x2 being VECTOR of X,
w1, w2 being Real,
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, x1, x2 be VECTOR of X,
w1, w2 be Real, u1, u2
be VECTOR of Prod_of_RLS(X,RLS_Real);
reconsider y1=w1 as VECTOR of RLS_Real by XREAL_0:def 1;
reconsider y2=w2 as VECTOR of RLS_Real by XREAL_0:def 1;
assume that
A1: u1 = [x1,w1] and
A2: u2 = [x2,w2];
y1+y2 = w1+w2 by BINOP_2:def 9;
hence thesis by A1,A2,Def1;
end;
Lm3: for a being FinSequence of the carrier of RLS_Real, 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, b be FinSequence of REAL;
defpred P[Nat] means for a be FinSequence of the carrier of
RLS_Real, b be 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 Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A2: P[n];
thus P[n+1]
proof
let a be FinSequence of the carrier of RLS_Real, b be FinSequence of
REAL;
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;
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;
assume
A10: i in Seg(n+1);
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 thesis by A5,A8,A10;
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;
assume i in dom(a|n);
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 thesis by A5,A8,A12,A14,A16;
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 16;
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 16;
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 thesis by A18,RVSUM_1:74;
end;
end;
A21: P[0]
proof
let a be FinSequence of the carrier of RLS_Real, b be FinSequence of REAL;
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;
a = <*>(the carrier of RLS_Real) by A22;
then
A24: Sum a = 0.RLS_Real by RLVECT_1:43;
b = <*> REAL by A23;
hence thesis by A24,RVSUM_1:72;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A21,A1);
hence thesis;
end;
begin
Lm4: for F being FinSequence of ExtREAL, x being Element of ExtREAL holds Sum(
F^<*x*>) = Sum F + x
proof
let F be FinSequence of ExtREAL, x be Element of ExtREAL;
consider f being sequence of ExtREAL such that
A1: Sum(F^<*x*>) = f.(len(F^<*x*>)) and
A2: f.0 = 0. and
A3: for i being 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 Nat st i < len F holds f.(i+1)=f.i+F.(i+1)
proof
let i be Nat;
A5: 1 <= i+1 by NAT_1:11;
assume
A6: i < len F;
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 thesis by A7,FINSEQ_1:def 7;
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 thesis by A1,A4,A8,FINSEQ_1:42;
end;
Lm5: for F being FinSequence of ExtREAL st not -infty in rng F holds Sum F <>
-infty
proof
defpred P[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 P[F
] holds P[F^<*x*>]
proof
let F be FinSequence of ExtREAL;
let x be Element of ExtREAL;
assume
A2: P[F];
A3: Sum(F^<*x*>) = Sum F + x by Lm4;
assume not -infty in rng(F^<*x*>);
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 thesis by A2,A4,A3,XBOOLE_0:def 3,XXREAL_3:17;
end;
A5: P[<*> ExtREAL] by EXTREAL1:7;
thus for F being FinSequence of ExtREAL holds P[F] from FINSEQ_2:sch 2 (A5,
A1);
end;
Lm6: for F being FinSequence of ExtREAL st +infty in rng F & not -infty in rng
F holds Sum F = +infty
proof
defpred P[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 P[F
] holds P[F^<*x*>]
proof
let F be FinSequence of ExtREAL;
let x be Element of ExtREAL;
assume
A2: P[F];
assume that
A3: +infty in rng(F^<*x*>) and
A4: not -infty in rng(F^<*x*>);
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;
per cases by A6,TARSKI:def 1;
suppose
+infty in rng F;
hence thesis by A2,A7,A9,A5,XBOOLE_0:def 3,XXREAL_3:def 2;
end;
suppose
+infty = x;
hence thesis by A5,A8,XXREAL_3:def 2;
end;
end;
A10: P[<*> ExtREAL];
thus for F being FinSequence of ExtREAL holds P[F] from FINSEQ_2:sch 2 (A10,
A1);
end;
Lm7: for a being FinSequence of ExtREAL, 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, b be FinSequence of REAL;
defpred P[Nat] means for a be FinSequence of ExtREAL, b be
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 Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A2: P[n];
thus P[n+1]
proof
let a be FinSequence of ExtREAL, b be FinSequence of REAL;
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;
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;
assume i in dom(a|n);
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 thesis by A5,A6,A10,A12,A14;
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 16;
then
A16: b = (b|n)^<*b.(n+1)*> by A4,FINSEQ_3:55;
a|n = a | Seg n by FINSEQ_1:def 16;
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 thesis by A16,RVSUM_1:74;
end;
end;
A17: P[0]
proof
let a be FinSequence of ExtREAL, b be FinSequence of REAL;
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;
a = <*>ExtREAL by A18;
then
A20: Sum a = 0. by EXTREAL1:7;
b = <*>ExtREAL by A19;
hence thesis by A20,RVSUM_1:72;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A17,A1);
hence thesis;
end;
Lm8: for n being Element of NAT, a being FinSequence of ExtREAL, 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, a be FinSequence of ExtREAL, b be FinSequence of
the carrier of RLS_Real;
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;
set c = b;
reconsider c 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 thesis by A4,A5,Lm3;
end;
Lm9: for F being FinSequence of ExtREAL st rng F c= {0.} holds Sum F = 0.
proof
let F be FinSequence of ExtREAL;
defpred P[FinSequence of ExtREAL] means rng $1 c= {0.} implies Sum $1 = 0.;
assume
A1: rng F c= {0.};
A2: for F being FinSequence of ExtREAL for x being Element of ExtREAL st P[F
] holds P[F^<*x*>]
proof
let F be FinSequence of ExtREAL;
let x be Element of ExtREAL;
assume
A3: P[F];
assume rng(F^<*x*>) c= {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;
end;
A6: P[<*> ExtREAL] by EXTREAL1:7;
for F being FinSequence of ExtREAL holds P[F] from FINSEQ_2:sch 2 (A6,
A2);
hence thesis by A1;
end;
Lm10: for F being FinSequence of REAL st rng F c= {0} holds Sum F = 0
proof
let F be FinSequence of REAL;
defpred P[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 P[F]
holds P[F^<*x*>]
proof
let F be FinSequence of REAL;
let x be Element of REAL;
assume
A2: P[F];
assume rng(F^<*x*>) c= {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;
end;
assume
A5: rng F c= {0};
A6: P[<*> REAL] by RVSUM_1:72;
for F being FinSequence of REAL holds P[F] from FINSEQ_2:sch 2(A6,A1 );
hence thesis by A5;
end;
Lm11: for X being RealLinearSpace, F being FinSequence of the carrier of X st
rng F c= {0.X} holds Sum F = 0.X
proof
let X be RealLinearSpace;
defpred P[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
P[F] holds P[F^<*x*>]
proof
let F be FinSequence of the carrier of X;
let x be Element of X;
assume
A2: P[F];
assume rng(F^<*x*>) c= {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,XBOOLE_1:11;
end;
let F be FinSequence of the carrier of X;
assume
A5: rng F c= {0.X};
A6: P[<*> the carrier of X] by RLVECT_1:43;
for F being FinSequence of the carrier of X holds P[F] from FINSEQ_2:
sch 2(A6,A1);
hence thesis by A5;
end;
begin :: Definition of Convex Function
definition
let X be non empty RLSStruct, f be Function of the carrier of X,ExtREAL;
func epigraph f -> Subset of Prod_of_RLS(X,RLS_Real) equals
{[x,y] where x is Element of X, y is Element of REAL: f.x <= (y)};
coherence
proof
deffunc f(Element of X, Element of REAL) = [$1,$2];
defpred P[Element of X, Real] means f.$1 <= ($2);
{f(x,y) where x is Element of X, y is Element of REAL: P[x,y]} is
Subset of [:the carrier of X,REAL:] from DOMAIN_1:sch 9;
hence thesis;
end;
end;
definition
let X be non empty RLSStruct, f be Function of the carrier of X,ExtREAL;
attr f is convex means
epigraph f is convex;
end;
Lm12: for w1,w2 being R_eal,
wr1,wr2,p1,p2 being Real st w1=wr1 & w2=wr2 holds
p1*wr1+p2*wr2 = (p1)*w1+(p2)*w2
proof
let w1,w2 be R_eal, wr1,wr2,p1,p2 be Real;
assume that
A1: w1=wr1 and
A2: w2=wr2;
A3: p2*wr2 = (p2)*w2 by A2,EXTREAL1:1;
p1*wr1 = (p1)*w1 by A1,EXTREAL1:1;
hence thesis by A3,SUPINF_2:1;
end;
theorem Th4:
for X being non empty RLSStruct, 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,
p being Real st 0<p & p<1 holds f.(p*x1+(1-p)
*x2) <= (p)*f.x1+(1-p)*f.x2
proof
let X be non empty RLSStruct, f be Function of the carrier of X,ExtREAL;
assume
A1: for x being VECTOR of X holds f.x <> -infty;
thus f is convex implies for x1, x2 being VECTOR of X,
p being Real st 0<p &
p<1 holds f.(p*x1+(1-p)*x2) <= (p)*f.x1+(1-p)*f.x2
proof
assume f is convex;
then
A2: epigraph f is convex;
let x1, x2 be VECTOR of X, p be Real;
assume that
A3: 0<p and
A4: p<1;
set p2 = (1-p);
set p1 = (p);
A5: 1-p > 0 by A4,XREAL_1:50;
per cases by A1,XXREAL_0:14;
suppose
A6: f.x1 in REAL & f.x2 in REAL;
then reconsider w2=f.x2 as Element of REAL;
reconsider w1=f.x1 as Element of 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);
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;
[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 <= (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 thesis by A11,A12,Lm12;
end;
suppose
A13: f.x1 = +infty & f.x2 in REAL;
A14: p2*f.x2 in REAL
by A13,XREAL_0:def 1;
p1*f.x1 = +infty by A3,A13,XXREAL_3:def 5;
then p1*f.x1+p2*f.x2 = +infty by A14,XXREAL_3:def 2;
hence thesis by XXREAL_0:4;
end;
suppose
A15: f.x1 in REAL & f.x2 = +infty;
A16: p1*f.x1 in REAL
by A15,XREAL_0:def 1;
p2*f.x2 = +infty by A5,A15,XXREAL_3:def 5;
then p1*f.x1+p2*f.x2 = +infty by A16,XXREAL_3:def 2;
hence thesis by XXREAL_0:4;
end;
suppose
A17: f.x1 = +infty & f.x2 = +infty;
then p2*f.x2 = +infty by A5,XXREAL_3:def 5;
then p1*f.x1+p2*f.x2 = +infty by A3,A17,XXREAL_3:def 2;
hence thesis by XXREAL_0:4;
end;
end;
assume
A18: for x1, x2 being VECTOR of X, p being Real
st 0<p & p<1 holds f.(p*
x1+(1-p)*x2) <= (p)*f.x1+(1-p)*f.x2;
for u1,u2 being VECTOR of Prod_of_RLS(X,RLS_Real),
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), p being Real;
assume that
A19: 0 < p and
A20: p < 1 and
A21: u1 in epigraph f and
A22: u2 in epigraph f;
reconsider pp=p as Real;
thus p*u1 + (1-p)*u2 in epigraph f
proof
consider x2 being Element of X, y2 being Element of REAL such that
A23: u2=[x2,y2] and
A24: f.x2 <= (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 Element of 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 <= (y1) by A21;
f.x1 <> +infty by A27,XXREAL_0:9;
then reconsider w1 = f.x1 as Element of 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: p*w1+(1-p)*w2 in REAL by XREAL_0:def 1;
A31: (p*w1+(1-p)*w2) = (p)*f.x1+(1-p)*f.x2 by Lm12;
then f.(pp*x1+(1-pp)*x2) <> +infty by A18,A19,A20,XXREAL_0:9,A30;
then reconsider w = f.(p*x1+(1-p)*x2) as Element of REAL
by A1,XXREAL_0:14;
A32: p*y1+(1-p)*y2 in REAL by XREAL_0:def 1;
w<=pp*w1+(1-pp)*w2 by A18,A19,A20,A31;
then f.(pp*x1+(1-pp)*x2) <= (p*y1+(1-p)*y2) by A29,XXREAL_0:2;
then
A33: [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 <= (y)} by A32;
p*u1 = [p*x1,p*y1] by A26,Lm1;
then p*u1 + (1-p)*u2 = [p*x1+(1-p)*x2,p*y1+(1-p)*y2] by A25,Lm2;
hence thesis by A33;
end;
end;
then epigraph f is convex by CONVEX1:def 2;
hence thesis;
end;
theorem
for X being RealLinearSpace, 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,
p being Real st 0<=p & p<=1 holds f.(p*x1+(1-p)*
x2) <= (p)*f.x1+(1-p)*f.x2
proof
let X be RealLinearSpace, f be Function of the carrier of X,ExtREAL;
assume
A1: for x being VECTOR of X holds f.x <> -infty;
thus f is convex implies for x1, x2 being VECTOR of X,
p being Real st 0<=p
& p<=1 holds f.(p*x1+(1-p)*x2) <= (p)*f.x1+(1-p)*f.x2
proof
assume
A2: f is convex;
let x1, x2 be VECTOR of X, p be Real;
assume that
A3: 0<=p and
A4: p<=1;
per cases;
suppose
A5: p=0;
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;
A8: (1-p)*f.x2=f.x2 by A5,XXREAL_3:81;
(p)*f.x1=0. by A5;
hence thesis by A7,A8,XXREAL_3:4;
end;
suppose
A9: p=1;
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;
A12: (p)*f.x1=f.x1 by A9,XXREAL_3:81;
(1-p)*f.x2=0. by A9;
hence thesis by A11,A12,XXREAL_3:4;
end;
suppose
A13: p<>0 & p<>1;
then p<1 by A4,XXREAL_0:1;
hence thesis by A1,A2,A3,A13,Th4;
end;
end;
assume for x1, x2 being VECTOR of X,
p being Real st 0<=p & p<=1 holds f.(
p*x1+(1-p)*x2) <= (p)*f.x1+(1-p)*f.x2;
then
for x1, x2 being VECTOR of X,
p being Real st 0<p & p<1 holds f.(p*x1+(
1-p)*x2) <= (p)*f.x1+(1-p)*f.x2;
hence thesis by A1,Th4;
end;
begin :: Relation between notions "function is convex" and "function is convex on set"
theorem
for f being PartFunc of REAL,REAL, g being Function of the carrier of
RLS_Real,ExtREAL, 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, g be Function of the carrier of RLS_Real,
ExtREAL, X be Subset of RLS_Real;
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);
A3: for v being VECTOR of RLS_Real holds g.v <> -infty
proof
let v be VECTOR of RLS_Real;
reconsider x=v as Real;
f.x in REAL by XREAL_0:def 1;
hence thesis by A2;
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;
reconsider x=v as Real;
assume v in X;
then g.x=f.x by A2;
hence thesis by XREAL_0:def 1;
end;
thus g is convex implies f is_convex_on X & X is convex
proof
assume
A5: g is convex;
for p be Real
st 0<=p & p<=1
for x1,x2 be 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;
assume that
A6: 0<=p and
A7: p<=1;
let x1,x2 be Real;
assume that
A8: x1 in X and
A9: x2 in X and
A10: p*x1 + (1-p)*x2 in X;
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;
per cases;
suppose
p=0;
hence thesis;
end;
suppose
p=1;
hence thesis;
end;
suppose
A14: p<>0 & p<>1;
reconsider v2=x2 as VECTOR of RLS_Real by XREAL_0:def 1;
reconsider v1=x1 as VECTOR of RLS_Real by XREAL_0:def 1;
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 = (p)*g.v1+(1-p)*g.v2 by A11,A13,Lm12;
hence thesis by A3,A5,A6,A14,A17,A16,Th4;
end;
end;
hence f is_convex_on X by A1,RFUNCT_3:def 12;
for v1,v2 being VECTOR of RLS_Real, 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, p be Real;
assume that
A18: 0 < p and
A19: p < 1 and
A20: v1 in X and
A21: v2 in X;
reconsider w1=g.v1, w2=g.v2 as Element of REAL by A4,A20,A21;
A22: p*w1+(1-p)*w2 in REAL by XREAL_0:def 1;
A23: p*w1+(1-p)*w2 = (p)*g.v1+(1-p)*g.v2 by Lm12;
g.(p*v1+(1-p)*v2) <= (p)*g.v1+(1-p)*g.v2 by A3,A5,A18,A19,Th4;
then g.(p*v1+(1-p)*v2) <> +infty by A23,XXREAL_0:9,A22;
hence thesis by A2;
end;
hence X is convex by CONVEX1:def 2;
end;
thus f is_convex_on X & X is convex implies g is convex
proof
assume that
A24: f is_convex_on X and
A25: X is convex;
for v1, v2 being VECTOR of RLS_Real, p being Real st 0<p & p<1
holds g.(p*v1+(1-p)*v2) <= (p)*g.v1+(1-p)*g.v2
proof
let v1, v2 be VECTOR of RLS_Real, p be Real;
assume that
A26: 0<p and
A27: p<1;
reconsider x2=v2 as Real;
reconsider x1=v1 as Real;
reconsider p as Real;
A28: 1-p > 0 by A27,XREAL_1:50;
per cases;
suppose
A29: v1 in X & v2 in X;
then
A30: f.x2 = g.v2 by A2;
f.x1 = g.v1 by A2,A29;
then
A31: p*f.x1+(1-p)*f.x2 = (p)*g.v1+(1-p)*g.v2 by A30,Lm12;
A32: (1-p)*v2 = (1-p)*x2 by BINOP_2:def 11;
p*v1 = p*x1 by BINOP_2:def 11;
then
A33: p*v1+(1-p)*v2 = p*x1+(1-p)*x2 by A32,BINOP_2:def 9;
reconsider pc = p*x1+(1-p)*x2 as Real;
A34: p*v1+(1-p)*v2 in X by A25,A26,A27,A29,CONVEX1:def 2;
then f.pc = g.(p*v1+(1-p)*v2) by A2,A33;
hence thesis by A24,A26,A27,A29,A34,A33,A31,RFUNCT_3:def 12;
end;
suppose
A35: v1 in X & not v2 in X;
then g.x2=+infty by A2;
then
A36: (1-p)*g.v2 = +infty by A28,XXREAL_3:def 5;
reconsider w1=g.x1 as Element of REAL by A4,A35;
p*w1 = (p)*g.v1 by EXTREAL1:1;
then (p)*g.v1+(1-p)*g.v2 = +infty by A36,XXREAL_3:def 2;
hence thesis by XXREAL_0:4;
end;
suppose
A37: not v1 in X & v2 in X;
then g.x1=+infty by A2;
then
A38: (p)*g.v1 = +infty by A26,XXREAL_3:def 5;
reconsider w2=g.x2 as Element of REAL by A4,A37;
(1-p)*w2 = (1-p)*g.v2 by EXTREAL1:1;
then (p)*g.v1+(1-p)*g.v2 = +infty by A38,XXREAL_3:def 2;
hence thesis by XXREAL_0:4;
end;
suppose
A39: not v1 in X & not v2 in X;
then g.x2=+infty by A2;
then
A40: (1-p)*g.v2 = +infty by A28,XXREAL_3:def 5;
g.x1=+infty by A2,A39;
then (p)*g.v1+(1-p)*g.v2 = +infty by A26,A40,XXREAL_3:def 2;
hence thesis by XXREAL_0:4;
end;
end;
hence thesis by A3,Th4;
end;
end;
begin :: CONVEX2:6 in other words
theorem Th7:
for X being RealLinearSpace, M being Subset of X holds M is
convex iff for n being non zero Nat, p being FinSequence of REAL, 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, M be Subset of X;
thus M is convex implies for n being non zero Nat, p being FinSequence of
REAL, 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
defpred P[Nat] means for p being FinSequence of REAL, 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;
A2: for n being non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A3: P[n];
thus for p being FinSequence of REAL, 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
proof
let p be FinSequence of REAL, y,z being FinSequence of the carrier of
X;
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;
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 16;
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;
assume
A17: i in dom (p|n);
then
A18: i <= n by A14,FINSEQ_1:1;
p.i > 0 by A8,A14,A15,A17;
hence thesis by A18,FINSEQ_3:112;
end;
set y9 = y|n;
set p9 = (1/q)*(p|n);
deffunc f(Nat) = p9.$1*y9/.$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 = f(i) from
FINSEQ_2:sch 1;
A21: len y9 = n by A5,A12,FINSEQ_1:59;
then
A22: dom y9 = Seg n by FINSEQ_1:def 3;
A23: for i being Nat, v being VECTOR of X st i in dom z9 &
v = (z|n).i holds z9.i = (1/q)*v
proof
let i be Nat, v be VECTOR of X;
assume that
A24: i in dom z9 and
A25: v = (z|n).i;
A26: i in Seg n by A19,A24,FINSEQ_1:def 3;
then
A27: y9/.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 = p9.i*y9/.i by A20,A24
.= ((1/q)*(p|n).i)*y9/.i by RVSUM_1:44
.= ((1/q)*p.i)*y9/.i by A28,FINSEQ_3:112
.= (1/q)*(p.i*y9/.i) by RLVECT_1:def 7
.= (1/q)*v by A8,A15,A25,A26,A29,A27;
hence thesis;
end;
1<=n by NAT_1:14;
then 1 in Seg n by FINSEQ_1:1;
then
A30: q>0 by A11,A14,A16,A10,RVSUM_1:85;
dom p9 = Seg len p9 by FINSEQ_1:def 3;
then Seg len p9 = Seg len(p|n) by A9,VALUED_1:def 5;
then
A31: len p9 = 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: q<1 by A8,A32,XREAL_1:44;
z|n = z | Seg n by FINSEQ_1:def 16;
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-q)*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 p9.i>0 & z9.i=p9.i*y9/.i & y9
/.i in M
proof
q" > 0 by A30;
then
A39: 1/q > 0;
let i be Nat;
assume
A40: i in Seg n;
then
A41: i <= n by FINSEQ_1:1;
A42: p9.i = (1/q)*(p|n).i by RVSUM_1:44
.= (1/q)*p.i by A41,FINSEQ_3:112;
AAA: (1/q)*p.i = (1/q) qua ExtReal *p.i;
A43: Seg n c= Seg(n+1) by A12,FINSEQ_1:5;
then p.i>0 by A8,A40;
hence p9.i>0 by A39,A42,AAA;
thus z9.i = p9.i*y9/.i by A20,A37,A40;
y/.i in M by A8,A40,A43;
hence thesis by A22,A40,FINSEQ_4:70;
end;
len(z|n) = n by A6,A12,FINSEQ_1:59;
then
A44: q*Sum(z9) = q*((1/q)*Sum(z|n)) by A19,A23,RLVECT_1:39
.= (q*(1/q))*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 p9 = (1/q)*q by A11,RVSUM_1:87
.= 1 by A30,XCMPLX_1:106;
then Sum(z9) in M by A3,A19,A31,A21,A38;
hence thesis by A1,A33,A34,A30,A36,A44,CONVEX1:def 2;
end;
end;
A45: P[1]
proof
let p be FinSequence of REAL, y,z be FinSequence of the carrier of X;
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;
reconsider p1 = p.1 as Element of REAL by XREAL_0:def 1;
p = <*p1*> 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 thesis by A53,A52,RLVECT_1:44;
end;
thus for n being non zero Nat holds P[n] from NAT_1:sch 10(A45, A2);
end;
thus (for n being non zero Nat, p being FinSequence of REAL, 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
assume
A54: for n being non zero Nat, p being FinSequence of REAL, y,z being
FinSequence of the carrier of X st len p = n & len y = n & len z = n & Sum p =
1 & (for i being Nat st i in Seg n holds p.i>0 & z.i=p.i*y/.i & y/.i in M)
holds Sum(z) in M;
for x1,x2 being VECTOR of X, r be 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, r be Real;
assume that
A55: 0 < r and
A56: r < 1 and
A57: x1 in M and
A58: x2 in M;
set z = <*r*x1,(1-r)*x2*>;
set y = <*x1,x2*>;
reconsider r as Element of REAL by XREAL_0:def 1;
reconsider r1 = 1- r as Element of REAL by XREAL_0:def 1;
set p = <*r,r1*>;
A59: for i being Nat st i in Seg 2 holds p.i>0 & z.i=p.i*y/.i & y/.i in M
proof
let i be Nat;
assume
A60: i in Seg 2;
per cases by A60,FINSEQ_1:2,TARSKI:def 2;
suppose
A61: i=1;
then
A62: y/.i = x1 by FINSEQ_4:17;
thus thesis by A55,A57,A61,A62;
end;
suppose
A63: i=2;
then
A64: y/.i = x2 by FINSEQ_4:17;
thus thesis by A56,A58,A63,A64,XREAL_1:50;
end;
end;
A65: len y = 2 by FINSEQ_1:44;
A66: Sum p = r+(1-r) by RVSUM_1:77
.= 1;
A67: len z = 2 by FINSEQ_1:44;
len p = 2 by FINSEQ_1:44;
then Sum(z) in M by A54,A65,A67,A66,A59;
hence thesis by RLVECT_1:45;
end;
hence thesis by CONVEX1:def 2;
end;
end;
begin :: Jensen's Inequality
Lm13: for X being RealLinearSpace, f being Function of the carrier of X,
ExtREAL, n being non zero Element of NAT, p being FinSequence of REAL, F being
FinSequence of ExtREAL, y being FinSequence of the carrier of X st len F = n &
(for x being VECTOR of X holds f.x <> -infty) & (for i being Element of NAT st
i in Seg n holds p.i>=0 & F.i = (p.i)*f.(y/.i)) holds not -infty in rng F
proof
let X be RealLinearSpace, f be Function of the carrier of X,ExtREAL, n be
non zero Element of NAT, p being FinSequence of REAL, F be FinSequence of
ExtREAL, y be FinSequence of the carrier of X;
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 = (
p.i)*f.(y/.i);
for i being object st i in dom F holds F.i <> -infty
proof
let i be object;
assume
A4: i in dom F;
then reconsider 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 = (p.i)*f.(y/.i) by A3,A5;
per cases;
suppose
(p.i) = 0.;
hence thesis by A7;
end;
suppose
f.(y/.i) <> +infty;
then reconsider w = f.(y/.i) as Element of REAL by A2,XXREAL_0:14;
F.i = p.i*w by A7,EXTREAL1:1;
hence thesis;
end;
suppose
(p.i) <> 0. & f.(y/.i) = +infty;
hence thesis by A6,A7;
end;
end;
hence thesis by FUNCT_1:def 3;
end;
theorem Th8:
for X being RealLinearSpace, f being Function of the carrier of
X,ExtREAL st (for x being VECTOR of X holds f.x <> -infty) holds f is convex
iff for n being non zero Element of NAT, p being FinSequence of REAL, F being
FinSequence of ExtREAL, y,z being FinSequence of the carrier of X st len p = n
& len F = n & len y = n & len z = n & Sum p = 1 & (for i being Element of NAT
st i in Seg n holds p.i>0 & z.i=p.i*y/.i & F.i = (p.i)*f.(y/.i)) holds f.
Sum(z) <= Sum F
proof
let X be RealLinearSpace, f being Function of the carrier of X,ExtREAL;
assume
A1: for x being VECTOR of X holds f.x <> -infty;
thus f is convex implies for n being non zero Element of NAT, p being
FinSequence of REAL, F being FinSequence of ExtREAL, y,z being FinSequence of
the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 &
(for i being Element of NAT st i in Seg n holds p.i>0 & z.i=p.i*y/.i & F.i =
(p.i)*f.(y/.i)) holds f.Sum(z) <= Sum F
proof
assume
A2: f is convex;
let n be non zero Element of NAT, p be FinSequence of REAL, F be
FinSequence of ExtREAL, y,z be FinSequence of the carrier of X;
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 = (p.i)*f.(y/.i);
for i being Element of NAT st i in Seg n holds p.i>=0 & F.i = (p.
i)*f.(y/.i) by A7;
then
A8: not -infty in rng F by A1,A4,Lm13;
per cases;
suppose
A9: for i being Element of NAT st i in Seg n holds f.(y/.i) <> +infty;
defpred P[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;
assume i in Seg n;
then f.(y/.i) <> +infty by A9;
hence thesis by A1,XXREAL_0:14;
end;
A11: for i being Nat st i in Seg n ex v being Element of V st
P[i,v]
proof
let i be Nat;
assume i in Seg n;
then reconsider w = f.(y/.i) as Element of REAL by A10;
set v = [y/.i, w];
reconsider v as Element of V;
take v;
thus thesis;
end;
consider g being FinSequence of the carrier of V such that
A12: dom g = Seg n and
A13: for i being Nat st i in Seg n holds P[i,g/.i] from
RECDEF_1:sch 17(A11);
A14: len g = n by A12,FINSEQ_1:def 3;
defpred P[set,set] means $2 = F.$1;
A15: for i being Nat st i in Seg n ex w being Element of
RLS_Real st P[i,w]
proof
let i be Nat;
assume
A16: i in Seg n;
then reconsider a = f.(y/.i) as Element of REAL by A10;
F.i = (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 by XREAL_0:def 1;
take w;
thus thesis;
end;
consider F1 being FinSequence of the carrier of RLS_Real such that
A17: dom F1 = Seg n and
A18: for i being Nat st i in Seg n holds P[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 f(Nat) = 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 = f(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;
assume
A24: i in Seg n;
hence p.i>0 by A7;
thus G.i=p.i*g/.i by A21,A22,A24;
reconsider w = f.(y/.i) as Element of REAL by A10,A24;
[y/.i, w] in {[x,a] where x is Element of X, a is Element of REAL
: f.x <= (a)};
hence thesis by A13,A24;
end;
M is convex by A2;
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;
assume
A27: i in Seg n;
then F1/.i = F1.i by A17,PARTFUN1:def 6;
hence thesis by A18,A27;
end;
for i being Nat st i in Seg n holds G.i = [z.i, F1.i]
proof
let i be Nat;
assume
A28: i in Seg n;
then reconsider a = f.(y/.i) as Element of 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 = (p.i)*f.(y/.i) by A7,A28;
then F.i = p.i*a by EXTREAL1:1;
hence thesis by A26,A28,A29;
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 <= (w);
x = Sum z by A30,XTUPLE_0:1;
hence thesis by A30,A31,XTUPLE_0:1;
end;
suppose
ex i being Element of NAT st i in Seg n & f.(y/.i) = +infty;
then consider i being Element of NAT such that
A32: i in Seg n and
A33: f.(y/.i) = +infty;
A34: F.i = (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 thesis by XXREAL_0:4;
end;
end;
thus (for n being non zero Element of NAT, p being FinSequence of REAL, F
being FinSequence of ExtREAL, y,z being FinSequence of the carrier of X st len
p = n & len F = n & len y = n & len z = n & Sum p = 1 & (for i being Element of
NAT st i in Seg n holds p.i>0 & z.i=p.i*y/.i & F.i = (p.i)*f.(y/.i)) holds
f.Sum(z) <= Sum F) implies f is convex
proof
assume
A36: for n being non zero Element of NAT, p being FinSequence of REAL
, F being FinSequence of ExtREAL, y,z being FinSequence of the carrier of X st
len p = n & len F = n & len y = n & len z = n & Sum p = 1 & (for i being
Element of NAT st i in Seg n holds p.i>0 & z.i=p.i*y/.i & F.i = (p.i)*f.(y
/.i)) holds f.Sum(z) <= Sum F;
for x1, x2 being VECTOR of X, q being Real
st 0<q & q<1 holds f.(q*x1
+(1-q)*x2) <= (q)*f.x1+(1-q)*f.x2
proof
set n=2;
let x1, x2 be VECTOR of X, q be Real;
assume that
A37: 0<q and
A38: q<1;
reconsider q1 =q*f.x1, q2=(1-q)*f.x2 as R_eal by XXREAL_0:def 1;
reconsider F=<*q1,q2*> 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 q as Element of REAL by XREAL_0:def 1;
reconsider q1 = 1-q as Element of REAL by XREAL_0:def 1;
reconsider p=<*q,q1*> as FinSequence of REAL;
A39: for i being Element of NAT st i in Seg n holds p.i>0 & z.i=p.i*y/.i
& F.i = (p.i)*f.(y/.i)
proof
let i be Element of NAT;
assume
A40: i in Seg n;
per cases by A40,FINSEQ_1:2,TARSKI:def 2;
suppose
A41: i=1;
then
A42: y/.i=x1 by FINSEQ_4:17;
thus thesis by A37,A41,A42;
end;
suppose
A43: i=2;
then
A44: y/.i=x2 by FINSEQ_4:17;
thus thesis by A38,A43,A44,XREAL_1:50;
end;
end;
A45: len p = n by FINSEQ_1:44;
A46: Sum p = q+(1-q) by RVSUM_1:77
.= 1;
A47: len z = n by FINSEQ_1:44;
A48: Sum z = q*x1+(1-q)*x2 by RLVECT_1:45;
A49: len y = n by FINSEQ_1:44;
A50: len F = n by FINSEQ_1:44;
Sum F = (q)*f.x1+(1-q)*f.x2 by EXTREAL1:9;
hence thesis by A36,A45,A50,A49,A47,A46,A39,A48;
end;
hence thesis by A1,Th4;
end;
end;
Lm14: for F being FinSequence of REAL ex s being Permutation of dom F,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 f(Nat) = $1;
let F be FinSequence of REAL;
defpred P[Nat] means F.$1 <> 0;
defpred R[Nat] means F.$1 = 0;
set A = {f(i) where i is Element of NAT : f(i) in dom F & P[i]};
set B = {f(i) where i is Element of NAT : f(i) in dom F & R[i]};
set N = len F;
A1: A c= dom F from FRAENKEL:sch 17;
then
A2: A c= Seg N by FINSEQ_1:def 3;
reconsider A as finite set by A1;
a2: A is included_in_Seg by A2,FINSEQ_1:def 13;
then
A3: rng(Sgm A)=A by FINSEQ_1:def 14;
A4: B c= dom F from FRAENKEL:sch 17;
then
A5: B c= Seg N by FINSEQ_1:def 3;
reconsider B as finite set by A4;
a5: B is included_in_Seg by A5,FINSEQ_1:def 13;
then
A6: rng(Sgm B)=B by FINSEQ_1:def 14;
for x being object holds not x in A /\ B
proof
let x be object;
assume
A7: x in A /\ B;
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;
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: s 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 object holds x in dom F iff (x in A or x in B)
proof
let x be object;
thus x in dom F implies (x in A or x in B)
proof
assume
A13: x in dom F;
then reconsider x as Element of NAT;
per cases;
suppose
F.x <> 0;
hence thesis by A13;
end;
suppose
F.x = 0;
hence thesis by A13;
end;
end;
thus thesis by A1,A4;
end;
then
A14: A \/ B = dom F by XBOOLE_0:def 3;
then
A15: rng s = dom F by A3,A6,FINSEQ_1:31;
len(Sgm B) = card B by a5,FINSEQ_3:39;
then len s = card A + card B by A12,FINSEQ_1:22
.= card (A \/ B) by A9,CARD_2:40
.= card (Seg N) by A14,FINSEQ_1:def 3;
then
A16: len s = N by FINSEQ_1:57;
then
A17: dom s = Seg N by FINSEQ_1:def 3;
A18: for x being Element of NAT st x in dom F & not x in Seg n ex k being
Element of NAT st x=k+n & k in dom(Sgm B) & s.x=(Sgm B).k
proof
let x be Element of NAT;
assume that
A19: x in dom F and
A20: not x in Seg n;
A21: x in Seg N by A19,FINSEQ_1:def 3;
not(1 <= x & x <= n) by A20,FINSEQ_1:1;
then n+1 <= x by A21,FINSEQ_1:1,INT_1:7;
then
A22: n+1-n <= x-n by XREAL_1:9;
reconsider k=x-n as Element of NAT by A22,INT_1:3;
take k;
len s = n + len(Sgm B) by FINSEQ_1:22;
then
A23: N-n = len(Sgm B) by A16;
x <= N 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+n;
hence thesis by A24,FINSEQ_1:def 7;
end;
dom F = Seg N by FINSEQ_1:def 3;
then reconsider s 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 as Permutation of dom F by A11;
take s,n;
let i be Element of NAT;
assume
A25: i in dom F;
thus i in Seg n implies F.(s.i) <> 0
proof
assume i in Seg n;
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 thesis;
end;
thus F.(s.i) <> 0 implies i in Seg n
proof
assume
A27: F.(s.i) <> 0;
assume not i in Seg n;
then
ex k being Element of NAT st i=k+n & 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 thesis by A27;
end;
end;
theorem
for X being RealLinearSpace, f being Function of the carrier of X,
ExtREAL st (for x being VECTOR of X holds f.x <> -infty) holds f is convex iff
for n being non zero Element of NAT, p being FinSequence of REAL, F being
FinSequence of ExtREAL, y,z being FinSequence of the carrier of X st len p = n
& len F = n & len y = n & len z = n & Sum p = 1 & (for i being Element of NAT
st i in Seg n holds p.i>=0 & z.i=p.i*y/.i & F.i = (p.i)*f.(y/.i)) holds f.
Sum(z) <= Sum F
proof
let X be RealLinearSpace, f being Function of the carrier of X,ExtREAL;
assume
A1: for x being VECTOR of X holds f.x <> -infty;
thus f is convex implies for n being non zero Element of NAT, p being
FinSequence of REAL, F being FinSequence of ExtREAL, y,z being FinSequence of
the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 &
(for i being Element of NAT st i in Seg n holds p.i>=0 & z.i=p.i*y/.i & F.i =
(p.i)*f.(y/.i)) holds f.Sum(z) <= Sum F
proof
assume
A2: f is convex;
let n be non zero Element of NAT, p be FinSequence of REAL, F be
FinSequence of ExtREAL, y,z be FinSequence of the carrier of X;
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 = (p.i)*f.(y/.i);
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;
assume that
A15: 1<=i and
A16: i<=n-k;
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 thesis by A9,A19,A17,A18,FINSEQ_1:1;
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
per cases;
suppose
k >= n;
then z9/^k = <*>(the carrier of X) by A23,FINSEQ_5:32;
hence thesis by RLVECT_1:43;
end;
suppose
A25: k < n;
for w being object 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 object;
assume w in rng(z9/^k);
then consider i being object such that
A26: i in dom(z9/^k) and
A27: (z9/^k).i = w by FUNCT_1:def 3;
reconsider 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 thesis by TARSKI:def 1;
end;
then rng(z9/^k) c= {0.X} by TARSKI:def 3;
hence thesis by Lm11;
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 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
per cases;
suppose
k >= n;
hence thesis by A34,EXTREAL1:7,FINSEQ_5:32;
end;
suppose
A36: k < n;
for w being object 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 object;
assume w in rng(F9/^k);
then consider i being object such that
A37: i in dom(F9/^k) and
A38: (F9/^k).i = w by FUNCT_1:def 3;
reconsider 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)) = (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 thesis by TARSKI:def 1;
end;
then rng(F9/^k) c= {0.} by TARSKI:def 3;
hence thesis by Lm9;
end;
end;
A44: F9|k = F9|(Seg k) by FINSEQ_1:def 16;
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 = (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 16;
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
per cases;
suppose
k >= n;
hence thesis by A51,FINSEQ_5:32,RVSUM_1:72;
end;
suppose
A53: k < n;
for w being object 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 object;
assume w in rng(p9/^k);
then consider i being object such that
A54: i in dom(p9/^k) and
A55: (p9/^k).i = w by FUNCT_1:def 3;
reconsider 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 thesis by TARSKI:def 1;
end;
then rng(p9/^k) c= {0} by TARSKI:def 3;
hence thesis by Lm10;
end;
end;
A60: p9|k = p9|(Seg k) by FINSEQ_1:def 16;
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;
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 16;
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 as non zero 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 = ((p9|k).i)*f.((y9|k)/.i)
proof
let i be Element of NAT;
assume
A72: i in Seg k9;
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 thesis by A8,A77,A94,A91,A86,A93;
end;
Sum(p9|k)=1 by A7,A33,A52,A70,RFINSEQ:9;
hence thesis by A1,A2,A65,A63,A61,A69,A50,A45,A71,Th8;
end;
thus (for n being non zero Element of NAT, p being FinSequence of REAL, F
being FinSequence of ExtREAL, y,z being FinSequence of the carrier of X st len
p = n & len F = n & len y = n & len z = n & Sum p = 1 & (for i being Element of
NAT st i in Seg n holds p.i>=0 & z.i=p.i*y/.i & F.i = (p.i)*f.(y/.i))
holds f.Sum(z) <= Sum F) implies f is convex
proof
assume
A95: for n being non zero Element of NAT, p being FinSequence of
REAL, F being FinSequence of ExtREAL, y,z being FinSequence of the carrier of X
st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & (for i being
Element of NAT st i in Seg n holds p.i>=0 & z.i=p.i*y/.i & F.i = (p.i)*f.(
y/.i)) holds f.Sum(z) <= Sum F;
for n being non zero Element of NAT, p being FinSequence of REAL, F
being FinSequence of ExtREAL, y,z being FinSequence of the carrier of X st len
p = n & len F = n & len y = n & len z = n & Sum p = 1 & (for i being Element of
NAT st i in Seg n holds p.i>0 & z.i=p.i*y/.i & F.i = (p.i)*f.(y/.i)) holds
f.Sum(z) <= Sum F
proof
let n be non zero Element of NAT, p be FinSequence of REAL, F be
FinSequence of ExtREAL, y,z be FinSequence of the carrier of X;
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 = (p.i)*f.(y/.i);
for i being Element of NAT st i in Seg n holds p.i>=0 & z.i=p.i*y
/.i & F.i = (p.i)*f.(y/.i) by A101;
hence thesis by A95,A96,A97,A98,A99,A100;
end;
hence thesis by A1,Th8;
end;
end;