The abstract of the Mizar article:

Introduction to Several Concepts of Convexity and Semicontinuity for Function from $\Bbb R$ to $\Bbb R$

by

Noboru Endou,

Katsumi Wasaki, and

Yasunari Shidama

Received March 23, 2000

MML identifier: RFUNCT_4

[ Mizar article, MML identifier index ]

environ

 vocabulary PARTFUN1, ARYTM, SQUARE_1, FINSEQ_2, RVSUM_1, FINSEQ_1, VECTSP_1,
      RELAT_1, FUNCT_1, ARYTM_1, RLVECT_1, RFUNCT_3, RCOMP_1, ARYTM_3, SEQ_1,
      BOOLE, MEASURE5, FCONT_1, SUPINF_1, ABSVALUE, RFUNCT_4;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XCMPLX_0, XREAL_0, RELAT_1,
      FUNCT_1, FINSEQ_1, REAL_1, NAT_1, ABSVALUE, FINSEQ_2, SQUARE_1, PARTFUN1,
      FINSEQOP, VECTSP_1, SEQ_1, RVSUM_1, RCOMP_1, RFUNCT_3, SUPINF_1,
      MEASURE5, FCONT_1;
 constructors MONOID_1, REAL_1, NAT_1, FINSEQOP, RCOMP_1, TOPREAL1, FINSEQ_4,
      RFUNCT_3, MEASURE5, FCONT_1, MEMBERED;
 clusters RELSET_1, FINSEQ_2, XREAL_0, ARYTM_3, MEMBERED;
 requirements NUMERALS, SUBSET, REAL, BOOLE, ARITHM;


begin :: Some useful properties of n-tuples_on REAL

reserve a,b,r,s,x0,x for Real;
reserve f,g for PartFunc of REAL,REAL;
reserve X,Y for set;
reserve k for Nat;

theorem :: RFUNCT_4:1
for a, b being real number 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 Nat st i in dom R holds 0 <= R.i) holds
for i being 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 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<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;

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<p & p<1 holds
for r,s be 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;

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 &
a<b & b<c holds f.b <=((c-b)/(c-a))*f.a + ((b-a)/(c-a))*f.c;

theorem :: RFUNCT_4:9
  for X being set, 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;

theorem :: RFUNCT_4:10
  f is_strictly_convex_on X & Y c= X implies f is_strictly_convex_on Y;

theorem :: RFUNCT_4:11
  f is_strictly_convex_on X iff f-r is_strictly_convex_on X;

theorem :: RFUNCT_4:12
0<r implies (f is_strictly_convex_on X iff r(#)f is_strictly_convex_on X);

theorem :: RFUNCT_4:13
f is_strictly_convex_on X & g is_strictly_convex_on X implies
f+g is_strictly_convex_on X;

theorem :: RFUNCT_4:14
f is_strictly_convex_on X & g is_convex_on X implies
f+g is_strictly_convex_on X;

theorem :: RFUNCT_4:15
  f is_strictly_convex_on X & g is_strictly_convex_on X &
((a>0 & 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 Nat, P,E,F being Element of n-tuples_on REAL st Sum P=1 &
(for i being 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;

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

definition
let f, X;
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;

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

definition let f; let x0 be real number;
pred f is_upper_semicontinuous_in x0 means
:: RFUNCT_4:def 5
x0 in dom f &
(for r st 0<r ex s st 0<s & for x st
 x in dom f & abs(x-x0)<s holds f.x0-f.x<r);
end;

definition let f,X;
pred f is_upper_semicontinuous_on X means
:: RFUNCT_4:def 6
X c= dom f & for x0 st x0 in X holds f|X is_upper_semicontinuous_in x0;
end;

definition let f; let x0 be real number;
pred f is_lower_semicontinuous_in x0 means
:: RFUNCT_4:def 7
x0 in dom f &
 (for r st 0<r ex s st 0<s &
  for x st x in dom f & abs(x-x0)<s holds f.x-f.x0<r);
end;

definition let f,X;
pred f is_lower_semicontinuous_on X means
:: RFUNCT_4:def 8
X c= dom f & for x0 st x0 in X holds f|X is_lower_semicontinuous_in x0;
end;

theorem :: RFUNCT_4:20
for x0 be real number, f holds
f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0
iff f is_continuous_in x0;

theorem :: RFUNCT_4:21
  for X, f holds
f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X
iff f is_continuous_on X;

theorem :: RFUNCT_4:22
  for X, f st f is_strictly_convex_on X holds f is_strongly_quasiconvex_on X;

theorem :: RFUNCT_4:23
  for X, f st f is_strongly_quasiconvex_on X holds f is_quasiconvex_on X;

theorem :: RFUNCT_4:24
  for X, f st f is_convex_on X holds f is_strictly_quasiconvex_on X;

theorem :: RFUNCT_4:25
  for X, f st f is_strongly_quasiconvex_on X holds
f is_strictly_quasiconvex_on X;

theorem :: RFUNCT_4:26
  for X, f st f is_strictly_quasiconvex_on X & f is one-to-one holds
f is_strongly_quasiconvex_on X;