let f be PartFunc of REAL,REAL; 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; 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; ( 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 ) )
; ( g is convex iff ( f is_convex_on X & X is convex ) )
A3:
for v being VECTOR of RLS_Real holds g . v <> -infty
A4:
for v being VECTOR of RLS_Real st v in X holds
g . v in REAL
thus
( g is convex implies ( f is_convex_on X & X is convex ) )
( f is_convex_on X & X is convex implies g is convex )proof
assume A5:
g is
convex
;
( 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;
( 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
;
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;
( 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
;
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
;
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))
;
verum end; suppose
p = 1
;
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))
;
verum end; suppose A14:
(
p <> 0 &
p <> 1 )
;
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;
verum end; end;
end;
hence
f is_convex_on X
by A1, RFUNCT_3:def 12;
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;
for p being Real st 0 < p & p < 1 & v1 in X & v2 in X holds
(p * v1) + ((1 - p) * v2) in Xlet p be
Real;
( 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
;
(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;
verum
end;
hence
X is
convex
by CONVEX1:def 2;
verum
end;
thus
( f is_convex_on X & X is convex implies g is convex )
verumproof
assume that A24:
f is_convex_on X
and A25:
X is
convex
;
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;
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;
( 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
;
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 )
;
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;
verum end; suppose A39:
( not
v1 in X & not
v2 in X )
;
g . ((p * v1) + ((1 - p) * v2)) <= (p * (g . v1)) + ((1 - p) * (g . v2))end; end;
end;
hence
g is
convex
by A3, Th4;
verum
end;