:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama

::

:: Received March 23, 2000

:: Copyright (c) 2000-2017 Association of Mizar Users

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)*>

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

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

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;

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

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

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

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

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

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;

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 )

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 )

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

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

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

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

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

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

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

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

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;

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

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

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

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

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

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

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

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 ;

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

( X c= dom f & ( for x0 being Real st x0 in X holds

f | X is_upper_semicontinuous_in x0 ) );

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

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

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

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 ;

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

( X c= dom f & ( for x0 being Real st x0 in X holds

f | X is_lower_semicontinuous_in x0 ) );

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

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 )

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 )

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

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

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

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 ;

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;

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;