:: deftheorem defines Risk_neutral_measure_exists_wrt FINANCE6:def 16 :
for Omega being non empty set
for F being SigmaField of Omega
for jpi being pricefunction
for G being sequence of (set_of_random_variables_on (F,Borel_Sets))
for r being Real holds
( Risk_neutral_measure_exists_wrt G,jpi,r iff ex Prob being Probability of F st
for d being Nat holds jpi . d = expect ((Real_RV (r,(Change_Element_to_Func (G,d)))),Prob) );