:: Definition of Convex Function and {J}ensen's Inequality :: by Grigory E. Ivanov :: :: Received July 17, 2003 :: Copyright (c) 2003-2012 Association of Mizar Users begin definition let X, Y be non empty RLSStruct ; func Add_in_Prod_of_RLS (X,Y) -> BinOp of [: the carrier of X, the carrier of Y:] means :Def1: :: CONVFUN1:def 1 for z1, z2 being Element of [: the carrier of X, the carrier of Y:] for x1, x2 being VECTOR of X for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds it . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])]; existence ex b1 being BinOp of [: the carrier of X, the carrier of Y:] st for z1, z2 being Element of [: the carrier of X, the carrier of Y:] for x1, x2 being VECTOR of X for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds b1 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] proofend; uniqueness for b1, b2 being BinOp of [: the carrier of X, the carrier of Y:] st ( for z1, z2 being Element of [: the carrier of X, the carrier of Y:] for x1, x2 being VECTOR of X for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds b1 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] ) & ( for z1, z2 being Element of [: the carrier of X, the carrier of Y:] for x1, x2 being VECTOR of X for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds b2 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines Add_in_Prod_of_RLS CONVFUN1:def_1_:_ for X, Y being non empty RLSStruct for b3 being BinOp of [: the carrier of X, the carrier of Y:] holds ( b3 = Add_in_Prod_of_RLS (X,Y) iff for z1, z2 being Element of [: the carrier of X, the carrier of Y:] for x1, x2 being VECTOR of X for y1, y2 being VECTOR of Y st z1 = [x1,y1] & z2 = [x2,y2] holds b3 . (z1,z2) = [( the addF of X . [x1,x2]),( the addF of Y . [y1,y2])] ); definition let X, Y be non empty RLSStruct ; func Mult_in_Prod_of_RLS (X,Y) -> Function of [:REAL,[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:] means :Def2: :: CONVFUN1:def 2 for a being Real for z being Element of [: the carrier of X, the carrier of Y:] for x being VECTOR of X for y being VECTOR of Y st z = [x,y] holds it . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])]; existence ex b1 being Function of [:REAL,[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:] st for a being Real for z being Element of [: the carrier of X, the carrier of Y:] for x being VECTOR of X for y being VECTOR of Y st z = [x,y] holds b1 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] proofend; uniqueness for b1, b2 being Function of [:REAL,[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:] st ( for a being Real for z being Element of [: the carrier of X, the carrier of Y:] for x being VECTOR of X for y being VECTOR of Y st z = [x,y] holds b1 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] ) & ( for a being Real for z being Element of [: the carrier of X, the carrier of Y:] for x being VECTOR of X for y being VECTOR of Y st z = [x,y] holds b2 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines Mult_in_Prod_of_RLS CONVFUN1:def_2_:_ for X, Y being non empty RLSStruct for b3 being Function of [:REAL,[: the carrier of X, the carrier of Y:]:],[: the carrier of X, the carrier of Y:] holds ( b3 = Mult_in_Prod_of_RLS (X,Y) iff for a being Real for z being Element of [: the carrier of X, the carrier of Y:] for x being VECTOR of X for y being VECTOR of Y st z = [x,y] holds b3 . (a,z) = [( the Mult of X . [a,x]),( the Mult of Y . [a,y])] ); definition let X, Y be non empty RLSStruct ; func Prod_of_RLS (X,Y) -> RLSStruct equals :: CONVFUN1:def 3 RLSStruct(# [: the carrier of X, the carrier of Y:],[(0. X),(0. Y)],(Add_in_Prod_of_RLS (X,Y)),(Mult_in_Prod_of_RLS (X,Y)) #); correctness coherence RLSStruct(# [: the carrier of X, the carrier of Y:],[(0. X),(0. Y)],(Add_in_Prod_of_RLS (X,Y)),(Mult_in_Prod_of_RLS (X,Y)) #) is RLSStruct ; ; end; :: deftheorem defines Prod_of_RLS CONVFUN1:def_3_:_ for X, Y being non empty RLSStruct holds Prod_of_RLS (X,Y) = RLSStruct(# [: the carrier of X, the carrier of Y:],[(0. X),(0. Y)],(Add_in_Prod_of_RLS (X,Y)),(Mult_in_Prod_of_RLS (X,Y)) #); registration let X, Y be non empty RLSStruct ; cluster Prod_of_RLS (X,Y) -> non empty ; coherence not Prod_of_RLS (X,Y) is empty ; end; theorem :: CONVFUN1:1 for X, Y being non empty RLSStruct for x being VECTOR of X for y being VECTOR of Y for u being VECTOR of (Prod_of_RLS (X,Y)) for p being Real st u = [x,y] holds p * u = [(p * x),(p * y)] by Def2; theorem Th2: :: CONVFUN1:2 for X, Y being non empty RLSStruct for x1, x2 being VECTOR of X for y1, y2 being VECTOR of Y for u1, u2 being VECTOR of (Prod_of_RLS (X,Y)) st u1 = [x1,y1] & u2 = [x2,y2] holds u1 + u2 = [(x1 + x2),(y1 + y2)] by Def1; registration let X, Y be non empty Abelian RLSStruct ; cluster Prod_of_RLS (X,Y) -> Abelian ; coherence Prod_of_RLS (X,Y) is Abelian proofend; end; registration let X, Y be non empty add-associative RLSStruct ; cluster Prod_of_RLS (X,Y) -> add-associative ; coherence Prod_of_RLS (X,Y) is add-associative proofend; end; registration let X, Y be non empty right_zeroed RLSStruct ; cluster Prod_of_RLS (X,Y) -> right_zeroed ; coherence Prod_of_RLS (X,Y) is right_zeroed proofend; end; registration let X, Y be non empty right_complementable RLSStruct ; cluster Prod_of_RLS (X,Y) -> right_complementable ; coherence Prod_of_RLS (X,Y) is right_complementable proofend; end; registration let X, Y be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; cluster Prod_of_RLS (X,Y) -> vector-distributive scalar-distributive scalar-associative scalar-unital ; coherence ( Prod_of_RLS (X,Y) is vector-distributive & Prod_of_RLS (X,Y) is scalar-distributive & Prod_of_RLS (X,Y) is scalar-associative & Prod_of_RLS (X,Y) is scalar-unital ) proofend; end; theorem Th3: :: CONVFUN1:3 for X, Y being RealLinearSpace for n being Element of NAT for x being FinSequence of the carrier of X for y being FinSequence of the carrier of Y for z being FinSequence of the carrier of (Prod_of_RLS (X,Y)) st len x = n & len y = n & len z = n & ( for i being Element of NAT st i in Seg n holds z . i = [(x . i),(y . i)] ) holds Sum z = [(Sum x),(Sum y)] proofend; begin definition func RLS_Real -> non empty RLSStruct equals :: CONVFUN1:def 4 RLSStruct(# REAL,0,addreal,multreal #); correctness coherence RLSStruct(# REAL,0,addreal,multreal #) is non empty RLSStruct ; ; end; :: deftheorem defines RLS_Real CONVFUN1:def_4_:_ RLS_Real = RLSStruct(# REAL,0,addreal,multreal #); registration cluster RLS_Real -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ; coherence ( RLS_Real is Abelian & RLS_Real is add-associative & RLS_Real is right_zeroed & RLS_Real is right_complementable & RLS_Real is vector-distributive & RLS_Real is scalar-distributive & RLS_Real is scalar-associative & RLS_Real is scalar-unital ) proofend; end; Lm1: for X being non empty RLSStruct for x being VECTOR of X for u being VECTOR of (Prod_of_RLS (X,RLS_Real)) for p, w being Real st u = [x,w] holds p * u = [(p * x),(p * w)] proofend; Lm2: for X being non empty RLSStruct for x1, x2 being VECTOR of X for w1, w2 being Real for u1, u2 being VECTOR of (Prod_of_RLS (X,RLS_Real)) st u1 = [x1,w1] & u2 = [x2,w2] holds u1 + u2 = [(x1 + x2),(w1 + w2)] proofend; Lm3: for a being FinSequence of the carrier of RLS_Real for b being FinSequence of REAL st len a = len b & ( for i being Element of NAT st i in dom a holds a . i = b . i ) holds Sum a = Sum b proofend; begin Lm4: for F being FinSequence of ExtREAL for x being Element of ExtREAL holds Sum (F ^ <*x*>) = (Sum F) + x proofend; Lm5: for F being FinSequence of ExtREAL st not -infty in rng F holds Sum F <> -infty proofend; Lm6: for F being FinSequence of ExtREAL st +infty in rng F & not -infty in rng F holds Sum F = +infty proofend; Lm7: for a being FinSequence of ExtREAL for b being FinSequence of REAL st len a = len b & ( for i being Element of NAT st i in dom a holds a . i = b . i ) holds Sum a = Sum b proofend; Lm8: for n being Element of NAT for a being FinSequence of ExtREAL for b being FinSequence of the carrier of RLS_Real st len a = n & len b = n & ( for i being Element of NAT st i in Seg n holds a . i = b . i ) holds Sum a = Sum b proofend; Lm9: for F being FinSequence of ExtREAL st rng F c= {0.} holds Sum F = 0. proofend; Lm10: for F being FinSequence of REAL st rng F c= {0} holds Sum F = 0 proofend; Lm11: for X being RealLinearSpace for F being FinSequence of the carrier of X st rng F c= {(0. X)} holds Sum F = 0. X proofend; begin definition let X be non empty RLSStruct ; let f be Function of the carrier of X,ExtREAL; func epigraph f -> Subset of (Prod_of_RLS (X,RLS_Real)) equals :: CONVFUN1:def 5 { [x,y] where x is Element of X, y is Element of REAL : f . x <= R_EAL y } ; coherence { [x,y] where x is Element of X, y is Element of REAL : f . x <= R_EAL y } is Subset of (Prod_of_RLS (X,RLS_Real)) proofend; end; :: deftheorem defines epigraph CONVFUN1:def_5_:_ for X being non empty RLSStruct for f being Function of the carrier of X,ExtREAL holds epigraph f = { [x,y] where x is Element of X, y is Element of REAL : f . x <= R_EAL y } ; definition let X be non empty RLSStruct ; let f be Function of the carrier of X,ExtREAL; attrf is convex means :Def6: :: CONVFUN1:def 6 epigraph f is convex ; end; :: deftheorem Def6 defines convex CONVFUN1:def_6_:_ for X being non empty RLSStruct for f being Function of the carrier of X,ExtREAL holds ( f is convex iff epigraph f is convex ); Lm12: for w1, w2 being R_eal for wr1, wr2, p1, p2 being Real st w1 = wr1 & w2 = wr2 holds (p1 * wr1) + (p2 * wr2) = ((R_EAL p1) * w1) + ((R_EAL p2) * w2) proofend; theorem Th4: :: CONVFUN1:4 for X being non empty RLSStruct 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)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) ) proofend; theorem :: CONVFUN1:5 for X being RealLinearSpace 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)) <= ((R_EAL p) * (f . x1)) + ((R_EAL (1 - p)) * (f . x2)) ) proofend; begin theorem :: CONVFUN1:6 for f being 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 ) ) proofend; begin theorem Th7: :: CONVFUN1:7 for X being RealLinearSpace for M being Subset of X holds ( M is convex iff for n being non empty Nat for p being FinSequence of REAL for y, z being FinSequence of the carrier of X st len p = n & len y = n & len z = n & Sum p = 1 & ( for i being Nat st i in Seg n holds ( p . i > 0 & z . i = (p . i) * (y /. i) & y /. i in M ) ) holds Sum z in M ) proofend; begin Lm13: for X being RealLinearSpace for f being Function of the carrier of X,ExtREAL for n being non empty Element of NAT for p being FinSequence of REAL for F being FinSequence of ExtREAL for y being FinSequence of the carrier of X st len F = n & ( for x being VECTOR of X holds f . x <> -infty ) & ( for i being Element of NAT st i in Seg n holds ( p . i >= 0 & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds not -infty in rng F proofend; theorem Th8: :: CONVFUN1:8 for X being RealLinearSpace 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 n being non empty Element of NAT for p being FinSequence of REAL for F being FinSequence of ExtREAL for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i > 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F ) proofend; Lm14: for F being FinSequence of REAL ex s being Permutation of (dom F) ex n being Element of NAT st for i being Element of NAT st i in dom F holds ( i in Seg n iff F . (s . i) <> 0 ) proofend; theorem :: CONVFUN1:9 for X being RealLinearSpace 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 n being non empty Element of NAT for p being FinSequence of REAL for F being FinSequence of ExtREAL for y, z being FinSequence of the carrier of X st len p = n & len F = n & len y = n & len z = n & Sum p = 1 & ( for i being Element of NAT st i in Seg n holds ( p . i >= 0 & z . i = (p . i) * (y /. i) & F . i = (R_EAL (p . i)) * (f . (y /. i)) ) ) holds f . (Sum z) <= Sum F ) proofend;