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 A4, XREAL_1:50;

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 A1, XXREAL_0:14;

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 (Prod_of_RLS (X,RLS_Real)) ;
reconsider u2 = [x2,w2] as VECTOR of (Prod_of_RLS (X,RLS_Real)) ;
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 A2, A3, A4, A7, CONVEX1:def 2;
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 A10, XTUPLE_0:1;
x0 = (p * x1) + ((1 - p) * x2) by A10, XTUPLE_0:1;
hence f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) by A11, A12, Lm12; :: 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 A13, XREAL_0:def 1;
p * (f . x1) = +infty by A3, A13, XXREAL_3:def 5;
then (p * (f . x1)) + ((1 - p) * (f . x2)) = +infty by A14, XXREAL_3:def 2;
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 A15, XREAL_0:def 1;
(1 - p) * (f . x2) = +infty by A5, A15, XXREAL_3:def 5;
then (p * (f . x1)) + ((1 - p) * (f . x2)) = +infty by A16, XXREAL_3:def 2;
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 A5, XXREAL_3:def 5;
then (p * (f . x1)) + ((1 - p) * (f . x2)) = +infty by A3, A17, XXREAL_3:def 2;
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 (Prod_of_RLS (X,RLS_Real))
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 (Prod_of_RLS (X,RLS_Real)); :: 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 A23, Lm1;
f . x2 <> +infty by A24, XXREAL_0:9;
then reconsider w2 = f . x2 as Element of REAL by A1, XXREAL_0:14;
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 A27, XXREAL_0:9;
then reconsider w1 = f . x1 as Element of REAL by A1, XXREAL_0:14;
1 - p > 0 by A20, XREAL_1:50;
then (1 - p) * w2 <= (1 - p) * y2 by A24, XREAL_1:64;
then A28: (p * w1) + ((1 - p) * w2) <= (p * w1) + ((1 - p) * y2) by XREAL_1:6;
p * w1 <= p * y1 by A19, A27, XREAL_1:64;
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 A28, XXREAL_0:2;
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 A18, A19, A20, XXREAL_0:9, A30;
then reconsider w = f . ((p * x1) + ((1 - p) * x2)) as Element of REAL by A1, XXREAL_0:14;
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 A29, XXREAL_0:2;
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 A26, Lm1;
then (p * u1) + ((1 - p) * u2) = [((p * x1) + ((1 - p) * x2)),((p * y1) + ((1 - p) * y2))] by A25, Lm2;
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