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 A1: ( 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 ) ) ) ) ; :: thesis: ( g is convex iff ( f is_convex_on X & X is convex ) )
A2: 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 ;

per cases ( x in X or not x in X ) ;

suppose x in X ; :: thesis: g . v <> -infty

f . x in REAL ;
hence g . v <> -infty by A1; :: thesis: verum

end;

suppose not x in X ; :: thesis: g . v <> -infty

hence g . v <> -infty by A1; :: thesis: verum

end;

end;

end;

A3: 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 ( v in dom f & g . x = f . x ) by A1;
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 A4: g is convex ; :: thesis: ( f is_convex_on X & X is convex )
thus f is_convex_on X :: thesis: X is convex

proof

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 A5: ( 0 <= p & 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 ( x1 in X & x2 in X & (p * x1) + ((1 - p) * x2) in X ) ; :: thesis: f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2))
then A6: ( f . x1 = g . x1 & f . x2 = g . x2 & f . ((p * x1) + ((1 - p) * x2)) = g . ((p * x1) + ((1 - p) * x2)) ) by A1;

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 ( p <> 0 & p <> 1 ) ; :: thesis: f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2))

then A7: ( 0 < p & p < 1 ) by A5, XXREAL_0:1;
reconsider v1 = x1 as VECTOR of RLS_Real ;
reconsider v2 = x2 as VECTOR of RLS_Real ;
A8: (p * (f . v1)) + ((1 - p) * (f . v2)) = ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by A6, Lm16;
( p * v1 = p * x1 & (1 - p) * v2 = (1 - p) * x2 ) by BINOP_2:def 11;
then g . ((p * v1) + ((1 - p) * v2)) = f . ((p * x1) + ((1 - p) * x2)) by A6, BINOP_2:def 9;
hence f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) by A2, A4, A7, A8, Th9; :: thesis: verum

end;

end;

end;

hence f is_convex_on X by A1, RFUNCT_3:def 13; :: thesis: verum

end;

thus X is convex :: thesis: verum

proof

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 A9: ( 0 < p & p < 1 & v1 in X & v2 in X ) ; :: thesis: (p * v1) + ((1 - p) * v2) in X
then A10: g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by A2, A4, Th9;
reconsider w1 = g . v1, w2 = g . v2 as Real by A3, A9;
(p * w1) + ((1 - p) * w2) = ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by Lm16;
then A11: g . ((p * v1) + ((1 - p) * v2)) <> +infty by A10, XXREAL_0:9;
thus (p * v1) + ((1 - p) * v2) in X by A1, A11; :: thesis: verum

end;

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

end;

end;

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

proof

assume A12: ( f is_convex_on X & 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 A13: ( 0 < p & p < 1 ) ; :: thesis: g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2))
A15: 1 - p > 0 by A13, XREAL_1:52;
A17: 0. < R_EAL (1 - p) by A15;
reconsider x1 = v1 as Real ;
reconsider x2 = v2 as Real ;

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 A18: ( 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 A19: (p * v1) + ((1 - p) * v2) in X by A12, A13, CONVEX1:def 2;
( p * v1 = p * x1 & (1 - p) * v2 = (1 - p) * x2 ) by BINOP_2:def 11;
then A20: (p * v1) + ((1 - p) * v2) = (p * x1) + ((1 - p) * x2) by BINOP_2:def 9;
then A21: ( f . x1 = g . v1 & f . x2 = g . v2 & f . ((p * x1) + ((1 - p) * x2)) = g . ((p * v1) + ((1 - p) * v2)) ) by A1, A18, A19;
then (p * (f . x1)) + ((1 - p) * (f . x2)) = ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by Lm16;
hence g . ((p * v1) + ((1 - p) * v2)) <= ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) by A12, A13, A18, A19, A20, A21, RFUNCT_3:def 13; :: thesis: verum

end;

suppose A22: ( 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 A1;
then A23: (R_EAL (1 - p)) * (g . v2) = +infty by A15, XXREAL_3:def 5;
reconsider w1 = g . x1 as Real by A3, A22;
p * w1 = (R_EAL p) * (g . v1) by EXTREAL1:13;
then ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) = +infty by A23, 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 A24: ( 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 A1;
then A25: (R_EAL p) * (g . v1) = +infty by A13, XXREAL_3:def 5;
reconsider w2 = g . x2 as Real by A3, A24;
(1 - p) * w2 = (R_EAL (1 - p)) * (g . v2) by EXTREAL1:13;
then ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) = +infty by A25, 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 ( 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 . x1 = +infty & g . x2 = +infty ) by A1;
then ( (R_EAL p) * (g . v1) = +infty & (R_EAL (1 - p)) * (g . v2) = +infty ) by A13, A17, XXREAL_3:def 5;
then ((R_EAL p) * (g . v1)) + ((R_EAL (1 - p)) * (g . v2)) = +infty by 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 A2, Th9; :: thesis: verum

end;