:: 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-2012 Association of Mizar Users begin theorem Th1: :: RFUNCT_4:1 for a, b being real number holds max (a,b) >= min (a,b) proofend; theorem Th2: :: RFUNCT_4:2 for n being Element of NAT for R1, R2 being Element of n -tuples_on REAL for r1, r2 being Real holds mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>)) = (mlt (R1,R2)) ^ <*(r1 * r2)*> proofend; theorem Th3: :: RFUNCT_4:3 for n being Element of NAT for 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 proofend; theorem Th4: :: RFUNCT_4:4 for n being Element of NAT for 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 proofend; theorem Th5: :: RFUNCT_4:5 for n being Element of NAT for R being Element of n -tuples_on REAL holds mlt ((n |-> 0),R) = n |-> 0 proofend; begin definition let f be PartFunc of REAL,REAL; let X be set ; predf is_strictly_convex_on X means :Def1: :: RFUNCT_4:def 1 ( 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; :: deftheorem Def1 defines is_strictly_convex_on RFUNCT_4:def_1_:_ for f being PartFunc of REAL,REAL for X being set holds ( f is_strictly_convex_on X iff ( 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)) ) ) ); theorem :: RFUNCT_4:6 for f being PartFunc of REAL,REAL for X being set st f is_strictly_convex_on X holds f is_convex_on X proofend; theorem :: RFUNCT_4:7 for a, b being Real for f being PartFunc of REAL,REAL holds ( f is_strictly_convex_on [.a,b.] iff ( [.a,b.] c= dom f & ( for p being Real st 0 < p & p < 1 holds for r, s being 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)) ) ) ) proofend; theorem :: RFUNCT_4:8 for X being set for 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)) ) ) ) proofend; theorem :: RFUNCT_4:9 for X being set for 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)) ) ) ) proofend; theorem :: RFUNCT_4:10 for f being PartFunc of REAL,REAL for X, Y being set st f is_strictly_convex_on X & Y c= X holds f is_strictly_convex_on Y proofend; Lm1: for r being Real for f being PartFunc of REAL,REAL for X being set st f is_strictly_convex_on X holds f - r is_strictly_convex_on X proofend; theorem :: RFUNCT_4:11 for r being Real for f being PartFunc of REAL,REAL for X being set holds ( f is_strictly_convex_on X iff f - r is_strictly_convex_on X ) proofend; Lm2: for r being Real for f being PartFunc of REAL,REAL for X being set st 0 < r & f is_strictly_convex_on X holds r (#) f is_strictly_convex_on X proofend; theorem Th12: :: RFUNCT_4:12 for r being Real for f being PartFunc of REAL,REAL for X being set st 0 < r holds ( f is_strictly_convex_on X iff r (#) f is_strictly_convex_on X ) proofend; theorem Th13: :: RFUNCT_4:13 for f, g being PartFunc of REAL,REAL for X being set st f is_strictly_convex_on X & g is_strictly_convex_on X holds f + g is_strictly_convex_on X proofend; theorem Th14: :: RFUNCT_4:14 for f, g being PartFunc of REAL,REAL for X being set st f is_strictly_convex_on X & g is_convex_on X holds f + g is_strictly_convex_on X proofend; theorem :: RFUNCT_4:15 for a, b being Real for f, g being PartFunc of REAL,REAL for X being set st f is_strictly_convex_on X & g is_strictly_convex_on X & ( ( a > 0 & b >= 0 ) or ( a >= 0 & b > 0 ) ) holds (a (#) f) + (b (#) g) is_strictly_convex_on X proofend; theorem Th16: :: RFUNCT_4:16 for f being PartFunc of REAL,REAL for X being set holds ( f is_convex_on X iff ( X c= dom f & ( for a, b, r being Real 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) ) ) ) ) proofend; theorem :: RFUNCT_4:17 for f being PartFunc of REAL,REAL for X being set holds ( f is_strictly_convex_on X iff ( X c= dom f & ( for a, b, r being Real 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) ) ) ) ) proofend; :: 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 for 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)) ) iff f is_convex_on REAL ) proofend; theorem :: RFUNCT_4:19 for f being PartFunc of REAL,REAL for I being Interval for 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 proofend; begin definition let f be PartFunc of REAL,REAL; let X be set ; predf is_quasiconvex_on X means :Def2: :: RFUNCT_4:def 2 ( 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; :: deftheorem Def2 defines is_quasiconvex_on RFUNCT_4:def_2_:_ for f being PartFunc of REAL,REAL for X being set holds ( f is_quasiconvex_on X iff ( 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)) ) ) ); definition let f be PartFunc of REAL,REAL; let X be set ; predf is_strictly_quasiconvex_on X means :Def3: :: RFUNCT_4:def 3 ( 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; :: deftheorem Def3 defines is_strictly_quasiconvex_on RFUNCT_4:def_3_:_ for f being PartFunc of REAL,REAL for X being set holds ( f is_strictly_quasiconvex_on X iff ( 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)) ) ) ); definition let f be PartFunc of REAL,REAL; let X be set ; predf is_strongly_quasiconvex_on X means :Def4: :: RFUNCT_4:def 4 ( 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; :: deftheorem Def4 defines is_strongly_quasiconvex_on RFUNCT_4:def_4_:_ for f being PartFunc of REAL,REAL for X being set holds ( f is_strongly_quasiconvex_on X iff ( 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)) ) ) ); definition let f be PartFunc of REAL,REAL; let x0 be real number ; predf is_upper_semicontinuous_in x0 means :Def5: :: RFUNCT_4:def 5 ( x0 in dom f & ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds (f . x0) - (f . x) < r ) ) ) ); end; :: deftheorem Def5 defines is_upper_semicontinuous_in RFUNCT_4:def_5_:_ for f being PartFunc of REAL,REAL for x0 being real number holds ( f is_upper_semicontinuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds (f . x0) - (f . x) < r ) ) ) ) ); definition let f be PartFunc of REAL,REAL; let X be set ; predf is_upper_semicontinuous_on X means :Def6: :: RFUNCT_4:def 6 ( X c= dom f & ( for x0 being Real st x0 in X holds f | X is_upper_semicontinuous_in x0 ) ); end; :: deftheorem Def6 defines is_upper_semicontinuous_on RFUNCT_4:def_6_:_ for f being PartFunc of REAL,REAL for X being set holds ( f is_upper_semicontinuous_on X iff ( X c= dom f & ( for x0 being Real st x0 in X holds f | X is_upper_semicontinuous_in x0 ) ) ); definition let f be PartFunc of REAL,REAL; let x0 be real number ; predf is_lower_semicontinuous_in x0 means :Def7: :: RFUNCT_4:def 7 ( x0 in dom f & ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds (f . x) - (f . x0) < r ) ) ) ); end; :: deftheorem Def7 defines is_lower_semicontinuous_in RFUNCT_4:def_7_:_ for f being PartFunc of REAL,REAL for x0 being real number holds ( f is_lower_semicontinuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds (f . x) - (f . x0) < r ) ) ) ) ); definition let f be PartFunc of REAL,REAL; let X be set ; predf is_lower_semicontinuous_on X means :Def8: :: RFUNCT_4:def 8 ( X c= dom f & ( for x0 being Real st x0 in X holds f | X is_lower_semicontinuous_in x0 ) ); end; :: deftheorem Def8 defines is_lower_semicontinuous_on RFUNCT_4:def_8_:_ for f being PartFunc of REAL,REAL for X being set holds ( f is_lower_semicontinuous_on X iff ( X c= dom f & ( for x0 being Real st x0 in X holds f | X is_lower_semicontinuous_in x0 ) ) ); theorem Th20: :: RFUNCT_4:20 for x0 being real number for f being PartFunc of REAL,REAL st x0 in dom f holds ( ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 ) iff f is_continuous_in x0 ) proofend; theorem :: RFUNCT_4:21 for X being set for f being PartFunc of REAL,REAL st X c= dom f holds ( ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) iff f | X is continuous ) proofend; theorem :: RFUNCT_4:22 for X being set for f being PartFunc of REAL,REAL st f is_strictly_convex_on X holds f is_strongly_quasiconvex_on X proofend; theorem :: RFUNCT_4:23 for X being set for f being PartFunc of REAL,REAL st f is_strongly_quasiconvex_on X holds f is_quasiconvex_on X proofend; theorem :: RFUNCT_4:24 for X being set for f being PartFunc of REAL,REAL st f is_convex_on X holds f is_strictly_quasiconvex_on X proofend; theorem :: RFUNCT_4:25 for X being set for f being PartFunc of REAL,REAL st f is_strongly_quasiconvex_on X holds f is_strictly_quasiconvex_on X proofend; theorem :: RFUNCT_4:26 for X being set for f being PartFunc of REAL,REAL st f is_strictly_quasiconvex_on X & f is one-to-one holds f is_strongly_quasiconvex_on X proofend;