Copyright (c) 2000 Association of Mizar Users
environ
vocabulary PARTFUN1, ARYTM, SQUARE_1, FINSEQ_2, RVSUM_1, FINSEQ_1, VECTSP_1,
RELAT_1, FUNCT_1, ARYTM_1, RLVECT_1, RFUNCT_3, RCOMP_1, ARYTM_3, SEQ_1,
BOOLE, MEASURE5, FCONT_1, SUPINF_1, ABSVALUE, RFUNCT_4;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XCMPLX_0, XREAL_0, RELAT_1,
FUNCT_1, FINSEQ_1, REAL_1, NAT_1, ABSVALUE, FINSEQ_2, SQUARE_1, PARTFUN1,
FINSEQOP, VECTSP_1, SEQ_1, RVSUM_1, RCOMP_1, RFUNCT_3, SUPINF_1,
MEASURE5, FCONT_1;
constructors MONOID_1, REAL_1, NAT_1, FINSEQOP, RCOMP_1, TOPREAL1, FINSEQ_4,
RFUNCT_3, MEASURE5, FCONT_1, MEMBERED;
clusters RELSET_1, FINSEQ_2, XREAL_0, ARYTM_3, MEMBERED;
requirements NUMERALS, SUBSET, REAL, BOOLE, ARITHM;
theorems RCOMP_1, REAL_1, REAL_2, AXIOMS, SQUARE_1, RFUNCT_3, TARSKI,
PARTFUN1, SEQ_1, FINSEQ_1, FINSEQ_2, RVSUM_1, NAT_1, MEASURE5, MEASURE6,
FCONT_1, ABSVALUE, FUNCT_1, XREAL_0, XBOOLE_1, XCMPLX_0, XCMPLX_1;
schemes NAT_1;
begin :: Some useful properties of n-tuples_on REAL
reserve a,b,r,s,x0,x for Real;
reserve f,g for PartFunc of REAL,REAL;
reserve X,Y for set;
reserve k for Nat;
theorem Th1:
for a, b being real number holds max(a,b) >= min(a,b)
proof
let a, b be real number;
per cases by SQUARE_1:38;
suppose min(a,b)=a;
hence thesis by SQUARE_1:46;
suppose min(a,b)=b;
hence thesis by SQUARE_1:46;
end;
theorem Th2:
for n being Nat, R1,R2 being Element of n-tuples_on REAL, r1,r2 being Real
holds mlt(R1^<*r1*>,R2^<*r2*>)=mlt(R1,R2)^<*r1*r2*>
proof
let n be Nat;
let R1,R2 be Element of n-tuples_on REAL;
let r1,r2 be Real;
A1:mlt(R1^<*r1*>,R2^<*r2*>) is Element of (n+1)-tuples_on REAL
proof
A2: len (R1^<*r1*>) = len R1 + 1 by FINSEQ_2:19 .= n+1 by FINSEQ_2:109
.= len R2 + 1 by FINSEQ_2:109 .= len (R2^<*r2*>) by FINSEQ_2:19;
len(mlt(R1^<*r1*>,R2^<*r2*>))
=len(multreal.:(R1^<*r1*>,R2^<*r2*>)) by RVSUM_1:def 9
.= len (R1^<*r1*>) by A2,FINSEQ_2:86
.= len R1 + 1 by FINSEQ_2:19 .= n+1 by FINSEQ_2:109;
hence thesis by FINSEQ_2:110;
end;
A3:mlt(R1,R2)^<*r1*r2*> is Element of (n+1)-tuples_on REAL
proof
A4: len R1 = n by FINSEQ_2:109 .= len R2 by FINSEQ_2:109;
len(mlt(R1,R2))=len(multreal.:(R1,R2)) by RVSUM_1:def 9
.= len R1 by A4,FINSEQ_2:86
.= n by FINSEQ_2:109;
then len(mlt(R1,R2)^<*r1*r2*>)= n+1 by FINSEQ_2:19;
hence thesis by FINSEQ_2:110;
end;
for k being Nat st k in Seg (n+1) holds
mlt(R1^<*r1*>,R2^<*r2*>).k = (mlt(R1,R2)^<*r1*r2*>).k
proof
let k be Nat such that
A5: k in Seg (n+1);
A6: 1<=k & k<=n+1 by A5,FINSEQ_1:3;
now per cases by A6,REAL_1:def 5;
suppose k<n+1;
then 1<=k & k<=n by A5,FINSEQ_1:3,NAT_1:38;
then A7: k in Seg n by FINSEQ_1:3;
then k in Seg len R1 & k in Seg len R2 by FINSEQ_2:109;
then k in dom R1 & k in dom R2 by FINSEQ_1:def 3;
then A8: (R1^<*r1*>).k = R1.k & (R2^<*r2*>).k = R2.k by FINSEQ_1:def 7;
k in Seg len (mlt(R1^<*r1*>,R2^<*r2*>)) by A1,A5,FINSEQ_2:109;
then k in dom(mlt(R1^<*r1*>,R2^<*r2*>)) by FINSEQ_1:def 3;
then A9: mlt(R1^<*r1*>,R2^<*r2*>).k = (R1.k)*(R2.k) by A8,RVSUM_1:86;
n+1 = len (mlt(R1,R2)) + 1 by FINSEQ_2:109;
then len (mlt(R1,R2)) = n+1-1 by XCMPLX_1:26 .= n by XCMPLX_1:26;
then A10: k in dom mlt(R1,R2) by A7,FINSEQ_1:def 3;
then (mlt(R1,R2)^<*r1*r2*>).k = mlt(R1,R2).k by FINSEQ_1:def 7;
hence thesis by A9,A10,RVSUM_1:86;
suppose A11:k=n+1;
then k=len R1+1 & k=len R2+1 by FINSEQ_2:109;
then A12: (R1^<*r1*>).k=r1 & (R2^<*r2*>).k=r2 by FINSEQ_1:59;
k in Seg len (mlt(R1^<*r1*>,R2^<*r2*>)) by A1,A5,FINSEQ_2:109;
then k in dom(mlt(R1^<*r1*>,R2^<*r2*>)) by FINSEQ_1:def 3;
then A13: mlt(R1^<*r1*>,R2^<*r2*>).k = r1*r2 by A12,RVSUM_1:86;
n+1 = len (mlt(R1,R2)) + 1 by FINSEQ_2:109;
hence thesis by A11,A13,FINSEQ_1:59;
end;
hence thesis;
end;
hence thesis by A1,A3,FINSEQ_2:139;
end;
theorem Th3:
for n being Nat, R being Element of n-tuples_on REAL st Sum R=0 &
(for i being Nat st i in dom R holds 0 <= R.i) holds
for i being Nat st i in dom R holds R.i = 0
proof
let n be Nat, R be Element of n-tuples_on REAL such that
A1:Sum R=0 & (for i being Nat st i in dom R holds 0 <= R.i);
given k being Nat such that
A2:k in dom R & R.k <> 0;
0 <= R.k by A1,A2;
hence contradiction by A1,A2,RVSUM_1:115;
end;
theorem Th4:
for n being Nat, R being Element of n-tuples_on REAL st
(for i being Nat st i in dom R holds 0 = R.i) holds
R = n |-> (0 qua Real)
proof
let n be Nat, R be Element of n-tuples_on REAL such that
A1:for i being Nat st i in dom R holds 0 = R.i;
A2:len R = n by FINSEQ_2:109 .= len (n |-> 0) by FINSEQ_2:69;
for k st 1 <= k & k <= len R holds R.k = (n |-> 0).k
proof
let k such that
A3: 1 <= k & k <= len R;
A4: k in Seg len R by A3,FINSEQ_1:3;
then k in dom R by FINSEQ_1:def 3;
then A5: R.k = 0 by A1;
k in Seg n by A4,FINSEQ_2:109;
hence thesis by A5,FINSEQ_2:70;
end;
hence thesis by A2,FINSEQ_1:18;
end;
theorem Th5:
for n being Nat, R being Element of n-tuples_on REAL
holds mlt(n |-> (0 qua Real),R) = n |-> (0 qua Real)
proof
let n be Nat, R be Element of n-tuples_on REAL;
A1:len (n |-> (0 qua Real)) = n by FINSEQ_2:69
.= len R by FINSEQ_2:109;
A2:len(mlt(n |-> (0 qua Real),R))
=len(multreal.:(n |-> (0 qua Real),R)) by RVSUM_1:def 9
.=len (n |-> (0 qua Real)) by A1,FINSEQ_2:86
.=n by FINSEQ_2:109;
A3:len (n |-> (0 qua Real)) = n by FINSEQ_2:69;
for k st 1 <= k & k <= len mlt(n |-> (0 qua Real),R) holds
mlt(n |-> (0 qua Real),R).k = (n |-> (0 qua Real)).k
proof
let k such that
A4: 1 <= k & k <= len mlt(n |-> (0 qua Real),R);
A5: k in Seg len mlt(n |-> (0 qua Real),R) by A4,FINSEQ_1:3;
mlt(n |-> (0 qua Real),R).k = (n |-> (0 qua Real)).k*R.k by RVSUM_1:87
.=0*R.k by A2,A5,FINSEQ_2:70;
hence thesis by A2,A5,FINSEQ_2:70;
end;
hence thesis by A2,A3,FINSEQ_1:18;
end;
begin :: Convex and strictly convex functions
definition let f, X;
pred f is_strictly_convex_on X means :Def1:
X c= dom f &
for p being Real st 0<p & p<1 holds
for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s;
end;
theorem Th6:
f is_strictly_convex_on X implies f is_convex_on X
proof
assume A1:f is_strictly_convex_on X;
then A2:X c= dom f &
for p being Real st 0<p & p<1 holds
for r,s be Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s by Def1;
for p being Real st 0<=p & p<=1 holds
for r,s being Real st r in X & s in X & p*r + (1-p)*s in X holds
f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s
proof
let p be Real;
assume A3:0<=p & p<=1;
for r,s being Real st r in X & s in X & p*r+(1-p)*s in X holds
f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s
proof
let r,s be Real;
assume A4:r in X & s in X & p*r+(1-p)*s in X;
now per cases by A3,REAL_1:def 5;
suppose p=0;
hence f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s;
suppose p=1;
hence f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s;
suppose A5:0<p & p<1;
now per cases;
suppose A6:r=s;
then A7: f.(p*r+(1-p)*s) = f.(1*r-p*r+p*r) by XCMPLX_1:40
.=f.(r-(p*r-p*r)) by XCMPLX_1:37
.=f.r by XCMPLX_1:17;
p*f.r + (1-p)*f.s = 1*f.r-p*f.r+p*f.r by A6,XCMPLX_1:40
.=f.r-(p*f.r-p*f.r) by XCMPLX_1:37;
hence f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s by A7,XCMPLX_1:17;
suppose r<>s;
hence thesis by A1,A4,A5,Def1;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis by A2,RFUNCT_3:def 13;
end;
theorem
for a,b be Real, f be PartFunc of REAL,REAL holds
f is_strictly_convex_on [.a,b.] iff
[.a,b.] c= dom f & for p be Real st 0<p & p<1 holds
for r,s be Real st r in [.a,b.] & s in [.a,b.] & r <> s holds
f.(p*r+(1-p)*s) < p*f.r + (1-p)*f.s
proof
let a,b be Real, f be PartFunc of REAL,REAL;
set ab = {r where r is Real: a<=r & r<=b};
A1: [.a,b.]= ab by RCOMP_1:def 1;
thus f is_strictly_convex_on [.a,b.] implies
[.a,b.] c= dom f & for p be Real st 0<p & p<1 holds
for x,y be Real st x in [.a,b.] & y in [.a,b.] & x <> y holds
f.(p*x + (1-p)*y) < p*f.x + (1-p)*f.y
proof
assume A2: f is_strictly_convex_on [.a,b.];
hence [.a,b.] c= dom f by Def1;
let p be Real;
assume A3: 0<p & p<1;
then A4: 0<=1-p by SQUARE_1:12;
let x,y be Real;
assume A5: x in [.a,b.] & y in [.a,b.] & x <> y;
then A6: (ex r1 be Real st r1=x & a<=r1 & r1<=b) &
ex r2 be Real st r2=y & a<=r2 & r2<=b by A1;
then A7: p*a<=p*x & p*x<=p*b by A3,AXIOMS:25;
A8: (1-p)*a<=(1-p)*y & (1-p)*y<=(1-p)*b by A4,A6,AXIOMS:25;
p*a+(1-p)*a=p*a+(1*a-p*a) by XCMPLX_1:40
.=a by XCMPLX_1:27;
then A9: a<=p*x+(1-p)*y by A7,A8,REAL_1:55;
p*b+(1-p)*b=p*b+(1*b-p*b) by XCMPLX_1:40
.=b by XCMPLX_1:27;
then p*x+(1-p)*y<=b by A7,A8,REAL_1:55;
then p*x+(1-p)*y in ab by A9;
hence thesis by A1,A2,A3,A5,Def1;
end;
assume A10: [.a,b.] c= dom f & for p be Real st 0<p & p<1 holds
for x,y be Real st x in [.a,b.] & y in [.a,b.] & x <> y holds
f.(p*x + (1-p)*y) < p*f.x + (1-p)*f.y;
hence [.a,b.] c= dom f;
let p be Real;
assume A11: 0<p & p<1;
let x,y be Real;
assume x in [.a,b.] & y in [.a,b.] & p*x + (1-p)*y in [.a,b.];
hence thesis by A10,A11;
end;
theorem
for X being set, f being PartFunc of REAL,REAL holds
f is_convex_on X iff
X c= dom f & for a,b,c being Real st a in X & b in X & c in X &
a<b & b<c holds f.b <=((c-b)/(c-a))*f.a + ((b-a)/(c-a))*f.c
proof
let X be set, f be PartFunc of REAL,REAL;
A1:f is_convex_on X implies
X c= dom f & for a,b,c being Real st a in X & b in X & c in X &
a<b & b<c holds f.b <=((c-b)/(c-a))*f.a + ((b-a)/(c-a))*f.c
proof
assume A2:f is_convex_on X;
for a,b,c being Real st a in X & b in X & c in X & a < b & b < c
holds f.b <=((c-b)/(c-a))*f.a + ((b-a)/(c-a))*f.c
proof
let a,b,c be Real; assume A3:a in X & b in X & c in X & a < b & b < c;
then A4: c-b < c-a & 0 < c-b by REAL_2:105,SQUARE_1:11;
then 0 < c-a by AXIOMS:22;
then A5: 0 < (c-b)/(c-a) & (c-b)/(c-a) < 1 by A4,REAL_2:127,142;
set p = (c-b)/(c-a);
1-p = (b-a)/(c-a) & p*a + (1-p)*c = b
proof
p+(b-a)/(c-a) = ((c-b)+(b-a))/(c-a) by XCMPLX_1:63
.= (c-a)/(c-a) by XCMPLX_1:39
.= 1 by A4,XCMPLX_1:60;
hence 1-p = (b-a)/(c-a) by XCMPLX_1:26;
then p*a + (1-p)*c
= (a*(c-b))/(c-a)+c*((b-a)/(c-a)) by XCMPLX_1:75
.= (a*(c-b))/(c-a)+(c*(b-a))/(c-a) by XCMPLX_1:75
.= ((c-b)*a + (b-a)*c)/(c-a) by XCMPLX_1:63
.= ((c*a-b*a)+(b-a)*c)/(c-a) by XCMPLX_1:40
.= ((c*a-b*a)+(b*c-a*c))/(c-a) by XCMPLX_1:40
.= (b*c-b*a)/(c-a) by XCMPLX_1:39
.= b*(c-a)/(c-a) by XCMPLX_1:40;
hence thesis by A4,XCMPLX_1:90;
end;
hence thesis by A2,A3,A5,RFUNCT_3:def 13;
end;
hence thesis by A2,RFUNCT_3:def 13;
end;
(X c= dom f & for a,b,c being Real st a in X & b in X & c in X &
a<b & b<c holds f.b <=((c-b)/(c-a))*f.a + ((b-a)/(c-a))*f.c) implies
f is_convex_on X
proof
assume that
A6:X c= dom f and A7:for a,b,c being Real st a in X & b in X & c in X &
a<b & b<c holds f.b <=((c-b)/(c-a))*f.a + ((b-a)/(c-a))*f.c;
for p being Real st 0<=p & p<=1 holds
for r,s being Real st r in X & s in X & p*r + (1-p)*s in X holds
f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s
proof
let p be Real;
assume A8:0<=p & p<=1;
for r,s being Real st r in X & s in X & p*r + (1-p)*s in X holds
f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s
proof
let r,s be Real;
assume A9: r in X & s in X & p*r + (1-p)*s in X;
f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s
proof
now per cases by A8,REAL_1:def 5;
suppose p=0;
hence f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s;
suppose p=1;
hence f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s;
suppose A10:0<p & p<1;
then 1 < 1+p by REAL_1:69;
then A11: 0 < 1-p & 1-p < 1 by A10,REAL_1:84,SQUARE_1:11;
now per cases by REAL_1:def 5;
suppose A12:r=s;
then A13: p*r+(1-p)*s = 1*r-p*r+p*r by XCMPLX_1:40 .= r-(p*r-p*r) by
XCMPLX_1:37
.= r by XCMPLX_1:17;
p*f.r + (1-p)*f.s = 1*f.r-p*f.r+p*f.r by A12,XCMPLX_1:40
.= f.r-(p*f.r-p*f.r) by XCMPLX_1:37 .= f.r by XCMPLX_1:17;
hence f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s by A13;
suppose r>s;
then A14: r-s > 0 by SQUARE_1:11;
set t = p*r + (1-p)*s;
A15: t - s = p*r + ((1-p)*s - s) by XCMPLX_1:29
.=p*r + (1*s - p*s - s) by XCMPLX_1:40
.=p*r + (-p*s + s - s) by XCMPLX_0:def 8
.=p*r + (-p*s) by XCMPLX_1:26
.=p*r - p*s by XCMPLX_0:def 8
.=p*(r-s) by XCMPLX_1:40;
then t - s > 0 by A10,A14,REAL_2:122;
then A16: s < t by REAL_2:106;
A17: r - t = 1*r - p*r - (1-p)*s by XCMPLX_1:36
.= (1-p)*r - (1-p)*s by XCMPLX_1:40
.= (1-p)*(r-s) by XCMPLX_1:40;
then r - t > 0 by A11,A14,REAL_2:122;
then A18: t < r by REAL_2:106;
(r-t)/(r-s)=(1-p) & (t-s)/(r-s)=p by A14,A15,A17,XCMPLX_1:90
;
hence f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s by A7,A9,A16,A18;
suppose r<s;
then A19: s-r > 0 by SQUARE_1:11;
set t = p*r + (1-p)*s;
A20: t - r = p*r - 1*r + (1-p)*s by XCMPLX_1:29
.= (p-1)*r + (1-p)*s by XCMPLX_1:40
.= -(1-p)*r + (1-p)*s by XCMPLX_1:186
.= (1-p)*s - (1-p)*r by XCMPLX_0:def 8
.= (1-p)*(s-r) by XCMPLX_1:40;
then t - r > 0 by A11,A19,REAL_2:122;
then A21: r < t by REAL_2:106;
A22: s - t = 1*s - (1-p)*s - p*r by XCMPLX_1:36
.= (1-(1-p))*s - p*r by XCMPLX_1:40
.= (1-1+p)*s - p*r by XCMPLX_1:37
.= p*(s-r) by XCMPLX_1:40;
then s - t > 0 by A10,A19,REAL_2:122;
then A23: t < s by REAL_2:106;
(s-t)/(s-r)=p & (t-r)/(s-r)=1-p by A19,A20,A22,XCMPLX_1:90;
hence thesis by A7,A9,A21,A23;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis by A6,RFUNCT_3:def 13;
end;
hence thesis by A1;
end;
theorem
for X being set, f being PartFunc of REAL,REAL holds
f is_strictly_convex_on X iff
X c= dom f & for a,b,c being Real st a in X & b in X & c in X &
a<b & b<c holds f.b < ((c-b)/(c-a))*f.a + ((b-a)/(c-a))*f.c
proof
let X be set;
let f be PartFunc of REAL,REAL;
A1:f is_strictly_convex_on X implies
X c= dom f & for a,b,c being Real st a in X & b in X & c in X &
a<b & b<c holds f.b < ((c-b)/(c-a))*f.a + ((b-a)/(c-a))*f.c
proof
assume A2:f is_strictly_convex_on X;
for a,b,c being Real st a in X & b in X & c in X & a < b & b < c
holds f.b <((c-b)/(c-a))*f.a + ((b-a)/(c-a))*f.c
proof
let a,b,c be Real; assume A3:a in X & b in X & c in X & a < b & b < c;
then A4: c-b < c-a & 0 < c-b by REAL_2:105,SQUARE_1:11;
then 0 < c-a by AXIOMS:22;
then A5: 0 < (c-b)/(c-a) & (c-b)/(c-a) < 1 by A4,REAL_2:127,142;
set p = (c-b)/(c-a);
1-p = (b-a)/(c-a) & p*a + (1-p)*c = b
proof
p+(b-a)/(c-a) = ((c-b)+(b-a))/(c-a) by XCMPLX_1:63
.= (c-a)/(c-a) by XCMPLX_1:39
.= 1 by A4,XCMPLX_1:60;
hence 1-p = (b-a)/(c-a) by XCMPLX_1:26;
then p*a + (1-p)*c
= (a*(c-b))/(c-a)+c*((b-a)/(c-a)) by XCMPLX_1:75
.= (a*(c-b))/(c-a)+(c*(b-a))/(c-a) by XCMPLX_1:75
.= ((c-b)*a + (b-a)*c)/(c-a) by XCMPLX_1:63
.= ((c*a-b*a)+(b-a)*c)/(c-a) by XCMPLX_1:40
.= ((c*a-b*a)+(b*c-a*c))/(c-a) by XCMPLX_1:40
.= (b*c-b*a)/(c-a) by XCMPLX_1:39
.= b*(c-a)/(c-a) by XCMPLX_1:40;
hence thesis by A4,XCMPLX_1:90;
end;
hence thesis by A2,A3,A5,Def1;
end;
hence thesis by A2,Def1;
end;
(X c= dom f & for a,b,c being Real st a in X & b in X & c in X &
a<b & b<c holds f.b < ((c-b)/(c-a))*f.a + ((b-a)/(c-a))*f.c) implies
f is_strictly_convex_on X
proof
assume that
A6:X c= dom f and A7:for a,b,c being Real st a in X & b in X & c in X &
a<b & b<c holds f.b < ((c-b)/(c-a))*f.a + ((b-a)/(c-a))*f.c;
for p being Real st 0<p & p<1 holds
for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s
proof
let p be Real; assume A8:0<p & p<1;
for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & r <> s
holds
f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s
proof
let r,s be Real;
assume A9: r in X & s in X & p*r + (1-p)*s in X & r <> s;
f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s
proof
now per cases by A8;
suppose A10:0<p & p<1;
then 1 < 1+p by REAL_1:69;
then A11: 0 < 1-p & 1-p < 1 by A10,REAL_1:84,SQUARE_1:11;
now per cases by A9,REAL_1:def 5;
suppose r>s;
then A12: r-s > 0 by SQUARE_1:11;
set t = p*r + (1-p)*s;
A13: t - s = p*r + ((1-p)*s - s) by XCMPLX_1:29
.=p*r + (1*s - p*s - s) by XCMPLX_1:40
.=p*r + (-p*s + s - s) by XCMPLX_0:def 8
.=p*r + (-p*s) by XCMPLX_1:26
.=p*r - p*s by XCMPLX_0:def 8
.=p*(r-s) by XCMPLX_1:40;
then t - s > 0 by A10,A12,REAL_2:122;
then A14: s < t by REAL_2:106;
A15: r - t = 1*r - p*r - (1-p)*s by XCMPLX_1:36
.= (1-p)*r - (1-p)*s by XCMPLX_1:40
.= (1-p)*(r-s) by XCMPLX_1:40;
then r - t > 0 by A11,A12,REAL_2:122;
then A16: t < r by REAL_2:106;
(r-t)/(r-s)=(1-p) & (t-s)/(r-s)=p by A12,A13,A15,XCMPLX_1:90
;
hence f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s by A7,A9,A14,A16;
suppose r<s;
then A17: s-r > 0 by SQUARE_1:11;
set t = p*r + (1-p)*s;
A18: t - r = p*r - 1*r + (1-p)*s by XCMPLX_1:29
.= (p-1)*r + (1-p)*s by XCMPLX_1:40
.= -(1-p)*r + (1-p)*s by XCMPLX_1:186
.= (1-p)*s - (1-p)*r by XCMPLX_0:def 8
.= (1-p)*(s-r) by XCMPLX_1:40;
then t - r > 0 by A11,A17,REAL_2:122;
then A19: r < t by REAL_2:106;
A20: s - t = 1*s - (1-p)*s - p*r by XCMPLX_1:36
.= (1-(1-p))*s - p*r by XCMPLX_1:40
.= (1-1+p)*s - p*r by XCMPLX_1:37
.= p*(s-r) by XCMPLX_1:40;
then s - t > 0 by A10,A17,REAL_2:122;
then A21: t < s by REAL_2:106;
(s-t)/(s-r)=p & (t-r)/(s-r)=1-p by A17,A18,A20,XCMPLX_1:90;
hence thesis by A7,A9,A19,A21;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis by A6,Def1;
end;
hence thesis by A1;
end;
theorem
f is_strictly_convex_on X & Y c= X implies f is_strictly_convex_on Y
proof
assume A1:f is_strictly_convex_on X & Y c= X;
then X c= dom f &
for p being Real st 0<p & p<1 holds
for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s by Def1;
then A2:Y c= dom f by A1,XBOOLE_1:1;
for p being Real st 0<p & p<1 holds
for r,s being Real st r in Y & s in Y & p*r + (1-p)*s in Y & r <> s holds
f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s by A1,Def1;
hence thesis by A2,Def1;
end;
Lm1:
(1-a)*b+a*b = b & b-(1-a)*b=a*b & b-a*b=(1-a)*b
proof
(1-a)*b+a*b = 1*b-a*b+a*b by XCMPLX_1:40 .= b-(a*b-a*b) by XCMPLX_1:37;
hence (1-a)*b+a*b = b by XCMPLX_1:17;
hence thesis by XCMPLX_1:26;
end;
Lm2:
f is_strictly_convex_on X implies f-r is_strictly_convex_on X
proof
assume A1:f is_strictly_convex_on X;
then X c= dom f &
for p being Real st 0<p & p<1 holds
for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s by Def1;
then A2:X c= dom(f-r) by RFUNCT_3:def 12;
for p being Real st 0<p & p<1 holds
for t,s being Real st t in X & s in X & p*t + (1-p)*s in X & t <> s holds
(f-r).(p*t + (1-p)*s) < p*(f-r).t + (1-p)*(f-r).s
proof
let p be Real; assume A3:0<p & p<1;
for t,s being Real st t in X & s in X & p*t + (1-p)*s in X & t <> s holds
(f-r).(p*t + (1-p)*s) < p*(f-r).t + (1-p)*(f-r).s
proof
let t,s be Real; assume
A4:t in X & s in X & p*t + (1-p)*s in X & t <> s;
then f.(p*t + (1-p)*s) < p*f.t + (1-p)*f.s by A1,A3,Def1;
then A5: f.(p*t + (1-p)*s)-r < p*f.t + (1-p)*f.s - r by REAL_1:54;
(f-r).t = f.t-r & (f-r).s = f.s-r &
(f-r).(p*t + (1-p)*s) = f.(p*t + (1-p)*s)-r by A2,A4,RFUNCT_3:def 12;
then p*(f-r).t + (1-p)*(f-r).s = p*f.t-p*r + (1-p)*(f.s-r) by XCMPLX_1:40
.=(1-p)*(f.s-r)-p*r+p*f.t by XCMPLX_1:30
.=(1-p)*f.s-(1-p)*r-p*r+p*f.t by XCMPLX_1:40
.=(1-p)*f.s-((1-p)*r+p*r)+p*f.t by XCMPLX_1:36
.=(1-p)*f.s-r+p*f.t by Lm1
.=p*f.t + (1-p)*f.s - r by XCMPLX_1:29;
hence thesis by A2,A4,A5,RFUNCT_3:def 12;
end;
hence thesis;
end;
hence thesis by A2,Def1;
end;
theorem
f is_strictly_convex_on X iff f-r is_strictly_convex_on X
proof
A1:dom((f-r)-(-r))=dom(f-r) by RFUNCT_3:def 12;
A2:dom(f-r) = dom f by RFUNCT_3:def 12;
for x being Element of REAL st x in dom (f-r) holds
((f-r)-(-r)).x = f.x
proof
let x be Element of REAL;
assume A3:x in dom (f-r);
then ((f-r)-(-r)).x=(f-r).x-(-r) by A1,RFUNCT_3:def 12 .=(f-r).x+r by
XCMPLX_1:151
.=f.x-r+r by A3,RFUNCT_3:def 12 .= f.x-(r-r) by XCMPLX_1:37;
hence thesis by XCMPLX_1:17;
end;
then (f-r)-(-r) = f by A1,A2,PARTFUN1:34;
hence thesis by Lm2;
end;
Lm3:
0<r implies (f is_strictly_convex_on X implies r(#)f is_strictly_convex_on X)
proof
assume A1:0<r;
assume A2:f is_strictly_convex_on X;
then X c= dom f &
for p being Real st 0<p & p<1 holds
for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s by Def1;
then A3:X c= dom(r(#)f) by SEQ_1:def 6;
for p being Real st 0<p & p<1 holds
for t,s being Real st t in X & s in X & p*t + (1-p)*s in X & t <> s holds
(r(#)f).(p*t + (1-p)*s) < p*(r(#)f).t + (1-p)*(r(#)f).s
proof
let p be Real; assume A4:0<p & p<1;
for t,s being Real st t in X & s in X & p*t + (1-p)*s in X & t <> s holds
(r(#)f).(p*t + (1-p)*s) < p*(r(#)f).t + (1-p)*(r(#)f).s
proof
let t,s be Real;
assume A5:t in X & s in X & p*t + (1-p)*s in X & t <> s;
then f.(p*t + (1-p)*s) < p*f.t + (1-p)*f.s by A2,A4,Def1;
then r*(f.(p*t + (1-p)*s)) < r*(p*f.t + (1-p)*f.s) by A1,REAL_1:70;
then r*(f.(p*t + (1-p)*s)) < p*f.t*r + (1-p)*f.s*r by XCMPLX_1:8;
then A6: r*(f.(p*t + (1-p)*s)) < p*(r*f.t) + (1-p)*f.s*r by XCMPLX_1:4;
(r(#)f).(p*t + (1-p)*s) = r*(f.(p*t + (1-p)*s)) &
p*(r(#)f).t=p*(r*f.t) & (1-p)*(r(#)
f).s = (1-p)*(r*f.s) by A3,A5,SEQ_1:def 6;
hence thesis by A6,XCMPLX_1:4;
end;
hence thesis;
end;
hence thesis by A3,Def1;
end;
theorem Th12:
0<r implies (f is_strictly_convex_on X iff r(#)f is_strictly_convex_on X)
proof
assume A1:0<r;
then A2:0 < 1/r by REAL_2:127;
A3:dom((1/r)(#)(r(#)f))=dom(r(#)f) & dom(r(#)f) = dom f by SEQ_1:def 6;
for x being Element of REAL st x in dom(r(#)f) holds
((1/r)(#)(r(#)f)).x = f.x
proof
let x be Element of REAL;
assume A4:x in dom (r(#)f);
then ((1/r)(#)(r(#)f)).x = (1/r)*(r(#)f).x by A3,SEQ_1:def 6
.= (1/r)*(r*f.x) by A4,SEQ_1:def 6
.= (1/r)*r*f.x by XCMPLX_1:4
.= 1*f.x by A1,XCMPLX_1:107;
hence thesis;
end;
then (1/r)(#)(r(#)f)=f by A3,PARTFUN1:34;
hence thesis by A1,A2,Lm3;
end;
theorem Th13:
f is_strictly_convex_on X & g is_strictly_convex_on X implies
f+g is_strictly_convex_on X
proof
assume A1:f is_strictly_convex_on X & g is_strictly_convex_on X;
then A2:X c= dom f &
for p be Real st 0<p & p<1 holds
for r,s be Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s by Def1;
X c= dom g &
for p be Real st 0<p & p<1 holds
for r,s be Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
g.(p*r + (1-p)*s) < p*g.r + (1-p)*g.s by A1,Def1;
then X c= dom f /\ dom g by A2,XBOOLE_1:19;
then A3:X c= dom (f+g) by SEQ_1:def 3;
for p be Real st 0<p & p<1 holds
for r,s be Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
(f+g).(p*r + (1-p)*s) < p*(f+g).r + (1-p)*(f+g).s
proof
let p be Real; assume A4:0<p & p<1;
for r,s be Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
(f+g).(p*r + (1-p)*s) < p*(f+g).r + (1-p)*(f+g).s
proof
let r,s be Real;
assume A5:r in X & s in X & p*r + (1-p)*s in X & r <> s;
then A6: f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s &
g.(p*r + (1-p)*s) < p*g.r + (1-p)*g.s by A1,A4,Def1;
A7: (p*f.r+(1-p)*f.s)+(p*g.r+(1-p)*g.s)
= p*f.r+ ((p*g.r+(1-p)*g.s)+(1-p)*f.s) by XCMPLX_1:1
.= p*f.r+ (p*g.r+ ((1-p)*g.s+(1-p)*f.s)) by XCMPLX_1:1
.= p*f.r+p*g.r+ ((1-p)*g.s+(1-p)*f.s) by XCMPLX_1:1
.= p*(f.r+g.r) + ((1-p)*g.s+(1-p)*f.s) by XCMPLX_1:8
.= p*(f.r+g.r) + (1-p)*(f.s+g.s) by XCMPLX_1:8;
(f+g).(p*r + (1-p)*s) = f.(p*r+(1-p)*s)+g.(p*r+(1-p)*s) &
(f+g).r = (f.r+g.r) & (f+g).s = (f.s+g.s) by A3,A5,SEQ_1:def 3;
hence thesis by A6,A7,REAL_1:67;
end;
hence thesis;
end;
hence thesis by A3,Def1;
end;
theorem Th14:
f is_strictly_convex_on X & g is_convex_on X implies
f+g is_strictly_convex_on X
proof
assume A1:f is_strictly_convex_on X & g is_convex_on X;
then X c= dom f & X c= dom g by Def1,RFUNCT_3:def 13;
then X c= dom f /\ dom g by XBOOLE_1:19;
then A2:X c= dom (f+g) by SEQ_1:def 3;
for p being Real st 0<p & p<1 holds
for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
(f+g).(p*r + (1-p)*s) < p*(f+g).r + (1-p)*(f+g).s
proof
let p be Real;
assume A3:0<p & p<1;
for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
(f+g).(p*r + (1-p)*s) < p*(f+g).r + (1-p)*(f+g).s
proof
let r,s be Real;
assume A4:r in X & s in X & p*r + (1-p)*s in X & r <> s;
then A5: f.(p*r+(1-p)*s) < p*f.r+(1-p)*f.s &
g.(p*r+(1-p)*s) <= p*g.r+(1-p)*g.s by A1,A3,Def1,RFUNCT_3:def 13;
A6: (p*f.r+(1-p)*f.s)+(p*g.r+(1-p)*g.s)
= p*f.r+ ((p*g.r+(1-p)*g.s)+(1-p)*f.s) by XCMPLX_1:1
.= p*f.r+ (p*g.r+ ((1-p)*g.s+(1-p)*f.s)) by XCMPLX_1:1
.= p*f.r+p*g.r+ ((1-p)*g.s+(1-p)*f.s) by XCMPLX_1:1
.= p*(f.r+g.r) + ((1-p)*g.s+(1-p)*f.s) by XCMPLX_1:8
.= p*(f.r+g.r) + (1-p)*(f.s+g.s) by XCMPLX_1:8;
(f+g).(p*r + (1-p)*s) = f.(p*r+(1-p)*s)+g.(p*r+(1-p)*s) &
(f+g).r = (f.r+g.r) & (f+g).s = (f.s+g.s) by A2,A4,SEQ_1:def 3;
hence thesis by A5,A6,REAL_1:67;
end;
hence thesis;
end;
hence thesis by A2,Def1;
end;
theorem
f is_strictly_convex_on X & g is_strictly_convex_on X &
((a>0 & b>=0) or (a>=0 & b>0)) implies a(#)f+b(#)g is_strictly_convex_on X
proof
assume A1:f is_strictly_convex_on X & g is_strictly_convex_on X &
((a>0 & b>=0) or (a>=0 & b>0));
now per cases by A1;
suppose a>0 & b>0;
then a(#)f is_strictly_convex_on X & b(#)g is_strictly_convex_on X by A1,
Th12;
hence thesis by Th13;
suppose A2:a>0 & b=0;
then A3: a(#)f is_strictly_convex_on X by A1,Th12;
g is_convex_on X & X c= dom g by A1,Def1,Th6;
then b(#)g is_convex_on X by A2,RFUNCT_3:60;
hence thesis by A3,Th14;
suppose A4:a=0 & b>0;
then A5: b(#)g is_strictly_convex_on X by A1,Th12;
f is_convex_on X & X c= dom f by A1,Def1,Th6;
then a(#)f is_convex_on X by A4,RFUNCT_3:60;
hence thesis by A5,Th14;
end;
hence thesis;
end;
Lm4:
for a,b,r be real number holds r*(a/b)=r*a/b
proof
let a,b,r be real number;
thus r*(a/b)=r*(a*b") by XCMPLX_0:def 9
.=r*a*b" by XCMPLX_1:4
.=r*a/b by XCMPLX_0:def 9;
end;
theorem Th16:
f is_convex_on X iff
X c= dom f & (for a,b,r st a in X & b in X & r in X & a < r & r < b holds
(f.r-f.a)/(r-a) <= (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) <= (f.b-f.r)/(b-r))
proof
A1:f is_convex_on X implies
X c= dom f & (for a,b,r st a in X & b in X & r in X & a < r & r < b holds
(f.r-f.a)/(r-a) <= (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) <= (f.b-f.r)/(b-r))
proof
assume A2:f is_convex_on X;
X c= dom f &
(for a,b,r st a in X & b in X & r in X & a < r & r < b holds
(f.r-f.a)/(r-a) <= (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) <= (f.b-f.r)/(b-r))
proof
thus X c= dom f by A2,RFUNCT_3:def 13;
(for a,b,r st a in X & b in X & r in X & a < r & r < b holds
(f.r-f.a)/(r-a) <= (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) <= (f.b-f.r)/(b-r))
proof
let a,b,r;
assume A3:a in X & b in X & r in X & a < r & r < b;
then A4: b-r < b-a & 0 < b-r & 0 < r-a by REAL_2:105,SQUARE_1:11;
then A5: 0 < b-a by AXIOMS:22;
then A6: 0 < (b-r)/(b-a) & (b-r)/(b-a) < 1 by A4,REAL_2:127,142;
set p = (b-r)/(b-a);
A7: 1-p = (r-a)/(b-a) & p*a + (1-p)*b = r
proof
p+(r-a)/(b-a) = ((b-r)+(r-a))/(b-a) by XCMPLX_1:63
.= (b-a)/(b-a) by XCMPLX_1:39
.= 1 by A4,XCMPLX_1:60;
hence 1-p = (r-a)/(b-a) by XCMPLX_1:26;
then p*a + (1-p)*b
= (a*(b-r))/(b-a)+b*((r-a)/(b-a)) by XCMPLX_1:75
.= (a*(b-r))/(b-a)+(b*(r-a))/(b-a) by XCMPLX_1:75
.= ((b-r)*a + (r-a)*b)/(b-a) by XCMPLX_1:63
.= ((b*a-r*a)+(r-a)*b)/(b-a) by XCMPLX_1:40
.= ((b*a-r*a)+(r*b-a*b))/(b-a) by XCMPLX_1:40
.= (r*b-r*a)/(b-a) by XCMPLX_1:39
.= r*(b-a)/(b-a) by XCMPLX_1:40;
hence thesis by A4,XCMPLX_1:90;
end;
then f.(p*a+(1-p)*b) <= p*f.a + (1-p)*f.b by A2,A3,A6,RFUNCT_3:def 13;
then A8: (b-a)*f.r<=(b-a)*((b-r)/(b-a)*f.a + (r-a)/(b-a)*f.b) by A5,A7,AXIOMS
:25;
A9: (b-a)*((b-r)/(b-a)*f.a + (r-a)/(b-a)*f.b)
= (b-a)*((b-r)/(b-a)*f.a) + (b-a)*((r-a)/(b-a)*f.b) by XCMPLX_1:8
.= (b-a)*((b-r)/(b-a))*f.a + (b-a)*((r-a)/(b-a)*f.b) by XCMPLX_1:4
.= (b-a)*((b-r)/(b-a))*f.a + (b-a)*((r-a)/(b-a))*f.b by XCMPLX_1:4
.= (b-r)*f.a + (b-a)*((r-a)/(b-a))*f.b by A4,XCMPLX_1:88
.= (b-r)*f.a + (r-a)*f.b by A4,XCMPLX_1:88;
then (b-a)*f.r <= ((b-a)-(r-a))*f.a + (r-a)*f.b by A8,XCMPLX_1:22;
then (b-a)*f.r <= (b-a)*f.a - (r-a)*f.a + (r-a)*f.b by XCMPLX_1:40;
then (b-a)*f.r <= (b-a)*f.a - ((r-a)*f.a - (r-a)*f.b) by XCMPLX_1:37;
then (b-a)*f.r <= (b-a)*f.a + ((r-a)*f.b - (r-a)*f.a) by XCMPLX_1:38;
then (b-a)*f.r - (b-a)*f.a <= (r-a)*f.b - (r-a)*f.a by REAL_1:86;
then (b-a)*(f.r-f.a) <= (r-a)*f.b - (r-a)*f.a by XCMPLX_1:40;
then (b-a)*(f.r-f.a) <= (r-a)*(f.b-f.a) by XCMPLX_1:40;
hence (f.r-f.a)/(r-a) <= (f.b-f.a)/(b-a) by A4,A5,REAL_2:187;
(b-a)*f.r <= (b-r)*f.a + ((r-b)+(b-a))*f.b by A8,A9,XCMPLX_1:39;
then (b-a)*f.r <= (b-r)*f.a + ((b-a)-(b-r))*f.b by XCMPLX_1:38;
then (b-a)*f.r <= (b-a)*f.b-(b-r)*f.b+(b-r)*f.a by XCMPLX_1:40;
then (b-a)*f.r <= (b-a)*f.b - ((b-r)*f.b - (b-r)*f.a) by XCMPLX_1:37;
then ((b-r)*f.b-(b-r)*f.a)+(b-a)*f.r <= (b-a)*f.b by REAL_1:84;
then (b-r)*f.b-(b-r)*f.a <= (b-a)*f.b-(b-a)*f.r by REAL_1:84;
then (b-r)*(f.b-f.a) <= (b-a)*f.b-(b-a)*f.r by XCMPLX_1:40;
then (b-r)*(f.b-f.a) <= (b-a)*(f.b-f.r) by XCMPLX_1:40;
hence thesis by A4,A5,REAL_2:187;
end;
hence thesis;
end;
hence thesis;
end;
X c= dom f &
(for a,b,r st a in X & b in X & r in X & a < r & r < b holds
(f.r-f.a)/(r-a) <= (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) <= (f.b-f.r)/(b-r))
implies f is_convex_on X
proof
assume A10:X c= dom f &
(for a,b,r st a in X & b in X & r in X & a < r & r < b holds
(f.r-f.a)/(r-a) <= (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) <= (f.b-f.r)/(b-r));
for p being Real st 0<=p & p<=1 holds
for r,s be Real st r in X & s in X & p*r + (1-p)*s in X holds
f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s
proof
let p be Real; assume A11:0<=p & p<=1;
for s,t being Real st s in X & t in X & p*s+(1-p)*t in X holds
f.(p*s+(1-p)*t) <= p*f.s + (1-p)*f.t
proof
let s,t be Real; assume A12:s in X & t in X & p*s+(1-p)*t in X;
now per cases by A11,REAL_1:def 5;
suppose p=0;
hence thesis;
suppose p=1;
hence thesis;
suppose A13:0<p & p<1;
then A14: 1-p > 0 by SQUARE_1:11;
now per cases by REAL_1:def 5;
suppose A15:s=t;
then p*s+(1-p)*t = s by Lm1;
hence thesis by A15,Lm1;
suppose s<t;
then A16: t-s > 0 by SQUARE_1:11;
A17: t-(p*s+(1-p)*t) = t-(1-p)*t - p*s by XCMPLX_1:36
.=p*t-p*s by Lm1
.=p*(t-s) by XCMPLX_1:40;
then A18: t-(p*s+(1-p)*t) > 0 by A13,A16,REAL_2:122;
then A19: (p*s+(1-p)*t) < t by REAL_2:106;
A20: (p*s+(1-p)*t)-s = (1-p)*t+(p*s-s) by XCMPLX_1:29
.=(1-p)*t-(s-p*s) by XCMPLX_1:38
.=(1-p)*t-(1-p)*s by Lm1
.=(1-p)*(t-s) by XCMPLX_1:40;
then A21: (p*s+(1-p)*t)-s > 0 by A14,A16,REAL_2:122;
then (p*s+(1-p)*t) > s by REAL_2:106;
then (f.(p*s+(1-p)*t)-f.s)/((p*s+(1-p)*t)-s) <= (f.t-f.s)/(t-s) &
(f.t-f.s)/(t-s)<=(f.t-f.(p*s+(1-p)*t))/(t-(p*s+(1-p)*t))
by A10,A12,A19;
then (f.(p*s+(1-p)*t)-f.s)/((p*s+(1-p)*t)-s)
<= (f.t-f.(p*s+(1-p)*t))/(t-(p*s+(1-p)*t)) by AXIOMS:22;
then (f.(p*s+(1-p)*t)-f.s)*(t-(p*s+(1-p)*t))
<= (f.t-f.(p*s+(1-p)*t))*((p*s+(1-p)*t)-s) by A18,A21,REAL_2:185;
then (f.(p*s+(1-p)*t)-f.s)*(t-s)*p
<= (f.t-f.(p*s+(1-p)*t))*((1-p)*(t-s)) by A17,A20,XCMPLX_1:4;
then A22: (f.(p*s+(1-p)*t)-f.s)*(t-s)*p
<= (f.t-f.(p*s+(1-p)*t))*(t-s)*(1-p) by XCMPLX_1:4;
A23: (f.(p*s+(1-p)*t)-f.s)*(t-s)*p
=((t-s)*f.(p*s+(1-p)*t)-(t-s)*f.s)*p by XCMPLX_1:40
.=p*((t-s)*f.(p*s+(1-p)*t))-p*((t-s)*f.s) by XCMPLX_1:40;
(f.t-f.(p*s+(1-p)*t))*(t-s)*(1-p)
=((t-s)*f.t-(t-s)*f.(p*s+(1-p)*t))*(1-p) by XCMPLX_1:40
.=(1-p)*((t-s)*f.t)-(1-p)*((t-s)*f.(p*s+(1-p)*t)) by XCMPLX_1:40;
then p*((t-s)*f.(p*s+(1-p)*t))+(1-p)*((t-s)*f.(p*s+(1-p)*t))
<=(1-p)*((t-s)*f.t)+p*((t-s)*f.s) by A22,A23,REAL_2:169;
then (t-s)*f.(p*s+(1-p)*t)
<=(1-p)*((t-s)*f.t)+p*((t-s)*f.s) by Lm1;
then (t-s)*f.(p*s+(1-p)*t)
<=(1-p)*f.t*(t-s)+p*((t-s)*f.s) by XCMPLX_1:4;
then (t-s)*f.(p*s+(1-p)*t)
<=(1-p)*f.t*(t-s)+p*f.s*(t-s) by XCMPLX_1:4;
then f.(p*s+(1-p)*t)
<=((1-p)*f.t*(t-s)+p*f.s*(t-s))/(t-s) by A16,REAL_2:177;
then f.(p*s+(1-p)*t)
<=((1-p)*f.t*(t-s))/(t-s)+(p*f.s*(t-s))/(t-s) by XCMPLX_1:63;
then f.(p*s+(1-p)*t)
<=(1-p)*f.t+(p*f.s*(t-s))/(t-s) by A16,XCMPLX_1:90;
hence thesis by A16,XCMPLX_1:90;
suppose s>t;
then A24: s-t > 0 by SQUARE_1:11;
A25: s-(p*s+(1-p)*t) = s-p*s - (1-p)*t by XCMPLX_1:36
.=(1-p)*s-(1-p)*t by Lm1
.=(1-p)*(s-t) by XCMPLX_1:40;
then A26: s-(p*s+(1-p)*t) > 0 by A14,A24,REAL_2:122;
then A27: (p*s+(1-p)*t) < s by REAL_2:106;
A28: (p*s+(1-p)*t)-t = p*s+((1-p)*t-t) by XCMPLX_1:29
.=p*s-(t-(1-p)*t) by XCMPLX_1:38
.=p*s-p*t by Lm1
.=p*(s-t) by XCMPLX_1:40;
then A29: (p*s+(1-p)*t)-t > 0 by A13,A24,REAL_2:122;
then (p*s+(1-p)*t) > t by REAL_2:106;
then (f.(p*s+(1-p)*t)-f.t)/((p*s+(1-p)*t)-t) <= (f.s-f.t)/(s-t) &
(f.s-f.t)/(s-t)<=(f.s-f.(p*s+(1-p)*t))/(s-(p*s+(1-p)*t))
by A10,A12,A27;
then (f.(p*s+(1-p)*t)-f.t)/((p*s+(1-p)*t)-t)
<= (f.s-f.(p*s+(1-p)*t))/(s-(p*s+(1-p)*t)) by AXIOMS:22;
then (f.(p*s+(1-p)*t)-f.t)*(s-(p*s+(1-p)*t))
<= (f.s-f.(p*s+(1-p)*t))*((p*s+(1-p)*t)-t) by A26,A29,REAL_2:185;
then (f.(p*s+(1-p)*t)-f.t)*(s-t)*(1-p)
<= (f.s-f.(p*s+(1-p)*t))*(p*(s-t)) by A25,A28,XCMPLX_1:4;
then A30: (f.(p*s+(1-p)*t)-f.t)*(s-t)*(1-p)
<= (f.s-f.(p*s+(1-p)*t))*(s-t)*p by XCMPLX_1:4;
A31: (f.(p*s+(1-p)*t)-f.t)*(s-t)*(1-p)
=((s-t)*f.(p*s+(1-p)*t)-(s-t)*f.t)*(1-p) by XCMPLX_1:40
.=(1-p)*((s-t)*f.(p*s+(1-p)*t))-(1-p)*((s-t)*f.t) by XCMPLX_1:40;
(f.s-f.(p*s+(1-p)*t))*(s-t)*p
=((s-t)*f.s-(s-t)*f.(p*s+(1-p)*t))*p by XCMPLX_1:40
.=p*((s-t)*f.s)-p*((s-t)*f.(p*s+(1-p)*t)) by XCMPLX_1:40;
then (1-p)*((s-t)*f.(p*s+(1-p)*t))+p*((s-t)*f.(p*s+(1-p)*t))
<=p*((s-t)*f.s)+(1-p)*((s-t)*f.t) by A30,A31,REAL_2:169;
then (s-t)*f.(p*s+(1-p)*t)
<=p*((s-t)*f.s)+(1-p)*((s-t)*f.t) by Lm1;
then (s-t)*f.(p*s+(1-p)*t)
<=p*f.s*(s-t)+(1-p)*((s-t)*f.t) by XCMPLX_1:4;
then (s-t)*f.(p*s+(1-p)*t)
<=p*f.s*(s-t)+(1-p)*f.t*(s-t) by XCMPLX_1:4;
then f.(p*s+(1-p)*t)
<=(p*f.s*(s-t)+(1-p)*f.t*(s-t))/(s-t) by A24,REAL_2:177;
then f.(p*s+(1-p)*t)
<=(p*f.s*(s-t))/(s-t)+((1-p)*f.t*(s-t))/(s-t) by XCMPLX_1:63;
then f.(p*s+(1-p)*t)
<=p*f.s+((1-p)*f.t*(s-t))/(s-t) by A24,XCMPLX_1:90;
hence thesis by A24,XCMPLX_1:90;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis by A10,RFUNCT_3:def 13;
end;
hence thesis by A1;
end;
theorem
f is_strictly_convex_on X iff
X c= dom f & (for a,b,r st a in X & b in X & r in X & a < r & r < b holds
(f.r-f.a)/(r-a) < (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) < (f.b-f.r)/(b-r))
proof
A1:f is_strictly_convex_on X implies
X c= dom f & (for a,b,r st a in X & b in X & r in X & a < r & r < b holds
(f.r-f.a)/(r-a) < (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) < (f.b-f.r)/(b-r))
proof
assume A2:f is_strictly_convex_on X;
X c= dom f & (for a,b,r st a in X & b in X & r in X & a < r & r < b holds
(f.r-f.a)/(r-a) < (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) < (f.b-f.r)/(b-r))
proof
(for a,b,r st a in X & b in X & r in X & a < r & r < b holds
(f.r-f.a)/(r-a) < (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) < (f.b-f.r)/(b-r))
proof
let a,b,r;
assume A3:a in X & b in X & r in X & a < r & r < b;
then A4: b-r < b-a & 0 < b-r & 0 < r-a by REAL_2:105,SQUARE_1:11;
then A5: 0 < b-a by AXIOMS:22;
then A6: 0 < (b-r)/(b-a) & (b-r)/(b-a) < 1 by A4,REAL_2:127,142;
set p = (b-r)/(b-a);
A7: 1-p = (r-a)/(b-a) & p*a + (1-p)*b = r
proof
p+(r-a)/(b-a) = ((b-r)+(r-a))/(b-a) by XCMPLX_1:63
.= (b-a)/(b-a) by XCMPLX_1:39
.= 1 by A4,XCMPLX_1:60;
hence 1-p = (r-a)/(b-a) by XCMPLX_1:26;
then p*a + (1-p)*b
= (a*(b-r))/(b-a)+b*((r-a)/(b-a)) by XCMPLX_1:75
.= (a*(b-r))/(b-a)+(b*(r-a))/(b-a) by XCMPLX_1:75
.= ((b-r)*a + (r-a)*b)/(b-a) by XCMPLX_1:63
.= ((b*a-r*a)+(r-a)*b)/(b-a) by XCMPLX_1:40
.= ((b*a-r*a)+(r*b-a*b))/(b-a) by XCMPLX_1:40
.= (r*b-r*a)/(b-a) by XCMPLX_1:39
.= r*(b-a)/(b-a) by XCMPLX_1:40;
hence thesis by A4,XCMPLX_1:90;
end;
then f.r < p*f.a + (1-p)*f.b by A2,A3,A6,Def1;
then A8: f.r*(b-a) < (p*f.a + (1-p)*f.b)*(b-a) by A5,REAL_1:70;
A9: (p*f.a+(1-p)*f.b)*(b-a)=(b-a)*(p*f.a)+(b-a)*((1-p)*f.b) by XCMPLX_1:8
.= (b-a)*p*f.a+(b-a)*((1-p)*f.b) by XCMPLX_1:4
.= (b-a)*p*f.a+(b-a)*(1-p)*f.b by XCMPLX_1:4
.= ((b-a)*(b-r)/(b-a))*f.a + ((b-a)*((r-a)/(b-a))*f.b) by A7,Lm4
.= ((b-r)*(b-a))/(b-a)*f.a + ((b-a)*(r-a)/(b-a))*f.b by Lm4
.= (b-r)*((b-a)/(b-a))*f.a + ((b-a)*(r-a)/(b-a))*f.b by Lm4
.= (b-r)*1*f.a + ((r-a)*(b-a))/(b-a)*f.b by A4,XCMPLX_1:60
.= (b-r)*f.a + (r-a)*((b-a)/(b-a))*f.b by Lm4
.= (b-r)*f.a + (r-a)*1*f.b by A4,XCMPLX_1:60;
then f.r*(b-a) < ((b-a)-(r-a))*f.a + (r-a)*f.b by A8,XCMPLX_1:22;
then f.r*(b-a) < (b-a)*f.a - (r-a)*f.a + (r-a)*f.b by XCMPLX_1:40;
then f.r*(b-a) < (b-a)*f.a +(r-a)*f.b-(r-a)*f.a by XCMPLX_1:29;
then f.r*(b-a) < (b-a)*f.a +((r-a)*f.b-(r-a)*f.a) by XCMPLX_1:29;
then f.r*(b-a)-(b-a)*f.a < (r-a)*f.b-(r-a)*f.a by REAL_1:84;
then (b-a)*(f.r-f.a) < (r-a)*f.b-(r-a)*f.a by XCMPLX_1:40;
then (b-a)*(f.r-f.a) < (r-a)*(f.b-f.a) by XCMPLX_1:40;
hence (f.r-f.a)/(r-a) < (f.b-f.a)/(b-a) by A4,A5,REAL_2:185;
f.r*(b-a) < (b-r)*f.a + ((r-b)+(b-a))*f.b by A8,A9,XCMPLX_1:39;
then f.r*(b-a) < (b-r)*f.a + ((r-b)*f.b + (b-a)*f.b) by XCMPLX_1:8;
then f.r*(b-a) < (r-b)*f.b + (b-r)*f.a + (b-a)*f.b by XCMPLX_1:1;
then f.r*(b-a)-((r-b)*f.b + (b-r)*f.a) < (b-a)*f.b by REAL_1:84;
then f.r*(b-a)+(-((r-b)*f.b+(b-r)*f.a))<(b-a)*f.b by XCMPLX_0:def 8;
then -((r-b)*f.b + (b-r)*f.a) < (b-a)*f.b - (b-a)*f.r by REAL_1:86;
then -(r-b)*f.b -(b-r)*f.a < (b-a)*f.b - (b-a)*f.r by XCMPLX_1:161;
then (-(r-b))*f.b -(b-r)*f.a < (b-a)*f.b - (b-a)*f.r by XCMPLX_1:175;
then (b-r)*f.b - (b-r)*f.a < (b-a)*f.b - (b-a)*f.r by XCMPLX_1:143;
then (b-r)*(f.b-f.a) < (b-a)*f.b - (b-a)*f.r by XCMPLX_1:40;
then (b-r)*(f.b-f.a) < (b-a)*(f.b-f.r) by XCMPLX_1:40;
hence thesis by A4,A5,REAL_2:185;
end;
hence thesis by A2,Def1;
end;
hence thesis;
end;
X c= dom f & (for a,b,r st a in X & b in X & r in X & a < r & r < b holds
(f.r-f.a)/(r-a) < (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) < (f.b-f.r)/(b-r))
implies f is_strictly_convex_on X
proof
assume A10:X c= dom f &
(for a,b,r st a in X & b in X & r in X & a<r & r<b holds
(f.r-f.a)/(r-a) < (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) < (f.b-f.r)/(b-r));
f is_strictly_convex_on X
proof
for p being Real st 0<p & p<1 holds
for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s
proof
let p be Real;
assume A11:0<p & p<1;
then A12: 1-p > 0 by SQUARE_1:11;
for s,t being Real st s in X & t in X & p*s+(1-p)*t in X & s <> t holds
f.(p*s + (1-p)*t) < p*f.s + (1-p)*f.t
proof
let s,t be Real;
assume A13:s in X & t in X & p*s+(1-p)*t in X & s <> t;
now per cases by A13,REAL_1:def 5;
suppose s<t;
then A14: t-s > 0 by SQUARE_1:11;
A15: t-(p*s+(1-p)*t) = t-(1-p)*t - p*s by XCMPLX_1:36
.=p*t-p*s by Lm1
.=p*(t-s) by XCMPLX_1:40;
then A16: t-(p*s+(1-p)*t) > 0 by A11,A14,REAL_2:122;
then A17: (p*s+(1-p)*t) < t by REAL_2:106;
A18: (p*s+(1-p)*t)-s = (1-p)*t+(p*s-s) by XCMPLX_1:29
.=(1-p)*t-(s-p*s) by XCMPLX_1:38
.=(1-p)*t-(1-p)*s by Lm1
.=(1-p)*(t-s) by XCMPLX_1:40;
then A19: (p*s+(1-p)*t)-s > 0 by A12,A14,REAL_2:122;
then (p*s+(1-p)*t) > s by REAL_2:106;
then (f.(p*s+(1-p)*t)-f.s)/((p*s+(1-p)*t)-s) < (f.t-f.s)/(t-s) &
(f.t-f.s)/(t-s)<(f.t-f.(p*s+(1-p)*t))/(t-(p*s+(1-p)*t))
by A10,A13,A17;
then (f.(p*s+(1-p)*t)-f.s)/((p*s+(1-p)*t)-s)
< (f.t-f.(p*s+(1-p)*t))/(t-(p*s+(1-p)*t)) by AXIOMS:22;
then (f.(p*s+(1-p)*t)-f.s)*(t-(p*s+(1-p)*t))
< (f.t-f.(p*s+(1-p)*t))*((p*s+(1-p)*t)-s) by A16,A19,REAL_2:187;
then (f.(p*s+(1-p)*t)-f.s)*(t-s)*p
< (f.t-f.(p*s+(1-p)*t))*((1-p)*(t-s)) by A15,A18,XCMPLX_1:4;
then A20: (f.(p*s+(1-p)*t)-f.s)*(t-s)*p
< (f.t-f.(p*s+(1-p)*t))*(t-s)*(1-p) by XCMPLX_1:4;
A21: (f.(p*s+(1-p)*t)-f.s)*(t-s)*p
=((t-s)*f.(p*s+(1-p)*t)-(t-s)*f.s)*p by XCMPLX_1:40
.=p*((t-s)*f.(p*s+(1-p)*t))-p*((t-s)*f.s) by XCMPLX_1:40;
(f.t-f.(p*s+(1-p)*t))*(t-s)*(1-p)
=((t-s)*f.t-(t-s)*f.(p*s+(1-p)*t))*(1-p) by XCMPLX_1:40
.=(1-p)*((t-s)*f.t)-(1-p)*((t-s)*f.(p*s+(1-p)*t)) by XCMPLX_1:40;
then p*((t-s)*f.(p*s+(1-p)*t))+(1-p)*((t-s)*f.(p*s+(1-p)*t))
<(1-p)*((t-s)*f.t)+p*((t-s)*f.s) by A20,A21,REAL_2:170;
then (t-s)*f.(p*s+(1-p)*t)
<(1-p)*((t-s)*f.t)+p*((t-s)*f.s) by Lm1;
then (t-s)*f.(p*s+(1-p)*t)
<(1-p)*f.t*(t-s)+p*((t-s)*f.s) by XCMPLX_1:4;
then (t-s)*f.(p*s+(1-p)*t)
<(1-p)*f.t*(t-s)+p*f.s*(t-s) by XCMPLX_1:4;
then f.(p*s+(1-p)*t)
<((1-p)*f.t*(t-s)+p*f.s*(t-s))/(t-s) by A14,REAL_2:178;
then f.(p*s+(1-p)*t)
<((1-p)*f.t*(t-s))/(t-s)+(p*f.s*(t-s))/(t-s) by XCMPLX_1:63;
then f.(p*s+(1-p)*t)
<(1-p)*f.t+(p*f.s*(t-s))/(t-s) by A14,XCMPLX_1:90;
hence thesis by A14,XCMPLX_1:90;
suppose s>t;
then A22: s-t > 0 by SQUARE_1:11;
A23: s-(p*s+(1-p)*t) = s-p*s - (1-p)*t by XCMPLX_1:36
.=(1-p)*s-(1-p)*t by Lm1
.=(1-p)*(s-t) by XCMPLX_1:40;
then A24: s-(p*s+(1-p)*t) > 0 by A12,A22,REAL_2:122;
then A25: (p*s+(1-p)*t) < s by REAL_2:106;
A26: (p*s+(1-p)*t)-t = p*s+((1-p)*t-t) by XCMPLX_1:29
.=p*s-(t-(1-p)*t) by XCMPLX_1:38
.=p*s-p*t by Lm1
.=p*(s-t) by XCMPLX_1:40;
then A27: (p*s+(1-p)*t)-t > 0 by A11,A22,REAL_2:122;
then (p*s+(1-p)*t) > t by REAL_2:106;
then (f.(p*s+(1-p)*t)-f.t)/((p*s+(1-p)*t)-t) < (f.s-f.t)/(s-t) &
(f.s-f.t)/(s-t)<(f.s-f.(p*s+(1-p)*t))/(s-(p*s+(1-p)*t))
by A10,A13,A25;
then (f.(p*s+(1-p)*t)-f.t)/((p*s+(1-p)*t)-t)
< (f.s-f.(p*s+(1-p)*t))/(s-(p*s+(1-p)*t)) by AXIOMS:22;
then (f.(p*s+(1-p)*t)-f.t)*(s-(p*s+(1-p)*t))
< (f.s-f.(p*s+(1-p)*t))*((p*s+(1-p)*t)-t) by A24,A27,REAL_2:187;
then (f.(p*s+(1-p)*t)-f.t)*(s-t)*(1-p)
< (f.s-f.(p*s+(1-p)*t))*(p*(s-t)) by A23,A26,XCMPLX_1:4;
then A28: (f.(p*s+(1-p)*t)-f.t)*(s-t)*(1-p)
< (f.s-f.(p*s+(1-p)*t))*(s-t)*p by XCMPLX_1:4;
A29: (f.(p*s+(1-p)*t)-f.t)*(s-t)*(1-p)
=((s-t)*f.(p*s+(1-p)*t)-(s-t)*f.t)*(1-p) by XCMPLX_1:40
.=(1-p)*((s-t)*f.(p*s+(1-p)*t))-(1-p)*((s-t)*f.t) by XCMPLX_1:40;
(f.s-f.(p*s+(1-p)*t))*(s-t)*p
=((s-t)*f.s-(s-t)*f.(p*s+(1-p)*t))*p by XCMPLX_1:40
.=p*((s-t)*f.s)-p*((s-t)*f.(p*s+(1-p)*t)) by XCMPLX_1:40;
then (1-p)*((s-t)*f.(p*s+(1-p)*t))+p*((s-t)*f.(p*s+(1-p)*t))
<p*((s-t)*f.s)+(1-p)*((s-t)*f.t) by A28,A29,REAL_2:170;
then (s-t)*f.(p*s+(1-p)*t)
<p*((s-t)*f.s)+(1-p)*((s-t)*f.t) by Lm1;
then (s-t)*f.(p*s+(1-p)*t)
<p*f.s*(s-t)+(1-p)*((s-t)*f.t) by XCMPLX_1:4;
then (s-t)*f.(p*s+(1-p)*t)
<p*f.s*(s-t)+(1-p)*f.t*(s-t) by XCMPLX_1:4;
then f.(p*s+(1-p)*t)
<(p*f.s*(s-t)+(1-p)*f.t*(s-t))/(s-t) by A22,REAL_2:178;
then f.(p*s+(1-p)*t)
<(p*f.s*(s-t))/(s-t)+((1-p)*f.t*(s-t))/(s-t) by XCMPLX_1:63;
then f.(p*s+(1-p)*t)
<p*f.s+((1-p)*f.t*(s-t))/(s-t) by A22,XCMPLX_1:90;
hence thesis by A22,XCMPLX_1:90;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis by A10,Def1;
end;
hence thesis;
end;
hence thesis by A1;
end;
:: Jensen's Inequality
theorem
for f being PartFunc of REAL,REAL
st f is total holds
(for n being Nat, P,E,F being Element of n-tuples_on REAL st Sum P=1 &
(for i being Nat st i in dom P holds P.i >=0 & F.i=f.(E.i))
holds f.Sum(mlt(P,E))<=Sum(mlt(P,F)))
iff f is_convex_on REAL
proof
let f be PartFunc of REAL,REAL;
assume f is total;
then A1:REAL c= dom f by PARTFUN1:def 4;
A2:(for n being Nat, P,E,F being Element of n-tuples_on REAL st Sum P=1 &
(for i being Nat st i in dom P holds P.i >=0 & F.i=f.(E.i))
holds f.Sum(mlt(P,E))<=Sum(mlt(P,F)))
implies f is_convex_on REAL
proof
assume A3:for n being Nat, P,E,F being Element of n-tuples_on REAL st Sum
P=1
& (for i being Nat st i in dom P holds P.i >=0 & F.i=f.(E.i))
holds f.Sum(mlt(P,E))<=Sum(mlt(P,F));
for p being Real st 0<=p & p<=1 holds
for r,s being Real st r in REAL & s in REAL & p*r + (1-p)*s in REAL holds
f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s
proof
let p be Real such that A4:0<=p & p<=1;
let r,s be Real such that r in REAL & s in REAL & p*r + (1-p)*s in REAL;
reconsider P=<*p,1-p*>, E=<*r,s*>, F=<*f.r,f.s*>
as Element of 2-tuples_on REAL by FINSEQ_2:121;
A5: Sum P=p+(1-p) by RVSUM_1:107 .= p-(p-1) by XCMPLX_1:38 .= 1
by XCMPLX_1:18;
for i being Nat st i in dom P holds P.i >=0 & F.i=f.(E.i)
proof
let i be Nat such that A6:i in dom P;
A7: dom P = Seg len P by FINSEQ_1:def 3 .= Seg 2 by FINSEQ_2:109;
now per cases by A6,A7,FINSEQ_1:4,TARSKI:def 2;
suppose i=1;
then E.i = r & P.i = p & F.i = f.r by FINSEQ_1:61;
hence thesis by A4;
suppose i=2;
then E.i = s & P.i = 1-p & F.i = f.s by FINSEQ_1:61;
hence thesis by A4,SQUARE_1:12;
end;
hence thesis;
end;
then A8: f.Sum(mlt(P,E))<=Sum(mlt(P,F)) by A3,A5;
A9: P.1=p & P.2=1-p & E.1=r & E.2=s & F.1=f.r & F.2=f.s by FINSEQ_1:61;
len P = 2 by FINSEQ_1:61 .= len E by FINSEQ_1:61;
then len (multreal.:(P,E)) = len P by FINSEQ_2:86;
then A10: len mlt(P,E) = len P by RVSUM_1:def 9 .= 2 by FINSEQ_1:61;
mlt(P,E).1 = P.1*E.1 & mlt(P,E).2 = P.2*E.2 by RVSUM_1:87;
then mlt(P,E)=<*p*r,(1-p)*s*> by A9,A10,FINSEQ_1:61;
then A11: Sum(mlt(P,E))=p*r+(1-p)*s by RVSUM_1:107;
len P = 2 by FINSEQ_1:61 .= len F by FINSEQ_1:61;
then len (multreal.:(P,F)) = len P by FINSEQ_2:86;
then A12: len mlt(P,F) = len P by RVSUM_1:def 9 .= 2 by FINSEQ_1:61;
mlt(P,F).1 = P.1*F.1 & mlt(P,F).2 = P.2*F.2 by RVSUM_1:87;
then mlt(P,F)=<*p*f.r,(1-p)*f.s*> by A9,A12,FINSEQ_1:61;
hence thesis by A8,A11,RVSUM_1:107;
end;
hence thesis by A1,RFUNCT_3:def 13;
end;
f is_convex_on REAL implies
(for n being Nat, P,E,F being Element of n-tuples_on REAL st Sum P=1 &
(for i being Nat st i in dom P holds P.i >=0 & F.i=f.(E.i))
holds f.Sum(mlt(P,E))<=Sum(mlt(P,F)))
proof
assume A13:f is_convex_on REAL;
for n being Nat, P,E,F being Element of n-tuples_on REAL st Sum P=1 &
(for i being Nat st i in dom P holds P.i >=0 & F.i=f.(E.i))
holds f.Sum(mlt(P,E))<=Sum(mlt(P,F))
proof
defpred S[Nat] means for P,E,F being Element of $1-tuples_on REAL st
Sum P=1 & (for i being Nat st i in dom P holds P.i >=0 & F.i=f.(E.i))
holds f.Sum(mlt(P,E))<=Sum(mlt(P,F));
A14: S[0] by RVSUM_1:109;
A15: for k being Nat st S[k] holds S[k+1]
proof
let k be Nat such that
A16: (for P,E,F being Element of k-tuples_on REAL st Sum P=1 &
(for i being Nat st i in dom P holds P.i >=0 & F.i=f.(E.i))
holds f.Sum(mlt(P,E))<=Sum(mlt(P,F)));
for P,E,F being Element of (k+1)-tuples_on REAL st Sum P=1 &
(for i being Nat st i in dom P holds P.i >=0 & F.i=f.(E.i))
holds f.Sum(mlt(P,E))<=Sum(mlt(P,F))
proof
let P,E,F be Element of (k+1)-tuples_on REAL such that
A17: Sum P=1 & (for i being Nat st i in dom P holds P.i>=0 & F.i=f.(E.i));
consider P1 being Element of k-tuples_on REAL, p1 being Real such that
A18: P=P1^<*p1*> by FINSEQ_2:137;
consider E1 being Element of k-tuples_on REAL, e1 being Real such that
A19: E=E1^<*e1*> by FINSEQ_2:137;
consider F1 being Element of k-tuples_on REAL, f1 being Real such that
A20: F=F1^<*f1*> by FINSEQ_2:137;
mlt(P,E) = mlt(P1,E1)^<*p1*e1*> by A18,A19,Th2;
then A21: Sum(mlt(P,E)) = 1*Sum(mlt(P1,E1))+p1*e1 by RVSUM_1:104;
mlt(P,F) = mlt(P1,F1)^<*p1*f1*> by A18,A20,Th2;
then A22: Sum(mlt(P,F)) = 1*Sum(mlt(P1,F1))+p1*f1 by RVSUM_1:104;
len F1 + 1 = k + 1 by FINSEQ_2:109 .= len P by FINSEQ_2:109;
then len F1 + 1 in Seg len P by FINSEQ_1:6;
then A23: len F1 + 1 in dom P by FINSEQ_1:def 3;
A24: f1=F.(len F1 + 1) by A20,FINSEQ_1:59 .= f.(E.(len F1 + 1)) by A17,A23
.= f.(E.(k+1)) by FINSEQ_2:109 .= f.(E.(len E1+1)) by FINSEQ_2:109
.= f.e1 by A19,FINSEQ_1:59;
A25: for i being Nat st i in dom P1 holds P1.i>=0
proof
let i be Nat such that
A26: i in dom P1;
i in Seg len P1 by A26,FINSEQ_1:def 3;
then 1 <= i & i <= len P1 by FINSEQ_1:3;
then 1 <= i & i <= k & k <= k+1 by FINSEQ_2:109,NAT_1:29;
then 1 <= i & i <= k+1 by AXIOMS:22;
then i in Seg (k+1) by FINSEQ_1:3;
then i in Seg len P by FINSEQ_2:109;
then A27: i in dom P by FINSEQ_1:def 3;
P1.i = P.i by A18,A26,FINSEQ_1:def 7;
hence thesis by A17,A27;
end;
now per cases;
suppose A28:Sum P1 = 0;
then for i being Nat st i in dom P1 holds P1.i=0 by A25,Th3;
then A29: P1 = k |-> (0 qua Real) by Th4;
then mlt(P1,E1)=k |-> 0 by Th5;
then A30: Sum(mlt(P1,E1))=k*0 by RVSUM_1:110;
A31: Sum P = 0+p1 by A18,A28,RVSUM_1:104;
mlt(P1,F1)=k |-> 0 by A29,Th5;
then Sum(mlt(P1,F1))=k*0 by RVSUM_1:110;
hence thesis by A17,A21,A22,A24,A30,A31;
suppose A32:Sum P1 <>0;
then A33: Sum(mlt(P,E))=Sum P1*(Sum P1)"*Sum(mlt(P1,E1))+p1*e1
by A21,XCMPLX_0:def 7
.=Sum P1*((Sum P1)"*Sum(mlt(P1,E1)))+p1*e1 by XCMPLX_1:4
.=Sum P1*(Sum((Sum P1)"*mlt(P1,E1)))+p1*e1 by RVSUM_1:117
.=Sum P1*Sum(mlt((Sum P1)"*P1,E1))+p1*e1 by RVSUM_1:94;
Sum P1+p1 = 1 by A17,A18,RVSUM_1:104;
then A34: p1 = 1 - Sum P1 by XCMPLX_1:26;
A35: 0 <= Sum P1 & Sum P1 <= 1
proof
thus 0 <= Sum P1 by A25,RVSUM_1:114;
len P1 + 1 = len P by A18,FINSEQ_2:19;
then len P1 + 1 in Seg len P by FINSEQ_1:6;
then A36: len P1 + 1 in dom P by FINSEQ_1:def 3;
P.(len P1+1) = p1 by A18,FINSEQ_1:59;
then p1 >= 0 by A17,A36;
hence thesis by A34,REAL_2:105;
end;
then A37: f.Sum(mlt(P,E)) <= Sum P1*f.Sum(mlt((Sum P1)"*P1,E1)) + p1*f.e1
by A13,A33,A34,RFUNCT_3:def 13;
f.Sum(mlt((Sum P1)"*P1,E1)) <= (Sum P1)"*Sum(mlt(P1,F1))
proof
A38: (Sum P1)"*Sum(mlt(P1,F1)) = Sum((Sum P1)"*mlt(P1,F1)) by RVSUM_1:117
.=Sum(mlt((Sum P1)"*P1,F1)) by RVSUM_1:94;
A39: Sum((Sum P1)"*P1) = (Sum P1)"*Sum
P1 by RVSUM_1:117 .= 1 by A32,XCMPLX_0:def 7;
for i being Nat st i in dom ((Sum P1)"*P1) holds
((Sum P1)"*P1).i >= 0 &
F1.i=f.(E1.i)
proof
let i be Nat such that
A40: i in dom ((Sum P1)"*P1);
i in Seg len ((Sum P1)"*P1) by A40,FINSEQ_1:def 3;
then A41: i in Seg k by FINSEQ_2:109;
A42: ((Sum P1)"*P1).i = (Sum P1)"*P1.i by RVSUM_1:67;
A43: (Sum P1)" > 0 by A32,A35,REAL_1:72;
A44: i in Seg len P1 by A41,FINSEQ_2:109;
then i in dom P1 by FINSEQ_1:def 3;
then P1.i >=0 by A25;
hence ((Sum P1)"*P1).i >= 0 by A42,A43,REAL_2:121;
i in Seg len F1 & i in Seg len E1 by A41,FINSEQ_2:109;
then A45: i in dom F1 & i in dom E1 by FINSEQ_1:def 3;
1 <= i & i <= len P1 by A44,FINSEQ_1:3;
then 1 <= i & i <= k & k <= k+1 by FINSEQ_2:109,NAT_1:29;
then 1 <= i & i <= k+1 by AXIOMS:22;
then i in Seg (k+1) by FINSEQ_1:3;
then i in Seg len P by FINSEQ_2:109;
then A46: i in dom P by FINSEQ_1:def 3;
F.i = F1.i & E.i = E1.i by A19,A20,A45,FINSEQ_1:def 7;
hence thesis by A17,A46;
end;
hence thesis by A16,A38,A39;
end;
then Sum P1*f.Sum(mlt((Sum P1)"*P1,E1)) <=
Sum P1*((Sum P1)"*Sum(mlt(P1,F1)))
by A35,AXIOMS:25;
then Sum P1*f.Sum(mlt((Sum P1)"*P1,E1)) + p1*f.e1
<= Sum P1*((Sum P1)"*Sum(mlt(P1,F1)))+p1*f.e1 by AXIOMS:24;
then f.Sum(mlt(P,E))<=Sum P1*((Sum P1)"*Sum
(mlt(P1,F1)))+p1*f.e1 by A37,AXIOMS:22;
then f.Sum(mlt(P,E)) <= Sum P1*(Sum P1)"*Sum(mlt(P1,F1))+p1*f.e1
by XCMPLX_1:4;
hence thesis by A22,A24,A32,XCMPLX_0:def 7;
end;
hence thesis;
end;
hence thesis;
end;
for k be Nat holds S[k] from Ind(A14,A15);
hence thesis;
end;
hence thesis;
end;
hence thesis by A2;
end;
theorem
for f being PartFunc of REAL,REAL, I being Interval, a being Real st
(ex x1,x2 being Real st x1 in I & x2 in I & x1 < a & a < x2) & f is_convex_on I
holds f is_continuous_in a
proof
let f be PartFunc of REAL,REAL, I be Interval, a be Real such that
A1:(ex x1,x2 being Real st x1 in I & x2 in I & x1<a & a<x2) & f is_convex_on I;
A2:I c= dom f by A1,RFUNCT_3:def 13;
consider x1,x2 being Real such that
A3:x1 in I & x2 in I & x1 < a & a < x2 by A1;
A4:a in I
proof
now per cases by MEASURE5:def 9;
suppose I is open_interval;
then consider p,q being R_eal such that
A5: p <=' q & I = ].p,q.[ by MEASURE5:def 5;
thus thesis by A3,A5,MEASURE6:38;
suppose I is closed_interval;
then consider p,q being R_eal such that
A6: p <=' q & I = [.p,q.] by MEASURE5:def 6;
thus thesis by A3,A6,MEASURE6:39;
suppose I is right_open_interval;
then consider p,q being R_eal such that
A7: p <=' q & I = [.p,q.[by MEASURE5:def 7;
thus thesis by A3,A7,MEASURE6:41;
suppose I is left_open_interval;
then consider p,q being R_eal such that
A8: p <=' q & I = ].p,q.] by MEASURE5:def 8;
thus thesis by A3,A8,MEASURE6:40;
end;
hence thesis;
end;
A9:for x being Real st x1<=x & x<=x2 & x<>a holds
(f.x1-f.a)/(x1-a) <= (f.x-f.a)/(x-a) &
(f.x-f.a)/(x-a) <= (f.x2-f.a)/(x2-a)
proof
let x be Real such that
A10: x1 <= x & x <= x2 & x<>a;
(f.x1-f.a)/(x1-a) <= (f.x-f.a)/(x-a) &
(f.x-f.a)/(x-a) <= (f.x2-f.a)/(x2-a)
proof
now per cases by A10,AXIOMS:21;
suppose A11:x < a;
A12: x in I
proof
now per cases by MEASURE5:def 9;
suppose I is open_interval;
then consider p,q being R_eal such that
A13: p <=' q & I = ].p,q.[ by MEASURE5:def 5;
thus thesis by A3,A10,A13,MEASURE6:38;
suppose I is closed_interval;
then consider p,q being R_eal such that
A14: p <=' q & I = [.p,q.] by MEASURE5:def 6;
thus thesis by A3,A10,A14,MEASURE6:39;
suppose I is right_open_interval;
then consider p,q being R_eal such that
A15: p <=' q & I = [.p,q.[by MEASURE5:def 7;
thus thesis by A3,A10,A15,MEASURE6:41;
suppose I is left_open_interval;
then consider p,q being R_eal such that
A16: p <=' q & I = ].p,q.] by MEASURE5:def 8;
thus thesis by A3,A10,A16,MEASURE6:40;
end;
hence thesis;
end;
then (f.a-f.x)/(a-x)<=(f.x2-f.x)/(x2-x) &
(f.x2-f.x)/(x2-x)<=(f.x2-f.a)/(x2-a) by A1,A3,A4,A11,Th16;
then (f.a-f.x)/(a-x)<=(f.x2-f.a)/(x2-a) by AXIOMS:22;
then (-(f.a-f.x))/(-(a-x)) <= (f.x2-f.a)/(x2-a) by XCMPLX_1:192
;
then A17: (f.x-f.a)/(-(a-x)) <= (f.x2-f.a)/(x2-a) by XCMPLX_1:143;
now per cases by A10,REAL_1:def 5;
suppose x1=x;
hence (f.x1-f.a)/(x1-a) <= (f.x-f.a)/(x-a);
suppose A18:x1 < x;
A19: (f.a-f.x)/(a-x) = (-(f.a-f.x))/(-(a-x)) by XCMPLX_1:192
.=(f.x-f.a)/(-(a-x)) by XCMPLX_1:143 .=(f.x-f.a)/(x-a) by XCMPLX_1:143;
(f.a-f.x1)/(a-x1) = (-(f.a-f.x1))/(-(a-x1)) by XCMPLX_1:192
.=(f.x1-f.a)/(-(a-x1)) by XCMPLX_1:143 .=(f.x1-f.a)/(x1-a) by XCMPLX_1:
143;
hence (f.x1-f.a)/(x1-a)<=(f.x-f.a)/(x-a) by A1,A3,A4,A11,A12,A18,A19,
Th16;
end;
hence thesis by A17,XCMPLX_1:143;
suppose A20:x > a;
A21: x in I
proof
now per cases by MEASURE5:def 9;
suppose I is open_interval;
then consider p,q being R_eal such that
A22: p <=' q & I = ].p,q.[ by MEASURE5:def 5;
thus thesis by A3,A10,A22,MEASURE6:38;
suppose I is closed_interval;
then consider p,q being R_eal such that
A23: p <=' q & I = [.p,q.] by MEASURE5:def 6;
thus thesis by A3,A10,A23,MEASURE6:39;
suppose I is right_open_interval;
then consider p,q being R_eal such that
A24: p <=' q & I = [.p,q.[ by MEASURE5:def 7;
thus thesis by A3,A10,A24,MEASURE6:41;
suppose I is left_open_interval;
then consider p,q being R_eal such that
A25: p <=' q & I = ].p,q.] by MEASURE5:def 8;
thus thesis by A3,A10,A25,MEASURE6:40;
end;
hence thesis;
end;
then A26: (f.a-f.x1)/(a-x1)<=(f.x-f.x1)/(x-x1) &
(f.x-f.x1)/(x-x1)<=(f.x-f.a)/(x-a) by A1,A3,A4,A20,Th16;
(f.a-f.x1)/(a-x1) = (-(f.a-f.x1))/(-(a-x1)) by XCMPLX_1:192
.=(f.x1-f.a)/(-(a-x1)) by XCMPLX_1:143 .=(f.x1-f.a)/(x1-a) by XCMPLX_1:
143;
hence (f.x1-f.a)/(x1-a) <= (f.x-f.a)/(x-a) by A26,AXIOMS:22;
now per cases by A10,REAL_1:def 5;
suppose x=x2;
hence (f.x-f.a)/(x-a) <= (f.x2-f.a)/(x2-a);
suppose x<x2;
hence (f.x-f.a)/(x-a)<=(f.x2-f.a)/(x2-a) by A1,A3,A4,A20,A21,Th16;
end;
hence (f.x-f.a)/(x-a) <= (f.x2-f.a)/(x2-a);
end;
hence thesis;
end;
hence thesis;
end;
set M = max(abs((f.x1-f.a)/(x1-a)),abs((f.x2-f.a)/(x2-a)));
A27: abs((f.x1-f.a)/(x1-a)) >= 0 & abs((f.x2-f.a)/(x2-a)) >= 0
by ABSVALUE:5;
then A28:min(abs((f.x1-f.a)/(x1-a)),abs((f.x2-f.a)/(x2-a))) >= 0 by SQUARE_1:39
;
A29: max(abs((f.x1-f.a)/(x1-a)),abs((f.x2-f.a)/(x2-a)))
>= min(abs((f.x1-f.a)/(x1-a)),abs((f.x2-f.a)/(x2-a))) by Th1;
A30:M >= 0 by A28,Th1;
A31:for x being real number st x1<=x & x<=x2 & x<>a holds
abs(f.x-f.a)<=M*abs(x-a)
proof
let x be real number such that A32:x1<=x & x<=x2 & x<>a;
reconsider x as Real by XREAL_0:def 1;
x<a or x>a by A32,AXIOMS:21;
then x-a <> 0 by REAL_2:105,SQUARE_1:11;
then A33: abs(x-a) > 0 by ABSVALUE:6;
A34: (f.x1-f.a)/(x1-a) <= (f.x-f.a)/(x-a) &
(f.x-f.a)/(x-a) <= (f.x2-f.a)/(x2-a) by A9,A32;
-abs((f.x1-f.a)/(x1-a)) <= (f.x1-f.a)/(x1-a) &
(f.x2-f.a)/(x2-a) <= abs((f.x2-f.a)/(x2-a)) by ABSVALUE:11;
then A35: -abs((f.x1-f.a)/(x1-a)) <= (f.x-f.a)/(x-a) &
(f.x-f.a)/(x-a) <= abs((f.x2-f.a)/(x2-a)) by A34,AXIOMS:22;
now per cases;
suppose abs((f.x1-f.a)/(x1-a)) <= abs((f.x2-f.a)/(x2-a));
then -abs((f.x1-f.a)/(x1-a)) >= -abs((f.x2-f.a)/(x2-a))
by REAL_1:50;
then -abs((f.x2-f.a)/(x2-a)) <= (f.x-f.a)/(x-a) by A35,AXIOMS:22;
then abs((f.x-f.a)/(x-a)) <= abs((f.x2-f.a)/(x2-a)) by A35,ABSVALUE:12;
then A36: abs((f.x-f.a))/abs((x-a)) <= abs((f.x2-f.a)/(x2-a)) by ABSVALUE:16;
abs((f.x2-f.a)/(x2-a)) <= M by SQUARE_1:46;
then abs((f.x-f.a))/abs((x-a)) <= M by A36,AXIOMS:22;
hence thesis by A33,REAL_2:178;
suppose abs((f.x1-f.a)/(x1-a)) >= abs((f.x2-f.a)/(x2-a));
then (f.x-f.a)/(x-a) <= abs((f.x1-f.a)/(x1-a)) by A35,AXIOMS:22;
then abs((f.x-f.a)/(x-a)) <= abs((f.x1-f.a)/(x1-a)) by A35,ABSVALUE:12;
then A37: abs((f.x-f.a))/abs((x-a)) <= abs((f.x1-f.a)/(x1-a)) by ABSVALUE:16;
abs((f.x1-f.a)/(x1-a)) <= M by SQUARE_1:46;
then abs((f.x-f.a))/abs((x-a)) <= M by A37,AXIOMS:22;
hence thesis by A33,REAL_2:178;
end;
hence thesis;
end;
for r being real number st 0<r ex s being real number st 0<s &
for x being real number st
x in dom f & abs(x-a)<s holds abs(f.x-f.a)<r
proof
let r be real number such that
A38: 0<r;
reconsider r as Real by XREAL_0:def 1;
ex s being real number st 0<s & for x being real number st
x in dom f & abs(x-a)<s holds abs(f.x-f.a)<r
proof
now per cases by A27,A29,SQUARE_1:39;
suppose A39:M>0;
set s = min(r/M,min(a-x1,x2-a));
A40: s>0
proof
A41: min(a-x1,x2-a) > 0
proof
now per cases by SQUARE_1:38;
suppose min(a-x1,x2-a)=a-x1;
hence thesis by A3,SQUARE_1:11;
suppose min(a-x1,x2-a)=x2-a;
hence thesis by A3,SQUARE_1:11;
end;
hence thesis;
end;
now per cases by SQUARE_1:38;
suppose s = r/M;
hence thesis by A38,A39,REAL_2:127;
suppose s = min(a-x1,x2-a);
hence thesis by A41;
end;
hence thesis;
end;
for x being real number st x in dom f & abs(x-a)<s holds
abs(f.x-f.a)<r
proof
let x be real number such that A42:x in dom f & abs(x-a)<s;
A43: s <= r/M & s<=min(a-x1,x2-a) by SQUARE_1:35;
min(a-x1,x2-a)<=a-x1 & min(a-x1,x2-a)<=x2-a by SQUARE_1:35;
then s <= a-x1 & s <= x2-a by A43,AXIOMS:22;
then abs(x-a)<a-x1 & abs(x-a)<x2-a by A42,AXIOMS:22;
then -(a-x1) <= x-a & x-a <= x2-a by ABSVALUE:12;
then x1-a <= x-a & x-a <=x2-a by XCMPLX_1:143;
then A44: x1 <= x & x <= x2 by REAL_1:54;
now per cases;
suppose x<>a;
then A45: abs(f.x-f.a)<=M*abs(x-a) by A31,A44;
now per cases;
suppose A46:M<>0;
then A47: M*abs(x-a) < M*s by A30,A42,REAL_1:70;
M*s <= M*(r/M) by A28,A29,A43,AXIOMS:25;
then M*abs(x-a) < M*(r/M) by A47,AXIOMS:22;
then M*abs(x-a) < (r*M)/M by Lm4;
then M*abs(x-a) < r*(M/M) by Lm4;
then M*abs(x-a) < r*1 by A46,XCMPLX_1:60;
hence thesis by A45,AXIOMS:22;
suppose M=0;
hence thesis by A38,A45;
end;
hence thesis;
suppose x=a;
then f.x-f.a=0 by XCMPLX_1:14;
hence thesis by A38,ABSVALUE:7;
end;
hence thesis;
end;
hence thesis by A40;
suppose A48:M=0;
A49: for x being real number st x1<=x & x<=x2 & x<>a holds
abs(f.x-f.a)=0
proof
let x be real number such that A50:x1<=x & x<=x2 & x<>a;
abs(f.x-f.a)<=M*abs(x-a) by A31,A50;
hence thesis by A48,ABSVALUE:5;
end;
set s = min(a-x1,x2-a);
A51: s > 0
proof
now per cases by SQUARE_1:38;
suppose s=a-x1;
hence thesis by A3,SQUARE_1:11;
suppose s=x2-a;
hence thesis by A3,SQUARE_1:11;
end;
hence thesis;
end;
for x being real number st x in dom f & abs(x-a)<s holds
abs(f.x-f.a)<r
proof
let x be real number such that A52:x in dom f & abs(x-a)<s;
s<=a-x1 & s<=x2-a by SQUARE_1:35;
then abs(x-a)<a-x1 & abs(x-a)<x2-a by A52,AXIOMS:22;
then -(a-x1) <= x-a & x-a <= x2-a by ABSVALUE:12;
then x1-a <= x-a & x-a <=x2-a by XCMPLX_1:143;
then A53: x1 <= x & x <= x2 by REAL_1:54;
now per cases;
suppose x<>a;
hence thesis by A38,A49,A53;
suppose x=a;
then f.x-f.a=0 by XCMPLX_1:14;
hence thesis by A38,ABSVALUE:7;
end;
hence thesis;
end;
hence thesis by A51;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis by A2,A4,FCONT_1:3;
end;
begin :: Definitions of several convexity and semicontinuity concepts
definition
let f, X;
pred f is_quasiconvex_on X means :Def2:
X c= dom f &
for p being Real st 0<p & p<1 holds
for r,s being Real st r in X & s in X & p*r + (1-p)*s in X holds
f.(p*r + (1-p)*s) <= max(f.r,f.s);
end;
definition
let f, X;
pred f is_strictly_quasiconvex_on X means :Def3:
X c= dom f &
for p being Real st 0<p & p<1 holds
for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & f.r <> f.s holds
f.(p*r + (1-p)*s) < max(f.r,f.s);
end;
definition
let f, X;
pred f is_strongly_quasiconvex_on X means :Def4:
X c= dom f &
for p being Real st 0<p & p<1 holds
for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
f.(p*r + (1-p)*s) < max(f.r,f.s);
end;
definition let f; let x0 be real number;
pred f is_upper_semicontinuous_in x0 means :Def5:
x0 in dom f &
(for r st 0<r ex s st 0<s & for x st
x in dom f & abs(x-x0)<s holds f.x0-f.x<r);
end;
definition let f,X;
pred f is_upper_semicontinuous_on X means :Def6:
X c= dom f & for x0 st x0 in X holds f|X is_upper_semicontinuous_in x0;
end;
definition let f; let x0 be real number;
pred f is_lower_semicontinuous_in x0 means :Def7:
x0 in dom f &
(for r st 0<r ex s st 0<s &
for x st x in dom f & abs(x-x0)<s holds f.x-f.x0<r);
end;
definition let f,X;
pred f is_lower_semicontinuous_on X means :Def8:
X c= dom f & for x0 st x0 in X holds f|X is_lower_semicontinuous_in x0;
end;
theorem Th20:
for x0 be real number, f holds
f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0
iff f is_continuous_in x0
proof
let x0 be real number, f;
A1:f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0
implies f is_continuous_in x0
proof
assume
A2: f is_upper_semicontinuous_in x0&f is_lower_semicontinuous_in x0;
then A3: x0 in dom f &
(for r st 0<r ex s st 0<s & for x st x in dom f & abs(x-x0)<s holds
f.x-f.x0<r) &
(for r st 0<r ex s st 0<s & for x st x in dom f & abs(x-x0)<s holds
f.x0-f.x<r) by Def5,Def7;
for r be real number st 0<r ex s be real number st 0<s &
for x be real number st x in dom f & abs(x-x0)<s holds
abs(f.x-f.x0)<r
proof
let r be real number such that A4: 0<r;
A5: r is Real by XREAL_0:def 1;
then consider s1 being Real such that
A6: 0<s1 & for x st x in dom f & abs(x-x0)<s1 holds f.x-f.x0<r by A2,A4,Def7;
consider s2 being Real such that
A7: 0<s2 &
for x st x in dom f & abs(x-x0)<s2 holds f.x0-f.x<r by A2,A4,A5,Def5;
set s = min(s1,s2);
A8: s > 0
proof
now per cases;
suppose s1<=s2;
hence 0<s by A6,SQUARE_1:def 1;
suppose not (s1<=s2);
hence 0<s by A7,SQUARE_1:def 1;
end;
hence thesis;
end;
A9: for x be real number st x in dom f & abs(x-x0)<s holds abs(f.x-f.x0)<r
proof
let x be real number such that A10:x in dom f & abs(x-x0)<s;
A11: x is Real by XREAL_0:def 1;
s <= s1 & s <= s2 by SQUARE_1:35;
then abs(x-x0)<s1 & abs(x-x0)<s2 by A10,AXIOMS:22;
then A12: f.x-f.x0<r & f.x0-f.x<r by A6,A7,A10,A11;
then f.x-f.x0<r & -(f.x0-f.x)>-r by REAL_1:50;
then f.x-f.x0<r & f.x-f.x0>-r by XCMPLX_1:143;
then A13: abs(f.x-f.x0)<=r & f.x-f.x0<>r & f.x-f.x0<>-r by ABSVALUE:12;
abs(f.x-f.x0)<>r
proof
assume A14:abs(f.x-f.x0)=r;
now per cases;
suppose f.x-f.x0>=0;
hence contradiction by A12,A14,ABSVALUE:def 1;
suppose not (f.x-f.x0>=0);
then abs(f.x-f.x0)=-(f.x-f.x0) by ABSVALUE:def 1;
hence contradiction by A12,A14,XCMPLX_1:143;
end;
hence thesis;
end;
hence thesis by A13,REAL_1:def 5;
end;
take s;
thus thesis by A8,A9;
end;
hence f is_continuous_in x0 by A3,FCONT_1:3;
end;
f is_continuous_in x0 implies
f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0
proof
assume A15:f is_continuous_in x0;
then A16:x0 in dom f &
for r be real number st 0<r ex s be real number st 0<s &
for x be real number st x in dom f & abs(x-x0)<s holds
abs(f.x-f.x0)<r by FCONT_1:3;
A17:for r st 0<r ex s st 0<s & for x st x in dom f & abs(x-x0)<s holds
f.x-f.x0<r
proof
let r such that A18:0<r;
consider s be real number such that
A19: 0<s & for x be real number st x in dom f &
abs(x-x0)<s holds abs(f.x-f.x0)<r
by A15,A18,FCONT_1:3;
A20: for x st x in dom f & abs(x-x0)<s holds f.x-f.x0<r
proof
let x such that A21:x in dom f & abs(x-x0)<s;
A22: abs(f.x-f.x0)<r by A19,A21;
f.x-f.x0<=abs(f.x-f.x0) by ABSVALUE:11;
hence thesis by A22,AXIOMS:22;
end;
take s;
thus s is Real by XREAL_0:def 1;
thus thesis by A19,A20;
end;
for r st 0<r ex s st 0<s & for x st x in dom f & abs(x-x0)<s holds
f.x0-f.x<r
proof
let r such that A23:0<r;
consider s be real number such that
A24: 0<s & for x be real number st x in dom f & abs(x-x0)<s
holds abs(f.x-f.x0)<r by A15,A23,FCONT_1:3;
A25: for x st x in dom f & abs(x-x0)<s holds f.x0-f.x<r
proof
let x such that A26:x in dom f & abs(x-x0)<s;
A27: abs(f.x-f.x0)<r by A24,A26;
f.x-f.x0>=-abs(f.x-f.x0) by ABSVALUE:11;
then -(f.x-f.x0)<=abs(f.x-f.x0) by REAL_2:110;
then f.x0-f.x <= abs(f.x-f.x0) by XCMPLX_1:143;
hence thesis by A27,AXIOMS:22;
end;
take s;
thus s is Real by XREAL_0:def 1;
thus thesis by A24,A25;
end;
hence thesis by A16,A17,Def5,Def7;
end;
hence thesis by A1;
end;
theorem
for X, f holds
f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X
iff f is_continuous_on X
proof
let X, f;
A1:f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X
implies f is_continuous_on X
proof
assume
A2: f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X;
X c= dom f & for x0 be real number st x0 in X holds f|X is_continuous_in
x0
proof
thus X c= dom f by A2,Def6;
let x0 be real number such that A3:x0 in X;
x0 is Real by XREAL_0:def 1;
then f|X is_upper_semicontinuous_in x0 & f|X is_lower_semicontinuous_in
x0
by A2,A3,Def6,Def8;
hence thesis by Th20;
end;
hence thesis by FCONT_1:def 2;
end;
f is_continuous_on X implies
f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X
proof
assume A4:f is_continuous_on X;
X c= dom f &
(for x0 st x0 in X holds f|X is_upper_semicontinuous_in x0) &
(for x0 st x0 in X holds f|X is_lower_semicontinuous_in x0)
proof
thus X c= dom f by A4,FCONT_1:def 2;
A5: for x0 st x0 in X holds f|X is_upper_semicontinuous_in x0
proof
let x0; assume
A6: x0 in X;
f|X is_upper_semicontinuous_in x0
proof
f|X is_continuous_in x0 by A4,A6,FCONT_1:def 2;
hence thesis by Th20;
end;
hence thesis;
end;
for x0 st x0 in X holds f|X is_lower_semicontinuous_in x0
proof
let x0; assume
A7: x0 in X;
f|X is_lower_semicontinuous_in x0
proof
f|X is_continuous_in x0 by A4,A7,FCONT_1:def 2;
hence thesis by Th20;
end;
hence thesis;
end;
hence thesis by A5;
end;
hence thesis by Def6,Def8;
end;
hence thesis by A1;
end;
theorem
for X, f st f is_strictly_convex_on X holds f is_strongly_quasiconvex_on X
proof
let X, f such that
A1:f is_strictly_convex_on X;
A2:X c= dom f by A1,Def1;
for p being Real st 0<p & p<1 holds
for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
f.(p*r + (1-p)*s) < max(f.r,f.s)
proof
let p be Real;
assume A3:0<p & p<1;
for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
f.(p*r + (1-p)*s) < max(f.r,f.s)
proof
let r,s be Real;
assume r in X & s in X & p*r + (1-p)*s in X & r <> s;
then A4: f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s by A1,A3,Def1;
A5: 1-p > 0 by A3,SQUARE_1:11;
f.r <= max(f.r,f.s) & f.s <= max(f.r,f.s) by SQUARE_1:46;
then p*f.r<=p*max(f.r,f.s) & (1-p)*f.s<=(1-p)*max(f.r,f.s)
by A3,A5,AXIOMS:25;
then p*f.r + (1-p)*f.s <= p*max(f.r,f.s)+(1-p)*max(f.r,f.s) by REAL_1:55;
then p*f.r + (1-p)*f.s <= max(f.r,f.s) by Lm1;
hence thesis by A4,AXIOMS:22;
end;
hence thesis;
end;
hence thesis by A2,Def4;
end;
theorem
for X, f st f is_strongly_quasiconvex_on X holds f is_quasiconvex_on X
proof
let X,f such that
A1:f is_strongly_quasiconvex_on X;
A2:X c= dom f by A1,Def4;
for p being Real st 0<p & p<1 holds
for r,s being Real st r in X & s in X & p*r + (1-p)*s in X holds
f.(p*r + (1-p)*s) <= max(f.r,f.s)
proof
let p be Real such that
A3: 0<p & p<1;
for r,s being Real st r in X & s in X & p*r + (1-p)*s in X holds
f.(p*r + (1-p)*s) <= max(f.r,f.s)
proof
let r,s be Real such that
A4: r in X & s in X & p*r + (1-p)*s in X;
now per cases;
suppose r<>s;
hence f.(p*r + (1-p)*s) <= max(f.r,f.s) by A1,A3,A4,Def4;
suppose r=s;
hence f.(p*r + (1-p)*s) <= max(f.r,f.s) by Lm1;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis by A2,Def2;
end;
theorem
for X, f st f is_convex_on X holds f is_strictly_quasiconvex_on X
proof
let X,f such that
A1:f is_convex_on X;
A2:X c= dom f by A1,RFUNCT_3:def 13;
for p being Real st 0<p & p<1 holds
for r,s being Real st r in X & s in X &
p*r + (1-p)*s in X & f.r <> f.s holds
f.(p*r + (1-p)*s) < max(f.r,f.s)
proof
let p be Real such that
A3: 0<p & p<1;
for r,s being Real st
r in X & s in X & p*r + (1-p)*s in X & f.r <> f.s holds
f.(p*r + (1-p)*s) < max(f.r,f.s)
proof
let r,s be Real such that
A4: r in X & s in X & p*r + (1-p)*s in X & f.r <> f.s;
A5: f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s by A1,A3,A4,RFUNCT_3:def 13;
A6: 1-p > 0 by A3,SQUARE_1:11;
now per cases by A4,REAL_1:def 5;
suppose f.r < f.s;
then p*f.r < p*f.s by A3,REAL_1:70;
then p*f.r + (1-p)*f.s < p*f.s + (1-p)*f.s by REAL_1:53;
then p*f.r + (1-p)*f.s < f.s by Lm1;
then A7: f.(p*r + (1-p)*s) < f.s by A5,AXIOMS:22;
f.s <= max(f.r,f.s) by SQUARE_1:46;
hence f.(p*r + (1-p)*s) < max(f.r,f.s) by A7,AXIOMS:22;
suppose f.r > f.s;
then (1-p)*f.r > (1-p)*f.s by A6,REAL_1:70;
then p*f.r + (1-p)*f.s < p*f.r + (1-p)*f.r by REAL_1:53;
then p*f.r + (1-p)*f.s < f.r by Lm1;
then A8: f.(p*r + (1-p)*s) < f.r by A5,AXIOMS:22;
f.r <= max(f.r,f.s) by SQUARE_1:46;
hence thesis by A8,AXIOMS:22;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis by A2,Def3;
end;
theorem
for X, f st f is_strongly_quasiconvex_on X holds
f is_strictly_quasiconvex_on X
proof
let X, f such that
A1:f is_strongly_quasiconvex_on X;
A2:X c= dom f by A1,Def4;
for p being Real st 0<p & p<1 holds
for r,s being Real st
r in X & s in X & p*r + (1-p)*s in X & f.r <> f.s holds
f.(p*r + (1-p)*s) < max(f.r,f.s) by A1,Def4;
hence thesis by A2,Def3;
end;
theorem
for X, f st f is_strictly_quasiconvex_on X & f is one-to-one holds
f is_strongly_quasiconvex_on X
proof
let X, f such that
A1:f is_strictly_quasiconvex_on X & f is one-to-one;
A2:X c= dom f by A1,Def3;
for p being Real st 0<p & p<1 holds
for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
f.(p*r + (1-p)*s) < max(f.r,f.s)
proof
let p be Real such that
A3: 0<p & p<1;
for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
f.(p*r + (1-p)*s) < max(f.r,f.s)
proof
let r,s be Real such that
A4: r in X & s in X & p*r + (1-p)*s in X & r <> s;
f.(p*r + (1-p)*s) < max(f.r,f.s)
proof
f.r <> f.s by A1,A2,A4,FUNCT_1:def 8;
hence thesis by A1,A3,A4,Def3;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis by A2,Def4;
end;