:: deftheorem defines Arbitrage_Opportunity_exists_wrt FINANCE6:def 12 :
for Omega being non empty set
for F being SigmaField of Omega
for Prob being Probability of F
for G being sequence of (set_of_random_variables_on (F,Borel_Sets))
for jpi being pricefunction
for n being Nat holds
( Arbitrage_Opportunity_exists_wrt Prob,G,jpi,n iff ex phi being Real_Sequence st
( BuyPortfolioExt (phi,jpi,n) <= 0 & Prob . (ArbitrageElSigma1 (phi,Omega,F,G,n)) = 1 & Prob . (ArbitrageElSigma2 (phi,Omega,F,G,n)) > 0 ) );