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:
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 ;
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 ;
A17: p < 1 by ;
(p * (f . v1)) + ((1 - p) * (f . v2)) = (p * (g . v1)) + ((1 - p) * (g . v2)) by ;
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 ; :: 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 ;
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 ;
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 ;
then A31: (p * (f . x1)) + ((1 - p) * (f . x2)) = (p * (g . v1)) + ((1 - p) * (g . v2)) by ;
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 ;
reconsider pc = (p * x1) + ((1 - p) * x2) as Real ;
A34: (p * v1) + ((1 - p) * v2) in X by ;
then f . pc = g . ((p * v1) + ((1 - p) * v2)) by ;
hence g . ((p * v1) + ((1 - p) * v2)) <= (p * (g . v1)) + ((1 - p) * (g . v2)) by ; :: 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 ;
reconsider w1 = g . x1 as Element of REAL by ;
p * w1 = p * (g . v1) by EXTREAL1:1;
then (p * (g . v1)) + ((1 - p) * (g . v2)) = +infty by ;
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 ;
reconsider w2 = g . x2 as Element of REAL by ;
(1 - p) * w2 = (1 - p) * (g . v2) by EXTREAL1:1;
then (p * (g . v1)) + ((1 - p) * (g . v2)) = +infty by ;
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 ;
g . x1 = +infty by ;
then (p * (g . v1)) + ((1 - p) * (g . v2)) = +infty by ;
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 ; :: thesis: verum
end;