:: Introduction to Stopping Time in Stochastic Finance Theory: Part {II}
:: by Peter Jaeger
::
:: Received November 29, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies SETFAM_1, XCMPLX_0, CARD_3, ZFMISC_1, EQREL_1, NUMBERS, XBOOLE_0,
PROB_1, SUBSET_1, RELAT_1, FUNCT_1, TARSKI, ARYTM_3, XXREAL_0, CARD_1,
RPR_1, FINANCE3, FUNCOP_1, FINANCE4, FINANCE5, RANDOM_3, FINANCE1,
XXREAL_1, NAT_1, MEMBERED, ARYTM_1, REAL_1, VALUED_0, PARTFUN1, INT_1,
FUNCT_7, ORDINAL1;
notations TARSKI, XBOOLE_0, SETFAM_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0,
XXREAL_3, XREAL_0, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, PROB_1,
FUNCOP_1, MEMBERED, XXREAL_1, VALUED_0, NAT_1, INT_1, RANDOM_3, FINANCE1,
FINANCE3, FINANCE4, RCOMP_1, XCMPLX_0;
constructors DYNKIN, RELSET_1, FINANCE3, SUPINF_1, FINANCE4, RCOMP_1,
PARTFUN3, ORDINAL1, XXREAL_3, FINSUB_1;
registrations XCMPLX_0, RELAT_1, PROB_1, SUBSET_1, MEMBERED, ORDINAL1,
FUNCT_2, NUMBERS, RELSET_1, XBOOLE_0, XXREAL_0, FINANCE4, NAT_1, XREAL_0,
XXREAL_1, VALUED_0, CARD_1, INT_1;
requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM;
begin :: Preliminaries
reserve Omega for non empty set;
reserve Sigma for SigmaField of Omega;
reserve S for non empty Subset of REAL;
reserve r for Real;
reserve T for Nat;
definition
let A be non empty set;
let I be ext-real-membered set;
let k1, k2 be Function of A, I;
pred k1 <= k2 means
:: FINANCE5:def 1 ::: ordinary ordering of functions
for w being Element of A holds k1.w <= k2.w;
end;
registration
let f be ext-real-valued Function;
let x be object;
cluster f.x -> ext-real;
end;
definition
let f1,f2 be ext-real-valued Function;
func f1 + f2 -> Function means
:: FINANCE5:def 2
dom it = dom f1 /\ dom f2 &
for x being object st x in dom it holds it.x = f1.x + f2.x;
commutativity;
end;
registration
let f1,f2 be ext-real-valued Function;
cluster f1+f2 -> ext-real-valued;
end;
registration
let C be set;
let D1,D2 be ext-real-membered non empty set;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1+f2 -> total for PartFunc of C,ExtREAL;
end;
definition
let C be set;
let D1,D2 be ext-real-membered set;
let f1 be PartFunc of C,D1;
let f2 be PartFunc of C,D2;
redefine func f1+f2 -> PartFunc of C,ExtREAL;
end;
theorem :: FINANCE5:1
for A, I, y being non empty set
for F being Function of A,I holds
{ z where z is Element of A : F.z in y } = F"y;
theorem :: FINANCE5:2
for r being Real st r>0 ex n being Nat st 1/n < r & n > 0;
theorem :: FINANCE5:3
for a,b being Real holds [.-infty,a.] /\ [.b,+infty.] = [.b,a.];
theorem :: FINANCE5:4
for r being Real st r >= 0 holds [.0,+infty.] \ [.0,r.[ = [.r,+infty.];
registration let r be ExtReal;
cluster [.r,+infty.] -> non empty;
end;
theorem :: FINANCE5:5
for k being ExtReal holds ExtREAL \ [.-infty,k.] = ].k,+infty.];
registration let a be Real;
cluster ].a,+infty.] -> non empty;
end;
begin :: Theory for Stopping Time in Discrete Time
definition
let Omega, Sigma, T;
let Filt be Filtration of StoppingSet(T),Sigma;
let k be Function of Omega,StoppingSetExt(T);
attr k is Filt-StoppingTime-like means
:: FINANCE5:def 3
k is_StoppingTime_wrt Filt,T;
end;
registration
let Omega, Sigma, T;
let MyFunc be Filtration of StoppingSet(T),Sigma;
cluster MyFunc-StoppingTime-like for Function of Omega, StoppingSetExt(T);
end;
definition
let Omega, Sigma, T;
let MyFunc be Filtration of StoppingSet(T),Sigma;
mode StoppingTime_Func of MyFunc is
MyFunc-StoppingTime-like Function of Omega,StoppingSetExt(T);
end;
theorem :: FINANCE5:6
for T be non zero Nat,
MyFunc be Filtration of StoppingSet(T),Sigma holds
not for k1,k2 be StoppingTime_Func of MyFunc holds
k1+k2 is StoppingTime_Func of MyFunc;
begin :: Theory for Stopping Time in Continuous Time
:: Using REAL, but a process, that never stops, can't be consider in this case
definition let r be Real;
mode TheEvent of r -> Subset of REAL means
:: FINANCE5:def 4
it = [.0,+infty.[ if r <= 0 otherwise it = [.0,r.];
end;
registration let r be Real;
cluster -> non empty for TheEvent of r;
end;
reserve I for TheEvent of r;
theorem :: FINANCE5:7
I is Event of Borel_Sets;
begin :: Borel-Sets
definition let r, I;
let A be Element of Borel_Sets;
func Borelsubsets_help(A,I) -> Element of Borel_Sets equals
:: FINANCE5:def 5
A /\ I;
end;
definition let r, I;
func BorelSubsets I -> SigmaField of I equals
:: FINANCE5:def 6
the set of all Borelsubsets_help(A,I) where
A is Element of Borel_Sets;
end;
definition
let Omega, Sigma, r, I;
let MyFunc be Function;
let k be random_variable of Sigma,BorelSubsets I;
pred k is_StoppingTime_wrt MyFunc means
:: FINANCE5:def 7
for t being Element of I holds
{w where w is Element of Omega: k.w<=t} in MyFunc.t;
end;
theorem :: FINANCE5:8
for MyFunc be Filtration of I,Sigma,
t2 being Element of I holds
ex q being random_variable of Sigma,BorelSubsets I st
q=Omega-->t2 & q is_StoppingTime_wrt MyFunc;
definition
let Omega, Sigma, r, I;
let Filt be Filtration of I,Sigma;
let k be random_variable of Sigma,BorelSubsets I;
attr k is Filt-StoppingTime-like means
:: FINANCE5:def 8
k is_StoppingTime_wrt Filt;
end;
registration
let Omega, Sigma, r, I;
let MyFunc be Filtration of I,Sigma;
cluster MyFunc-StoppingTime-like for random_variable of Sigma,BorelSubsets I;
end;
definition
let Omega, Sigma, r, I;
let MyFunc be Filtration of I,Sigma;
mode StoppingTime_Func of MyFunc is
MyFunc-StoppingTime-like random_variable of Sigma,BorelSubsets I;
end;
begin :: $\sigma$-Algebra of the $\tau$-past
definition
let Omega, Sigma, r, I;
let MyFunc be Filtration of I,Sigma;
let tau be StoppingTime_Func of MyFunc;
let A1 be SetSequence of Omega such that
rng(A1) c= {A where A is Element of Sigma:
for t2 being Element of I holds
A /\ {w where w is Element of Omega: tau.w<=t2} in MyFunc.t2};
let t be Element of I;
let n be Nat;
func Sigma_tauhelp2(tau,A1,n,t) ->
Element of El_Filtration(t,MyFunc) equals
:: FINANCE5:def 9
(Complement A1).n /\ {w where w is Element of Omega: tau.w<=t};
end;
definition
let Omega, Sigma, r, I;
let MyFunc be Filtration of I,Sigma;
let tau be StoppingTime_Func of MyFunc;
let A be SetSequence of Omega;
let t be Element of I;
func Sigma_tauhelp3(tau,A,t) ->
SetSequence of El_Filtration(t,MyFunc) means
:: FINANCE5:def 10
for n being Nat holds it.n=Sigma_tauhelp2(tau,A,n,t);
end;
definition
let Omega, Sigma, r, I;
let MyFunc be Filtration of I,Sigma;
let tau be StoppingTime_Func of MyFunc;
func Sigma_tau(tau) -> SigmaField of Omega equals
:: FINANCE5:def 11
{A where A is Element of Sigma:
for t being Element of I holds
A /\ {w where w is Element of Omega: tau.w<=t} in MyFunc.t};
end;
theorem :: FINANCE5:9
for MyFunc being Filtration of I,Sigma,
k1,k2 be StoppingTime_Func of MyFunc
st k1<=k2 holds
Sigma_tau(k1) c= Sigma_tau(k2);
:: Theory for Stopping time in continuous time
definition
func Ext_Family_of_halflines -> Subset-Family of ExtREAL equals
:: FINANCE5:def 12
the set of all [.-infty,r.] where r is Real;
end;
definition
func Ext_Borel_Sets -> SigmaField of ExtREAL equals
:: FINANCE5:def 13
sigma Ext_Family_of_halflines;
end;
theorem :: FINANCE5:10
for k being Real holds
].k,+infty.] is Element of Ext_Borel_Sets &
[.-infty,k.] is Element of Ext_Borel_Sets;
definition
let b be Real;
func ext_half_open_sets(b) -> SetSequence of ExtREAL means
:: FINANCE5:def 14
it.0 = ].b-1,+infty.] &
for n being Nat holds it.(n+1) = ].b-1/(n+1),+infty.];
end;
theorem :: FINANCE5:11
for b being Real holds
Intersection ext_half_open_sets(b) is Element of Ext_Borel_Sets;
theorem :: FINANCE5:12
for b being Real holds
Intersection ext_half_open_sets(b) = [.b,+infty.];
theorem :: FINANCE5:13
for a,b being Real holds [.b,a.] is Element of Ext_Borel_Sets;
theorem :: FINANCE5:14
for a being Real holds {a} is Element of Ext_Borel_Sets;
theorem :: FINANCE5:15
for r being Real holds [.r,+infty.] is Event of Ext_Borel_Sets;
definition let b be Real;
func ext_right_closed_sets(b) -> SetSequence of ExtREAL means
:: FINANCE5:def 15
for n being Nat holds it.n = [.-infty,b-n.];
end;
theorem :: FINANCE5:16
for b being Real holds
Intersection ext_right_closed_sets(b) is Element of Ext_Borel_Sets;
theorem :: FINANCE5:17
Intersection ext_right_closed_sets(0) = {-infty};
theorem :: FINANCE5:18
{-infty} is Element of Ext_Borel_Sets;
definition let b be Real;
func ext_left_closed_sets(b) -> SetSequence of ExtREAL means
:: FINANCE5:def 16
for n being Nat holds it.n = [.b+n,+infty.];
end;
theorem :: FINANCE5:19
for b being Real holds
Intersection ext_left_closed_sets(b) is Element of Ext_Borel_Sets;
theorem :: FINANCE5:20
Intersection ext_left_closed_sets(0) = {+infty};
theorem :: FINANCE5:21
{+infty} is Element of Ext_Borel_Sets;
theorem :: FINANCE5:22
REAL is Element of Ext_Borel_Sets;
theorem :: FINANCE5:23
Family_of_halflines c= Ext_Borel_Sets;
:: Ext-Borel-Sets
definition
let A be Element of Ext_Borel_Sets;
func Ext_Borelsubsets_help(A) -> Element of Ext_Borel_Sets equals
:: FINANCE5:def 17
A /\ [.0,+infty.];
end;
definition
func ExtBorelsubsets -> SigmaField of [.0,+infty.] equals
:: FINANCE5:def 18
the set of all Ext_Borelsubsets_help(A) where
A is Element of Ext_Borel_Sets;
end;
definition
let Omega, Sigma;
let MyFunc be Function;
let S be non empty ext-real-membered set;
let k be random_variable of Sigma,ExtBorelsubsets;
pred k is_StoppingTime_wrt MyFunc,S means
:: FINANCE5:def 19
for t being Element of S holds
{w where w is Element of Omega: k.w<=t} in MyFunc.t;
end;
theorem :: FINANCE5:24
for MyFunc be Filtration of S,Sigma,
t2 being Element of [.0,+infty.] holds
ex q being random_variable of Sigma,ExtBorelsubsets st
q=Omega-->t2 & q is_StoppingTime_wrt MyFunc,S;
definition
let Omega, Sigma, S;
let Filt be Filtration of S,Sigma;
let k be random_variable of Sigma,ExtBorelsubsets;
attr k is Filt-StoppingTime-like means
:: FINANCE5:def 20
k is_StoppingTime_wrt Filt,S;
end;
registration
let Omega, Sigma, S;
let MyFunc be Filtration of S,Sigma;
cluster MyFunc-StoppingTime-like for
random_variable of Sigma,ExtBorelsubsets;
end;
definition
let Omega, Sigma, S;
let MyFunc be Filtration of S,Sigma;
mode StoppingTime_Func of Sigma,MyFunc is
MyFunc-StoppingTime-like random_variable of Sigma,ExtBorelsubsets;
end;
:: $\sigma$-Algebra of the $\tau$-past
definition
let Omega, Sigma, S;
let MyFunc be Filtration of S,Sigma;
let tau be StoppingTime_Func of Sigma,MyFunc;
let A1 be SetSequence of Omega such that
rng(A1) c= {A where A is Element of Sigma:
for t2 being Element of S holds
A /\ {w where w is Element of Omega: tau.w<=t2} in MyFunc.t2};
let t be Element of S;
let n be Nat;
func Sigma_tauhelp2(MyFunc,tau,A1,n,t) ->
Element of El_Filtration(t,MyFunc) equals
:: FINANCE5:def 21
(Complement A1).n /\ {w where w is Element of Omega: tau.w<=t};
end;
definition
let Omega, Sigma, S;
let MyFunc be Filtration of S,Sigma;
let tau be StoppingTime_Func of Sigma,MyFunc;
let A1 be SetSequence of Omega;
let t be Element of S;
func Sigma_tauhelp3(MyFunc,tau,A1,t) ->
SetSequence of El_Filtration(t,MyFunc) means
:: FINANCE5:def 22
for n being Nat holds it.n=Sigma_tauhelp2(MyFunc,tau,A1,n,t);
end;
definition
let Omega, Sigma, S;
let MyFunc be Filtration of S,Sigma;
let tau be StoppingTime_Func of Sigma,MyFunc;
func Sigma_tau(MyFunc,tau) -> SigmaField of Omega equals
:: FINANCE5:def 23
{A where A is Element of Sigma:
for t being Element of S holds
A /\ {w where w is Element of Omega: tau.w<=t} in MyFunc.t};
end;
theorem :: FINANCE5:25
for MyFunc being Filtration of S,Sigma,
k1,k2 be StoppingTime_Func of Sigma,MyFunc
st k1<=k2 holds
Sigma_tau(MyFunc,k1) c= Sigma_tau(MyFunc,k2);