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 A3: ( 0 <= p & 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 A4: p = 0 ; :: thesis: f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2))

then ( p * x1 = 0. X & (1 - p) * x2 = x2 ) by RLVECT_1:23, RLVECT_1:def 9;
then A5: (p * x1) + ((1 - p) * x2) = x2 by RLVECT_1:10;
R_EAL p = 0. by A4;
then A6: (R_EAL p) * (f . x1) = 0. ;
(R_EAL (1 - p)) * (f . x2) = f . x2 by A4, XXREAL_3:92;
hence f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by A5, A6, XXREAL_3:4; :: thesis: verum

end;

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

then ( p * x1 = x1 & (1 - p) * x2 = 0. X ) by RLVECT_1:23, RLVECT_1:def 9;
then A8: (p * x1) + ((1 - p) * x2) = x1 by RLVECT_1:10;
R_EAL (1 - p) = 0. by A7;
then A9: (R_EAL (1 - p)) * (f . x2) = 0. ;
(R_EAL p) * (f . x1) = f . x1 by A7, XXREAL_3:92;
hence f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by A8, A9, XXREAL_3:4; :: thesis: verum

end;

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

then ( 0 < p & p < 1 ) by A3, XXREAL_0:1;
hence f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by A1, A2, 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