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 by XREAL_0:def 1;
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 by XREAL_0:def 1; :: 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 by XREAL_0:def 1;
reconsider v1 = x1 as VECTOR of RLS_Real by XREAL_0:def 1;
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)) = (p * (g . v1)) + ((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, Th4; :: 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 Element of REAL by A4, A20, A21;
A22: (p * w1) + ((1 - p) * w2) in REAL by XREAL_0:def 1;
A23: (p * w1) + ((1 - p) * w2) = (p * (g . v1)) + ((1 - p) * (g . v2)) by Lm12;
g . ((p * v1) + ((1 - p) * v2)) <= (p * (g . v1)) + ((1 - p) * (g . v2)) by A3, A5, A18, A19, Th4;
then g . ((p * v1) + ((1 - p) * v2)) <> +infty by A23, XXREAL_0:9, A22;
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
A24: f is_convex_on X and
A25: 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)) <= (p * (g . v1)) + ((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)) <= (p * (g . v1)) + ((1 - p) * (g . v2))
let p be Real; :: thesis: ( 0 < p & p < 1 implies g . ((p * v1) + ((1 - p) * v2)) <= (p * (g . v1)) + ((1 - p) * (g . v2)) )
assume that
A26: 0 < p and
A27: p < 1 ; :: thesis: g . ((p * v1) + ((1 - p) * v2)) <= (p * (g . v1)) + ((1 - p) * (g . v2))
reconsider x2 = v2 as Real ;
reconsider x1 = v1 as Real ;
reconsider p = p as Real ;
A28: 1 - p > 0 by A27, 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 A29: ( v1 in X & v2 in X ) ; :: thesis: g . ((p * v1) + ((1 - p) * v2)) <= (p * (g . v1)) + ((1 - p) * (g . v2))

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

end;

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

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

end;

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

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

end;

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

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

end;

end;

end;

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

end;