begin
:: deftheorem defines max+ RFUNCT_3:def 1 :
for r being real number holds max+ r = max r,0 ;
:: deftheorem defines max- RFUNCT_3:def 2 :
for r being real number holds max- r = max (- r),0 ;
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
Lm1:
for n being Element of NAT
for D being non empty set
for f being FinSequence of D st len f <= n holds
f | n = f
Lm2:
for f being Function
for x being set st not x in rng f holds
f " {x} = {}
begin
theorem
canceled;
theorem
canceled;
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem
theorem
:: deftheorem Def3 defines PartFunc-set RFUNCT_3:def 3 :
for X, Y being set
for b3 being set holds
( b3 is PartFunc-set of X,Y iff for x being Element of b3 holds x is PartFunc of X,Y );
definition
let D be non
empty set ;
let E be
real-membered set ;
let F1,
F2 be
Element of
PFuncs D,
E;
+redefine func F1 + F2 -> Element of
PFuncs D,
REAL ;
coherence
F1 + F2 is Element of PFuncs D,REAL
-redefine func F1 - F2 -> Element of
PFuncs D,
REAL ;
coherence
F1 - F2 is Element of PFuncs D,REAL
(#)redefine func F1 (#) F2 -> Element of
PFuncs D,
REAL ;
coherence
F1 (#) F2 is Element of PFuncs D,REAL
/redefine func F1 / F2 -> Element of
PFuncs D,
REAL ;
coherence
F1 / F2 is Element of PFuncs D,REAL
end;
definition
let D be non
empty set ;
func addpfunc D -> BinOp of
(PFuncs D,REAL ) means :
Def4:
for
F1,
F2 being
Element of
PFuncs D,
REAL holds
it . F1,
F2 = F1 + F2;
existence
ex b1 being BinOp of (PFuncs D,REAL ) st
for F1, F2 being Element of PFuncs D,REAL holds b1 . F1,F2 = F1 + F2
uniqueness
for b1, b2 being BinOp of (PFuncs D,REAL ) st ( for F1, F2 being Element of PFuncs D,REAL holds b1 . F1,F2 = F1 + F2 ) & ( for F1, F2 being Element of PFuncs D,REAL holds b2 . F1,F2 = F1 + F2 ) holds
b1 = b2
end;
:: deftheorem Def4 defines addpfunc RFUNCT_3:def 4 :
for D being non empty set
for b2 being BinOp of (PFuncs D,REAL ) holds
( b2 = addpfunc D iff for F1, F2 being Element of PFuncs D,REAL holds b2 . F1,F2 = F1 + F2 );
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
:: deftheorem defines Sum RFUNCT_3:def 5 :
for D being non empty set
for f being FinSequence of PFuncs D,REAL holds Sum f = (addpfunc D) $$ f;
theorem Th21:
theorem
canceled;
theorem Th23:
theorem Th24:
theorem
theorem Th26:
theorem
theorem
:: deftheorem Def6 defines CHI RFUNCT_3:def 6 :
for D being non empty set
for f being FinSequence
for b3 being FinSequence of PFuncs D,REAL holds
( b3 = CHI f,D iff ( len b3 = len f & ( for n being Element of NAT st n in dom b3 holds
b3 . n = chi (f . n),D ) ) );
definition
let D be non
empty set ;
let f be
FinSequence of
PFuncs D,
REAL ;
let R be
FinSequence of
REAL ;
func R (#) f -> FinSequence of
PFuncs D,
REAL means :
Def7:
(
len it = min (len R),
(len f) & ( for
n being
Element of
NAT st
n in dom it holds
for
F being
PartFunc of
D,
REAL for
r being
Real st
r = R . n &
F = f . n holds
it . n = r (#) F ) );
existence
ex b1 being FinSequence of PFuncs D,REAL st
( len b1 = min (len R),(len f) & ( for n being Element of NAT st n in dom b1 holds
for F being PartFunc of D,REAL
for r being Real st r = R . n & F = f . n holds
b1 . n = r (#) F ) )
uniqueness
for b1, b2 being FinSequence of PFuncs D,REAL st len b1 = min (len R),(len f) & ( for n being Element of NAT st n in dom b1 holds
for F being PartFunc of D,REAL
for r being Real st r = R . n & F = f . n holds
b1 . n = r (#) F ) & len b2 = min (len R),(len f) & ( for n being Element of NAT st n in dom b2 holds
for F being PartFunc of D,REAL
for r being Real st r = R . n & F = f . n holds
b2 . n = r (#) F ) holds
b1 = b2
end;
:: deftheorem Def7 defines (#) RFUNCT_3:def 7 :
for D being non empty set
for f being FinSequence of PFuncs D,REAL
for R being FinSequence of REAL
for b4 being FinSequence of PFuncs D,REAL holds
( b4 = R (#) f iff ( len b4 = min (len R),(len f) & ( for n being Element of NAT st n in dom b4 holds
for F being PartFunc of D,REAL
for r being Real st r = R . n & F = f . n holds
b4 . n = r (#) F ) ) );
:: deftheorem Def8 defines # RFUNCT_3:def 8 :
for D being non empty set
for f being FinSequence of PFuncs D,REAL
for d being Element of D
for b4 being FinSequence of REAL holds
( b4 = f # d iff ( len b4 = len f & ( for n being Element of NAT
for G being Element of PFuncs D,REAL st n in dom b4 & f . n = G holds
b4 . n = G . d ) ) );
:: deftheorem Def9 defines is_common_for_dom RFUNCT_3:def 9 :
for D, C being non empty set
for f being FinSequence of PFuncs D,C
for d being Element of D holds
( d is_common_for_dom f iff for G being Element of PFuncs D,C
for n being Element of NAT st n in dom f & f . n = G holds
d in dom G );
theorem Th29:
theorem
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem
theorem
:: deftheorem Def10 defines max+ RFUNCT_3:def 10 :
for D being non empty set
for F, b3 being PartFunc of D,REAL holds
( b3 = max+ F iff ( dom b3 = dom F & ( for d being Element of D st d in dom b3 holds
b3 . d = max+ (F . d) ) ) );
:: deftheorem Def11 defines max- RFUNCT_3:def 11 :
for D being non empty set
for F, b3 being PartFunc of D,REAL holds
( b3 = max- F iff ( dom b3 = dom F & ( for d being Element of D st d in dom b3 holds
b3 . d = max- (F . d) ) ) );
theorem
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem
theorem
theorem
theorem Th47:
theorem
theorem Th49:
theorem
theorem Th51:
theorem
theorem Th53:
theorem
:: deftheorem RFUNCT_3:def 12 :
canceled;
:: deftheorem Def13 defines is_convex_on RFUNCT_3:def 13 :
for F being PartFunc of REAL ,REAL
for X being set holds
( F is_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 holds
F . ((p * r) + ((1 - p) * s)) <= (p * (F . r)) + ((1 - p) * (F . s)) ) ) );
theorem Th55:
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th62:
theorem
theorem Th64:
theorem
:: deftheorem Def14 defines FinS RFUNCT_3:def 14 :
for D being non empty set
for F being PartFunc of D,REAL
for X being set st dom (F | X) is finite holds
for b4 being non-increasing FinSequence of REAL holds
( b4 = FinS F,X iff F | X,b4 are_fiberwise_equipotent );
theorem Th66:
theorem Th67:
theorem Th68:
theorem Th69:
theorem Th70:
theorem Th71:
theorem Th72:
theorem Th73:
defpred S1[ Element of NAT ] means for D being non empty set
for F being PartFunc of D,REAL
for X, Y being set
for Z being finite set st Z = dom (F | Y) & dom (F | X) is finite & Y c= X & $1 = card Z & ( for d1, d2 being Element of D st d1 in dom (F | Y) & d2 in dom (F | (X \ Y)) holds
F . d1 >= F . d2 ) holds
FinS F,X = (FinS F,Y) ^ (FinS F,(X \ Y));
Lm3:
S1[ 0 ]
Lm4:
for n being Element of NAT st S1[n] holds
S1[n + 1]
theorem
theorem Th75:
theorem Th76:
theorem
theorem
theorem Th79:
:: deftheorem defines Sum RFUNCT_3:def 15 :
for D being non empty set
for F being PartFunc of D,REAL
for X being set holds Sum F,X = Sum (FinS F,X);
theorem Th80:
theorem Th81:
theorem
theorem
theorem
theorem
theorem
theorem