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