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)) <= ((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 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))
then A2: epigraph f is convex by Def7;
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))
set p2 = R_EAL (1 - p);
set p1 = R_EAL p;
A5: 1 - p > 0 by A4, XREAL_1:52;

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

then reconsider w2 = f . x2 as Real ;
reconsider w1 = f . x1 as 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 ) ;
f . x2 <= R_EAL w2 ;
then 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;
f . x1 <= R_EAL w1 ;
then [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 <= R_EAL y0 ;
A12: y0 = (p * w1) + ((1 - p) * w2) by A10, ZFMISC_1:33;
x0 = (p * x1) + ((1 - p) * x2) by A10, ZFMISC_1:33;
hence f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by A11, A12, Lm15; :: thesis: verum

end;

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

A14: (R_EAL (1 - p)) * (f . x2) in REAL

proof

reconsider w2 = f . x2 as Real by A13;
(R_EAL (1 - p)) * (f . x2) = (1 - p) * w2 by EXTREAL1:13;
hence (R_EAL (1 - p)) * (f . x2) in REAL ; :: thesis: verum

end;

(R_EAL p) * (f . x1) = +infty by A3, A13, XXREAL_3:def 5;
then ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) = +infty by A14, XXREAL_3:def 2;
hence f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (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)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2))

A16: (R_EAL p) * (f . x1) in REAL

proof

reconsider w1 = f . x1 as Real by A15;
(R_EAL p) * (f . x1) = p * w1 by EXTREAL1:13;
hence (R_EAL p) * (f . x1) in REAL ; :: thesis: verum

end;

(R_EAL (1 - p)) * (f . x2) = +infty by A5, A15, XXREAL_3:def 5;
then ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) = +infty by A16, XXREAL_3:def 2;
hence f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (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)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2))

then (R_EAL (1 - p)) * (f . x2) = +infty by A5, XXREAL_3:def 5;
then ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) = +infty by A3, A17, XXREAL_3:def 2;
hence f . ((p * x1) + ((1 - p) * x2)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (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)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (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
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 <= R_EAL 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 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 <= R_EAL y1 by A21;
f . x1 <> +infty by A27, XXREAL_0:9;
then reconsider w1 = f . x1 as Real by A1, XXREAL_0:14;
1 - p > 0 by A20, XREAL_1:52;
then (1 - p) * w2 <= (1 - p) * y2 by A24, XREAL_1:66;
then A28: (p * w1) + ((1 - p) * w2) <= (p * w1) + ((1 - p) * y2) by XREAL_1:8;
p * w1 <= p * y1 by A19, A27, XREAL_1:66;
then (p * w1) + ((1 - p) * y2) <= (p * y1) + ((1 - p) * y2) by XREAL_1:8;
then A29: (p * w1) + ((1 - p) * w2) <= (p * y1) + ((1 - p) * y2) by A28, XXREAL_0:2;
A30: R_EAL ((p * w1) + ((1 - p) * w2)) = ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) by Lm15;
then f . ((p * x1) + ((1 - p) * x2)) <> +infty by A18, A19, A20, XXREAL_0:9;
then reconsider w = f . ((p * x1) + ((1 - p) * x2)) as Real by A1, XXREAL_0:14;
w <= (p * w1) + ((1 - p) * w2) by A18, A19, A20, A30;
then f . ((p * x1) + ((1 - p) * x2)) <= R_EAL ((p * y1) + ((1 - p) * y2)) by A29, XXREAL_0:2;
then A31: [((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 <= R_EAL y } ;
p * u1 = [(p * x1),(p * y1)] by A26, Lm1;
hence (p * u1) + ((1 - p) * u2) in epigraph f by A31, A25, Lm2; :: thesis: verum

end;

end;

then epigraph f is convex by CONVEX1:def 2;
hence f is convex by Def7; :: thesis: verum