environ
vocabularies HIDDEN, FINANCE1, NUMBERS, XBOOLE_0, PROB_1, SUBSET_1, FUNCT_1, TARSKI, RELAT_1, CARD_1, ARYTM_1, CARD_3, PROB_3, NAT_1, ARYTM_3, XXREAL_0, SERIES_1, EQREL_1, SEQ_1, XXREAL_1, MESFUNC1, RANDOM_1, RANDOM_2, FUNCOP_1, VALUED_1, FUNCT_7, REAL_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, XCMPLX_0, XXREAL_0, NAT_1, XREAL_0, NUMBERS, FUNCT_1, RELSET_1, FUNCT_2, PROB_3, SERIES_1, PROB_1, MEASURE6, SEQ_1, MESFUNC1, MESFUNC6, RANDOM_1, XXREAL_1, RCOMP_1, FUNCOP_1, VALUED_1, RANDOM_2;
definitions TARSKI, FUNCT_2;
theorems SERIES_1, PROB_1, PROB_3, XBOOLE_0, NAT_1, FUNCT_2, XXREAL_0, ORDINAL1, TARSKI, XREAL_1, XXREAL_1, MESFUNC1, FINSUB_1, MESFUNC6, XREAL_0, RANDOM_1, RANDOM_2, FUNCOP_1, VALUED_1, FRECHET, XBOOLE_1, FUNCT_1;
schemes NAT_1, FUNCT_2, RECDEF_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, PROB_1, VALUED_0, XXREAL_0, NAT_1, XCMPLX_0, VALUED_1, FUNCT_2;
constructors HIDDEN, REAL_1, PROB_3, SERIES_1, BINOP_2, RELSET_1, MEASURE6, RCOMP_1, MESFUNC1, MESFUNC6, RANDOM_2;
requirements HIDDEN, SUBSET, NUMERALS, BOOLE, ARITHM, REAL;
equalities XXREAL_0, PROB_1, SUBSET_1;
expansions FUNCT_2;
Lm1:
for Omega, Omega2 being non empty set
for F being Function of Omega,Omega2
for y being non empty set holds { z where z is Element of Omega : F . z is Element of y } = F " y
theorem Th12:
for
Omega being non
empty set for
F being
SigmaField of
Omega for
d being
Nat st
d > 0 holds
for
r being
Real for
phi being
Real_Sequence for
G being
sequence of
(set_of_random_variables_on (F,Borel_Sets)) st
Element_Of (
F,
Borel_Sets,
G,
0)
= Omega --> (1 + r) holds
for
w being
Element of
Omega holds
PortfolioValueFutExt (
d,
phi,
F,
G,
w)
= ((1 + r) * (phi . 0)) + (PortfolioValueFut (d,phi,F,G,w))
theorem Th13:
for
Omega being non
empty set for
F being
SigmaField of
Omega for
d being
Nat st
d > 0 holds
for
r being
Real st
r > - 1 holds
for
phi being
Real_Sequence for
jpi being
pricefunction for
G being
sequence of
(set_of_random_variables_on (F,Borel_Sets)) st
Element_Of (
F,
Borel_Sets,
G,
0)
= Omega --> (1 + r) holds
for
w being
Element of
Omega st
BuyPortfolioExt (
phi,
jpi,
d)
<= 0 holds
PortfolioValueFutExt (
d,
phi,
F,
G,
w)
<= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d)))
theorem
for
Omega being non
empty set for
F being
SigmaField of
Omega for
d being
Nat st
d > 0 holds
for
r being
Real st
r > - 1 holds
for
phi being
Real_Sequence for
jpi being
pricefunction for
G being
sequence of
(set_of_random_variables_on (F,Borel_Sets)) st
Element_Of (
F,
Borel_Sets,
G,
0)
= Omega --> (1 + r) &
BuyPortfolioExt (
phi,
jpi,
d)
<= 0 holds
(
{ w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } &
{ w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } )