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

correctness

coherence

( ( n = 1 implies t is Element of REAL ) & ( not n = 1 implies 0 is Element of REAL ) );

consistency

for b_{1} being Element of REAL holds verum;

by XREAL_0:def 1;

end;
let n be Nat;

correctness

coherence

( ( n = 1 implies t is Element of REAL ) & ( not n = 1 implies 0 is Element of REAL ) );

consistency

for b

by XREAL_0:def 1;

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

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;

correctness

coherence

( ( n = 0 implies 1 is Element of REAL ) & ( not n = 0 implies Conv (n,t) is Element of REAL ) );

consistency

for b_{1} being Element of REAL holds verum;

by NUMBERS:19;

end;
let n be Nat;

correctness

coherence

( ( n = 0 implies 1 is Element of REAL ) & ( not n = 0 implies Conv (n,t) is Element of REAL ) );

consistency

for b

by NUMBERS:19;

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

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;

coherence

( ( n = 0 implies - 1 is Element of REAL ) & ( not n = 0 implies Conv (n,t) is Element of REAL ) );

consistency

for b_{1} being Element of REAL holds verum;

by XREAL_0:def 1;

end;
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 - 1 if n = 0

otherwise Conv (n,t);

coherence

( ( n = 0 implies - 1 is Element of REAL ) & ( not n = 0 implies Conv (n,t) is Element of REAL ) );

consistency

for b

by XREAL_0:def 1;

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

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

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

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 ;

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

definition

let Omega be non empty set ;

let RV be Function of Omega,REAL;

let w be Element of Omega;

coherence

( ( RV . w >= 0 implies RV . w is Element of REAL ) & ( not RV . w >= 0 implies 0 is Element of REAL ) );

consistency

for b_{1} being Element of REAL holds verum;

by NUMBERS:19;

end;
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 RV . w if RV . w >= 0

otherwise 0 ;

coherence

( ( RV . w >= 0 implies RV . w is Element of REAL ) & ( not RV . w >= 0 implies 0 is Element of REAL ) );

consistency

for b

by NUMBERS:19;

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

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;

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 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 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 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_{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 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

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

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)

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;

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

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

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 ;

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

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

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

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

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;

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

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

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

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

end;
let F be SigmaField of Omega;

coherence

not set_of_constant_RV F is empty

proof end;

definition

let Omega be non empty set ;

let F be SigmaField of Omega;

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

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

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

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;

coherence

not set_of_chi_RV F is empty

end;
let F be SigmaField of Omega;

coherence

not set_of_chi_RV F is empty

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

coherence

ChiFuncs . n is random_variable of F, Borel_Sets ;

end;
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 ChiFuncs . n;

coherence

ChiFuncs . n is random_variable of F, Borel_Sets ;

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

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;

ConstFuncs . n is random_variable of F, Borel_Sets

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

ConstFuncs . n is random_variable of F, Borel_Sets

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

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;

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

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

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

b_{1} = b_{2}

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

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

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

( b_{5} = Conv2_constant_RV (ConstFuncs,w) iff for n being Nat holds b_{5} . n = (Conv_constant_RV (ConstFuncs,n)) . w );

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

( b

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;

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

for n being Nat holds b_{1} . n = (Conv_chi_RV (ChiFuncs,n)) . w

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

b_{1} = b_{2}

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

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

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

( b_{5} = Conv2_chi_RV (ChiFuncs,w) iff for n being Nat holds b_{5} . n = (Conv_chi_RV (ChiFuncs,n)) . w );

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

( b

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;

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

for w being Element of Omega holds b_{1} . w = (Partial_Sums ((Conv2_constant_RV (ConstFuncs,w)) (#) (Conv2_chi_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_constant_RV (ConstFuncs,w)) (#) (Conv2_chi_RV (ChiFuncs,w)))) . n ) & ( for w being Element of Omega holds b_{2} . w = (Partial_Sums ((Conv2_constant_RV (ConstFuncs,w)) (#) (Conv2_chi_RV (ChiFuncs,w)))) . n ) holds

b_{1} = b_{2}

end;
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 for w being Element of Omega holds it . w = (Partial_Sums ((Conv2_constant_RV (ConstFuncs,w)) (#) (Conv2_chi_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 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_{6} being Function of Omega,REAL holds

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

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

( b

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;

ex b_{1} being random_variable of F, Borel_Sets st

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

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

ex b

for w being Element of Omega holds b

proof 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_{6} being random_variable of F, Borel_Sets holds

( b_{6} is simple_RV of ConstFuncs,ChiFuncs,n iff for w being Element of Omega holds b_{6} . w = (simple_RV_help (ChiFuncs,ConstFuncs,n)) . w );

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

( b

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

coherence

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 15

G . q;

correctness G . q;

coherence

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

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

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

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

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;

coherence

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

by JA1;

coherence

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

by JA2;

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 16

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

by JA1;

func ArbitrageElSigma2 (phi,Omega,F,G,n) -> Element of F equals :: FINANCE6:def 17

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

by JA2;

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

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

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

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

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 19

{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

{1,2,3,4} --> ((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 20

{1,2,3,4} --> ((jpi . d) * (1 + r));

correctness {1,2,3,4} --> ((jpi . d) * (1 + r));

coherence

{1,2,3,4} --> ((jpi . d) * (1 + r)) is Element of set_of_random_variables_on (Special_SigmaField2,Borel_Sets);

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

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;

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_{1} being Element of set_of_random_variables_on (Special_SigmaField1,Borel_Sets) holds verum;

;

end;
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 RVfirst 5 if n = 1

otherwise RVfirst 0;

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

;

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

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;

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_{1} being Element of set_of_random_variables_on (Special_SigmaField1,Borel_Sets) holds verum;

;

end;
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 RVfirst 1 if n = 0

otherwise RVswitchsecond n;

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

;

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

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

( 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

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

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

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

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

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

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

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;

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_{1} being Element of REAL holds verum;

by XREAL_0:def 1;

end;
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 - (BuyPortfolio (phi,jpi,d)) if n = 0

otherwise phi . n;

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

by XREAL_0:def 1;

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

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

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;

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

coherence

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

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

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;

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

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

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

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 )

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)

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 )

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

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;