:: Elementary Introduction to Stochastic Finance in Discrete Time
:: by Peter Jaeger
::
:: Received March 22, 2011
:: Copyright (c) 2011-2012 Association of Mizar Users


begin

notation
let a, r be real number ;
synonym  halfline_fin (a,r) for [.a,r.[;
end;

definition
let a, r be real number ;
:: original:halfline_fin
redefine func halfline_fin (a,r) ->  Subset of REAL;
coherence
 halfline_fin (a,r) is Subset of REAL
proofend;
end;

theorem :: FINANCE1:1
for k being real number holds REAL \ [.k,+infty.[ = ].-infty,k.[
proofend;

theorem Th2: :: FINANCE1:2
for k being real number holds REAL \ ].-infty,k.[ = [.k,+infty.[
proofend;

definition
let a, b be real number ;
func half_open_sets (a,b) ->  SetSequence of REAL means :Def1: :: FINANCE1:def 1
( 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)))) ) )
proofend;
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
proofend;
end;

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

definition
mode pricefunction  ->  Real_Sequence means :Def2: :: FINANCE1:def 2
( it . 0 = 1 & ( for n being Element of NAT holds it . n >= 0 ) );
existence
 ex b1 being Real_Sequence st
( b1 . 0 = 1 & ( for n being Element of NAT holds b1 . n >= 0 ) )
proofend;
end;

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

notation
let phi, jpi be Real_Sequence;
synonym  ElementsOfBuyPortfolio (phi,jpi) for phi (#) jpi;
end;

definition
let phi, jpi be Real_Sequence;
:: original:ElementsOfBuyPortfolio
redefine func ElementsOfBuyPortfolio (phi,jpi) ->  Real_Sequence;
coherence
 ElementsOfBuyPortfolio (phi,jpi) is Real_Sequence
proofend;
end;

definition
let d be Nat;
let phi, jpi be Real_Sequence;
func BuyPortfolioExt (phi,jpi,d) ->  Element of REAL  equals :: FINANCE1:def 3
(Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . d;
coherence
 (Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . d is Element of REAL ;
func BuyPortfolio (phi,jpi,d) ->  Element of REAL  equals :: FINANCE1:def 4
(Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . (d - 1);
coherence
 (Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . (d - 1) is Element of REAL ;
end;

:: deftheorem  defines BuyPortfolioExt FINANCE1:def_3_:_
 for d being Nat
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 Nat
for phi, jpi being Real_Sequence holds BuyPortfolio (phi,jpi,d) = (Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . (d - 1);

definition
let Omega, Omega2 be set ;
let Sigma be SigmaField of Omega;
let Sigma2 be SigmaField of Omega2;
let X be Function;
predX is_random_variable_on Sigma,Sigma2 means :Def5: :: FINANCE1:def 5
 for x being Element of Sigma2 holds  {  y where y is Element of Omega : X . y is Element of x  }  is Element of Sigma;
end;

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

definition
let Omega, Omega2 be set ;
let F be SigmaField of Omega;
let F2 be SigmaField of Omega2;
func set_of_random_variables_on (F,F2) ->  set  equals :: FINANCE1:def 6
 {  f where f is Function of Omega,Omega2 : f is_random_variable_on F,F2  }  ;
coherence
  {  f where f is Function of Omega,Omega2 : f is_random_variable_on F,F2  }  is set ;
end;

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

registration
let Omega, Omega2 be non empty set ;
let F be SigmaField of Omega;
let F2 be SigmaField of Omega2;
cluster set_of_random_variables_on (F,F2) ->  non empty ;
coherence
 not set_of_random_variables_on (F,F2) is empty
proofend;
end;

definition
let Omega, Omega2 be non empty set ;
let F be SigmaField of Omega;
let F2 be SigmaField of Omega2;
let X be set ;
assume T1: X = set_of_random_variables_on (F,F2) ;
let k be Element of X;
func Change_Element_to_Func (F,F2,k) ->  Function of Omega,Omega2 equals :Def7: :: FINANCE1:def 7
k;
coherence
 k is Function of Omega,Omega2
proofend;
end;

:: deftheorem Def7 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 :Def8: :: FINANCE1:def 8
 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
proofend;
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
proofend;
end;

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

definition
let p be Nat;
let Omega, Omega2 be non empty set ;
let F be SigmaField of Omega;
let F2 be SigmaField of Omega2;
let X be set ;
assume T1: X = set_of_random_variables_on (F,F2) ;
let G be Function of NAT,X;
func Element_Of (F,F2,G,p) ->  Function of Omega,Omega2 equals :Def9: :: FINANCE1:def 9
G . p;
coherence
 G . p is Function of Omega,Omega2
proofend;
end;

:: deftheorem Def9 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 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 (phi,F,w,G) ->  Real_Sequence means :Def10: :: FINANCE1:def 10
 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)
proofend;
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
proofend;
end;

:: deftheorem Def10 defines ElementsOfPortfolioValue_fut FINANCE1:def_10_:_
 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, b7 being Real_Sequence holds
( b7 = ElementsOfPortfolioValue_fut (phi,F,w,G) iff for n being Element of NAT holds b7 . n = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) );

definition
let d be Nat;
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 (d,phi,F,G,w) ->  Element of REAL  equals :: FINANCE1:def 11
(Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . d;
coherence
 (Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . d is Element of REAL ;
func PortfolioValueFut (d,phi,F,G,w) ->  Element of REAL  equals :: FINANCE1:def 12
(Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . (d - 1);
coherence
 (Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . (d - 1) is Element of REAL ;
end;

:: deftheorem  defines PortfolioValueFutExt FINANCE1:def_11_:_
 for d being Nat
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 (d,phi,F,G,w) = (Partial_Sums (ElementsOfPortfolioValue_fut (phi,F,w,G))) . d;

:: deftheorem  defines PortfolioValueFut FINANCE1:def_12_:_
 for d being Nat
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 (d,phi,F,G,w) = (Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . (d - 1);

registration
cluster non empty for Element of Borel_Sets ;
existence
 not for b1 being Element of Borel_Sets holds b1 is empty
proofend;
end;

theorem Th3: :: FINANCE1:3
for k being real number holds
( [.k,+infty.[ is Element of Borel_Sets & ].-infty,k.[ is Element of Borel_Sets )
proofend;

theorem Th4: :: FINANCE1:4
for k1, k2 being real number holds [.k2,k1.[ is Element of Borel_Sets
proofend;

theorem Th5: :: FINANCE1:5
for a, b being real number holds Intersection (half_open_sets (a,b)) is Element of Borel_Sets
proofend;

theorem Th6: :: FINANCE1:6
for a, b being real number holds Intersection (half_open_sets (a,b)) = [.a,b.]
proofend;

theorem :: FINANCE1:7
for a, b being real number
for n being Nat holds (Partial_Intersection (half_open_sets (a,b))) . n is Element of Borel_Sets
proofend;

theorem Th8: :: FINANCE1:8
for k1, k2 being real number holds [.k2,k1.] is Element of Borel_Sets
proofend;

theorem Th9: :: FINANCE1:9
for Omega being non empty set
for Sigma being SigmaField of Omega
for X being Function of Omega,REAL st X is_random_variable_on Sigma, Borel_Sets holds
( ( for k being real number holds
(  {  w where w is Element of Omega : X . w >= k  }  is Element of Sigma &amp;  {  w where w is Element of Omega : X . w < k  }  is Element of Sigma ) ) &amp; ( for k1, k2 being real number st k1 < k2 holds
{  w where w is Element of Omega : ( k1 <= X . w &amp; X . w < k2 )  }  is Element of Sigma ) &amp; ( for k1, k2 being real number st k1 <= k2 holds
{  w where w is Element of Omega : ( k1 <= X . w &amp; X . w <= k2 )  }  is Element of Sigma ) &amp; ( for r being real number holds less_dom (X,r) =  {  w where w is Element of Omega : X . w < r  }  ) &amp; ( for r being real number holds great_eq_dom (X,r) =  {  w where w is Element of Omega : X . w >= r  }  ) &amp; ( for r being real number holds eq_dom (X,r) =  {  w where w is Element of Omega : X . w = r  }  ) &amp; ( for r being real number holds eq_dom (X,r) is Element of Sigma ) )
proofend;

theorem :: FINANCE1:10
for Omega being non empty set
for Sigma being SigmaField of Omega
for s being real number holds Omega --> s is_random_variable_on Sigma, Borel_Sets
proofend;

theorem Th11: :: FINANCE1:11
for phi being Real_Sequence
for jpi being pricefunction
for d being Nat st d > 0 holds
BuyPortfolioExt (phi,jpi,d) = (phi . 0) + (BuyPortfolio (phi,jpi,d))
proofend;

theorem Th12: :: FINANCE1:12
for Omega being non empty set
for F being SigmaField of Omega
for d being Nat 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 (d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (d,phi,F,G,w))
proofend;

theorem Th13: :: FINANCE1:13
for Omega being non empty set
for F being SigmaField of Omega
for d being Nat 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 (d,phi,F,G,w) <= (PortfolioValueFut (d,phi,F,G,w)) - ((1 + r) * (BuyPortfolio (phi,jpi,d)))
proofend;

theorem :: FINANCE1:14
for Omega being non empty set
for F being SigmaField of Omega
for d being Nat 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) &amp; BuyPortfolioExt (phi,jpi,d) <= 0 holds
(  {  w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) >= 0  }  c=  {  w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) >= (1 + r) * (BuyPortfolio (phi,jpi,d))  }  &amp;  {  w where w is Element of Omega : PortfolioValueFutExt (d,phi,F,G,w) > 0  }  c=  {  w where w is Element of Omega : PortfolioValueFut (d,phi,F,G,w) > (1 + r) * (BuyPortfolio (phi,jpi,d))  }  )
proofend;

theorem Th15: :: FINANCE1:15
for Omega being non empty set
for Sigma being SigmaField of Omega
for f being Function of Omega,REAL st f is_random_variable_on Sigma, Borel_Sets holds
( f is_measurable_on [#] Sigma &amp; f is Real-Valued-Random-Variable of Sigma )
proofend;

theorem :: FINANCE1:16
for Omega being non empty set
for Sigma being SigmaField of Omega holds set_of_random_variables_on (Sigma,Borel_Sets) c= Real-Valued-Random-Variables-Set Sigma
proofend;