:: 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-2021 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; begin reserve a,b,p,r,r1,r2,s,s1,s2,x0,x for Real; reserve f,g for PartFunc of REAL,REAL; reserve X,Y for set; theorem :: RFUNCT_4:1 for a, b being Real holds max(a,b) >= min(a,b); theorem :: RFUNCT_4:2 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*>; theorem :: RFUNCT_4:3 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; theorem :: RFUNCT_4:4 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); theorem :: RFUNCT_4:5 for n being Nat, R being Element of n-tuples_on REAL holds mlt(n |-> (0 qua Real),R) = n |-> (0 qua Real); begin :: Convex and strictly convex functions definition let f, X; pred f is_strictly_convex_on X means :: RFUNCT_4:def 1 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 :: RFUNCT_4:6 f is_strictly_convex_on X implies f is_convex_on X; theorem :: RFUNCT_4:7 for a,b be Real, f be PartFunc of REAL,REAL holds f is_strictly_convex_on [.a,b.] iff [.a,b.] c= dom f & for p be Real st 0

s holds f.(p*r+(1-p )*s) < p*f.r + (1-p)*f.s; theorem :: RFUNCT_4:8 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 & a0 & b>=0 or a>=0 & b>0 ) implies a(#)f+b(#)g is_strictly_convex_on X; theorem :: RFUNCT_4:16 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); theorem :: RFUNCT_4:17 f is_strictly_convex_on X iff X c= dom f & for a,b,r st a in X & b in X & r in X & a < r & r < b holds (f.r-f.a)/(r-a) < (f.b-f.a)/(b-a) & (f.b-f.a)/ (b-a) < (f.b-f.r)/(b-r); :: Jensen's Inequality theorem :: RFUNCT_4:18 for f being PartFunc of REAL,REAL st f is total holds (for n being Element of NAT, P,E,F being Element of n-tuples_on REAL st Sum P=1 & (for i being Element of NAT st i in dom P holds P.i >=0 & F.i=f.(E.i)) holds f.Sum(mlt (P,E))<=Sum(mlt(P,F))) implies f is_convex_on REAL; theorem :: RFUNCT_4:19 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))); theorem :: RFUNCT_4:20 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; begin :: Definitions of several convexity and semicontinuity concepts definition let f, X; pred f is_quasiconvex_on X means :: RFUNCT_4:def 2 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 :: RFUNCT_4:def 4 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 :: RFUNCT_4:def 5 x0 in dom f & for r st 0