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)) <= (p * (f . x1)) + ((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)) <= (p * (f . x1)) + ((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)) <= (p * (f . x1)) + ((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)) <= (p * (f . x1)) + ((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)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) ) implies f is convex )

for p being Real st 0 <= p & p <= 1 holds

f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((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)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) ;

hence f is convex by A1, Th4; :: thesis: verum

( 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)) <= (p * (f . x1)) + ((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)) <= (p * (f . x1)) + ((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)) <= (p * (f . x1)) + ((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)) <= (p * (f . x1)) + ((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)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) ) implies f is convex )

proof

assume
for x1, x2 being VECTOR of X
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)) <= (p * (f . x1)) + ((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)) <= (p * (f . x1)) + ((1 - p) * (f . x2))

let p be Real; :: thesis: ( 0 <= p & p <= 1 implies f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) )

assume that

A3: 0 <= p and

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

end;for p being Real st 0 <= p & p <= 1 holds

f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((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)) <= (p * (f . x1)) + ((1 - p) * (f . x2))

let p be Real; :: thesis: ( 0 <= p & p <= 1 implies f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) )

assume that

A3: 0 <= p and

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

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

end;

suppose A5:
p = 0
; :: thesis: f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((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;

A8: (1 - p) * (f . x2) = f . x2 by A5, XXREAL_3:81;

p * (f . x1) = 0. by A5;

hence f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) by A7, A8, XXREAL_3:4; :: thesis: verum

end;p * x1 = 0. X by A5, RLVECT_1:10;

then A7: (p * x1) + ((1 - p) * x2) = x2 by A6;

A8: (1 - p) * (f . x2) = f . x2 by A5, XXREAL_3:81;

p * (f . x1) = 0. by A5;

hence f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) by A7, A8, XXREAL_3:4; :: thesis: verum

suppose A9:
p = 1
; :: thesis: f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((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;

A12: p * (f . x1) = f . x1 by A9, XXREAL_3:81;

(1 - p) * (f . x2) = 0. by A9;

hence f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) by A11, A12, XXREAL_3:4; :: thesis: verum

end;p * x1 = x1 by A9, RLVECT_1:def 8;

then A11: (p * x1) + ((1 - p) * x2) = x1 by A10;

A12: p * (f . x1) = f . x1 by A9, XXREAL_3:81;

(1 - p) * (f . x2) = 0. by A9;

hence f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) by A11, A12, XXREAL_3:4; :: thesis: verum

for p being Real st 0 <= p & p <= 1 holds

f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((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)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) ;

hence f is convex by A1, Th4; :: thesis: verum