begin
theorem
theorem AJF0:
definition
let a,
b be
real number ;
func half_open_sets (
a,
b)
-> SetSequence of
REAL means :
Def3:
(
it . 0 = halfline_fin (
a,
(b + 1)) & ( for
n being
Element of
NAT holds
it . (n + 1) = halfline_fin (
a,
(b + (1 / (n + 1)))) ) );
existence
ex b1 being SetSequence of REAL st
( b1 . 0 = halfline_fin (a,(b + 1)) & ( for n being Element of NAT holds b1 . (n + 1) = halfline_fin (a,(b + (1 / (n + 1)))) ) )
uniqueness
for b1, b2 being SetSequence of REAL st b1 . 0 = halfline_fin (a,(b + 1)) & ( for n being Element of NAT holds b1 . (n + 1) = halfline_fin (a,(b + (1 / (n + 1)))) ) & b2 . 0 = halfline_fin (a,(b + 1)) & ( for n being Element of NAT holds b2 . (n + 1) = halfline_fin (a,(b + (1 / (n + 1)))) ) holds
b1 = b2
end;
:: deftheorem Def3 defines half_open_sets FINANCE1:def 1 :
for a, b being real number
for b3 being SetSequence of REAL holds
( b3 = half_open_sets (a,b) iff ( b3 . 0 = halfline_fin (a,(b + 1)) & ( for n being Element of NAT holds b3 . (n + 1) = halfline_fin (a,(b + (1 / (n + 1)))) ) ) );
:: deftheorem Def4 defines pricefunction FINANCE1:def 2 :
for b1 being Real_Sequence holds
( b1 is pricefunction iff ( b1 . 0 = 1 & ( for n being Element of NAT holds b1 . n >= 0 ) ) );
:: deftheorem defines BuyPortfolioExt FINANCE1:def 3 :
for d being natural number
for phi, jpi being Real_Sequence holds BuyPortfolioExt (phi,jpi,d) = (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . d;
:: deftheorem defines BuyPortfolio FINANCE1:def 4 :
for d being natural number
for phi, jpi being Real_Sequence holds BuyPortfolio (phi,jpi,d) = (Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . (d - 1);
:: deftheorem Def8 defines is_random_variable_on FINANCE1:def 5 :
for Omega, Omega2 being set
for Sigma being SigmaField of Omega
for Sigma2 being SigmaField of Omega2
for X being Function holds
( X is_random_variable_on Sigma,Sigma2 iff for x being Element of Sigma2 holds { y where y is Element of Omega : X . y is Element of x } is Element of Sigma );
:: deftheorem defines set_of_random_variables_on FINANCE1:def 6 :
for Omega, Omega2 being set
for F being SigmaField of Omega
for F2 being SigmaField of Omega2 holds set_of_random_variables_on (F,F2) = { f where f is Function of Omega,Omega2 : f is_random_variable_on F,F2 } ;
:: deftheorem Def10 defines Change_Element_to_Func FINANCE1:def 7 :
for Omega, Omega2 being non empty set
for F being SigmaField of Omega
for F2 being SigmaField of Omega2
for X being set st X = set_of_random_variables_on (F,F2) holds
for k being Element of X holds Change_Element_to_Func (F,F2,k) = k;
definition
let Omega be non
empty set ;
let F be
SigmaField of
Omega;
let X be non
empty set ;
let k be
Element of
X;
func ElementsOfPortfolioValueProb_fut (
F,
k)
-> Function of
Omega,
REAL means :
Def11:
for
w being
Element of
Omega holds
it . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w;
existence
ex b1 being Function of Omega,REAL st
for w being Element of Omega holds b1 . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w
uniqueness
for b1, b2 being Function of Omega,REAL st ( for w being Element of Omega holds b1 . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w ) & ( for w being Element of Omega holds b2 . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w ) holds
b1 = b2
end;
:: deftheorem Def11 defines ElementsOfPortfolioValueProb_fut FINANCE1:def 8 :
for Omega being non empty set
for F being SigmaField of Omega
for X being non empty set
for k being Element of X
for b5 being Function of Omega,REAL holds
( b5 = ElementsOfPortfolioValueProb_fut (F,k) iff for w being Element of Omega holds b5 . w = (Change_Element_to_Func (F,Borel_Sets,k)) . w );
:: deftheorem Def13 defines Element_Of FINANCE1:def 9 :
for p being Nat
for Omega, Omega2 being non empty set
for F being SigmaField of Omega
for F2 being SigmaField of Omega2
for X being set st X = set_of_random_variables_on (F,F2) holds
for G being Function of NAT,X holds Element_Of (F,F2,G,p) = G . p;
definition
let r be
real number ;
let Omega be non
empty set ;
let F be
SigmaField of
Omega;
let X be non
empty set ;
let w be
Element of
Omega;
let G be
Function of
NAT,
X;
let phi be
Real_Sequence;
func ElementsOfPortfolioValue_fut (
r,
phi,
F,
w,
G)
-> Real_Sequence means :
Def14:
for
n being
Element of
NAT holds
it . n = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n);
existence
ex b1 being Real_Sequence st
for n being Element of NAT holds b1 . n = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n)
uniqueness
for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) ) & ( for n being Element of NAT holds b2 . n = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) ) holds
b1 = b2
end;
:: deftheorem Def14 defines ElementsOfPortfolioValue_fut FINANCE1:def 10 :
for r being real number
for Omega being non empty set
for F being SigmaField of Omega
for X being non empty set
for w being Element of Omega
for G being Function of NAT,X
for phi, b8 being Real_Sequence holds
( b8 = ElementsOfPortfolioValue_fut (r,phi,F,w,G) iff for n being Element of NAT holds b8 . n = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) );
definition
let r be
real number ;
let d be
natural number ;
let phi be
Real_Sequence;
let Omega be non
empty set ;
let F be
SigmaField of
Omega;
let X be non
empty set ;
let G be
Function of
NAT,
X;
let w be
Element of
Omega;
func PortfolioValueFutExt (
r,
d,
phi,
F,
G,
w)
-> Element of
REAL equals
(Partial_Sums (ElementsOfPortfolioValue_fut (r,phi,F,w,G))) . d;
coherence
(Partial_Sums (ElementsOfPortfolioValue_fut (r,phi,F,w,G))) . d is Element of REAL
;
func PortfolioValueFut (
r,
d,
phi,
F,
G,
w)
-> Element of
REAL equals
(Partial_Sums ((ElementsOfPortfolioValue_fut (r,phi,F,w,G)) ^\ 1)) . (d - 1);
coherence
(Partial_Sums ((ElementsOfPortfolioValue_fut (r,phi,F,w,G)) ^\ 1)) . (d - 1) is Element of REAL
;
end;
:: deftheorem defines PortfolioValueFutExt FINANCE1:def 11 :
for r being real number
for d being natural number
for phi being Real_Sequence
for Omega being non empty set
for F being SigmaField of Omega
for X being non empty set
for G being Function of NAT,X
for w being Element of Omega holds PortfolioValueFutExt (r,d,phi,F,G,w) = (Partial_Sums (ElementsOfPortfolioValue_fut (r,phi,F,w,G))) . d;
:: deftheorem defines PortfolioValueFut FINANCE1:def 12 :
for r being real number
for d being natural number
for phi being Real_Sequence
for Omega being non empty set
for F being SigmaField of Omega
for X being non empty set
for G being Function of NAT,X
for w being Element of Omega holds PortfolioValueFut (r,d,phi,F,G,w) = (Partial_Sums ((ElementsOfPortfolioValue_fut (r,phi,F,w,G)) ^\ 1)) . (d - 1);
theorem BJ1:
theorem BJ2:
theorem BJ4:
theorem SP2:
theorem
theorem Th3:
theorem Th4:
theorem
theorem Th6:
theorem Th7:
for
Omega being non
empty set for
F being
SigmaField of
Omega for
d being
natural number st
d > 0 holds
for
r being
real number for
phi being
Real_Sequence for
G being
Function of
NAT,
(set_of_random_variables_on (F,Borel_Sets)) st
Element_Of (
F,
Borel_Sets,
G,
0)
= Omega --> (1 + r) holds
for
w being
Element of
Omega holds
PortfolioValueFutExt (
r,
d,
phi,
F,
G,
w)
= ((1 + r) * (phi . 0)) + (PortfolioValueFut (r,d,phi,F,G,w))
theorem Th8:
for
Omega being non
empty set for
F being
SigmaField of
Omega for
d being
natural number st
d > 0 holds
for
r being
real number st
r > - 1 holds
for
phi being
Real_Sequence for
jpi being
pricefunction for
G being
Function of
NAT,
(set_of_random_variables_on (F,Borel_Sets)) st
Element_Of (
F,
Borel_Sets,
G,
0)
= Omega --> (1 + r) holds
for
w being
Element of
Omega st
BuyPortfolioExt (
phi,
jpi,
d)
<= 0 holds
PortfolioValueFutExt (
r,
d,
phi,
F,
G,
w)
<= (PortfolioValueFut (r,d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d)))
theorem
for
Omega being non
empty set for
F being
SigmaField of
Omega for
d being
natural number st
d > 0 holds
for
r being
real number st
r > - 1 holds
for
phi being
Real_Sequence for
jpi being
pricefunction for
G being
Function of
NAT,
(set_of_random_variables_on (F,Borel_Sets)) st
Element_Of (
F,
Borel_Sets,
G,
0)
= Omega --> (1 + r) &
BuyPortfolioExt (
phi,
jpi,
d)
<= 0 holds
(
{ w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) >= 0 } c= { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d)) } &
{ w where w is Element of Omega : PortfolioValueFutExt (r,d,phi,F,G,w) > 0 } c= { w where w is Element of Omega : PortfolioValueFut (r,d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d)) } )
theorem Th10:
theorem