let f be PartFunc of REAL,REAL; :: thesis: for g being Function of the carrier of RLS_Real,ExtREAL
for X being Subset of RLS_Real st X c= dom f & ( for x being Real holds
( ( x in X implies g . x = f . x ) & ( not x in X implies g . x = +infty ) ) ) holds
( g is convex iff ( f is_convex_on X & X is convex ) )
let g be Function of the carrier of RLS_Real,ExtREAL; :: thesis: for X being Subset of RLS_Real st X c= dom f & ( for x being Real holds
( ( x in X implies g . x = f . x ) & ( not x in X implies g . x = +infty ) ) ) holds
( g is convex iff ( f is_convex_on X & X is convex ) )
let X be Subset of RLS_Real; :: thesis: ( X c= dom f & ( for x being Real holds
( ( x in X implies g . x = f . x ) & ( not x in X implies g . x = +infty ) ) ) implies ( g is convex iff ( f is_convex_on X & X is convex ) ) )
assume that
A1: X c= dom f and
A2: for x being Real holds
( ( x in X implies g . x = f . x ) & ( not x in X implies g . x = +infty ) ) ; :: thesis: ( g is convex iff ( f is_convex_on X & X is convex ) )
A3: for v being VECTOR of RLS_Real holds g . v <> -infty

proof

let v be VECTOR of RLS_Real; :: thesis: g . v <> -infty
reconsider x = v as Real ;
f . x in REAL ;
hence g . v <> -infty by A2; :: thesis: verum

end;

A4: for v being VECTOR of RLS_Real st v in X holds
g . v in REAL

proof

let v be VECTOR of RLS_Real; :: thesis: ( v in X implies g . v in REAL )
reconsider x = v as Real ;
assume v in X ; :: thesis: g . v in REAL
then g . x = f . x by A2;
hence g . v in REAL ; :: thesis: verum

end;

thus ( g is convex implies ( f is_convex_on X & X is convex ) ) :: thesis: ( f is_convex_on X & X is convex implies g is convex )

proof

assume A5: g is convex ; :: thesis: ( f is_convex_on X & X is convex )
for p being Real st 0 <= p & p <= 1 holds
for x1, x2 being Real st x1 in X & x2 in X & (p * x1) + ((1 - p) * x2) in X holds
f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2))

proof

let p be Real; :: thesis: ( 0 <= p & p <= 1 implies for x1, x2 being Real st x1 in X & x2 in X & (p * x1) + ((1 - p) * x2) in X holds
f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) )
assume that
A6: 0 <= p and
A7: p <= 1 ; :: thesis: for x1, x2 being Real st x1 in X & x2 in X & (p * x1) + ((1 - p) * x2) in X holds
f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2))
let x1, x2 be Real; :: thesis: ( x1 in X & x2 in X & (p * x1) + ((1 - p) * x2) in X implies f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) )
assume that
A8: x1 in X and
A9: x2 in X and
A10: (p * x1) + ((1 - p) * x2) in X ; :: thesis: f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2))
A11: f . x1 = g . x1 by A2, A8;
A12: f . ((p * x1) + ((1 - p) * x2)) = g . ((p * x1) + ((1 - p) * x2)) by A2, A10;
A13: f . x2 = g . x2 by A2, A9;

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

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

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

end;

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

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

end;

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

reconsider v2 = x2 as VECTOR of RLS_Real ;
reconsider v1 = x1 as VECTOR of RLS_Real ;
A15: (1 - p) * v2 = (1 - p) * x2 by BINOP_2:def 11;
p * v1 = p * x1 by BINOP_2:def 11;
then A16: g . ((p * v1) + ((1 - p) * v2)) = f . ((p * x1) + ((1 - p) * x2)) by A12, A15, BINOP_2:def 9;
A17: p < 1 by A7, A14, XXREAL_0:1;
(p * (f . v1)) + ((1 - p) * (f . v2)) = ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by A11, A13, Lm12;
hence f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) by A3, A5, A6, A14, A17, A16, Th9; :: thesis: verum

end;

end;

end;

hence f is_convex_on X by A1, RFUNCT_3:def 12; :: thesis: X is convex
for v1, v2 being VECTOR of RLS_Real
for p being Real st 0 < p & p < 1 & v1 in X & v2 in X holds
(p * v1) + ((1 - p) * v2) in X

proof

let v1, v2 be VECTOR of RLS_Real; :: thesis: for p being Real st 0 < p & p < 1 & v1 in X & v2 in X holds
(p * v1) + ((1 - p) * v2) in X
let p be Real; :: thesis: ( 0 < p & p < 1 & v1 in X & v2 in X implies (p * v1) + ((1 - p) * v2) in X )
assume that
A18: 0 < p and
A19: p < 1 and
A20: v1 in X and
A21: v2 in X ; :: thesis: (p * v1) + ((1 - p) * v2) in X
reconsider w1 = g . v1, w2 = g . v2 as Real by A4, A20, A21;
A22: (p * w1) + ((1 - p) * w2) = ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by Lm12;
g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by A3, A5, A18, A19, Th9;
then g . ((p * v1) + ((1 - p) * v2)) <> +infty by A22, XXREAL_0:9;
hence (p * v1) + ((1 - p) * v2) in X by A2; :: thesis: verum

end;

hence X is convex by CONVEX1:def 2; :: thesis: verum

end;

thus ( f is_convex_on X & X is convex implies g is convex ) :: thesis: verum

proof

assume that
A23: f is_convex_on X and
A24: X is convex ; :: thesis: g is convex
for v1, v2 being VECTOR of RLS_Real
for p being Real st 0 < p & p < 1 holds
g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2))

proof

let v1, v2 be VECTOR of RLS_Real; :: thesis: for p being Real st 0 < p & p < 1 holds
g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2))
let p be Real; :: thesis: ( 0 < p & p < 1 implies g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) )
assume that
A25: 0 < p and
A26: p < 1 ; :: thesis: g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2))
reconsider x2 = v2 as Real ;
reconsider x1 = v1 as Real ;
A27: 1 - p > 0 by A26, XREAL_1:50;

per cases ( ( v1 in X & v2 in X ) or ( v1 in X & not v2 in X ) or ( not v1 in X & v2 in X ) or ( not v1 in X & not v2 in X ) ) ;

suppose A28: ( v1 in X & v2 in X ) ; :: thesis: g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2))

then A29: f . x2 = g . v2 by A2;
f . x1 = g . v1 by A2, A28;
then A30: (p * (f . x1)) + ((1 - p) * (f . x2)) = ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by A29, Lm12;
A31: (1 - p) * v2 = (1 - p) * x2 by BINOP_2:def 11;
p * v1 = p * x1 by BINOP_2:def 11;
then A32: (p * v1) + ((1 - p) * v2) = (p * x1) + ((1 - p) * x2) by A31, BINOP_2:def 9;
A33: (p * v1) + ((1 - p) * v2) in X by A24, A25, A26, A28, CONVEX1:def 2;
then f . ((p * x1) + ((1 - p) * x2)) = g . ((p * v1) + ((1 - p) * v2)) by A2, A32;
hence g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by A23, A25, A26, A28, A33, A32, A30, RFUNCT_3:def 12; :: thesis: verum

end;

suppose A34: ( v1 in X & not v2 in X ) ; :: thesis: g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2))

then g . x2 = +infty by A2;
then A35: (R_EAL (1 - p)) * (g . v2) = +infty by A27, XXREAL_3:def 5;
reconsider w1 = g . x1 as Real by A4, A34;
p * w1 = (R_EAL p) * (g . v1) by EXTREAL1:1;
then ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) = +infty by A35, XXREAL_3:def 2;
hence g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by XXREAL_0:4; :: thesis: verum

end;

suppose A36: ( not v1 in X & v2 in X ) ; :: thesis: g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2))

then g . x1 = +infty by A2;
then A37: (R_EAL p) * (g . v1) = +infty by A25, XXREAL_3:def 5;
reconsider w2 = g . x2 as Real by A4, A36;
(1 - p) * w2 = (R_EAL (1 - p)) * (g . v2) by EXTREAL1:1;
then ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) = +infty by A37, XXREAL_3:def 2;
hence g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by XXREAL_0:4; :: thesis: verum

end;

suppose A38: ( not v1 in X & not v2 in X ) ; :: thesis: g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2))

then g . x2 = +infty by A2;
then A39: (R_EAL (1 - p)) * (g . v2) = +infty by A27, XXREAL_3:def 5;
g . x1 = +infty by A2, A38;
then ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) = +infty by A25, A39, XXREAL_3:def 2;
hence g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by XXREAL_0:4; :: thesis: verum

end;

end;

end;

hence g is convex by A3, Th9; :: thesis: verum

end;