let X be non empty RLSStruct ; :: thesis: for f being Function of the carrier of X,ExtREAL st ( for x being VECTOR of X holds f . x <> -infty ) holds

( f is convex iff for x1, x2 being VECTOR of X

for p being Real st 0 < p & p < 1 holds

f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) )

let f be Function of the carrier of X,ExtREAL; :: thesis: ( ( for x being VECTOR of X holds f . x <> -infty ) implies ( f is convex iff for x1, x2 being VECTOR of X

for p being Real st 0 < p & p < 1 holds

f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) ) )

assume A1: for x being VECTOR of X holds f . x <> -infty ; :: thesis: ( f is convex iff for x1, x2 being VECTOR of X

for p being Real st 0 < p & p < 1 holds

f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) )

thus ( f is convex implies for x1, x2 being VECTOR of X

for p being Real st 0 < p & p < 1 holds

f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) ) :: thesis: ( ( for x1, x2 being VECTOR of X

for p being Real st 0 < p & p < 1 holds

f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) ) implies f is convex )

for p being Real st 0 < p & p < 1 holds

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

for u1, u2 being VECTOR of (Prod_of_RLS (X,RLS_Real))

for p being Real st 0 < p & p < 1 & u1 in epigraph f & u2 in epigraph f holds

(p * u1) + ((1 - p) * u2) in epigraph f

hence f is convex ; :: thesis: verum

( f is convex iff for x1, x2 being VECTOR of X

for p being Real st 0 < p & p < 1 holds

f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) )

let f be Function of the carrier of X,ExtREAL; :: thesis: ( ( for x being VECTOR of X holds f . x <> -infty ) implies ( f is convex iff for x1, x2 being VECTOR of X

for p being Real st 0 < p & p < 1 holds

f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) ) )

assume A1: for x being VECTOR of X holds f . x <> -infty ; :: thesis: ( f is convex iff for x1, x2 being VECTOR of X

for p being Real st 0 < p & p < 1 holds

f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) )

thus ( f is convex implies for x1, x2 being VECTOR of X

for p being Real st 0 < p & p < 1 holds

f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) ) :: thesis: ( ( for x1, x2 being VECTOR of X

for p being Real st 0 < p & p < 1 holds

f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) ) implies f is convex )

proof

assume A18:
for x1, x2 being VECTOR of X
assume
f is convex
; :: thesis: for x1, x2 being VECTOR of X

for p being Real st 0 < p & p < 1 holds

f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2))

then A2: epigraph f is convex ;

let x1, x2 be VECTOR of X; :: thesis: for p being Real st 0 < p & p < 1 holds

f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2))

let p be Real; :: thesis: ( 0 < p & p < 1 implies f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) )

assume that

A3: 0 < p and

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

set p2 = 1 - p;

set p1 = p;

A5: 1 - p > 0 by A4, XREAL_1:50;

end;for p being Real st 0 < p & p < 1 holds

f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2))

then A2: epigraph f is convex ;

let x1, x2 be VECTOR of X; :: thesis: for p being Real st 0 < p & p < 1 holds

f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2))

let p be Real; :: thesis: ( 0 < p & p < 1 implies f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) )

assume that

A3: 0 < p and

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

set p2 = 1 - p;

set p1 = p;

A5: 1 - p > 0 by A4, XREAL_1:50;

per cases
( ( f . x1 in REAL & f . x2 in REAL ) or ( f . x1 = +infty & f . x2 in REAL ) or ( f . x1 in REAL & f . x2 = +infty ) or ( f . x1 = +infty & f . x2 = +infty ) )
by A1, XXREAL_0:14;

end;

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

then reconsider w2 = f . x2 as Element of REAL ;

reconsider w1 = f . x1 as Element of REAL by A6;

reconsider u1 = [x1,w1] as VECTOR of (Prod_of_RLS (X,RLS_Real)) ;

reconsider u2 = [x2,w2] as VECTOR of (Prod_of_RLS (X,RLS_Real)) ;

A7: [x2,w2] in epigraph f ;

A8: p * u1 = [(p * x1),(p * w1)] by Lm1;

A9: (1 - p) * u2 = [((1 - p) * x2),((1 - p) * w2)] by Lm1;

[x1,w1] in epigraph f ;

then (p * u1) + ((1 - p) * u2) in epigraph f by A2, A3, A4, A7, CONVEX1:def 2;

then [((p * x1) + ((1 - p) * x2)),((p * w1) + ((1 - p) * w2))] in epigraph f by A8, A9, Lm2;

then consider x0 being Element of X, y0 being Element of REAL such that

A10: [((p * x1) + ((1 - p) * x2)),((p * w1) + ((1 - p) * w2))] = [x0,y0] and

A11: f . x0 <= y0 ;

A12: y0 = (p * w1) + ((1 - p) * w2) by A10, XTUPLE_0:1;

x0 = (p * x1) + ((1 - p) * x2) by A10, XTUPLE_0:1;

hence f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) by A11, A12, Lm12; :: thesis: verum

end;reconsider w1 = f . x1 as Element of REAL by A6;

reconsider u1 = [x1,w1] as VECTOR of (Prod_of_RLS (X,RLS_Real)) ;

reconsider u2 = [x2,w2] as VECTOR of (Prod_of_RLS (X,RLS_Real)) ;

A7: [x2,w2] in epigraph f ;

A8: p * u1 = [(p * x1),(p * w1)] by Lm1;

A9: (1 - p) * u2 = [((1 - p) * x2),((1 - p) * w2)] by Lm1;

[x1,w1] in epigraph f ;

then (p * u1) + ((1 - p) * u2) in epigraph f by A2, A3, A4, A7, CONVEX1:def 2;

then [((p * x1) + ((1 - p) * x2)),((p * w1) + ((1 - p) * w2))] in epigraph f by A8, A9, Lm2;

then consider x0 being Element of X, y0 being Element of REAL such that

A10: [((p * x1) + ((1 - p) * x2)),((p * w1) + ((1 - p) * w2))] = [x0,y0] and

A11: f . x0 <= y0 ;

A12: y0 = (p * w1) + ((1 - p) * w2) by A10, XTUPLE_0:1;

x0 = (p * x1) + ((1 - p) * x2) by A10, XTUPLE_0:1;

hence f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2)) by A11, A12, Lm12; :: thesis: verum

suppose A13:
( f . x1 = +infty & f . x2 in REAL )
; :: thesis: f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2))

A14:
(1 - p) * (f . x2) in REAL
by A13, XREAL_0:def 1;

p * (f . x1) = +infty by A3, A13, XXREAL_3:def 5;

then (p * (f . x1)) + ((1 - p) * (f . x2)) = +infty by A14, XXREAL_3:def 2;

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

end;p * (f . x1) = +infty by A3, A13, XXREAL_3:def 5;

then (p * (f . x1)) + ((1 - p) * (f . x2)) = +infty by A14, XXREAL_3:def 2;

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

suppose A15:
( f . x1 in REAL & f . x2 = +infty )
; :: thesis: f . ((p * x1) + ((1 - p) * x2)) <= (p * (f . x1)) + ((1 - p) * (f . x2))

A16:
p * (f . x1) in REAL
by A15, XREAL_0:def 1;

(1 - p) * (f . x2) = +infty by A5, A15, XXREAL_3:def 5;

then (p * (f . x1)) + ((1 - p) * (f . x2)) = +infty by A16, XXREAL_3:def 2;

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

end;(1 - p) * (f . x2) = +infty by A5, A15, XXREAL_3:def 5;

then (p * (f . x1)) + ((1 - p) * (f . x2)) = +infty by A16, XXREAL_3:def 2;

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

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

then
(1 - p) * (f . x2) = +infty
by A5, XXREAL_3:def 5;

then (p * (f . x1)) + ((1 - p) * (f . x2)) = +infty by A3, A17, XXREAL_3:def 2;

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

end;then (p * (f . x1)) + ((1 - p) * (f . x2)) = +infty by A3, A17, XXREAL_3:def 2;

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

for p being Real st 0 < p & p < 1 holds

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

for u1, u2 being VECTOR of (Prod_of_RLS (X,RLS_Real))

for p being Real st 0 < p & p < 1 & u1 in epigraph f & u2 in epigraph f holds

(p * u1) + ((1 - p) * u2) in epigraph f

proof

then
epigraph f is convex
by CONVEX1:def 2;
let u1, u2 be VECTOR of (Prod_of_RLS (X,RLS_Real)); :: thesis: for p being Real st 0 < p & p < 1 & u1 in epigraph f & u2 in epigraph f holds

(p * u1) + ((1 - p) * u2) in epigraph f

let p be Real; :: thesis: ( 0 < p & p < 1 & u1 in epigraph f & u2 in epigraph f implies (p * u1) + ((1 - p) * u2) in epigraph f )

assume that

A19: 0 < p and

A20: p < 1 and

A21: u1 in epigraph f and

A22: u2 in epigraph f ; :: thesis: (p * u1) + ((1 - p) * u2) in epigraph f

reconsider pp = p as Real ;

thus (p * u1) + ((1 - p) * u2) in epigraph f :: thesis: verum

end;(p * u1) + ((1 - p) * u2) in epigraph f

let p be Real; :: thesis: ( 0 < p & p < 1 & u1 in epigraph f & u2 in epigraph f implies (p * u1) + ((1 - p) * u2) in epigraph f )

assume that

A19: 0 < p and

A20: p < 1 and

A21: u1 in epigraph f and

A22: u2 in epigraph f ; :: thesis: (p * u1) + ((1 - p) * u2) in epigraph f

reconsider pp = p as Real ;

thus (p * u1) + ((1 - p) * u2) in epigraph f :: thesis: verum

proof

consider x2 being Element of X, y2 being Element of REAL such that

A23: u2 = [x2,y2] and

A24: f . x2 <= y2 by A22;

A25: (1 - p) * u2 = [((1 - p) * x2),((1 - p) * y2)] by A23, Lm1;

f . x2 <> +infty by A24, XXREAL_0:9;

then reconsider w2 = f . x2 as Element of REAL by A1, XXREAL_0:14;

consider x1 being Element of X, y1 being Element of REAL such that

A26: u1 = [x1,y1] and

A27: f . x1 <= y1 by A21;

f . x1 <> +infty by A27, XXREAL_0:9;

then reconsider w1 = f . x1 as Element of REAL by A1, XXREAL_0:14;

1 - p > 0 by A20, XREAL_1:50;

then (1 - p) * w2 <= (1 - p) * y2 by A24, XREAL_1:64;

then A28: (p * w1) + ((1 - p) * w2) <= (p * w1) + ((1 - p) * y2) by XREAL_1:6;

p * w1 <= p * y1 by A19, A27, XREAL_1:64;

then (p * w1) + ((1 - p) * y2) <= (p * y1) + ((1 - p) * y2) by XREAL_1:6;

then A29: (p * w1) + ((1 - p) * w2) <= (p * y1) + ((1 - p) * y2) by A28, XXREAL_0:2;

A30: (p * w1) + ((1 - p) * w2) in REAL by XREAL_0:def 1;

A31: (p * w1) + ((1 - p) * w2) = (p * (f . x1)) + ((1 - p) * (f . x2)) by Lm12;

then f . ((pp * x1) + ((1 - pp) * x2)) <> +infty by A18, A19, A20, XXREAL_0:9, A30;

then reconsider w = f . ((p * x1) + ((1 - p) * x2)) as Element of REAL by A1, XXREAL_0:14;

A32: (p * y1) + ((1 - p) * y2) in REAL by XREAL_0:def 1;

w <= (pp * w1) + ((1 - pp) * w2) by A18, A19, A20, A31;

then f . ((pp * x1) + ((1 - pp) * x2)) <= (p * y1) + ((1 - p) * y2) by A29, XXREAL_0:2;

then A33: [((p * x1) + ((1 - p) * x2)),((p * y1) + ((1 - p) * y2))] in { [x,y] where x is Element of X, y is Element of REAL : f . x <= y } by A32;

p * u1 = [(p * x1),(p * y1)] by A26, Lm1;

then (p * u1) + ((1 - p) * u2) = [((p * x1) + ((1 - p) * x2)),((p * y1) + ((1 - p) * y2))] by A25, Lm2;

hence (p * u1) + ((1 - p) * u2) in epigraph f by A33; :: thesis: verum

end;A23: u2 = [x2,y2] and

A24: f . x2 <= y2 by A22;

A25: (1 - p) * u2 = [((1 - p) * x2),((1 - p) * y2)] by A23, Lm1;

f . x2 <> +infty by A24, XXREAL_0:9;

then reconsider w2 = f . x2 as Element of REAL by A1, XXREAL_0:14;

consider x1 being Element of X, y1 being Element of REAL such that

A26: u1 = [x1,y1] and

A27: f . x1 <= y1 by A21;

f . x1 <> +infty by A27, XXREAL_0:9;

then reconsider w1 = f . x1 as Element of REAL by A1, XXREAL_0:14;

1 - p > 0 by A20, XREAL_1:50;

then (1 - p) * w2 <= (1 - p) * y2 by A24, XREAL_1:64;

then A28: (p * w1) + ((1 - p) * w2) <= (p * w1) + ((1 - p) * y2) by XREAL_1:6;

p * w1 <= p * y1 by A19, A27, XREAL_1:64;

then (p * w1) + ((1 - p) * y2) <= (p * y1) + ((1 - p) * y2) by XREAL_1:6;

then A29: (p * w1) + ((1 - p) * w2) <= (p * y1) + ((1 - p) * y2) by A28, XXREAL_0:2;

A30: (p * w1) + ((1 - p) * w2) in REAL by XREAL_0:def 1;

A31: (p * w1) + ((1 - p) * w2) = (p * (f . x1)) + ((1 - p) * (f . x2)) by Lm12;

then f . ((pp * x1) + ((1 - pp) * x2)) <> +infty by A18, A19, A20, XXREAL_0:9, A30;

then reconsider w = f . ((p * x1) + ((1 - p) * x2)) as Element of REAL by A1, XXREAL_0:14;

A32: (p * y1) + ((1 - p) * y2) in REAL by XREAL_0:def 1;

w <= (pp * w1) + ((1 - pp) * w2) by A18, A19, A20, A31;

then f . ((pp * x1) + ((1 - pp) * x2)) <= (p * y1) + ((1 - p) * y2) by A29, XXREAL_0:2;

then A33: [((p * x1) + ((1 - p) * x2)),((p * y1) + ((1 - p) * y2))] in { [x,y] where x is Element of X, y is Element of REAL : f . x <= y } by A32;

p * u1 = [(p * x1),(p * y1)] by A26, Lm1;

then (p * u1) + ((1 - p) * u2) = [((p * x1) + ((1 - p) * x2)),((p * y1) + ((1 - p) * y2))] by A25, Lm2;

hence (p * u1) + ((1 - p) * u2) in epigraph f by A33; :: thesis: verum

hence f is convex ; :: thesis: verum