The Mizar article:

Introduction to Several Concepts of Convexity and Semicontinuity for Function from $\Bbb R$ to $\Bbb R$

by
Noboru Endou,
Katsumi Wasaki, and
Yasunari Shidama

Received March 23, 2000

Copyright (c) 2000 Association of Mizar Users

MML identifier: RFUNCT_4
[ MML identifier index ]


environ

 vocabulary PARTFUN1, ARYTM, SQUARE_1, FINSEQ_2, RVSUM_1, FINSEQ_1, VECTSP_1,
      RELAT_1, FUNCT_1, ARYTM_1, RLVECT_1, RFUNCT_3, RCOMP_1, ARYTM_3, SEQ_1,
      BOOLE, MEASURE5, FCONT_1, SUPINF_1, ABSVALUE, RFUNCT_4;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XCMPLX_0, XREAL_0, RELAT_1,
      FUNCT_1, FINSEQ_1, REAL_1, NAT_1, ABSVALUE, FINSEQ_2, SQUARE_1, PARTFUN1,
      FINSEQOP, VECTSP_1, SEQ_1, RVSUM_1, RCOMP_1, RFUNCT_3, SUPINF_1,
      MEASURE5, FCONT_1;
 constructors MONOID_1, REAL_1, NAT_1, FINSEQOP, RCOMP_1, TOPREAL1, FINSEQ_4,
      RFUNCT_3, MEASURE5, FCONT_1, MEMBERED;
 clusters RELSET_1, FINSEQ_2, XREAL_0, ARYTM_3, MEMBERED;
 requirements NUMERALS, SUBSET, REAL, BOOLE, ARITHM;
 theorems RCOMP_1, REAL_1, REAL_2, AXIOMS, SQUARE_1, RFUNCT_3, TARSKI,
      PARTFUN1, SEQ_1, FINSEQ_1, FINSEQ_2, RVSUM_1, NAT_1, MEASURE5, MEASURE6,
      FCONT_1, ABSVALUE, FUNCT_1, XREAL_0, XBOOLE_1, XCMPLX_0, XCMPLX_1;
 schemes NAT_1;

begin :: Some useful properties of n-tuples_on REAL

reserve a,b,r,s,x0,x for Real;
reserve f,g for PartFunc of REAL,REAL;
reserve X,Y for set;
reserve k for Nat;

theorem Th1:
for a, b being real number holds max(a,b) >= min(a,b)
proof
 let a, b be real number;
 per cases by SQUARE_1:38;
  suppose min(a,b)=a;
  hence thesis by SQUARE_1:46;
  suppose min(a,b)=b;
  hence thesis by SQUARE_1:46;
end;

theorem Th2:
for n being Nat, R1,R2 being Element of n-tuples_on REAL, r1,r2 being Real
holds mlt(R1^<*r1*>,R2^<*r2*>)=mlt(R1,R2)^<*r1*r2*>
proof
   let n be Nat;
   let R1,R2 be Element of n-tuples_on REAL;
   let r1,r2 be Real;
A1:mlt(R1^<*r1*>,R2^<*r2*>) is Element of (n+1)-tuples_on REAL
   proof
A2: len (R1^<*r1*>) = len R1 + 1 by FINSEQ_2:19 .= n+1 by FINSEQ_2:109
    .= len R2 + 1 by FINSEQ_2:109 .= len (R2^<*r2*>) by FINSEQ_2:19;
      len(mlt(R1^<*r1*>,R2^<*r2*>))
     =len(multreal.:(R1^<*r1*>,R2^<*r2*>)) by RVSUM_1:def 9
    .= len (R1^<*r1*>) by A2,FINSEQ_2:86
    .= len R1 + 1 by FINSEQ_2:19 .= n+1 by FINSEQ_2:109;
    hence thesis by FINSEQ_2:110;
   end;
A3:mlt(R1,R2)^<*r1*r2*> is Element of (n+1)-tuples_on REAL
   proof
A4: len R1 = n by FINSEQ_2:109 .= len R2 by FINSEQ_2:109;
  len(mlt(R1,R2))=len(multreal.:(R1,R2)) by RVSUM_1:def 9
    .= len R1 by A4,FINSEQ_2:86
    .= n by FINSEQ_2:109;
    then len(mlt(R1,R2)^<*r1*r2*>)= n+1 by FINSEQ_2:19;
    hence thesis by FINSEQ_2:110;
   end;
     for k being Nat st k in Seg (n+1) holds
   mlt(R1^<*r1*>,R2^<*r2*>).k = (mlt(R1,R2)^<*r1*r2*>).k
   proof
    let k be Nat such that
A5: k in Seg (n+1);
A6: 1<=k & k<=n+1 by A5,FINSEQ_1:3;
      now per cases by A6,REAL_1:def 5;
     suppose k<n+1;
     then 1<=k & k<=n by A5,FINSEQ_1:3,NAT_1:38;
then A7: k in Seg n by FINSEQ_1:3;
     then k in Seg len R1 & k in Seg len R2 by FINSEQ_2:109;
     then k in dom R1 & k in dom R2 by FINSEQ_1:def 3;
then A8:  (R1^<*r1*>).k = R1.k & (R2^<*r2*>).k = R2.k by FINSEQ_1:def 7;
       k in Seg len (mlt(R1^<*r1*>,R2^<*r2*>)) by A1,A5,FINSEQ_2:109;
     then k in dom(mlt(R1^<*r1*>,R2^<*r2*>)) by FINSEQ_1:def 3;
then A9:  mlt(R1^<*r1*>,R2^<*r2*>).k = (R1.k)*(R2.k) by A8,RVSUM_1:86;
       n+1 = len (mlt(R1,R2)) + 1 by FINSEQ_2:109;
     then len (mlt(R1,R2)) = n+1-1 by XCMPLX_1:26 .= n by XCMPLX_1:26;
then A10: k in dom mlt(R1,R2) by A7,FINSEQ_1:def 3;
     then (mlt(R1,R2)^<*r1*r2*>).k = mlt(R1,R2).k by FINSEQ_1:def 7;
     hence thesis by A9,A10,RVSUM_1:86;
     suppose A11:k=n+1;
     then k=len R1+1 & k=len R2+1 by FINSEQ_2:109;
then A12: (R1^<*r1*>).k=r1 & (R2^<*r2*>).k=r2 by FINSEQ_1:59;
       k in Seg len (mlt(R1^<*r1*>,R2^<*r2*>)) by A1,A5,FINSEQ_2:109;
     then k in dom(mlt(R1^<*r1*>,R2^<*r2*>)) by FINSEQ_1:def 3;
then A13: mlt(R1^<*r1*>,R2^<*r2*>).k = r1*r2 by A12,RVSUM_1:86;
       n+1 = len (mlt(R1,R2)) + 1 by FINSEQ_2:109;
     hence thesis by A11,A13,FINSEQ_1:59;
    end;
    hence thesis;
   end;
   hence thesis by A1,A3,FINSEQ_2:139;
end;

theorem Th3:
for n being Nat, R being Element of n-tuples_on REAL st Sum R=0 &
(for i being Nat st i in dom R holds 0 <= R.i) holds
for i being Nat st i in dom R holds R.i = 0
proof
   let n be Nat, R be Element of n-tuples_on REAL such that
A1:Sum R=0 & (for i being Nat st i in dom R holds 0 <= R.i);
   given k being Nat such that
A2:k in dom R & R.k <> 0;
     0 <= R.k by A1,A2;
   hence contradiction by A1,A2,RVSUM_1:115;
end;

theorem Th4:
for n being Nat, R being Element of n-tuples_on REAL st
(for i being Nat st i in dom R holds 0 = R.i) holds
R = n |-> (0 qua Real)
proof
   let n be Nat, R be Element of n-tuples_on REAL such that
A1:for i being Nat st i in dom R holds 0 = R.i;
A2:len R = n by FINSEQ_2:109 .= len (n |-> 0) by FINSEQ_2:69;
     for k st 1 <= k & k <= len R holds R.k = (n |-> 0).k
   proof
    let k such that
A3: 1 <= k & k <= len R;
A4: k in Seg len R by A3,FINSEQ_1:3;
    then k in dom R by FINSEQ_1:def 3;
then A5:    R.k = 0 by A1;
      k in Seg n by A4,FINSEQ_2:109;
    hence thesis by A5,FINSEQ_2:70;
   end;
   hence thesis by A2,FINSEQ_1:18;
end;

theorem Th5:
for n being Nat, R being Element of n-tuples_on REAL
holds mlt(n |-> (0 qua Real),R) = n |-> (0 qua Real)
proof
   let n be Nat, R be Element of n-tuples_on REAL;
A1:len (n |-> (0 qua Real)) = n by FINSEQ_2:69
   .= len R by FINSEQ_2:109;
A2:len(mlt(n |-> (0 qua Real),R))
    =len(multreal.:(n |-> (0 qua Real),R)) by RVSUM_1:def 9
   .=len (n |-> (0 qua Real)) by A1,FINSEQ_2:86
   .=n by FINSEQ_2:109;
A3:len (n |-> (0 qua Real)) = n by FINSEQ_2:69;

     for k st 1 <= k & k <= len mlt(n |-> (0 qua Real),R) holds
   mlt(n |-> (0 qua Real),R).k = (n |-> (0 qua Real)).k
   proof
    let k such that
A4: 1 <= k & k <= len mlt(n |-> (0 qua Real),R);
A5: k in Seg len mlt(n |-> (0 qua Real),R) by A4,FINSEQ_1:3;
      mlt(n |-> (0 qua Real),R).k = (n |-> (0 qua Real)).k*R.k by RVSUM_1:87
    .=0*R.k by A2,A5,FINSEQ_2:70;
    hence thesis by A2,A5,FINSEQ_2:70;
   end;
   hence thesis by A2,A3,FINSEQ_1:18;
end;

begin :: Convex and strictly convex functions

definition let f, X;
pred f is_strictly_convex_on X means :Def1:
X c= dom f &
for p being Real st 0<p & p<1 holds
 for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
  f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s;
end;

theorem Th6:
f is_strictly_convex_on X implies f is_convex_on X
proof
   assume A1:f is_strictly_convex_on X;
then A2:X c= dom f &
   for p being Real st 0<p & p<1 holds
   for r,s be Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
   f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s by Def1;

     for p being Real st 0<=p & p<=1 holds
   for r,s being Real st r in X & s in X & p*r + (1-p)*s in X holds
   f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s
   proof
    let p be Real;
    assume A3:0<=p & p<=1;
      for r,s being Real st r in X & s in X & p*r+(1-p)*s in X holds
    f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s
    proof
     let r,s be Real;
     assume A4:r in X & s in X & p*r+(1-p)*s in X;
        now per cases by A3,REAL_1:def 5;
       suppose p=0;
       hence f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s;
       suppose p=1;
       hence f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s;
       suppose A5:0<p & p<1;
          now per cases;
         suppose A6:r=s;
then A7:     f.(p*r+(1-p)*s) = f.(1*r-p*r+p*r) by XCMPLX_1:40
         .=f.(r-(p*r-p*r)) by XCMPLX_1:37
         .=f.r by XCMPLX_1:17;
           p*f.r + (1-p)*f.s = 1*f.r-p*f.r+p*f.r by A6,XCMPLX_1:40
         .=f.r-(p*f.r-p*f.r) by XCMPLX_1:37;
         hence f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s by A7,XCMPLX_1:17;
         suppose r<>s;
         hence thesis by A1,A4,A5,Def1;
        end;
       hence thesis;
      end;
     hence thesis;
    end;
    hence thesis;
   end;
   hence thesis by A2,RFUNCT_3:def 13;
end;

theorem
  for a,b be Real, f be PartFunc of REAL,REAL holds
f is_strictly_convex_on [.a,b.] iff
[.a,b.] c= dom f & for p be Real st 0<p & p<1 holds
for r,s be Real st r in [.a,b.] & s in [.a,b.] & r <> s holds
f.(p*r+(1-p)*s) < p*f.r + (1-p)*f.s
proof
  let a,b be Real, f be PartFunc of REAL,REAL;
  set ab = {r where r is Real: a<=r & r<=b};
  A1: [.a,b.]= ab by RCOMP_1:def 1;
  thus f is_strictly_convex_on [.a,b.] implies
   [.a,b.] c= dom f & for p be Real st 0<p & p<1 holds
   for x,y be Real st x in [.a,b.] & y in [.a,b.] & x <> y holds
       f.(p*x + (1-p)*y) < p*f.x + (1-p)*f.y
     proof
      assume A2: f is_strictly_convex_on [.a,b.];
      hence [.a,b.] c= dom f by Def1;
      let p be Real;
      assume A3: 0<p & p<1;
      then A4: 0<=1-p by SQUARE_1:12;
      let x,y be Real;
      assume A5: x in [.a,b.] & y in [.a,b.] & x <> y;
      then A6: (ex r1 be Real st r1=x & a<=r1 & r1<=b) &
      ex r2 be Real st r2=y & a<=r2 & r2<=b by A1;
      then A7: p*a<=p*x & p*x<=p*b by A3,AXIOMS:25;
      A8: (1-p)*a<=(1-p)*y & (1-p)*y<=(1-p)*b by A4,A6,AXIOMS:25;
        p*a+(1-p)*a=p*a+(1*a-p*a) by XCMPLX_1:40
       .=a by XCMPLX_1:27;
      then A9: a<=p*x+(1-p)*y by A7,A8,REAL_1:55;
        p*b+(1-p)*b=p*b+(1*b-p*b) by XCMPLX_1:40
       .=b by XCMPLX_1:27;
      then p*x+(1-p)*y<=b by A7,A8,REAL_1:55;
      then p*x+(1-p)*y in ab by A9;
      hence thesis by A1,A2,A3,A5,Def1;
    end;
  assume A10: [.a,b.] c= dom f & for p be Real st 0<p & p<1 holds
       for x,y be Real st x in [.a,b.] & y in [.a,b.] & x <> y holds
        f.(p*x + (1-p)*y) < p*f.x + (1-p)*f.y;
  hence [.a,b.] c= dom f;
  let p be Real;
  assume A11: 0<p & p<1;
  let x,y be Real;
  assume x in [.a,b.] & y in [.a,b.] & p*x + (1-p)*y in [.a,b.];
  hence thesis by A10,A11;
end;

theorem
  for X being set, f being PartFunc of REAL,REAL holds
f is_convex_on X iff
X c= dom f & for a,b,c being Real st a in X & b in X & c in X &
a<b & b<c holds f.b <=((c-b)/(c-a))*f.a + ((b-a)/(c-a))*f.c
proof
   let X be set, f be PartFunc of REAL,REAL;
A1:f is_convex_on X implies
   X c= dom f & for a,b,c being Real st a in X & b in X & c in X &
   a<b & b<c holds f.b <=((c-b)/(c-a))*f.a + ((b-a)/(c-a))*f.c
   proof
    assume A2:f is_convex_on X;

      for a,b,c being Real st a in X & b in X & c in X & a < b & b < c
    holds f.b <=((c-b)/(c-a))*f.a + ((b-a)/(c-a))*f.c
    proof
     let a,b,c be Real; assume A3:a in X & b in X & c in X & a < b & b < c;
then A4:  c-b < c-a & 0 < c-b by REAL_2:105,SQUARE_1:11;
     then 0 < c-a by AXIOMS:22;
then A5:  0 < (c-b)/(c-a) & (c-b)/(c-a) < 1 by A4,REAL_2:127,142;
     set p = (c-b)/(c-a);
       1-p = (b-a)/(c-a) & p*a + (1-p)*c = b
     proof
        p+(b-a)/(c-a) = ((c-b)+(b-a))/(c-a) by XCMPLX_1:63
      .= (c-a)/(c-a) by XCMPLX_1:39
      .= 1 by A4,XCMPLX_1:60;
      hence 1-p = (b-a)/(c-a) by XCMPLX_1:26;
      then p*a + (1-p)*c
      = (a*(c-b))/(c-a)+c*((b-a)/(c-a)) by XCMPLX_1:75
      .= (a*(c-b))/(c-a)+(c*(b-a))/(c-a) by XCMPLX_1:75
      .= ((c-b)*a + (b-a)*c)/(c-a) by XCMPLX_1:63
      .= ((c*a-b*a)+(b-a)*c)/(c-a) by XCMPLX_1:40
      .= ((c*a-b*a)+(b*c-a*c))/(c-a) by XCMPLX_1:40
      .= (b*c-b*a)/(c-a) by XCMPLX_1:39
      .= b*(c-a)/(c-a) by XCMPLX_1:40;
      hence thesis by A4,XCMPLX_1:90;
     end;
     hence thesis by A2,A3,A5,RFUNCT_3:def 13;
    end;
    hence thesis by A2,RFUNCT_3:def 13;
   end;

     (X c= dom f & for a,b,c being Real st a in X & b in X & c in X &
   a<b & b<c holds f.b <=((c-b)/(c-a))*f.a + ((b-a)/(c-a))*f.c) implies
   f is_convex_on X
   proof
    assume that
    A6:X c= dom f and A7:for a,b,c being Real st a in X & b in X & c in X &
    a<b & b<c holds f.b <=((c-b)/(c-a))*f.a + ((b-a)/(c-a))*f.c;
      for p being Real st 0<=p & p<=1 holds
    for r,s being Real st r in X & s in X & p*r + (1-p)*s in X holds
    f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s
    proof
     let p be Real;
     assume A8:0<=p & p<=1;
       for r,s being Real st r in X & s in X & p*r + (1-p)*s in X holds
     f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s
     proof
      let r,s be Real;

      assume A9: r in X & s in X & p*r + (1-p)*s in X;
        f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s
      proof
         now per cases by A8,REAL_1:def 5;
        suppose p=0;
        hence f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s;
        suppose p=1;
        hence f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s;
        suppose A10:0<p & p<1;
        then 1 < 1+p by REAL_1:69;
then A11:    0 < 1-p & 1-p < 1 by A10,REAL_1:84,SQUARE_1:11;
           now per cases by REAL_1:def 5;
          suppose A12:r=s;
then A13:       p*r+(1-p)*s = 1*r-p*r+p*r by XCMPLX_1:40 .= r-(p*r-p*r) by
XCMPLX_1:37
          .= r by XCMPLX_1:17;
            p*f.r + (1-p)*f.s = 1*f.r-p*f.r+p*f.r by A12,XCMPLX_1:40
          .= f.r-(p*f.r-p*f.r) by XCMPLX_1:37 .= f.r by XCMPLX_1:17;
          hence f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s by A13;
          suppose r>s;
then A14:       r-s > 0 by SQUARE_1:11;
          set t = p*r + (1-p)*s;
A15:       t - s = p*r + ((1-p)*s - s) by XCMPLX_1:29
          .=p*r + (1*s - p*s - s) by XCMPLX_1:40
          .=p*r + (-p*s + s - s) by XCMPLX_0:def 8
          .=p*r + (-p*s) by XCMPLX_1:26
          .=p*r - p*s by XCMPLX_0:def 8
          .=p*(r-s) by XCMPLX_1:40;
          then t - s > 0 by A10,A14,REAL_2:122;
then A16:       s < t by REAL_2:106;

A17:       r - t = 1*r - p*r - (1-p)*s by XCMPLX_1:36
          .= (1-p)*r - (1-p)*s by XCMPLX_1:40
          .= (1-p)*(r-s) by XCMPLX_1:40;
          then r - t > 0 by A11,A14,REAL_2:122;
then A18:       t < r by REAL_2:106;
            (r-t)/(r-s)=(1-p) & (t-s)/(r-s)=p by A14,A15,A17,XCMPLX_1:90
;
          hence f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s by A7,A9,A16,A18;
          suppose r<s;
then A19:       s-r > 0 by SQUARE_1:11;
          set t = p*r + (1-p)*s;
A20:       t - r = p*r - 1*r + (1-p)*s by XCMPLX_1:29
          .= (p-1)*r + (1-p)*s by XCMPLX_1:40
          .= -(1-p)*r + (1-p)*s by XCMPLX_1:186
          .= (1-p)*s - (1-p)*r by XCMPLX_0:def 8
          .= (1-p)*(s-r) by XCMPLX_1:40;
          then t - r > 0 by A11,A19,REAL_2:122;
then A21:       r < t by REAL_2:106;

A22:       s - t = 1*s - (1-p)*s - p*r by XCMPLX_1:36
          .= (1-(1-p))*s - p*r by XCMPLX_1:40
          .= (1-1+p)*s - p*r by XCMPLX_1:37
          .= p*(s-r) by XCMPLX_1:40;
          then s - t > 0 by A10,A19,REAL_2:122;
then A23:       t < s by REAL_2:106;
            (s-t)/(s-r)=p & (t-r)/(s-r)=1-p by A19,A20,A22,XCMPLX_1:90;
          hence thesis by A7,A9,A21,A23;
         end;
        hence thesis;
       end;
       hence thesis;
      end;
      hence thesis;
     end;
     hence thesis;
    end;
    hence thesis by A6,RFUNCT_3:def 13;
   end;
   hence thesis by A1;
end;

theorem
  for X being set, f being PartFunc of REAL,REAL holds
f is_strictly_convex_on X iff
X c= dom f & for a,b,c being Real st a in X & b in X & c in X &
a<b & b<c holds f.b < ((c-b)/(c-a))*f.a + ((b-a)/(c-a))*f.c
proof
   let X be set;
   let f be PartFunc of REAL,REAL;
A1:f is_strictly_convex_on X implies
   X c= dom f & for a,b,c being Real st a in X & b in X & c in X &
   a<b & b<c holds f.b < ((c-b)/(c-a))*f.a + ((b-a)/(c-a))*f.c
   proof
    assume A2:f is_strictly_convex_on X;

      for a,b,c being Real st a in X & b in X & c in X & a < b & b < c
    holds f.b <((c-b)/(c-a))*f.a + ((b-a)/(c-a))*f.c
    proof
     let a,b,c be Real; assume A3:a in X & b in X & c in X & a < b & b < c;
then A4:  c-b < c-a & 0 < c-b by REAL_2:105,SQUARE_1:11;
     then 0 < c-a by AXIOMS:22;
then A5:  0 < (c-b)/(c-a) & (c-b)/(c-a) < 1 by A4,REAL_2:127,142;
     set p = (c-b)/(c-a);
       1-p = (b-a)/(c-a) & p*a + (1-p)*c = b
     proof
        p+(b-a)/(c-a) = ((c-b)+(b-a))/(c-a) by XCMPLX_1:63
      .= (c-a)/(c-a) by XCMPLX_1:39
      .= 1 by A4,XCMPLX_1:60;
      hence 1-p = (b-a)/(c-a) by XCMPLX_1:26;
      then p*a + (1-p)*c
      = (a*(c-b))/(c-a)+c*((b-a)/(c-a)) by XCMPLX_1:75
      .= (a*(c-b))/(c-a)+(c*(b-a))/(c-a) by XCMPLX_1:75
      .= ((c-b)*a + (b-a)*c)/(c-a) by XCMPLX_1:63
      .= ((c*a-b*a)+(b-a)*c)/(c-a) by XCMPLX_1:40
      .= ((c*a-b*a)+(b*c-a*c))/(c-a) by XCMPLX_1:40
      .= (b*c-b*a)/(c-a) by XCMPLX_1:39
      .= b*(c-a)/(c-a) by XCMPLX_1:40;
      hence thesis by A4,XCMPLX_1:90;
     end;
     hence thesis by A2,A3,A5,Def1;
    end;
    hence thesis by A2,Def1;
   end;

     (X c= dom f & for a,b,c being Real st a in X & b in X & c in X &
   a<b & b<c holds f.b < ((c-b)/(c-a))*f.a + ((b-a)/(c-a))*f.c) implies
   f is_strictly_convex_on X
   proof
    assume that
    A6:X c= dom f and A7:for a,b,c being Real st a in X & b in X & c in X &
    a<b & b<c holds f.b < ((c-b)/(c-a))*f.a + ((b-a)/(c-a))*f.c;

      for p being Real st 0<p & p<1 holds
    for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
    f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s
    proof
     let p be Real; assume A8:0<p & p<1;
       for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & r <> s
holds
     f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s
     proof
      let r,s be Real;
      assume A9: r in X & s in X & p*r + (1-p)*s in X & r <> s;
        f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s
      proof
         now per cases by A8;
        suppose A10:0<p & p<1;
        then 1 < 1+p by REAL_1:69;
then A11:    0 < 1-p & 1-p < 1 by A10,REAL_1:84,SQUARE_1:11;
           now per cases by A9,REAL_1:def 5;
          suppose r>s;
then A12:       r-s > 0 by SQUARE_1:11;
          set t = p*r + (1-p)*s;
A13:       t - s = p*r + ((1-p)*s - s) by XCMPLX_1:29
          .=p*r + (1*s - p*s - s) by XCMPLX_1:40
          .=p*r + (-p*s + s - s) by XCMPLX_0:def 8
          .=p*r + (-p*s) by XCMPLX_1:26
          .=p*r - p*s by XCMPLX_0:def 8
          .=p*(r-s) by XCMPLX_1:40;
          then t - s > 0 by A10,A12,REAL_2:122;
then A14:       s < t by REAL_2:106;
A15:       r - t = 1*r - p*r - (1-p)*s by XCMPLX_1:36
          .= (1-p)*r - (1-p)*s by XCMPLX_1:40
          .= (1-p)*(r-s) by XCMPLX_1:40;
          then r - t > 0 by A11,A12,REAL_2:122;
then A16:       t < r by REAL_2:106;
            (r-t)/(r-s)=(1-p) & (t-s)/(r-s)=p by A12,A13,A15,XCMPLX_1:90
;
          hence f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s by A7,A9,A14,A16;
          suppose r<s;
then A17:       s-r > 0 by SQUARE_1:11;
          set t = p*r + (1-p)*s;
A18:       t - r = p*r - 1*r + (1-p)*s by XCMPLX_1:29
          .= (p-1)*r + (1-p)*s by XCMPLX_1:40
          .= -(1-p)*r + (1-p)*s by XCMPLX_1:186
          .= (1-p)*s - (1-p)*r by XCMPLX_0:def 8
          .= (1-p)*(s-r) by XCMPLX_1:40;
          then t - r > 0 by A11,A17,REAL_2:122;
then A19:       r < t by REAL_2:106;
A20:       s - t = 1*s - (1-p)*s - p*r by XCMPLX_1:36
          .= (1-(1-p))*s - p*r by XCMPLX_1:40
          .= (1-1+p)*s - p*r by XCMPLX_1:37
          .= p*(s-r) by XCMPLX_1:40;
          then s - t > 0 by A10,A17,REAL_2:122;
then A21:       t < s by REAL_2:106;
            (s-t)/(s-r)=p & (t-r)/(s-r)=1-p by A17,A18,A20,XCMPLX_1:90;
          hence thesis by A7,A9,A19,A21;
         end;
        hence thesis;
       end;
       hence thesis;
      end;
      hence thesis;
     end;
     hence thesis;
    end;
    hence thesis by A6,Def1;
   end;
   hence thesis by A1;
end;

theorem
  f is_strictly_convex_on X & Y c= X implies f is_strictly_convex_on Y
proof
   assume A1:f is_strictly_convex_on X & Y c= X;
   then X c= dom f &
   for p being Real st 0<p & p<1 holds
   for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
   f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s by Def1;
then A2:Y c= dom f by A1,XBOOLE_1:1;
     for p being Real st 0<p & p<1 holds
   for r,s being Real st r in Y & s in Y & p*r + (1-p)*s in Y & r <> s holds
   f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s by A1,Def1;
   hence thesis by A2,Def1;
end;

Lm1:
(1-a)*b+a*b = b & b-(1-a)*b=a*b & b-a*b=(1-a)*b
proof
     (1-a)*b+a*b = 1*b-a*b+a*b by XCMPLX_1:40 .= b-(a*b-a*b) by XCMPLX_1:37;
   hence (1-a)*b+a*b = b by XCMPLX_1:17;
   hence thesis by XCMPLX_1:26;
end;

Lm2:
f is_strictly_convex_on X implies f-r is_strictly_convex_on X
proof
   assume A1:f is_strictly_convex_on X;
   then X c= dom f &
   for p being Real st 0<p & p<1 holds
   for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
   f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s by Def1;
then A2:X c= dom(f-r) by RFUNCT_3:def 12;
     for p being Real st 0<p & p<1 holds
   for t,s being Real st t in X & s in X & p*t + (1-p)*s in X & t <> s holds
   (f-r).(p*t + (1-p)*s) < p*(f-r).t + (1-p)*(f-r).s
   proof
    let p be Real; assume A3:0<p & p<1;
      for t,s being Real st t in X & s in X & p*t + (1-p)*s in X & t <> s holds
    (f-r).(p*t + (1-p)*s) < p*(f-r).t + (1-p)*(f-r).s
    proof
     let t,s be Real; assume
     A4:t in X & s in X & p*t + (1-p)*s in X & t <> s;
     then f.(p*t + (1-p)*s) < p*f.t + (1-p)*f.s by A1,A3,Def1;
then A5:  f.(p*t + (1-p)*s)-r < p*f.t + (1-p)*f.s - r by REAL_1:54;
       (f-r).t = f.t-r & (f-r).s = f.s-r &
     (f-r).(p*t + (1-p)*s) = f.(p*t + (1-p)*s)-r by A2,A4,RFUNCT_3:def 12;
     then p*(f-r).t + (1-p)*(f-r).s = p*f.t-p*r + (1-p)*(f.s-r) by XCMPLX_1:40
     .=(1-p)*(f.s-r)-p*r+p*f.t by XCMPLX_1:30
     .=(1-p)*f.s-(1-p)*r-p*r+p*f.t by XCMPLX_1:40
     .=(1-p)*f.s-((1-p)*r+p*r)+p*f.t by XCMPLX_1:36
     .=(1-p)*f.s-r+p*f.t by Lm1
     .=p*f.t + (1-p)*f.s - r by XCMPLX_1:29;
     hence thesis by A2,A4,A5,RFUNCT_3:def 12;
    end;
    hence thesis;
   end;
   hence thesis by A2,Def1;
end;

theorem
  f is_strictly_convex_on X iff f-r is_strictly_convex_on X
proof
A1:dom((f-r)-(-r))=dom(f-r) by RFUNCT_3:def 12;
A2:dom(f-r) = dom f by RFUNCT_3:def 12;
     for x being Element of REAL st x in dom (f-r) holds
   ((f-r)-(-r)).x = f.x
   proof
    let x be Element of REAL;
    assume A3:x in dom (f-r);
    then ((f-r)-(-r)).x=(f-r).x-(-r) by A1,RFUNCT_3:def 12 .=(f-r).x+r by
XCMPLX_1:151
    .=f.x-r+r by A3,RFUNCT_3:def 12 .= f.x-(r-r) by XCMPLX_1:37;
    hence thesis by XCMPLX_1:17;
   end;
   then (f-r)-(-r) = f by A1,A2,PARTFUN1:34;
   hence thesis by Lm2;
end;

Lm3:
0<r implies (f is_strictly_convex_on X implies r(#)f is_strictly_convex_on X)
proof
   assume A1:0<r;
   assume A2:f is_strictly_convex_on X;
   then X c= dom f &
   for p being Real st 0<p & p<1 holds
   for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
   f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s by Def1;
then A3:X c= dom(r(#)f) by SEQ_1:def 6;
     for p being Real st 0<p & p<1 holds
   for t,s being Real st t in X & s in X & p*t + (1-p)*s in X & t <> s holds
   (r(#)f).(p*t + (1-p)*s) < p*(r(#)f).t + (1-p)*(r(#)f).s
   proof
    let p be Real; assume A4:0<p & p<1;
      for t,s being Real st t in X & s in X & p*t + (1-p)*s in X & t <> s holds
    (r(#)f).(p*t + (1-p)*s) < p*(r(#)f).t + (1-p)*(r(#)f).s
    proof
     let t,s be Real;
     assume A5:t in X & s in X & p*t + (1-p)*s in X & t <> s;
     then f.(p*t + (1-p)*s) < p*f.t + (1-p)*f.s by A2,A4,Def1;
     then r*(f.(p*t + (1-p)*s)) < r*(p*f.t + (1-p)*f.s) by A1,REAL_1:70;
     then r*(f.(p*t + (1-p)*s)) < p*f.t*r + (1-p)*f.s*r by XCMPLX_1:8;
then A6:  r*(f.(p*t + (1-p)*s)) < p*(r*f.t) + (1-p)*f.s*r by XCMPLX_1:4;
       (r(#)f).(p*t + (1-p)*s) = r*(f.(p*t + (1-p)*s)) &
     p*(r(#)f).t=p*(r*f.t) & (1-p)*(r(#)
f).s = (1-p)*(r*f.s) by A3,A5,SEQ_1:def 6;
     hence thesis by A6,XCMPLX_1:4;
    end;
    hence thesis;
   end;
   hence thesis by A3,Def1;
end;

theorem Th12:
0<r implies (f is_strictly_convex_on X iff r(#)f is_strictly_convex_on X)
proof
   assume A1:0<r;
then A2:0 < 1/r by REAL_2:127;
A3:dom((1/r)(#)(r(#)f))=dom(r(#)f) & dom(r(#)f) = dom f by SEQ_1:def 6;
     for x being Element of REAL st x in dom(r(#)f) holds
   ((1/r)(#)(r(#)f)).x = f.x
   proof
    let x be Element of REAL;
    assume A4:x in dom (r(#)f);
    then ((1/r)(#)(r(#)f)).x = (1/r)*(r(#)f).x by A3,SEQ_1:def 6
    .= (1/r)*(r*f.x) by A4,SEQ_1:def 6
    .= (1/r)*r*f.x by XCMPLX_1:4
    .= 1*f.x by A1,XCMPLX_1:107;
    hence thesis;
   end;
   then (1/r)(#)(r(#)f)=f by A3,PARTFUN1:34;
   hence thesis by A1,A2,Lm3;
end;

theorem Th13:
f is_strictly_convex_on X & g is_strictly_convex_on X implies
f+g is_strictly_convex_on X
proof
   assume A1:f is_strictly_convex_on X & g is_strictly_convex_on X;
then A2:X c= dom f &
   for p be Real st 0<p & p<1 holds
   for r,s be Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
   f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s by Def1;
     X c= dom g &
   for p be Real st 0<p & p<1 holds
   for r,s be Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
   g.(p*r + (1-p)*s) < p*g.r + (1-p)*g.s by A1,Def1;
   then X c= dom f /\ dom g by A2,XBOOLE_1:19;
then A3:X c= dom (f+g) by SEQ_1:def 3;
     for p be Real st 0<p & p<1 holds
   for r,s be Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
   (f+g).(p*r + (1-p)*s) < p*(f+g).r + (1-p)*(f+g).s
   proof
    let p be Real; assume A4:0<p & p<1;
      for r,s be Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
    (f+g).(p*r + (1-p)*s) < p*(f+g).r + (1-p)*(f+g).s
    proof
     let r,s be Real;
     assume A5:r in X & s in X & p*r + (1-p)*s in X & r <> s;
then A6:  f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s &
     g.(p*r + (1-p)*s) < p*g.r + (1-p)*g.s by A1,A4,Def1;
A7:  (p*f.r+(1-p)*f.s)+(p*g.r+(1-p)*g.s)
      = p*f.r+ ((p*g.r+(1-p)*g.s)+(1-p)*f.s) by XCMPLX_1:1
     .= p*f.r+ (p*g.r+ ((1-p)*g.s+(1-p)*f.s)) by XCMPLX_1:1
     .= p*f.r+p*g.r+ ((1-p)*g.s+(1-p)*f.s) by XCMPLX_1:1
     .= p*(f.r+g.r) + ((1-p)*g.s+(1-p)*f.s) by XCMPLX_1:8
     .= p*(f.r+g.r) + (1-p)*(f.s+g.s) by XCMPLX_1:8;
       (f+g).(p*r + (1-p)*s) = f.(p*r+(1-p)*s)+g.(p*r+(1-p)*s) &
     (f+g).r = (f.r+g.r) & (f+g).s = (f.s+g.s) by A3,A5,SEQ_1:def 3;
     hence thesis by A6,A7,REAL_1:67;
    end;
    hence thesis;
   end;
   hence thesis by A3,Def1;
end;

theorem Th14:
f is_strictly_convex_on X & g is_convex_on X implies
f+g is_strictly_convex_on X
proof
   assume A1:f is_strictly_convex_on X & g is_convex_on X;
   then X c= dom f & X c= dom g by Def1,RFUNCT_3:def 13;
   then X c= dom f /\ dom g by XBOOLE_1:19;
then A2:X c= dom (f+g) by SEQ_1:def 3;
     for p being Real st 0<p & p<1 holds
   for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
   (f+g).(p*r + (1-p)*s) < p*(f+g).r + (1-p)*(f+g).s
   proof
    let p be Real;
    assume A3:0<p & p<1;
      for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
    (f+g).(p*r + (1-p)*s) < p*(f+g).r + (1-p)*(f+g).s
    proof
     let r,s be Real;
     assume A4:r in X & s in X & p*r + (1-p)*s in X & r <> s;
then A5:  f.(p*r+(1-p)*s) < p*f.r+(1-p)*f.s &
     g.(p*r+(1-p)*s) <= p*g.r+(1-p)*g.s by A1,A3,Def1,RFUNCT_3:def 13;
A6:  (p*f.r+(1-p)*f.s)+(p*g.r+(1-p)*g.s)
      = p*f.r+ ((p*g.r+(1-p)*g.s)+(1-p)*f.s) by XCMPLX_1:1
     .= p*f.r+ (p*g.r+ ((1-p)*g.s+(1-p)*f.s)) by XCMPLX_1:1
     .= p*f.r+p*g.r+ ((1-p)*g.s+(1-p)*f.s) by XCMPLX_1:1
     .= p*(f.r+g.r) + ((1-p)*g.s+(1-p)*f.s) by XCMPLX_1:8
     .= p*(f.r+g.r) + (1-p)*(f.s+g.s) by XCMPLX_1:8;
       (f+g).(p*r + (1-p)*s) = f.(p*r+(1-p)*s)+g.(p*r+(1-p)*s) &
     (f+g).r = (f.r+g.r) & (f+g).s = (f.s+g.s) by A2,A4,SEQ_1:def 3;
     hence thesis by A5,A6,REAL_1:67;
    end;
    hence thesis;
   end;
   hence thesis by A2,Def1;
end;

theorem
  f is_strictly_convex_on X & g is_strictly_convex_on X &
((a>0 & b>=0) or (a>=0 & b>0)) implies a(#)f+b(#)g is_strictly_convex_on X
proof
   assume A1:f is_strictly_convex_on X & g is_strictly_convex_on X &
   ((a>0 & b>=0) or (a>=0 & b>0));
     now per cases by A1;
    suppose a>0 & b>0;
    then a(#)f is_strictly_convex_on X & b(#)g is_strictly_convex_on X by A1,
Th12;
    hence thesis by Th13;
    suppose A2:a>0 & b=0;
then A3: a(#)f is_strictly_convex_on X by A1,Th12;
      g is_convex_on X & X c= dom g by A1,Def1,Th6;
    then b(#)g is_convex_on X by A2,RFUNCT_3:60;
    hence thesis by A3,Th14;
    suppose A4:a=0 & b>0;
then A5: b(#)g is_strictly_convex_on X by A1,Th12;
      f is_convex_on X & X c= dom f by A1,Def1,Th6;
    then a(#)f is_convex_on X by A4,RFUNCT_3:60;
    hence thesis by A5,Th14;
   end;
   hence thesis;
end;

Lm4:
for a,b,r be real number holds r*(a/b)=r*a/b
proof
 let a,b,r be real number;
 thus r*(a/b)=r*(a*b") by XCMPLX_0:def 9
            .=r*a*b" by XCMPLX_1:4
            .=r*a/b by XCMPLX_0:def 9;
end;

theorem Th16:
f is_convex_on X iff
X c= dom f & (for a,b,r st a in X & b in X & r in X & a < r & r < b holds
(f.r-f.a)/(r-a) <= (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) <= (f.b-f.r)/(b-r))
proof
A1:f is_convex_on X implies
   X c= dom f & (for a,b,r st a in X & b in X & r in X & a < r & r < b holds
   (f.r-f.a)/(r-a) <= (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) <= (f.b-f.r)/(b-r))
   proof
    assume A2:f is_convex_on X;
      X c= dom f &
    (for a,b,r st a in X & b in X & r in X & a < r & r < b holds
    (f.r-f.a)/(r-a) <= (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) <= (f.b-f.r)/(b-r))
    proof
     thus X c= dom f by A2,RFUNCT_3:def 13;
       (for a,b,r st a in X & b in X & r in X & a < r & r < b holds
     (f.r-f.a)/(r-a) <= (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) <= (f.b-f.r)/(b-r))
     proof
      let a,b,r;
      assume A3:a in X & b in X & r in X & a < r & r < b;
then A4:   b-r < b-a & 0 < b-r & 0 < r-a by REAL_2:105,SQUARE_1:11;
then A5:   0 < b-a by AXIOMS:22;
then A6:   0 < (b-r)/(b-a) & (b-r)/(b-a) < 1 by A4,REAL_2:127,142;
      set p = (b-r)/(b-a);

A7:   1-p = (r-a)/(b-a) & p*a + (1-p)*b = r
      proof
         p+(r-a)/(b-a) = ((b-r)+(r-a))/(b-a) by XCMPLX_1:63
       .= (b-a)/(b-a) by XCMPLX_1:39
       .= 1 by A4,XCMPLX_1:60;
       hence 1-p = (r-a)/(b-a) by XCMPLX_1:26;
       then p*a + (1-p)*b
       = (a*(b-r))/(b-a)+b*((r-a)/(b-a)) by XCMPLX_1:75
       .= (a*(b-r))/(b-a)+(b*(r-a))/(b-a) by XCMPLX_1:75
       .= ((b-r)*a + (r-a)*b)/(b-a) by XCMPLX_1:63
       .= ((b*a-r*a)+(r-a)*b)/(b-a) by XCMPLX_1:40
       .= ((b*a-r*a)+(r*b-a*b))/(b-a) by XCMPLX_1:40
       .= (r*b-r*a)/(b-a) by XCMPLX_1:39
       .= r*(b-a)/(b-a) by XCMPLX_1:40;
       hence thesis by A4,XCMPLX_1:90;
      end;
      then f.(p*a+(1-p)*b) <= p*f.a + (1-p)*f.b by A2,A3,A6,RFUNCT_3:def 13;
then A8:   (b-a)*f.r<=(b-a)*((b-r)/(b-a)*f.a + (r-a)/(b-a)*f.b) by A5,A7,AXIOMS
:25;
A9:   (b-a)*((b-r)/(b-a)*f.a + (r-a)/(b-a)*f.b)
       = (b-a)*((b-r)/(b-a)*f.a) + (b-a)*((r-a)/(b-a)*f.b) by XCMPLX_1:8
      .= (b-a)*((b-r)/(b-a))*f.a + (b-a)*((r-a)/(b-a)*f.b) by XCMPLX_1:4
      .= (b-a)*((b-r)/(b-a))*f.a + (b-a)*((r-a)/(b-a))*f.b by XCMPLX_1:4
      .= (b-r)*f.a + (b-a)*((r-a)/(b-a))*f.b by A4,XCMPLX_1:88
      .= (b-r)*f.a + (r-a)*f.b by A4,XCMPLX_1:88;
      then (b-a)*f.r <= ((b-a)-(r-a))*f.a + (r-a)*f.b by A8,XCMPLX_1:22;
      then (b-a)*f.r <= (b-a)*f.a - (r-a)*f.a + (r-a)*f.b by XCMPLX_1:40;
      then (b-a)*f.r <= (b-a)*f.a - ((r-a)*f.a - (r-a)*f.b) by XCMPLX_1:37;
      then (b-a)*f.r <= (b-a)*f.a + ((r-a)*f.b - (r-a)*f.a) by XCMPLX_1:38;
      then (b-a)*f.r - (b-a)*f.a <= (r-a)*f.b - (r-a)*f.a by REAL_1:86;
      then (b-a)*(f.r-f.a) <= (r-a)*f.b - (r-a)*f.a by XCMPLX_1:40;
      then (b-a)*(f.r-f.a) <= (r-a)*(f.b-f.a) by XCMPLX_1:40;
      hence (f.r-f.a)/(r-a) <= (f.b-f.a)/(b-a) by A4,A5,REAL_2:187;
        (b-a)*f.r <= (b-r)*f.a + ((r-b)+(b-a))*f.b by A8,A9,XCMPLX_1:39;
      then (b-a)*f.r <= (b-r)*f.a + ((b-a)-(b-r))*f.b by XCMPLX_1:38;
      then (b-a)*f.r <= (b-a)*f.b-(b-r)*f.b+(b-r)*f.a by XCMPLX_1:40;
      then (b-a)*f.r <= (b-a)*f.b - ((b-r)*f.b - (b-r)*f.a) by XCMPLX_1:37;
      then ((b-r)*f.b-(b-r)*f.a)+(b-a)*f.r <= (b-a)*f.b by REAL_1:84;
      then (b-r)*f.b-(b-r)*f.a <= (b-a)*f.b-(b-a)*f.r by REAL_1:84;
      then (b-r)*(f.b-f.a) <= (b-a)*f.b-(b-a)*f.r by XCMPLX_1:40;
      then (b-r)*(f.b-f.a) <= (b-a)*(f.b-f.r) by XCMPLX_1:40;
      hence thesis by A4,A5,REAL_2:187;
     end;
     hence thesis;
    end;
    hence thesis;
   end;
     X c= dom f &
   (for a,b,r st a in X & b in X & r in X & a < r & r < b holds
   (f.r-f.a)/(r-a) <= (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) <= (f.b-f.r)/(b-r))
   implies f is_convex_on X
   proof
    assume A10:X c= dom f &
    (for a,b,r st a in X & b in X & r in X & a < r & r < b holds
    (f.r-f.a)/(r-a) <= (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) <= (f.b-f.r)/(b-r));

      for p being Real st 0<=p & p<=1 holds
    for r,s be Real st r in X & s in X & p*r + (1-p)*s in X holds
    f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s
    proof
     let p be Real; assume A11:0<=p & p<=1;
       for s,t being Real st s in X & t in X & p*s+(1-p)*t in X holds
     f.(p*s+(1-p)*t) <= p*f.s + (1-p)*f.t
     proof
      let s,t be Real; assume A12:s in X & t in X & p*s+(1-p)*t in X;

        now per cases by A11,REAL_1:def 5;
       suppose p=0;
       hence thesis;
       suppose p=1;
       hence thesis;
       suppose A13:0<p & p<1;
then A14:   1-p > 0 by SQUARE_1:11;
         now per cases by REAL_1:def 5;
        suppose A15:s=t;
        then p*s+(1-p)*t = s by Lm1;
        hence thesis by A15,Lm1;
        suppose s<t;
then A16:    t-s > 0 by SQUARE_1:11;
A17:    t-(p*s+(1-p)*t) = t-(1-p)*t - p*s by XCMPLX_1:36
        .=p*t-p*s by Lm1
        .=p*(t-s) by XCMPLX_1:40;
then A18:    t-(p*s+(1-p)*t) > 0 by A13,A16,REAL_2:122;
then A19:    (p*s+(1-p)*t) < t by REAL_2:106;
A20:    (p*s+(1-p)*t)-s = (1-p)*t+(p*s-s) by XCMPLX_1:29
        .=(1-p)*t-(s-p*s) by XCMPLX_1:38
        .=(1-p)*t-(1-p)*s by Lm1
        .=(1-p)*(t-s) by XCMPLX_1:40;
then A21:    (p*s+(1-p)*t)-s > 0 by A14,A16,REAL_2:122;
        then (p*s+(1-p)*t) > s by REAL_2:106;
        then (f.(p*s+(1-p)*t)-f.s)/((p*s+(1-p)*t)-s) <= (f.t-f.s)/(t-s) &
        (f.t-f.s)/(t-s)<=(f.t-f.(p*s+(1-p)*t))/(t-(p*s+(1-p)*t))
        by A10,A12,A19;
        then (f.(p*s+(1-p)*t)-f.s)/((p*s+(1-p)*t)-s)
        <= (f.t-f.(p*s+(1-p)*t))/(t-(p*s+(1-p)*t)) by AXIOMS:22;
        then (f.(p*s+(1-p)*t)-f.s)*(t-(p*s+(1-p)*t))
        <= (f.t-f.(p*s+(1-p)*t))*((p*s+(1-p)*t)-s) by A18,A21,REAL_2:185;
        then (f.(p*s+(1-p)*t)-f.s)*(t-s)*p
        <= (f.t-f.(p*s+(1-p)*t))*((1-p)*(t-s)) by A17,A20,XCMPLX_1:4;
then A22:    (f.(p*s+(1-p)*t)-f.s)*(t-s)*p
        <= (f.t-f.(p*s+(1-p)*t))*(t-s)*(1-p) by XCMPLX_1:4;
A23:    (f.(p*s+(1-p)*t)-f.s)*(t-s)*p
         =((t-s)*f.(p*s+(1-p)*t)-(t-s)*f.s)*p by XCMPLX_1:40
        .=p*((t-s)*f.(p*s+(1-p)*t))-p*((t-s)*f.s) by XCMPLX_1:40;
          (f.t-f.(p*s+(1-p)*t))*(t-s)*(1-p)
         =((t-s)*f.t-(t-s)*f.(p*s+(1-p)*t))*(1-p) by XCMPLX_1:40
        .=(1-p)*((t-s)*f.t)-(1-p)*((t-s)*f.(p*s+(1-p)*t)) by XCMPLX_1:40;
        then p*((t-s)*f.(p*s+(1-p)*t))+(1-p)*((t-s)*f.(p*s+(1-p)*t))
        <=(1-p)*((t-s)*f.t)+p*((t-s)*f.s) by A22,A23,REAL_2:169;
        then (t-s)*f.(p*s+(1-p)*t)
        <=(1-p)*((t-s)*f.t)+p*((t-s)*f.s) by Lm1;
        then (t-s)*f.(p*s+(1-p)*t)
        <=(1-p)*f.t*(t-s)+p*((t-s)*f.s) by XCMPLX_1:4;
        then (t-s)*f.(p*s+(1-p)*t)
        <=(1-p)*f.t*(t-s)+p*f.s*(t-s) by XCMPLX_1:4;
        then f.(p*s+(1-p)*t)
        <=((1-p)*f.t*(t-s)+p*f.s*(t-s))/(t-s) by A16,REAL_2:177;
        then f.(p*s+(1-p)*t)
        <=((1-p)*f.t*(t-s))/(t-s)+(p*f.s*(t-s))/(t-s) by XCMPLX_1:63;
        then f.(p*s+(1-p)*t)
        <=(1-p)*f.t+(p*f.s*(t-s))/(t-s) by A16,XCMPLX_1:90;
        hence thesis by A16,XCMPLX_1:90;
        suppose s>t;

then A24:    s-t > 0 by SQUARE_1:11;
A25:    s-(p*s+(1-p)*t) = s-p*s - (1-p)*t by XCMPLX_1:36
        .=(1-p)*s-(1-p)*t by Lm1
        .=(1-p)*(s-t) by XCMPLX_1:40;
then A26:    s-(p*s+(1-p)*t) > 0 by A14,A24,REAL_2:122;
then A27:    (p*s+(1-p)*t) < s by REAL_2:106;
A28:    (p*s+(1-p)*t)-t = p*s+((1-p)*t-t) by XCMPLX_1:29
        .=p*s-(t-(1-p)*t) by XCMPLX_1:38
        .=p*s-p*t by Lm1
        .=p*(s-t) by XCMPLX_1:40;
then A29:    (p*s+(1-p)*t)-t > 0 by A13,A24,REAL_2:122;
        then (p*s+(1-p)*t) > t by REAL_2:106;
        then (f.(p*s+(1-p)*t)-f.t)/((p*s+(1-p)*t)-t) <= (f.s-f.t)/(s-t) &
        (f.s-f.t)/(s-t)<=(f.s-f.(p*s+(1-p)*t))/(s-(p*s+(1-p)*t))
        by A10,A12,A27;
        then (f.(p*s+(1-p)*t)-f.t)/((p*s+(1-p)*t)-t)
        <= (f.s-f.(p*s+(1-p)*t))/(s-(p*s+(1-p)*t)) by AXIOMS:22;
        then (f.(p*s+(1-p)*t)-f.t)*(s-(p*s+(1-p)*t))
        <= (f.s-f.(p*s+(1-p)*t))*((p*s+(1-p)*t)-t) by A26,A29,REAL_2:185;
        then (f.(p*s+(1-p)*t)-f.t)*(s-t)*(1-p)
        <= (f.s-f.(p*s+(1-p)*t))*(p*(s-t)) by A25,A28,XCMPLX_1:4;
then A30:    (f.(p*s+(1-p)*t)-f.t)*(s-t)*(1-p)
        <= (f.s-f.(p*s+(1-p)*t))*(s-t)*p by XCMPLX_1:4;
A31:    (f.(p*s+(1-p)*t)-f.t)*(s-t)*(1-p)
         =((s-t)*f.(p*s+(1-p)*t)-(s-t)*f.t)*(1-p) by XCMPLX_1:40
        .=(1-p)*((s-t)*f.(p*s+(1-p)*t))-(1-p)*((s-t)*f.t) by XCMPLX_1:40;
          (f.s-f.(p*s+(1-p)*t))*(s-t)*p
         =((s-t)*f.s-(s-t)*f.(p*s+(1-p)*t))*p by XCMPLX_1:40
        .=p*((s-t)*f.s)-p*((s-t)*f.(p*s+(1-p)*t)) by XCMPLX_1:40;
        then (1-p)*((s-t)*f.(p*s+(1-p)*t))+p*((s-t)*f.(p*s+(1-p)*t))
        <=p*((s-t)*f.s)+(1-p)*((s-t)*f.t) by A30,A31,REAL_2:169;
        then (s-t)*f.(p*s+(1-p)*t)
        <=p*((s-t)*f.s)+(1-p)*((s-t)*f.t) by Lm1;
        then (s-t)*f.(p*s+(1-p)*t)
        <=p*f.s*(s-t)+(1-p)*((s-t)*f.t) by XCMPLX_1:4;
        then (s-t)*f.(p*s+(1-p)*t)
        <=p*f.s*(s-t)+(1-p)*f.t*(s-t) by XCMPLX_1:4;
        then f.(p*s+(1-p)*t)
        <=(p*f.s*(s-t)+(1-p)*f.t*(s-t))/(s-t) by A24,REAL_2:177;
        then f.(p*s+(1-p)*t)
        <=(p*f.s*(s-t))/(s-t)+((1-p)*f.t*(s-t))/(s-t) by XCMPLX_1:63;
        then f.(p*s+(1-p)*t)
        <=p*f.s+((1-p)*f.t*(s-t))/(s-t) by A24,XCMPLX_1:90;
        hence thesis by A24,XCMPLX_1:90;
       end;
       hence thesis;
      end;
      hence thesis;
     end;
     hence thesis;
    end;
    hence thesis by A10,RFUNCT_3:def 13;
   end;
   hence thesis by A1;
end;

theorem
  f is_strictly_convex_on X iff
X c= dom f & (for a,b,r st a in X & b in X & r in X & a < r & r < b holds
(f.r-f.a)/(r-a) < (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) < (f.b-f.r)/(b-r))
proof
A1:f is_strictly_convex_on X implies
   X c= dom f & (for a,b,r st a in X & b in X & r in X & a < r & r < b holds
   (f.r-f.a)/(r-a) < (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) < (f.b-f.r)/(b-r))
   proof
    assume A2:f is_strictly_convex_on X;
      X c= dom f & (for a,b,r st a in X & b in X & r in X & a < r & r < b holds
    (f.r-f.a)/(r-a) < (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) < (f.b-f.r)/(b-r))
    proof
       (for a,b,r st a in X & b in X & r in X & a < r & r < b holds
     (f.r-f.a)/(r-a) < (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) < (f.b-f.r)/(b-r))
     proof
      let a,b,r;
      assume A3:a in X & b in X & r in X & a < r & r < b;
then A4:   b-r < b-a & 0 < b-r & 0 < r-a by REAL_2:105,SQUARE_1:11;
then A5:   0 < b-a by AXIOMS:22;
then A6:   0 < (b-r)/(b-a) & (b-r)/(b-a) < 1 by A4,REAL_2:127,142;
      set p = (b-r)/(b-a);
A7:   1-p = (r-a)/(b-a) & p*a + (1-p)*b = r
      proof
         p+(r-a)/(b-a) = ((b-r)+(r-a))/(b-a) by XCMPLX_1:63
       .= (b-a)/(b-a) by XCMPLX_1:39
       .= 1 by A4,XCMPLX_1:60;
       hence 1-p = (r-a)/(b-a) by XCMPLX_1:26;
       then p*a + (1-p)*b
       = (a*(b-r))/(b-a)+b*((r-a)/(b-a)) by XCMPLX_1:75
       .= (a*(b-r))/(b-a)+(b*(r-a))/(b-a) by XCMPLX_1:75
       .= ((b-r)*a + (r-a)*b)/(b-a) by XCMPLX_1:63
       .= ((b*a-r*a)+(r-a)*b)/(b-a) by XCMPLX_1:40
       .= ((b*a-r*a)+(r*b-a*b))/(b-a) by XCMPLX_1:40
       .= (r*b-r*a)/(b-a) by XCMPLX_1:39
       .= r*(b-a)/(b-a) by XCMPLX_1:40;
       hence thesis by A4,XCMPLX_1:90;
      end;
      then f.r < p*f.a + (1-p)*f.b by A2,A3,A6,Def1;
then A8:   f.r*(b-a) < (p*f.a + (1-p)*f.b)*(b-a) by A5,REAL_1:70;
A9:  (p*f.a+(1-p)*f.b)*(b-a)=(b-a)*(p*f.a)+(b-a)*((1-p)*f.b) by XCMPLX_1:8
      .= (b-a)*p*f.a+(b-a)*((1-p)*f.b) by XCMPLX_1:4
      .= (b-a)*p*f.a+(b-a)*(1-p)*f.b by XCMPLX_1:4
      .= ((b-a)*(b-r)/(b-a))*f.a + ((b-a)*((r-a)/(b-a))*f.b) by A7,Lm4
      .= ((b-r)*(b-a))/(b-a)*f.a + ((b-a)*(r-a)/(b-a))*f.b by Lm4
      .= (b-r)*((b-a)/(b-a))*f.a + ((b-a)*(r-a)/(b-a))*f.b by Lm4
      .= (b-r)*1*f.a + ((r-a)*(b-a))/(b-a)*f.b by A4,XCMPLX_1:60
      .= (b-r)*f.a + (r-a)*((b-a)/(b-a))*f.b by Lm4
      .= (b-r)*f.a + (r-a)*1*f.b by A4,XCMPLX_1:60;
      then f.r*(b-a) < ((b-a)-(r-a))*f.a + (r-a)*f.b by A8,XCMPLX_1:22;
      then f.r*(b-a) < (b-a)*f.a - (r-a)*f.a + (r-a)*f.b by XCMPLX_1:40;
      then f.r*(b-a) < (b-a)*f.a +(r-a)*f.b-(r-a)*f.a by XCMPLX_1:29;
      then f.r*(b-a) < (b-a)*f.a +((r-a)*f.b-(r-a)*f.a) by XCMPLX_1:29;
      then f.r*(b-a)-(b-a)*f.a < (r-a)*f.b-(r-a)*f.a by REAL_1:84;
      then (b-a)*(f.r-f.a) < (r-a)*f.b-(r-a)*f.a by XCMPLX_1:40;
      then (b-a)*(f.r-f.a) < (r-a)*(f.b-f.a) by XCMPLX_1:40;
      hence (f.r-f.a)/(r-a) < (f.b-f.a)/(b-a) by A4,A5,REAL_2:185;
        f.r*(b-a) < (b-r)*f.a + ((r-b)+(b-a))*f.b by A8,A9,XCMPLX_1:39;
      then f.r*(b-a) < (b-r)*f.a + ((r-b)*f.b + (b-a)*f.b) by XCMPLX_1:8;
      then f.r*(b-a) < (r-b)*f.b + (b-r)*f.a + (b-a)*f.b by XCMPLX_1:1;
      then f.r*(b-a)-((r-b)*f.b + (b-r)*f.a) < (b-a)*f.b by REAL_1:84;
      then f.r*(b-a)+(-((r-b)*f.b+(b-r)*f.a))<(b-a)*f.b by XCMPLX_0:def 8;
      then -((r-b)*f.b + (b-r)*f.a) < (b-a)*f.b - (b-a)*f.r by REAL_1:86;
      then -(r-b)*f.b -(b-r)*f.a < (b-a)*f.b - (b-a)*f.r by XCMPLX_1:161;
      then (-(r-b))*f.b -(b-r)*f.a < (b-a)*f.b - (b-a)*f.r by XCMPLX_1:175;
      then (b-r)*f.b - (b-r)*f.a < (b-a)*f.b - (b-a)*f.r by XCMPLX_1:143;
      then (b-r)*(f.b-f.a) < (b-a)*f.b - (b-a)*f.r by XCMPLX_1:40;
      then (b-r)*(f.b-f.a) < (b-a)*(f.b-f.r) by XCMPLX_1:40;
      hence thesis by A4,A5,REAL_2:185;
     end;
     hence thesis by A2,Def1;
    end;
    hence thesis;
   end;

     X c= dom f & (for a,b,r st a in X & b in X & r in X & a < r & r < b holds
   (f.r-f.a)/(r-a) < (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) < (f.b-f.r)/(b-r))
   implies f is_strictly_convex_on X
   proof
    assume A10:X c= dom f &
    (for a,b,r st a in X & b in X & r in X & a<r & r<b holds
    (f.r-f.a)/(r-a) < (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) < (f.b-f.r)/(b-r));
      f is_strictly_convex_on X
    proof
       for p being Real st 0<p & p<1 holds
     for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
     f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s
     proof
      let p be Real;
      assume A11:0<p & p<1;
then A12:  1-p > 0 by SQUARE_1:11;
        for s,t being Real st s in X & t in X & p*s+(1-p)*t in X & s <> t holds
      f.(p*s + (1-p)*t) < p*f.s + (1-p)*f.t
      proof
       let s,t be Real;
       assume A13:s in X & t in X & p*s+(1-p)*t in X & s <> t;

         now per cases by A13,REAL_1:def 5;
        suppose s<t;
then A14:    t-s > 0 by SQUARE_1:11;
A15:    t-(p*s+(1-p)*t) = t-(1-p)*t - p*s by XCMPLX_1:36
        .=p*t-p*s by Lm1
        .=p*(t-s) by XCMPLX_1:40;
then A16:    t-(p*s+(1-p)*t) > 0 by A11,A14,REAL_2:122;
then A17:    (p*s+(1-p)*t) < t by REAL_2:106;
A18:    (p*s+(1-p)*t)-s = (1-p)*t+(p*s-s) by XCMPLX_1:29
        .=(1-p)*t-(s-p*s) by XCMPLX_1:38
        .=(1-p)*t-(1-p)*s by Lm1
        .=(1-p)*(t-s) by XCMPLX_1:40;
then A19:    (p*s+(1-p)*t)-s > 0 by A12,A14,REAL_2:122;
        then (p*s+(1-p)*t) > s by REAL_2:106;
        then (f.(p*s+(1-p)*t)-f.s)/((p*s+(1-p)*t)-s) < (f.t-f.s)/(t-s) &
        (f.t-f.s)/(t-s)<(f.t-f.(p*s+(1-p)*t))/(t-(p*s+(1-p)*t))
        by A10,A13,A17;
        then (f.(p*s+(1-p)*t)-f.s)/((p*s+(1-p)*t)-s)
        < (f.t-f.(p*s+(1-p)*t))/(t-(p*s+(1-p)*t)) by AXIOMS:22;
        then (f.(p*s+(1-p)*t)-f.s)*(t-(p*s+(1-p)*t))
        < (f.t-f.(p*s+(1-p)*t))*((p*s+(1-p)*t)-s) by A16,A19,REAL_2:187;
        then (f.(p*s+(1-p)*t)-f.s)*(t-s)*p
        < (f.t-f.(p*s+(1-p)*t))*((1-p)*(t-s)) by A15,A18,XCMPLX_1:4;
then A20:    (f.(p*s+(1-p)*t)-f.s)*(t-s)*p
        < (f.t-f.(p*s+(1-p)*t))*(t-s)*(1-p) by XCMPLX_1:4;
A21:    (f.(p*s+(1-p)*t)-f.s)*(t-s)*p
         =((t-s)*f.(p*s+(1-p)*t)-(t-s)*f.s)*p by XCMPLX_1:40
        .=p*((t-s)*f.(p*s+(1-p)*t))-p*((t-s)*f.s) by XCMPLX_1:40;
          (f.t-f.(p*s+(1-p)*t))*(t-s)*(1-p)
         =((t-s)*f.t-(t-s)*f.(p*s+(1-p)*t))*(1-p) by XCMPLX_1:40
        .=(1-p)*((t-s)*f.t)-(1-p)*((t-s)*f.(p*s+(1-p)*t)) by XCMPLX_1:40;
        then p*((t-s)*f.(p*s+(1-p)*t))+(1-p)*((t-s)*f.(p*s+(1-p)*t))
        <(1-p)*((t-s)*f.t)+p*((t-s)*f.s) by A20,A21,REAL_2:170;
        then (t-s)*f.(p*s+(1-p)*t)
        <(1-p)*((t-s)*f.t)+p*((t-s)*f.s) by Lm1;
        then (t-s)*f.(p*s+(1-p)*t)
        <(1-p)*f.t*(t-s)+p*((t-s)*f.s) by XCMPLX_1:4;
        then (t-s)*f.(p*s+(1-p)*t)
        <(1-p)*f.t*(t-s)+p*f.s*(t-s) by XCMPLX_1:4;
        then f.(p*s+(1-p)*t)
        <((1-p)*f.t*(t-s)+p*f.s*(t-s))/(t-s) by A14,REAL_2:178;
        then f.(p*s+(1-p)*t)
        <((1-p)*f.t*(t-s))/(t-s)+(p*f.s*(t-s))/(t-s) by XCMPLX_1:63;
        then f.(p*s+(1-p)*t)
        <(1-p)*f.t+(p*f.s*(t-s))/(t-s) by A14,XCMPLX_1:90;
        hence thesis by A14,XCMPLX_1:90;
        suppose s>t;
then A22:    s-t > 0 by SQUARE_1:11;
A23:    s-(p*s+(1-p)*t) = s-p*s - (1-p)*t by XCMPLX_1:36
        .=(1-p)*s-(1-p)*t by Lm1
        .=(1-p)*(s-t) by XCMPLX_1:40;
then A24:    s-(p*s+(1-p)*t) > 0 by A12,A22,REAL_2:122;
then A25:    (p*s+(1-p)*t) < s by REAL_2:106;
A26:    (p*s+(1-p)*t)-t = p*s+((1-p)*t-t) by XCMPLX_1:29
        .=p*s-(t-(1-p)*t) by XCMPLX_1:38
        .=p*s-p*t by Lm1
        .=p*(s-t) by XCMPLX_1:40;
then A27:    (p*s+(1-p)*t)-t > 0 by A11,A22,REAL_2:122;
        then (p*s+(1-p)*t) > t by REAL_2:106;
        then (f.(p*s+(1-p)*t)-f.t)/((p*s+(1-p)*t)-t) < (f.s-f.t)/(s-t) &
        (f.s-f.t)/(s-t)<(f.s-f.(p*s+(1-p)*t))/(s-(p*s+(1-p)*t))
        by A10,A13,A25;
        then (f.(p*s+(1-p)*t)-f.t)/((p*s+(1-p)*t)-t)
        < (f.s-f.(p*s+(1-p)*t))/(s-(p*s+(1-p)*t)) by AXIOMS:22;
        then (f.(p*s+(1-p)*t)-f.t)*(s-(p*s+(1-p)*t))
        < (f.s-f.(p*s+(1-p)*t))*((p*s+(1-p)*t)-t) by A24,A27,REAL_2:187;
        then (f.(p*s+(1-p)*t)-f.t)*(s-t)*(1-p)
        < (f.s-f.(p*s+(1-p)*t))*(p*(s-t)) by A23,A26,XCMPLX_1:4;
then A28:    (f.(p*s+(1-p)*t)-f.t)*(s-t)*(1-p)
        < (f.s-f.(p*s+(1-p)*t))*(s-t)*p by XCMPLX_1:4;
A29:    (f.(p*s+(1-p)*t)-f.t)*(s-t)*(1-p)
         =((s-t)*f.(p*s+(1-p)*t)-(s-t)*f.t)*(1-p) by XCMPLX_1:40
        .=(1-p)*((s-t)*f.(p*s+(1-p)*t))-(1-p)*((s-t)*f.t) by XCMPLX_1:40;
          (f.s-f.(p*s+(1-p)*t))*(s-t)*p
         =((s-t)*f.s-(s-t)*f.(p*s+(1-p)*t))*p by XCMPLX_1:40
        .=p*((s-t)*f.s)-p*((s-t)*f.(p*s+(1-p)*t)) by XCMPLX_1:40;
        then (1-p)*((s-t)*f.(p*s+(1-p)*t))+p*((s-t)*f.(p*s+(1-p)*t))
        <p*((s-t)*f.s)+(1-p)*((s-t)*f.t) by A28,A29,REAL_2:170;
        then (s-t)*f.(p*s+(1-p)*t)
        <p*((s-t)*f.s)+(1-p)*((s-t)*f.t) by Lm1;
        then (s-t)*f.(p*s+(1-p)*t)
        <p*f.s*(s-t)+(1-p)*((s-t)*f.t) by XCMPLX_1:4;
        then (s-t)*f.(p*s+(1-p)*t)
        <p*f.s*(s-t)+(1-p)*f.t*(s-t) by XCMPLX_1:4;
        then f.(p*s+(1-p)*t)
        <(p*f.s*(s-t)+(1-p)*f.t*(s-t))/(s-t) by A22,REAL_2:178;
        then f.(p*s+(1-p)*t)
        <(p*f.s*(s-t))/(s-t)+((1-p)*f.t*(s-t))/(s-t) by XCMPLX_1:63;
        then f.(p*s+(1-p)*t)
        <p*f.s+((1-p)*f.t*(s-t))/(s-t) by A22,XCMPLX_1:90;
        hence thesis by A22,XCMPLX_1:90;
       end;
       hence thesis;
      end;
      hence thesis;
     end;
     hence thesis by A10,Def1;
    end;
    hence thesis;
   end;
   hence thesis by A1;
end;

:: Jensen's Inequality

theorem
  for f being PartFunc of REAL,REAL
st f is total holds
(for n being Nat, P,E,F being Element of n-tuples_on REAL st Sum P=1 &
(for i being Nat st i in dom P holds P.i >=0 & F.i=f.(E.i))
holds f.Sum(mlt(P,E))<=Sum(mlt(P,F)))
iff f is_convex_on REAL
proof
   let f be PartFunc of REAL,REAL;
   assume f is total;
then A1:REAL c= dom f by PARTFUN1:def 4;
A2:(for n being Nat, P,E,F being Element of n-tuples_on REAL st Sum P=1 &
   (for i being Nat st i in dom P holds P.i >=0 & F.i=f.(E.i))
   holds f.Sum(mlt(P,E))<=Sum(mlt(P,F)))
   implies f is_convex_on REAL
   proof
    assume A3:for n being Nat, P,E,F being Element of n-tuples_on REAL st Sum
P=1
    & (for i being Nat st i in dom P holds P.i >=0 & F.i=f.(E.i))
    holds f.Sum(mlt(P,E))<=Sum(mlt(P,F));
      for p being Real st 0<=p & p<=1 holds
    for r,s being Real st r in REAL & s in REAL & p*r + (1-p)*s in REAL holds
    f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s
    proof
     let p be Real such that A4:0<=p & p<=1;
     let r,s be Real such that r in REAL & s in REAL & p*r + (1-p)*s in REAL;
     reconsider P=<*p,1-p*>, E=<*r,s*>, F=<*f.r,f.s*>
       as Element of 2-tuples_on REAL by FINSEQ_2:121;
A5:  Sum P=p+(1-p) by RVSUM_1:107 .= p-(p-1) by XCMPLX_1:38 .= 1
     by XCMPLX_1:18;
       for i being Nat st i in dom P holds P.i >=0 & F.i=f.(E.i)
     proof
      let i be Nat such that A6:i in dom P;
A7:   dom P = Seg len P by FINSEQ_1:def 3 .= Seg 2 by FINSEQ_2:109;
        now per cases by A6,A7,FINSEQ_1:4,TARSKI:def 2;
       suppose i=1;
       then E.i = r & P.i = p & F.i = f.r by FINSEQ_1:61;
       hence thesis by A4;
       suppose i=2;
       then E.i = s & P.i = 1-p & F.i = f.s by FINSEQ_1:61;
       hence thesis by A4,SQUARE_1:12;
      end;
      hence thesis;
     end;
then A8:  f.Sum(mlt(P,E))<=Sum(mlt(P,F)) by A3,A5;
A9:  P.1=p & P.2=1-p & E.1=r & E.2=s & F.1=f.r & F.2=f.s by FINSEQ_1:61;
       len P = 2 by FINSEQ_1:61 .= len E by FINSEQ_1:61;
     then len (multreal.:(P,E)) = len P by FINSEQ_2:86;
then A10: len mlt(P,E) = len P by RVSUM_1:def 9 .= 2 by FINSEQ_1:61;
       mlt(P,E).1 = P.1*E.1 & mlt(P,E).2 = P.2*E.2 by RVSUM_1:87;
     then mlt(P,E)=<*p*r,(1-p)*s*> by A9,A10,FINSEQ_1:61;
then A11: Sum(mlt(P,E))=p*r+(1-p)*s by RVSUM_1:107;
       len P = 2 by FINSEQ_1:61 .= len F by FINSEQ_1:61;
     then len (multreal.:(P,F)) = len P by FINSEQ_2:86;
then A12: len mlt(P,F) = len P by RVSUM_1:def 9 .= 2 by FINSEQ_1:61;
       mlt(P,F).1 = P.1*F.1 & mlt(P,F).2 = P.2*F.2 by RVSUM_1:87;
     then mlt(P,F)=<*p*f.r,(1-p)*f.s*> by A9,A12,FINSEQ_1:61;
     hence thesis by A8,A11,RVSUM_1:107;
    end;
    hence thesis by A1,RFUNCT_3:def 13;
   end;
     f is_convex_on REAL implies
   (for n being Nat, P,E,F being Element of n-tuples_on REAL st Sum P=1 &
   (for i being Nat st i in dom P holds P.i >=0 & F.i=f.(E.i))
   holds f.Sum(mlt(P,E))<=Sum(mlt(P,F)))
   proof
    assume A13:f is_convex_on REAL;
      for n being Nat, P,E,F being Element of n-tuples_on REAL st Sum P=1 &
    (for i being Nat st i in dom P holds P.i >=0 & F.i=f.(E.i))
    holds f.Sum(mlt(P,E))<=Sum(mlt(P,F))
    proof
      defpred S[Nat] means for P,E,F being Element of $1-tuples_on REAL st
      Sum P=1 & (for i being Nat st i in dom P holds P.i >=0 & F.i=f.(E.i))
       holds f.Sum(mlt(P,E))<=Sum(mlt(P,F));
A14: S[0] by RVSUM_1:109;
A15:  for k being Nat st S[k] holds S[k+1]
     proof
      let k be Nat such that
A16:  (for P,E,F being Element of k-tuples_on REAL st Sum P=1 &
      (for i being Nat st i in dom P holds P.i >=0 & F.i=f.(E.i))
      holds f.Sum(mlt(P,E))<=Sum(mlt(P,F)));

        for P,E,F being Element of (k+1)-tuples_on REAL st Sum P=1 &
      (for i being Nat st i in dom P holds P.i >=0 & F.i=f.(E.i))
      holds f.Sum(mlt(P,E))<=Sum(mlt(P,F))
      proof
       let P,E,F be Element of (k+1)-tuples_on REAL such that
A17:   Sum P=1 & (for i being Nat st i in dom P holds P.i>=0 & F.i=f.(E.i));
       consider P1 being Element of k-tuples_on REAL, p1 being Real such that
A18:   P=P1^<*p1*> by FINSEQ_2:137;
       consider E1 being Element of k-tuples_on REAL, e1 being Real such that
A19:   E=E1^<*e1*> by FINSEQ_2:137;
       consider F1 being Element of k-tuples_on REAL, f1 being Real such that
A20:   F=F1^<*f1*> by FINSEQ_2:137;
         mlt(P,E) = mlt(P1,E1)^<*p1*e1*> by A18,A19,Th2;
then A21:   Sum(mlt(P,E)) = 1*Sum(mlt(P1,E1))+p1*e1 by RVSUM_1:104;
         mlt(P,F) = mlt(P1,F1)^<*p1*f1*> by A18,A20,Th2;
then A22:   Sum(mlt(P,F)) = 1*Sum(mlt(P1,F1))+p1*f1 by RVSUM_1:104;
         len F1 + 1 = k + 1 by FINSEQ_2:109 .= len P by FINSEQ_2:109;
       then len F1 + 1 in Seg len P by FINSEQ_1:6;
then A23:   len F1 + 1 in dom P by FINSEQ_1:def 3;
A24:   f1=F.(len F1 + 1) by A20,FINSEQ_1:59 .= f.(E.(len F1 + 1)) by A17,A23
       .= f.(E.(k+1)) by FINSEQ_2:109 .= f.(E.(len E1+1)) by FINSEQ_2:109
       .= f.e1 by A19,FINSEQ_1:59;
A25:   for i being Nat st i in dom P1 holds P1.i>=0
       proof
        let i be Nat such that
A26:     i in dom P1;
          i in Seg len P1 by A26,FINSEQ_1:def 3;
        then 1 <= i & i <= len P1 by FINSEQ_1:3;
        then 1 <= i & i <= k & k <= k+1 by FINSEQ_2:109,NAT_1:29;
        then 1 <= i & i <= k+1 by AXIOMS:22;
        then i in Seg (k+1) by FINSEQ_1:3;
        then i in Seg len P by FINSEQ_2:109;
then A27:     i in dom P by FINSEQ_1:def 3;
          P1.i = P.i by A18,A26,FINSEQ_1:def 7;
        hence thesis by A17,A27;
       end;
         now per cases;
        suppose A28:Sum P1 = 0;
        then for i being Nat st i in dom P1 holds P1.i=0 by A25,Th3;
then A29:    P1 = k |-> (0 qua Real) by Th4;
        then mlt(P1,E1)=k |-> 0 by Th5;
then A30:    Sum(mlt(P1,E1))=k*0 by RVSUM_1:110;
A31:    Sum P = 0+p1 by A18,A28,RVSUM_1:104;
          mlt(P1,F1)=k |-> 0 by A29,Th5;
        then Sum(mlt(P1,F1))=k*0 by RVSUM_1:110;
        hence thesis by A17,A21,A22,A24,A30,A31;
        suppose A32:Sum P1 <>0;
then A33: Sum(mlt(P,E))=Sum P1*(Sum P1)"*Sum(mlt(P1,E1))+p1*e1
         by A21,XCMPLX_0:def 7
        .=Sum P1*((Sum P1)"*Sum(mlt(P1,E1)))+p1*e1 by XCMPLX_1:4
        .=Sum P1*(Sum((Sum P1)"*mlt(P1,E1)))+p1*e1 by RVSUM_1:117
        .=Sum P1*Sum(mlt((Sum P1)"*P1,E1))+p1*e1 by RVSUM_1:94;
          Sum P1+p1 = 1 by A17,A18,RVSUM_1:104;
then A34:    p1 = 1 - Sum P1 by XCMPLX_1:26;
A35:    0 <= Sum P1 & Sum P1 <= 1
        proof
         thus 0 <= Sum P1 by A25,RVSUM_1:114;
           len P1 + 1 = len P by A18,FINSEQ_2:19;
         then len P1 + 1 in Seg len P by FINSEQ_1:6;
then A36:     len P1 + 1 in dom P by FINSEQ_1:def 3;
           P.(len P1+1) = p1 by A18,FINSEQ_1:59;
         then p1 >= 0 by A17,A36;
         hence thesis by A34,REAL_2:105;
        end;
then A37:    f.Sum(mlt(P,E)) <= Sum P1*f.Sum(mlt((Sum P1)"*P1,E1)) + p1*f.e1
        by A13,A33,A34,RFUNCT_3:def 13;
          f.Sum(mlt((Sum P1)"*P1,E1)) <= (Sum P1)"*Sum(mlt(P1,F1))
        proof
A38:     (Sum P1)"*Sum(mlt(P1,F1)) = Sum((Sum P1)"*mlt(P1,F1)) by RVSUM_1:117
         .=Sum(mlt((Sum P1)"*P1,F1)) by RVSUM_1:94;
A39:     Sum((Sum P1)"*P1) = (Sum P1)"*Sum
P1 by RVSUM_1:117 .= 1 by A32,XCMPLX_0:def 7;
           for i being Nat st i in dom ((Sum P1)"*P1) holds
         ((Sum P1)"*P1).i >= 0 &
         F1.i=f.(E1.i)
         proof
          let i be Nat such that
A40:      i in dom ((Sum P1)"*P1);
            i in Seg len ((Sum P1)"*P1) by A40,FINSEQ_1:def 3;
then A41:      i in Seg k by FINSEQ_2:109;
A42:      ((Sum P1)"*P1).i = (Sum P1)"*P1.i by RVSUM_1:67;
A43:      (Sum P1)" > 0 by A32,A35,REAL_1:72;
A44:      i in Seg len P1 by A41,FINSEQ_2:109;
          then i in dom P1 by FINSEQ_1:def 3;
          then P1.i >=0 by A25;
          hence ((Sum P1)"*P1).i >= 0 by A42,A43,REAL_2:121;
            i in Seg len F1 & i in Seg len E1 by A41,FINSEQ_2:109;
then A45:      i in dom F1 & i in dom E1 by FINSEQ_1:def 3;

            1 <= i & i <= len P1 by A44,FINSEQ_1:3;
          then 1 <= i & i <= k & k <= k+1 by FINSEQ_2:109,NAT_1:29;
          then 1 <= i & i <= k+1 by AXIOMS:22;
          then i in Seg (k+1) by FINSEQ_1:3;
          then i in Seg len P by FINSEQ_2:109;
then A46:      i in dom P by FINSEQ_1:def 3;
            F.i = F1.i & E.i = E1.i by A19,A20,A45,FINSEQ_1:def 7;
          hence thesis by A17,A46;
         end;
         hence thesis by A16,A38,A39;
        end;
        then Sum P1*f.Sum(mlt((Sum P1)"*P1,E1)) <=
        Sum P1*((Sum P1)"*Sum(mlt(P1,F1)))
        by A35,AXIOMS:25;
        then Sum P1*f.Sum(mlt((Sum P1)"*P1,E1)) + p1*f.e1
        <= Sum P1*((Sum P1)"*Sum(mlt(P1,F1)))+p1*f.e1 by AXIOMS:24;
        then f.Sum(mlt(P,E))<=Sum P1*((Sum P1)"*Sum
(mlt(P1,F1)))+p1*f.e1 by A37,AXIOMS:22;
        then f.Sum(mlt(P,E)) <= Sum P1*(Sum P1)"*Sum(mlt(P1,F1))+p1*f.e1
        by XCMPLX_1:4;
        hence thesis by A22,A24,A32,XCMPLX_0:def 7;
       end;
       hence thesis;
      end;
      hence thesis;
     end;
     for k be Nat holds S[k] from Ind(A14,A15);
     hence thesis;
    end;
    hence thesis;
   end;
   hence thesis by A2;
end;

theorem
  for f being PartFunc of REAL,REAL, I being Interval, a being Real st
(ex x1,x2 being Real st x1 in I & x2 in I & x1 < a & a < x2) & f is_convex_on I
holds f is_continuous_in a
proof
   let f be PartFunc of REAL,REAL, I be Interval, a be Real such that
A1:(ex x1,x2 being Real st x1 in I & x2 in I & x1<a & a<x2) & f is_convex_on I;
A2:I c= dom f by A1,RFUNCT_3:def 13;
   consider x1,x2 being Real such that
A3:x1 in I & x2 in I & x1 < a & a < x2 by A1;
A4:a in I
   proof
      now per cases by MEASURE5:def 9;
     suppose I is open_interval;
     then consider p,q being R_eal such that
A5:  p <=' q & I = ].p,q.[ by MEASURE5:def 5;
     thus thesis by A3,A5,MEASURE6:38;
     suppose I is closed_interval;
     then consider p,q being R_eal such that
A6:  p <=' q & I = [.p,q.] by MEASURE5:def 6;
     thus thesis by A3,A6,MEASURE6:39;
     suppose I is right_open_interval;
     then consider p,q being R_eal such that
A7:  p <=' q & I = [.p,q.[by MEASURE5:def 7;
     thus thesis by A3,A7,MEASURE6:41;
     suppose I is left_open_interval;
     then consider p,q being R_eal such that
A8:  p <=' q & I = ].p,q.] by MEASURE5:def 8;
     thus thesis by A3,A8,MEASURE6:40;
    end;
    hence thesis;
   end;

A9:for x being Real st x1<=x & x<=x2 & x<>a holds
   (f.x1-f.a)/(x1-a) <= (f.x-f.a)/(x-a) &
   (f.x-f.a)/(x-a) <= (f.x2-f.a)/(x2-a)
   proof
    let x be Real such that
A10: x1 <= x & x <= x2 & x<>a;
      (f.x1-f.a)/(x1-a) <= (f.x-f.a)/(x-a) &
    (f.x-f.a)/(x-a) <= (f.x2-f.a)/(x2-a)
    proof
       now per cases by A10,AXIOMS:21;
      suppose A11:x < a;
A12:   x in I
      proof
         now per cases by MEASURE5:def 9;
        suppose I is open_interval;
        then consider p,q being R_eal such that
  A13:   p <=' q & I = ].p,q.[ by MEASURE5:def 5;
        thus thesis by A3,A10,A13,MEASURE6:38;
        suppose I is closed_interval;
        then consider p,q being R_eal such that
  A14:   p <=' q & I = [.p,q.] by MEASURE5:def 6;
        thus thesis by A3,A10,A14,MEASURE6:39;
        suppose I is right_open_interval;
        then consider p,q being R_eal such that
  A15:   p <=' q & I = [.p,q.[by MEASURE5:def 7;
        thus thesis by A3,A10,A15,MEASURE6:41;
        suppose I is left_open_interval;
        then consider p,q being R_eal such that
  A16:   p <=' q & I = ].p,q.] by MEASURE5:def 8;
        thus thesis by A3,A10,A16,MEASURE6:40;
       end;
       hence thesis;
      end;
      then (f.a-f.x)/(a-x)<=(f.x2-f.x)/(x2-x) &
      (f.x2-f.x)/(x2-x)<=(f.x2-f.a)/(x2-a) by A1,A3,A4,A11,Th16;
      then (f.a-f.x)/(a-x)<=(f.x2-f.a)/(x2-a) by AXIOMS:22;
      then (-(f.a-f.x))/(-(a-x)) <= (f.x2-f.a)/(x2-a) by XCMPLX_1:192
;
then A17:   (f.x-f.a)/(-(a-x)) <= (f.x2-f.a)/(x2-a) by XCMPLX_1:143;
        now per cases by A10,REAL_1:def 5;
       suppose x1=x;
       hence (f.x1-f.a)/(x1-a) <= (f.x-f.a)/(x-a);
       suppose A18:x1 < x;
A19:    (f.a-f.x)/(a-x) = (-(f.a-f.x))/(-(a-x)) by XCMPLX_1:192
       .=(f.x-f.a)/(-(a-x)) by XCMPLX_1:143 .=(f.x-f.a)/(x-a) by XCMPLX_1:143;
         (f.a-f.x1)/(a-x1) = (-(f.a-f.x1))/(-(a-x1)) by XCMPLX_1:192
       .=(f.x1-f.a)/(-(a-x1)) by XCMPLX_1:143 .=(f.x1-f.a)/(x1-a) by XCMPLX_1:
143;
       hence (f.x1-f.a)/(x1-a)<=(f.x-f.a)/(x-a) by A1,A3,A4,A11,A12,A18,A19,
Th16;
      end;
      hence thesis by A17,XCMPLX_1:143;

      suppose A20:x > a;
A21:  x in I
      proof
         now per cases by MEASURE5:def 9;
        suppose I is open_interval;
        then consider p,q being R_eal such that
  A22:   p <=' q & I = ].p,q.[ by MEASURE5:def 5;
        thus thesis by A3,A10,A22,MEASURE6:38;
        suppose I is closed_interval;
        then consider p,q being R_eal such that
  A23:   p <=' q & I = [.p,q.] by MEASURE5:def 6;
        thus thesis by A3,A10,A23,MEASURE6:39;
        suppose I is right_open_interval;
        then consider p,q being R_eal such that
  A24:   p <=' q & I = [.p,q.[ by MEASURE5:def 7;
        thus thesis by A3,A10,A24,MEASURE6:41;
        suppose I is left_open_interval;
        then consider p,q being R_eal such that
  A25:   p <=' q & I = ].p,q.] by MEASURE5:def 8;
        thus thesis by A3,A10,A25,MEASURE6:40;
       end;
       hence thesis;
      end;
then A26:  (f.a-f.x1)/(a-x1)<=(f.x-f.x1)/(x-x1) &
      (f.x-f.x1)/(x-x1)<=(f.x-f.a)/(x-a) by A1,A3,A4,A20,Th16;
        (f.a-f.x1)/(a-x1) = (-(f.a-f.x1))/(-(a-x1)) by XCMPLX_1:192
      .=(f.x1-f.a)/(-(a-x1)) by XCMPLX_1:143 .=(f.x1-f.a)/(x1-a) by XCMPLX_1:
143;
      hence (f.x1-f.a)/(x1-a) <= (f.x-f.a)/(x-a) by A26,AXIOMS:22;
        now per cases by A10,REAL_1:def 5;
       suppose x=x2;
       hence (f.x-f.a)/(x-a) <= (f.x2-f.a)/(x2-a);
       suppose x<x2;
       hence (f.x-f.a)/(x-a)<=(f.x2-f.a)/(x2-a) by A1,A3,A4,A20,A21,Th16;
      end;
      hence (f.x-f.a)/(x-a) <= (f.x2-f.a)/(x2-a);
     end;
     hence thesis;
    end;
    hence thesis;
   end;

   set M = max(abs((f.x1-f.a)/(x1-a)),abs((f.x2-f.a)/(x2-a)));
    A27: abs((f.x1-f.a)/(x1-a)) >= 0 & abs((f.x2-f.a)/(x2-a)) >= 0
     by ABSVALUE:5;
then A28:min(abs((f.x1-f.a)/(x1-a)),abs((f.x2-f.a)/(x2-a))) >= 0 by SQUARE_1:39
;
    A29: max(abs((f.x1-f.a)/(x1-a)),abs((f.x2-f.a)/(x2-a)))
   >= min(abs((f.x1-f.a)/(x1-a)),abs((f.x2-f.a)/(x2-a))) by Th1;
A30:M >= 0 by A28,Th1;

A31:for x being real number st x1<=x & x<=x2 & x<>a holds
   abs(f.x-f.a)<=M*abs(x-a)
   proof
    let x be real number such that A32:x1<=x & x<=x2 & x<>a;
    reconsider x as Real by XREAL_0:def 1;
      x<a or x>a by A32,AXIOMS:21;
 then x-a <> 0 by REAL_2:105,SQUARE_1:11;
then A33: abs(x-a) > 0 by ABSVALUE:6;

A34: (f.x1-f.a)/(x1-a) <= (f.x-f.a)/(x-a) &
    (f.x-f.a)/(x-a) <= (f.x2-f.a)/(x2-a) by A9,A32;
      -abs((f.x1-f.a)/(x1-a)) <= (f.x1-f.a)/(x1-a) &
    (f.x2-f.a)/(x2-a) <= abs((f.x2-f.a)/(x2-a)) by ABSVALUE:11;
then A35: -abs((f.x1-f.a)/(x1-a)) <= (f.x-f.a)/(x-a) &
    (f.x-f.a)/(x-a) <= abs((f.x2-f.a)/(x2-a)) by A34,AXIOMS:22;
      now per cases;
     suppose abs((f.x1-f.a)/(x1-a)) <= abs((f.x2-f.a)/(x2-a));
     then -abs((f.x1-f.a)/(x1-a)) >= -abs((f.x2-f.a)/(x2-a))
     by REAL_1:50;
     then -abs((f.x2-f.a)/(x2-a)) <= (f.x-f.a)/(x-a) by A35,AXIOMS:22;
     then abs((f.x-f.a)/(x-a)) <= abs((f.x2-f.a)/(x2-a)) by A35,ABSVALUE:12;
then A36:  abs((f.x-f.a))/abs((x-a)) <= abs((f.x2-f.a)/(x2-a)) by ABSVALUE:16;
       abs((f.x2-f.a)/(x2-a)) <= M by SQUARE_1:46;
     then abs((f.x-f.a))/abs((x-a)) <= M by A36,AXIOMS:22;
     hence thesis by A33,REAL_2:178;
     suppose abs((f.x1-f.a)/(x1-a)) >= abs((f.x2-f.a)/(x2-a));
     then (f.x-f.a)/(x-a) <= abs((f.x1-f.a)/(x1-a)) by A35,AXIOMS:22;
     then abs((f.x-f.a)/(x-a)) <= abs((f.x1-f.a)/(x1-a)) by A35,ABSVALUE:12;
then A37:  abs((f.x-f.a))/abs((x-a)) <= abs((f.x1-f.a)/(x1-a)) by ABSVALUE:16;
       abs((f.x1-f.a)/(x1-a)) <= M by SQUARE_1:46;
     then abs((f.x-f.a))/abs((x-a)) <= M by A37,AXIOMS:22;
     hence thesis by A33,REAL_2:178;
    end;
    hence thesis;
   end;

     for r being real number st 0<r ex s being real number st 0<s &
    for x being real number st
   x in dom f & abs(x-a)<s holds abs(f.x-f.a)<r
   proof
    let r be real number such that
A38: 0<r;
    reconsider r as Real by XREAL_0:def 1;
      ex s being real number st 0<s & for x being real number st
     x in dom f & abs(x-a)<s holds abs(f.x-f.a)<r
    proof
       now per cases by A27,A29,SQUARE_1:39;
      suppose A39:M>0;
      set s = min(r/M,min(a-x1,x2-a));
A40:   s>0
      proof
A41:   min(a-x1,x2-a) > 0
       proof
          now per cases by SQUARE_1:38;
         suppose min(a-x1,x2-a)=a-x1;
         hence thesis by A3,SQUARE_1:11;
         suppose min(a-x1,x2-a)=x2-a;
         hence thesis by A3,SQUARE_1:11;
        end;
        hence thesis;
       end;
         now per cases by SQUARE_1:38;
        suppose s = r/M;
        hence thesis by A38,A39,REAL_2:127;
        suppose s = min(a-x1,x2-a);
        hence thesis by A41;
       end;
       hence thesis;
      end;
    for x being real number st x in dom f & abs(x-a)<s holds
      abs(f.x-f.a)<r
      proof
       let x be real number such that A42:x in dom f & abs(x-a)<s;
A43:   s <= r/M & s<=min(a-x1,x2-a) by SQUARE_1:35;
         min(a-x1,x2-a)<=a-x1 & min(a-x1,x2-a)<=x2-a by SQUARE_1:35;
       then s <= a-x1 & s <= x2-a by A43,AXIOMS:22;
       then abs(x-a)<a-x1 & abs(x-a)<x2-a by A42,AXIOMS:22;
       then -(a-x1) <= x-a & x-a <= x2-a by ABSVALUE:12;
       then x1-a <= x-a & x-a <=x2-a by XCMPLX_1:143;
then A44:   x1 <= x & x <= x2 by REAL_1:54;
         now per cases;
        suppose x<>a;
then A45:    abs(f.x-f.a)<=M*abs(x-a) by A31,A44;
          now per cases;
         suppose A46:M<>0;
then A47:     M*abs(x-a) < M*s by A30,A42,REAL_1:70;
           M*s <= M*(r/M) by A28,A29,A43,AXIOMS:25;
         then M*abs(x-a) < M*(r/M) by A47,AXIOMS:22;
         then M*abs(x-a) < (r*M)/M by Lm4;
         then M*abs(x-a) < r*(M/M) by Lm4;
         then M*abs(x-a) < r*1 by A46,XCMPLX_1:60;
         hence thesis by A45,AXIOMS:22;
         suppose M=0;
         hence thesis by A38,A45;
        end;
        hence thesis;
        suppose x=a;
        then f.x-f.a=0 by XCMPLX_1:14;
        hence thesis by A38,ABSVALUE:7;
       end;
       hence thesis;
      end;
      hence thesis by A40;

      suppose A48:M=0;
A49:   for x being real number st x1<=x & x<=x2 & x<>a holds
      abs(f.x-f.a)=0
      proof
       let x be real number such that A50:x1<=x & x<=x2 & x<>a;
    abs(f.x-f.a)<=M*abs(x-a) by A31,A50;
       hence thesis by A48,ABSVALUE:5;
      end;
      set s = min(a-x1,x2-a);
A51:   s > 0
      proof
         now per cases by SQUARE_1:38;
        suppose s=a-x1;
        hence thesis by A3,SQUARE_1:11;
        suppose s=x2-a;
        hence thesis by A3,SQUARE_1:11;
       end;
       hence thesis;
      end;
    for x being real number st x in dom f & abs(x-a)<s holds
      abs(f.x-f.a)<r
      proof
       let x be real number such that A52:x in dom f & abs(x-a)<s;
         s<=a-x1 & s<=x2-a by SQUARE_1:35;
       then abs(x-a)<a-x1 & abs(x-a)<x2-a by A52,AXIOMS:22;
       then -(a-x1) <= x-a & x-a <= x2-a by ABSVALUE:12;
       then x1-a <= x-a & x-a <=x2-a by XCMPLX_1:143;
then A53:    x1 <= x & x <= x2 by REAL_1:54;
         now per cases;
        suppose x<>a;
        hence thesis by A38,A49,A53;
        suppose x=a;
        then f.x-f.a=0 by XCMPLX_1:14;
        hence thesis by A38,ABSVALUE:7;
       end;
       hence thesis;
      end;
      hence thesis by A51;
     end;
     hence thesis;
    end;
    hence thesis;
   end;
   hence thesis by A2,A4,FCONT_1:3;
end;

begin :: Definitions of several convexity and semicontinuity concepts

definition
let f, X;
pred f is_quasiconvex_on X means :Def2:
X c= dom f &
for p being Real st 0<p & p<1 holds
 for r,s being Real st r in X & s in X & p*r + (1-p)*s in X holds
  f.(p*r + (1-p)*s) <= max(f.r,f.s);
end;

definition
let f, X;
pred f is_strictly_quasiconvex_on X means :Def3:
X c= dom f &
for p being Real st 0<p & p<1 holds
 for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & f.r <> f.s holds
  f.(p*r + (1-p)*s) < max(f.r,f.s);
end;

definition
let f, X;
pred f is_strongly_quasiconvex_on X means :Def4:
X c= dom f &
for p being Real st 0<p & p<1 holds
 for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
  f.(p*r + (1-p)*s) < max(f.r,f.s);
end;

definition let f; let x0 be real number;
pred f is_upper_semicontinuous_in x0 means :Def5:
x0 in dom f &
(for r st 0<r ex s st 0<s & for x st
 x in dom f & abs(x-x0)<s holds f.x0-f.x<r);
end;

definition let f,X;
pred f is_upper_semicontinuous_on X means :Def6:
X c= dom f & for x0 st x0 in X holds f|X is_upper_semicontinuous_in x0;
end;

definition let f; let x0 be real number;
pred f is_lower_semicontinuous_in x0 means :Def7:
x0 in dom f &
 (for r st 0<r ex s st 0<s &
  for x st x in dom f & abs(x-x0)<s holds f.x-f.x0<r);
end;

definition let f,X;
pred f is_lower_semicontinuous_on X means :Def8:
X c= dom f & for x0 st x0 in X holds f|X is_lower_semicontinuous_in x0;
end;

theorem Th20:
for x0 be real number, f holds
f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0
iff f is_continuous_in x0
proof
   let x0 be real number, f;
A1:f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0
   implies f is_continuous_in x0
   proof
    assume
A2: f is_upper_semicontinuous_in x0&f is_lower_semicontinuous_in x0;
then A3: x0 in dom f &
    (for r st 0<r ex s st 0<s & for x st x in dom f & abs(x-x0)<s holds
    f.x-f.x0<r) &
    (for r st 0<r ex s st 0<s & for x st x in dom f & abs(x-x0)<s holds
    f.x0-f.x<r) by Def5,Def7;
      for r be real number st 0<r ex s be real number st 0<s &
    for x be real number st x in dom f & abs(x-x0)<s holds
    abs(f.x-f.x0)<r
    proof
     let r be real number such that A4: 0<r;
A5:  r is Real by XREAL_0:def 1;
     then consider s1 being Real such that
A6:  0<s1 & for x st x in dom f & abs(x-x0)<s1 holds f.x-f.x0<r by A2,A4,Def7;
     consider s2 being Real such that
A7:  0<s2 &
     for x st x in dom f & abs(x-x0)<s2 holds f.x0-f.x<r by A2,A4,A5,Def5;
     set s = min(s1,s2);
A8:  s > 0
     proof
        now per cases;
       suppose s1<=s2;
       hence 0<s by A6,SQUARE_1:def 1;
       suppose not (s1<=s2);
       hence 0<s by A7,SQUARE_1:def 1;
      end;
      hence thesis;
     end;
A9:  for x be real number st x in dom f & abs(x-x0)<s holds abs(f.x-f.x0)<r
     proof
      let x be real number such that A10:x in dom f & abs(x-x0)<s;
A11:   x is Real by XREAL_0:def 1;
        s <= s1 & s <= s2 by SQUARE_1:35;
      then abs(x-x0)<s1 & abs(x-x0)<s2 by A10,AXIOMS:22;
then A12:   f.x-f.x0<r & f.x0-f.x<r by A6,A7,A10,A11;
      then f.x-f.x0<r & -(f.x0-f.x)>-r by REAL_1:50;
      then f.x-f.x0<r & f.x-f.x0>-r by XCMPLX_1:143;
then A13:   abs(f.x-f.x0)<=r & f.x-f.x0<>r & f.x-f.x0<>-r by ABSVALUE:12;
        abs(f.x-f.x0)<>r
      proof
       assume A14:abs(f.x-f.x0)=r;
         now per cases;
        suppose f.x-f.x0>=0;
        hence contradiction by A12,A14,ABSVALUE:def 1;
        suppose not (f.x-f.x0>=0);
        then abs(f.x-f.x0)=-(f.x-f.x0) by ABSVALUE:def 1;
        hence contradiction by A12,A14,XCMPLX_1:143;
       end;
       hence thesis;
      end;
      hence thesis by A13,REAL_1:def 5;
     end;
     take s;
     thus thesis by A8,A9;
    end;
    hence f is_continuous_in x0 by A3,FCONT_1:3;
   end;
     f is_continuous_in x0 implies
   f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0
   proof
    assume A15:f is_continuous_in x0;
then A16:x0 in dom f &
    for r be real number st 0<r ex s be real number st 0<s &
    for x be real number st x in dom f & abs(x-x0)<s holds
    abs(f.x-f.x0)<r by FCONT_1:3;
A17:for r st 0<r ex s st 0<s & for x st x in dom f & abs(x-x0)<s holds
    f.x-f.x0<r
    proof
     let r such that A18:0<r;
     consider s be real number such that
A19: 0<s & for x be real number st x in dom f &
     abs(x-x0)<s holds abs(f.x-f.x0)<r
     by A15,A18,FCONT_1:3;
A20: for x st x in dom f & abs(x-x0)<s holds f.x-f.x0<r
     proof
      let x such that A21:x in dom f & abs(x-x0)<s;
A22:  abs(f.x-f.x0)<r by A19,A21;
        f.x-f.x0<=abs(f.x-f.x0) by ABSVALUE:11;
      hence thesis by A22,AXIOMS:22;
     end;
     take s;
     thus s is Real by XREAL_0:def 1;
     thus thesis by A19,A20;
    end;
      for r st 0<r ex s st 0<s & for x st x in dom f & abs(x-x0)<s holds
    f.x0-f.x<r
    proof
     let r such that A23:0<r;
     consider s be real number such that
A24: 0<s & for x be real number st x in dom f & abs(x-x0)<s
        holds abs(f.x-f.x0)<r by A15,A23,FCONT_1:3;
A25: for x st x in dom f & abs(x-x0)<s holds f.x0-f.x<r
     proof
      let x such that A26:x in dom f & abs(x-x0)<s;
A27:  abs(f.x-f.x0)<r by A24,A26;
        f.x-f.x0>=-abs(f.x-f.x0) by ABSVALUE:11;
      then -(f.x-f.x0)<=abs(f.x-f.x0) by REAL_2:110;
      then f.x0-f.x <= abs(f.x-f.x0) by XCMPLX_1:143;
      hence thesis by A27,AXIOMS:22;
     end;
     take s;
     thus s is Real by XREAL_0:def 1;
     thus thesis by A24,A25;
    end;
    hence thesis by A16,A17,Def5,Def7;
   end;
   hence thesis by A1;
end;

theorem
  for X, f holds
f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X
iff f is_continuous_on X
proof
   let X, f;
A1:f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X
   implies f is_continuous_on X
   proof
    assume
A2: f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X;

      X c= dom f & for x0 be real number st x0 in X holds f|X is_continuous_in
x0
    proof
     thus X c= dom f by A2,Def6;
     let x0 be real number such that A3:x0 in X;
       x0 is Real by XREAL_0:def 1;
      then f|X is_upper_semicontinuous_in x0 & f|X is_lower_semicontinuous_in
x0
      by A2,A3,Def6,Def8;
     hence thesis by Th20;
    end;
    hence thesis by FCONT_1:def 2;
   end;
     f is_continuous_on X implies
   f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X
   proof
    assume A4:f is_continuous_on X;
      X c= dom f &
    (for x0 st x0 in X holds f|X is_upper_semicontinuous_in x0) &
    (for x0 st x0 in X holds f|X is_lower_semicontinuous_in x0)
    proof
     thus X c= dom f by A4,FCONT_1:def 2;
A5:  for x0 st x0 in X holds f|X is_upper_semicontinuous_in x0
     proof
      let x0; assume
A6:   x0 in X;
        f|X is_upper_semicontinuous_in x0
      proof
         f|X is_continuous_in x0 by A4,A6,FCONT_1:def 2;
       hence thesis by Th20;
      end;
      hence thesis;
     end;
       for x0 st x0 in X holds f|X is_lower_semicontinuous_in x0
     proof
      let x0; assume
A7:   x0 in X;
        f|X is_lower_semicontinuous_in x0
      proof
         f|X is_continuous_in x0 by A4,A7,FCONT_1:def 2;
       hence thesis by Th20;
      end;
      hence thesis;
     end;
     hence thesis by A5;
    end;
    hence thesis by Def6,Def8;
   end;
   hence thesis by A1;
end;

theorem
  for X, f st f is_strictly_convex_on X holds f is_strongly_quasiconvex_on X
proof
   let X, f such that
A1:f is_strictly_convex_on X;

A2:X c= dom f by A1,Def1;

     for p being Real st 0<p & p<1 holds
   for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
   f.(p*r + (1-p)*s) < max(f.r,f.s)
   proof
    let p be Real;
    assume A3:0<p & p<1;
      for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
    f.(p*r + (1-p)*s) < max(f.r,f.s)
    proof
     let r,s be Real;
     assume r in X & s in X & p*r + (1-p)*s in X & r <> s;
then A4:  f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s by A1,A3,Def1;
A5:  1-p > 0 by A3,SQUARE_1:11;
       f.r <= max(f.r,f.s) & f.s <= max(f.r,f.s) by SQUARE_1:46;
     then p*f.r<=p*max(f.r,f.s) & (1-p)*f.s<=(1-p)*max(f.r,f.s)
     by A3,A5,AXIOMS:25;
     then p*f.r + (1-p)*f.s <= p*max(f.r,f.s)+(1-p)*max(f.r,f.s) by REAL_1:55;
     then p*f.r + (1-p)*f.s <= max(f.r,f.s) by Lm1;
     hence thesis by A4,AXIOMS:22;
    end;
    hence thesis;
   end;
   hence thesis by A2,Def4;
end;

theorem
  for X, f st f is_strongly_quasiconvex_on X holds f is_quasiconvex_on X
proof
   let X,f such that
A1:f is_strongly_quasiconvex_on X;
A2:X c= dom f by A1,Def4;
     for p being Real st 0<p & p<1 holds
   for r,s being Real st r in X & s in X & p*r + (1-p)*s in X holds
   f.(p*r + (1-p)*s) <= max(f.r,f.s)
   proof
    let p be Real such that
A3: 0<p & p<1;
      for r,s being Real st r in X & s in X & p*r + (1-p)*s in X holds
    f.(p*r + (1-p)*s) <= max(f.r,f.s)
    proof
     let r,s be Real such that
A4:  r in X & s in X & p*r + (1-p)*s in X;
       now per cases;
      suppose r<>s;
      hence f.(p*r + (1-p)*s) <= max(f.r,f.s) by A1,A3,A4,Def4;
      suppose r=s;
      hence f.(p*r + (1-p)*s) <= max(f.r,f.s) by Lm1;
     end;
     hence thesis;
    end;
    hence thesis;
   end;
   hence thesis by A2,Def2;
end;

theorem
  for X, f st f is_convex_on X holds f is_strictly_quasiconvex_on X
proof
   let X,f such that
A1:f is_convex_on X;
A2:X c= dom f by A1,RFUNCT_3:def 13;

     for p being Real st 0<p & p<1 holds
   for r,s being Real st r in X & s in X &
   p*r + (1-p)*s in X & f.r <> f.s holds
   f.(p*r + (1-p)*s) < max(f.r,f.s)
   proof
    let p be Real such that
A3: 0<p & p<1;
      for r,s being Real st
    r in X & s in X & p*r + (1-p)*s in X & f.r <> f.s holds
    f.(p*r + (1-p)*s) < max(f.r,f.s)
    proof
     let r,s be Real such that
A4:  r in X & s in X & p*r + (1-p)*s in X & f.r <> f.s;
A5:  f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s by A1,A3,A4,RFUNCT_3:def 13;
A6:  1-p > 0 by A3,SQUARE_1:11;
       now per cases by A4,REAL_1:def 5;
      suppose f.r < f.s;
      then p*f.r < p*f.s by A3,REAL_1:70;
      then p*f.r + (1-p)*f.s < p*f.s + (1-p)*f.s by REAL_1:53;
      then p*f.r + (1-p)*f.s < f.s by Lm1;
then A7:   f.(p*r + (1-p)*s) < f.s by A5,AXIOMS:22;
        f.s <= max(f.r,f.s) by SQUARE_1:46;
      hence f.(p*r + (1-p)*s) < max(f.r,f.s) by A7,AXIOMS:22;
      suppose f.r > f.s;
      then (1-p)*f.r > (1-p)*f.s by A6,REAL_1:70;
      then p*f.r + (1-p)*f.s < p*f.r + (1-p)*f.r by REAL_1:53;
      then p*f.r + (1-p)*f.s < f.r by Lm1;
then A8:   f.(p*r + (1-p)*s) < f.r by A5,AXIOMS:22;
        f.r <= max(f.r,f.s) by SQUARE_1:46;
      hence thesis by A8,AXIOMS:22;
     end;
     hence thesis;
    end;
    hence thesis;
   end;
   hence thesis by A2,Def3;
end;

theorem
  for X, f st f is_strongly_quasiconvex_on X holds
f is_strictly_quasiconvex_on X
proof
   let X, f such that
A1:f is_strongly_quasiconvex_on X;
A2:X c= dom f by A1,Def4;
     for p being Real st 0<p & p<1 holds
   for r,s being Real st
   r in X & s in X & p*r + (1-p)*s in X & f.r <> f.s holds
   f.(p*r + (1-p)*s) < max(f.r,f.s) by A1,Def4;
   hence thesis by A2,Def3;
end;

theorem
  for X, f st f is_strictly_quasiconvex_on X & f is one-to-one holds
f is_strongly_quasiconvex_on X
proof
   let X, f such that
A1:f is_strictly_quasiconvex_on X & f is one-to-one;
A2:X c= dom f by A1,Def3;
     for p being Real st 0<p & p<1 holds
   for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
   f.(p*r + (1-p)*s) < max(f.r,f.s)
   proof
    let p be Real such that
A3: 0<p & p<1;
      for r,s being Real st r in X & s in X & p*r + (1-p)*s in X & r <> s holds
    f.(p*r + (1-p)*s) < max(f.r,f.s)
    proof
     let r,s be Real such that
A4:  r in X & s in X & p*r + (1-p)*s in X & r <> s;
       f.(p*r + (1-p)*s) < max(f.r,f.s)
     proof
        f.r <> f.s by A1,A2,A4,FUNCT_1:def 8;
      hence thesis by A1,A3,A4,Def3;
     end;
     hence thesis;
    end;
    hence thesis;
   end;
   hence thesis by A2,Def4;
end;

Back to top