rfunct_4.miz

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 :: RFUNCT_4:1



 Th1: for a,b be 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 :: RFUNCT_4:2



 Th2: for n be Nat, R1,R2 be Element of (n -tuples_on REAL ), r1,r2 be 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 be 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 :: RFUNCT_4:3



 Th3: for n be Nat, R be Element of (n -tuples_on REAL ) st ( Sum R) = 0 & (for i be Element of NAT st i in ( dom R) holds 0 <= (R . i)) holds for i be 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 be Element of NAT st i in ( dom R) holds 0 <= (R . i);



 A3: for i be Nat st i in ( dom R) holds 0 <= (R . i) by A2;

 given k be 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 :: RFUNCT_4:4



 Th4: for n be Nat, R be Element of (n -tuples_on REAL ) st (for i be 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 be 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 :: RFUNCT_4:5



 Th5: for n be Nat, R be 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

 definition

 let f, X;

 :: RFUNCT_4:def1

 pred f is_strictly_convex_on X means X c= ( dom f) & for p be Real st 0 s holds (f . ((p * r) + ((1 - p) * s))) < ((p * (f . r)) + ((1 - p) * (f . s)));

 end

 theorem :: RFUNCT_4:6

 f is_strictly_convex_on X implies f is_convex_on X

 proof

 assume

 A1: f is_strictly_convex_on X;



 A2: 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 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 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 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 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 :: RFUNCT_4:7

 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 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 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 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 :: RFUNCT_4:8

 for X be set, f be PartFunc of REAL , REAL holds f is_convex_on X iff X c= ( dom f) & for a,b,c be 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 be 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 be 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 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 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 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 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 be 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 be 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, XREAL_1: 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 :: RFUNCT_4:9

 for X be set, f be PartFunc of REAL , REAL holds f is_strictly_convex_on X iff X c= ( dom f) & for a,b,c be 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 be 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 be 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 be Real st 0 s holds (f . ((p * r) + ((1 - p) * s))) < ((p * (f . r)) + ((1 - p) * (f . s)))

 proof

 let p be Real;

 assume

 A4: 0 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 be 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 be 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, XREAL_1: 50;

 then

 A27: 0 < ((c - b) / (c - a)) & ((c - b) / (c - a)) < 1 by XREAL_1: 139, XREAL_1: 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 :: RFUNCT_4:10

 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 be Real st 0 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 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 :: RFUNCT_4:11

 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 be 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 be Real st 0 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 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 :: RFUNCT_4:12



 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 be 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 :: RFUNCT_4:13



 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 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 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 :: RFUNCT_4:14



 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 be Real st 0 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 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 :: RFUNCT_4:15

 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 :: RFUNCT_4:16



 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 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 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 be 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 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, XREAL_1: 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 :: RFUNCT_4:17

 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 be Real st 0 s holds (f . ((p * r) + ((1 - p) * s))) < ((p * (f . r)) + ((1 - p) * (f . s)))

 proof

 let p be Real;

 assume that

 A4: 0 0 by A5, XREAL_1: 50;

 for s,t be 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, XREAL_1: 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, XREAL_1: 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;

 theorem :: RFUNCT_4:18

 for f be PartFunc of REAL , REAL st f is total holds (for n be Element of NAT , P,E,F be Element of (n -tuples_on REAL ) st ( Sum P) = 1 & (for i be 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 be Element of NAT , P,E,F be Element of (n -tuples_on REAL ) st ( Sum P) = 1 & (for i be 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 be Element of NAT , P,E,F be Element of (n -tuples_on REAL ) st ( Sum P) = 1 & (for i be 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 be Real st 0 <= p & p <= 1 holds for r,s be 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 be 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;

 then (E . i) = r by FINSEQ_1: 44;

 hence thesis by A3, A8, FINSEQ_1: 44;

 end;

 suppose

 A9: i = 2;

 then (E . i) = s & (P . i) = (1 - p) by FINSEQ_1: 44;

 hence thesis by A4, A9, FINSEQ_1: 44, 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;



 A11: (P . 1) = p & (P . 2) = (1 - p) by FINSEQ_1: 44;

 ( 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;

 (E . 1) = r & (E . 2) = s by FINSEQ_1: 44;

 then ( mlt (P,E)) = <*(p * r), ((1 - p) * s)*> by A11, 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;

 (F . 1) = (f . r) & (F . 2) = (f . s) by FINSEQ_1: 44;

 then ( mlt (P,F)) = <*(p * (f . r)), ((1 - p) * (f . s))*> by A11, 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 :: RFUNCT_4:19

 for f be PartFunc of REAL , REAL st f is_convex_on REAL holds (for n be Element of NAT , P,E,F be Element of (n -tuples_on REAL ) st ( Sum P) = 1 & (for i be 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 be Element of ($1 -tuples_on REAL ) st ( Sum P) = 1 & (for i be 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 be 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 be Element of NAT st i in ( dom P) holds (P . i) >= 0 & (F . i) = (f . (E . i));

 consider E1 be Element of (k -tuples_on REAL ), e1 be Element of REAL such that

 A6: E = (E1 ^ <*e1*>) by FINSEQ_2: 117;

 consider F1 be Element of (k -tuples_on REAL ), f1 be 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 be Element of (k -tuples_on REAL ), p1 be 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 be 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 be Element of NAT st i in ( dom P1) holds (P1 . i) >= 0 ;

 now

 per cases ;

 suppose

 A20: ( Sum P1) = 0 ;

 then for i be 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 be 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 :: RFUNCT_4:20

 for f be PartFunc of REAL , REAL , I be Interval, a be Real st (ex x1,x2 be 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 be Real st x1 in I & x2 in I & x1 < a & a < x2 and

 A2: f is_convex_on I;

 consider x1,x2 be 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 be 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 be 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 be Real st 0 < r holds ex s be Real st 0 < s & for x be 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 be Real st 0 < s & for x be 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 be 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 be 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 be 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

 definition

 let f, X;

 :: RFUNCT_4:def2

 pred f is_quasiconvex_on X means 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 holds (f . ((p * r) + ((1 - p) * s))) <= ( max ((f . r),(f . s)));

 end

 definition

 let f, X;

 :: RFUNCT_4:def3

 pred f is_strictly_quasiconvex_on X means X c= ( dom f) & for p be Real st 0 (f . s) holds (f . ((p * r) + ((1 - p) * s))) < ( max ((f . r),(f . s)));

 end

 definition

 let f, X;

 :: RFUNCT_4:def4

 pred f is_strongly_quasiconvex_on X means X c= ( dom f) & for p be Real st 0 s holds (f . ((p * r) + ((1 - p) * s))) < ( max ((f . r),(f . s)));

 end

 definition

 let f;

 let x0 be Real;

 :: RFUNCT_4:def5

 pred f is_upper_semicontinuous_in x0 means x0 in ( dom f) & for r st 0 < r holds 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;

 :: RFUNCT_4:def6

 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;

 :: RFUNCT_4:def7

 pred f is_lower_semicontinuous_in x0 means x0 in ( dom f) & for r st 0 < r holds 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;

 :: RFUNCT_4:def8

 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 :: RFUNCT_4:21



 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 holds 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 holds 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 holds 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 :: RFUNCT_4:22

 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 :: RFUNCT_4:23

 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 be Real st 0 s holds (f . ((p * r) + ((1 - p) * s))) < ( max ((f . r),(f . s)))

 proof

 let p be Real;

 assume that

 A3: 0 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 :: RFUNCT_4:24

 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 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 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 be 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 :: RFUNCT_4:25

 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 be Real st 0 (f . s) holds (f . ((p * r) + ((1 - p) * s))) < ( max ((f . r),(f . s)))

 proof

 let p be Real such that

 A3: 0 (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 :: RFUNCT_4:26

 for X, f st f is_strongly_quasiconvex_on X holds f is_strictly_quasiconvex_on X;

 theorem :: RFUNCT_4:27

 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;