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:50;
then A5:
(1 - p) * (f . s) <= (1 - p) * (max ((f . r),(f . s)))
by XREAL_1:64, 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;
p * (f . r) <= p * (max ((f . r),(f . s)))
by A3, XREAL_1:64, 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:7;
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;
hence
f is_strongly_quasiconvex_on X
by A2; verum