:: Introduction to Several Concepts of Convexity and Semicontinuity for Function from REAL to REAL
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Copyright (c) 2000-2021 Association of Mizar Users

theorem Th1: :: RFUNCT_4:1
for a, b being Real holds max (a,b) >= min (a,b)
proof end;

theorem Th2: :: RFUNCT_4:2
for n being 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)*>
proof end;

theorem Th3: :: RFUNCT_4:3
for n being 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
proof end;

theorem Th4: :: RFUNCT_4:4
for n being 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
proof end;

theorem Th5: :: RFUNCT_4:5
for n being Nat
for R being Element of n -tuples_on REAL holds mlt ((n |-> 0),R) = n |-> 0
proof end;

definition
let f be PartFunc of REAL,REAL;
let X be set ;
pred f is_strictly_convex_on X means :: 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 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
proof end;

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)) ) ) )
proof end;

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)) ) ) )
proof end;

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)) ) ) )
proof end;

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 by XBOOLE_1:1;

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

proof end;

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 )
proof end;

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

proof end;

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 )
proof end;

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
proof end;

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
proof end;

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
proof end;

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) ) ) ) )
proof end;

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) ) ) ) )
proof end;

:: Jensen's Inequality
theorem :: RFUNCT_4:18
for f being PartFunc of REAL,REAL st f is total & ( 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)) ) holds
f is_convex_on REAL
proof end;

theorem :: RFUNCT_4:19
for f being PartFunc of REAL,REAL st f is_convex_on REAL 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))
proof end;

theorem :: RFUNCT_4:20
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
proof end;

definition
let f be PartFunc of REAL,REAL;
let X be set ;
pred f is_quasiconvex_on X means :: 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 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 ;
pred f is_strictly_quasiconvex_on X means :: 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 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 ;
pred f is_strongly_quasiconvex_on X means :: 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 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;
pred f is_upper_semicontinuous_in x0 means :: 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 & |.(x - x0).| < s holds
(f . x0) - (f . x) < r ) ) ) );
end;

:: deftheorem defines is_upper_semicontinuous_in RFUNCT_4:def 5 :
for f being PartFunc of REAL,REAL
for x0 being Real 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 & |.(x - x0).| < s holds
(f . x0) - (f . x) < r ) ) ) ) );

definition
let f be PartFunc of REAL,REAL;
let X be set ;
pred f is_upper_semicontinuous_on X means :: 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 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;
pred f is_lower_semicontinuous_in x0 means :: 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 & |.(x - x0).| < s holds
(f . x) - (f . x0) < r ) ) ) );
end;

:: deftheorem defines is_lower_semicontinuous_in RFUNCT_4:def 7 :
for f being PartFunc of REAL,REAL
for x0 being Real 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 & |.(x - x0).| < s holds
(f . x) - (f . x0) < r ) ) ) ) );

definition
let f be PartFunc of REAL,REAL;
let X be set ;
pred f is_lower_semicontinuous_on X means :: 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 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 Th21: :: RFUNCT_4:21
for x0 being Real
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 )
proof end;

theorem :: RFUNCT_4:22
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 )
proof end;

theorem :: RFUNCT_4:23
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
proof end;

theorem :: RFUNCT_4:24
for X being set
for f being PartFunc of REAL,REAL st f is_strongly_quasiconvex_on X holds
f is_quasiconvex_on X
proof end;

theorem :: RFUNCT_4:25
for X being set
for f being PartFunc of REAL,REAL st f is_convex_on X holds
f is_strictly_quasiconvex_on X
proof end;

theorem :: RFUNCT_4:26
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 ;

theorem :: RFUNCT_4:27
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 by FUNCT_1:def 4;