:: RFUNCT_4 semantic presentation begin theorem Th1: :: RFUNCT_4:1 for a, b being real number holds max (a,b) >= min (a,b) proof let a, b be real number ; ::_thesis: max (a,b) >= min (a,b) percases ( min (a,b) = a or min (a,b) = b ) by XXREAL_0:15; suppose min (a,b) = a ; ::_thesis: max (a,b) >= min (a,b) hence max (a,b) >= min (a,b) by XXREAL_0:25; ::_thesis: verum end; suppose min (a,b) = b ; ::_thesis: max (a,b) >= min (a,b) hence max (a,b) >= min (a,b) by XXREAL_0:25; ::_thesis: verum end; end; end; theorem Th2: :: RFUNCT_4:2 for n being Element of NAT for R1, R2 being Element of n -tuples_on REAL for r1, r2 being Real holds mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>)) = (mlt (R1,R2)) ^ <*(r1 * r2)*> proof let n be Element of NAT ; ::_thesis: for R1, R2 being Element of n -tuples_on REAL for r1, r2 being Real holds mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>)) = (mlt (R1,R2)) ^ <*(r1 * r2)*> let R1, R2 be Element of n -tuples_on REAL; ::_thesis: for r1, r2 being Real holds mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>)) = (mlt (R1,R2)) ^ <*(r1 * r2)*> let r1, r2 be Real; ::_thesis: mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>)) = (mlt (R1,R2)) ^ <*(r1 * r2)*> len (R1 ^ <*r1*>) = (len R1) + 1 by FINSEQ_2:16 .= n + 1 by CARD_1:def_7 .= (len R2) + 1 by CARD_1:def_7 .= len (R2 ^ <*r2*>) by FINSEQ_2:16 ; then A1: len (mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) = len (R1 ^ <*r1*>) by FINSEQ_2:72 .= (len R1) + 1 by FINSEQ_2:16 .= n + 1 by CARD_1:def_7 ; A2: for k being Nat st k in Seg (n + 1) holds (mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = ((mlt (R1,R2)) ^ <*(r1 * r2)*>) . k proof let k be Nat; ::_thesis: ( k in Seg (n + 1) implies (mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = ((mlt (R1,R2)) ^ <*(r1 * r2)*>) . k ) assume A3: k in Seg (n + 1) ; ::_thesis: (mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = ((mlt (R1,R2)) ^ <*(r1 * r2)*>) . k A4: k <= n + 1 by A3, FINSEQ_1:1; now__::_thesis:_(mlt_((R1_^_<*r1*>),(R2_^_<*r2*>)))_._k_=_((mlt_(R1,R2))_^_<*(r1_*_r2)*>)_._k percases ( k < n + 1 or k = n + 1 ) by A4, XXREAL_0:1; suppose k < n + 1 ; ::_thesis: (mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = ((mlt (R1,R2)) ^ <*(r1 * r2)*>) . k then A5: k <= n by NAT_1:13; 1 <= k by A3, FINSEQ_1:1; then A6: k in Seg n by A5, FINSEQ_1:1; then k in Seg (len R1) by CARD_1:def_7; then k in dom R1 by FINSEQ_1:def_3; then A7: (R1 ^ <*r1*>) . k = R1 . k by FINSEQ_1:def_7; k in Seg (len R2) by A6, CARD_1:def_7; then k in dom R2 by FINSEQ_1:def_3; then (R2 ^ <*r2*>) . k = R2 . k by FINSEQ_1:def_7; then A8: (mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = (R1 . k) * (R2 . k) by A7, RVSUM_1:59; len (mlt (R1,R2)) = n by CARD_1:def_7; then k in dom (mlt (R1,R2)) by A6, FINSEQ_1:def_3; then ((mlt (R1,R2)) ^ <*(r1 * r2)*>) . k = (mlt (R1,R2)) . k by FINSEQ_1:def_7; hence (mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = ((mlt (R1,R2)) ^ <*(r1 * r2)*>) . k by A8, RVSUM_1:59; ::_thesis: verum end; supposeA9: k = n + 1 ; ::_thesis: (mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = ((mlt (R1,R2)) ^ <*(r1 * r2)*>) . k then k = (len R1) + 1 by CARD_1:def_7; then A10: (R1 ^ <*r1*>) . k = r1 by FINSEQ_1:42; A11: n + 1 = (len (mlt (R1,R2))) + 1 by CARD_1:def_7; k = (len R2) + 1 by A9, CARD_1:def_7; then (R2 ^ <*r2*>) . k = r2 by FINSEQ_1:42; then (mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = r1 * r2 by A10, RVSUM_1:59; hence (mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = ((mlt (R1,R2)) ^ <*(r1 * r2)*>) . k by A9, A11, FINSEQ_1:42; ::_thesis: verum end; end; end; hence (mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>))) . k = ((mlt (R1,R2)) ^ <*(r1 * r2)*>) . k ; ::_thesis: verum end; mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>)) is Element of (n + 1) -tuples_on REAL by A1, FINSEQ_2:92; hence mlt ((R1 ^ <*r1*>),(R2 ^ <*r2*>)) = (mlt (R1,R2)) ^ <*(r1 * r2)*> by A2, FINSEQ_2:119; ::_thesis: verum end; theorem Th3: :: RFUNCT_4:3 for n being Element of NAT for R being Element of n -tuples_on REAL st Sum R = 0 & ( for i being Element of NAT st i in dom R holds 0 <= R . i ) holds for i being Element of NAT st i in dom R holds R . i = 0 proof let n be Element of NAT ; ::_thesis: for R being Element of n -tuples_on REAL st Sum R = 0 & ( for i being Element of NAT st i in dom R holds 0 <= R . i ) holds for i being Element of NAT st i in dom R holds R . i = 0 let R be Element of n -tuples_on REAL; ::_thesis: ( Sum R = 0 & ( for i being Element of NAT st i in dom R holds 0 <= R . i ) implies for i being Element of NAT st i in dom R holds R . i = 0 ) assume that A1: Sum R = 0 and A2: for i being Element of NAT st i in dom R holds 0 <= R . i ; ::_thesis: for i being Element of NAT st i in dom R holds R . i = 0 A3: for i being Nat st i in dom R holds 0 <= R . i by A2; given k being Element of NAT such that A4: k in dom R and A5: R . k <> 0 ; ::_thesis: contradiction 0 <= R . k by A2, A4; hence contradiction by A1, A3, A4, A5, RVSUM_1:85; ::_thesis: verum end; theorem Th4: :: RFUNCT_4:4 for n being Element of NAT for R being Element of n -tuples_on REAL st ( for i being Element of NAT st i in dom R holds 0 = R . i ) holds R = n |-> 0 proof let n be Element of NAT ; ::_thesis: for R being Element of n -tuples_on REAL st ( for i being Element of NAT st i in dom R holds 0 = R . i ) holds R = n |-> 0 let R be Element of n -tuples_on REAL; ::_thesis: ( ( for i being Element of NAT st i in dom R holds 0 = R . i ) implies R = n |-> 0 ) assume A1: for i being Element of NAT st i in dom R holds 0 = R . i ; ::_thesis: R = n |-> 0 A2: for k being Nat st 1 <= k & k <= len R holds R . k = (n |-> 0) . k proof let k be Nat; ::_thesis: ( 1 <= k & k <= len R implies R . k = (n |-> 0) . k ) assume ( 1 <= k & k <= len R ) ; ::_thesis: R . k = (n |-> 0) . k then A3: k in Seg (len R) by FINSEQ_1:1; then k in dom R by FINSEQ_1:def_3; then A4: R . k = 0 by A1; k in Seg n by A3, CARD_1:def_7; hence R . k = (n |-> 0) . k by A4, FUNCOP_1:7; ::_thesis: verum end; len R = n by CARD_1:def_7 .= len (n |-> 0) by CARD_1:def_7 ; hence R = n |-> 0 by A2, FINSEQ_1:14; ::_thesis: verum end; theorem Th5: :: RFUNCT_4:5 for n being Element of NAT for R being Element of n -tuples_on REAL holds mlt ((n |-> 0),R) = n |-> 0 proof let n be Element of NAT ; ::_thesis: for R being Element of n -tuples_on REAL holds mlt ((n |-> 0),R) = n |-> 0 let R be Element of n -tuples_on REAL; ::_thesis: mlt ((n |-> 0),R) = n |-> 0 A1: len (mlt ((n |-> 0),R)) = n by CARD_1:def_7; A2: for k being Nat st 1 <= k & k <= len (mlt ((n |-> 0),R)) holds (mlt ((n |-> 0),R)) . k = (n |-> 0) . k proof let k be Nat; ::_thesis: ( 1 <= k & k <= len (mlt ((n |-> 0),R)) implies (mlt ((n |-> 0),R)) . k = (n |-> 0) . k ) assume ( 1 <= k & k <= len (mlt ((n |-> 0),R)) ) ; ::_thesis: (mlt ((n |-> 0),R)) . k = (n |-> 0) . k then A3: k in Seg (len (mlt ((n |-> 0),R))) by FINSEQ_1:1; (mlt ((n |-> 0),R)) . k = ((n |-> 0) . k) * (R . k) by RVSUM_1:60 .= 0 * (R . k) by A1, A3, FUNCOP_1:7 ; hence (mlt ((n |-> 0),R)) . k = (n |-> 0) . k by A1, A3, FUNCOP_1:7; ::_thesis: verum end; len (n |-> 0) = n by CARD_1:def_7; hence mlt ((n |-> 0),R) = n |-> 0 by A1, A2, FINSEQ_1:14; ::_thesis: verum end; begin definition let f be PartFunc of REAL,REAL; let X be set ; predf is_strictly_convex_on X means :Def1: :: RFUNCT_4:def 1 ( X c= dom f & ( for p being Real st 0 < p & p < 1 holds for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ) ); end; :: deftheorem Def1 defines is_strictly_convex_on RFUNCT_4:def_1_:_ for f being PartFunc of REAL,REAL for X being set holds ( f is_strictly_convex_on X iff ( X c= dom f & ( for p being Real st 0 < p & p < 1 holds for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ) ) ); theorem :: RFUNCT_4:6 for f being PartFunc of REAL,REAL for X being set st f is_strictly_convex_on X holds f is_convex_on X proof let f be PartFunc of REAL,REAL; ::_thesis: for X being set st f is_strictly_convex_on X holds f is_convex_on X let X be set ; ::_thesis: ( f is_strictly_convex_on X implies f is_convex_on X ) assume A1: f is_strictly_convex_on X ; ::_thesis: f is_convex_on X A2: for p being Real st 0 <= p & p <= 1 holds for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) proof let p be Real; ::_thesis: ( 0 <= p & p <= 1 implies for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ) assume A3: ( 0 <= p & p <= 1 ) ; ::_thesis: for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) proof let r, s be Real; ::_thesis: ( r in X & s in X & (p * r) + ((1 - p) * s) in X implies f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ) assume A4: ( r in X & s in X & (p * r) + ((1 - p) * s) in X ) ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) now__::_thesis:_f_._((p_*_r)_+_((1_-_p)_*_s))_<=_(p_*_(f_._r))_+_((1_-_p)_*_(f_._s)) percases ( p = 0 or p = 1 or ( 0 < p & p < 1 ) ) by A3, XXREAL_0:1; suppose p = 0 ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) hence f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum end; suppose p = 1 ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) hence f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum end; supposeA5: ( 0 < p & p < 1 ) ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) now__::_thesis:_f_._((p_*_r)_+_((1_-_p)_*_s))_<=_(p_*_(f_._r))_+_((1_-_p)_*_(f_._s)) percases ( r = s or r <> s ) ; suppose r = s ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) hence f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum end; suppose r <> s ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) hence f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) by A1, A4, A5, Def1; ::_thesis: verum end; end; end; hence f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum end; end; end; hence f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum end; hence for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum end; X c= dom f by A1, Def1; hence f is_convex_on X by A2, RFUNCT_3:def_12; ::_thesis: verum end; theorem :: RFUNCT_4:7 for a, b being Real for f being PartFunc of REAL,REAL holds ( f is_strictly_convex_on [.a,b.] iff ( [.a,b.] c= dom f & ( for p being Real st 0 < p & p < 1 holds for r, s being Real st r in [.a,b.] & s in [.a,b.] & r <> s holds f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ) ) ) proof let a, b be Real; ::_thesis: for f being PartFunc of REAL,REAL holds ( f is_strictly_convex_on [.a,b.] iff ( [.a,b.] c= dom f & ( for p being Real st 0 < p & p < 1 holds for r, s being Real st r in [.a,b.] & s in [.a,b.] & r <> s holds f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( f is_strictly_convex_on [.a,b.] iff ( [.a,b.] c= dom f & ( for p being Real st 0 < p & p < 1 holds for r, s being Real st r in [.a,b.] & s in [.a,b.] & r <> s holds f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ) ) ) set ab = { r where r is Real : ( a <= r & r <= b ) } ; A1: [.a,b.] = { r where r is Real : ( a <= r & r <= b ) } by RCOMP_1:def_1; thus ( f is_strictly_convex_on [.a,b.] implies ( [.a,b.] c= dom f & ( for p being Real st 0 < p & p < 1 holds for x, y being Real st x in [.a,b.] & y in [.a,b.] & x <> y holds f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) ) ) ) ::_thesis: ( [.a,b.] c= dom f & ( for p being Real st 0 < p & p < 1 holds for r, s being Real st r in [.a,b.] & s in [.a,b.] & r <> s holds f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ) implies f is_strictly_convex_on [.a,b.] ) proof assume A2: f is_strictly_convex_on [.a,b.] ; ::_thesis: ( [.a,b.] c= dom f & ( for p being Real st 0 < p & p < 1 holds for x, y being Real st x in [.a,b.] & y in [.a,b.] & x <> y holds f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) ) ) hence [.a,b.] c= dom f by Def1; ::_thesis: for p being Real st 0 < p & p < 1 holds for x, y being Real st x in [.a,b.] & y in [.a,b.] & x <> y holds f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) let p be Real; ::_thesis: ( 0 < p & p < 1 implies for x, y being Real st x in [.a,b.] & y in [.a,b.] & x <> y holds f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) ) assume that A3: 0 < p and A4: p < 1 ; ::_thesis: for x, y being Real st x in [.a,b.] & y in [.a,b.] & x <> y holds f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) A5: 0 <= 1 - p by A4, XREAL_1:48; A6: (p * b) + ((1 - p) * b) = b ; A7: (p * a) + ((1 - p) * a) = a ; let x, y be Real; ::_thesis: ( x in [.a,b.] & y in [.a,b.] & x <> y implies f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) ) assume that A8: x in [.a,b.] and A9: y in [.a,b.] and A10: x <> y ; ::_thesis: f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) A11: ex r2 being Real st ( r2 = y & a <= r2 & r2 <= b ) by A1, A9; then A12: (1 - p) * y <= (1 - p) * b by A5, XREAL_1:64; A13: ex r1 being Real st ( r1 = x & a <= r1 & r1 <= b ) by A1, A8; then p * x <= p * b by A3, XREAL_1:64; then A14: (p * x) + ((1 - p) * y) <= b by A12, A6, XREAL_1:7; A15: (1 - p) * a <= (1 - p) * y by A5, A11, XREAL_1:64; p * a <= p * x by A3, A13, XREAL_1:64; then a <= (p * x) + ((1 - p) * y) by A15, A7, XREAL_1:7; then (p * x) + ((1 - p) * y) in { r where r is Real : ( a <= r & r <= b ) } by A14; hence f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) by A1, A2, A3, A4, A8, A9, A10, Def1; ::_thesis: verum end; assume that A16: [.a,b.] c= dom f and A17: for p being Real st 0 < p & p < 1 holds for x, y being Real st x in [.a,b.] & y in [.a,b.] & x <> y holds f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) ; ::_thesis: f is_strictly_convex_on [.a,b.] thus [.a,b.] c= dom f by A16; :: according to RFUNCT_4:def_1 ::_thesis: for p being Real st 0 < p & p < 1 holds for r, s being Real st r in [.a,b.] & s in [.a,b.] & (p * r) + ((1 - p) * s) in [.a,b.] & r <> s holds f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) let p be Real; ::_thesis: ( 0 < p & p < 1 implies for r, s being Real st r in [.a,b.] & s in [.a,b.] & (p * r) + ((1 - p) * s) in [.a,b.] & r <> s holds f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ) assume A18: ( 0 < p & p < 1 ) ; ::_thesis: for r, s being Real st r in [.a,b.] & s in [.a,b.] & (p * r) + ((1 - p) * s) in [.a,b.] & r <> s holds f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) let x, y be Real; ::_thesis: ( x in [.a,b.] & y in [.a,b.] & (p * x) + ((1 - p) * y) in [.a,b.] & x <> y implies f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) ) assume that A19: ( x in [.a,b.] & y in [.a,b.] ) and (p * x) + ((1 - p) * y) in [.a,b.] ; ::_thesis: ( not x <> y or f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) ) thus ( not x <> y or f . ((p * x) + ((1 - p) * y)) < (p * (f . x)) + ((1 - p) * (f . y)) ) by A17, A18, A19; ::_thesis: verum end; theorem :: RFUNCT_4:8 for X being set for f being PartFunc of REAL,REAL holds ( f is_convex_on X iff ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) ) ) proof let X be set ; ::_thesis: for f being PartFunc of REAL,REAL holds ( f is_convex_on X iff ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( f is_convex_on X iff ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) ) ) A1: ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) implies f is_convex_on X ) proof assume that A2: X c= dom f and A3: for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ; ::_thesis: f is_convex_on X for p being Real st 0 <= p & p <= 1 holds for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) proof let p be Real; ::_thesis: ( 0 <= p & p <= 1 implies for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ) assume A4: ( 0 <= p & p <= 1 ) ; ::_thesis: for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) proof let r, s be Real; ::_thesis: ( r in X & s in X & (p * r) + ((1 - p) * s) in X implies f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ) assume A5: ( r in X & s in X & (p * r) + ((1 - p) * s) in X ) ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) proof percases ( p = 0 or p = 1 or ( 0 < p & p < 1 ) ) by A4, XXREAL_0:1; suppose p = 0 ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) hence f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum end; suppose p = 1 ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) hence f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum end; supposeA6: ( 0 < p & p < 1 ) ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) then A7: 0 < 1 - p by XREAL_1:50; percases ( r = s or r > s or r < s ) by XXREAL_0:1; suppose r = s ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) hence f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum end; supposeA8: r > s ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) set t = (p * r) + ((1 - p) * s); A9: r - s > 0 by A8, XREAL_1:50; A10: r - ((p * r) + ((1 - p) * s)) = (1 - p) * (r - s) ; then r - ((p * r) + ((1 - p) * s)) > 0 by A7, A9, XREAL_1:129; then A11: (p * r) + ((1 - p) * s) < r by XREAL_1:47; A12: ((p * r) + ((1 - p) * s)) - s = p * (r - s) ; then A13: (((p * r) + ((1 - p) * s)) - s) / (r - s) = p by A9, XCMPLX_1:89; ((p * r) + ((1 - p) * s)) - s > 0 by A6, A9, A12, XREAL_1:129; then A14: s < (p * r) + ((1 - p) * s) by XREAL_1:47; (r - ((p * r) + ((1 - p) * s))) / (r - s) = 1 - p by A9, A10, XCMPLX_1:89; hence f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) by A3, A5, A14, A11, A13; ::_thesis: verum end; supposeA15: r < s ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) set t = (p * r) + ((1 - p) * s); A16: s - r > 0 by A15, XREAL_1:50; A17: s - ((p * r) + ((1 - p) * s)) = p * (s - r) ; then s - ((p * r) + ((1 - p) * s)) > 0 by A6, A16, XREAL_1:129; then A18: (p * r) + ((1 - p) * s) < s by XREAL_1:47; A19: ((p * r) + ((1 - p) * s)) - r = (1 - p) * (s - r) ; then A20: (((p * r) + ((1 - p) * s)) - r) / (s - r) = 1 - p by A16, XCMPLX_1:89; ((p * r) + ((1 - p) * s)) - r > 0 by A7, A16, A19, XREAL_1:129; then A21: r < (p * r) + ((1 - p) * s) by XREAL_1:47; (s - ((p * r) + ((1 - p) * s))) / (s - r) = p by A16, A17, XCMPLX_1:89; hence f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) by A3, A5, A21, A18, A20; ::_thesis: verum end; end; end; end; end; hence f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum end; hence for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum end; hence f is_convex_on X by A2, RFUNCT_3:def_12; ::_thesis: verum end; ( f is_convex_on X implies ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) ) ) proof assume A22: f is_convex_on X ; ::_thesis: ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) ) for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) proof let a, b, c be Real; ::_thesis: ( a in X & b in X & c in X & a < b & b < c implies f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) assume that A23: ( a in X & b in X & c in X ) and A24: ( a < b & b < c ) ; ::_thesis: f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) set p = (c - b) / (c - a); A25: ( c - b < c - a & 0 < c - b ) by A24, XREAL_1:10, XREAL_1:50; then A26: (c - b) / (c - a) < 1 by XREAL_1:189; A27: ((c - b) / (c - a)) + ((b - a) / (c - a)) = ((c - b) + (b - a)) / (c - a) by XCMPLX_1:62 .= 1 by A25, XCMPLX_1:60 ; then (((c - b) / (c - a)) * a) + ((1 - ((c - b) / (c - a))) * c) = ((a * (c - b)) / (c - a)) + (c * ((b - a) / (c - a))) by XCMPLX_1:74 .= ((a * (c - b)) / (c - a)) + ((c * (b - a)) / (c - a)) by XCMPLX_1:74 .= (((c * a) - (b * a)) + ((b - a) * c)) / (c - a) by XCMPLX_1:62 .= (b * (c - a)) / (c - a) ; then (((c - b) / (c - a)) * a) + ((1 - ((c - b) / (c - a))) * c) = b by A25, XCMPLX_1:89; hence f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) by A22, A23, A25, A26, A27, RFUNCT_3:def_12; ::_thesis: verum end; hence ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) ) by A22, RFUNCT_3:def_12; ::_thesis: verum end; hence ( f is_convex_on X iff ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds f . b <= (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) ) ) by A1; ::_thesis: verum end; theorem :: RFUNCT_4:9 for X being set for f being PartFunc of REAL,REAL holds ( f is_strictly_convex_on X iff ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds f . b < (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) ) ) proof let X be set ; ::_thesis: for f being PartFunc of REAL,REAL holds ( f is_strictly_convex_on X iff ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds f . b < (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( f is_strictly_convex_on X iff ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds f . b < (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) ) ) A1: ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds f . b < (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) implies f is_strictly_convex_on X ) proof assume that A2: X c= dom f and A3: for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds f . b < (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ; ::_thesis: f is_strictly_convex_on X for p being Real st 0 < p & p < 1 holds for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) proof let p be Real; ::_thesis: ( 0 < p & p < 1 implies for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ) assume A4: ( 0 < p & p < 1 ) ; ::_thesis: for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) proof let r, s be Real; ::_thesis: ( r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s implies f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ) assume that A5: ( r in X & s in X & (p * r) + ((1 - p) * s) in X ) and A6: r <> s ; ::_thesis: f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) proof now__::_thesis:_f_._((p_*_r)_+_((1_-_p)_*_s))_<_(p_*_(f_._r))_+_((1_-_p)_*_(f_._s)) percases ( 0 < p & p < 1 ) by A4; supposeA7: ( 0 < p & p < 1 ) ; ::_thesis: f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) then A8: 0 < 1 - p by XREAL_1:50; now__::_thesis:_f_._((p_*_r)_+_((1_-_p)_*_s))_<_(p_*_(f_._r))_+_((1_-_p)_*_(f_._s)) percases ( r > s or r < s ) by A6, XXREAL_0:1; supposeA9: r > s ; ::_thesis: f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) set t = (p * r) + ((1 - p) * s); A10: r - s > 0 by A9, XREAL_1:50; A11: r - ((p * r) + ((1 - p) * s)) = (1 - p) * (r - s) ; then r - ((p * r) + ((1 - p) * s)) > 0 by A8, A10, XREAL_1:129; then A12: (p * r) + ((1 - p) * s) < r by XREAL_1:47; A13: ((p * r) + ((1 - p) * s)) - s = p * (r - s) ; then A14: (((p * r) + ((1 - p) * s)) - s) / (r - s) = p by A10, XCMPLX_1:89; ((p * r) + ((1 - p) * s)) - s > 0 by A7, A10, A13, XREAL_1:129; then A15: s < (p * r) + ((1 - p) * s) by XREAL_1:47; (r - ((p * r) + ((1 - p) * s))) / (r - s) = 1 - p by A10, A11, XCMPLX_1:89; hence f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) by A3, A5, A15, A12, A14; ::_thesis: verum end; supposeA16: r < s ; ::_thesis: f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) set t = (p * r) + ((1 - p) * s); A17: s - r > 0 by A16, XREAL_1:50; A18: s - ((p * r) + ((1 - p) * s)) = p * (s - r) ; then s - ((p * r) + ((1 - p) * s)) > 0 by A7, A17, XREAL_1:129; then A19: (p * r) + ((1 - p) * s) < s by XREAL_1:47; A20: ((p * r) + ((1 - p) * s)) - r = (1 - p) * (s - r) ; then A21: (((p * r) + ((1 - p) * s)) - r) / (s - r) = 1 - p by A17, XCMPLX_1:89; ((p * r) + ((1 - p) * s)) - r > 0 by A8, A17, A20, XREAL_1:129; then A22: r < (p * r) + ((1 - p) * s) by XREAL_1:47; (s - ((p * r) + ((1 - p) * s))) / (s - r) = p by A17, A18, XCMPLX_1:89; hence f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) by A3, A5, A22, A19, A21; ::_thesis: verum end; end; end; hence f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum end; end; end; hence f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum end; hence f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum end; hence for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum end; hence f is_strictly_convex_on X by A2, Def1; ::_thesis: verum end; ( f is_strictly_convex_on X implies ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds f . b < (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) ) ) proof assume A23: f is_strictly_convex_on X ; ::_thesis: ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds f . b < (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) ) for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds f . b < (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) proof let a, b, c be Real; ::_thesis: ( a in X & b in X & c in X & a < b & b < c implies f . b < (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) assume that A24: ( a in X & b in X & c in X ) and A25: ( a < b & b < c ) ; ::_thesis: f . b < (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) set p = (c - b) / (c - a); A26: ( c - b < c - a & 0 < c - b ) by A25, XREAL_1:10, XREAL_1:50; then A27: ( 0 < (c - b) / (c - a) & (c - b) / (c - a) < 1 ) by XREAL_1:139, XREAL_1:189; A28: ((c - b) / (c - a)) + ((b - a) / (c - a)) = ((c - b) + (b - a)) / (c - a) by XCMPLX_1:62 .= 1 by A26, XCMPLX_1:60 ; then (((c - b) / (c - a)) * a) + ((1 - ((c - b) / (c - a))) * c) = ((a * (c - b)) / (c - a)) + (c * ((b - a) / (c - a))) by XCMPLX_1:74 .= ((a * (c - b)) / (c - a)) + ((c * (b - a)) / (c - a)) by XCMPLX_1:74 .= (((c * a) - (b * a)) + ((b - a) * c)) / (c - a) by XCMPLX_1:62 .= (b * (c - a)) / (c - a) ; then (((c - b) / (c - a)) * a) + ((1 - ((c - b) / (c - a))) * c) = b by A26, XCMPLX_1:89; hence f . b < (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) by A23, A24, A25, A27, A28, Def1; ::_thesis: verum end; hence ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds f . b < (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) ) by A23, Def1; ::_thesis: verum end; hence ( f is_strictly_convex_on X iff ( X c= dom f & ( for a, b, c being Real st a in X & b in X & c in X & a < b & b < c holds f . b < (((c - b) / (c - a)) * (f . a)) + (((b - a) / (c - a)) * (f . c)) ) ) ) by A1; ::_thesis: verum end; theorem :: RFUNCT_4:10 for f being PartFunc of REAL,REAL for X, Y being set st f is_strictly_convex_on X & Y c= X holds f is_strictly_convex_on Y proof let f be PartFunc of REAL,REAL; ::_thesis: for X, Y being set st f is_strictly_convex_on X & Y c= X holds f is_strictly_convex_on Y let X, Y be set ; ::_thesis: ( f is_strictly_convex_on X & Y c= X implies f is_strictly_convex_on Y ) assume that A1: f is_strictly_convex_on X and A2: Y c= X ; ::_thesis: f is_strictly_convex_on Y X c= dom f by A1, Def1; then A3: Y c= dom f by A2, XBOOLE_1:1; for p being Real st 0 < p & p < 1 holds for r, s being Real st r in Y & s in Y & (p * r) + ((1 - p) * s) in Y & r <> s holds f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) by A1, A2, Def1; hence f is_strictly_convex_on Y by A3, Def1; ::_thesis: verum end; Lm1: for r being Real for f being PartFunc of REAL,REAL for X being set st f is_strictly_convex_on X holds f - r is_strictly_convex_on X proof let r be Real; ::_thesis: for f being PartFunc of REAL,REAL for X being set st f is_strictly_convex_on X holds f - r is_strictly_convex_on X let f be PartFunc of REAL,REAL; ::_thesis: for X being set st f is_strictly_convex_on X holds f - r is_strictly_convex_on X let X be set ; ::_thesis: ( f is_strictly_convex_on X implies f - r is_strictly_convex_on X ) assume A1: f is_strictly_convex_on X ; ::_thesis: f - r is_strictly_convex_on X then A2: X c= dom f by Def1; A3: for p being Real st 0 < p & p < 1 holds for t, s being Real st t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s holds (f - r) . ((p * t) + ((1 - p) * s)) < (p * ((f - r) . t)) + ((1 - p) * ((f - r) . s)) proof let p be Real; ::_thesis: ( 0 < p & p < 1 implies for t, s being Real st t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s holds (f - r) . ((p * t) + ((1 - p) * s)) < (p * ((f - r) . t)) + ((1 - p) * ((f - r) . s)) ) assume A4: ( 0 < p & p < 1 ) ; ::_thesis: for t, s being Real st t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s holds (f - r) . ((p * t) + ((1 - p) * s)) < (p * ((f - r) . t)) + ((1 - p) * ((f - r) . s)) for t, s being Real st t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s holds (f - r) . ((p * t) + ((1 - p) * s)) < (p * ((f - r) . t)) + ((1 - p) * ((f - r) . s)) proof let t, s be Real; ::_thesis: ( t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s implies (f - r) . ((p * t) + ((1 - p) * s)) < (p * ((f - r) . t)) + ((1 - p) * ((f - r) . s)) ) assume that A5: ( t in X & s in X ) and A6: (p * t) + ((1 - p) * s) in X and A7: t <> s ; ::_thesis: (f - r) . ((p * t) + ((1 - p) * s)) < (p * ((f - r) . t)) + ((1 - p) * ((f - r) . s)) f . ((p * t) + ((1 - p) * s)) < (p * (f . t)) + ((1 - p) * (f . s)) by A1, A4, A5, A6, A7, Def1; then A8: (f . ((p * t) + ((1 - p) * s))) - r < ((p * (f . t)) + ((1 - p) * (f . s))) - r by XREAL_1:9; ( (f - r) . t = (f . t) - r & (f - r) . s = (f . s) - r ) by A2, A5, VALUED_1:3; hence (f - r) . ((p * t) + ((1 - p) * s)) < (p * ((f - r) . t)) + ((1 - p) * ((f - r) . s)) by A2, A6, A8, VALUED_1:3; ::_thesis: verum end; hence for t, s being Real st t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s holds (f - r) . ((p * t) + ((1 - p) * s)) < (p * ((f - r) . t)) + ((1 - p) * ((f - r) . s)) ; ::_thesis: verum end; dom f = dom (f - r) by VALUED_1:3; hence f - r is_strictly_convex_on X by A2, A3, Def1; ::_thesis: verum end; theorem :: RFUNCT_4:11 for r being Real for f being PartFunc of REAL,REAL for X being set holds ( f is_strictly_convex_on X iff f - r is_strictly_convex_on X ) proof let r be Real; ::_thesis: for f being PartFunc of REAL,REAL for X being set holds ( f is_strictly_convex_on X iff f - r is_strictly_convex_on X ) let f be PartFunc of REAL,REAL; ::_thesis: for X being set holds ( f is_strictly_convex_on X iff f - r is_strictly_convex_on X ) let X be set ; ::_thesis: ( f is_strictly_convex_on X iff f - r is_strictly_convex_on X ) A1: dom (f - r) = dom f by VALUED_1:3; A2: for x being Element of REAL st x in dom (f - r) holds ((f - r) - (- r)) . x = f . x proof let x be Element of REAL ; ::_thesis: ( x in dom (f - r) implies ((f - r) - (- r)) . x = f . x ) assume A3: x in dom (f - r) ; ::_thesis: ((f - r) - (- r)) . x = f . x then ((f - r) - (- r)) . x = ((f - r) . x) - (- r) by VALUED_1:3 .= ((f - r) . x) + r .= ((f . x) - r) + r by A1, A3, VALUED_1:3 .= (f . x) - (r - r) ; hence ((f - r) - (- r)) . x = f . x ; ::_thesis: verum end; dom ((f - r) - (- r)) = dom (f - r) by VALUED_1:3; then (f - r) - (- r) = f by A1, A2, PARTFUN1:5; hence ( f is_strictly_convex_on X iff f - r is_strictly_convex_on X ) by Lm1; ::_thesis: verum end; Lm2: for r being Real for f being PartFunc of REAL,REAL for X being set st 0 < r & f is_strictly_convex_on X holds r (#) f is_strictly_convex_on X proof let r be Real; ::_thesis: for f being PartFunc of REAL,REAL for X being set st 0 < r & f is_strictly_convex_on X holds r (#) f is_strictly_convex_on X let f be PartFunc of REAL,REAL; ::_thesis: for X being set st 0 < r & f is_strictly_convex_on X holds r (#) f is_strictly_convex_on X let X be set ; ::_thesis: ( 0 < r & f is_strictly_convex_on X implies r (#) f is_strictly_convex_on X ) assume A1: 0 < r ; ::_thesis: ( not f is_strictly_convex_on X or r (#) f is_strictly_convex_on X ) assume A2: f is_strictly_convex_on X ; ::_thesis: r (#) f is_strictly_convex_on X then X c= dom f by Def1; then A3: X c= dom (r (#) f) by VALUED_1:def_5; for p being Real st 0 < p & p < 1 holds for t, s being Real st t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s holds (r (#) f) . ((p * t) + ((1 - p) * s)) < (p * ((r (#) f) . t)) + ((1 - p) * ((r (#) f) . s)) proof let p be Real; ::_thesis: ( 0 < p & p < 1 implies for t, s being Real st t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s holds (r (#) f) . ((p * t) + ((1 - p) * s)) < (p * ((r (#) f) . t)) + ((1 - p) * ((r (#) f) . s)) ) assume A4: ( 0 < p & p < 1 ) ; ::_thesis: for t, s being Real st t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s holds (r (#) f) . ((p * t) + ((1 - p) * s)) < (p * ((r (#) f) . t)) + ((1 - p) * ((r (#) f) . s)) for t, s being Real st t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s holds (r (#) f) . ((p * t) + ((1 - p) * s)) < (p * ((r (#) f) . t)) + ((1 - p) * ((r (#) f) . s)) proof let t, s be Real; ::_thesis: ( t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s implies (r (#) f) . ((p * t) + ((1 - p) * s)) < (p * ((r (#) f) . t)) + ((1 - p) * ((r (#) f) . s)) ) assume that A5: ( t in X & s in X ) and A6: (p * t) + ((1 - p) * s) in X and A7: t <> s ; ::_thesis: (r (#) f) . ((p * t) + ((1 - p) * s)) < (p * ((r (#) f) . t)) + ((1 - p) * ((r (#) f) . s)) f . ((p * t) + ((1 - p) * s)) < (p * (f . t)) + ((1 - p) * (f . s)) by A2, A4, A5, A6, A7, Def1; then A8: r * (f . ((p * t) + ((1 - p) * s))) < r * ((p * (f . t)) + ((1 - p) * (f . s))) by A1, XREAL_1:68; ( p * ((r (#) f) . t) = p * (r * (f . t)) & (1 - p) * ((r (#) f) . s) = (1 - p) * (r * (f . s)) ) by A3, A5, VALUED_1:def_5; hence (r (#) f) . ((p * t) + ((1 - p) * s)) < (p * ((r (#) f) . t)) + ((1 - p) * ((r (#) f) . s)) by A3, A6, A8, VALUED_1:def_5; ::_thesis: verum end; hence for t, s being Real st t in X & s in X & (p * t) + ((1 - p) * s) in X & t <> s holds (r (#) f) . ((p * t) + ((1 - p) * s)) < (p * ((r (#) f) . t)) + ((1 - p) * ((r (#) f) . s)) ; ::_thesis: verum end; hence r (#) f is_strictly_convex_on X by A3, Def1; ::_thesis: verum end; theorem Th12: :: RFUNCT_4:12 for r being Real for f being PartFunc of REAL,REAL for X being set st 0 < r holds ( f is_strictly_convex_on X iff r (#) f is_strictly_convex_on X ) proof let r be Real; ::_thesis: for f being PartFunc of REAL,REAL for X being set st 0 < r holds ( f is_strictly_convex_on X iff r (#) f is_strictly_convex_on X ) let f be PartFunc of REAL,REAL; ::_thesis: for X being set st 0 < r holds ( f is_strictly_convex_on X iff r (#) f is_strictly_convex_on X ) let X be set ; ::_thesis: ( 0 < r implies ( f is_strictly_convex_on X iff r (#) f is_strictly_convex_on X ) ) A1: dom ((1 / r) (#) (r (#) f)) = dom (r (#) f) by VALUED_1:def_5; assume A2: 0 < r ; ::_thesis: ( f is_strictly_convex_on X iff r (#) f is_strictly_convex_on X ) A3: for x being Element of REAL st x in dom (r (#) f) holds ((1 / r) (#) (r (#) f)) . x = f . x proof let x be Element of REAL ; ::_thesis: ( x in dom (r (#) f) implies ((1 / r) (#) (r (#) f)) . x = f . x ) assume A4: x in dom (r (#) f) ; ::_thesis: ((1 / r) (#) (r (#) f)) . x = f . x then ((1 / r) (#) (r (#) f)) . x = (1 / r) * ((r (#) f) . x) by A1, VALUED_1:def_5 .= (1 / r) * (r * (f . x)) by A4, VALUED_1:def_5 .= ((1 / r) * r) * (f . x) .= 1 * (f . x) by A2, XCMPLX_1:106 ; hence ((1 / r) (#) (r (#) f)) . x = f . x ; ::_thesis: verum end; dom (r (#) f) = dom f by VALUED_1:def_5; then (1 / r) (#) (r (#) f) = f by A1, A3, PARTFUN1:5; hence ( f is_strictly_convex_on X iff r (#) f is_strictly_convex_on X ) by A2, Lm2, XREAL_1:139; ::_thesis: verum end; theorem Th13: :: RFUNCT_4:13 for f, g being PartFunc of REAL,REAL for X being set st f is_strictly_convex_on X & g is_strictly_convex_on X holds f + g is_strictly_convex_on X proof let f, g be PartFunc of REAL,REAL; ::_thesis: for X being set st f is_strictly_convex_on X & g is_strictly_convex_on X holds f + g is_strictly_convex_on X let X be set ; ::_thesis: ( f is_strictly_convex_on X & g is_strictly_convex_on X implies f + g is_strictly_convex_on X ) assume A1: ( f is_strictly_convex_on X & g is_strictly_convex_on X ) ; ::_thesis: f + g is_strictly_convex_on X then ( X c= dom f & X c= dom g ) by Def1; then X c= (dom f) /\ (dom g) by XBOOLE_1:19; then A2: X c= dom (f + g) by VALUED_1:def_1; for p being Real st 0 < p & p < 1 holds for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds (f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) proof let p be Real; ::_thesis: ( 0 < p & p < 1 implies for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds (f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) ) assume A3: ( 0 < p & p < 1 ) ; ::_thesis: for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds (f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds (f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) proof let r, s be Real; ::_thesis: ( r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s implies (f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) ) assume that A4: r in X and A5: s in X and A6: (p * r) + ((1 - p) * s) in X and A7: r <> s ; ::_thesis: (f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) A8: ( (f + g) . ((p * r) + ((1 - p) * s)) = (f . ((p * r) + ((1 - p) * s))) + (g . ((p * r) + ((1 - p) * s))) & (f + g) . r = (f . r) + (g . r) ) by A2, A4, A6, VALUED_1:def_1; A9: ( ((p * (f . r)) + ((1 - p) * (f . s))) + ((p * (g . r)) + ((1 - p) * (g . s))) = (p * ((f . r) + (g . r))) + ((1 - p) * ((f . s) + (g . s))) & (f + g) . s = (f . s) + (g . s) ) by A2, A5, VALUED_1:def_1; ( f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) & g . ((p * r) + ((1 - p) * s)) < (p * (g . r)) + ((1 - p) * (g . s)) ) by A1, A3, A4, A5, A6, A7, Def1; hence (f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) by A8, A9, XREAL_1:8; ::_thesis: verum end; hence for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds (f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) ; ::_thesis: verum end; hence f + g is_strictly_convex_on X by A2, Def1; ::_thesis: verum end; theorem Th14: :: RFUNCT_4:14 for f, g being PartFunc of REAL,REAL for X being set st f is_strictly_convex_on X & g is_convex_on X holds f + g is_strictly_convex_on X proof let f, g be PartFunc of REAL,REAL; ::_thesis: for X being set st f is_strictly_convex_on X & g is_convex_on X holds f + g is_strictly_convex_on X let X be set ; ::_thesis: ( f is_strictly_convex_on X & g is_convex_on X implies f + g is_strictly_convex_on X ) assume A1: ( f is_strictly_convex_on X & g is_convex_on X ) ; ::_thesis: f + g is_strictly_convex_on X then ( X c= dom f & X c= dom g ) by Def1, RFUNCT_3:def_12; then X c= (dom f) /\ (dom g) by XBOOLE_1:19; then A2: X c= dom (f + g) by VALUED_1:def_1; for p being Real st 0 < p & p < 1 holds for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds (f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) proof let p be Real; ::_thesis: ( 0 < p & p < 1 implies for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds (f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) ) assume A3: ( 0 < p & p < 1 ) ; ::_thesis: for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds (f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds (f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) proof let r, s be Real; ::_thesis: ( r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s implies (f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) ) assume that A4: r in X and A5: s in X and A6: (p * r) + ((1 - p) * s) in X and A7: r <> s ; ::_thesis: (f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) A8: ( (f + g) . ((p * r) + ((1 - p) * s)) = (f . ((p * r) + ((1 - p) * s))) + (g . ((p * r) + ((1 - p) * s))) & (f + g) . r = (f . r) + (g . r) ) by A2, A4, A6, VALUED_1:def_1; A9: ( ((p * (f . r)) + ((1 - p) * (f . s))) + ((p * (g . r)) + ((1 - p) * (g . s))) = (p * ((f . r) + (g . r))) + ((1 - p) * ((f . s) + (g . s))) & (f + g) . s = (f . s) + (g . s) ) by A2, A5, VALUED_1:def_1; ( f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) & g . ((p * r) + ((1 - p) * s)) <= (p * (g . r)) + ((1 - p) * (g . s)) ) by A1, A3, A4, A5, A6, A7, Def1, RFUNCT_3:def_12; hence (f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) by A8, A9, XREAL_1:8; ::_thesis: verum end; hence for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds (f + g) . ((p * r) + ((1 - p) * s)) < (p * ((f + g) . r)) + ((1 - p) * ((f + g) . s)) ; ::_thesis: verum end; hence f + g is_strictly_convex_on X by A2, Def1; ::_thesis: verum end; theorem :: RFUNCT_4:15 for a, b being Real for f, g being PartFunc of REAL,REAL for X being set st f is_strictly_convex_on X & g is_strictly_convex_on X & ( ( a > 0 & b >= 0 ) or ( a >= 0 & b > 0 ) ) holds (a (#) f) + (b (#) g) is_strictly_convex_on X proof let a, b be Real; ::_thesis: for f, g being PartFunc of REAL,REAL for X being set st f is_strictly_convex_on X & g is_strictly_convex_on X & ( ( a > 0 & b >= 0 ) or ( a >= 0 & b > 0 ) ) holds (a (#) f) + (b (#) g) is_strictly_convex_on X let f, g be PartFunc of REAL,REAL; ::_thesis: for X being set st f is_strictly_convex_on X & g is_strictly_convex_on X & ( ( a > 0 & b >= 0 ) or ( a >= 0 & b > 0 ) ) holds (a (#) f) + (b (#) g) is_strictly_convex_on X let X be set ; ::_thesis: ( f is_strictly_convex_on X & g is_strictly_convex_on X & ( ( a > 0 & b >= 0 ) or ( a >= 0 & b > 0 ) ) implies (a (#) f) + (b (#) g) is_strictly_convex_on X ) assume that A1: f is_strictly_convex_on X and A2: g is_strictly_convex_on X and A3: ( ( a > 0 & b >= 0 ) or ( a >= 0 & b > 0 ) ) ; ::_thesis: (a (#) f) + (b (#) g) is_strictly_convex_on X now__::_thesis:_(a_(#)_f)_+_(b_(#)_g)_is_strictly_convex_on_X percases ( ( a > 0 & b > 0 ) or ( a > 0 & b = 0 ) or ( a = 0 & b > 0 ) ) by A3; suppose ( a > 0 & b > 0 ) ; ::_thesis: (a (#) f) + (b (#) g) is_strictly_convex_on X then ( a (#) f is_strictly_convex_on X & b (#) g is_strictly_convex_on X ) by A1, A2, Th12; hence (a (#) f) + (b (#) g) is_strictly_convex_on X by Th13; ::_thesis: verum end; supposeA4: ( a > 0 & b = 0 ) ; ::_thesis: (a (#) f) + (b (#) g) is_strictly_convex_on X A5: X c= dom g by A2, Def1; a (#) f is_strictly_convex_on X by A1, A4, Th12; hence (a (#) f) + (b (#) g) is_strictly_convex_on X by A4, A5, Th14, RFUNCT_3:57; ::_thesis: verum end; supposeA6: ( a = 0 & b > 0 ) ; ::_thesis: (a (#) f) + (b (#) g) is_strictly_convex_on X A7: X c= dom f by A1, Def1; b (#) g is_strictly_convex_on X by A2, A6, Th12; hence (a (#) f) + (b (#) g) is_strictly_convex_on X by A6, A7, Th14, RFUNCT_3:57; ::_thesis: verum end; end; end; hence (a (#) f) + (b (#) g) is_strictly_convex_on X ; ::_thesis: verum end; theorem Th16: :: RFUNCT_4:16 for f being PartFunc of REAL,REAL for X being set holds ( f is_convex_on X iff ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds ( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ) ) ) proof let f be PartFunc of REAL,REAL; ::_thesis: for X being set holds ( f is_convex_on X iff ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds ( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ) ) ) let X be set ; ::_thesis: ( f is_convex_on X iff ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds ( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ) ) ) A1: ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds ( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ) implies f is_convex_on X ) proof assume that A2: X c= dom f and A3: for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds ( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ; ::_thesis: f is_convex_on X for p being Real st 0 <= p & p <= 1 holds for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) proof let p be Real; ::_thesis: ( 0 <= p & p <= 1 implies for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ) assume A4: ( 0 <= p & p <= 1 ) ; ::_thesis: for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) for s, t being Real st s in X & t in X & (p * s) + ((1 - p) * t) in X holds f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) proof let s, t be Real; ::_thesis: ( s in X & t in X & (p * s) + ((1 - p) * t) in X implies f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) ) assume A5: ( s in X & t in X & (p * s) + ((1 - p) * t) in X ) ; ::_thesis: f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) now__::_thesis:_f_._((p_*_s)_+_((1_-_p)_*_t))_<=_(p_*_(f_._s))_+_((1_-_p)_*_(f_._t)) percases ( p = 0 or p = 1 or ( 0 < p & p < 1 ) ) by A4, XXREAL_0:1; suppose p = 0 ; ::_thesis: f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) hence f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) ; ::_thesis: verum end; suppose p = 1 ; ::_thesis: f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) hence f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) ; ::_thesis: verum end; supposeA6: ( 0 < p & p < 1 ) ; ::_thesis: f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) then A7: 1 - p > 0 by XREAL_1:50; now__::_thesis:_f_._((p_*_s)_+_((1_-_p)_*_t))_<=_(p_*_(f_._s))_+_((1_-_p)_*_(f_._t)) percases ( s = t or s < t or s > t ) by XXREAL_0:1; suppose s = t ; ::_thesis: f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) hence f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) ; ::_thesis: verum end; suppose s < t ; ::_thesis: f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) then A8: t - s > 0 by XREAL_1:50; ((p * s) + ((1 - p) * t)) - s = (1 - p) * (t - s) ; then A9: ((p * s) + ((1 - p) * t)) - s > 0 by A7, A8, XREAL_1:129; then A10: (p * s) + ((1 - p) * t) > s by XREAL_1:47; A11: ( (((f . ((p * s) + ((1 - p) * t))) - (f . s)) * (t - s)) * p = (p * ((t - s) * (f . ((p * s) + ((1 - p) * t))))) - (p * ((t - s) * (f . s))) & (((f . t) - (f . ((p * s) + ((1 - p) * t)))) * (t - s)) * (1 - p) = ((1 - p) * ((t - s) * (f . t))) - ((1 - p) * ((t - s) * (f . ((p * s) + ((1 - p) * t))))) ) ; t - ((p * s) + ((1 - p) * t)) = p * (t - s) ; then A12: t - ((p * s) + ((1 - p) * t)) > 0 by A6, A8, XREAL_1:129; then (p * s) + ((1 - p) * t) < t by XREAL_1:47; then ( ((f . ((p * s) + ((1 - p) * t))) - (f . s)) / (((p * s) + ((1 - p) * t)) - s) <= ((f . t) - (f . s)) / (t - s) & ((f . t) - (f . s)) / (t - s) <= ((f . t) - (f . ((p * s) + ((1 - p) * t)))) / (t - ((p * s) + ((1 - p) * t))) ) by A3, A5, A10; then ((f . ((p * s) + ((1 - p) * t))) - (f . s)) / (((p * s) + ((1 - p) * t)) - s) <= ((f . t) - (f . ((p * s) + ((1 - p) * t)))) / (t - ((p * s) + ((1 - p) * t))) by XXREAL_0:2; then ((f . ((p * s) + ((1 - p) * t))) - (f . s)) * (t - ((p * s) + ((1 - p) * t))) <= ((f . t) - (f . ((p * s) + ((1 - p) * t)))) * (((p * s) + ((1 - p) * t)) - s) by A12, A9, XREAL_1:106; then (p * ((t - s) * (f . ((p * s) + ((1 - p) * t))))) + ((1 - p) * ((t - s) * (f . ((p * s) + ((1 - p) * t))))) <= ((1 - p) * ((t - s) * (f . t))) + (p * ((t - s) * (f . s))) by A11, XREAL_1:21; then f . ((p * s) + ((1 - p) * t)) <= ((((1 - p) * (f . t)) * (t - s)) + ((p * (f . s)) * (t - s))) / (t - s) by A8, XREAL_1:77; then f . ((p * s) + ((1 - p) * t)) <= ((((1 - p) * (f . t)) * (t - s)) / (t - s)) + (((p * (f . s)) * (t - s)) / (t - s)) by XCMPLX_1:62; then f . ((p * s) + ((1 - p) * t)) <= ((1 - p) * (f . t)) + (((p * (f . s)) * (t - s)) / (t - s)) by A8, XCMPLX_1:89; hence f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) by A8, XCMPLX_1:89; ::_thesis: verum end; suppose s > t ; ::_thesis: f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) then A13: s - t > 0 by XREAL_1:50; ((p * s) + ((1 - p) * t)) - t = p * (s - t) ; then A14: ((p * s) + ((1 - p) * t)) - t > 0 by A6, A13, XREAL_1:129; then A15: (p * s) + ((1 - p) * t) > t by XREAL_1:47; A16: ( (((f . ((p * s) + ((1 - p) * t))) - (f . t)) * (s - t)) * (1 - p) = ((1 - p) * ((s - t) * (f . ((p * s) + ((1 - p) * t))))) - ((1 - p) * ((s - t) * (f . t))) & (((f . s) - (f . ((p * s) + ((1 - p) * t)))) * (s - t)) * p = (p * ((s - t) * (f . s))) - (p * ((s - t) * (f . ((p * s) + ((1 - p) * t))))) ) ; s - ((p * s) + ((1 - p) * t)) = (1 - p) * (s - t) ; then A17: s - ((p * s) + ((1 - p) * t)) > 0 by A7, A13, XREAL_1:129; then (p * s) + ((1 - p) * t) < s by XREAL_1:47; then ( ((f . ((p * s) + ((1 - p) * t))) - (f . t)) / (((p * s) + ((1 - p) * t)) - t) <= ((f . s) - (f . t)) / (s - t) & ((f . s) - (f . t)) / (s - t) <= ((f . s) - (f . ((p * s) + ((1 - p) * t)))) / (s - ((p * s) + ((1 - p) * t))) ) by A3, A5, A15; then ((f . ((p * s) + ((1 - p) * t))) - (f . t)) / (((p * s) + ((1 - p) * t)) - t) <= ((f . s) - (f . ((p * s) + ((1 - p) * t)))) / (s - ((p * s) + ((1 - p) * t))) by XXREAL_0:2; then ((f . ((p * s) + ((1 - p) * t))) - (f . t)) * (s - ((p * s) + ((1 - p) * t))) <= ((f . s) - (f . ((p * s) + ((1 - p) * t)))) * (((p * s) + ((1 - p) * t)) - t) by A17, A14, XREAL_1:106; then ((1 - p) * ((s - t) * (f . ((p * s) + ((1 - p) * t))))) + (p * ((s - t) * (f . ((p * s) + ((1 - p) * t))))) <= (p * ((s - t) * (f . s))) + ((1 - p) * ((s - t) * (f . t))) by A16, XREAL_1:21; then f . ((p * s) + ((1 - p) * t)) <= (((p * (f . s)) * (s - t)) + (((1 - p) * (f . t)) * (s - t))) / (s - t) by A13, XREAL_1:77; then f . ((p * s) + ((1 - p) * t)) <= (((p * (f . s)) * (s - t)) / (s - t)) + ((((1 - p) * (f . t)) * (s - t)) / (s - t)) by XCMPLX_1:62; then f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((((1 - p) * (f . t)) * (s - t)) / (s - t)) by A13, XCMPLX_1:89; hence f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) by A13, XCMPLX_1:89; ::_thesis: verum end; end; end; hence f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) ; ::_thesis: verum end; end; end; hence f . ((p * s) + ((1 - p) * t)) <= (p * (f . s)) + ((1 - p) * (f . t)) ; ::_thesis: verum end; hence for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum end; hence f is_convex_on X by A2, RFUNCT_3:def_12; ::_thesis: verum end; ( f is_convex_on X implies ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds ( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ) ) ) proof assume A18: f is_convex_on X ; ::_thesis: ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds ( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ) ) for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds ( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) proof let a, b, r be Real; ::_thesis: ( a in X & b in X & r in X & a < r & r < b implies ( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ) assume that A19: ( a in X & b in X & r in X ) and A20: a < r and A21: r < b ; ::_thesis: ( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) A22: ( b - r < b - a & 0 < b - r ) by A20, A21, XREAL_1:10, XREAL_1:50; set p = (b - r) / (b - a); A23: 0 < r - a by A20, XREAL_1:50; A24: ((b - r) / (b - a)) + ((r - a) / (b - a)) = ((b - r) + (r - a)) / (b - a) by XCMPLX_1:62 .= 1 by A22, XCMPLX_1:60 ; then (((b - r) / (b - a)) * a) + ((1 - ((b - r) / (b - a))) * b) = ((a * (b - r)) / (b - a)) + (b * ((r - a) / (b - a))) by XCMPLX_1:74 .= ((a * (b - r)) / (b - a)) + ((b * (r - a)) / (b - a)) by XCMPLX_1:74 .= (((b * a) - (r * a)) + ((r - a) * b)) / (b - a) by XCMPLX_1:62 .= (r * (b - a)) / (b - a) ; then A25: (((b - r) / (b - a)) * a) + ((1 - ((b - r) / (b - a))) * b) = r by A22, XCMPLX_1:89; A26: (b - a) * ((((b - r) / (b - a)) * (f . a)) + (((r - a) / (b - a)) * (f . b))) = (((b - a) * ((b - r) / (b - a))) * (f . a)) + ((b - a) * (((r - a) / (b - a)) * (f . b))) .= ((b - r) * (f . a)) + (((b - a) * ((r - a) / (b - a))) * (f . b)) by A22, XCMPLX_1:87 .= ((b - r) * (f . a)) + ((r - a) * (f . b)) by A22, XCMPLX_1:87 ; (b - r) / (b - a) < 1 by A22, XREAL_1:189; then A27: f . ((((b - r) / (b - a)) * a) + ((1 - ((b - r) / (b - a))) * b)) <= (((b - r) / (b - a)) * (f . a)) + ((1 - ((b - r) / (b - a))) * (f . b)) by A18, A19, A22, A25, RFUNCT_3:def_12; then (b - a) * (f . r) <= ((b - a) * (f . a)) + (((r - a) * (f . b)) - ((r - a) * (f . a))) by A22, A24, A25, A26, XREAL_1:64; then ((b - a) * (f . r)) - ((b - a) * (f . a)) <= ((r - a) * (f . b)) - ((r - a) * (f . a)) by XREAL_1:20; then (b - a) * ((f . r) - (f . a)) <= (r - a) * ((f . b) - (f . a)) ; hence ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) by A22, A23, XREAL_1:102; ::_thesis: ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) (b - a) * (f . r) <= ((b - a) * (f . b)) - (((b - r) * (f . b)) - ((b - r) * (f . a))) by A22, A24, A25, A27, A26, XREAL_1:64; then (((b - r) * (f . b)) - ((b - r) * (f . a))) + ((b - a) * (f . r)) <= (b - a) * (f . b) by XREAL_1:19; then ((b - r) * (f . b)) - ((b - r) * (f . a)) <= ((b - a) * (f . b)) - ((b - a) * (f . r)) by XREAL_1:19; then (b - r) * ((f . b) - (f . a)) <= (b - a) * ((f . b) - (f . r)) ; hence ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) by A22, XREAL_1:102; ::_thesis: verum end; hence ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds ( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ) ) by A18, RFUNCT_3:def_12; ::_thesis: verum end; hence ( f is_convex_on X iff ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds ( ((f . r) - (f . a)) / (r - a) <= ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) <= ((f . b) - (f . r)) / (b - r) ) ) ) ) by A1; ::_thesis: verum end; theorem :: RFUNCT_4:17 for f being PartFunc of REAL,REAL for X being set holds ( f is_strictly_convex_on X iff ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds ( ((f . r) - (f . a)) / (r - a) < ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r) ) ) ) ) proof let f be PartFunc of REAL,REAL; ::_thesis: for X being set holds ( f is_strictly_convex_on X iff ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds ( ((f . r) - (f . a)) / (r - a) < ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r) ) ) ) ) let X be set ; ::_thesis: ( f is_strictly_convex_on X iff ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds ( ((f . r) - (f . a)) / (r - a) < ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r) ) ) ) ) A1: ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds ( ((f . r) - (f . a)) / (r - a) < ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r) ) ) implies f is_strictly_convex_on X ) proof assume that A2: X c= dom f and A3: for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds ( ((f . r) - (f . a)) / (r - a) < ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r) ) ; ::_thesis: f is_strictly_convex_on X for p being Real st 0 < p & p < 1 holds for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) proof let p be Real; ::_thesis: ( 0 < p & p < 1 implies for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ) assume that A4: 0 < p and A5: p < 1 ; ::_thesis: for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) A6: 1 - p > 0 by A5, XREAL_1:50; for s, t being Real st s in X & t in X & (p * s) + ((1 - p) * t) in X & s <> t holds f . ((p * s) + ((1 - p) * t)) < (p * (f . s)) + ((1 - p) * (f . t)) proof let s, t be Real; ::_thesis: ( s in X & t in X & (p * s) + ((1 - p) * t) in X & s <> t implies f . ((p * s) + ((1 - p) * t)) < (p * (f . s)) + ((1 - p) * (f . t)) ) assume that A7: ( s in X & t in X & (p * s) + ((1 - p) * t) in X ) and A8: s <> t ; ::_thesis: f . ((p * s) + ((1 - p) * t)) < (p * (f . s)) + ((1 - p) * (f . t)) now__::_thesis:_f_._((p_*_s)_+_((1_-_p)_*_t))_<_(p_*_(f_._s))_+_((1_-_p)_*_(f_._t)) percases ( s < t or s > t ) by A8, XXREAL_0:1; suppose s < t ; ::_thesis: f . ((p * s) + ((1 - p) * t)) < (p * (f . s)) + ((1 - p) * (f . t)) then A9: t - s > 0 by XREAL_1:50; ((p * s) + ((1 - p) * t)) - s = (1 - p) * (t - s) ; then A10: ((p * s) + ((1 - p) * t)) - s > 0 by A6, A9, XREAL_1:129; then A11: (p * s) + ((1 - p) * t) > s by XREAL_1:47; A12: ( (((f . ((p * s) + ((1 - p) * t))) - (f . s)) * (t - s)) * p = (p * ((t - s) * (f . ((p * s) + ((1 - p) * t))))) - (p * ((t - s) * (f . s))) & (((f . t) - (f . ((p * s) + ((1 - p) * t)))) * (t - s)) * (1 - p) = ((1 - p) * ((t - s) * (f . t))) - ((1 - p) * ((t - s) * (f . ((p * s) + ((1 - p) * t))))) ) ; t - ((p * s) + ((1 - p) * t)) = p * (t - s) ; then A13: t - ((p * s) + ((1 - p) * t)) > 0 by A4, A9, XREAL_1:129; then (p * s) + ((1 - p) * t) < t by XREAL_1:47; then ( ((f . ((p * s) + ((1 - p) * t))) - (f . s)) / (((p * s) + ((1 - p) * t)) - s) < ((f . t) - (f . s)) / (t - s) & ((f . t) - (f . s)) / (t - s) < ((f . t) - (f . ((p * s) + ((1 - p) * t)))) / (t - ((p * s) + ((1 - p) * t))) ) by A3, A7, A11; then ((f . ((p * s) + ((1 - p) * t))) - (f . s)) / (((p * s) + ((1 - p) * t)) - s) < ((f . t) - (f . ((p * s) + ((1 - p) * t)))) / (t - ((p * s) + ((1 - p) * t))) by XXREAL_0:2; then ((f . ((p * s) + ((1 - p) * t))) - (f . s)) * (t - ((p * s) + ((1 - p) * t))) < ((f . t) - (f . ((p * s) + ((1 - p) * t)))) * (((p * s) + ((1 - p) * t)) - s) by A13, A10, XREAL_1:102; then (p * ((t - s) * (f . ((p * s) + ((1 - p) * t))))) + ((1 - p) * ((t - s) * (f . ((p * s) + ((1 - p) * t))))) < ((1 - p) * ((t - s) * (f . t))) + (p * ((t - s) * (f . s))) by A12, XREAL_1:21; then f . ((p * s) + ((1 - p) * t)) < ((((1 - p) * (f . t)) * (t - s)) + ((p * (f . s)) * (t - s))) / (t - s) by A9, XREAL_1:81; then f . ((p * s) + ((1 - p) * t)) < ((((1 - p) * (f . t)) * (t - s)) / (t - s)) + (((p * (f . s)) * (t - s)) / (t - s)) by XCMPLX_1:62; then f . ((p * s) + ((1 - p) * t)) < ((1 - p) * (f . t)) + (((p * (f . s)) * (t - s)) / (t - s)) by A9, XCMPLX_1:89; hence f . ((p * s) + ((1 - p) * t)) < (p * (f . s)) + ((1 - p) * (f . t)) by A9, XCMPLX_1:89; ::_thesis: verum end; suppose s > t ; ::_thesis: f . ((p * s) + ((1 - p) * t)) < (p * (f . s)) + ((1 - p) * (f . t)) then A14: s - t > 0 by XREAL_1:50; ((p * s) + ((1 - p) * t)) - t = p * (s - t) ; then A15: ((p * s) + ((1 - p) * t)) - t > 0 by A4, A14, XREAL_1:129; then A16: (p * s) + ((1 - p) * t) > t by XREAL_1:47; A17: ( (((f . ((p * s) + ((1 - p) * t))) - (f . t)) * (s - t)) * (1 - p) = ((1 - p) * ((s - t) * (f . ((p * s) + ((1 - p) * t))))) - ((1 - p) * ((s - t) * (f . t))) & (((f . s) - (f . ((p * s) + ((1 - p) * t)))) * (s - t)) * p = (p * ((s - t) * (f . s))) - (p * ((s - t) * (f . ((p * s) + ((1 - p) * t))))) ) ; s - ((p * s) + ((1 - p) * t)) = (1 - p) * (s - t) ; then A18: s - ((p * s) + ((1 - p) * t)) > 0 by A6, A14, XREAL_1:129; then (p * s) + ((1 - p) * t) < s by XREAL_1:47; then ( ((f . ((p * s) + ((1 - p) * t))) - (f . t)) / (((p * s) + ((1 - p) * t)) - t) < ((f . s) - (f . t)) / (s - t) & ((f . s) - (f . t)) / (s - t) < ((f . s) - (f . ((p * s) + ((1 - p) * t)))) / (s - ((p * s) + ((1 - p) * t))) ) by A3, A7, A16; then ((f . ((p * s) + ((1 - p) * t))) - (f . t)) / (((p * s) + ((1 - p) * t)) - t) < ((f . s) - (f . ((p * s) + ((1 - p) * t)))) / (s - ((p * s) + ((1 - p) * t))) by XXREAL_0:2; then ((f . ((p * s) + ((1 - p) * t))) - (f . t)) * (s - ((p * s) + ((1 - p) * t))) < ((f . s) - (f . ((p * s) + ((1 - p) * t)))) * (((p * s) + ((1 - p) * t)) - t) by A18, A15, XREAL_1:102; then ((1 - p) * ((s - t) * (f . ((p * s) + ((1 - p) * t))))) + (p * ((s - t) * (f . ((p * s) + ((1 - p) * t))))) < (p * ((s - t) * (f . s))) + ((1 - p) * ((s - t) * (f . t))) by A17, XREAL_1:21; then f . ((p * s) + ((1 - p) * t)) < (((p * (f . s)) * (s - t)) + (((1 - p) * (f . t)) * (s - t))) / (s - t) by A14, XREAL_1:81; then f . ((p * s) + ((1 - p) * t)) < (((p * (f . s)) * (s - t)) / (s - t)) + ((((1 - p) * (f . t)) * (s - t)) / (s - t)) by XCMPLX_1:62; then f . ((p * s) + ((1 - p) * t)) < (p * (f . s)) + ((((1 - p) * (f . t)) * (s - t)) / (s - t)) by A14, XCMPLX_1:89; hence f . ((p * s) + ((1 - p) * t)) < (p * (f . s)) + ((1 - p) * (f . t)) by A14, XCMPLX_1:89; ::_thesis: verum end; end; end; hence f . ((p * s) + ((1 - p) * t)) < (p * (f . s)) + ((1 - p) * (f . t)) ; ::_thesis: verum end; hence for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) ; ::_thesis: verum end; hence f is_strictly_convex_on X by A2, Def1; ::_thesis: verum end; ( f is_strictly_convex_on X implies ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds ( ((f . r) - (f . a)) / (r - a) < ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r) ) ) ) ) proof assume A19: f is_strictly_convex_on X ; ::_thesis: ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds ( ((f . r) - (f . a)) / (r - a) < ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r) ) ) ) for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds ( ((f . r) - (f . a)) / (r - a) < ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r) ) proof let a, b, r be Real; ::_thesis: ( a in X & b in X & r in X & a < r & r < b implies ( ((f . r) - (f . a)) / (r - a) < ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r) ) ) assume that A20: ( a in X & b in X & r in X ) and A21: a < r and A22: r < b ; ::_thesis: ( ((f . r) - (f . a)) / (r - a) < ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r) ) set p = (b - r) / (b - a); A23: ( b - r < b - a & 0 < b - r ) by A21, A22, XREAL_1:10, XREAL_1:50; A24: ((b - r) / (b - a)) + ((r - a) / (b - a)) = ((b - r) + (r - a)) / (b - a) by XCMPLX_1:62 .= 1 by A23, XCMPLX_1:60 ; then (((b - r) / (b - a)) * a) + ((1 - ((b - r) / (b - a))) * b) = ((a * (b - r)) / (b - a)) + (b * ((r - a) / (b - a))) by XCMPLX_1:74 .= ((a * (b - r)) / (b - a)) + ((b * (r - a)) / (b - a)) by XCMPLX_1:74 .= (((b * a) - (r * a)) + ((r - a) * b)) / (b - a) by XCMPLX_1:62 .= (r * (b - a)) / (b - a) ; then A25: (((b - r) / (b - a)) * a) + ((1 - ((b - r) / (b - a))) * b) = r by A23, XCMPLX_1:89; ( 0 < (b - r) / (b - a) & (b - r) / (b - a) < 1 ) by A23, XREAL_1:139, XREAL_1:189; then A26: f . r < (((b - r) / (b - a)) * (f . a)) + ((1 - ((b - r) / (b - a))) * (f . b)) by A19, A20, A21, A22, A25, Def1; A27: 0 < r - a by A21, XREAL_1:50; A28: ((((b - r) / (b - a)) * (f . a)) + ((1 - ((b - r) / (b - a))) * (f . b))) * (b - a) = (((b - a) * ((b - r) / (b - a))) * (f . a)) + ((b - a) * ((1 - ((b - r) / (b - a))) * (f . b))) .= ((((b - a) * (b - r)) / (b - a)) * (f . a)) + (((b - a) * ((r - a) / (b - a))) * (f . b)) by A24, XCMPLX_1:74 .= ((((b - r) * (b - a)) / (b - a)) * (f . a)) + ((((b - a) * (r - a)) / (b - a)) * (f . b)) by XCMPLX_1:74 .= (((b - r) * ((b - a) / (b - a))) * (f . a)) + ((((b - a) * (r - a)) / (b - a)) * (f . b)) by XCMPLX_1:74 .= (((b - r) * 1) * (f . a)) + ((((r - a) * (b - a)) / (b - a)) * (f . b)) by A23, XCMPLX_1:60 .= ((b - r) * (f . a)) + (((r - a) * ((b - a) / (b - a))) * (f . b)) by XCMPLX_1:74 .= ((b - r) * (f . a)) + (((r - a) * 1) * (f . b)) by A23, XCMPLX_1:60 ; then (f . r) * (b - a) < ((b - a) * (f . a)) + (((r - a) * (f . b)) - ((r - a) * (f . a))) by A23, A26, XREAL_1:68; then ((f . r) * (b - a)) - ((b - a) * (f . a)) < ((r - a) * (f . b)) - ((r - a) * (f . a)) by XREAL_1:19; then (b - a) * ((f . r) - (f . a)) < (r - a) * ((f . b) - (f . a)) ; hence ((f . r) - (f . a)) / (r - a) < ((f . b) - (f . a)) / (b - a) by A23, A27, XREAL_1:106; ::_thesis: ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r) (f . r) * (b - a) < (((r - b) * (f . b)) + ((b - r) * (f . a))) + ((b - a) * (f . b)) by A23, A26, A28, XREAL_1:68; then ((f . r) * (b - a)) - (((r - b) * (f . b)) + ((b - r) * (f . a))) < (b - a) * (f . b) by XREAL_1:19; then ((f . r) * (b - a)) + (- (((r - b) * (f . b)) + ((b - r) * (f . a)))) < (b - a) * (f . b) ; then (- ((r - b) * (f . b))) - ((b - r) * (f . a)) < ((b - a) * (f . b)) - ((b - a) * (f . r)) by XREAL_1:20; then (b - r) * ((f . b) - (f . a)) < (b - a) * ((f . b) - (f . r)) ; hence ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r) by A23, XREAL_1:106; ::_thesis: verum end; hence ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds ( ((f . r) - (f . a)) / (r - a) < ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r) ) ) ) by A19, Def1; ::_thesis: verum end; hence ( f is_strictly_convex_on X iff ( X c= dom f & ( for a, b, r being Real st a in X & b in X & r in X & a < r & r < b holds ( ((f . r) - (f . a)) / (r - a) < ((f . b) - (f . a)) / (b - a) & ((f . b) - (f . a)) / (b - a) < ((f . b) - (f . r)) / (b - r) ) ) ) ) by A1; ::_thesis: verum end; theorem :: RFUNCT_4:18 for f being PartFunc of REAL,REAL st f is total holds ( ( for n being Element of NAT for P, E, F being Element of n -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds ( P . i >= 0 & F . i = f . (E . i) ) ) holds f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ) iff f is_convex_on REAL ) proof let f be PartFunc of REAL,REAL; ::_thesis: ( f is total implies ( ( for n being Element of NAT for P, E, F being Element of n -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds ( P . i >= 0 & F . i = f . (E . i) ) ) holds f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ) iff f is_convex_on REAL ) ) A1: ( f is_convex_on REAL implies for n being Element of NAT for P, E, F being Element of n -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds ( P . i >= 0 & F . i = f . (E . i) ) ) holds f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ) proof assume A2: f is_convex_on REAL ; ::_thesis: for n being Element of NAT for P, E, F being Element of n -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds ( P . i >= 0 & F . i = f . (E . i) ) ) holds f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) for n being Element of NAT for P, E, F being Element of n -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds ( P . i >= 0 & F . i = f . (E . i) ) ) holds f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) proof defpred S1[ Element of NAT ] means for P, E, F being Element of \$1 -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds ( P . i >= 0 & F . i = f . (E . i) ) ) holds f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)); A3: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: for P, E, F being Element of k -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds ( P . i >= 0 & F . i = f . (E . i) ) ) holds f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ; ::_thesis: S1[k + 1] for P, E, F being Element of (k + 1) -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds ( P . i >= 0 & F . i = f . (E . i) ) ) holds f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) proof let P, E, F be Element of (k + 1) -tuples_on REAL; ::_thesis: ( Sum P = 1 & ( for i being Element of NAT st i in dom P holds ( P . i >= 0 & F . i = f . (E . i) ) ) implies f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ) assume that A5: Sum P = 1 and A6: for i being Element of NAT st i in dom P holds ( P . i >= 0 & F . i = f . (E . i) ) ; ::_thesis: f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) consider E1 being Element of k -tuples_on REAL, e1 being Real such that A7: E = E1 ^ <*e1*> by FINSEQ_2:117; consider F1 being Element of k -tuples_on REAL, f1 being Real such that A8: F = F1 ^ <*f1*> by FINSEQ_2:117; (len F1) + 1 = k + 1 by CARD_1:def_7 .= len P by CARD_1:def_7 ; then (len F1) + 1 in Seg (len P) by FINSEQ_1:4; then A9: (len F1) + 1 in dom P by FINSEQ_1:def_3; A10: f1 = F . ((len F1) + 1) by A8, FINSEQ_1:42 .= f . (E . ((len F1) + 1)) by A6, A9 .= f . (E . (k + 1)) by CARD_1:def_7 .= f . (E . ((len E1) + 1)) by CARD_1:def_7 .= f . e1 by A7, FINSEQ_1:42 ; consider P1 being Element of k -tuples_on REAL, p1 being Real such that A11: P = P1 ^ <*p1*> by FINSEQ_2:117; mlt (P,F) = (mlt (P1,F1)) ^ <*(p1 * f1)*> by A11, A8, Th2; then A12: Sum (mlt (P,F)) = (1 * (Sum (mlt (P1,F1)))) + (p1 * f1) by RVSUM_1:74; mlt (P,E) = (mlt (P1,E1)) ^ <*(p1 * e1)*> by A11, A7, Th2; then A13: Sum (mlt (P,E)) = (1 * (Sum (mlt (P1,E1)))) + (p1 * e1) by RVSUM_1:74; A14: for i being Nat st i in dom P1 holds P1 . i >= 0 proof let i be Nat; ::_thesis: ( i in dom P1 implies P1 . i >= 0 ) assume A15: i in dom P1 ; ::_thesis: P1 . i >= 0 A16: i in Seg (len P1) by A15, FINSEQ_1:def_3; then A17: 1 <= i by FINSEQ_1:1; i <= len P1 by A16, FINSEQ_1:1; then A18: i <= k by CARD_1:def_7; k <= k + 1 by NAT_1:11; then i <= k + 1 by A18, XXREAL_0:2; then i in Seg (k + 1) by A17, FINSEQ_1:1; then i in Seg (len P) by CARD_1:def_7; then A19: i in dom P by FINSEQ_1:def_3; P1 . i = P . i by A11, A15, FINSEQ_1:def_7; hence P1 . i >= 0 by A6, A19; ::_thesis: verum end; then A20: for i being Element of NAT st i in dom P1 holds P1 . i >= 0 ; now__::_thesis:_f_._(Sum_(mlt_(P,E)))_<=_Sum_(mlt_(P,F)) percases ( Sum P1 = 0 or Sum P1 <> 0 ) ; supposeA21: Sum P1 = 0 ; ::_thesis: f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) then for i being Element of NAT st i in dom P1 holds P1 . i = 0 by A20, Th3; then A22: P1 = k |-> 0 by Th4; then mlt (P1,E1) = k |-> 0 by Th5; then A23: Sum (mlt (P1,E1)) = k * 0 by RVSUM_1:80; mlt (P1,F1) = k |-> 0 by A22, Th5; then A24: Sum (mlt (P1,F1)) = k * 0 by RVSUM_1:80; Sum P = 0 + p1 by A11, A21, RVSUM_1:74; hence f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) by A5, A13, A12, A10, A23, A24; ::_thesis: verum end; supposeA25: Sum P1 <> 0 ; ::_thesis: f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) A26: 0 <= Sum P1 by A14, RVSUM_1:84; A27: for i being Element of NAT st i in dom (((Sum P1) ") * P1) holds ( (((Sum P1) ") * P1) . i >= 0 & F1 . i = f . (E1 . i) ) proof let i be Element of NAT ; ::_thesis: ( i in dom (((Sum P1) ") * P1) implies ( (((Sum P1) ") * P1) . i >= 0 & F1 . i = f . (E1 . i) ) ) assume i in dom (((Sum P1) ") * P1) ; ::_thesis: ( (((Sum P1) ") * P1) . i >= 0 & F1 . i = f . (E1 . i) ) then A28: i in Seg (len (((Sum P1) ") * P1)) by FINSEQ_1:def_3; then A29: i in Seg k by CARD_1:def_7; then A30: i in Seg (len P1) by CARD_1:def_7; then i <= len P1 by FINSEQ_1:1; then A31: i <= k by CARD_1:def_7; A32: 1 <= i by A28, FINSEQ_1:1; k <= k + 1 by NAT_1:11; then i <= k + 1 by A31, XXREAL_0:2; then i in Seg (k + 1) by A32, FINSEQ_1:1; then i in Seg (len P) by CARD_1:def_7; then A33: i in dom P by FINSEQ_1:def_3; i in dom P1 by A30, FINSEQ_1:def_3; then ( (((Sum P1) ") * P1) . i = ((Sum P1) ") * (P1 . i) & P1 . i >= 0 ) by A14, RVSUM_1:45; hence (((Sum P1) ") * P1) . i >= 0 by A26; ::_thesis: F1 . i = f . (E1 . i) i in Seg (len E1) by A29, CARD_1:def_7; then i in dom E1 by FINSEQ_1:def_3; then A34: E . i = E1 . i by A7, FINSEQ_1:def_7; i in Seg (len F1) by A29, CARD_1:def_7; then i in dom F1 by FINSEQ_1:def_3; then F . i = F1 . i by A8, FINSEQ_1:def_7; hence F1 . i = f . (E1 . i) by A6, A33, A34; ::_thesis: verum end; A35: Sum (mlt (P,E)) = (((Sum P1) * ((Sum P1) ")) * (Sum (mlt (P1,E1)))) + (p1 * e1) by A13, A25, XCMPLX_0:def_7 .= ((Sum P1) * (((Sum P1) ") * (Sum (mlt (P1,E1))))) + (p1 * e1) .= ((Sum P1) * (Sum (((Sum P1) ") * (mlt (P1,E1))))) + (p1 * e1) by RVSUM_1:87 .= ((Sum P1) * (Sum (mlt ((((Sum P1) ") * P1),E1)))) + (p1 * e1) by FINSEQOP:26 ; A36: ((Sum P1) ") * (Sum (mlt (P1,F1))) = Sum (((Sum P1) ") * (mlt (P1,F1))) by RVSUM_1:87 .= Sum (mlt ((((Sum P1) ") * P1),F1)) by FINSEQOP:26 ; (len P1) + 1 = len P by A11, FINSEQ_2:16; then (len P1) + 1 in Seg (len P) by FINSEQ_1:4; then A37: (len P1) + 1 in dom P by FINSEQ_1:def_3; (Sum P1) + p1 = 1 by A5, A11, RVSUM_1:74; then A38: p1 = 1 - (Sum P1) ; Sum (((Sum P1) ") * P1) = ((Sum P1) ") * (Sum P1) by RVSUM_1:87 .= 1 by A25, XCMPLX_0:def_7 ; then (Sum P1) * (f . (Sum (mlt ((((Sum P1) ") * P1),E1)))) <= (Sum P1) * (((Sum P1) ") * (Sum (mlt (P1,F1)))) by A4, A26, A36, A27, XREAL_1:64; then A39: ((Sum P1) * (f . (Sum (mlt ((((Sum P1) ") * P1),E1))))) + (p1 * (f . e1)) <= ((Sum P1) * (((Sum P1) ") * (Sum (mlt (P1,F1))))) + (p1 * (f . e1)) by XREAL_1:6; P . ((len P1) + 1) = p1 by A11, FINSEQ_1:42; then Sum P1 <= 1 by A6, A38, A37, XREAL_1:49; then f . (Sum (mlt (P,E))) <= ((Sum P1) * (f . (Sum (mlt ((((Sum P1) ") * P1),E1))))) + (p1 * (f . e1)) by A2, A35, A38, A26, RFUNCT_3:def_12; then f . (Sum (mlt (P,E))) <= (((Sum P1) * ((Sum P1) ")) * (Sum (mlt (P1,F1)))) + (p1 * (f . e1)) by A39, XXREAL_0:2; hence f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) by A12, A10, A25, XCMPLX_0:def_7; ::_thesis: verum end; end; end; hence f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; A40: S1[ 0 ] by RVSUM_1:79; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A40, A3); hence for n being Element of NAT for P, E, F being Element of n -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds ( P . i >= 0 & F . i = f . (E . i) ) ) holds f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ; ::_thesis: verum end; hence for n being Element of NAT for P, E, F being Element of n -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds ( P . i >= 0 & F . i = f . (E . i) ) ) holds f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ; ::_thesis: verum end; assume f is total ; ::_thesis: ( ( for n being Element of NAT for P, E, F being Element of n -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds ( P . i >= 0 & F . i = f . (E . i) ) ) holds f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ) iff f is_convex_on REAL ) then A41: REAL c= dom f by PARTFUN1:def_2; ( ( for n being Element of NAT for P, E, F being Element of n -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds ( P . i >= 0 & F . i = f . (E . i) ) ) holds f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ) implies f is_convex_on REAL ) proof assume A42: for n being Element of NAT for P, E, F being Element of n -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds ( P . i >= 0 & F . i = f . (E . i) ) ) holds f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ; ::_thesis: f is_convex_on REAL for p being Real st 0 <= p & p <= 1 holds for r, s being Real st r in REAL & s in REAL & (p * r) + ((1 - p) * s) in REAL holds f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) proof let p be Real; ::_thesis: ( 0 <= p & p <= 1 implies for r, s being Real st r in REAL & s in REAL & (p * r) + ((1 - p) * s) in REAL holds f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ) assume that A43: 0 <= p and A44: p <= 1 ; ::_thesis: for r, s being Real st r in REAL & s in REAL & (p * r) + ((1 - p) * s) in REAL holds f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) let r, s be Real; ::_thesis: ( r in REAL & s in REAL & (p * r) + ((1 - p) * s) in REAL implies f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) ) assume that r in REAL and s in REAL and (p * r) + ((1 - p) * s) in REAL ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) reconsider P = <*p,(1 - p)*>, E = <*r,s*>, F = <*(f . r),(f . s)*> as Element of 2 -tuples_on REAL by FINSEQ_2:101; A45: for i being Element of NAT st i in dom P holds ( P . i >= 0 & F . i = f . (E . i) ) proof A46: dom P = Seg (len P) by FINSEQ_1:def_3 .= Seg 2 by CARD_1:def_7 ; let i be Element of NAT ; ::_thesis: ( i in dom P implies ( P . i >= 0 & F . i = f . (E . i) ) ) assume A47: i in dom P ; ::_thesis: ( P . i >= 0 & F . i = f . (E . i) ) now__::_thesis:_(_P_._i_>=_0_&_F_._i_=_f_._(E_._i)_) percases ( i = 1 or i = 2 ) by A47, A46, FINSEQ_1:2, TARSKI:def_2; supposeA48: i = 1 ; ::_thesis: ( P . i >= 0 & F . i = f . (E . i) ) then E . i = r by FINSEQ_1:44; hence ( P . i >= 0 & F . i = f . (E . i) ) by A43, A48, FINSEQ_1:44; ::_thesis: verum end; supposeA49: i = 2 ; ::_thesis: ( P . i >= 0 & F . i = f . (E . i) ) then ( E . i = s & P . i = 1 - p ) by FINSEQ_1:44; hence ( P . i >= 0 & F . i = f . (E . i) ) by A44, A49, FINSEQ_1:44, XREAL_1:48; ::_thesis: verum end; end; end; hence ( P . i >= 0 & F . i = f . (E . i) ) ; ::_thesis: verum end; Sum P = p + (1 - p) by RVSUM_1:77 .= 1 ; then A50: f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) by A42, A45; A51: ( P . 1 = p & P . 2 = 1 - p ) by FINSEQ_1:44; len P = 2 by FINSEQ_1:44 .= len E by FINSEQ_1:44 ; then len (multreal .: (P,E)) = len P by FINSEQ_2:72; then A52: len (mlt (P,E)) = 2 by FINSEQ_1:44; A53: ( (mlt (P,E)) . 1 = (P . 1) * (E . 1) & (mlt (P,E)) . 2 = (P . 2) * (E . 2) ) by RVSUM_1:60; ( E . 1 = r & E . 2 = s ) by FINSEQ_1:44; then mlt (P,E) = <*(p * r),((1 - p) * s)*> by A51, A52, A53, FINSEQ_1:44; then A54: Sum (mlt (P,E)) = (p * r) + ((1 - p) * s) by RVSUM_1:77; A55: ( (mlt (P,F)) . 1 = (P . 1) * (F . 1) & (mlt (P,F)) . 2 = (P . 2) * (F . 2) ) by RVSUM_1:60; len P = 2 by FINSEQ_1:44 .= len F by FINSEQ_1:44 ; then len (multreal .: (P,F)) = len P by FINSEQ_2:72; then A56: len (mlt (P,F)) = 2 by FINSEQ_1:44; ( F . 1 = f . r & F . 2 = f . s ) by FINSEQ_1:44; then mlt (P,F) = <*(p * (f . r)),((1 - p) * (f . s))*> by A51, A56, A55, FINSEQ_1:44; hence f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) by A50, A54, RVSUM_1:77; ::_thesis: verum end; hence f is_convex_on REAL by A41, RFUNCT_3:def_12; ::_thesis: verum end; hence ( ( for n being Element of NAT for P, E, F being Element of n -tuples_on REAL st Sum P = 1 & ( for i being Element of NAT st i in dom P holds ( P . i >= 0 & F . i = f . (E . i) ) ) holds f . (Sum (mlt (P,E))) <= Sum (mlt (P,F)) ) iff f is_convex_on REAL ) by A1; ::_thesis: verum end; theorem :: RFUNCT_4:19 for f being PartFunc of REAL,REAL for I being Interval for a being Real st ex x1, x2 being Real st ( x1 in I & x2 in I & x1 < a & a < x2 ) & f is_convex_on I holds f is_continuous_in a proof let f be PartFunc of REAL,REAL; ::_thesis: for I being Interval for a being Real st ex x1, x2 being Real st ( x1 in I & x2 in I & x1 < a & a < x2 ) & f is_convex_on I holds f is_continuous_in a let I be Interval; ::_thesis: for a being Real st ex x1, x2 being Real st ( x1 in I & x2 in I & x1 < a & a < x2 ) & f is_convex_on I holds f is_continuous_in a let a be Real; ::_thesis: ( ex x1, x2 being Real st ( x1 in I & x2 in I & x1 < a & a < x2 ) & f is_convex_on I implies f is_continuous_in a ) assume that A1: ex x1, x2 being Real st ( x1 in I & x2 in I & x1 < a & a < x2 ) and A2: f is_convex_on I ; ::_thesis: f is_continuous_in a consider x1, x2 being Real such that A3: x1 in I and A4: x2 in I and A5: x1 < a and A6: a < x2 by A1; set M = max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))); A7: a in I by A3, A4, A5, A6, XXREAL_2:80; A8: for x being Real st x1 <= x & x <= x2 & x <> a holds ( ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) ) proof let x be Real; ::_thesis: ( x1 <= x & x <= x2 & x <> a implies ( ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) ) ) assume that A9: x1 <= x and A10: x <= x2 and A11: x <> a ; ::_thesis: ( ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) ) A12: x in I by A3, A4, A9, A10, XXREAL_2:80; ( ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) ) proof now__::_thesis:_(_((f_._x1)_-_(f_._a))_/_(x1_-_a)_<=_((f_._x)_-_(f_._a))_/_(x_-_a)_&_((f_._x)_-_(f_._a))_/_(x_-_a)_<=_((f_._x2)_-_(f_._a))_/_(x2_-_a)_) percases ( x < a or x > a ) by A11, XXREAL_0:1; supposeA13: x < a ; ::_thesis: ( ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) ) A14: now__::_thesis:_((f_._x1)_-_(f_._a))_/_(x1_-_a)_<=_((f_._x)_-_(f_._a))_/_(x_-_a) percases ( x1 = x or x1 < x ) by A9, XXREAL_0:1; suppose x1 = x ; ::_thesis: ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) hence ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) ; ::_thesis: verum end; supposeA15: x1 < x ; ::_thesis: ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) A16: ((f . a) - (f . x1)) / (a - x1) = (- ((f . a) - (f . x1))) / (- (a - x1)) by XCMPLX_1:191 .= ((f . x1) - (f . a)) / (x1 - a) ; ((f . a) - (f . x)) / (a - x) = (- ((f . a) - (f . x))) / (- (a - x)) by XCMPLX_1:191 .= ((f . x) - (f . a)) / (x - a) ; hence ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) by A2, A3, A7, A12, A13, A15, A16, Th16; ::_thesis: verum end; end; end; ( ((f . a) - (f . x)) / (a - x) <= ((f . x2) - (f . x)) / (x2 - x) & ((f . x2) - (f . x)) / (x2 - x) <= ((f . x2) - (f . a)) / (x2 - a) ) by A2, A4, A6, A7, A12, A13, Th16; then ((f . a) - (f . x)) / (a - x) <= ((f . x2) - (f . a)) / (x2 - a) by XXREAL_0:2; then (- ((f . a) - (f . x))) / (- (a - x)) <= ((f . x2) - (f . a)) / (x2 - a) by XCMPLX_1:191; hence ( ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) ) by A14; ::_thesis: verum end; supposeA17: x > a ; ::_thesis: ( ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) ) A18: ((f . a) - (f . x1)) / (a - x1) = (- ((f . a) - (f . x1))) / (- (a - x1)) by XCMPLX_1:191 .= ((f . x1) - (f . a)) / (x1 - a) ; ( ((f . a) - (f . x1)) / (a - x1) <= ((f . x) - (f . x1)) / (x - x1) & ((f . x) - (f . x1)) / (x - x1) <= ((f . x) - (f . a)) / (x - a) ) by A2, A3, A5, A7, A12, A17, Th16; hence ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) by A18, XXREAL_0:2; ::_thesis: ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) now__::_thesis:_((f_._x)_-_(f_._a))_/_(x_-_a)_<=_((f_._x2)_-_(f_._a))_/_(x2_-_a) percases ( x = x2 or x < x2 ) by A10, XXREAL_0:1; suppose x = x2 ; ::_thesis: ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) hence ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) ; ::_thesis: verum end; suppose x < x2 ; ::_thesis: ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) hence ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) by A2, A4, A7, A12, A17, Th16; ::_thesis: verum end; end; end; hence ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) ; ::_thesis: verum end; end; end; hence ( ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) ) ; ::_thesis: verum end; hence ( ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) & ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) ) ; ::_thesis: verum end; A19: for x being real number st x1 <= x & x <= x2 & x <> a holds abs ((f . x) - (f . a)) <= (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a)) proof A20: - (abs (((f . x1) - (f . a)) / (x1 - a))) <= ((f . x1) - (f . a)) / (x1 - a) by ABSVALUE:4; A21: ((f . x2) - (f . a)) / (x2 - a) <= abs (((f . x2) - (f . a)) / (x2 - a)) by ABSVALUE:4; let x be real number ; ::_thesis: ( x1 <= x & x <= x2 & x <> a implies abs ((f . x) - (f . a)) <= (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a)) ) assume that A22: ( x1 <= x & x <= x2 ) and A23: x <> a ; ::_thesis: abs ((f . x) - (f . a)) <= (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a)) reconsider x = x as Real by XREAL_0:def_1; ((f . x) - (f . a)) / (x - a) <= ((f . x2) - (f . a)) / (x2 - a) by A8, A22, A23; then A24: ((f . x) - (f . a)) / (x - a) <= abs (((f . x2) - (f . a)) / (x2 - a)) by A21, XXREAL_0:2; x - a <> 0 by A23; then A25: abs (x - a) > 0 by COMPLEX1:47; ((f . x1) - (f . a)) / (x1 - a) <= ((f . x) - (f . a)) / (x - a) by A8, A22, A23; then A26: - (abs (((f . x1) - (f . a)) / (x1 - a))) <= ((f . x) - (f . a)) / (x - a) by A20, XXREAL_0:2; now__::_thesis:_abs_((f_._x)_-_(f_._a))_<=_(max_((abs_(((f_._x1)_-_(f_._a))_/_(x1_-_a))),(abs_(((f_._x2)_-_(f_._a))_/_(x2_-_a)))))_*_(abs_(x_-_a)) percases ( abs (((f . x1) - (f . a)) / (x1 - a)) <= abs (((f . x2) - (f . a)) / (x2 - a)) or abs (((f . x1) - (f . a)) / (x1 - a)) >= abs (((f . x2) - (f . a)) / (x2 - a)) ) ; suppose abs (((f . x1) - (f . a)) / (x1 - a)) <= abs (((f . x2) - (f . a)) / (x2 - a)) ; ::_thesis: abs ((f . x) - (f . a)) <= (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a)) then - (abs (((f . x1) - (f . a)) / (x1 - a))) >= - (abs (((f . x2) - (f . a)) / (x2 - a))) by XREAL_1:24; then - (abs (((f . x2) - (f . a)) / (x2 - a))) <= ((f . x) - (f . a)) / (x - a) by A26, XXREAL_0:2; then abs (((f . x) - (f . a)) / (x - a)) <= abs (((f . x2) - (f . a)) / (x2 - a)) by A24, ABSVALUE:5; then A27: (abs ((f . x) - (f . a))) / (abs (x - a)) <= abs (((f . x2) - (f . a)) / (x2 - a)) by COMPLEX1:67; abs (((f . x2) - (f . a)) / (x2 - a)) <= max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) by XXREAL_0:25; then (abs ((f . x) - (f . a))) / (abs (x - a)) <= max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) by A27, XXREAL_0:2; hence abs ((f . x) - (f . a)) <= (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a)) by A25, XREAL_1:81; ::_thesis: verum end; suppose abs (((f . x1) - (f . a)) / (x1 - a)) >= abs (((f . x2) - (f . a)) / (x2 - a)) ; ::_thesis: abs ((f . x) - (f . a)) <= (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a)) then ((f . x) - (f . a)) / (x - a) <= abs (((f . x1) - (f . a)) / (x1 - a)) by A24, XXREAL_0:2; then abs (((f . x) - (f . a)) / (x - a)) <= abs (((f . x1) - (f . a)) / (x1 - a)) by A26, ABSVALUE:5; then A28: (abs ((f . x) - (f . a))) / (abs (x - a)) <= abs (((f . x1) - (f . a)) / (x1 - a)) by COMPLEX1:67; abs (((f . x1) - (f . a)) / (x1 - a)) <= max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) by XXREAL_0:25; then (abs ((f . x) - (f . a))) / (abs (x - a)) <= max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) by A28, XXREAL_0:2; hence abs ((f . x) - (f . a)) <= (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a)) by A25, XREAL_1:81; ::_thesis: verum end; end; end; hence abs ((f . x) - (f . a)) <= (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a)) ; ::_thesis: verum end; A29: max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) >= min ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) by Th1; A30: ( abs (((f . x1) - (f . a)) / (x1 - a)) >= 0 & abs (((f . x2) - (f . a)) / (x2 - a)) >= 0 ) by COMPLEX1:46; then A31: min ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) >= 0 by XXREAL_0:20; then A32: max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) >= 0 by Th1; for r being real number st 0 < r holds ex s being real number st ( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds abs ((f . x) - (f . a)) < r ) ) proof let r be real number ; ::_thesis: ( 0 < r implies ex s being real number st ( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds abs ((f . x) - (f . a)) < r ) ) ) assume A33: 0 < r ; ::_thesis: ex s being real number st ( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds abs ((f . x) - (f . a)) < r ) ) reconsider r = r as Real by XREAL_0:def_1; ex s being real number st ( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds abs ((f . x) - (f . a)) < r ) ) proof now__::_thesis:_ex_s_being_real_number_st_ (_0_<_s_&_(_for_x_being_real_number_st_x_in_dom_f_&_abs_(x_-_a)_<_s_holds_ abs_((f_._x)_-_(f_._a))_<_r_)_) percases ( max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) > 0 or max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) = 0 ) by A30, A29, XXREAL_0:20; supposeA34: max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) > 0 ; ::_thesis: ex s being real number st ( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds abs ((f . x) - (f . a)) < r ) ) set s = min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))); A35: for x being real number st x in dom f & abs (x - a) < min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) holds abs ((f . x) - (f . a)) < r proof A36: min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) <= min ((a - x1),(x2 - a)) by XXREAL_0:17; let x be real number ; ::_thesis: ( x in dom f & abs (x - a) < min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) implies abs ((f . x) - (f . a)) < r ) assume that x in dom f and A37: abs (x - a) < min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) ; ::_thesis: abs ((f . x) - (f . a)) < r min ((a - x1),(x2 - a)) <= a - x1 by XXREAL_0:17; then min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) <= a - x1 by A36, XXREAL_0:2; then abs (x - a) < a - x1 by A37, XXREAL_0:2; then - (a - x1) <= x - a by ABSVALUE:5; then x1 - a <= x - a ; then A38: x1 <= x by XREAL_1:9; min ((a - x1),(x2 - a)) <= x2 - a by XXREAL_0:17; then min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) <= x2 - a by A36, XXREAL_0:2; then abs (x - a) < x2 - a by A37, XXREAL_0:2; then x - a <= x2 - a by ABSVALUE:5; then A39: x <= x2 by XREAL_1:9; now__::_thesis:_abs_((f_._x)_-_(f_._a))_<_r percases ( x <> a or x = a ) ; suppose x <> a ; ::_thesis: abs ((f . x) - (f . a)) < r then A40: abs ((f . x) - (f . a)) <= (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a)) by A19, A38, A39; now__::_thesis:_abs_((f_._x)_-_(f_._a))_<_r percases ( max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) <> 0 or max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) = 0 ) ; supposeA41: max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) <> 0 ; ::_thesis: abs ((f . x) - (f . a)) < r A42: (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a))))) <= (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))) by A31, A29, XREAL_1:64, XXREAL_0:17; (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a)) < (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a))))) by A32, A37, A41, XREAL_1:68; then (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a)) < (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))) by A42, XXREAL_0:2; then (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a)) < (r * (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))) / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) by XCMPLX_1:74; then (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a)) < r * ((max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))) by XCMPLX_1:74; then (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a)) < r * 1 by A41, XCMPLX_1:60; hence abs ((f . x) - (f . a)) < r by A40, XXREAL_0:2; ::_thesis: verum end; suppose max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) = 0 ; ::_thesis: abs ((f . x) - (f . a)) < r hence abs ((f . x) - (f . a)) < r by A33, A40; ::_thesis: verum end; end; end; hence abs ((f . x) - (f . a)) < r ; ::_thesis: verum end; suppose x = a ; ::_thesis: abs ((f . x) - (f . a)) < r hence abs ((f . x) - (f . a)) < r by A33, ABSVALUE:2; ::_thesis: verum end; end; end; hence abs ((f . x) - (f . a)) < r ; ::_thesis: verum end; min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) > 0 proof A43: min ((a - x1),(x2 - a)) > 0 proof now__::_thesis:_min_((a_-_x1),(x2_-_a))_>_0 percases ( min ((a - x1),(x2 - a)) = a - x1 or min ((a - x1),(x2 - a)) = x2 - a ) by XXREAL_0:15; suppose min ((a - x1),(x2 - a)) = a - x1 ; ::_thesis: min ((a - x1),(x2 - a)) > 0 hence min ((a - x1),(x2 - a)) > 0 by A5, XREAL_1:50; ::_thesis: verum end; suppose min ((a - x1),(x2 - a)) = x2 - a ; ::_thesis: min ((a - x1),(x2 - a)) > 0 hence min ((a - x1),(x2 - a)) > 0 by A6, XREAL_1:50; ::_thesis: verum end; end; end; hence min ((a - x1),(x2 - a)) > 0 ; ::_thesis: verum end; now__::_thesis:_min_((r_/_(max_((abs_(((f_._x1)_-_(f_._a))_/_(x1_-_a))),(abs_(((f_._x2)_-_(f_._a))_/_(x2_-_a)))))),(min_((a_-_x1),(x2_-_a))))_>_0 percases ( min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) = r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) or min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) = min ((a - x1),(x2 - a)) ) by XXREAL_0:15; suppose min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) = r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) ; ::_thesis: min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) > 0 hence min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) > 0 by A33, A34, XREAL_1:139; ::_thesis: verum end; suppose min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) = min ((a - x1),(x2 - a)) ; ::_thesis: min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) > 0 hence min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) > 0 by A43; ::_thesis: verum end; end; end; hence min ((r / (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))))),(min ((a - x1),(x2 - a)))) > 0 ; ::_thesis: verum end; hence ex s being real number st ( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds abs ((f . x) - (f . a)) < r ) ) by A35; ::_thesis: verum end; supposeA44: max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a)))) = 0 ; ::_thesis: ex s being real number st ( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds abs ((f . x) - (f . a)) < r ) ) set s = min ((a - x1),(x2 - a)); A45: for x being real number st x1 <= x & x <= x2 & x <> a holds abs ((f . x) - (f . a)) = 0 proof let x be real number ; ::_thesis: ( x1 <= x & x <= x2 & x <> a implies abs ((f . x) - (f . a)) = 0 ) assume ( x1 <= x & x <= x2 & x <> a ) ; ::_thesis: abs ((f . x) - (f . a)) = 0 then abs ((f . x) - (f . a)) <= (max ((abs (((f . x1) - (f . a)) / (x1 - a))),(abs (((f . x2) - (f . a)) / (x2 - a))))) * (abs (x - a)) by A19; hence abs ((f . x) - (f . a)) = 0 by A44, COMPLEX1:46; ::_thesis: verum end; A46: for x being real number st x in dom f & abs (x - a) < min ((a - x1),(x2 - a)) holds abs ((f . x) - (f . a)) < r proof let x be real number ; ::_thesis: ( x in dom f & abs (x - a) < min ((a - x1),(x2 - a)) implies abs ((f . x) - (f . a)) < r ) assume that x in dom f and A47: abs (x - a) < min ((a - x1),(x2 - a)) ; ::_thesis: abs ((f . x) - (f . a)) < r min ((a - x1),(x2 - a)) <= a - x1 by XXREAL_0:17; then abs (x - a) < a - x1 by A47, XXREAL_0:2; then - (a - x1) <= x - a by ABSVALUE:5; then x1 - a <= x - a ; then A48: x1 <= x by XREAL_1:9; min ((a - x1),(x2 - a)) <= x2 - a by XXREAL_0:17; then abs (x - a) < x2 - a by A47, XXREAL_0:2; then x - a <= x2 - a by ABSVALUE:5; then A49: x <= x2 by XREAL_1:9; now__::_thesis:_abs_((f_._x)_-_(f_._a))_<_r percases ( x <> a or x = a ) ; suppose x <> a ; ::_thesis: abs ((f . x) - (f . a)) < r hence abs ((f . x) - (f . a)) < r by A33, A45, A48, A49; ::_thesis: verum end; suppose x = a ; ::_thesis: abs ((f . x) - (f . a)) < r hence abs ((f . x) - (f . a)) < r by A33, ABSVALUE:2; ::_thesis: verum end; end; end; hence abs ((f . x) - (f . a)) < r ; ::_thesis: verum end; min ((a - x1),(x2 - a)) > 0 proof now__::_thesis:_min_((a_-_x1),(x2_-_a))_>_0 percases ( min ((a - x1),(x2 - a)) = a - x1 or min ((a - x1),(x2 - a)) = x2 - a ) by XXREAL_0:15; suppose min ((a - x1),(x2 - a)) = a - x1 ; ::_thesis: min ((a - x1),(x2 - a)) > 0 hence min ((a - x1),(x2 - a)) > 0 by A5, XREAL_1:50; ::_thesis: verum end; suppose min ((a - x1),(x2 - a)) = x2 - a ; ::_thesis: min ((a - x1),(x2 - a)) > 0 hence min ((a - x1),(x2 - a)) > 0 by A6, XREAL_1:50; ::_thesis: verum end; end; end; hence min ((a - x1),(x2 - a)) > 0 ; ::_thesis: verum end; hence ex s being real number st ( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds abs ((f . x) - (f . a)) < r ) ) by A46; ::_thesis: verum end; end; end; hence ex s being real number st ( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds abs ((f . x) - (f . a)) < r ) ) ; ::_thesis: verum end; hence ex s being real number st ( 0 < s & ( for x being real number st x in dom f & abs (x - a) < s holds abs ((f . x) - (f . a)) < r ) ) ; ::_thesis: verum end; hence f is_continuous_in a by FCONT_1:3; ::_thesis: verum end; begin definition let f be PartFunc of REAL,REAL; let X be set ; predf is_quasiconvex_on X means :Def2: :: RFUNCT_4:def 2 ( X c= dom f & ( for p being Real st 0 < p & p < 1 holds for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds f . ((p * r) + ((1 - p) * s)) <= max ((f . r),(f . s)) ) ); end; :: deftheorem Def2 defines is_quasiconvex_on RFUNCT_4:def_2_:_ for f being PartFunc of REAL,REAL for X being set holds ( f is_quasiconvex_on X iff ( X c= dom f & ( for p being Real st 0 < p & p < 1 holds for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds f . ((p * r) + ((1 - p) * s)) <= max ((f . r),(f . s)) ) ) ); definition let f be PartFunc of REAL,REAL; let X be set ; predf is_strictly_quasiconvex_on X means :Def3: :: RFUNCT_4:def 3 ( X c= dom f & ( for p being Real st 0 < p & p < 1 holds for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & f . r <> f . s holds f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) ) ); end; :: deftheorem Def3 defines is_strictly_quasiconvex_on RFUNCT_4:def_3_:_ for f being PartFunc of REAL,REAL for X being set holds ( f is_strictly_quasiconvex_on X iff ( X c= dom f & ( for p being Real st 0 < p & p < 1 holds for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & f . r <> f . s holds f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) ) ) ); definition let f be PartFunc of REAL,REAL; let X be set ; predf is_strongly_quasiconvex_on X means :Def4: :: RFUNCT_4:def 4 ( X c= dom f & ( for p being Real st 0 < p & p < 1 holds for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) ) ); end; :: deftheorem Def4 defines is_strongly_quasiconvex_on RFUNCT_4:def_4_:_ for f being PartFunc of REAL,REAL for X being set holds ( f is_strongly_quasiconvex_on X iff ( X c= dom f & ( for p being Real st 0 < p & p < 1 holds for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) ) ) ); definition let f be PartFunc of REAL,REAL; let x0 be real number ; predf is_upper_semicontinuous_in x0 means :Def5: :: RFUNCT_4:def 5 ( x0 in dom f & ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds (f . x0) - (f . x) < r ) ) ) ); end; :: deftheorem Def5 defines is_upper_semicontinuous_in RFUNCT_4:def_5_:_ for f being PartFunc of REAL,REAL for x0 being real number holds ( f is_upper_semicontinuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds (f . x0) - (f . x) < r ) ) ) ) ); definition let f be PartFunc of REAL,REAL; let X be set ; predf is_upper_semicontinuous_on X means :Def6: :: RFUNCT_4:def 6 ( X c= dom f & ( for x0 being Real st x0 in X holds f | X is_upper_semicontinuous_in x0 ) ); end; :: deftheorem Def6 defines is_upper_semicontinuous_on RFUNCT_4:def_6_:_ for f being PartFunc of REAL,REAL for X being set holds ( f is_upper_semicontinuous_on X iff ( X c= dom f & ( for x0 being Real st x0 in X holds f | X is_upper_semicontinuous_in x0 ) ) ); definition let f be PartFunc of REAL,REAL; let x0 be real number ; predf is_lower_semicontinuous_in x0 means :Def7: :: RFUNCT_4:def 7 ( x0 in dom f & ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds (f . x) - (f . x0) < r ) ) ) ); end; :: deftheorem Def7 defines is_lower_semicontinuous_in RFUNCT_4:def_7_:_ for f being PartFunc of REAL,REAL for x0 being real number holds ( f is_lower_semicontinuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds (f . x) - (f . x0) < r ) ) ) ) ); definition let f be PartFunc of REAL,REAL; let X be set ; predf is_lower_semicontinuous_on X means :Def8: :: RFUNCT_4:def 8 ( X c= dom f & ( for x0 being Real st x0 in X holds f | X is_lower_semicontinuous_in x0 ) ); end; :: deftheorem Def8 defines is_lower_semicontinuous_on RFUNCT_4:def_8_:_ for f being PartFunc of REAL,REAL for X being set holds ( f is_lower_semicontinuous_on X iff ( X c= dom f & ( for x0 being Real st x0 in X holds f | X is_lower_semicontinuous_in x0 ) ) ); theorem Th20: :: RFUNCT_4:20 for x0 being real number for f being PartFunc of REAL,REAL st x0 in dom f holds ( ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 ) iff f is_continuous_in x0 ) proof let x0 be real number ; ::_thesis: for f being PartFunc of REAL,REAL st x0 in dom f holds ( ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 ) iff f is_continuous_in x0 ) let f be PartFunc of REAL,REAL; ::_thesis: ( x0 in dom f implies ( ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 ) iff f is_continuous_in x0 ) ) assume A1: x0 in dom f ; ::_thesis: ( ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 ) iff f is_continuous_in x0 ) A2: ( f is_continuous_in x0 implies ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 ) ) proof assume A3: f is_continuous_in x0 ; ::_thesis: ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 ) A4: for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds (f . x0) - (f . x) < r ) ) proof let r be Real; ::_thesis: ( 0 < r implies ex s being Real st ( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds (f . x0) - (f . x) < r ) ) ) assume 0 < r ; ::_thesis: ex s being Real st ( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds (f . x0) - (f . x) < r ) ) then consider s being real number such that A5: 0 < s and A6: for x being real number st x in dom f & abs (x - x0) < s holds abs ((f . x) - (f . x0)) < r by A3, FCONT_1:3; take s ; ::_thesis: ( s is Real & 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds (f . x0) - (f . x) < r ) ) thus s is Real by XREAL_0:def_1; ::_thesis: ( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds (f . x0) - (f . x) < r ) ) for x being Real st x in dom f & abs (x - x0) < s holds (f . x0) - (f . x) < r proof let x be Real; ::_thesis: ( x in dom f & abs (x - x0) < s implies (f . x0) - (f . x) < r ) assume ( x in dom f & abs (x - x0) < s ) ; ::_thesis: (f . x0) - (f . x) < r then A7: abs ((f . x) - (f . x0)) < r by A6; (f . x) - (f . x0) >= - (abs ((f . x) - (f . x0))) by ABSVALUE:4; then - ((f . x) - (f . x0)) <= abs ((f . x) - (f . x0)) by XREAL_1:26; hence (f . x0) - (f . x) < r by A7, XXREAL_0:2; ::_thesis: verum end; hence ( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds (f . x0) - (f . x) < r ) ) by A5; ::_thesis: verum end; for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds (f . x) - (f . x0) < r ) ) proof let r be Real; ::_thesis: ( 0 < r implies ex s being Real st ( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds (f . x) - (f . x0) < r ) ) ) assume 0 < r ; ::_thesis: ex s being Real st ( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds (f . x) - (f . x0) < r ) ) then consider s being real number such that A8: 0 < s and A9: for x being real number st x in dom f & abs (x - x0) < s holds abs ((f . x) - (f . x0)) < r by A3, FCONT_1:3; take s ; ::_thesis: ( s is Real & 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds (f . x) - (f . x0) < r ) ) thus s is Real by XREAL_0:def_1; ::_thesis: ( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds (f . x) - (f . x0) < r ) ) for x being Real st x in dom f & abs (x - x0) < s holds (f . x) - (f . x0) < r proof let x be Real; ::_thesis: ( x in dom f & abs (x - x0) < s implies (f . x) - (f . x0) < r ) assume ( x in dom f & abs (x - x0) < s ) ; ::_thesis: (f . x) - (f . x0) < r then A10: abs ((f . x) - (f . x0)) < r by A9; (f . x) - (f . x0) <= abs ((f . x) - (f . x0)) by ABSVALUE:4; hence (f . x) - (f . x0) < r by A10, XXREAL_0:2; ::_thesis: verum end; hence ( 0 < s & ( for x being Real st x in dom f & abs (x - x0) < s holds (f . x) - (f . x0) < r ) ) by A8; ::_thesis: verum end; hence ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 ) by A1, A4, Def5, Def7; ::_thesis: verum end; ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 implies f is_continuous_in x0 ) proof assume that A11: f is_upper_semicontinuous_in x0 and A12: f is_lower_semicontinuous_in x0 ; ::_thesis: f is_continuous_in x0 for r being real number st 0 < r holds ex s being real number st ( 0 < s & ( for x being real number st x in dom f & abs (x - x0) < s holds abs ((f . x) - (f . x0)) < r ) ) proof let r be real number ; ::_thesis: ( 0 < r implies ex s being real number st ( 0 < s & ( for x being real number st x in dom f & abs (x - x0) < s holds abs ((f . x) - (f . x0)) < r ) ) ) assume A13: 0 < r ; ::_thesis: ex s being real number st ( 0 < s & ( for x being real number st x in dom f & abs (x - x0) < s holds abs ((f . x) - (f . x0)) < r ) ) A14: r is Real by XREAL_0:def_1; then consider s1 being Real such that A15: 0 < s1 and A16: for x being Real st x in dom f & abs (x - x0) < s1 holds (f . x) - (f . x0) < r by A12, A13, Def7; consider s2 being Real such that A17: 0 < s2 and A18: for x being Real st x in dom f & abs (x - x0) < s2 holds (f . x0) - (f . x) < r by A11, A13, A14, Def5; set s = min (s1,s2); A19: for x being real number st x in dom f & abs (x - x0) < min (s1,s2) holds abs ((f . x) - (f . x0)) < r proof let x be real number ; ::_thesis: ( x in dom f & abs (x - x0) < min (s1,s2) implies abs ((f . x) - (f . x0)) < r ) assume that A20: x in dom f and A21: abs (x - x0) < min (s1,s2) ; ::_thesis: abs ((f . x) - (f . x0)) < r A22: x is Real by XREAL_0:def_1; min (s1,s2) <= s2 by XXREAL_0:17; then abs (x - x0) < s2 by A21, XXREAL_0:2; then A23: (f . x0) - (f . x) < r by A18, A20, A22; min (s1,s2) <= s1 by XXREAL_0:17; then abs (x - x0) < s1 by A21, XXREAL_0:2; then A24: (f . x) - (f . x0) < r by A16, A20, A22; A25: abs ((f . x) - (f . x0)) <> r proof assume A26: abs ((f . x) - (f . x0)) = r ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( (f . x) - (f . x0) >= 0 or not (f . x) - (f . x0) >= 0 ) ; suppose (f . x) - (f . x0) >= 0 ; ::_thesis: contradiction hence contradiction by A24, A26, ABSVALUE:def_1; ::_thesis: verum end; suppose not (f . x) - (f . x0) >= 0 ; ::_thesis: contradiction then abs ((f . x) - (f . x0)) = - ((f . x) - (f . x0)) by ABSVALUE:def_1; hence contradiction by A23, A26; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; - ((f . x0) - (f . x)) > - r by A23, XREAL_1:24; then abs ((f . x) - (f . x0)) <= r by A24, ABSVALUE:5; hence abs ((f . x) - (f . x0)) < r by A25, XXREAL_0:1; ::_thesis: verum end; take min (s1,s2) ; ::_thesis: ( 0 < min (s1,s2) & ( for x being real number st x in dom f & abs (x - x0) < min (s1,s2) holds abs ((f . x) - (f . x0)) < r ) ) min (s1,s2) > 0 proof now__::_thesis:_min_(s1,s2)_>_0 percases ( s1 <= s2 or not s1 <= s2 ) ; suppose s1 <= s2 ; ::_thesis: min (s1,s2) > 0 hence min (s1,s2) > 0 by A15, XXREAL_0:def_9; ::_thesis: verum end; suppose not s1 <= s2 ; ::_thesis: min (s1,s2) > 0 hence min (s1,s2) > 0 by A17, XXREAL_0:def_9; ::_thesis: verum end; end; end; hence min (s1,s2) > 0 ; ::_thesis: verum end; hence ( 0 < min (s1,s2) & ( for x being real number st x in dom f & abs (x - x0) < min (s1,s2) holds abs ((f . x) - (f . x0)) < r ) ) by A19; ::_thesis: verum end; hence f is_continuous_in x0 by FCONT_1:3; ::_thesis: verum end; hence ( ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 ) iff f is_continuous_in x0 ) by A2; ::_thesis: verum end; theorem :: RFUNCT_4:21 for X being set for f being PartFunc of REAL,REAL st X c= dom f holds ( ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) iff f | X is continuous ) proof let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st X c= dom f holds ( ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) iff f | X is continuous ) let f be PartFunc of REAL,REAL; ::_thesis: ( X c= dom f implies ( ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) iff f | X is continuous ) ) assume A1: X c= dom f ; ::_thesis: ( ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) iff f | X is continuous ) A2: ( f | X is continuous implies ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) ) proof assume A3: f | X is continuous ; ::_thesis: ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) A4: for x0 being Real st x0 in X holds f | X is_lower_semicontinuous_in x0 proof let x0 be Real; ::_thesis: ( x0 in X implies f | X is_lower_semicontinuous_in x0 ) assume x0 in X ; ::_thesis: f | X is_lower_semicontinuous_in x0 then A5: x0 in dom (f | X) by A1, RELAT_1:57; then f | X is_continuous_in x0 by A3, FCONT_1:def_2; hence f | X is_lower_semicontinuous_in x0 by A5, Th20; ::_thesis: verum end; for x0 being Real st x0 in X holds f | X is_upper_semicontinuous_in x0 proof let x0 be Real; ::_thesis: ( x0 in X implies f | X is_upper_semicontinuous_in x0 ) assume x0 in X ; ::_thesis: f | X is_upper_semicontinuous_in x0 then A6: x0 in dom (f | X) by A1, RELAT_1:57; then f | X is_continuous_in x0 by A3, FCONT_1:def_2; hence f | X is_upper_semicontinuous_in x0 by A6, Th20; ::_thesis: verum end; hence ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) by A1, A4, Def6, Def8; ::_thesis: verum end; ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X implies f | X is continuous ) proof assume that A7: f is_upper_semicontinuous_on X and A8: f is_lower_semicontinuous_on X ; ::_thesis: f | X is continuous ( X c= dom f & ( for x0 being real number st x0 in dom (f | X) holds f | X is_continuous_in x0 ) ) proof thus X c= dom f by A7, Def6; ::_thesis: for x0 being real number st x0 in dom (f | X) holds f | X is_continuous_in x0 let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 ) assume A9: x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0 A10: x0 is Real by XREAL_0:def_1; x0 in X by A9, RELAT_1:57; then ( f | X is_upper_semicontinuous_in x0 & f | X is_lower_semicontinuous_in x0 ) by A7, A8, A10, Def6, Def8; hence f | X is_continuous_in x0 by A9, Th20; ::_thesis: verum end; hence f | X is continuous by FCONT_1:def_2; ::_thesis: verum end; hence ( ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) iff f | X is continuous ) by A2; ::_thesis: verum end; theorem :: RFUNCT_4:22 for X being set for f being PartFunc of REAL,REAL st f is_strictly_convex_on X holds f is_strongly_quasiconvex_on X proof let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st f is_strictly_convex_on X holds f is_strongly_quasiconvex_on X let f be PartFunc of REAL,REAL; ::_thesis: ( f is_strictly_convex_on X implies f is_strongly_quasiconvex_on X ) assume A1: f is_strictly_convex_on X ; ::_thesis: f is_strongly_quasiconvex_on X A2: for p being Real st 0 < p & p < 1 holds for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) proof let p be Real; ::_thesis: ( 0 < p & p < 1 implies for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) ) assume that A3: 0 < p and A4: p < 1 ; ::_thesis: for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) proof let r, s be Real; ::_thesis: ( r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s implies f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) ) 1 - p > 0 by A4, XREAL_1:50; then A5: (1 - p) * (f . s) <= (1 - p) * (max ((f . r),(f . s))) by XREAL_1:64, XXREAL_0:25; assume ( r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s ) ; ::_thesis: f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) then A6: f . ((p * r) + ((1 - p) * s)) < (p * (f . r)) + ((1 - p) * (f . s)) by A1, A3, A4, Def1; p * (f . r) <= p * (max ((f . r),(f . s))) by A3, XREAL_1:64, XXREAL_0:25; then (p * (f . r)) + ((1 - p) * (f . s)) <= (p * (max ((f . r),(f . s)))) + ((1 - p) * (max ((f . r),(f . s)))) by A5, XREAL_1:7; hence f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) by A6, XXREAL_0:2; ::_thesis: verum end; hence for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) ; ::_thesis: verum end; X c= dom f by A1, Def1; hence f is_strongly_quasiconvex_on X by A2, Def4; ::_thesis: verum end; theorem :: RFUNCT_4:23 for X being set for f being PartFunc of REAL,REAL st f is_strongly_quasiconvex_on X holds f is_quasiconvex_on X proof let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st f is_strongly_quasiconvex_on X holds f is_quasiconvex_on X let f be PartFunc of REAL,REAL; ::_thesis: ( f is_strongly_quasiconvex_on X implies f is_quasiconvex_on X ) assume A1: f is_strongly_quasiconvex_on X ; ::_thesis: f is_quasiconvex_on X A2: for p being Real st 0 < p & p < 1 holds for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds f . ((p * r) + ((1 - p) * s)) <= max ((f . r),(f . s)) proof let p be Real; ::_thesis: ( 0 < p & p < 1 implies for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds f . ((p * r) + ((1 - p) * s)) <= max ((f . r),(f . s)) ) assume A3: ( 0 < p & p < 1 ) ; ::_thesis: for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds f . ((p * r) + ((1 - p) * s)) <= max ((f . r),(f . s)) for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds f . ((p * r) + ((1 - p) * s)) <= max ((f . r),(f . s)) proof let r, s be Real; ::_thesis: ( r in X & s in X & (p * r) + ((1 - p) * s) in X implies f . ((p * r) + ((1 - p) * s)) <= max ((f . r),(f . s)) ) assume A4: ( r in X & s in X & (p * r) + ((1 - p) * s) in X ) ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= max ((f . r),(f . s)) now__::_thesis:_f_._((p_*_r)_+_((1_-_p)_*_s))_<=_max_((f_._r),(f_._s)) percases ( r <> s or r = s ) ; suppose r <> s ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= max ((f . r),(f . s)) hence f . ((p * r) + ((1 - p) * s)) <= max ((f . r),(f . s)) by A1, A3, A4, Def4; ::_thesis: verum end; suppose r = s ; ::_thesis: f . ((p * r) + ((1 - p) * s)) <= max ((f . r),(f . s)) hence f . ((p * r) + ((1 - p) * s)) <= max ((f . r),(f . s)) ; ::_thesis: verum end; end; end; hence f . ((p * r) + ((1 - p) * s)) <= max ((f . r),(f . s)) ; ::_thesis: verum end; hence for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X holds f . ((p * r) + ((1 - p) * s)) <= max ((f . r),(f . s)) ; ::_thesis: verum end; X c= dom f by A1, Def4; hence f is_quasiconvex_on X by A2, Def2; ::_thesis: verum end; theorem :: RFUNCT_4:24 for X being set for f being PartFunc of REAL,REAL st f is_convex_on X holds f is_strictly_quasiconvex_on X proof let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st f is_convex_on X holds f is_strictly_quasiconvex_on X let f be PartFunc of REAL,REAL; ::_thesis: ( f is_convex_on X implies f is_strictly_quasiconvex_on X ) assume A1: f is_convex_on X ; ::_thesis: f is_strictly_quasiconvex_on X A2: for p being Real st 0 < p & p < 1 holds for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & f . r <> f . s holds f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) proof let p be Real; ::_thesis: ( 0 < p & p < 1 implies for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & f . r <> f . s holds f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) ) assume that A3: 0 < p and A4: p < 1 ; ::_thesis: for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & f . r <> f . s holds f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & f . r <> f . s holds f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) proof let r, s be Real; ::_thesis: ( r in X & s in X & (p * r) + ((1 - p) * s) in X & f . r <> f . s implies f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) ) assume that A5: ( r in X & s in X & (p * r) + ((1 - p) * s) in X ) and A6: f . r <> f . s ; ::_thesis: f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) A7: f . ((p * r) + ((1 - p) * s)) <= (p * (f . r)) + ((1 - p) * (f . s)) by A1, A3, A4, A5, RFUNCT_3:def_12; A8: 1 - p > 0 by A4, XREAL_1:50; now__::_thesis:_f_._((p_*_r)_+_((1_-_p)_*_s))_<_max_((f_._r),(f_._s)) percases ( f . r < f . s or f . r > f . s ) by A6, XXREAL_0:1; suppose f . r < f . s ; ::_thesis: f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) then p * (f . r) < p * (f . s) by A3, XREAL_1:68; then (p * (f . r)) + ((1 - p) * (f . s)) < (p * (f . s)) + ((1 - p) * (f . s)) by XREAL_1:6; then A9: f . ((p * r) + ((1 - p) * s)) < f . s by A7, XXREAL_0:2; f . s <= max ((f . r),(f . s)) by XXREAL_0:25; hence f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) by A9, XXREAL_0:2; ::_thesis: verum end; suppose f . r > f . s ; ::_thesis: f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) then (1 - p) * (f . r) > (1 - p) * (f . s) by A8, XREAL_1:68; then (p * (f . r)) + ((1 - p) * (f . s)) < (p * (f . r)) + ((1 - p) * (f . r)) by XREAL_1:6; then A10: f . ((p * r) + ((1 - p) * s)) < f . r by A7, XXREAL_0:2; f . r <= max ((f . r),(f . s)) by XXREAL_0:25; hence f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) by A10, XXREAL_0:2; ::_thesis: verum end; end; end; hence f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) ; ::_thesis: verum end; hence for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & f . r <> f . s holds f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) ; ::_thesis: verum end; X c= dom f by A1, RFUNCT_3:def_12; hence f is_strictly_quasiconvex_on X by A2, Def3; ::_thesis: verum end; theorem :: RFUNCT_4:25 for X being set for f being PartFunc of REAL,REAL st f is_strongly_quasiconvex_on X holds f is_strictly_quasiconvex_on X proof let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st f is_strongly_quasiconvex_on X holds f is_strictly_quasiconvex_on X let f be PartFunc of REAL,REAL; ::_thesis: ( f is_strongly_quasiconvex_on X implies f is_strictly_quasiconvex_on X ) assume f is_strongly_quasiconvex_on X ; ::_thesis: f is_strictly_quasiconvex_on X then ( X c= dom f & ( for p being Real st 0 < p & p < 1 holds for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & f . r <> f . s holds f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) ) ) by Def4; hence f is_strictly_quasiconvex_on X by Def3; ::_thesis: verum end; theorem :: RFUNCT_4:26 for X being set for f being PartFunc of REAL,REAL st f is_strictly_quasiconvex_on X & f is one-to-one holds f is_strongly_quasiconvex_on X proof let X be set ; ::_thesis: for f being PartFunc of REAL,REAL st f is_strictly_quasiconvex_on X & f is one-to-one holds f is_strongly_quasiconvex_on X let f be PartFunc of REAL,REAL; ::_thesis: ( f is_strictly_quasiconvex_on X & f is one-to-one implies f is_strongly_quasiconvex_on X ) assume that A1: f is_strictly_quasiconvex_on X and A2: f is one-to-one ; ::_thesis: f is_strongly_quasiconvex_on X A3: X c= dom f by A1, Def3; for p being Real st 0 < p & p < 1 holds for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) proof let p be Real; ::_thesis: ( 0 < p & p < 1 implies for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) ) assume A4: ( 0 < p & p < 1 ) ; ::_thesis: for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) proof let r, s be Real; ::_thesis: ( r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s implies f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) ) assume that A5: ( r in X & s in X ) and A6: (p * r) + ((1 - p) * s) in X and A7: r <> s ; ::_thesis: f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) f . r <> f . s by A2, A3, A5, A7, FUNCT_1:def_4; hence f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) by A1, A4, A5, A6, Def3; ::_thesis: verum end; hence for r, s being Real st r in X & s in X & (p * r) + ((1 - p) * s) in X & r <> s holds f . ((p * r) + ((1 - p) * s)) < max ((f . r),(f . s)) ; ::_thesis: verum end; hence f is_strongly_quasiconvex_on X by A3, Def4; ::_thesis: verum end;