let X be non empty RLSStruct ; :: 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 )
proof
assume 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))

then A2: epigraph f is convex ;
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))
set p2 = 1 - p;
set p1 = p;
A5: 1 - p > 0 by ;
per cases ( ( f . x1 in REAL & f . x2 in REAL ) or ( f . x1 = +infty & f . x2 in REAL ) or ( f . x1 in REAL & f . x2 = +infty ) or ( f . x1 = +infty & f . x2 = +infty ) ) by ;
suppose A6: ( f . x1 in REAL & f . x2 in REAL ) ; :: thesis: f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2))
then reconsider w2 = f . x2 as Element of REAL ;
reconsider w1 = f . x1 as Element of REAL by A6;
reconsider u1 = [x1,w1] as VECTOR of () ;
reconsider u2 = [x2,w2] as VECTOR of () ;
A7: [x2,w2] in epigraph f ;
A8: p * u1 = [(p * x1),(p * w1)] by Lm1;
A9: (1 - p) * u2 = [((1 - p) * x2),((1 - p) * w2)] by Lm1;
[x1,w1] in epigraph f ;
then (p * u1) + ((1 - p) * u2) in epigraph f by ;
then [((p * x1) + ((1 - p) * x2)),((p * w1) + ((1 - p) * w2))] in epigraph f by A8, A9, Lm2;
then consider x0 being Element of X, y0 being Element of REAL such that
A10: [((p * x1) + ((1 - p) * x2)),((p * w1) + ((1 - p) * w2))] = [x0,y0] and
A11: f . x0 <= y0 ;
A12: y0 = (p * w1) + ((1 - p) * w2) by ;
x0 = (p * x1) + ((1 - p) * x2) by ;
hence f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) by ; :: thesis: verum
end;
suppose A13: ( f . x1 = +infty & f . x2 in REAL ) ; :: thesis: f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2))
A14: (1 - p) * (f . x2) in REAL by ;
p * (f . x1) = +infty by ;
then (p * (f . x1)) + ((1 - p) * (f . x2)) = +infty by ;
hence f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) by XXREAL_0:4; :: thesis: verum
end;
suppose A15: ( f . x1 in REAL & f . x2 = +infty ) ; :: thesis: f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2))
A16: p * (f . x1) in REAL by ;
(1 - p) * (f . x2) = +infty by ;
then (p * (f . x1)) + ((1 - p) * (f . x2)) = +infty by ;
hence f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) by XXREAL_0:4; :: thesis: verum
end;
suppose A17: ( f . x1 = +infty & f . x2 = +infty ) ; :: thesis: f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2))
then (1 - p) * (f . x2) = +infty by ;
then (p * (f . x1)) + ((1 - p) * (f . x2)) = +infty by ;
hence f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) by XXREAL_0:4; :: thesis: verum
end;
end;
end;
assume A18: 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: f is convex
for u1, u2 being VECTOR of ()
for p being Real st 0 < p & p < 1 & u1 in epigraph f & u2 in epigraph f holds
(p * u1) + ((1 - p) * u2) in epigraph f
proof
let u1, u2 be VECTOR of (); :: thesis: for p being Real st 0 < p & p < 1 & u1 in epigraph f & u2 in epigraph f holds
(p * u1) + ((1 - p) * u2) in epigraph f

let p be Real; :: thesis: ( 0 < p & p < 1 & u1 in epigraph f & u2 in epigraph f implies (p * u1) + ((1 - p) * u2) in epigraph f )
assume that
A19: 0 < p and
A20: p < 1 and
A21: u1 in epigraph f and
A22: u2 in epigraph f ; :: thesis: (p * u1) + ((1 - p) * u2) in epigraph f
reconsider pp = p as Real ;
thus (p * u1) + ((1 - p) * u2) in epigraph f :: thesis: verum
proof
consider x2 being Element of X, y2 being Element of REAL such that
A23: u2 = [x2,y2] and
A24: f . x2 <= y2 by A22;
A25: (1 - p) * u2 = [((1 - p) * x2),((1 - p) * y2)] by ;
f . x2 <> +infty by ;
then reconsider w2 = f . x2 as Element of REAL by ;
consider x1 being Element of X, y1 being Element of REAL such that
A26: u1 = [x1,y1] and
A27: f . x1 <= y1 by A21;
f . x1 <> +infty by ;
then reconsider w1 = f . x1 as Element of REAL by ;
1 - p > 0 by ;
then (1 - p) * w2 <= (1 - p) * y2 by ;
then A28: (p * w1) + ((1 - p) * w2) <= (p * w1) + ((1 - p) * y2) by XREAL_1:6;
p * w1 <= p * y1 by ;
then (p * w1) + ((1 - p) * y2) <= (p * y1) + ((1 - p) * y2) by XREAL_1:6;
then A29: (p * w1) + ((1 - p) * w2) <= (p * y1) + ((1 - p) * y2) by ;
A30: (p * w1) + ((1 - p) * w2) in REAL by XREAL_0:def 1;
A31: (p * w1) + ((1 - p) * w2) = (p * (f . x1)) + ((1 - p) * (f . x2)) by Lm12;
then f . ((pp * x1) + ((1 - pp) * x2)) <> +infty by ;
then reconsider w = f . ((p * x1) + ((1 - p) * x2)) as Element of REAL by ;
A32: (p * y1) + ((1 - p) * y2) in REAL by XREAL_0:def 1;
w <= (pp * w1) + ((1 - pp) * w2) by A18, A19, A20, A31;
then f . ((pp * x1) + ((1 - pp) * x2)) <= (p * y1) + ((1 - p) * y2) by ;
then A33: [((p * x1) + ((1 - p) * x2)),((p * y1) + ((1 - p) * y2))] in { [x,y] where x is Element of X, y is Element of REAL : f . x <= y } by A32;
p * u1 = [(p * x1),(p * y1)] by ;
then (p * u1) + ((1 - p) * u2) = [((p * x1) + ((1 - p) * x2)),((p * y1) + ((1 - p) * y2))] by ;
hence (p * u1) + ((1 - p) * u2) in epigraph f by A33; :: thesis: verum
end;
end;
then epigraph f is convex by CONVEX1:def 2;
hence f is convex ; :: thesis: verum