:: Introduction to Several Concepts of Convexity and Semicontinuity
:: for Function from REAL to REAL
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received March 23, 2000
:: Copyright (c) 2000-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, REAL_1, PARTFUN1, SUBSET_1, XXREAL_0, FINSEQ_2, RVSUM_1,
ORDINAL4, FINSEQ_1, RELAT_1, ARYTM_3, NAT_1, FUNCT_1, CARD_3, CARD_1,
TARSKI, ARYTM_1, RFUNCT_3, XXREAL_1, VALUED_1, XBOOLE_0, BINOP_2,
MEASURE5, FCONT_1, COMPLEX1, ORDINAL2, RFUNCT_4, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
RELAT_1, COMPLEX1, NAT_1, FUNCT_1, FINSEQ_1, REAL_1, FINSEQ_2, PARTFUN1,
FUNCOP_1, FINSEQOP, BINOP_1, BINOP_2, VALUED_1, RVSUM_1, RCOMP_1,
RFUNCT_3, MEASURE5, FCONT_1, XXREAL_0;
constructors BINOP_1, REAL_1, NAT_1, BINOP_2, COMPLEX1, FINSEQOP, RCOMP_1,
RVSUM_1, FCONT_1, RFUNCT_3, MEASURE5, XXREAL_2, RELSET_1, FINSEQ_4,
CARD_3, FUNCOP_1;
registrations RELSET_1, NUMBERS, XXREAL_0, XREAL_0, BINOP_2, MEMBERED,
FINSEQ_2, VALUED_0, FINSEQ_1, FUNCT_1, RVSUM_1, ORDINAL1;
requirements NUMERALS, SUBSET, REAL, BOOLE, ARITHM;
equalities RVSUM_1, ORDINAL1;
theorems RCOMP_1, RFUNCT_3, TARSKI, PARTFUN1, FINSEQ_1, FINSEQ_2, RVSUM_1,
NAT_1, FCONT_1, ABSVALUE, FUNCT_1, XREAL_0, XBOOLE_1, XCMPLX_0, XCMPLX_1,
XREAL_1, COMPLEX1, XXREAL_0, FINSEQOP, VALUED_1, XXREAL_2, RELAT_1,
CARD_1;
schemes NAT_1;
begin
reserve a,b,p,r,r1,r2,s,s1,s2,x0,x for Real;
reserve f,g for PartFunc of REAL,REAL;
reserve X,Y for set;
theorem Th1:
for a, b being Real holds max(a,b) >= min(a,b)
proof
let a, b be Real;
per cases by XXREAL_0:15;
suppose
min(a,b)=a;
hence thesis by XXREAL_0:25;
end;
suppose
min(a,b)=b;
hence thesis by XXREAL_0:25;
end;
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;
reconsider r1,r2 as Element of REAL by XREAL_0:def 1;
len (R1^<*r1*>) = len R1 + 1 by FINSEQ_2:16
.= n+1 by CARD_1:def 7
.= len R2 + 1 by CARD_1:def 7
.= len (R2^<*r2*>) by FINSEQ_2:16;
then
A1: len(mlt(R1^<*r1*>,R2^<*r2*>)) = len (R1^<*r1*>) by FINSEQ_2:72
.= len R1 + 1 by FINSEQ_2:16
.= n+1 by CARD_1:def 7;
A2: 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
A3: k in Seg (n+1);
A4: k<=n+1 by A3,FINSEQ_1:1;
now
per cases by A4,XXREAL_0:1;
suppose
k<n+1;
then
A5: k<=n by NAT_1:13;
1<=k by A3,FINSEQ_1:1;
then
A6: k in Seg n by A5,FINSEQ_1:1;
then k in Seg len R1 by CARD_1:def 7;
then k in dom R1 by FINSEQ_1:def 3;
then
A7: (R1^<*r1*>).k = R1.k by FINSEQ_1:def 7;
k in Seg len R2 by A6,CARD_1:def 7;
then k in dom R2 by FINSEQ_1:def 3;
then
(R2^<*r2*>).k = R2.k by FINSEQ_1:def 7;
then A8: mlt(R1^<*r1*>,R2^<*r2*>).k = (R1.k)*(R2.k) by A7,RVSUM_1:59;
len (mlt(R1,R2)) = n by CARD_1:def 7;
then
k in dom mlt(R1,R2) by A6,FINSEQ_1:def 3;
then (mlt(R1,R2)^<*r1*r2*>).k = mlt(R1,R2).k by FINSEQ_1:def 7;
hence thesis by A8,RVSUM_1:59;
end;
suppose
A9: k=n+1;
then k=len R1+1 by CARD_1:def 7;
then
A10: (R1^<*r1*>).k=r1 by FINSEQ_1:42;
A11: n+1 = len (mlt(R1,R2)) + 1 by CARD_1:def 7;
k=len R2+1 by A9,CARD_1:def 7;
then
(R2^<*r2*>).k=r2 by FINSEQ_1:42;
then mlt(R1^<*r1*>,R2^<*r2*>).k = r1*r2 by A10,RVSUM_1:59;
hence thesis by A9,A11,FINSEQ_1:42;
end;
end;
hence thesis;
end;
reconsider rr = r1*r2 as Element of REAL;
mlt(R1^<*r1*>,R2^<*r2*>) is Element of (n+1)-tuples_on REAL
by A1,FINSEQ_2:92;
hence thesis by A2,FINSEQ_2:119;
end;
theorem Th3:
for n being Nat, R being Element of n-tuples_on REAL
st Sum R=0 & (for i being Element of NAT st i in dom R holds 0 <= R.i) holds
for i being Element of 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 and
A2: for i being Element of NAT st i in dom R holds 0 <= R.i;
A3: for i being Nat st i in dom R holds 0 <= R.i by A2;
given k being Element of NAT such that
A4: k in dom R and
A5: R.k <> 0;
0 <= R.k by A2,A4;
hence contradiction by A1,A3,A4,A5,RVSUM_1:85;
end;
theorem Th4:
for n being Nat, R being Element of n-tuples_on REAL
st (for i being Element of 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 Element of NAT st i in dom R holds 0 = R.i;
A2: for k be Nat st 1 <= k & k <= len R holds R.k = (n |-> 0).k
proof
let k be Nat;
assume 1 <= k & k <= len R;
then
k in Seg len R by FINSEQ_1:1;
then k in dom R by FINSEQ_1:def 3;
then
A3: R.k = 0 by A1;
thus thesis by A3;
end;
len R = n by CARD_1:def 7
.= len (n |-> 0) by CARD_1:def 7;
hence thesis by A2,FINSEQ_1:14;
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(mlt(n |-> In(0,REAL),R)) =n by CARD_1:def 7;
A2: for k be Nat 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 be Nat;
assume 1 <= k & k <= len mlt(n |-> (0 qua Real),R);
mlt(n |-> (0 qua Real),R).k = (n |-> (0 qua Real)).k*R.k by RVSUM_1:60
.=0*R.k;
hence thesis;
end;
len (n |-> (0 qua Real)) = n by CARD_1:def 7;
hence thesis by A1,A2,FINSEQ_1:14;
end;
begin :: Convex and strictly convex functions
definition
let f, X;
pred f is_strictly_convex_on X means
X c= dom f & for p being Real st 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;
end;
theorem
f is_strictly_convex_on X implies f is_convex_on X
proof
assume
A1: f is_strictly_convex_on X;
A2: 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,XXREAL_0:1;
suppose
p=0;
hence thesis;
end;
suppose
p=1;
hence thesis;
end;
suppose
A5: 0<p & p<1;
now
per cases;
suppose
r=s;
hence thesis;
end;
suppose
r<>s;
hence thesis by A1,A4,A5;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis;
end;
X c= dom f by A1;
hence thesis by A2,RFUNCT_3:def 12;
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
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: 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
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;
let p be Real;
assume that
A3: 0<p and
A4: p<1;
A5: 0<=1-p by A4,XREAL_1:48;
A6: p*b+(1-p)*b=b;
A7: p*a+(1-p)*a=a;
let x,y be Real;
assume that
A8: x in [.a,b.] and
A9: y in [.a,b.] and
A10: x <> y;
A11: ex r2 st r2=y & a<=r2 & r2<=b by A1,A9;
then
A12: (1-p)*y<=(1-p)*b by A5,XREAL_1:64;
A13: ex r1 st r1=x & a<=r1 & r1<=b by A1,A8;
then p*x<=p*b by A3,XREAL_1:64;
then
A14: p*x+(1-p)*y<=b by A12,A6,XREAL_1:7;
A15: (1-p)*a<=(1-p)*y by A5,A11,XREAL_1:64;
p*a<=p*x by A3,A13,XREAL_1:64;
then a<=p*x+(1-p)*y by A15,A7,XREAL_1:7;
then p*x+(1-p)*y in ab by A14;
hence thesis by A1,A2,A3,A4,A8,A9,A10;
end;
assume that
A16: [.a,b.] c= dom f and
A17: for p be Real st 0<p & p<1
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;
thus [.a,b.] c= dom f by A16;
let p be Real;
assume
A18: 0<p & p<1;
let x,y be Real;
assume that
A19: x in [.a,b.] & y in [.a,b.] and
p*x + (1-p)*y in [.a,b.];
thus thesis by A17,A18,A19;
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: (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
A2: X c= dom f and
A3: 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
A4: 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
A5: 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
per cases by A4,XXREAL_0:1;
suppose
p=0;
hence thesis;
end;
suppose
p=1;
hence thesis;
end;
suppose
A6: 0<p & p<1;
then
A7: 0 < 1-p by XREAL_1:50;
per cases by XXREAL_0:1;
suppose
r=s;
hence thesis;
end;
suppose
A8: r>s;
set t = p*r + (1-p)*s;
A9: r-s > 0 by A8,XREAL_1:50;
A10: r - t = (1-p)*(r-s);
then r - t > 0 by A7,A9,XREAL_1:129;
then
A11: t < r by XREAL_1:47;
A12: t - s =p*(r-s);
then
A13: (t-s)/(r-s)=p by A9,XCMPLX_1:89;
t - s > 0 by A6,A9,A12,XREAL_1:129;
then
A14: s < t by XREAL_1:47;
(r-t)/(r-s)=(1-p) by A9,A10,XCMPLX_1:89;
hence thesis by A3,A5,A14,A11,A13;
end;
suppose
A15: r<s;
set t = p*r + (1-p)*s;
A16: s-r > 0 by A15,XREAL_1:50;
A17: s - t = p*(s-r);
then s - t > 0 by A6,A16,XREAL_1:129;
then
A18: t < s by XREAL_1:47;
A19: t - r = (1-p)*(s-r);
then
A20: (t-r)/(s-r)=1-p by A16,XCMPLX_1:89;
t - r > 0 by A7,A16,A19,XREAL_1:129;
then
A21: r < t by XREAL_1:47;
(s-t)/(s-r)=p by A16,A17,XCMPLX_1:89;
hence thesis by A3,A5,A21,A18,A20;
end;
end;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis by A2,RFUNCT_3:def 12;
end;
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
A22: 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 that
A23: a in X & b in X & c in X and
A24: a < b & b < c;
set p = (c-b)/(c-a);
A25: c-b < c-a & 0 < c-b by A24,XREAL_1:10,50;
then
A26: (c-b)/(c-a) < 1 by XREAL_1:189;
A27: p+(b-a)/(c-a) = ((c-b)+(b-a))/(c-a) by XCMPLX_1:62
.= 1 by A25,XCMPLX_1:60;
then p*a + (1-p)*c = (a*(c-b))/(c-a)+c*((b-a)/(c-a)) by XCMPLX_1:74
.= (a*(c-b))/(c-a)+(c*(b-a))/(c-a) by XCMPLX_1:74
.= ((c*a-b*a)+(b-a)*c)/(c-a) by XCMPLX_1:62
.= b*(c-a)/(c-a);
then p*a + (1-p)*c = b by A25,XCMPLX_1:89;
hence thesis by A22,A23,A25,A26,A27,RFUNCT_3:def 12;
end;
hence thesis by A22,RFUNCT_3:def 12;
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: (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
A2: X c= dom f and
A3: 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
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
A4: 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 that
A5: r in X & s in X & p*r + (1-p)*s in X and
A6: r <> s;
f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s
proof
now
per cases by A4;
suppose
A7: 0<p & p<1;
then
A8: 0 < 1-p by XREAL_1:50;
now
per cases by A6,XXREAL_0:1;
suppose
A9: r>s;
set t = p*r + (1-p)*s;
A10: r-s > 0 by A9,XREAL_1:50;
A11: r - t = (1-p)*(r-s);
then r - t > 0 by A8,A10,XREAL_1:129;
then
A12: t < r by XREAL_1:47;
A13: t - s =p*(r-s);
then
A14: (t-s)/(r-s)=p by A10,XCMPLX_1:89;
t - s > 0 by A7,A10,A13,XREAL_1:129;
then
A15: s < t by XREAL_1:47;
(r-t)/(r-s)=(1-p) by A10,A11,XCMPLX_1:89;
hence thesis by A3,A5,A15,A12,A14;
end;
suppose
A16: r<s;
set t = p*r + (1-p)*s;
A17: s-r > 0 by A16,XREAL_1:50;
A18: s - t = p*(s-r);
then s - t > 0 by A7,A17,XREAL_1:129;
then
A19: t < s by XREAL_1:47;
A20: t - r = (1-p)*(s-r);
then
A21: (t-r)/(s-r)=1-p by A17,XCMPLX_1:89;
t - r > 0 by A8,A17,A20,XREAL_1:129;
then
A22: r < t by XREAL_1:47;
(s-t)/(s-r)=p by A17,A18,XCMPLX_1:89;
hence thesis by A3,A5,A22,A19,A21;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis by A2;
end;
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
A23: 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 that
A24: a in X & b in X & c in X and
A25: a < b & b < c;
set p = (c-b)/(c-a);
A26: c-b < c-a & 0 < c-b by A25,XREAL_1:10,50;
then
A27: 0 < (c-b)/(c-a) & (c-b)/(c-a) < 1 by XREAL_1:139,189;
A28: p+(b-a)/(c-a) = ((c-b)+(b-a))/(c-a) by XCMPLX_1:62
.= 1 by A26,XCMPLX_1:60;
then p*a + (1-p)*c = (a*(c-b))/(c-a)+c*((b-a)/(c-a)) by XCMPLX_1:74
.= (a*(c-b))/(c-a)+(c*(b-a))/(c-a) by XCMPLX_1:74
.= ((c*a-b*a)+(b-a)*c)/(c-a) by XCMPLX_1:62
.= b*(c-a)/(c-a);
then p*a + (1-p)*c = b by A26,XCMPLX_1:89;
hence thesis by A23,A24,A25,A27,A28;
end;
hence thesis by A23;
end;
hence thesis by A1;
end;
theorem
f is_strictly_convex_on X & Y c= X implies f is_strictly_convex_on Y
by XBOOLE_1:1;
Lm1: f is_strictly_convex_on X implies f-r is_strictly_convex_on X
proof
assume
A1: f is_strictly_convex_on X;
then
A2: X c= dom f;
A3: for p being Real st 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 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 (f-r).(p*t + (1-p)*s) < p*(f-r).t + (1-p)*(f-r).s
proof
let t,s be Real;
assume that
A5: t in X & s in X and
A6: p*t + (1-p)*s in X and
A7: t <> s;
f.(p*t + (1-p)*s) < p*f.t + (1-p)*f.s by A1,A4,A5,A6,A7;
then
A8: f.(p*t + (1-p)*s)-r < p*f.t + (1-p)*f.s - r by XREAL_1:9;
(f-r).t = f.t-r & (f-r).s = f.s-r by A2,A5,VALUED_1:3;
hence thesis by A2,A6,A8,VALUED_1:3;
end;
hence thesis;
end;
dom f = dom (f-r) by VALUED_1:3;
hence thesis by A2,A3;
end;
theorem
f is_strictly_convex_on X iff f-r is_strictly_convex_on X
proof
A1: dom(f-r) = dom f by VALUED_1:3;
A2: 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 VALUED_1:3
.=(f-r).x+r
.=f.x-r+r by A1,A3,VALUED_1:3
.= f.x-(r-r);
hence thesis;
end;
dom((f-r)-(-r))=dom(f-r) by VALUED_1:3;
then (f-r)-(-r) = f by A1,A2,PARTFUN1:5;
hence thesis by Lm1;
end;
Lm2: 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;
then
A3: X c= dom(r(#)f) by VALUED_1:def 5;
for p being Real st 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 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 that
A5: t in X & s in X and
A6: p*t + (1-p)*s in X and
A7: t <> s;
f.(p*t + (1-p)*s) < p*f.t + (1-p)*f.s by A2,A4,A5,A6,A7;
then
A8: r*(f.(p*t + (1-p)*s)) < r*(p*f.t + (1-p)*f.s) by A1,XREAL_1:68;
p*(r(#)f).t=p*(r*f.t) & (1-p)*(r(#) f).s = (1-p)*(r*f.s) by A3,A5,
VALUED_1:def 5;
hence thesis by A3,A6,A8,VALUED_1:def 5;
end;
hence thesis;
end;
hence thesis by A3;
end;
theorem Th12:
0<r implies (f is_strictly_convex_on X iff r(#)f is_strictly_convex_on X)
proof
A1: dom((1/r)(#)(r(#)f))=dom(r(#)f) by VALUED_1:def 5;
assume
A2: 0<r;
A3: 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 A1,VALUED_1:def 5
.= (1/r)*(r*f.x) by A4,VALUED_1:def 5
.= (1/r)*r*f.x
.= 1*f.x by A2,XCMPLX_1:106;
hence thesis;
end;
dom(r(#)f) = dom f by VALUED_1:def 5;
then (1/r)(#)(r(#)f)=f by A1,A3,PARTFUN1:5;
hence thesis by A2,Lm2,XREAL_1:139;
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 X c= dom f & X c= dom g;
then X c= dom f /\ dom g by XBOOLE_1:19;
then
A2: X c= dom (f+g) by VALUED_1:def 1;
for p be Real st 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 p be Real;
assume
A3: 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 that
A4: r in X and
A5: s in X and
A6: p*r + (1-p)*s in X and
A7: r <> s;
A8: (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 ) by A2,A4,A6,VALUED_1:def 1;
A9: (p*f.r+(1-p)*f.s)+(p*g.r+(1-p)*g.s) = p*(f.r+g.r) + (1-p)*(f.s+g.s)
& (f+g). s = (f.s+g.s) by A2,A5,VALUED_1:def 1;
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,A4,A5,A6,A7;
hence thesis by A8,A9,XREAL_1:8;
end;
hence thesis;
end;
hence thesis by A2;
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 RFUNCT_3:def 12;
then X c= dom f /\ dom g by XBOOLE_1:19;
then
A2: X c= dom (f+g) by VALUED_1:def 1;
for p being Real st 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 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 that
A4: r in X and
A5: s in X and
A6: p*r + (1-p)*s in X and
A7: r <> s;
A8: (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 ) by A2,A4,A6,VALUED_1:def 1;
A9: (p*f.r+(1-p)*f.s)+(p*g.r+(1-p)*g.s) = p*(f.r+g.r) + (1-p)*(f.s+g.s)
& (f+g). s = (f.s+g.s) by A2,A5,VALUED_1:def 1;
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,A4,A5,A6,A7,RFUNCT_3:def 12;
hence thesis by A8,A9,XREAL_1:8;
end;
hence thesis;
end;
hence thesis by A2;
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 that
A1: f is_strictly_convex_on X and
A2: g is_strictly_convex_on X and
A3: a>0 & b>=0 or a>=0 & b>0;
now
per cases by A3;
suppose
a>0 & b>0;
then
a(#)f is_strictly_convex_on X & b(#)g is_strictly_convex_on X by A1,A2
,Th12;
hence thesis by Th13;
end;
suppose
A4: a>0 & b=0;
A5: X c= dom g by A2;
a(#)f is_strictly_convex_on X by A1,A4,Th12;
hence thesis by A4,A5,Th14,RFUNCT_3:57;
end;
suppose
A6: a=0 & b>0;
A7: X c= dom f by A1;
b(#)g is_strictly_convex_on X by A2,A6,Th12;
hence thesis by A6,A7,Th14,RFUNCT_3:57;
end;
end;
hence thesis;
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: 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 that
A2: X c= dom f and
A3: 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
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
A4: 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
A5: s in X & t in X & p*s+(1-p)*t in X;
now
per cases by A4,XXREAL_0:1;
suppose
p=0;
hence thesis;
end;
suppose
p=1;
hence thesis;
end;
suppose
A6: 0<p & p<1;
then
A7: 1-p > 0 by XREAL_1:50;
now
per cases by XXREAL_0:1;
suppose
s=t;
hence thesis;
end;
suppose
s<t;
then
A8: t-s > 0 by XREAL_1:50;
(p*s+(1-p)*t)-s =(1-p)*(t-s);
then
A9: (p*s+(1-p)*t)-s > 0 by A7,A8,XREAL_1:129;
then
A10: (p*s+(1-p)*t) > s by XREAL_1:47;
A11: (f.(p*s+(1-p)*t)-f.s)*(t-s)*p =p*((t-s)*f.(p*s+(1-p)*t))-
p*((t-s)*f.s) & (f. t-f.(p*s+(1-p)*t))*(t-s)*(1-p) =(1-p)*((t-s)*f.t)-(1-p)*((t
-s)*f.(p*s+(1-p)*t));
t-(p*s+(1-p)*t) =p*(t-s);
then
A12: t-(p*s+(1-p)*t) > 0 by A6,A8,XREAL_1:129;
then (p*s+(1-p)*t) < t by XREAL_1:47;
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 A3,A5,A10;
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 XXREAL_0:2;
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 A12,A9,XREAL_1:106;
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 A11,XREAL_1:21;
then f.(p*s+(1-p)*t) <=((1-p)*f.t*(t-s)+p*f.s*(t-s))/(t-s) by
A8,XREAL_1:77;
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:62;
then f.(p*s+(1-p)*t) <=(1-p)*f.t+(p*f.s*(t-s))/(t-s) by A8,
XCMPLX_1:89;
hence thesis by A8,XCMPLX_1:89;
end;
suppose
s>t;
then
A13: s-t > 0 by XREAL_1:50;
(p*s+(1-p)*t)-t =p*(s-t);
then
A14: (p*s+(1-p)*t)-t > 0 by A6,A13,XREAL_1:129;
then
A15: (p*s+(1-p)*t) > t by XREAL_1:47;
A16: (f.(p*s+(1-p)*t)-f.t)*(s-t)*(1-p) =(1-p)*((s-t)*f.(p*s+(1
-p)*t))-(1-p)*((s-t) *f.t) & (f.s-f.(p*s+(1-p)*t))*(s-t)*p =p*((s-t)*f.s)-p*((s
-t)*f.(p*s+(1-p)*t));
s-(p*s+(1-p)*t) =(1-p)*(s-t);
then
A17: s-(p*s+(1-p)*t) > 0 by A7,A13,XREAL_1:129;
then (p*s+(1-p)*t) < s by XREAL_1:47;
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 A3,A5,A15;
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 XXREAL_0:2;
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 A17,A14,XREAL_1:106;
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 A16,XREAL_1:21;
then f.(p*s+(1-p)*t) <=(p*f.s*(s-t)+(1-p)*f.t*(s-t))/(s-t) by
A13,XREAL_1:77;
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:62;
then f.(p*s+(1-p)*t) <=p*f.s+((1-p)*f.t*(s-t))/(s-t) by A13,
XCMPLX_1:89;
hence thesis by A13,XCMPLX_1:89;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis by A2,RFUNCT_3:def 12;
end;
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
A18: f is_convex_on X;
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 that
A19: a in X & b in X & r in X and
A20: a < r and
A21: r < b;
reconsider aa=a, bb=b as Real;
A22: b-r < b-a & 0 < b-r by A20,A21,XREAL_1:10,50;
reconsider p = (b-r)/(b-a) as Real;
A23: 0 < r-a by A20,XREAL_1:50;
A24: p+(r-a)/(b-a) = ((b-r)+(r-a))/(b-a) by XCMPLX_1:62
.= 1 by A22,XCMPLX_1:60;
then p*a + (1-p)*b = (a*(b-r))/(b-a)+b*((r-a)/(b-a)) by XCMPLX_1:74
.= (a*(b-r))/(b-a)+(b*(r-a))/(b-a) by XCMPLX_1:74
.= ((b*a-r*a)+(r-a)*b)/(b-a) by XCMPLX_1:62
.= r*(b-a)/(b-a);
then
A25: p*a + (1-p)*b = r by A22,XCMPLX_1:89;
A26: (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)
.= (b-r)*f.a + (b-a)*((r-a)/(b-a))*f.b by A22,XCMPLX_1:87
.= (b-r)*f.a + (r-a)*f.b by A22,XCMPLX_1:87;
(bb-r)/(bb-aa) < 1 by A22,XREAL_1:189;
then
A27: f.(p*a+(1-p)*b) <= p*f.a + (1-p)*f.b by A18,A19,A22,A25,RFUNCT_3:def 12;
then (b-a)*f.r <= (b-a)*f.a + ((r-a)*f.b - (r-a)*f.a) by A22,A24,A25,A26,
XREAL_1:64;
then (b-a)*f.r - (b-a)*f.a <= (r-a)*f.b - (r-a)*f.a by XREAL_1:20;
then (b-a)*(f.r-f.a) <= (r-a)*(f.b-f.a);
hence (f.r-f.a)/(r-a) <= (f.b-f.a)/(b-a) by A22,A23,XREAL_1:102;
(b-a)*f.r <= (b-a)*f.b - ((b-r)*f.b - (b-r)*f.a) by A22,A24,A25,A27,A26,
XREAL_1:64;
then ((b-r)*f.b-(b-r)*f.a)+(b-a)*f.r <= (b-a)*f.b by XREAL_1:19;
then (b-r)*f.b-(b-r)*f.a <= (b-a)*f.b-(b-a)*f.r by XREAL_1:19;
then (b-r)*(f.b-f.a) <= (b-a)*(f.b-f.r);
hence thesis by A22,XREAL_1:102;
end;
hence thesis by A18,RFUNCT_3:def 12;
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: 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 that
A2: X c= dom f and
A3: 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
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 that
A4: 0<p and
A5: p<1;
A6: 1-p > 0 by A5,XREAL_1:50;
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 that
A7: s in X & t in X & p*s+(1-p)*t in X and
A8: s <> t;
now
per cases by A8,XXREAL_0:1;
suppose
s<t;
then
A9: t-s > 0 by XREAL_1:50;
(p*s+(1-p)*t)-s =(1-p)*(t-s);
then
A10: (p*s+(1-p)*t)-s > 0 by A6,A9,XREAL_1:129;
then
A11: (p*s+(1-p)*t) > s by XREAL_1:47;
A12: (f.(p*s+(1-p)*t)-f.s)*(t-s)*p =p*((t-s)*f.(p*s+(1-p)*t))-p*((
t-s)*f.s) & (f. t-f.(p*s+(1-p)*t))*(t-s)*(1-p) =(1-p)*((t-s)*f.t)-(1-p)*((t-s)*
f.(p*s+(1-p)*t));
t-(p*s+(1-p)*t) =p*(t-s);
then
A13: t-(p*s+(1-p)*t) > 0 by A4,A9,XREAL_1:129;
then (p*s+(1-p)*t) < t by XREAL_1:47;
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 A3,A7,A11;
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 XXREAL_0:2;
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 A13,A10,XREAL_1:102;
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 A12,XREAL_1:21;
then f.(p*s+(1-p)*t) <((1-p)*f.t*(t-s)+p*f.s*(t-s))/(t-s) by A9,
XREAL_1:81;
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:62;
then f.(p*s+(1-p)*t) <(1-p)*f.t+(p*f.s*(t-s))/(t-s) by A9,
XCMPLX_1:89;
hence thesis by A9,XCMPLX_1:89;
end;
suppose
s>t;
then
A14: s-t > 0 by XREAL_1:50;
(p*s+(1-p)*t)-t =p*(s-t);
then
A15: (p*s+(1-p)*t)-t > 0 by A4,A14,XREAL_1:129;
then
A16: (p*s+(1-p)*t) > t by XREAL_1:47;
A17: (f.(p*s+(1-p)*t)-f.t)*(s-t)*(1-p) =(1-p)*((s-t)*f.(p*s+(1-p)*
t))-(1-p)*((s-t) *f.t) & (f.s-f.(p*s+(1-p)*t))*(s-t)*p =p*((s-t)*f.s)-p*((s-t)*
f.(p*s+(1-p)*t));
s-(p*s+(1-p)*t) =(1-p)*(s-t);
then
A18: s-(p*s+(1-p)*t) > 0 by A6,A14,XREAL_1:129;
then (p*s+(1-p)*t) < s by XREAL_1:47;
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 A3,A7,A16;
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 XXREAL_0:2;
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 A18,A15,XREAL_1:102;
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 A17,XREAL_1:21;
then f.(p*s+(1-p)*t) <(p*f.s*(s-t)+(1-p)*f.t*(s-t))/(s-t) by A14,
XREAL_1:81;
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:62;
then f.(p*s+(1-p)*t) <p*f.s+((1-p)*f.t*(s-t))/(s-t) by A14,
XCMPLX_1:89;
hence thesis by A14,XCMPLX_1:89;
end;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis by A2;
end;
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
A19: f is_strictly_convex_on X;
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 that
A20: a in X & b in X & r in X and
A21: a < r and
A22: r < b;
reconsider p = (b-r)/(b-a) as Real;
reconsider aa=a, bb=b as Real;
A23: b-r < b-a & 0 < b-r by A21,A22,XREAL_1:10,50;
A24: p+(r-a)/(b-a) = ((b-r)+(r-a))/(b-a) by XCMPLX_1:62
.= 1 by A23,XCMPLX_1:60;
then p*a + (1-p)*b = (a*(b-r))/(b-a)+b*((r-a)/(b-a)) by XCMPLX_1:74
.= (a*(b-r))/(b-a)+(b*(r-a))/(b-a) by XCMPLX_1:74
.= ((b*a-r*a)+(r-a)*b)/(b-a) by XCMPLX_1:62
.= r*(b-a)/(b-a);
then
A25: p*a + (1-p)*b = r by A23,XCMPLX_1:89;
0 < (b-r)/(b-a) & (bb-r)/(bb-aa) < 1 by A23,XREAL_1:139,189;
then
A26: f.r < p*f.a + (1-p)*f.b by A19,A20,A21,A22,A25;
A27: 0 < r-a by A21,XREAL_1:50;
A28: (p*f.a+(1-p)*f.b)*(b-a)= (b-a)*p*f.a+(b-a)*((1-p)*f.b)
.= ((b-a)*(b-r)/(b-a))*f.a + ((b-a)*((r-a)/(b-a))*f.b) by A24,
XCMPLX_1:74
.= ((b-r)*(b-a))/(b-a)*f.a + ((b-a)*(r-a)/(b-a))*f.b by XCMPLX_1:74
.= (b-r)*((b-a)/(b-a))*f.a + ((b-a)*(r-a)/(b-a))*f.b by XCMPLX_1:74
.= (b-r)*1*f.a + ((r-a)*(b-a))/(b-a)*f.b by A23,XCMPLX_1:60
.= (b-r)*f.a + (r-a)*((b-a)/(b-a))*f.b by XCMPLX_1:74
.= (b-r)*f.a + (r-a)*1*f.b by A23,XCMPLX_1:60;
then f.r*(b-a) < (b-a)*f.a +((r-a)*f.b-(r-a)*f.a) by A23,A26,XREAL_1:68;
then f.r*(b-a)-(b-a)*f.a < (r-a)*f.b-(r-a)*f.a by XREAL_1:19;
then (b-a)*(f.r-f.a) < (r-a)*(f.b-f.a);
hence (f.r-f.a)/(r-a) < (f.b-f.a)/(b-a) by A23,A27,XREAL_1:106;
f.r*(b-a) < (r-b)*f.b + (b-r)*f.a + (b-a)*f.b by A23,A26,A28,XREAL_1:68;
then f.r*(b-a)-((r-b)*f.b + (b-r)*f.a) < (b-a)*f.b by XREAL_1:19;
then f.r*(b-a)+(-((r-b)*f.b+(b-r)*f.a))<(b-a)*f.b;
then -(r-b)*f.b -(b-r)*f.a < (b-a)*f.b - (b-a)*f.r by XREAL_1:20;
then (b-r)*(f.b-f.a) < (b-a)*(f.b-f.r);
hence thesis by A23,XREAL_1:106;
end;
hence thesis by A19;
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
Element of NAT, P,E,F being Element of n-tuples_on REAL st Sum P=1 & (for i
being Element of 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
let f be PartFunc of REAL,REAL;
assume f is total;
then
A1: REAL c= dom f by PARTFUN1:def 2;
(for n being Element of NAT, P,E,F being Element of n-tuples_on REAL st
Sum P=1 & (for i being Element of 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
A2: for n being Element of NAT, P,E,F being Element of n-tuples_on
REAL st Sum P=1 & (for i being Element of 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
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
A3: 0<=p and
A4: p<=1;
let r,s be Real such that
r in REAL and
s in REAL and
p*r + (1-p)*s in REAL;
reconsider rr=r,ss=s,pp=p, mp=1-p as Element of REAL by XREAL_0:def 1;
f.rr in REAL & f.ss in REAL by XREAL_0:def 1;
then reconsider P=<*pp,mp*>, E=<*rr,ss*>, F=<*f.rr,f.ss*>
as Element of 2-tuples_on REAL
by FINSEQ_2:101;
A5: for i being Element of NAT st i in dom P holds P.i >=0 & F.i=f.(E.i )
proof
A6: dom P = Seg len P by FINSEQ_1:def 3
.= Seg 2 by CARD_1:def 7;
let i be Element of NAT such that
A7: i in dom P;
now
per cases by A7,A6,FINSEQ_1:2,TARSKI:def 2;
suppose
A8: i=1;
thus thesis by A3,A8;
end;
suppose
A9: i=2;
thus thesis by A4,A9,XREAL_1:48;
end;
end;
hence thesis;
end;
Sum P=p+(1-p) by RVSUM_1:77
.= 1;
then
A10: f.Sum(mlt(P,E))<=Sum(mlt(P,F)) by A2,A5;
len P = 2 by FINSEQ_1:44
.= len E by FINSEQ_1:44;
then len (multreal.:(P,E)) = len P by FINSEQ_2:72;
then
A12: len mlt(P,E) = 2 by FINSEQ_1:44;
A13: mlt(P,E).1 = P.1*E.1 & mlt(P,E).2 = P.2*E.2 by RVSUM_1:60;
mlt(P,E)=<*p*r,(1-p)*s*> by A12,A13,FINSEQ_1:44;
then
A14: Sum(mlt(P,E))=p*r+(1-p)*s by RVSUM_1:77;
A15: mlt(P,F).1 = P.1*F.1 & mlt(P,F).2 = P.2*F.2 by RVSUM_1:60;
len P = 2 by FINSEQ_1:44
.= len F by FINSEQ_1:44;
then len (multreal.:(P,F)) = len P by FINSEQ_2:72;
then
A16: len mlt(P,F) = 2 by FINSEQ_1:44;
mlt(P,F)=<*p*f.r,(1-p)*f.s*> by A16,A15,FINSEQ_1:44;
hence thesis by A10,A14,RVSUM_1:77;
end;
hence thesis by A1,RFUNCT_3:def 12;
end;
hence thesis;
end;
theorem
for f being PartFunc of REAL,REAL st f is_convex_on REAL
holds (for n being
Element of NAT, P,E,F being Element of n-tuples_on REAL st Sum P=1 & (for i
being Element of 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 f be PartFunc of REAL,REAL;
assume
A1: f is_convex_on REAL;
defpred S[Nat] means for P,E,F being Element of $1-tuples_on
REAL st Sum P=1 & (for i being Element of 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));
A2: for k being Nat st S[k] holds S[k+1]
proof
let k be Nat such that
A3: S[k];
let P,E,F be Element of (k+1)-tuples_on REAL such that
A4: Sum P=1 and
A5: for i being Element of NAT st i in dom P holds P.i>=0 & F.i=f.(E.i);
consider E1 being Element of k-tuples_on REAL,
e1 being Element of REAL such that
A6: E=E1^<*e1*> by FINSEQ_2:117;
consider F1 being Element of k-tuples_on REAL,
f1 being Element of REAL such that
A7: F=F1^<*f1*> by FINSEQ_2:117;
len F1 + 1 = k + 1 by CARD_1:def 7
.= len P by CARD_1:def 7;
then len F1 + 1 in Seg len P by FINSEQ_1:4;
then
A8: len F1 + 1 in dom P by FINSEQ_1:def 3;
A9: f1=F.(len F1 + 1) by A7,FINSEQ_1:42
.= f.(E.(len F1 + 1)) by A5,A8
.= f.(E.(k+1)) by CARD_1:def 7
.= f.(E.(len E1+1)) by CARD_1:def 7
.= f.e1 by A6,FINSEQ_1:42;
consider P1 being Element of k-tuples_on REAL,
p1 being Element of REAL such that
A10: P=P1^<*p1*> by FINSEQ_2:117;
reconsider SP = (Sum P1)" as Element of REAL by XREAL_0:def 1;
mlt(P,F) = mlt(P1,F1)^<*p1*f1*> by A10,A7,Th2;
then
A11: Sum(mlt(P,F)) = 1*Sum(mlt(P1,F1))+p1*f1 by RVSUM_1:74;
mlt(P,E) = mlt(P1,E1)^<*p1*e1*> by A10,A6,Th2;
then
A12: Sum(mlt(P,E)) = 1*Sum(mlt(P1,E1))+p1*e1 by RVSUM_1:74;
A13: for i being Nat st i in dom P1 holds P1.i>=0
proof
let i be Nat such that
A14: i in dom P1;
A15: i in Seg len P1 by A14,FINSEQ_1:def 3;
then
A16: 1 <= i by FINSEQ_1:1;
i <= len P1 by A15,FINSEQ_1:1;
then
A17: i <= k by CARD_1:def 7;
k <= k+1 by NAT_1:11;
then i <= k+1 by A17,XXREAL_0:2;
then i in Seg (k+1) by A16,FINSEQ_1:1;
then i in Seg len P by CARD_1:def 7;
then
A18: i in dom P by FINSEQ_1:def 3;
P1.i = P.i by A10,A14,FINSEQ_1:def 7;
hence thesis by A5,A18;
end;
then
A19: for i being Element of NAT st i in dom P1 holds P1.i>= 0;
now
per cases;
suppose
A20: Sum P1 = 0;
then for i being Element of NAT st i in dom P1 holds P1.i=0
by A19,Th3;
then
A21: P1 = k |-> (0 qua Real) by Th4;
then mlt(P1,E1)=k |-> 0 by Th5;
then
A22: Sum(mlt(P1,E1))=k*0 by RVSUM_1:80;
mlt(P1,F1)=k |-> 0 by A21,Th5;
then
A23: Sum(mlt(P1,F1))=k*0 by RVSUM_1:80;
Sum P = 0+p1 by A10,A20,RVSUM_1:74;
hence thesis by A4,A12,A11,A9,A22,A23;
end;
suppose
A24: Sum P1 <>0;
A25: 0 <= Sum P1 by A13,RVSUM_1:84;
A26: for i being Element of NAT st i in dom ((Sum P1)"*P1)
holds ((Sum P1)"*P1).i >= 0 & F1.i=f.(E1.i)
proof
let i be Element of NAT;
assume i in dom ((Sum P1)"*P1);
then
A27: i in Seg len ((Sum P1)"*P1) by FINSEQ_1:def 3;
then
A28: i in Seg k by CARD_1:def 7;
then
A29: i in Seg len P1 by CARD_1:def 7;
then i <= len P1 by FINSEQ_1:1;
then
A30: i <= k by CARD_1:def 7;
A31: 1 <= i by A27,FINSEQ_1:1;
k <= k+1 by NAT_1:11;
then i <= k+1 by A30,XXREAL_0:2;
then i in Seg (k+1) by A31,FINSEQ_1:1;
then i in Seg len P by CARD_1:def 7;
then
A32: i in dom P by FINSEQ_1:def 3;
i in dom P1 by A29,FINSEQ_1:def 3;
then
((Sum P1)"*P1).i = (Sum P1)"*P1.i & P1.i >=0 by A13,RVSUM_1:45;
hence ((Sum P1)"*P1).i >= 0 by A25;
i in Seg len E1 by A28,CARD_1:def 7;
then i in dom E1 by FINSEQ_1:def 3;
then
A33: E.i = E1.i by A6,FINSEQ_1:def 7;
i in Seg len F1 by A28,CARD_1:def 7;
then i in dom F1 by FINSEQ_1:def 3;
then F.i = F1.i by A7,FINSEQ_1:def 7;
hence thesis by A5,A32,A33;
end;
A34: Sum(mlt(P,E))=Sum P1*(Sum P1)"*Sum(mlt(P1,E1)) +p1*e1
by A12,A24,XCMPLX_0:def 7
.=Sum P1*((Sum P1)"*Sum(mlt(P1,E1)))+p1*e1
.=Sum P1*(Sum(SP*mlt(P1,E1)))+p1*e1 by RVSUM_1:87
.=Sum P1*Sum(mlt(SP*P1,E1))+p1*e1 by FINSEQOP:26;
A35: ( Sum P1)"*Sum(mlt(P1,F1))
= Sum(SP*mlt(P1,F1)) by RVSUM_1:87
.=Sum(mlt(SP*P1,F1)) by FINSEQOP:26;
len P1 + 1 = len P by A10,FINSEQ_2:16;
then len P1 + 1 in Seg len P by FINSEQ_1:4;
then
A36: len P1 + 1 in dom P by FINSEQ_1:def 3;
Sum P1+p1 = 1 by A4,A10,RVSUM_1:74;
then
A37: p1 = 1 - Sum P1;
Sum((Sum P1)"*P1) = (Sum P1)"*Sum P1 by RVSUM_1:87
.= 1 by A24,XCMPLX_0:def 7;
then Sum P1*f.Sum(mlt((Sum P1)"*P1,E1)) <= Sum P1*((Sum P1)"*
Sum(mlt(P1,F1))) by A3,A25,A35,A26,XREAL_1:64;
then
A38: Sum P1*f.Sum(mlt((Sum P1)"*P1,E1)) + p1*f.e1 <= Sum P1*((
Sum P1)"*Sum(mlt(P1,F1)))+p1*f.e1 by XREAL_1:6;
A39: Sum(mlt(SP*P1,E1)) in REAL by XREAL_0:def 1;
A40: (Sum P1)*Sum(mlt(SP*P1,E1)) + p1*e1 in REAL by XREAL_0:def 1;
P.(len P1+1) = p1 by A10,FINSEQ_1:42;
then Sum P1 <= 1 by A5,A37,A36,XREAL_1:49;
then f.Sum(mlt(P,E)) <= Sum P1*f.Sum(mlt((Sum P1)"* P1,E1)) +
p1*f.e1 by A1,A34,A37,A25,RFUNCT_3:def 12,A39,A40;
then f.Sum(mlt(P,E)) <= Sum P1*(Sum P1)"*Sum(mlt(P1,F1))+p1*f.
e1 by A38,XXREAL_0:2;
hence thesis by A11,A9,A24,XCMPLX_0:def 7;
end;
end;
hence thesis;
end;
A41: S[0] by RVSUM_1:79;
for k be Nat holds S[k] from NAT_1:sch 2(A41,A2);
hence thesis;
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 and
A2: f is_convex_on I;
consider x1,x2 being Real such that
A3: x1 in I and
A4: x2 in I and
A5: x1 < a and
A6: a < x2 by A1;
set M = max(|.(f.x1-f.a)/(x1-a).|,|.(f.x2-f.a)/(x2-a).|);
A7: a in I by A3,A4,A5,A6,XXREAL_2:80;
A8: 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
A9: x1 <= x and
A10: x <= x2 and
A11: x<>a;
A12: x in I by A3,A4,A9,A10,XXREAL_2:80;
(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 A11,XXREAL_0:1;
suppose
A13: x < a;
A14: now
per cases by A9,XXREAL_0:1;
suppose
x1=x;
hence (f.x1-f.a)/(x1-a) <= (f.x-f.a)/(x-a);
end;
suppose
A15: x1 < x;
A16: (f.a-f.x1)/(a-x1) = (-(f.a-f.x1))/(-(a-x1)) by XCMPLX_1:191
.=(f.x1-f.a)/(x1-a);
(f.a-f.x)/(a-x) = (-(f.a-f.x))/(-(a-x)) by XCMPLX_1:191
.=(f.x-f.a)/(x-a);
hence
(f.x1-f.a)/(x1-a)<=(f.x-f.a)/(x-a) by A2,A3,A7,A12,A13,A15,A16
,Th16;
end;
end;
(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 A2,A4,A6,A7,A12,A13,Th16;
then (f.a-f.x)/(a-x)<=(f.x2-f.a)/(x2-a) by XXREAL_0:2;
then (-(f.a-f.x))/(-(a-x)) <= (f.x2-f.a)/(x2-a) by XCMPLX_1:191;
hence thesis by A14;
end;
suppose
A17: x > a;
A18: (f.a-f.x1)/(a-x1) = (-(f.a-f.x1))/(-(a-x1)) by XCMPLX_1:191
.=(f.x1-f.a)/(x1-a);
(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 A2,A3,A5,A7,A12,A17,Th16;
hence (f.x1-f.a)/(x1-a) <= (f.x-f.a)/(x-a) by A18,XXREAL_0:2;
now
per cases by A10,XXREAL_0:1;
suppose
x=x2;
hence (f.x-f.a)/(x-a) <= (f.x2-f.a)/(x2-a);
end;
suppose
x<x2;
hence (f.x-f.a)/(x-a)<=(f.x2-f.a)/(x2-a) by A2,A4,A7,A12,A17,Th16
;
end;
end;
hence (f.x-f.a)/(x-a) <= (f.x2-f.a)/(x2-a);
end;
end;
hence thesis;
end;
hence thesis;
end;
A19: for x being Real st x1<=x & x<=x2 & x<>a holds |.f.x-f.a.|<=M*
|.x-a.|
proof
A20: -|.(f.x1-f.a)/(x1-a).| <= (f.x1-f.a)/(x1-a) by ABSVALUE:4;
A21: (f.x2-f.a)/(x2-a) <= |.(f.x2-f.a)/(x2-a).| by ABSVALUE:4;
let x be Real such that
A22: x1<=x & x<=x2 and
A23: x<>a;
reconsider x as Real;
(f.x-f.a)/(x-a) <= (f.x2-f.a)/(x2-a) by A8,A22,A23;
then
A24: (f.x-f.a)/(x-a) <= |.(f.x2-f.a)/(x2-a).| by A21,XXREAL_0:2;
x-a <> 0 by A23;
then
A25: |.x-a.| > 0 by COMPLEX1:47;
(f.x1-f.a)/(x1-a) <= (f.x-f.a)/(x-a) by A8,A22,A23;
then
A26: -|.(f.x1-f.a)/(x1-a).| <= (f.x-f.a)/(x-a) by A20,XXREAL_0:2;
now
per cases;
suppose
|.(f.x1-f.a)/(x1-a).| <= |.(f.x2-f.a)/(x2-a).|;
then -|.(f.x1-f.a)/(x1-a).| >= -|.(f.x2-f.a)/(x2-a).| by XREAL_1:24;
then -|.(f.x2-f.a)/(x2-a).| <= (f.x-f.a)/(x-a) by A26,XXREAL_0:2;
then |.(f.x-f.a)/(x-a).| <= |.(f.x2-f.a)/(x2-a).| by A24,ABSVALUE:5;
then
A27: |.(f.x-f.a).|/|.(x-a).| <= |.(f.x2-f.a)/(x2-a).| by COMPLEX1:67;
|.(f.x2-f.a)/(x2-a).| <= M by XXREAL_0:25;
then |.(f.x-f.a).|/|.(x-a).| <= M by A27,XXREAL_0:2;
hence thesis by A25,XREAL_1:81;
end;
suppose
|.(f.x1-f.a)/(x1-a).| >= |.(f.x2-f.a)/(x2-a).|;
then (f.x-f.a)/(x-a) <= |.(f.x1-f.a)/(x1-a).| by A24,XXREAL_0:2;
then |.(f.x-f.a)/(x-a).| <= |.(f.x1-f.a)/(x1-a).| by A26,ABSVALUE:5;
then
A28: |.(f.x-f.a).|/|.(x-a).| <= |.(f.x1-f.a)/(x1-a).| by COMPLEX1:67;
|.(f.x1-f.a)/(x1-a).| <= M by XXREAL_0:25;
then |.(f.x-f.a).|/|.(x-a).| <= M by A28,XXREAL_0:2;
hence thesis by A25,XREAL_1:81;
end;
end;
hence thesis;
end;
A29: max(|.(f.x1-f.a)/(x1-a).|,|.(f.x2-f.a)/(x2-a).|) >= min(|.(f.x1-f.a
)/(x1-a).|,|.(f.x2-f.a)/(x2-a).|) by Th1;
A30: |.(f.x1-f.a)/(x1-a).| >= 0 & |.(f.x2-f.a)/(x2-a).| >= 0 by COMPLEX1:46;
then
A31: min(|.(f.x1-f.a)/(x1-a).|,|.(f.x2-f.a)/(x2-a).|) >= 0 by XXREAL_0:20;
then
A32: M >= 0 by Th1;
for r being Real st 0<r ex s being Real st 0<s & for x
being Real st x in dom f & |.x-a.|<s holds |.f.x-f.a.|<r
proof
let r be Real such that
A33: 0<r;
reconsider r as Real;
ex s being Real st 0<s & for x being Real st x in dom f
& |.x-a.|<s holds |.f.x-f.a.|<r
proof
now
per cases by A30,A29,XXREAL_0:20;
suppose
A34: M>0;
set s = min(r/M,min(a-x1,x2-a));
A35: for x being Real st x in dom f & |.x-a.|<s holds |.f.
x-f.a.|<r
proof
A36: s<=min(a-x1,x2-a) by XXREAL_0:17;
let x be Real such that
x in dom f and
A37: |.x-a.|<s;
min(a-x1,x2-a)<=a-x1 by XXREAL_0:17;
then s <= a-x1 by A36,XXREAL_0:2;
then |.x-a.|<a-x1 by A37,XXREAL_0:2;
then -(a-x1) <= x-a by ABSVALUE:5;
then x1-a <= x-a;
then
A38: x1 <= x by XREAL_1:9;
min(a-x1,x2-a)<=x2-a by XXREAL_0:17;
then s <= x2-a by A36,XXREAL_0:2;
then |.x-a.|<x2-a by A37,XXREAL_0:2;
then x-a <=x2-a by ABSVALUE:5;
then
A39: x <= x2 by XREAL_1:9;
now
per cases;
suppose
x<>a;
then
A40: |.f.x-f.a.|<=M*|.x-a.| by A19,A38,A39;
now
per cases;
suppose
A41: M<>0;
A42: M*s <= M*(r/M) by A31,A29,XREAL_1:64,XXREAL_0:17;
M*|.x-a.| < M*s by A32,A37,A41,XREAL_1:68;
then M*|.x-a.| < M*(r/M) by A42,XXREAL_0:2;
then M*|.x-a.| < (r*M)/M by XCMPLX_1:74;
then M*|.x-a.| < r*(M/M) by XCMPLX_1:74;
then M*|.x-a.| < r*1 by A41,XCMPLX_1:60;
hence thesis by A40,XXREAL_0:2;
end;
suppose
M=0;
hence thesis by A33,A40;
end;
end;
hence thesis;
end;
suppose
x=a;
hence thesis by A33,ABSVALUE:2;
end;
end;
hence thesis;
end;
s>0
proof
A43: min(a-x1,x2-a) > 0
proof
now
per cases by XXREAL_0:15;
suppose
min(a-x1,x2-a)=a-x1;
hence thesis by A5,XREAL_1:50;
end;
suppose
min(a-x1,x2-a)=x2-a;
hence thesis by A6,XREAL_1:50;
end;
end;
hence thesis;
end;
now
per cases by XXREAL_0:15;
suppose
s = r/M;
hence thesis by A33,A34,XREAL_1:139;
end;
suppose
s = min(a-x1,x2-a);
hence thesis by A43;
end;
end;
hence thesis;
end;
hence thesis by A35;
end;
suppose
A44: M=0;
set s = min(a-x1,x2-a);
A45: for x being Real st x1<=x & x<=x2 & x<>a holds |.f.x- f.a.|=0
proof
let x be Real;
assume x1<=x & x<=x2 & x<>a;
then |.f.x-f.a.|<=M*|.x-a.| by A19;
hence thesis by A44,COMPLEX1:46;
end;
A46: for x being Real st x in dom f & |.x-a.|<s holds |.f
.x-f.a.|<r
proof
let x be Real such that
x in dom f and
A47: |.x-a.|<s;
s<=a-x1 by XXREAL_0:17;
then |.x-a.|<a-x1 by A47,XXREAL_0:2;
then -(a-x1) <= x-a by ABSVALUE:5;
then x1-a <= x-a;
then
A48: x1 <= x by XREAL_1:9;
s<=x2-a by XXREAL_0:17;
then |.x-a.|<x2-a by A47,XXREAL_0:2;
then x-a <=x2-a by ABSVALUE:5;
then
A49: x <= x2 by XREAL_1:9;
now
per cases;
suppose
x<>a;
hence thesis by A33,A45,A48,A49;
end;
suppose
x=a;
hence thesis by A33,ABSVALUE:2;
end;
end;
hence thesis;
end;
s > 0
proof
now
per cases by XXREAL_0:15;
suppose
s=a-x1;
hence thesis by A5,XREAL_1:50;
end;
suppose
s=x2-a;
hence thesis by A6,XREAL_1:50;
end;
end;
hence thesis;
end;
hence thesis by A46;
end;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis by FCONT_1:3;
end;
begin :: Definitions of several convexity and semicontinuity concepts
definition
let f, X;
pred f is_quasiconvex_on X means
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
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
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;
pred f is_upper_semicontinuous_in x0 means
x0 in dom f & for r st 0<r
ex s st 0<s & for x st x in dom f & |.x-x0.|<s holds f.x0-f.x<r;
end;
definition
let f,X;
pred f is_upper_semicontinuous_on X means
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;
pred f is_lower_semicontinuous_in x0 means
x0 in dom f & for r st 0<r
ex s st 0<s & for x st x in dom f & |.x-x0.|<s holds f.x-f.x0<r;
end;
definition
let f,X;
pred f is_lower_semicontinuous_on X means
X c= dom f & for x0 st x0 in X holds f|X is_lower_semicontinuous_in x0;
end;
theorem Th21:
for x0 be Real, f st x0 in dom 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, f such that
A1: x0 in dom f;
A2: f is_continuous_in x0 implies f is_upper_semicontinuous_in x0 & f
is_lower_semicontinuous_in x0
proof
assume
A3: f is_continuous_in x0;
A4: for r st 0<r ex s st 0<s & for x st x in dom f & |.x-x0.|<s holds f.
x0-f.x<r
proof
let r;
assume 0<r;
then consider s be Real such that
A5: 0<s and
A6: for x be Real st x in dom f & |.x-x0.|<s holds |.f.x-
f.x0 .|<r by A3,FCONT_1:3;
take s;
for x st x in dom f & |.x-x0.|<s holds f.x0-f.x<r
proof
let x;
assume x in dom f & |.x-x0.|<s;
then
A7: |.f.x-f.x0.|<r by A6;
f.x-f.x0>=-|.f.x-f.x0.| by ABSVALUE:4;
then -(f.x-f.x0)<=|.f.x-f.x0.| by XREAL_1:26;
hence thesis by A7,XXREAL_0:2;
end;
hence thesis by A5;
end;
for r st 0<r ex s st 0<s & for x st x in dom f & |.x-x0.|<s holds f.
x-f.x0<r
proof
let r;
assume 0<r;
then consider s be Real such that
A8: 0<s and
A9: for x be Real st x in dom f & |.x-x0.|<s holds |.f.x-
f.x0 .|<r by A3,FCONT_1:3;
take s;
for x st x in dom f & |.x-x0.|<s holds f.x-f.x0<r
proof
let x;
assume x in dom f & |.x-x0.|<s;
then
A10: |.f.x-f.x0.|<r by A9;
f.x-f.x0<=|.f.x-f.x0.| by ABSVALUE:4;
hence thesis by A10,XXREAL_0:2;
end;
hence thesis by A8;
end;
hence thesis by A1,A4;
end;
f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0
implies f is_continuous_in x0
proof
assume that
A11: f is_upper_semicontinuous_in x0 and
A12: f is_lower_semicontinuous_in x0;
for r be Real st 0<r ex s be Real st 0<s & for x be Real
st x in dom f & |.x-x0.|<s holds |.f.x-f.x0.|<r
proof
let r be Real such that
A13: 0<r;
consider s1 such that
A14: 0<s1 and
A15: for x st x in dom f & |.x-x0.|<s1 holds f.x-f.x0<r by A12,A13;
consider s2 such that
A16: 0<s2 and
A17: for x st x in dom f & |.x-x0.|<s2 holds f.x0-f.x<r by A11,A13;
set s = min(s1,s2);
A18: for x be Real st x in dom f & |.x-x0.|<s holds |.f.x-f.x0.|<r
proof
let x be Real such that
A19: x in dom f and
A20: |.x-x0.|<s;
s <= s2 by XXREAL_0:17;
then |.x-x0.|<s2 by A20,XXREAL_0:2;
then
A21: f.x0-f.x<r by A17,A19;
s <= s1 by XXREAL_0:17;
then |.x-x0.|<s1 by A20,XXREAL_0:2;
then
A22: f.x-f.x0<r by A15,A19;
A23: |.f.x-f.x0.|<>r
proof
assume
A24: |.f.x-f.x0.|=r;
now
per cases;
suppose
f.x-f.x0>=0;
hence contradiction by A22,A24,ABSVALUE:def 1;
end;
suppose
not f.x-f.x0>=0;
then |.f.x-f.x0.|=-(f.x-f.x0) by ABSVALUE:def 1;
hence contradiction by A21,A24;
end;
end;
hence thesis;
end;
-(f.x0-f.x)>-r by A21,XREAL_1:24;
then |.f.x-f.x0.|<=r by A22,ABSVALUE:5;
hence thesis by A23,XXREAL_0:1;
end;
take s;
s > 0
proof
now
per cases;
suppose
s1<=s2;
hence thesis by A14,XXREAL_0:def 9;
end;
suppose
not s1<=s2;
hence thesis by A16,XXREAL_0:def 9;
end;
end;
hence thesis;
end;
hence thesis by A18;
end;
hence thesis by FCONT_1:3;
end;
hence thesis by A2;
end;
theorem
for X, f st X c= dom f holds f is_upper_semicontinuous_on X & f
is_lower_semicontinuous_on X iff f|X is continuous
proof
let X, f such that
A1: X c= dom f;
A2: f|X is continuous implies f is_upper_semicontinuous_on X & f
is_lower_semicontinuous_on X
proof
assume
A3: f|X is continuous;
A4: for x0 st x0 in X holds f|X is_lower_semicontinuous_in x0
proof
let x0;
assume x0 in X;
then
A5: x0 in dom(f|X) by A1,RELAT_1:57;
then f|X is_continuous_in x0 by A3,FCONT_1:def 2;
hence thesis by A5,Th21;
end;
for x0 st x0 in X holds f|X is_upper_semicontinuous_in x0
proof
let x0;
assume x0 in X;
then
A6: x0 in dom(f|X) by A1,RELAT_1:57;
then f|X is_continuous_in x0 by A3,FCONT_1:def 2;
hence thesis by A6,Th21;
end;
hence thesis by A1,A4;
end;
f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X implies
f|X is continuous
proof
assume that
A7: f is_upper_semicontinuous_on X and
A8: f is_lower_semicontinuous_on X;
X c= dom f & for x0 be Real st x0 in dom(f|X) holds f|X
is_continuous_in x0
proof
thus X c= dom f by A7;
let x0 be Real such that
A9: x0 in dom(f|X);
x0 in X by A9,RELAT_1:57;
then f|X is_upper_semicontinuous_in x0 & f|X is_lower_semicontinuous_in
x0 by A7,A8;
hence thesis by Th21;
end;
hence thesis by FCONT_1:def 2;
end;
hence thesis by A2;
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: 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 that
A3: 0<p and
A4: 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;
1-p > 0 by A4,XREAL_1:50;
then
A5: (1-p)*f.s<=(1-p)*max(f.r,f.s) by XREAL_1:64,XXREAL_0:25;
assume 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 by A1,A3,A4;
p*f.r<=p*max(f.r,f.s) by A3,XREAL_1:64,XXREAL_0:25;
then p*f.r + (1-p)*f.s <= p*max(f.r,f.s)+(1-p)*max(f.r,f.s) by A5,
XREAL_1:7;
hence thesis by A6,XXREAL_0:2;
end;
hence thesis;
end;
X c= dom f by A1;
hence thesis by A2;
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: 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 thesis by A1,A3,A4;
end;
suppose
r=s;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis;
end;
X c= dom f by A1;
hence thesis by A2;
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: 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 and
A4: 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
A5: r in X & s in X & p*r + (1-p)*s in X and
A6: f.r <> f.s;
A7: f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s by A1,A3,A4,A5,RFUNCT_3:def 12;
A8: 1-p > 0 by A4,XREAL_1:50;
now
per cases by A6,XXREAL_0:1;
suppose
f.r < f.s;
then p*f.r < p*f.s by A3,XREAL_1:68;
then p*f.r + (1-p)*f.s < p*f.s + (1-p)*f.s by XREAL_1:6;
then
A9: f.(p*r + (1-p)*s) < f.s by A7,XXREAL_0:2;
f.s <= max(f.r,f.s) by XXREAL_0:25;
hence thesis by A9,XXREAL_0:2;
end;
suppose
f.r > f.s;
then (1-p)*f.r > (1-p)*f.s by A8,XREAL_1:68;
then p*f.r + (1-p)*f.s < p*f.r + (1-p)*f.r by XREAL_1:6;
then
A10: f.(p*r + (1-p)*s) < f.r by A7,XXREAL_0:2;
f.r <= max(f.r,f.s) by XXREAL_0:25;
hence thesis by A10,XXREAL_0:2;
end;
end;
hence thesis;
end;
hence thesis;
end;
X c= dom f by A1,RFUNCT_3:def 12;
hence thesis by A2;
end;
theorem
for X, f st f is_strongly_quasiconvex_on X holds f
is_strictly_quasiconvex_on X;
theorem
for X, f st f is_strictly_quasiconvex_on X & f is one-to-one holds f
is_strongly_quasiconvex_on X
by FUNCT_1:def 4;