-infty; thus f is convex implies for x1, x2 being VECTOR of X, p being Real st 0

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

+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

-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

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 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;
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 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-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 by XCMPLX_1:215;
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;
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;
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;
p.i = r by A61,FINSEQ_1:44;
hence thesis by A55,A57,A61,A62,FINSEQ_1:44;
end;
suppose
A63: i=2;
then
A64: y/.i = x2 by FINSEQ_4:17;
p.i = 1-r by A63,FINSEQ_1:44;
hence thesis by A56,A58,A63,A64,FINSEQ_1:44,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 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;
p.i=q by A41,FINSEQ_1:44;
hence thesis by A37,A41,A42,FINSEQ_1:44;
end;
suppose
A43: i=2;
then
A44: y/.i=x2 by FINSEQ_4:17;
p.i=1-q by A43,FINSEQ_1:44;
hence thesis by A38,A43,A44,FINSEQ_1:44,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;
A3: rng(Sgm A)=A by A2,FINSEQ_1:def 13;
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;
A6: rng(Sgm B)=B by A5,FINSEQ_1:def 13;
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 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 = (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
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 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;
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 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;