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

H0: {0,1} c= REAL

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 b₁ 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 b₁ 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 b₁ 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

].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 Real holds chi (((RV - (Omega --> K)) " [.0,+infty.[),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)) " [.0,+infty.[),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 b₁ 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 b₁ being Function of Omega,REAL st
for w being Element of Omega holds
( ( ((Omega --> K) - RV) . w >= 0 implies b₁ . w = ((Omega --> K) - RV) . w ) & ( ((Omega --> K) - RV) . w < 0 implies b₁ . w = 0 ) )

proof end;

uniqueness
for b₁, b₂ being Function of Omega,REAL st ( for w being Element of Omega holds
( ( ((Omega --> K) - RV) . w >= 0 implies b₁ . w = ((Omega --> K) - RV) . w ) & ( ((Omega --> K) - RV) . w < 0 implies b₁ . w = 0 ) ) ) & ( for w being Element of Omega holds
( ( ((Omega --> K) - RV) . w >= 0 implies b₂ . w = ((Omega --> K) - RV) . w ) & ( ((Omega --> K) - RV) . w < 0 implies b₂ . w = 0 ) ) ) holds
b₁ = b₂

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 b₅ being Function of Omega,REAL holds
( b₅ = Put-Option (RV,K) iff for w being Element of Omega holds
( ( ((Omega --> K) - RV) . w >= 0 implies b₅ . w = ((Omega --> K) - RV) . w ) & ( ((Omega --> K) - RV) . w < 0 implies b₅ . 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) " [.0,+infty.[),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) " [.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;

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;

cluster set_of_constant_RV F -> non empty ;

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 (set_of_chi_RV F);
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 (set_of_chi_RV F)
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 (set_of_constant_RV F);
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 (set_of_constant_RV F)
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 (set_of_constant_RV F);
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 b₁ being Function of NAT,REAL st
for n being Nat holds b₁ . n = (Conv_constant_RV (ConstFuncs,n)) . w

proof end;

uniqueness
for b₁, b₂ being Function of NAT,REAL st ( for n being Nat holds b₁ . n = (Conv_constant_RV (ConstFuncs,n)) . w ) & ( for n being Nat holds b₂ . n = (Conv_constant_RV (ConstFuncs,n)) . w ) holds
b₁ = b₂

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 (set_of_constant_RV F)
for w being Element of Omega
for b₅ being Function of NAT,REAL holds
( b₅ = Conv2_constant_RV (ConstFuncs,w) iff for n being Nat holds b₅ . 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 (set_of_chi_RV F);
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 b₁ being Function of NAT,REAL st
for n being Nat holds b₁ . n = (Conv_chi_RV (ChiFuncs,n)) . w

proof end;

uniqueness
for b₁, b₂ being Function of NAT,REAL st ( for n being Nat holds b₁ . n = (Conv_chi_RV (ChiFuncs,n)) . w ) & ( for n being Nat holds b₂ . n = (Conv_chi_RV (ChiFuncs,n)) . w ) holds
b₁ = b₂

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 (set_of_chi_RV F)
for w being Element of Omega
for b₅ being Function of NAT,REAL holds
( b₅ = Conv2_chi_RV (ChiFuncs,w) iff for n being Nat holds b₅ . 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 (set_of_chi_RV F);
let ConstFuncs be sequence of (set_of_constant_RV F);
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 b₁ being Function of Omega,REAL st
for w being Element of Omega holds b₁ . w = (Partial_Sums ((Conv2_constant_RV (ConstFuncs,w)) (#) (Conv2_chi_RV (ChiFuncs,w)))) . n

proof end;

uniqueness
for b₁, b₂ being Function of Omega,REAL st ( for w being Element of Omega holds b₁ . w = (Partial_Sums ((Conv2_constant_RV (ConstFuncs,w)) (#) (Conv2_chi_RV (ChiFuncs,w)))) . n ) & ( for w being Element of Omega holds b₂ . w = (Partial_Sums ((Conv2_constant_RV (ConstFuncs,w)) (#) (Conv2_chi_RV (ChiFuncs,w)))) . n ) holds
b₁ = b₂

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 (set_of_chi_RV F)
for ConstFuncs being sequence of (set_of_constant_RV F)
for n being Nat
for b₆ being Function of Omega,REAL holds
( b₆ = simple_RV_help (ChiFuncs,ConstFuncs,n) iff for w being Element of Omega holds b₆ . 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 (set_of_chi_RV F);
let ConstFuncs be sequence of (set_of_constant_RV F);
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 b₁ being random_variable of F, Borel_Sets st
for w being Element of Omega holds b₁ . 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 (set_of_chi_RV F)
for ConstFuncs being sequence of (set_of_constant_RV F)
for n being Nat
for b₆ being random_variable of F, Borel_Sets holds
( b₆ is simple_RV of ConstFuncs,ChiFuncs,n iff for w being Element of Omega holds b₆ . 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 (set_of_random_variables_on (F,Borel_Sets));

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 (set_of_random_variables_on (F,Borel_Sets)) 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 (set_of_random_variables_on (F,Borel_Sets))
for n being Nat holds (RVPortfolioValueFutExt (phi,F,G,n)) " [.0,+infty.[ 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 (set_of_random_variables_on (F,Borel_Sets))
for n being Nat holds (RVPortfolioValueFutExt (phi,F,G,n)) " ].0,+infty.[ 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 (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 16
(RVPortfolioValueFutExt (phi,F,G,n)) " [.0,+infty.[;

correctness
coherence
(RVPortfolioValueFutExt (phi,F,G,n)) " [.0,+infty.[ 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)) " ].0,+infty.[;

correctness
coherence
(RVPortfolioValueFutExt (phi,F,G,n)) " ].0,+infty.[ 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 (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 17 :
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 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 (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 19
{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 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 b₁ 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 b₁ 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 (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:13

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

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

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 b₁ 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 (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 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 (set_of_random_variables_on (F,Borel_Sets));
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,(Change_Element_to_Func (G,d)))),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 (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 (d,r,(Change_Element_to_Func (G,d)))),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 (set_of_random_variables_on (Special_SigmaField2,Borel_Sets)) 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 (set_of_random_variables_on (Special_SigmaField2,Borel_Sets)) 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,(Change_Element_to_Func (G,s)))),Prob) ) )

proof end;