:: 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

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;