:: Introduction to Stochastic Finance: Random-Variables and Arbitrage Theory
:: by Peter Jaeger
::
:: Received March 27, 2018
:: Copyright (c) 2018-2021 Association of Mizar Users


theorem A1: :: FINANCE6:1
].0,+infty.[ is Element of Borel_Sets
proof end;

theorem :: FINANCE6:2
for Omega being non empty set
for F being SigmaField of Omega
for RV being random_variable of F, Borel_Sets
for K being Element of REAL
for g2 being Function of Omega,REAL st g2 = chi (((RV - (Omega --> K)) " [.0,+infty.[),Omega) holds
Call-Option (RV,K) = g2 (#) (RV - (Omega --> K))
proof end;

theorem TH1: :: FINANCE6:3
for Omega being non empty set
for F being SigmaField of Omega
for RV being random_variable of F, Borel_Sets
for K being Real holds (Omega --> K) - RV is random_variable of F, Borel_Sets
proof end;

theorem ZZZ: :: FINANCE6:4
for Omega being non empty set
for F being SigmaField of Omega
for A being Element of F holds chi (A,Omega) is random_variable of F, Borel_Sets
proof end;

registration
let Omega be non empty set ;
let F be SigmaField of Omega;
cluster Relation-like Omega -defined REAL -valued Function-like non empty V14(Omega) V18(Omega, REAL ) V39() V40() V41() F, Borel_Sets -random_variable-like for Element of Trivial-SigmaField K20(Omega,REAL);
existence
ex b1 being Function of Omega,REAL st b1 is F, Borel_Sets -random_variable-like
proof end;
end;

theorem ChiRandom: :: FINANCE6:5
for Omega being non empty set
for F being SigmaField of Omega holds chi (Omega,Omega) is b2, Borel_Sets -random_variable-like Function of Omega,REAL
proof end;

theorem Lemma00: :: FINANCE6:6
for Omega being non empty set
for F being SigmaField of Omega
for f, RV being random_variable of F, Borel_Sets
for K being Real holds (f - RV) " [.0,+infty.[ is Element of F
proof end;

LemmaRandom: for Omega being non empty set
for F being SigmaField of Omega
for RV being random_variable of F, Borel_Sets
for K being Real holds chi (((RV - (Omega --> K)) " [.0,+infty.[),Omega) is random_variable of F, Borel_Sets
proof end;

definition
let Omega be non empty set ;
let F be SigmaField of Omega;
let RV be random_variable of F, Borel_Sets ;
let K be Real;
:: original: Call-Option
redefine func Call-Option (RV,K) -> random_variable of F, Borel_Sets ;
correctness
coherence
Call-Option (RV,K) is random_variable of F, Borel_Sets ;
proof end;
end;

definition
let Omega be non empty set ;
let F be SigmaField of Omega;
let RV be random_variable of F, Borel_Sets ;
let K be Real;
func Put-Option (RV,K) -> Function of Omega,REAL means :Def30: :: FINANCE6:def 1
 for w being Element of Omega holds
( ( ((Omega --> K) - RV) . w >= 0 implies it . w = ((Omega --> K) - RV) . w ) & ( ((Omega --> K) - RV) . w < 0 implies it . w = 0 ) );
existence
ex b1 being Function of Omega,REAL st
for w being Element of Omega holds
( ( ((Omega --> K) - RV) . w >= 0 implies b1 . w = ((Omega --> K) - RV) . w ) & ( ((Omega --> K) - RV) . w < 0 implies b1 . w = 0 ) )
proof end;
uniqueness
for b1, b2 being Function of Omega,REAL st ( for w being Element of Omega holds
( ( ((Omega --> K) - RV) . w >= 0 implies b1 . w = ((Omega --> K) - RV) . w ) & ( ((Omega --> K) - RV) . w < 0 implies b1 . w = 0 ) ) ) & ( for w being Element of Omega holds
( ( ((Omega --> K) - RV) . w >= 0 implies b2 . w = ((Omega --> K) - RV) . w ) & ( ((Omega --> K) - RV) . w < 0 implies b2 . w = 0 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def30 defines Put-Option FINANCE6:def 1 :
for Omega being non empty set
for F being SigmaField of Omega
for RV being random_variable of F, Borel_Sets
for K being Real
for b5 being Function of Omega,REAL holds
( b5 = Put-Option (RV,K) iff for w being Element of Omega holds
( ( ((Omega --> K) - RV) . w >= 0 implies b5 . w = ((Omega --> K) - RV) . w ) & ( ((Omega --> K) - RV) . w < 0 implies b5 . w = 0 ) ) );

theorem JA3: :: FINANCE6:7
for Omega being non empty set
for F being SigmaField of Omega
for RV being random_variable of F, Borel_Sets
for K being Real
for g2 being Function of Omega,REAL st g2 = chi ((((Omega --> K) - RV) " [.0,+infty.[),Omega) holds
Put-Option (RV,K) = g2 (#) ((Omega --> K) - RV)
proof end;

definition
let Omega be non empty set ;
let F be SigmaField of Omega;
let RV be random_variable of F, Borel_Sets ;
let K be Real;
:: original: Put-Option
redefine func Put-Option (RV,K) -> random_variable of F, Borel_Sets ;
correctness
coherence
Put-Option (RV,K) is random_variable of F, Borel_Sets ;
proof end;
end;

definition
let Omega be non empty set ;
let F be SigmaField of Omega;
let RV be random_variable of F, Borel_Sets ;
let K be Real;
func Straddle (RV,K) -> random_variable of F, Borel_Sets equals :: FINANCE6:def 2
(Put-Option (RV,K)) + (Call-Option (RV,K));
coherence
(Put-Option (RV,K)) + (Call-Option (RV,K)) is random_variable of F, Borel_Sets by FINANCE2:23;
end;

:: deftheorem defines Straddle FINANCE6:def 2 :
for Omega being non empty set
for F being SigmaField of Omega
for RV being random_variable of F, Borel_Sets
for K being Real holds Straddle (RV,K) = (Put-Option (RV,K)) + (Call-Option (RV,K));

theorem :: FINANCE6:8
for Omega being non empty set
for F being SigmaField of Omega
for RV being random_variable of F, Borel_Sets
for K being Real
for w being Element of Omega holds (Straddle (RV,K)) . w = |.((RV - (Omega --> K)) . w).|
proof end;

definition
let Omega be non empty set ;
let F be SigmaField of Omega;
func set_of_constant_RV F -> set equals :: FINANCE6:def 3
 { f where f is Function of Omega,REAL : ( f is random_variable of F, Borel_Sets & f is constant ) } ;
coherence
{ f where f is Function of Omega,REAL : ( f is random_variable of F, Borel_Sets & f is constant ) } is set ;
func set_of_chi_RV F -> set equals :: FINANCE6:def 4
 { (chi (A,Omega)) where A is Element of F : chi (A,Omega) is random_variable of F, Borel_Sets } ;
coherence
{ (chi (A,Omega)) where A is Element of F : chi (A,Omega) is random_variable of F, Borel_Sets } is set ;
end;

:: deftheorem defines set_of_constant_RV FINANCE6:def 3 :
for Omega being non empty set
for F being SigmaField of Omega holds set_of_constant_RV F = { f where f is Function of Omega,REAL : ( f is random_variable of F, Borel_Sets & f is constant ) } ;

:: deftheorem defines set_of_chi_RV FINANCE6:def 4 :
for Omega being non empty set
for F being SigmaField of Omega holds set_of_chi_RV F = { (chi (A,Omega)) where A is Element of F : chi (A,Omega) is random_variable of F, Borel_Sets } ;

definition
let Omega be non empty set ;
let F be SigmaField of Omega;
let X be set ;
attr X is F -random-membered means :RanDef: :: FINANCE6:def 5
 for x being object st x in X holds
x is random_variable of F, Borel_Sets ;
end;

:: deftheorem RanDef defines -random-membered FINANCE6:def 5 :
for Omega being non empty set
for F being SigmaField of Omega
for X being set holds
( X is F -random-membered iff for x being object st x in X holds
x is random_variable of F, Borel_Sets );

registration
let Omega be non empty set ;
let F be SigmaField of Omega;
cluster set_of_constant_RV F -> non empty ;
coherence
not set_of_constant_RV F is empty
proof end;
cluster set_of_chi_RV F -> non empty ;
coherence
not set_of_chi_RV F is empty
proof end;
end;

registration
let Omega be non empty set ;
let F be SigmaField of Omega;
cluster set_of_constant_RV F -> F -random-membered ;
coherence
set_of_constant_RV F is F -random-membered
proof end;
cluster set_of_chi_RV F -> F -random-membered ;
coherence
set_of_chi_RV F is F -random-membered
proof end;
end;

registration
let Omega be non empty set ;
let F be SigmaField of Omega;
cluster non empty F -random-membered for set ;
existence
ex b1 being set st
( b1 is F -random-membered & not b1 is empty )
proof end;
end;

definition
let Omega be non empty set ;
let F be SigmaField of Omega;
let D be non empty F -random-membered set ;
let ChiFuncs be sequence of D;
let n be Nat;
func Conv_RV (ChiFuncs,n) -> random_variable of F, Borel_Sets equals :: FINANCE6:def 6
ChiFuncs . n;
coherence
ChiFuncs . n is random_variable of F, Borel_Sets by RanDef;
end;

:: deftheorem defines Conv_RV FINANCE6:def 6 :
for Omega being non empty set
for F being SigmaField of Omega
for D being non empty b2 -random-membered set
for ChiFuncs being sequence of D
for n being Nat holds Conv_RV (ChiFuncs,n) = ChiFuncs . n;

definition
let Omega be non empty set ;
let F be SigmaField of Omega;
let D be non empty F -random-membered set ;
let ConstFuncs be sequence of D;
let w be Element of Omega;
func Conv2_RV (ConstFuncs,w) -> Function of NAT,REAL means :Def770: :: FINANCE6:def 7
 for n being Nat holds it . n = (Conv_RV (ConstFuncs,n)) . w;
existence
ex b1 being Function of NAT,REAL st
for n being Nat holds b1 . n = (Conv_RV (ConstFuncs,n)) . w
proof end;
uniqueness
for b1, b2 being Function of NAT,REAL st ( for n being Nat holds b1 . n = (Conv_RV (ConstFuncs,n)) . w ) & ( for n being Nat holds b2 . n = (Conv_RV (ConstFuncs,n)) . w ) holds
b1 = b2
proof end;
end;

:: deftheorem Def770 defines Conv2_RV FINANCE6:def 7 :
for Omega being non empty set
for F being SigmaField of Omega
for D being non empty b2 -random-membered set
for ConstFuncs being sequence of D
for w being Element of Omega
for b6 being Function of NAT,REAL holds
( b6 = Conv2_RV (ConstFuncs,w) iff for n being Nat holds b6 . n = (Conv_RV (ConstFuncs,n)) . w );

definition
let Omega be non empty set ;
let F be SigmaField of Omega;
let D1, D2 be non empty F -random-membered set ;
let ChiFuncs be sequence of D1;
let ConstFuncs be sequence of D2;
let n be Nat;
func simple_RV_help (ChiFuncs,ConstFuncs,n) -> Function of Omega,REAL means :Def777: :: FINANCE6:def 8
 for w being Element of Omega holds it . w = (Partial_Sums ((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w)))) . n;
existence
ex b1 being Function of Omega,REAL st
for w being Element of Omega holds b1 . w = (Partial_Sums ((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w)))) . n
proof end;
uniqueness
for b1, b2 being Function of Omega,REAL st ( for w being Element of Omega holds b1 . w = (Partial_Sums ((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w)))) . n ) & ( for w being Element of Omega holds b2 . w = (Partial_Sums ((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w)))) . n ) holds
b1 = b2
proof end;
end;

:: deftheorem Def777 defines simple_RV_help FINANCE6:def 8 :
for Omega being non empty set
for F being SigmaField of Omega
for D1, D2 being non empty b2 -random-membered set
for ChiFuncs being sequence of D1
for ConstFuncs being sequence of D2
for n being Nat
for b8 being Function of Omega,REAL holds
( b8 = simple_RV_help (ChiFuncs,ConstFuncs,n) iff for w being Element of Omega holds b8 . w = (Partial_Sums ((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w)))) . n );

definition
let Omega be non empty set ;
let F be SigmaField of Omega;
let D1, D2 be non empty F -random-membered set ;
let ChiFuncs be sequence of D1;
let ConstFuncs be sequence of D2;
let n be Nat;
:: original: simple_RV_help
redefine func simple_RV_help (ChiFuncs,ConstFuncs,n) -> random_variable of F, Borel_Sets ;
correctness
coherence
simple_RV_help (ChiFuncs,ConstFuncs,n) is random_variable of F, Borel_Sets ;
proof end;
end;

Lemacik: for Omega being non empty set
for F being SigmaField of Omega
for x being object holds
( x in set_of_random_variables_on (F,Borel_Sets) iff x is random_variable of F, Borel_Sets )
proof end;

definition
let Omega be non empty set ;
let F be SigmaField of Omega;
let q be Nat;
let G be sequence of (set_of_random_variables_on (F,Borel_Sets));
func Change_Element_to_Func (G,q) -> Real-Valued-Random-Variable of F equals :: FINANCE6:def 9
G . q;
coherence
G . q is Real-Valued-Random-Variable of F
proof end;
end;

:: deftheorem defines Change_Element_to_Func FINANCE6:def 9 :
for Omega being non empty set
for F being SigmaField of Omega
for q being Nat
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) holds Change_Element_to_Func (G,q) = G . q;

definition
let phi be Real_Sequence;
let Omega be non empty set ;
let F be SigmaField of Omega;
let G be sequence of (set_of_random_variables_on (F,Borel_Sets));
let n be Nat;
func ArbitrageElSigma1 (phi,Omega,F,G,n) -> Element of F equals :: FINANCE6:def 10
(RVPortfolioValueFutExt (phi,F,G,n)) " [.0,+infty.[;
correctness
coherence
(RVPortfolioValueFutExt (phi,F,G,n)) " [.0,+infty.[ is Element of F;
proof end;
func ArbitrageElSigma2 (phi,Omega,F,G,n) -> Element of F equals :: FINANCE6:def 11
(RVPortfolioValueFutExt (phi,F,G,n)) " ].0,+infty.[;
correctness
coherence
(RVPortfolioValueFutExt (phi,F,G,n)) " ].0,+infty.[ is Element of F;
proof end;
end;

:: deftheorem defines ArbitrageElSigma1 FINANCE6:def 10 :
for phi being Real_Sequence
for Omega being non empty set
for F being SigmaField of Omega
for G being sequence of (set_of_random_variables_on (F,Borel_Sets))
for n being Nat holds ArbitrageElSigma1 (phi,Omega,F,G,n) = (RVPortfolioValueFutExt (phi,F,G,n)) " [.0,+infty.[;

:: deftheorem defines ArbitrageElSigma2 FINANCE6:def 11 :
for phi being Real_Sequence
for Omega being non empty set
for F being SigmaField of Omega
for G being sequence of (set_of_random_variables_on (F,Borel_Sets))
for n being Nat holds ArbitrageElSigma2 (phi,Omega,F,G,n) = (RVPortfolioValueFutExt (phi,F,G,n)) " ].0,+infty.[;

definition
let Omega be non empty set ;
let F be SigmaField of Omega;
let Prob be Probability of F;
let G be sequence of (set_of_random_variables_on (F,Borel_Sets));
let jpi be pricefunction ;
let n be Nat;
pred Arbitrage_Opportunity_exists_wrt Prob,G,jpi,n means :: FINANCE6:def 12
 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 );
end;

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

definition
let r be Real;
func RVfirst r -> Element of set_of_random_variables_on (Special_SigmaField1,Borel_Sets) equals :: FINANCE6:def 13
{1,2,3,4} --> r;
correctness
coherence
{1,2,3,4} --> r is Element of set_of_random_variables_on (Special_SigmaField1,Borel_Sets);
proof end;
end;

:: deftheorem defines RVfirst FINANCE6:def 13 :
for r being Real holds RVfirst r = {1,2,3,4} --> r;

definition
let jpi be pricefunction ;
let r be Real;
let d be Nat;
func RVfourth (jpi,r,d) -> Element of set_of_random_variables_on (Special_SigmaField2,Borel_Sets) equals :: FINANCE6:def 14
 RVfirst ((jpi . d) * (1 + r));
correctness
coherence
RVfirst ((jpi . d) * (1 + r)) is Element of set_of_random_variables_on (Special_SigmaField2,Borel_Sets);
proof end;
end;

:: deftheorem defines RVfourth FINANCE6:def 14 :
for jpi being pricefunction
for r being Real
for d being Nat holds RVfourth (jpi,r,d) = RVfirst ((jpi . d) * (1 + r));

theorem :: FINANCE6:9
ex G being sequence of (set_of_random_variables_on (Special_SigmaField1,Borel_Sets)) st
( G . 0 = {1,2,3,4} --> 1 & G . 1 = {1,2,3,4} --> 5 & ( for k being Nat st k > 1 holds
G . k = {1,2,3,4} --> 0 ) )
proof end;

theorem :: FINANCE6:10
for Prob being Probability of Special_SigmaField1
for G being sequence of (set_of_random_variables_on (Special_SigmaField1,Borel_Sets)) st G . 0 = {1,2,3,4} --> 1 & G . 1 = {1,2,3,4} --> 5 & ( for k being Nat st k > 1 holds
G . k = {1,2,3,4} --> 0 ) holds
ex jpi being pricefunction st Arbitrage_Opportunity_exists_wrt Prob,G,jpi,1
proof end;

theorem JB1: :: FINANCE6:11
for Omega being non empty set
for F being SigmaField of Omega
for phi being Real_Sequence
for n being Nat
for r being Real
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) holds { w where w is Element of Omega : PortfolioValueFutExt (n,phi,F,G,w) >= 0 } = (RVPortfolioValueFutExt (phi,F,G,n)) " [.0,+infty.[
proof end;

theorem JB2: :: FINANCE6:12
for Omega being non empty set
for F being SigmaField of Omega
for phi being Real_Sequence
for jpi being pricefunction
for d, d2 being Nat st d2 = d - 1 holds
for r being Real
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) holds { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } = ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " [.0,+infty.[
proof end;

theorem JB3: :: FINANCE6:13
for Omega being non empty set
for F being SigmaField of Omega
for phi being Real_Sequence
for jpi being pricefunction
for d, d2 being Nat
for r being Real
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) holds ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " [.0,+infty.[ is Event of F
proof end;

theorem JC1: :: FINANCE6:14
for Omega being non empty set
for F being SigmaField of Omega
for phi being Real_Sequence
for d being Nat
for r being Real
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) holds { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) > 0 } = (RVPortfolioValueFutExt (phi,F,G,d)) " ].0,+infty.[
proof end;

theorem JC2: :: FINANCE6:15
for Omega being non empty set
for F being SigmaField of Omega
for phi being Real_Sequence
for jpi being pricefunction
for d, d2 being Nat st d2 = d - 1 holds
for r being Real
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) holds { w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } = ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[
proof end;

ZZ: [.0,+infty.[ \ {0} = ].0,+infty.[
by XXREAL_1:136;

theorem JC3: :: FINANCE6:16
for Omega being non empty set
for F being SigmaField of Omega
for phi being Real_Sequence
for jpi being pricefunction
for d, d2 being Nat
for r being Real
for G being sequence of (set_of_random_variables_on (F,Borel_Sets)) holds ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " ].0,+infty.[ is Event of F
proof end;

theorem :: FINANCE6:17
for Omega being non empty set
for F being SigmaField of Omega
for jpi being pricefunction
for d, d2 being Nat st d > 0 & d2 = d - 1 holds
for Prob being Probability of F
for r being Real st r > - 1 holds
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
( Arbitrage_Opportunity_exists_wrt Prob,G,jpi,d iff ex myphi being Real_Sequence st
( Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " [.0,+infty.[) = 1 & Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " ].0,+infty.[) > 0 ) )
proof end;

definition
let Omega be non empty set ;
let F be SigmaField of Omega;
let RV be Real-Valued-Random-Variable of F;
let r be Real;
func Real_RV (r,RV) -> Real-Valued-Random-Variable of F equals :: FINANCE6:def 15
RV (#) (1 / (1 + r));
correctness
coherence
RV (#) (1 / (1 + r)) is Real-Valued-Random-Variable of F;
proof end;
end;

:: deftheorem defines Real_RV FINANCE6:def 15 :
for Omega being non empty set
for F being SigmaField of Omega
for RV being Real-Valued-Random-Variable of F
for r being Real holds Real_RV (r,RV) = RV (#) (1 / (1 + r));

definition
let Omega be non empty set ;
let F be SigmaField of Omega;
let jpi be pricefunction ;
let G be sequence of (set_of_random_variables_on (F,Borel_Sets));
let r be Real;
pred Risk_neutral_measure_exists_wrt G,jpi,r means :: FINANCE6:def 16
 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);
end;

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

theorem ThArbPrel: :: FINANCE6:18
for Prob being Probability of Special_SigmaField2
for r being Real st r > 0 holds
for jpi being pricefunction
for d being Nat ex f being Real-Valued-Random-Variable of Special_SigmaField2 st
( f = {1,2,3,4} --> ((jpi . d) * (1 + r)) & f is_integrable_on P2M Prob & f is_simple_func_in Special_SigmaField2 )
proof end;

theorem ThArb: :: FINANCE6:19
for Prob being Probability of Special_SigmaField2
for n being Nat
for r being Real st r > 0 holds
for jpi being pricefunction
for d being Nat
for RV being Real-Valued-Random-Variable of Special_SigmaField2 st RV = {1,2,3,4} --> ((jpi . d) * (1 + r)) & RV is_integrable_on P2M Prob & RV is_simple_func_in Special_SigmaField2 holds
jpi . d = expect ((Real_RV (r,RV)),Prob)
proof end;

theorem :: FINANCE6:20
for Prob being Probability of Special_SigmaField2
for r being Real st r > 0 holds
for jpi being pricefunction ex G being sequence of (set_of_random_variables_on (Special_SigmaField2,Borel_Sets)) st
for d being Nat holds
( G . d = {1,2,3,4} --> ((jpi . d) * (1 + r)) & Change_Element_to_Func (G,d) is_integrable_on P2M Prob & Change_Element_to_Func (G,d) is_simple_func_in Special_SigmaField2 )
proof end;

theorem :: FINANCE6:21
for Prob being Probability of Special_SigmaField2
for r being Real st r > 0 holds
for jpi being pricefunction
for G being sequence of (set_of_random_variables_on (Special_SigmaField2,Borel_Sets)) st ( for d being Nat holds
( G . d = {1,2,3,4} --> ((jpi . d) * (1 + r)) & Change_Element_to_Func (G,d) is_integrable_on P2M Prob & Change_Element_to_Func (G,d) is_simple_func_in Special_SigmaField2 ) ) holds
( Risk_neutral_measure_exists_wrt G,jpi,r & ( for s being Nat holds jpi . s = expect ((Real_RV (r,(Change_Element_to_Func (G,s)))),Prob) ) )
proof end;