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