let X be RealLinearSpace; :: thesis: for f being Function of the carrier of X,ExtREAL st ( for x being VECTOR of X holds f . x <> -infty ) holds
( f is convex iff for x1, x2 being VECTOR of X
for p being Real st 0 <= p & p <= 1 holds
f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) )
let f be Function of the carrier of X,ExtREAL; :: thesis: ( ( for x being VECTOR of X holds f . x <> -infty ) implies ( f is convex iff for x1, x2 being VECTOR of X
for p being Real st 0 <= p & p <= 1 holds
f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) ) )
assume A1: for x being VECTOR of X holds f . x <> -infty ; :: thesis: ( f is convex iff for x1, x2 being VECTOR of X
for p being Real st 0 <= p & p <= 1 holds
f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) )
thus ( f is convex implies for x1, x2 being VECTOR of X
for p being Real st 0 <= p & p <= 1 holds
f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) ) :: thesis: ( ( for x1, x2 being VECTOR of X
for p being Real st 0 <= p & p <= 1 holds
f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) ) implies f is convex )

proof

assume A2: f is convex ; :: thesis: for x1, x2 being VECTOR of X
for p being Real st 0 <= p & p <= 1 holds
f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2))
let x1, x2 be VECTOR of X; :: thesis: for p being Real st 0 <= p & p <= 1 holds
f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2))
let p be Real; :: thesis: ( 0 <= p & p <= 1 implies f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) )
assume that
A3: 0 <= p and
A4: p <= 1 ; :: thesis: f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2))

per cases ( p = 0 or p = 1 or ( p <> 0 & p <> 1 ) ) ;

suppose A5: p = 0 ; :: thesis: f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2))

then A6: (1 - p) * x2 = x2 by RLVECT_1:def 8;
p * x1 = 0. X by A5, RLVECT_1:10;
then A7: (p * x1) + ((1 - p) * x2) = x2 by A6, RLVECT_1:4;
A8: (R_EAL (1 - p)) * (f . x2) = f . x2 by A5, XXREAL_3:81;
(R_EAL p) * (f . x1) = 0. by A5;
hence f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by A7, A8, XXREAL_3:4; :: thesis: verum

end;

suppose A9: p = 1 ; :: thesis: f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2))

then A10: (1 - p) * x2 = 0. X by RLVECT_1:10;
p * x1 = x1 by A9, RLVECT_1:def 8;
then A11: (p * x1) + ((1 - p) * x2) = x1 by A10, RLVECT_1:4;
A12: (R_EAL p) * (f . x1) = f . x1 by A9, XXREAL_3:81;
(R_EAL (1 - p)) * (f . x2) = 0. by A9;
hence f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by A11, A12, XXREAL_3:4; :: thesis: verum

end;

suppose A13: ( p <> 0 & p <> 1 ) ; :: thesis: f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2))

then p < 1 by A4, XXREAL_0:1;
hence f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by A1, A2, A3, A13, Th9; :: thesis: verum

end;

end;

end;

assume for x1, x2 being VECTOR of X
for p being Real st 0 <= p & p <= 1 holds
f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) ; :: thesis: f is convex
then for x1, x2 being VECTOR of X
for p being Real st 0 < p & p < 1 holds
f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) ;
hence f is convex by A1, Th9; :: thesis: verum