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


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

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

theorem :: FINANCE1:1
for k being Real holds REAL \ [.k,+infty.[ = ].-infty,k.[
proof end;

theorem Th2: :: FINANCE1:2
for k being Real holds REAL \ ].-infty,k.[ = [.k,+infty.[
proof end;

definition
let a, b be Real;
func half_open_sets (a,b) -> SetSequence of REAL means :Def1: :: FINANCE1:def 1
( it . 0 = halfline_fin (a,(b + 1)) & ( for n being 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 Nat holds b1 . (n + 1) = halfline_fin (a,(b + (1 / (n + 1)))) ) )
proof end;
uniqueness
for b1, b2 being SetSequence of REAL st b1 . 0 = halfline_fin (a,(b + 1)) & ( for n being Nat holds b1 . (n + 1) = halfline_fin (a,(b + (1 / (n + 1)))) ) & b2 . 0 = halfline_fin (a,(b + 1)) & ( for n being Nat holds b2 . (n + 1) = halfline_fin (a,(b + (1 / (n + 1)))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines half_open_sets FINANCE1:def 1 :
for a, b being Real
for b3 being SetSequence of REAL holds
( b3 = half_open_sets (a,b) iff ( b3 . 0 = halfline_fin (a,(b + 1)) & ( for n being 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 ) )
proof end;
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
proof end;
end;

definition
let d be Nat;
let phi, jpi be Real_Sequence;
func BuyPortfolioExt (phi,jpi,d) -> Real equals :: FINANCE1:def 3
(Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . d;
coherence
(Partial_Sums (ElementsOfBuyPortfolio (phi,jpi))) . d is Real
;
func BuyPortfolio (phi,jpi,d) -> Real equals :: FINANCE1:def 4
(Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . (d - 1);
coherence
(Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . (d - 1) is 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 of Omega,Omega2;
attr X is Sigma,Sigma2 -random_variable-like means :: FINANCE1:def 5
for x being set st x in Sigma2 holds
X " x in Sigma;
end;

:: deftheorem defines -random_variable-like FINANCE1:def 5 :
for Omega, Omega2 being set
for Sigma being SigmaField of Omega
for Sigma2 being SigmaField of Omega2
for X being Function of Omega,Omega2 holds
( X is Sigma,Sigma2 -random_variable-like iff for x being set st x in Sigma2 holds
X " x in Sigma );

Lm1: for Omega, Omega2 being non empty set
for F being Function of Omega,Omega2
for y being non empty set holds { z where z is Element of Omega : F . z is Element of y } = F " y

proof end;

LemmaExample: for Omega, Omega2 being non empty set
for F being SigmaField of Omega
for F2 being SigmaField of Omega2
for f being Function of Omega,Omega2 st f = Omega --> the Element of Omega2 holds
f is F,F2 -random_variable-like

proof end;

registration
let Omega1, Omega2 be non empty set ;
let S1 be SigmaField of Omega1;
let S2 be SigmaField of Omega2;
cluster V1() V4(Omega1) V5(Omega2) non empty Function-like V28(Omega1) V32(Omega1,Omega2) S1,S2 -random_variable-like for Element of Trivial-SigmaField K17(Omega1,Omega2);
existence
ex b1 being Function of Omega1,Omega2 st b1 is S1,S2 -random_variable-like
proof end;
end;

definition
let Omega, Omega2 be non empty set ;
let F be SigmaField of Omega;
let F2 be SigmaField of Omega2;
mode random_variable of F,F2 is F,F2 -random_variable-like Function of Omega,Omega2;
end;

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
{ M where M is Function of Omega,Omega2 : M is F,F2 -random_variable-like } ;
coherence
{ M where M is Function of Omega,Omega2 : M is F,F2 -random_variable-like } 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) = { M where M is Function of Omega,Omega2 : M is F,F2 -random_variable-like } ;

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

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) -> functional ;
coherence
set_of_random_variables_on (F,F2) is functional
proof end;
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 A1: 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
proof end;
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
proof end;
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
proof end;
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 A1: X = set_of_random_variables_on (F,F2) ;
let G be sequence of 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
proof end;
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 sequence of 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 sequence of 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)
proof end;
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
proof end;
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 sequence of 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 sequence of X;
let w be Element of Omega;
func PortfolioValueFutExt (d,phi,F,G,w) -> 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 Real
;
func PortfolioValueFut (d,phi,F,G,w) -> 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 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 sequence of 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 sequence of 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
proof end;
end;

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

theorem Th4: :: FINANCE1:4
for k1, k2 being Real holds [.k2,k1.[ is Element of Borel_Sets
proof end;

theorem Th5: :: FINANCE1:5
for a, b being Real holds Intersection (half_open_sets (a,b)) is Element of Borel_Sets
proof end;

theorem Th6: :: FINANCE1:6
for a, b being Real holds Intersection (half_open_sets (a,b)) = [.a,b.]
proof end;

theorem :: FINANCE1:7
for a, b being Real
for n being Nat holds (Partial_Intersection (half_open_sets (a,b))) . n is Element of Borel_Sets
proof end;

theorem Th8: :: FINANCE1:8
for k1, k2 being Real holds [.k2,k1.] is Element of Borel_Sets
proof end;

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 Sigma, Borel_Sets -random_variable-like holds
( ( for k being Real holds
( { w where w is Element of Omega : X . w >= k } is Element of Sigma & { w where w is Element of Omega : X . w < k } is Element of Sigma ) ) & ( for k1, k2 being Real st k1 < k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma ) & ( for k1, k2 being Real st k1 <= k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma ) & ( for r being Real holds less_dom (X,r) = { w where w is Element of Omega : X . w < r } ) & ( for r being Real holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } ) & ( for r being Real holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r } ) & ( for r being Real holds eq_dom (X,r) is Element of Sigma ) )
proof end;

theorem :: FINANCE1:10
for Omega being non empty set
for Sigma being SigmaField of Omega
for s being Real
for f being Function of Omega,REAL st f = Omega --> s holds
f is Sigma, Borel_Sets -random_variable-like
proof end;

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

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
for phi being Real_Sequence
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
for w being Element of Omega holds PortfolioValueFutExt (d,phi,F,G,w) = ((1 + r) * (phi . 0)) + (PortfolioValueFut (d,phi,F,G,w))
proof end;

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 st r > - 1 holds
for phi being Real_Sequence
for jpi being pricefunction
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
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)))
proof end;

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 st r > - 1 holds
for phi being Real_Sequence
for jpi being pricefunction
for G being sequence of (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 (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)) } & { 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)) } )
proof end;

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 Sigma, Borel_Sets -random_variable-like holds
( f is [#] Sigma -measurable & f is Real-Valued-Random-Variable of Sigma )
proof end;

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

theorem :: FINANCE1:17
for Omega, Omega2 being non empty set
for F being SigmaField of Omega
for F2 being SigmaField of Omega2 holds Omega --> the Element of Omega2 is random_variable of F,F2 by LemmaExample;