:: by Peter Jaeger

::

:: Received March 27, 2018

:: Copyright (c) 2018-2019 Association of Mizar Users

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

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

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

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;

ex b_{1} being Function of Omega,REAL st b_{1} is F, Borel_Sets -random_variable-like

end;
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 b

proof end;

theorem ChiRandom: :: FINANCE6:5

for Omega being non empty set

for F being SigmaField of Omega holds chi (Omega,Omega) is b_{2}, Borel_Sets -random_variable-like Function of Omega,REAL

for F being SigmaField of Omega holds chi (Omega,Omega) is b

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

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 ;

end;
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;

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;

ex b_{1} being Function of Omega,REAL st

for w being Element of Omega holds

( ( ((Omega --> K) - RV) . w >= 0 implies b_{1} . w = ((Omega --> K) - RV) . w ) & ( ((Omega --> K) - RV) . w < 0 implies b_{1} . w = 0 ) )

for b_{1}, b_{2} being Function of Omega,REAL st ( for w being Element of Omega holds

( ( ((Omega --> K) - RV) . w >= 0 implies b_{1} . w = ((Omega --> K) - RV) . w ) & ( ((Omega --> K) - RV) . w < 0 implies b_{1} . w = 0 ) ) ) & ( for w being Element of Omega holds

( ( ((Omega --> K) - RV) . w >= 0 implies b_{2} . w = ((Omega --> K) - RV) . w ) & ( ((Omega --> K) - RV) . w < 0 implies b_{2} . w = 0 ) ) ) holds

b_{1} = b_{2}

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

ex b

for w being Element of Omega holds

( ( ((Omega --> K) - RV) . w >= 0 implies b

proof end;

uniqueness for b

( ( ((Omega --> K) - RV) . w >= 0 implies b

( ( ((Omega --> K) - RV) . w >= 0 implies b

b

proof 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 b_{5} being Function of Omega,REAL holds

( b_{5} = Put-Option (RV,K) iff for w being Element of Omega holds

( ( ((Omega --> K) - RV) . w >= 0 implies b_{5} . w = ((Omega --> K) - RV) . w ) & ( ((Omega --> K) - RV) . w < 0 implies b_{5} . w = 0 ) ) );

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

( b

( ( ((Omega --> K) - RV) . w >= 0 implies b

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)

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 ;

end;
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;

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;

(Put-Option (RV,K)) + (Call-Option (RV,K)) is random_variable of F, Borel_Sets by FINANCE2:23;

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

(Put-Option (RV,K)) + (Call-Option (RV,K)) is random_variable of F, Borel_Sets by FINANCE2:23;

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

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).|

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;

{ f where f is Function of Omega,REAL : ( f is random_variable of F, Borel_Sets & f is constant ) } is set ;

{ (chi (A,Omega)) where A is Element of F : chi (A,Omega) is random_variable of F, Borel_Sets } is set ;

end;
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 ) } ;

{ 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 } ;

{ (chi (A,Omega)) where A is Element of F : chi (A,Omega) is random_variable of F, Borel_Sets } is set ;

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

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 } ;

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 ;

end;
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 ;

for x being object st x in X holds

x is random_variable of F, Borel_Sets ;

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

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;

coherence

not set_of_constant_RV F is empty

not set_of_chi_RV F is empty

end;
let F be SigmaField of Omega;

coherence

not set_of_constant_RV F is empty

proof end;

coherence not set_of_chi_RV F is empty

proof end;

registration

let Omega be non empty set ;

let F be SigmaField of Omega;

coherence

set_of_constant_RV F is F -random-membered

set_of_chi_RV F is F -random-membered

end;
let F be SigmaField of Omega;

coherence

set_of_constant_RV F is F -random-membered

proof end;

coherence set_of_chi_RV F is F -random-membered

proof end;

registration

let Omega be non empty set ;

let F be SigmaField of Omega;

existence

ex b_{1} being set st

( b_{1} is F -random-membered & not b_{1} is empty )

end;
let F be SigmaField of Omega;

existence

ex b

( b

proof 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;

coherence

ChiFuncs . n is random_variable of F, Borel_Sets by RanDef;

end;
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;

coherence

ChiFuncs . n is random_variable of F, Borel_Sets by RanDef;

:: deftheorem defines Conv_RV FINANCE6:def 6 :

for Omega being non empty set

for F being SigmaField of Omega

for D being non empty b_{2} -random-membered set

for ChiFuncs being sequence of D

for n being Nat holds Conv_RV (ChiFuncs,n) = ChiFuncs . n;

for Omega being non empty set

for F being SigmaField of Omega

for D being non empty b

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;

ex b_{1} being Function of NAT,REAL st

for n being Nat holds b_{1} . n = (Conv_RV (ConstFuncs,n)) . w

for b_{1}, b_{2} being Function of NAT,REAL st ( for n being Nat holds b_{1} . n = (Conv_RV (ConstFuncs,n)) . w ) & ( for n being Nat holds b_{2} . n = (Conv_RV (ConstFuncs,n)) . w ) holds

b_{1} = b_{2}

end;
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 for n being Nat holds it . n = (Conv_RV (ConstFuncs,n)) . w;

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof 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 b_{2} -random-membered set

for ConstFuncs being sequence of D

for w being Element of Omega

for b_{6} being Function of NAT,REAL holds

( b_{6} = Conv2_RV (ConstFuncs,w) iff for n being Nat holds b_{6} . n = (Conv_RV (ConstFuncs,n)) . w );

for Omega being non empty set

for F being SigmaField of Omega

for D being non empty b

for ConstFuncs being sequence of D

for w being Element of Omega

for b

( b

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;

ex b_{1} being Function of Omega,REAL st

for w being Element of Omega holds b_{1} . w = (Partial_Sums ((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w)))) . n

for b_{1}, b_{2} being Function of Omega,REAL st ( for w being Element of Omega holds b_{1} . w = (Partial_Sums ((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w)))) . n ) & ( for w being Element of Omega holds b_{2} . w = (Partial_Sums ((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w)))) . n ) holds

b_{1} = b_{2}

end;
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 for w being Element of Omega holds it . w = (Partial_Sums ((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w)))) . n;

ex b

for w being Element of Omega holds b

proof end;

uniqueness for b

b

proof 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 b_{2} -random-membered set

for ChiFuncs being sequence of D1

for ConstFuncs being sequence of D2

for n being Nat

for b_{8} being Function of Omega,REAL holds

( b_{8} = simple_RV_help (ChiFuncs,ConstFuncs,n) iff for w being Element of Omega holds b_{8} . w = (Partial_Sums ((Conv2_RV (ConstFuncs,w)) (#) (Conv2_RV (ChiFuncs,w)))) . n );

for Omega being non empty set

for F being SigmaField of Omega

for D1, D2 being non empty b

for ChiFuncs being sequence of D1

for ConstFuncs being sequence of D2

for n being Nat

for b

( b

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 ;

end;
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;

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

G . q is Real-Valued-Random-Variable of F

end;
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;

G . q is Real-Valued-Random-Variable of F

proof 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;

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;

coherence

(RVPortfolioValueFutExt (phi,F,G,n)) " [.0,+infty.[ is Element of F;

coherence

(RVPortfolioValueFutExt (phi,F,G,n)) " ].0,+infty.[ is Element of F;

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

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

coherence

(RVPortfolioValueFutExt (phi,F,G,n)) " ].0,+infty.[ is Element of F;

proof 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.[;

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.[;

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;

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

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

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

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;

coherence

{1,2,3,4} --> r is Element of set_of_random_variables_on (Special_SigmaField1,Borel_Sets);

end;
func RVfirst r -> Element of set_of_random_variables_on (Special_SigmaField1,Borel_Sets) equals :: FINANCE6:def 13

{1,2,3,4} --> r;

correctness {1,2,3,4} --> r;

coherence

{1,2,3,4} --> r is Element of set_of_random_variables_on (Special_SigmaField1,Borel_Sets);

proof end;

definition

let jpi be pricefunction ;

let r be Real;

let d be Nat;

coherence

RVfirst ((jpi . d) * (1 + r)) is Element of set_of_random_variables_on (Special_SigmaField2,Borel_Sets);

end;
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 RVfirst ((jpi . d) * (1 + r));

coherence

RVfirst ((jpi . d) * (1 + r)) is Element of set_of_random_variables_on (Special_SigmaField2,Borel_Sets);

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

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

( 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

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.[

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.[

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

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.[

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.[

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

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

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;

coherence

RV (#) (1 / (1 + r)) is Real-Valued-Random-Variable of F;

end;
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 RV (#) (1 / (1 + r));

coherence

RV (#) (1 / (1 + r)) is Real-Valued-Random-Variable of F;

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

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;

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

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

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

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 )

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)

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 )

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

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;