:: Introduction to Several Concepts of Convexity and Semicontinuity :: for Function from REAL to REAL :: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama :: :: Received March 23, 2000 :: Copyright (c) 2000-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, REAL_1, PARTFUN1, SUBSET_1, XXREAL_0, FINSEQ_2, RVSUM_1, ORDINAL4, FINSEQ_1, RELAT_1, ARYTM_3, NAT_1, FUNCT_1, CARD_3, CARD_1, TARSKI, ARYTM_1, RFUNCT_3, XXREAL_1, VALUED_1, XBOOLE_0, BINOP_2, MEASURE5, FCONT_1, COMPLEX1, ORDINAL2, RFUNCT_4, FUNCT_7; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, RELAT_1, COMPLEX1, NAT_1, FUNCT_1, FINSEQ_1, REAL_1, FINSEQ_2, PARTFUN1, FUNCOP_1, FINSEQOP, BINOP_1, BINOP_2, VALUED_1, RVSUM_1, RCOMP_1, RFUNCT_3, MEASURE5, FCONT_1, XXREAL_0; constructors BINOP_1, REAL_1, NAT_1, BINOP_2, COMPLEX1, FINSEQOP, RCOMP_1, RVSUM_1, FCONT_1, RFUNCT_3, MEASURE5, XXREAL_2, RELSET_1, FINSEQ_4, CARD_3, FUNCOP_1; registrations RELSET_1, NUMBERS, XXREAL_0, XREAL_0, BINOP_2, MEMBERED, FINSEQ_2, VALUED_0, FINSEQ_1, FUNCT_1, RVSUM_1, ORDINAL1; requirements NUMERALS, SUBSET, REAL, BOOLE, ARITHM; equalities RVSUM_1, ORDINAL1; theorems RCOMP_1, RFUNCT_3, TARSKI, PARTFUN1, FINSEQ_1, FINSEQ_2, RVSUM_1, NAT_1, FCONT_1, ABSVALUE, FUNCT_1, XREAL_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, FINSEQOP, VALUED_1, XXREAL_2, RELAT_1, CARD_1; schemes NAT_1; begin reserve a,b,p,r,r1,r2,s,s1,s2,x0,x for Real; reserve f,g for PartFunc of REAL,REAL; reserve X,Y for set; theorem Th1: for a, b being Real holds max(a,b) >= min(a,b) proof let a, b be Real; per cases by XXREAL_0:15; suppose min(a,b)=a; hence thesis by XXREAL_0:25; end; suppose min(a,b)=b; hence thesis by XXREAL_0:25; end; end; theorem Th2: for n being Nat, R1,R2 being Element of n-tuples_on REAL, r1,r2 being Real holds mlt(R1^<*r1*>,R2^<*r2*>)=mlt(R1,R2)^<*r1*r2*> proof let n be Nat; let R1,R2 be Element of n-tuples_on REAL; let r1,r2 be Real; reconsider r1,r2 as Element of REAL by XREAL_0:def 1; len (R1^<*r1*>) = len R1 + 1 by FINSEQ_2:16 .= n+1 by CARD_1:def 7 .= len R2 + 1 by CARD_1:def 7 .= len (R2^<*r2*>) by FINSEQ_2:16; then A1: len(mlt(R1^<*r1*>,R2^<*r2*>)) = len (R1^<*r1*>) by FINSEQ_2:72 .= len R1 + 1 by FINSEQ_2:16 .= n+1 by CARD_1:def 7; A2: for k being Nat st k in Seg(n+1) holds mlt(R1^<*r1*>,R2^<*r2*>).k = ( mlt(R1,R2)^<*r1*r2*>).k proof let k be Nat such that A3: k in Seg (n+1); A4: k<=n+1 by A3,FINSEQ_1:1; now per cases by A4,XXREAL_0:1; suppose k).k = R1.k by FINSEQ_1:def 7; k in Seg len R2 by A6,CARD_1:def 7; then k in dom R2 by FINSEQ_1:def 3; then (R2^<*r2*>).k = R2.k by FINSEQ_1:def 7; then A8: mlt(R1^<*r1*>,R2^<*r2*>).k = (R1.k)*(R2.k) by A7,RVSUM_1:59; len (mlt(R1,R2)) = n by CARD_1:def 7; then k in dom mlt(R1,R2) by A6,FINSEQ_1:def 3; then (mlt(R1,R2)^<*r1*r2*>).k = mlt(R1,R2).k by FINSEQ_1:def 7; hence thesis by A8,RVSUM_1:59; end; suppose A9: k=n+1; then k=len R1+1 by CARD_1:def 7; then A10: (R1^<*r1*>).k=r1 by FINSEQ_1:42; A11: n+1 = len (mlt(R1,R2)) + 1 by CARD_1:def 7; k=len R2+1 by A9,CARD_1:def 7; then (R2^<*r2*>).k=r2 by FINSEQ_1:42; then mlt(R1^<*r1*>,R2^<*r2*>).k = r1*r2 by A10,RVSUM_1:59; hence thesis by A9,A11,FINSEQ_1:42; end; end; hence thesis; end; reconsider rr = r1*r2 as Element of REAL; mlt(R1^<*r1*>,R2^<*r2*>) is Element of (n+1)-tuples_on REAL by A1,FINSEQ_2:92; hence thesis by A2,FINSEQ_2:119; end; theorem Th3: for n being Nat, R being Element of n-tuples_on REAL st Sum R=0 & (for i being Element of NAT st i in dom R holds 0 <= R.i) holds for i being Element of NAT st i in dom R holds R.i = 0 proof let n be Nat, R be Element of n-tuples_on REAL such that A1: Sum R=0 and A2: for i being Element of NAT st i in dom R holds 0 <= R.i; A3: for i being Nat st i in dom R holds 0 <= R.i by A2; given k being Element of NAT such that A4: k in dom R and A5: R.k <> 0; 0 <= R.k by A2,A4; hence contradiction by A1,A3,A4,A5,RVSUM_1:85; end; theorem Th4: for n being Nat, R being Element of n-tuples_on REAL st (for i being Element of NAT st i in dom R holds 0 = R.i) holds R = n |-> (0 qua Real) proof let n be Nat, R be Element of n-tuples_on REAL such that A1: for i being Element of NAT st i in dom R holds 0 = R.i; A2: for k be Nat st 1 <= k & k <= len R holds R.k = (n |-> 0).k proof let k be Nat; assume 1 <= k & k <= len R; then k in Seg len R by FINSEQ_1:1; then k in dom R by FINSEQ_1:def 3; then A3: R.k = 0 by A1; thus thesis by A3; end; len R = n by CARD_1:def 7 .= len (n |-> 0) by CARD_1:def 7; hence thesis by A2,FINSEQ_1:14; end; theorem Th5: for n being Nat, R being Element of n-tuples_on REAL holds mlt(n |-> (0 qua Real),R) = n |-> (0 qua Real) proof let n be Nat, R be Element of n-tuples_on REAL; A1: len(mlt(n |-> In(0,REAL),R)) =n by CARD_1:def 7; A2: for k be Nat st 1 <= k & k <= len mlt(n |-> (0 qua Real),R) holds mlt(n |-> (0 qua Real),R).k = (n |-> (0 qua Real)).k proof let k be Nat; assume 1 <= k & k <= len mlt(n |-> (0 qua Real),R); mlt(n |-> (0 qua Real),R).k = (n |-> (0 qua Real)).k*R.k by RVSUM_1:60 .=0*R.k; hence thesis; end; len (n |-> (0 qua Real)) = n by CARD_1:def 7; hence thesis by A1,A2,FINSEQ_1:14; end; begin :: Convex and strictly convex functions definition let f, X; pred f is_strictly_convex_on X means X c= dom f & for p being Real st 0

s holds f.(p*r + (1-p)*s) < p*f.r + (1-p)*f.s; end; theorem f is_strictly_convex_on X implies f is_convex_on X proof assume A1: f is_strictly_convex_on X; A2: for p being Real st 0<=p & p<=1 holds for r,s being Real st r in X & s in X & p*r + (1-p)*s in X holds f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s proof let p be Real; assume A3: 0<=p & p<=1; for r,s being Real st r in X & s in X & p*r+(1-p)*s in X holds f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s proof let r,s be Real; assume A4: r in X & s in X & p*r+(1-p)*s in X; now per cases by A3,XXREAL_0:1; suppose p=0; hence thesis; end; suppose p=1; hence thesis; end; suppose A5: 0

s; hence thesis by A1,A4,A5; end; end; hence thesis; end; end; hence thesis; end; hence thesis; end; X c= dom f by A1; hence thesis by A2,RFUNCT_3:def 12; end; theorem for a,b be Real, f be PartFunc of REAL,REAL holds f is_strictly_convex_on [.a,b.] iff [.a,b.] c= dom f & for p be Real st 0

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

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

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 0 by A15,XREAL_1:50; A17: s - t = p*(s-r); then s - t > 0 by A6,A16,XREAL_1:129; then A18: t < s by XREAL_1:47; A19: t - r = (1-p)*(s-r); then A20: (t-r)/(s-r)=1-p by A16,XCMPLX_1:89; t - r > 0 by A7,A16,A19,XREAL_1:129; then A21: r < t by XREAL_1:47; (s-t)/(s-r)=p by A16,A17,XCMPLX_1:89; hence thesis by A3,A5,A21,A18,A20; end; end; end; hence thesis; end; hence thesis; end; hence thesis by A2,RFUNCT_3:def 12; end; f is_convex_on X implies X c= dom f & for a,b,c being Real st a in X & b in X & c in X & a 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

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 0 by A16,XREAL_1:50; A18: s - t = p*(s-r); then s - t > 0 by A7,A17,XREAL_1:129; then A19: t < s by XREAL_1:47; A20: t - r = (1-p)*(s-r); then A21: (t-r)/(s-r)=1-p by A17,XCMPLX_1:89; t - r > 0 by A8,A17,A20,XREAL_1:129; then A22: r < t by XREAL_1:47; (s-t)/(s-r)=p by A17,A18,XCMPLX_1:89; hence thesis by A3,A5,A22,A19,A21; end; end; hence thesis; end; end; hence thesis; end; hence thesis; end; hence thesis; end; hence thesis by A2; end; f is_strictly_convex_on X implies X c= dom f & for a,b,c being Real st a in X & b in X & c in X & a 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 f is_strictly_convex_on X iff f-r is_strictly_convex_on X proof A1: dom(f-r) = dom f by VALUED_1:3; A2: for x being Element of REAL st x in dom (f-r) holds ((f-r)-(-r)).x = f.x proof let x be Element of REAL; assume A3: x in dom (f-r); then ((f-r)-(-r)).x=(f-r).x-(-r) by VALUED_1:3 .=(f-r).x+r .=f.x-r+r by A1,A3,VALUED_1:3 .= f.x-(r-r); hence thesis; end; dom((f-r)-(-r))=dom(f-r) by VALUED_1:3; then (f-r)-(-r) = f by A1,A2,PARTFUN1:5; hence thesis by Lm1; end; Lm2: 0 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 Th12: 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 Th14: f is_strictly_convex_on X & g is_convex_on X implies f+g is_strictly_convex_on X proof assume A1: f is_strictly_convex_on X & g is_convex_on X; then X c= dom f & X c= dom g by RFUNCT_3:def 12; then X c= dom f /\ dom g by XBOOLE_1:19; then A2: X c= dom (f+g) by VALUED_1:def 1; for p being Real st 0

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 f is_strictly_convex_on X & g is_strictly_convex_on X & ( a>0 & b>=0 or a>=0 & b>0 ) implies a(#)f+b(#)g is_strictly_convex_on X proof assume that A1: f is_strictly_convex_on X and A2: g is_strictly_convex_on X and A3: a>0 & b>=0 or a>=0 & b>0; now per cases by A3; suppose a>0 & b>0; then a(#)f is_strictly_convex_on X & b(#)g is_strictly_convex_on X by A1,A2 ,Th12; hence thesis by Th13; end; suppose A4: a>0 & b=0; A5: X c= dom g by A2; a(#)f is_strictly_convex_on X by A1,A4,Th12; hence thesis by A4,A5,Th14,RFUNCT_3:57; end; suppose A6: a=0 & b>0; A7: X c= dom f by A1; b(#)g is_strictly_convex_on X by A2,A6,Th12; hence thesis by A6,A7,Th14,RFUNCT_3:57; end; end; hence thesis; end; theorem Th16: f is_convex_on X iff X c= dom f & for a,b,r st a in X & b in X & r in X & a < r & r < b holds (f.r-f.a)/(r-a) <= (f.b-f.a)/(b-a) & (f.b-f.a)/(b- a) <= (f.b-f.r)/(b-r) proof A1: X c= dom f & (for a,b,r st a in X & b in X & r in X & a < r & r < b holds (f.r-f.a)/(r-a) <= (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) <= (f.b-f.r)/(b-r)) implies f is_convex_on X proof assume that A2: X c= dom f and A3: for a,b,r st a in X & b in X & r in X & a < r & r < b holds (f.r- f .a)/(r-a) <= (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) <= (f.b-f.r)/(b-r); for p being Real st 0<=p & p<=1 for r,s be Real st r in X & s in X & p*r + (1-p)*s in X holds f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f.s proof let p be Real; assume A4: 0<=p & p<=1; for s,t being Real st s in X & t in X & p*s+(1-p)*t in X holds f.(p *s+(1-p)*t) <= p*f.s + (1-p)*f.t proof let s,t be Real; assume A5: s in X & t in X & p*s+(1-p)*t in X; now per cases by A4,XXREAL_0:1; suppose p=0; hence thesis; end; suppose p=1; hence thesis; end; suppose A6: 0

0 by XREAL_1:50; now per cases by XXREAL_0:1; suppose s=t; hence thesis; end; suppose s 0 by XREAL_1:50; (p*s+(1-p)*t)-s =(1-p)*(t-s); then A9: (p*s+(1-p)*t)-s > 0 by A7,A8,XREAL_1:129; then A10: (p*s+(1-p)*t) > s by XREAL_1:47; A11: (f.(p*s+(1-p)*t)-f.s)*(t-s)*p =p*((t-s)*f.(p*s+(1-p)*t))- p*((t-s)*f.s) & (f. t-f.(p*s+(1-p)*t))*(t-s)*(1-p) =(1-p)*((t-s)*f.t)-(1-p)*((t -s)*f.(p*s+(1-p)*t)); t-(p*s+(1-p)*t) =p*(t-s); then A12: t-(p*s+(1-p)*t) > 0 by A6,A8,XREAL_1:129; then (p*s+(1-p)*t) < t by XREAL_1:47; then (f.(p*s+(1-p)*t)-f.s)/((p*s+(1-p)*t)-s) <= (f.t-f.s)/(t-s ) & (f.t-f.s)/(t-s) <=(f.t-f.(p*s+(1-p)*t))/(t-(p*s+(1-p)*t)) by A3,A5,A10; then (f.(p*s+(1-p)*t)-f.s)/((p*s+(1-p)*t)-s) <= (f.t-f.(p*s+(1 -p)*t))/(t-(p*s+(1-p)*t)) by XXREAL_0:2; then (f.(p*s+(1-p)*t)-f.s)*(t-(p*s+(1-p)*t)) <= (f.t-f.(p*s+(1 -p)*t))*((p*s+(1-p)*t)-s) by A12,A9,XREAL_1:106; then p*((t-s)*f.(p*s+(1-p)*t))+(1-p)*((t-s)*f.(p*s+(1-p)*t)) <=(1-p)*((t-s)*f.t)+p*((t-s)*f.s) by A11,XREAL_1:21; then f.(p*s+(1-p)*t) <=((1-p)*f.t*(t-s)+p*f.s*(t-s))/(t-s) by A8,XREAL_1:77; then f.(p*s+(1-p)*t) <=((1-p)*f.t*(t-s))/(t-s)+(p*f.s*(t-s))/( t-s) by XCMPLX_1:62; then f.(p*s+(1-p)*t) <=(1-p)*f.t+(p*f.s*(t-s))/(t-s) by A8, XCMPLX_1:89; hence thesis by A8,XCMPLX_1:89; end; suppose s>t; then A13: s-t > 0 by XREAL_1:50; (p*s+(1-p)*t)-t =p*(s-t); then A14: (p*s+(1-p)*t)-t > 0 by A6,A13,XREAL_1:129; then A15: (p*s+(1-p)*t) > t by XREAL_1:47; A16: (f.(p*s+(1-p)*t)-f.t)*(s-t)*(1-p) =(1-p)*((s-t)*f.(p*s+(1 -p)*t))-(1-p)*((s-t) *f.t) & (f.s-f.(p*s+(1-p)*t))*(s-t)*p =p*((s-t)*f.s)-p*((s -t)*f.(p*s+(1-p)*t)); s-(p*s+(1-p)*t) =(1-p)*(s-t); then A17: s-(p*s+(1-p)*t) > 0 by A7,A13,XREAL_1:129; then (p*s+(1-p)*t) < s by XREAL_1:47; then (f.(p*s+(1-p)*t)-f.t)/((p*s+(1-p)*t)-t) <= (f.s-f.t)/(s-t ) & (f.s-f.t)/(s-t) <=(f.s-f.(p*s+(1-p)*t))/(s-(p*s+(1-p)*t)) by A3,A5,A15; then (f.(p*s+(1-p)*t)-f.t)/((p*s+(1-p)*t)-t) <= (f.s-f.(p*s+(1 -p)*t))/(s-(p*s+(1-p)*t)) by XXREAL_0:2; then (f.(p*s+(1-p)*t)-f.t)*(s-(p*s+(1-p)*t)) <= (f.s-f.(p*s+(1 -p)*t))*((p*s+(1-p)*t)-t) by A17,A14,XREAL_1:106; then (1-p)*((s-t)*f.(p*s+(1-p)*t))+p*((s-t)*f.(p*s+(1-p)*t)) <=p*((s-t)*f.s)+(1-p)*((s-t)*f.t) by A16,XREAL_1:21; then f.(p*s+(1-p)*t) <=(p*f.s*(s-t)+(1-p)*f.t*(s-t))/(s-t) by A13,XREAL_1:77; then f.(p*s+(1-p)*t) <=(p*f.s*(s-t))/(s-t)+((1-p)*f.t*(s-t))/( s-t) by XCMPLX_1:62; then f.(p*s+(1-p)*t) <=p*f.s+((1-p)*f.t*(s-t))/(s-t) by A13, XCMPLX_1:89; hence thesis by A13,XCMPLX_1:89; end; end; hence thesis; end; end; hence thesis; end; hence thesis; end; hence thesis by A2,RFUNCT_3:def 12; end; f is_convex_on X implies X c= dom f & for a,b,r st a in X & b in X & r in X & a < r & r < b holds (f.r-f.a)/(r-a) <= (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) <= (f.b-f.r)/(b-r) proof assume A18: f is_convex_on X; for a,b,r st a in X & b in X & r in X & a < r & r < b holds (f.r-f.a)/ (r-a) <= (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) <= (f.b-f.r)/(b-r) proof let a,b,r; assume that A19: a in X & b in X & r in X and A20: a < r and A21: r < b; reconsider aa=a, bb=b as Real; A22: b-r < b-a & 0 < b-r by A20,A21,XREAL_1:10,50; reconsider p = (b-r)/(b-a) as Real; A23: 0 < r-a by A20,XREAL_1:50; A24: p+(r-a)/(b-a) = ((b-r)+(r-a))/(b-a) by XCMPLX_1:62 .= 1 by A22,XCMPLX_1:60; then p*a + (1-p)*b = (a*(b-r))/(b-a)+b*((r-a)/(b-a)) by XCMPLX_1:74 .= (a*(b-r))/(b-a)+(b*(r-a))/(b-a) by XCMPLX_1:74 .= ((b*a-r*a)+(r-a)*b)/(b-a) by XCMPLX_1:62 .= r*(b-a)/(b-a); then A25: p*a + (1-p)*b = r by A22,XCMPLX_1:89; A26: (b-a)*((b-r)/(b-a)*f.a + (r-a)/(b-a)*f.b) = (b-a)*((b-r)/(b-a))*f.a + (b-a)*((r-a)/(b-a)*f.b) .= (b-r)*f.a + (b-a)*((r-a)/(b-a))*f.b by A22,XCMPLX_1:87 .= (b-r)*f.a + (r-a)*f.b by A22,XCMPLX_1:87; (bb-r)/(bb-aa) < 1 by A22,XREAL_1:189; then A27: f.(p*a+(1-p)*b) <= p*f.a + (1-p)*f.b by A18,A19,A22,A25,RFUNCT_3:def 12; then (b-a)*f.r <= (b-a)*f.a + ((r-a)*f.b - (r-a)*f.a) by A22,A24,A25,A26, XREAL_1:64; then (b-a)*f.r - (b-a)*f.a <= (r-a)*f.b - (r-a)*f.a by XREAL_1:20; then (b-a)*(f.r-f.a) <= (r-a)*(f.b-f.a); hence (f.r-f.a)/(r-a) <= (f.b-f.a)/(b-a) by A22,A23,XREAL_1:102; (b-a)*f.r <= (b-a)*f.b - ((b-r)*f.b - (b-r)*f.a) by A22,A24,A25,A27,A26, XREAL_1:64; then ((b-r)*f.b-(b-r)*f.a)+(b-a)*f.r <= (b-a)*f.b by XREAL_1:19; then (b-r)*f.b-(b-r)*f.a <= (b-a)*f.b-(b-a)*f.r by XREAL_1:19; then (b-r)*(f.b-f.a) <= (b-a)*(f.b-f.r); hence thesis by A22,XREAL_1:102; end; hence thesis by A18,RFUNCT_3:def 12; end; hence thesis by A1; end; theorem f is_strictly_convex_on X iff X c= dom f & for a,b,r st a in X & b in X & r in X & a < r & r < b holds (f.r-f.a)/(r-a) < (f.b-f.a)/(b-a) & (f.b-f.a)/ (b-a) < (f.b-f.r)/(b-r) proof A1: X c= dom f & (for a,b,r st a in X & b in X & r in X & a < r & r < b holds (f.r-f.a)/(r-a) < (f.b-f.a)/(b-a) & (f.b-f.a)/(b-a) < (f.b-f.r)/(b-r)) implies f is_strictly_convex_on X proof assume that A2: X c= dom f and A3: for a,b,r st a in X & b in X & r in X & a 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 being Real st s in X & t in X & p*s+(1-p)*t in X & s <> t holds f.(p*s + (1-p)*t) < p*f.s + (1-p)*f.t proof let s,t be Real; assume that A7: s in X & t in X & p*s+(1-p)*t in X and A8: s <> t; now per cases by A8,XXREAL_0:1; suppose s 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)) =0 & F.i=f.(E.i)) holds f.Sum(mlt (P,E))<=Sum(mlt(P,F))) implies f is_convex_on REAL proof let f be PartFunc of REAL,REAL; assume f is total; then A1: REAL c= dom f by PARTFUN1:def 2; (for n being Element of NAT, P,E,F being Element of n-tuples_on REAL st Sum P=1 & (for i being Element of NAT st i in dom P holds P.i >=0 & F.i=f.(E.i) ) holds f.Sum(mlt(P,E))<=Sum(mlt(P,F))) implies f is_convex_on REAL proof assume A2: for n being Element of NAT, P,E,F being Element of n-tuples_on REAL st Sum P=1 & (for i being Element of NAT st i in dom P holds P.i >=0 & F.i =f.(E.i)) holds f.Sum(mlt(P,E))<=Sum(mlt(P,F)); for p being Real st 0<=p & p<=1 for r,s being Real st r in REAL & s in REAL & p*r + (1-p)*s in REAL holds f.(p*r + (1-p)*s) <= p*f.r + (1-p)*f. s proof let p be Real such that A3: 0<=p and A4: p<=1; let r,s be Real such that r in REAL and s in REAL and p*r + (1-p)*s in REAL; reconsider rr=r,ss=s,pp=p, mp=1-p as Element of REAL by XREAL_0:def 1; f.rr in REAL & f.ss in REAL by XREAL_0:def 1; then reconsider P=<*pp,mp*>, E=<*rr,ss*>, F=<*f.rr,f.ss*> as Element of 2-tuples_on REAL by FINSEQ_2:101; A5: for i being Element of NAT st i in dom P holds P.i >=0 & F.i=f.(E.i ) proof A6: dom P = Seg len P by FINSEQ_1:def 3 .= Seg 2 by CARD_1:def 7; let i be Element of NAT such that A7: i in dom P; now per cases by A7,A6,FINSEQ_1:2,TARSKI:def 2; suppose A8: i=1; 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 for f being PartFunc of REAL,REAL st f is_convex_on REAL holds (for n being Element of NAT, P,E,F being Element of n-tuples_on REAL st Sum P=1 & (for i being Element of NAT st i in dom P holds P.i >=0 & F.i=f.(E.i)) holds f.Sum(mlt (P,E))<=Sum(mlt(P,F))) proof let f be PartFunc of REAL,REAL; assume A1: f is_convex_on REAL; defpred S[Nat] means for P,E,F being Element of \$1-tuples_on REAL st Sum P=1 & (for i being Element of NAT st i in dom P holds P.i >=0 & F.i =f.(E.i)) holds f.Sum(mlt(P,E))<=Sum(mlt(P,F)); A2: for k being Nat st S[k] holds S[k+1] proof let k be Nat such that A3: S[k]; let P,E,F be Element of (k+1)-tuples_on REAL such that A4: Sum P=1 and A5: for i being Element of NAT st i in dom P holds P.i>=0 & F.i=f.(E.i); consider E1 being Element of k-tuples_on REAL, e1 being Element of REAL such that A6: E=E1^<*e1*> by FINSEQ_2:117; consider F1 being Element of k-tuples_on REAL, f1 being Element of REAL such that A7: F=F1^<*f1*> by FINSEQ_2:117; len F1 + 1 = k + 1 by CARD_1:def 7 .= len P by CARD_1:def 7; then len F1 + 1 in Seg len P by FINSEQ_1:4; then A8: len F1 + 1 in dom P by FINSEQ_1:def 3; A9: f1=F.(len F1 + 1) by A7,FINSEQ_1:42 .= f.(E.(len F1 + 1)) by A5,A8 .= f.(E.(k+1)) by CARD_1:def 7 .= f.(E.(len E1+1)) by CARD_1:def 7 .= f.e1 by A6,FINSEQ_1:42; consider P1 being Element of k-tuples_on REAL, p1 being Element of REAL such that A10: P=P1^<*p1*> by FINSEQ_2:117; reconsider SP = (Sum P1)" as Element of REAL by XREAL_0:def 1; mlt(P,F) = mlt(P1,F1)^<*p1*f1*> by A10,A7,Th2; then A11: Sum(mlt(P,F)) = 1*Sum(mlt(P1,F1))+p1*f1 by RVSUM_1:74; mlt(P,E) = mlt(P1,E1)^<*p1*e1*> by A10,A6,Th2; then A12: Sum(mlt(P,E)) = 1*Sum(mlt(P1,E1))+p1*e1 by RVSUM_1:74; A13: for i being Nat st i in dom P1 holds P1.i>=0 proof let i be Nat such that A14: i in dom P1; A15: i in Seg len P1 by A14,FINSEQ_1:def 3; then A16: 1 <= i by FINSEQ_1:1; i <= len P1 by A15,FINSEQ_1:1; then A17: i <= k by CARD_1:def 7; k <= k+1 by NAT_1:11; then i <= k+1 by A17,XXREAL_0:2; then i in Seg (k+1) by A16,FINSEQ_1:1; then i in Seg len P by CARD_1:def 7; then A18: i in dom P by FINSEQ_1:def 3; P1.i = P.i by A10,A14,FINSEQ_1:def 7; hence thesis by A5,A18; end; then A19: for i being Element of NAT st i in dom P1 holds P1.i>= 0; now per cases; suppose A20: Sum P1 = 0; then for i being Element of NAT st i in dom P1 holds P1.i=0 by A19,Th3; then A21: P1 = k |-> (0 qua Real) by Th4; then mlt(P1,E1)=k |-> 0 by Th5; then A22: Sum(mlt(P1,E1))=k*0 by RVSUM_1:80; mlt(P1,F1)=k |-> 0 by A21,Th5; then A23: Sum(mlt(P1,F1))=k*0 by RVSUM_1:80; Sum P = 0+p1 by A10,A20,RVSUM_1:74; hence thesis by A4,A12,A11,A9,A22,A23; end; suppose A24: Sum P1 <>0; A25: 0 <= Sum P1 by A13,RVSUM_1:84; A26: for i being Element of NAT st i in dom ((Sum P1)"*P1) holds ((Sum P1)"*P1).i >= 0 & F1.i=f.(E1.i) proof let i be Element of NAT; assume i in dom ((Sum P1)"*P1); then A27: i in Seg len ((Sum P1)"*P1) by FINSEQ_1:def 3; then A28: i in Seg k by CARD_1:def 7; then A29: i in Seg len P1 by CARD_1:def 7; then i <= len P1 by FINSEQ_1:1; then A30: i <= k by CARD_1:def 7; A31: 1 <= i by A27,FINSEQ_1:1; k <= k+1 by NAT_1:11; then i <= k+1 by A30,XXREAL_0:2; then i in Seg (k+1) by A31,FINSEQ_1:1; then i in Seg len P by CARD_1:def 7; then A32: i in dom P by FINSEQ_1:def 3; i in dom P1 by A29,FINSEQ_1:def 3; then ((Sum P1)"*P1).i = (Sum P1)"*P1.i & P1.i >=0 by A13,RVSUM_1:45; hence ((Sum P1)"*P1).i >= 0 by A25; i in Seg len E1 by A28,CARD_1:def 7; then i in dom E1 by FINSEQ_1:def 3; then A33: E.i = E1.i by A6,FINSEQ_1:def 7; i in Seg len F1 by A28,CARD_1:def 7; then i in dom F1 by FINSEQ_1:def 3; then F.i = F1.i by A7,FINSEQ_1:def 7; hence thesis by A5,A32,A33; end; A34: Sum(mlt(P,E))=Sum P1*(Sum P1)"*Sum(mlt(P1,E1)) +p1*e1 by A12,A24,XCMPLX_0:def 7 .=Sum P1*((Sum P1)"*Sum(mlt(P1,E1)))+p1*e1 .=Sum P1*(Sum(SP*mlt(P1,E1)))+p1*e1 by RVSUM_1:87 .=Sum P1*Sum(mlt(SP*P1,E1))+p1*e1 by FINSEQOP:26; A35: ( Sum P1)"*Sum(mlt(P1,F1)) = Sum(SP*mlt(P1,F1)) by RVSUM_1:87 .=Sum(mlt(SP*P1,F1)) by FINSEQOP:26; len P1 + 1 = len P by A10,FINSEQ_2:16; then len P1 + 1 in Seg len P by FINSEQ_1:4; then A36: len P1 + 1 in dom P by FINSEQ_1:def 3; Sum P1+p1 = 1 by A4,A10,RVSUM_1:74; then A37: p1 = 1 - Sum P1; Sum((Sum P1)"*P1) = (Sum P1)"*Sum P1 by RVSUM_1:87 .= 1 by A24,XCMPLX_0:def 7; then Sum P1*f.Sum(mlt((Sum P1)"*P1,E1)) <= Sum P1*((Sum P1)"* Sum(mlt(P1,F1))) by A3,A25,A35,A26,XREAL_1:64; then A38: Sum P1*f.Sum(mlt((Sum P1)"*P1,E1)) + p1*f.e1 <= Sum P1*(( Sum P1)"*Sum(mlt(P1,F1)))+p1*f.e1 by XREAL_1:6; A39: Sum(mlt(SP*P1,E1)) in REAL by XREAL_0:def 1; A40: (Sum P1)*Sum(mlt(SP*P1,E1)) + p1*e1 in REAL by XREAL_0:def 1; P.(len P1+1) = p1 by A10,FINSEQ_1:42; then Sum P1 <= 1 by A5,A37,A36,XREAL_1:49; then f.Sum(mlt(P,E)) <= Sum P1*f.Sum(mlt((Sum P1)"* P1,E1)) + p1*f.e1 by A1,A34,A37,A25,RFUNCT_3:def 12,A39,A40; then f.Sum(mlt(P,E)) <= Sum P1*(Sum P1)"*Sum(mlt(P1,F1))+p1*f. e1 by A38,XXREAL_0:2; hence thesis by A11,A9,A24,XCMPLX_0:def 7; end; end; hence thesis; end; A41: S[0] by RVSUM_1:79; for k be Nat holds S[k] from NAT_1:sch 2(A41,A2); hence thesis; end; theorem for f being PartFunc of REAL,REAL, I being Interval, a being Real st ( ex x1,x2 being Real st x1 in I & x2 in I & x1 < a & a < x2) & f is_convex_on I holds f is_continuous_in a proof let f be PartFunc of REAL,REAL, I be Interval, a be Real such that A1: ex x1,x2 being Real st x1 in I & x2 in I & x1a 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 xa holds |.f.x-f.a.|<=M* |.x-a.| proof A20: -|.(f.x1-f.a)/(x1-a).| <= (f.x1-f.a)/(x1-a) by ABSVALUE:4; A21: (f.x2-f.a)/(x2-a) <= |.(f.x2-f.a)/(x2-a).| by ABSVALUE:4; let x be Real such that A22: x1<=x & x<=x2 and A23: x<>a; reconsider x as Real; (f.x-f.a)/(x-a) <= (f.x2-f.a)/(x2-a) by A8,A22,A23; then A24: (f.x-f.a)/(x-a) <= |.(f.x2-f.a)/(x2-a).| by A21,XXREAL_0:2; x-a <> 0 by A23; then A25: |.x-a.| > 0 by COMPLEX1:47; (f.x1-f.a)/(x1-a) <= (f.x-f.a)/(x-a) by A8,A22,A23; then A26: -|.(f.x1-f.a)/(x1-a).| <= (f.x-f.a)/(x-a) by A20,XXREAL_0:2; now per cases; suppose |.(f.x1-f.a)/(x1-a).| <= |.(f.x2-f.a)/(x2-a).|; then -|.(f.x1-f.a)/(x1-a).| >= -|.(f.x2-f.a)/(x2-a).| by XREAL_1:24; then -|.(f.x2-f.a)/(x2-a).| <= (f.x-f.a)/(x-a) by A26,XXREAL_0:2; then |.(f.x-f.a)/(x-a).| <= |.(f.x2-f.a)/(x2-a).| by A24,ABSVALUE:5; then A27: |.(f.x-f.a).|/|.(x-a).| <= |.(f.x2-f.a)/(x2-a).| by COMPLEX1:67; |.(f.x2-f.a)/(x2-a).| <= M by XXREAL_0:25; then |.(f.x-f.a).|/|.(x-a).| <= M by A27,XXREAL_0:2; hence thesis by A25,XREAL_1:81; end; suppose |.(f.x1-f.a)/(x1-a).| >= |.(f.x2-f.a)/(x2-a).|; then (f.x-f.a)/(x-a) <= |.(f.x1-f.a)/(x1-a).| by A24,XXREAL_0:2; then |.(f.x-f.a)/(x-a).| <= |.(f.x1-f.a)/(x1-a).| by A26,ABSVALUE:5; then A28: |.(f.x-f.a).|/|.(x-a).| <= |.(f.x1-f.a)/(x1-a).| by COMPLEX1:67; |.(f.x1-f.a)/(x1-a).| <= M by XXREAL_0:25; then |.(f.x-f.a).|/|.(x-a).| <= M by A28,XXREAL_0:2; hence thesis by A25,XREAL_1:81; end; end; hence thesis; end; A29: max(|.(f.x1-f.a)/(x1-a).|,|.(f.x2-f.a)/(x2-a).|) >= min(|.(f.x1-f.a )/(x1-a).|,|.(f.x2-f.a)/(x2-a).|) by Th1; A30: |.(f.x1-f.a)/(x1-a).| >= 0 & |.(f.x2-f.a)/(x2-a).| >= 0 by COMPLEX1:46; then A31: min(|.(f.x1-f.a)/(x1-a).|,|.(f.x2-f.a)/(x2-a).|) >= 0 by XXREAL_0:20; then A32: M >= 0 by Th1; for r being Real st 00; set s = min(r/M,min(a-x1,x2-a)); A35: for x being Real st x in dom f & |.x-a.|a; then A40: |.f.x-f.a.|<=M*|.x-a.| by A19,A38,A39; now per cases; suppose A41: M<>0; A42: M*s <= M*(r/M) by A31,A29,XREAL_1:64,XXREAL_0:17; M*|.x-a.| < M*s by A32,A37,A41,XREAL_1:68; then M*|.x-a.| < M*(r/M) by A42,XXREAL_0:2; then M*|.x-a.| < (r*M)/M by XCMPLX_1:74; then M*|.x-a.| < r*(M/M) by XCMPLX_1:74; then M*|.x-a.| < r*1 by A41,XCMPLX_1:60; hence thesis by A40,XXREAL_0:2; end; suppose M=0; hence thesis by A33,A40; end; end; hence thesis; end; suppose x=a; hence thesis by A33,ABSVALUE:2; end; end; hence thesis; end; s>0 proof A43: min(a-x1,x2-a) > 0 proof now per cases by XXREAL_0:15; suppose min(a-x1,x2-a)=a-x1; hence thesis by A5,XREAL_1:50; end; suppose min(a-x1,x2-a)=x2-a; hence thesis by A6,XREAL_1:50; end; end; hence thesis; end; now per cases by XXREAL_0:15; suppose s = r/M; hence thesis by A33,A34,XREAL_1:139; end; suppose s = min(a-x1,x2-a); hence thesis by A43; end; end; hence thesis; end; hence thesis by A35; end; suppose A44: M=0; set s = min(a-x1,x2-a); A45: for x being Real st x1<=x & x<=x2 & x<>a holds |.f.x- f.a.|=0 proof let x be Real; assume x1<=x & x<=x2 & x<>a; then |.f.x-f.a.|<=M*|.x-a.| by A19; hence thesis by A44,COMPLEX1:46; end; A46: for x being Real st x in dom f & |.x-a.|a; hence thesis by A33,A45,A48,A49; end; suppose x=a; hence thesis by A33,ABSVALUE:2; end; end; hence thesis; end; s > 0 proof now per cases by XXREAL_0:15; suppose s=a-x1; hence thesis by A5,XREAL_1:50; end; suppose s=x2-a; hence thesis by A6,XREAL_1:50; end; end; hence thesis; end; hence thesis by A46; end; end; hence thesis; end; hence thesis; end; hence thesis by FCONT_1:3; end; begin :: Definitions of several convexity and semicontinuity concepts definition let f, X; pred f is_quasiconvex_on X means X c= dom f & for p being Real st 0

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

s holds f.(p*r + (1-p)*s) < max(f.r,f.s); end; definition let f; let x0 be Real; pred f is_upper_semicontinuous_in x0 means x0 in dom f & for r st 0=-|.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 0r proof assume A24: |.f.x-f.x0.|=r; now per cases; suppose f.x-f.x0>=0; hence contradiction by A22,A24,ABSVALUE:def 1; end; suppose not f.x-f.x0>=0; then |.f.x-f.x0.|=-(f.x-f.x0) by ABSVALUE:def 1; hence contradiction by A21,A24; end; end; hence thesis; end; -(f.x0-f.x)>-r by A21,XREAL_1:24; then |.f.x-f.x0.|<=r by A22,ABSVALUE:5; hence thesis by A23,XXREAL_0:1; end; take s; s > 0 proof now per cases; suppose s1<=s2; hence thesis by A14,XXREAL_0:def 9; end; suppose not s1<=s2; hence thesis by A16,XXREAL_0:def 9; end; end; hence thesis; end; hence thesis by A18; end; hence thesis by FCONT_1:3; end; hence thesis by A2; end; theorem for X, f st X c= dom f holds f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X iff f|X is continuous proof let X, f such that A1: X c= dom f; A2: f|X is continuous implies f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X proof assume A3: f|X is continuous; A4: for x0 st x0 in X holds f|X is_lower_semicontinuous_in x0 proof let x0; assume x0 in X; then A5: x0 in dom(f|X) by A1,RELAT_1:57; then f|X is_continuous_in x0 by A3,FCONT_1:def 2; hence thesis by A5,Th21; end; for x0 st x0 in X holds f|X is_upper_semicontinuous_in x0 proof let x0; assume x0 in X; then A6: x0 in dom(f|X) by A1,RELAT_1:57; then f|X is_continuous_in x0 by A3,FCONT_1:def 2; hence thesis by A6,Th21; end; hence thesis by A1,A4; end; f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X implies f|X is continuous proof assume that A7: f is_upper_semicontinuous_on X and A8: f is_lower_semicontinuous_on X; X c= dom f & for x0 be Real st x0 in dom(f|X) holds f|X is_continuous_in x0 proof thus X c= dom f by A7; let x0 be Real such that A9: x0 in dom(f|X); x0 in X by A9,RELAT_1:57; then f|X is_upper_semicontinuous_in x0 & f|X is_lower_semicontinuous_in x0 by A7,A8; hence thesis by Th21; end; hence thesis by FCONT_1:def 2; end; hence thesis by A2; end; theorem for X, f st f is_strictly_convex_on X holds f is_strongly_quasiconvex_on X proof let X, f such that A1: f is_strictly_convex_on X; A2: for p being Real st 0

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 for X, f st f is_strongly_quasiconvex_on X holds f is_quasiconvex_on X proof let X,f such that A1: f is_strongly_quasiconvex_on X; A2: for p being Real st 0

s; hence thesis by A1,A3,A4; end; suppose r=s; hence thesis; end; end; hence thesis; end; hence thesis; end; X c= dom f by A1; hence thesis by A2; end; theorem for X, f st f is_convex_on X holds f is_strictly_quasiconvex_on X proof let X,f such that A1: f is_convex_on X; A2: for p being Real st 0

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 for X, f st f is_strongly_quasiconvex_on X holds f is_strictly_quasiconvex_on X; theorem for X, f st f is_strictly_quasiconvex_on X & f is one-to-one holds f is_strongly_quasiconvex_on X by FUNCT_1:def 4;