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)))