FINANCE1: Elementary Introduction to Stochastic Finance in Discrete Time

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

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines half_open_sets FINANCE1:def 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

proof end;

end;

:: deftheorem Def2 defines pricefunction FINANCE1:def 2 :

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

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 ;

func BuyPortfolio (phi,jpi,d) -> Real equals :: FINANCE1:def 4
(Partial_Sums ((ElementsOfBuyPortfolio (phi,jpi)) ^\ 1)) . (d - 1);

coherence ;

end;

:: deftheorem defines BuyPortfolioExt FINANCE1:def 3 :

:: deftheorem defines BuyPortfolio FINANCE1:def 4 :

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 :

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

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 ;

end;

:: deftheorem defines set_of_random_variables_on FINANCE1:def 6 :

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

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

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

proof end;

end;

:: deftheorem Def7 defines Change_Element_to_Func FINANCE1:def 7 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines ElementsOfPortfolioValueProb_fut FINANCE1:def 8 :

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

proof end;

end;

:: deftheorem Def9 defines Element_Of FINANCE1:def 9 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines ElementsOfPortfolioValue_fut FINANCE1:def 10 :

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 ;

func PortfolioValueFut (d,phi,F,G,w) -> Real equals :: FINANCE1:def 12
(Partial_Sums ((ElementsOfPortfolioValue_fut (phi,F,w,G)) ^\ 1)) . (d - 1);

coherence ;

end;

:: deftheorem defines PortfolioValueFutExt FINANCE1:def 11 :

:: deftheorem defines PortfolioValueFut FINANCE1:def 12 :

registration

cluster non empty for Element of Borel_Sets ;

existence

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

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;