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

H0:
proof end;

definition
let t be Real;
let n be Nat;
func Conv (n,t) -> Element of REAL equals :Def2: :: FINANCE6:def 1
t if n = 1
otherwise 0 ;
correctness
coherence
( ( n = 1 implies t is Element of REAL ) & ( not n = 1 implies 0 is Element of REAL ) )
;
consistency
for b1 being Element of REAL holds verum
;
by XREAL_0:def 1;
end;

:: deftheorem Def2 defines Conv FINANCE6:def 1 :
for t being Real
for n being Nat holds
( ( n = 1 implies Conv (n,t) = t ) & ( not n = 1 implies Conv (n,t) = 0 ) );

definition
let t be Real;
let n be Nat;
func Conv2 (n,t) -> Element of REAL equals :Def3: :: FINANCE6:def 2
1 if n = 0
otherwise Conv (n,t);
correctness
coherence
( ( n = 0 implies 1 is Element of REAL ) & ( not n = 0 implies Conv (n,t) is Element of REAL ) )
;
consistency
for b1 being Element of REAL holds verum
;
by NUMBERS:19;
end;

:: deftheorem Def3 defines Conv2 FINANCE6:def 2 :
for t being Real
for n being Nat holds
( ( n = 0 implies Conv2 (n,t) = 1 ) & ( not n = 0 implies Conv2 (n,t) = Conv (n,t) ) );

definition
let t be Real;
let n be Nat;
func Conv4 (n,t) -> Element of REAL equals :Def5: :: FINANCE6:def 3
- 1 if n = 0
otherwise Conv (n,t);
correctness
coherence
( ( n = 0 implies - 1 is Element of REAL ) & ( not n = 0 implies Conv (n,t) is Element of REAL ) )
;
consistency
for b1 being Element of REAL holds verum
;
by XREAL_0:def 1;
end;

:: deftheorem Def5 defines Conv4 FINANCE6:def 3 :
for t being Real
for n being Nat holds
( ( n = 0 implies Conv4 (n,t) = - 1 ) & ( not n = 0 implies Conv4 (n,t) = Conv (n,t) ) );

theorem A1: :: FINANCE6:1
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 Real holds chi (((RV - (Omega --> K)) " ),Omega) is Function of Omega,REAL
proof end;

theorem :: 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 Element of REAL
for g2 being Function of Omega,REAL st g2 = chi (((RV - (Omega --> K)) " ),Omega) holds
Call-Option (RV,K) = g2 (#) (RV - (Omega --> K))
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 Element of 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 RV be Function of Omega,REAL;
let w be Element of Omega;
func SetForPut-Option (RV,w) -> Element of REAL equals :Def2x: :: FINANCE6:def 4
RV . w if RV . w >= 0
otherwise 0 ;
correctness
coherence
( ( RV . w >= 0 implies RV . w is Element of REAL ) & ( not RV . w >= 0 implies 0 is Element of REAL ) )
;
consistency
for b1 being Element of REAL holds verum
;
by NUMBERS:19;
end;

:: deftheorem Def2x defines SetForPut-Option FINANCE6:def 4 :
for Omega being non empty set
for RV being Function of Omega,REAL
for w being Element of Omega holds
( ( RV . w >= 0 implies SetForPut-Option (RV,w) = RV . w ) & ( not RV . w >= 0 implies SetForPut-Option (RV,w) = 0 ) );

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 5
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 5 :
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 TH1: :: FINANCE6:4
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 JA2: :: FINANCE6:5
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 ((((Omega --> K) - RV) " ),Omega) is Function of Omega,REAL
proof end;

theorem JA3: :: FINANCE6:6
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) " ),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;

theorem :: FINANCE6:7
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;

theorem ChiRandom: :: FINANCE6:8
for Omega being non empty set
for F being SigmaField of Omega holds chi (Omega,Omega) is_random_variable_on 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 Element of REAL ;
func Straddle (RV,K) -> random_variable of F, Borel_Sets equals :: FINANCE6:def 6
(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 6 :
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 holds Straddle (RV,K) = (Put-Option (RV,K)) + (Call-Option (RV,K));

theorem :: FINANCE6:9
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 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 7
{ f where f is Function of Omega,REAL : ex K being Element of REAL st
( f is_random_variable_on F, Borel_Sets & f = Omega --> K )
}
;
coherence
{ f where f is Function of Omega,REAL : ex K being Element of REAL st
( f is_random_variable_on F, Borel_Sets & f = Omega --> K )
}
is set
;
end;

:: deftheorem defines set_of_constant_RV FINANCE6:def 7 :
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 : ex K being Element of REAL st
( f is_random_variable_on F, Borel_Sets & f = Omega --> K )
}
;

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

definition
let Omega be non empty set ;
let F be SigmaField of Omega;
func set_of_chi_RV F -> set equals :: FINANCE6:def 8
{ f where f is Function of Omega,REAL : ex A being Element of F st
( chi (A,Omega) is_random_variable_on F, Borel_Sets & chi (A,Omega) = f )
}
;
coherence
{ f where f is Function of Omega,REAL : ex A being Element of F st
( chi (A,Omega) is_random_variable_on F, Borel_Sets & chi (A,Omega) = f )
}
is set
;
end;

:: deftheorem defines set_of_chi_RV FINANCE6:def 8 :
for Omega being non empty set
for F being SigmaField of Omega holds set_of_chi_RV F = { f where f is Function of Omega,REAL : ex A being Element of F st
( chi (A,Omega) is_random_variable_on F, Borel_Sets & chi (A,Omega) = f )
}
;

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

definition
let Omega be non empty set ;
let F be SigmaField of Omega;
let ChiFuncs be sequence of ();
let n be Nat;
func Conv_chi_RV (ChiFuncs,n) -> random_variable of F, Borel_Sets equals :: FINANCE6:def 9
ChiFuncs . n;
correctness
coherence
ChiFuncs . n is random_variable of F, Borel_Sets
;
proof end;
end;

:: deftheorem defines Conv_chi_RV FINANCE6:def 9 :
for Omega being non empty set
for F being SigmaField of Omega
for ChiFuncs being sequence of ()
for n being Nat holds Conv_chi_RV (ChiFuncs,n) = ChiFuncs . n;

definition
let Omega be non empty set ;
let F be SigmaField of Omega;
let ConstFuncs be sequence of ;
let n be Nat;
func Conv_constant_RV (ConstFuncs,n) -> random_variable of F, Borel_Sets equals :: FINANCE6:def 10
ConstFuncs . n;
coherence
ConstFuncs . n is random_variable of F, Borel_Sets
proof end;
end;

:: deftheorem defines Conv_constant_RV FINANCE6:def 10 :
for Omega being non empty set
for F being SigmaField of Omega
for ConstFuncs being sequence of
for n being Nat holds Conv_constant_RV (ConstFuncs,n) = ConstFuncs . n;

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

:: deftheorem Def770 defines Conv2_constant_RV FINANCE6:def 11 :
for Omega being non empty set
for F being SigmaField of Omega
for ConstFuncs being sequence of
for w being Element of Omega
for b5 being Function of NAT,REAL holds
( b5 = Conv2_constant_RV (ConstFuncs,w) iff for n being Nat holds b5 . n = (Conv_constant_RV (ConstFuncs,n)) . w );

definition
let Omega be non empty set ;
let F be SigmaField of Omega;
let ChiFuncs be sequence of ();
let w be Element of Omega;
func Conv2_chi_RV (ChiFuncs,w) -> Function of NAT,REAL means :Def771: :: FINANCE6:def 12
for n being Nat holds it . n = (Conv_chi_RV (ChiFuncs,n)) . w;
existence
ex b1 being Function of NAT,REAL st
for n being Nat holds b1 . n = (Conv_chi_RV (ChiFuncs,n)) . w
proof end;
uniqueness
for b1, b2 being Function of NAT,REAL st ( for n being Nat holds b1 . n = (Conv_chi_RV (ChiFuncs,n)) . w ) & ( for n being Nat holds b2 . n = (Conv_chi_RV (ChiFuncs,n)) . w ) holds
b1 = b2
proof end;
end;

:: deftheorem Def771 defines Conv2_chi_RV FINANCE6:def 12 :
for Omega being non empty set
for F being SigmaField of Omega
for ChiFuncs being sequence of ()
for w being Element of Omega
for b5 being Function of NAT,REAL holds
( b5 = Conv2_chi_RV (ChiFuncs,w) iff for n being Nat holds b5 . n = (Conv_chi_RV (ChiFuncs,n)) . w );

definition
let Omega be non empty set ;
let F be SigmaField of Omega;
let ChiFuncs be sequence of ();
let ConstFuncs be sequence of ;
let n be Nat;
func simple_RV_help (ChiFuncs,ConstFuncs,n) -> Function of Omega,REAL means :Def777: :: FINANCE6:def 13
for w being Element of Omega holds it . w = (Partial_Sums ((Conv2_constant_RV (ConstFuncs,w)) (#) (Conv2_chi_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_constant_RV (ConstFuncs,w)) (#) (Conv2_chi_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_constant_RV (ConstFuncs,w)) (#) (Conv2_chi_RV (ChiFuncs,w)))) . n ) & ( for w being Element of Omega holds b2 . w = (Partial_Sums ((Conv2_constant_RV (ConstFuncs,w)) (#) (Conv2_chi_RV (ChiFuncs,w)))) . n ) holds
b1 = b2
proof end;
end;

:: deftheorem Def777 defines simple_RV_help FINANCE6:def 13 :
for Omega being non empty set
for F being SigmaField of Omega
for ChiFuncs being sequence of ()
for ConstFuncs being sequence of
for n being Nat
for b6 being Function of Omega,REAL holds
( b6 = simple_RV_help (ChiFuncs,ConstFuncs,n) iff for w being Element of Omega holds b6 . w = (Partial_Sums ((Conv2_constant_RV (ConstFuncs,w)) (#) (Conv2_chi_RV (ChiFuncs,w)))) . n );

definition
let Omega be non empty set ;
let F be SigmaField of Omega;
let ChiFuncs be sequence of ();
let ConstFuncs be sequence of ;
let n be Nat;
mode simple_RV of ConstFuncs,ChiFuncs,n -> random_variable of F, Borel_Sets means :: FINANCE6:def 14
for w being Element of Omega holds it . w = (simple_RV_help (ChiFuncs,ConstFuncs,n)) . w;
existence
ex b1 being random_variable of F, Borel_Sets st
for w being Element of Omega holds b1 . w = (simple_RV_help (ChiFuncs,ConstFuncs,n)) . w
proof end;
end;

:: deftheorem defines simple_RV FINANCE6:def 14 :
for Omega being non empty set
for F being SigmaField of Omega
for ChiFuncs being sequence of ()
for ConstFuncs being sequence of
for n being Nat
for b6 being random_variable of F, Borel_Sets holds
( b6 is simple_RV of ConstFuncs,ChiFuncs,n iff for w being Element of Omega holds b6 . w = (simple_RV_help (ChiFuncs,ConstFuncs,n)) . w );

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

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

theorem JA1: :: FINANCE6:10
for Omega being non empty set
for F being SigmaField of Omega
for phi being Real_Sequence
for G being sequence of
for n being Nat holds (RVPortfolioValueFutExt (phi,F,G,n)) " in F
proof end;

theorem JA2: :: FINANCE6:11
for Omega being non empty set
for F being SigmaField of Omega
for phi being Real_Sequence
for G being sequence of
for n being Nat holds (RVPortfolioValueFutExt (phi,F,G,n)) " in F
proof end;

definition
let phi be Real_Sequence;
let Omega be non empty set ;
let F be SigmaField of Omega;
let G be sequence of ;
let n be Nat;
func ArbitrageElSigma1 (phi,Omega,F,G,n) -> Element of F equals :: FINANCE6:def 16
(RVPortfolioValueFutExt (phi,F,G,n)) " ;
correctness
coherence
(RVPortfolioValueFutExt (phi,F,G,n)) " is Element of F
;
by JA1;
func ArbitrageElSigma2 (phi,Omega,F,G,n) -> Element of F equals :: FINANCE6:def 17
(RVPortfolioValueFutExt (phi,F,G,n)) " ;
correctness
coherence
(RVPortfolioValueFutExt (phi,F,G,n)) " is Element of F
;
by JA2;
end;

:: deftheorem defines ArbitrageElSigma1 FINANCE6:def 16 :
for phi being Real_Sequence
for Omega being non empty set
for F being SigmaField of Omega
for G being sequence of
for n being Nat holds ArbitrageElSigma1 (phi,Omega,F,G,n) = (RVPortfolioValueFutExt (phi,F,G,n)) " ;

:: deftheorem defines ArbitrageElSigma2 FINANCE6:def 17 :
for phi being Real_Sequence
for Omega being non empty set
for F being SigmaField of Omega
for G being sequence of
for n being Nat holds ArbitrageElSigma2 (phi,Omega,F,G,n) = (RVPortfolioValueFutExt (phi,F,G,n)) " ;

definition
let Omega be non empty set ;
let F be SigmaField of Omega;
let Prob be Probability of F;
let G be sequence of ;
let jpi be pricefunction ;
let n be Nat;
pred Arbitrage_Opportunity_exists_wrt Prob,G,jpi,n means :: FINANCE6:def 18
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 18 :
for Omega being non empty set
for F being SigmaField of Omega
for Prob being Probability of F
for G being sequence of
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;
correctness
coherence ;
proof end;
end;

:: deftheorem defines RVfirst FINANCE6:def 19 :
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 20
{1,2,3,4} --> ((jpi . d) * (1 + r));
correctness
coherence
{1,2,3,4} --> ((jpi . d) * (1 + r)) is Element of set_of_random_variables_on (Special_SigmaField2,Borel_Sets)
;
proof end;
end;

:: deftheorem defines RVfourth FINANCE6:def 20 :
for jpi being pricefunction
for r being Real
for d being Nat holds RVfourth (jpi,r,d) = {1,2,3,4} --> ((jpi . d) * (1 + r));

definition
let n be Nat;
func RVswitchsecond n -> Element of set_of_random_variables_on (Special_SigmaField1,Borel_Sets) equals :Def61: :: FINANCE6:def 21
RVfirst 5 if n = 1
otherwise RVfirst 0;
correctness
coherence
( ( n = 1 implies RVfirst 5 is Element of set_of_random_variables_on (Special_SigmaField1,Borel_Sets) ) & ( not n = 1 implies RVfirst 0 is Element of set_of_random_variables_on (Special_SigmaField1,Borel_Sets) ) )
;
consistency
for b1 being Element of set_of_random_variables_on (Special_SigmaField1,Borel_Sets) holds verum
;
;
end;

:: deftheorem Def61 defines RVswitchsecond FINANCE6:def 21 :
for n being Nat holds
( ( n = 1 implies RVswitchsecond n = RVfirst 5 ) & ( not n = 1 implies RVswitchsecond n = RVfirst 0 ) );

definition
let n be Nat;
func RVswitchfirst n -> Element of set_of_random_variables_on (Special_SigmaField1,Borel_Sets) equals :Def60: :: FINANCE6:def 22
RVfirst 1 if n = 0
otherwise RVswitchsecond n;
correctness
coherence
( ( n = 0 implies RVfirst 1 is Element of set_of_random_variables_on (Special_SigmaField1,Borel_Sets) ) & ( not n = 0 implies RVswitchsecond n is Element of set_of_random_variables_on (Special_SigmaField1,Borel_Sets) ) )
;
consistency
for b1 being Element of set_of_random_variables_on (Special_SigmaField1,Borel_Sets) holds verum
;
;
end;

:: deftheorem Def60 defines RVswitchfirst FINANCE6:def 22 :
for n being Nat holds
( ( n = 0 implies RVswitchfirst n = RVfirst 1 ) & ( not n = 0 implies RVswitchfirst n = RVswitchsecond n ) );

theorem :: FINANCE6:12
ex G being sequence of 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:13
for Prob being Probability of Special_SigmaField1
for G being sequence of 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:14
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 holds { w where w is Element of Omega : PortfolioValueFutExt (n,phi,F,G,w) >= 0 } = (RVPortfolioValueFutExt (phi,F,G,n)) "
proof end;

theorem JB2: :: 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 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))))) "
proof end;

theorem JB3: :: 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 holds ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " is Event of F
proof end;

theorem JC1: :: FINANCE6:17
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 holds { w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) > 0 } = (RVPortfolioValueFutExt (phi,F,G,d)) "
proof end;

theorem JC2: :: FINANCE6:18
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 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))))) "
proof end;

ZZ:
by XXREAL_1:136;

theorem JC3: :: FINANCE6:19
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 holds ((RVPortfolioValueFut (phi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (phi,jpi,d))))) " is Event of F
proof end;

definition
let d, n be Nat;
let jpi be pricefunction ;
let phi be Real_Sequence;
func Helpme (phi,jpi,n,d) -> Element of REAL equals :Def444: :: FINANCE6:def 23
- (BuyPortfolio (phi,jpi,d)) if n = 0
otherwise phi . n;
correctness
coherence
( ( n = 0 implies - (BuyPortfolio (phi,jpi,d)) is Element of REAL ) & ( not n = 0 implies phi . n is Element of REAL ) )
;
consistency
for b1 being Element of REAL holds verum
;
by XREAL_0:def 1;
end;

:: deftheorem Def444 defines Helpme FINANCE6:def 23 :
for d, n being Nat
for jpi being pricefunction
for phi being Real_Sequence holds
( ( n = 0 implies Helpme (phi,jpi,n,d) = - (BuyPortfolio (phi,jpi,d)) ) & ( not n = 0 implies Helpme (phi,jpi,n,d) = phi . n ) );

theorem :: FINANCE6:20
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 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))))) " ) = 1 & Prob . (((RVPortfolioValueFut (myphi,F,G,d2)) - (Omega --> ((1 + r) * (BuyPortfolio (myphi,jpi,d))))) " ) > 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 d be Nat;
let r be Real;
func Real_RV (d,r,RV) -> Real-Valued-Random-Variable of F equals :: FINANCE6:def 24
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 24 :
for Omega being non empty set
for F being SigmaField of Omega
for RV being Real-Valued-Random-Variable of F
for d being Nat
for r being Real holds Real_RV (d,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 ;
let r be Real;
pred Risk_neutral_measure_exists_wrt G,jpi,r means :: FINANCE6:def 25
ex Prob being Probability of F st
for d being Nat holds jpi . d = expect ((Real_RV (d,r,())),Prob);
end;

:: deftheorem defines Risk_neutral_measure_exists_wrt FINANCE6:def 25 :
for Omega being non empty set
for F being SigmaField of Omega
for jpi being pricefunction
for G being sequence of
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 (d,r,())),Prob) );

theorem ThArbPrel: :: FINANCE6:21
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:22
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 (d,r,RV)),Prob)
proof end;

theorem :: FINANCE6:23
for Prob being Probability of Special_SigmaField2
for r being Real st r > 0 holds
for jpi being pricefunction ex G being sequence of st
for d being Nat holds
( Change_Element_to_Func (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:24
for Prob being Probability of Special_SigmaField2
for r being Real st r > 0 holds
for jpi being pricefunction
for G being sequence of st ( for d being Nat holds
( Change_Element_to_Func (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 (s,r,())),Prob) ) )
proof end;