let X be set ; for f being PartFunc of REAL ,REAL st f is_strictly_convex_on X holds
f is_strongly_quasiconvex_on X
let f be PartFunc of REAL ,REAL ; ( f is_strictly_convex_on X implies f is_strongly_quasiconvex_on X )
assume A1:
f is_strictly_convex_on X
; f is_strongly_quasiconvex_on X
A2:
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)
proof
let p be
Real;
( 0 < p & p < 1 implies 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) )
assume that A3:
0 < p
and A4:
p < 1
;
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
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)
proof
let r,
s be
Real;
( r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s implies f . ((p * r) + ((1 - p) * s)) < max (f . r),(f . s) )
1
- p > 0
by A4, XREAL_1:52;
then A5:
(1 - p) * (f . s) <= (1 - p) * (max (f . r),(f . s))
by XREAL_1:66, XXREAL_0:25;
assume
(
r in X &
s in X &
(p * r) + ((1 - p) * s) in X &
r <> s )
;
f . ((p * r) + ((1 - p) * s)) < max (f . r),(f . s)
then A6:
f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s))
by A1, A3, A4, Def1;
p * (f . r) <= p * (max (f . r),(f . s))
by A3, XREAL_1:66, XXREAL_0:25;
then
(p * (f . r)) + ((1 - p) * (f . s)) <= (p * (max (f . r),(f . s))) + ((1 - p) * (max (f . r),(f . s)))
by A5, XREAL_1:9;
hence
f . ((p * r) + ((1 - p) * s)) < max (f . r),
(f . s)
by A6, XXREAL_0:2;
verum
end;
hence
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)
;
verum
end;
X c= dom f
by A1, Def1;
hence
f is_strongly_quasiconvex_on X
by A2, Def4; verum