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


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
 for w being Element of A holds k1 . w <= k2 . w;
end;

:: deftheorem defines <= FINANCE5:def 1 :
for A being non empty set
for I being ext-real-membered set
for k1, k2 being Function of A,I holds
( k1 <= k2 iff for w being Element of A holds k1 . w <= k2 . w );

registration
let f be ext-real-valued Function;
let x be object ;
cluster f . x -> ext-real ;
coherence
f . x is ext-real ;
end;

definition
let f1, f2 be ext-real-valued Function;
deffunc H1( object ) -> object = (f1 . $1) + (f2 . $1);
set X = (dom f1) /\ (dom f2);
func f1 + f2 -> Function means :Def888: :: 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) ) );
existence
ex b1 being Function st
( dom b1 = (dom f1) /\ (dom f2) & ( for x being object st x in dom b1 holds
b1 . x = (f1 . x) + (f2 . x) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = (dom f1) /\ (dom f2) & ( for x being object st x in dom b1 holds
b1 . x = (f1 . x) + (f2 . x) ) & dom b2 = (dom f1) /\ (dom f2) & ( for x being object st x in dom b2 holds
b2 . x = (f1 . x) + (f2 . x) ) holds
b1 = b2
proof end;
commutativity
for b1 being Function
for f1, f2 being ext-real-valued Function st dom b1 = (dom f1) /\ (dom f2) & ( for x being object st x in dom b1 holds
b1 . x = (f1 . x) + (f2 . x) ) holds
( dom b1 = (dom f2) /\ (dom f1) & ( for x being object st x in dom b1 holds
b1 . x = (f2 . x) + (f1 . x) ) ) ;
end;

:: deftheorem Def888 defines + FINANCE5:def 2 :
for f1, f2 being ext-real-valued Function
for b3 being Function holds
( b3 = f1 + f2 iff ( dom b3 = (dom f1) /\ (dom f2) & ( for x being object st x in dom b3 holds
b3 . x = (f1 . x) + (f2 . x) ) ) );

registration
let f1, f2 be ext-real-valued Function;
cluster f1 + f2 -> ext-real-valued ;
coherence
f1 + f2 is ext-real-valued
proof end;
end;

registration
let C be set ;
let D1, D2 be non empty ext-real-membered set ;
let f1 be Function of C,D1;
let f2 be Function of C,D2;
cluster f1 + f2 -> total for PartFunc of C,ExtREAL;
coherence
for b1 being PartFunc of C,ExtREAL st b1 = f1 + f2 holds
b1 is total
proof end;
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;
:: original: +
redefine func f1 + f2 -> PartFunc of C,ExtREAL;
coherence
f1 + f2 is PartFunc of C,ExtREAL
proof end;
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
proof end;

XX: for b being Real holds [.b,+infty.] c= ].(b - 1),+infty.]
proof end;

Lemma2: for b being Real
for n being Nat st n > 0 holds
[.b,+infty.] c= ].(b - (1 / n)),+infty.]
proof end;

theorem PP: :: FINANCE5:2
for r being Real st r > 0 holds
ex n being Nat st
( 1 / n < r & n > 0 )
proof end;

theorem CrossTh: :: FINANCE5:3
for a, b being Real holds [.-infty,a.] /\ [.b,+infty.] = [.b,a.]
proof end;

theorem :: FINANCE5:4
for r being Real st r >= 0 holds
[.0,+infty.] \ [.0,r.[ = [.r,+infty.]
proof end;

registration
let r be ExtReal;
cluster [.r,+infty.] -> non empty ;
coherence
not [.r,+infty.] is empty
proof end;
end;

theorem Th2: :: FINANCE5:5
for k being ExtReal holds ExtREAL \ [.-infty,k.] = ].k,+infty.]
proof end;

registration
let a be Real;
cluster ].a,+infty.] -> non empty ;
coherence
not ].a,+infty.] is empty
proof end;
end;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let T be Nat;
let Filt be Filtration of StoppingSet T,Sigma;
let k be Function of Omega,(StoppingSetExt T);
attr k is Filt -StoppingTime-like means :Def1: :: FINANCE5:def 3
k is_StoppingTime_wrt Filt,T;
end;

:: deftheorem Def1 defines -StoppingTime-like FINANCE5:def 3 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for T being Nat
for Filt being Filtration of StoppingSet T,Sigma
for k being Function of Omega,(StoppingSetExt T) holds
( k is Filt -StoppingTime-like iff k is_StoppingTime_wrt Filt,T );

registration
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let T be Nat;
let MyFunc be Filtration of StoppingSet T,Sigma;
cluster non empty Relation-like Omega -defined StoppingSetExt T -valued Function-like total V34(Omega, StoppingSetExt T) ext-real-valued MyFunc -StoppingTime-like for Element of K10(K11(Omega,(StoppingSetExt T)));
existence
ex b1 being Function of Omega,(StoppingSetExt T) st b1 is MyFunc -StoppingTime-like
proof end;
end;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let T be Nat;
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 Omega being non empty set
for Sigma being SigmaField of Omega
for T being non zero Nat
for MyFunc being Filtration of StoppingSet T,Sigma holds
not for k1, k2 being StoppingTime_Func of MyFunc holds k1 + k2 is StoppingTime_Func of MyFunc
proof end;

:: Using REAL, but a process, that never stops, can't be consider in this case
definition
let r be Real;
:: Using REAL, but a process, that never stops, can't be consider in this case
mode TheEvent of r -> Subset of REAL means :Def555: :: FINANCE5:def 4
it = [.0,+infty.[ if r <= 0
otherwise it = [.0,r.];
correctness
consistency
for b1 being Subset of REAL holds verum;
existence
( ( for b1 being Subset of REAL holds verum ) & ( r <= 0 implies ex b1 being Subset of REAL st b1 = [.0,+infty.[ ) & ( not r <= 0 implies ex b1 being Subset of REAL st b1 = [.0,r.] ) );
;
end;

:: deftheorem Def555 defines TheEvent FINANCE5:def 4 :
for r being Real
for b2 being Subset of REAL holds
( ( r <= 0 implies ( b2 is TheEvent of r iff b2 = [.0,+infty.[ ) ) & ( not r <= 0 implies ( b2 is TheEvent of r iff b2 = [.0,r.] ) ) );

registration
let r be Real;
cluster -> non empty for TheEvent of r;
coherence
for b1 being TheEvent of r holds not b1 is empty
proof end;
end;

theorem :: FINANCE5:7
for r being Real
for I being TheEvent of r holds I is Event of Borel_Sets
proof end;

definition
let r be Real;
let I be TheEvent of r;
let A be Element of Borel_Sets ;
func Borelsubsets_help (A,I) -> Element of Borel_Sets equals :: FINANCE5:def 5
A /\ I;
coherence
A /\ I is Element of Borel_Sets
proof end;
end;

:: deftheorem defines Borelsubsets_help FINANCE5:def 5 :
for r being Real
for I being TheEvent of r
for A being Element of Borel_Sets holds Borelsubsets_help (A,I) = A /\ I;

definition
let r be Real;
let I be TheEvent of r;
func BorelSubsets I -> SigmaField of I equals :: FINANCE5:def 6
 { (Borelsubsets_help (A,I)) where A is Element of Borel_Sets : verum } ;
coherence
{ (Borelsubsets_help (A,I)) where A is Element of Borel_Sets : verum } is SigmaField of I
proof end;
end;

:: deftheorem defines BorelSubsets FINANCE5:def 6 :
for r being Real
for I being TheEvent of r holds BorelSubsets I = { (Borelsubsets_help (A,I)) where A is Element of Borel_Sets : verum } ;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let r be Real;
let I be TheEvent of r;
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;

:: deftheorem defines is_StoppingTime_wrt FINANCE5:def 7 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for r being Real
for I being TheEvent of r
for MyFunc being Function
for k being random_variable of Sigma, BorelSubsets I holds
( k is_StoppingTime_wrt MyFunc iff for t being Element of I holds { w where w is Element of Omega : k . w <= t } in MyFunc . t );

theorem Th1: :: FINANCE5:8
for Omega being non empty set
for Sigma being SigmaField of Omega
for r being Real
for I being TheEvent of r
for MyFunc being Filtration of I,Sigma
for t2 being Element of I ex q being random_variable of Sigma, BorelSubsets I st
( q = Omega --> t2 & q is_StoppingTime_wrt MyFunc )
proof end;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let r be Real;
let I be TheEvent of r;
let Filt be Filtration of I,Sigma;
let k be random_variable of Sigma, BorelSubsets I;
attr k is Filt -StoppingTime-like means :Def1111: :: FINANCE5:def 8
k is_StoppingTime_wrt Filt;
end;

:: deftheorem Def1111 defines -StoppingTime-like FINANCE5:def 8 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for r being Real
for I being TheEvent of r
for Filt being Filtration of I,Sigma
for k being random_variable of Sigma, BorelSubsets I holds
( k is Filt -StoppingTime-like iff k is_StoppingTime_wrt Filt );

registration
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let r be Real;
let I be TheEvent of r;
let MyFunc be Filtration of I,Sigma;
cluster non empty Relation-like Omega -defined I -valued Function-like total V34(Omega,I) complex-valued ext-real-valued real-valued Sigma, BorelSubsets I -random_variable-like MyFunc -StoppingTime-like for Element of K10(K11(Omega,I));
existence
ex b1 being random_variable of Sigma, BorelSubsets I st b1 is MyFunc -StoppingTime-like
proof end;
end;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let r be Real;
let I be TheEvent of r;
let MyFunc be Filtration of I,Sigma;
mode StoppingTime_Func of MyFunc is MyFunc -StoppingTime-like random_variable of Sigma, BorelSubsets I;
end;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let r be Real;
let I be TheEvent of r;
let MyFunc be Filtration of I,Sigma;
let tau be StoppingTime_Func of MyFunc;
let A1 be SetSequence of Omega;
assume LOC1: 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 :Def8869: :: FINANCE5:def 9
((Complement A1) . n) /\ { w where w is Element of Omega : tau . w <= t } ;
correctness
coherence
((Complement A1) . n) /\ { w where w is Element of Omega : tau . w <= t } is Element of El_Filtration (t,MyFunc);
proof end;
end;

:: deftheorem Def8869 defines Sigma_tauhelp2 FINANCE5:def 9 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for r being Real
for I being TheEvent of r
for MyFunc being Filtration of I,Sigma
for tau being StoppingTime_Func of MyFunc
for A1 being SetSequence of Omega st 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 } holds
for t being Element of I
for n being Nat holds Sigma_tauhelp2 (tau,A1,n,t) = ((Complement A1) . n) /\ { w where w is Element of Omega : tau . w <= t } ;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let r be Real;
let I be TheEvent of r;
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 :Def8868: :: FINANCE5:def 10
 for n being Nat holds it . n = Sigma_tauhelp2 (tau,A,n,t);
existence
ex b1 being SetSequence of El_Filtration (t,MyFunc) st
for n being Nat holds b1 . n = Sigma_tauhelp2 (tau,A,n,t)
proof end;
uniqueness
for b1, b2 being SetSequence of El_Filtration (t,MyFunc) st ( for n being Nat holds b1 . n = Sigma_tauhelp2 (tau,A,n,t) ) & ( for n being Nat holds b2 . n = Sigma_tauhelp2 (tau,A,n,t) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8868 defines Sigma_tauhelp3 FINANCE5:def 10 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for r being Real
for I being TheEvent of r
for MyFunc being Filtration of I,Sigma
for tau being StoppingTime_Func of MyFunc
for A being SetSequence of Omega
for t being Element of I
for b9 being SetSequence of El_Filtration (t,MyFunc) holds
( b9 = Sigma_tauhelp3 (tau,A,t) iff for n being Nat holds b9 . n = Sigma_tauhelp2 (tau,A,n,t) );

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let r be Real;
let I be TheEvent of r;
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 } ;
correctness
coherence
{ 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 } is SigmaField of Omega;
proof end;
end;

:: deftheorem defines Sigma_tau FINANCE5:def 11 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for r being Real
for I being TheEvent of r
for MyFunc being Filtration of I,Sigma
for tau being StoppingTime_Func of MyFunc holds Sigma_tau tau = { 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 } ;

theorem :: FINANCE5:9
for Omega being non empty set
for Sigma being SigmaField of Omega
for r being Real
for I being TheEvent of r
for MyFunc being Filtration of I,Sigma
for k1, k2 being StoppingTime_Func of MyFunc st k1 <= k2 holds
Sigma_tau k1 c= Sigma_tau k2
proof end;

:: Theory for Stopping time in continuous time
definition
func Ext_Family_of_halflines -> Subset-Family of ExtREAL equals :: FINANCE5:def 12
 { [.-infty,r.] where r is Real : verum } ;
coherence
{ [.-infty,r.] where r is Real : verum } is Subset-Family of ExtREAL
proof end;
end;

:: deftheorem defines Ext_Family_of_halflines FINANCE5:def 12 :
Ext_Family_of_halflines = { [.-infty,r.] where r is Real : verum } ;

definition
func Ext_Borel_Sets -> SigmaField of ExtREAL equals :: FINANCE5:def 13
 sigma Ext_Family_of_halflines;
correctness
coherence
sigma Ext_Family_of_halflines is SigmaField of ExtREAL;
;
end;

:: deftheorem defines Ext_Borel_Sets FINANCE5:def 13 :
Ext_Borel_Sets = sigma Ext_Family_of_halflines;

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

definition
let b be Real;
func ext_half_open_sets b -> SetSequence of ExtREAL means :Def300: :: FINANCE5:def 14
( it . 0 = ].(b - 1),+infty.] & ( for n being Nat holds it . (n + 1) = ].(b - (1 / (n + 1))),+infty.] ) );
existence
ex b1 being SetSequence of ExtREAL st
( b1 . 0 = ].(b - 1),+infty.] & ( for n being Nat holds b1 . (n + 1) = ].(b - (1 / (n + 1))),+infty.] ) )
proof end;
uniqueness
for b1, b2 being SetSequence of ExtREAL st b1 . 0 = ].(b - 1),+infty.] & ( for n being Nat holds b1 . (n + 1) = ].(b - (1 / (n + 1))),+infty.] ) & b2 . 0 = ].(b - 1),+infty.] & ( for n being Nat holds b2 . (n + 1) = ].(b - (1 / (n + 1))),+infty.] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def300 defines ext_half_open_sets FINANCE5:def 14 :
for b being Real
for b2 being SetSequence of ExtREAL holds
( b2 = ext_half_open_sets b iff ( b2 . 0 = ].(b - 1),+infty.] & ( for n being Nat holds b2 . (n + 1) = ].(b - (1 / (n + 1))),+infty.] ) ) );

theorem Th50: :: FINANCE5:11
for b being Real holds Intersection (ext_half_open_sets b) is Element of Ext_Borel_Sets
proof end;

theorem Th60: :: FINANCE5:12
for b being Real holds Intersection (ext_half_open_sets b) = [.b,+infty.]
proof end;

theorem Th70: :: FINANCE5:13
for a, b being Real holds [.b,a.] is Element of Ext_Borel_Sets
proof end;

theorem Th71: :: FINANCE5:14
for a being Real holds {a} is Element of Ext_Borel_Sets
proof end;

theorem Th72: :: FINANCE5:15
for r being Real holds [.r,+infty.] is Event of Ext_Borel_Sets
proof end;

definition
let b be Real;
func ext_right_closed_sets b -> SetSequence of ExtREAL means :Def3000: :: FINANCE5:def 15
 for n being Nat holds it . n = [.-infty,(b - n).];
existence
ex b1 being SetSequence of ExtREAL st
for n being Nat holds b1 . n = [.-infty,(b - n).]
proof end;
uniqueness
for b1, b2 being SetSequence of ExtREAL st ( for n being Nat holds b1 . n = [.-infty,(b - n).] ) & ( for n being Nat holds b2 . n = [.-infty,(b - n).] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3000 defines ext_right_closed_sets FINANCE5:def 15 :
for b being Real
for b2 being SetSequence of ExtREAL holds
( b2 = ext_right_closed_sets b iff for n being Nat holds b2 . n = [.-infty,(b - n).] );

theorem Th500: :: FINANCE5:16
for b being Real holds Intersection (ext_right_closed_sets b) is Element of Ext_Borel_Sets
proof end;

theorem Th600: :: FINANCE5:17
Intersection (ext_right_closed_sets 0) = {-infty}
proof end;

theorem :: FINANCE5:18
{-infty} is Element of Ext_Borel_Sets by Th500, Th600;

definition
let b be Real;
func ext_left_closed_sets b -> SetSequence of ExtREAL means :Def4000: :: FINANCE5:def 16
 for n being Nat holds it . n = [.(b + n),+infty.];
existence
ex b1 being SetSequence of ExtREAL st
for n being Nat holds b1 . n = [.(b + n),+infty.]
proof end;
uniqueness
for b1, b2 being SetSequence of ExtREAL st ( for n being Nat holds b1 . n = [.(b + n),+infty.] ) & ( for n being Nat holds b2 . n = [.(b + n),+infty.] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4000 defines ext_left_closed_sets FINANCE5:def 16 :
for b being Real
for b2 being SetSequence of ExtREAL holds
( b2 = ext_left_closed_sets b iff for n being Nat holds b2 . n = [.(b + n),+infty.] );

theorem Th5000: :: FINANCE5:19
for b being Real holds Intersection (ext_left_closed_sets b) is Element of Ext_Borel_Sets
proof end;

theorem Th6000: :: FINANCE5:20
Intersection (ext_left_closed_sets 0) = {+infty}
proof end;

theorem :: FINANCE5:21
{+infty} is Element of Ext_Borel_Sets by Th5000, Th6000;

theorem :: FINANCE5:22
REAL is Element of Ext_Borel_Sets
proof end;

theorem :: FINANCE5:23
Family_of_halflines c= Ext_Borel_Sets
proof end;

:: 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.];
coherence
A /\ [.0,+infty.] is Element of Ext_Borel_Sets
proof end;
end;

:: deftheorem defines Ext_Borelsubsets_help FINANCE5:def 17 :
for A being Element of Ext_Borel_Sets holds Ext_Borelsubsets_help A = A /\ [.0,+infty.];

definition
func ExtBorelsubsets -> SigmaField of [.0,+infty.] equals :: FINANCE5:def 18
 { (Ext_Borelsubsets_help A) where A is Element of Ext_Borel_Sets : verum } ;
coherence
{ (Ext_Borelsubsets_help A) where A is Element of Ext_Borel_Sets : verum } is SigmaField of [.0,+infty.]
proof end;
end;

:: deftheorem defines ExtBorelsubsets FINANCE5:def 18 :
ExtBorelsubsets = { (Ext_Borelsubsets_help A) where A is Element of Ext_Borel_Sets : verum } ;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
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;

:: deftheorem defines is_StoppingTime_wrt FINANCE5:def 19 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for MyFunc being Function
for S being non empty ext-real-membered set
for k being random_variable of Sigma, ExtBorelsubsets holds
( k is_StoppingTime_wrt MyFunc,S iff for t being Element of S holds { w where w is Element of Omega : k . w <= t } in MyFunc . t );

theorem Th1: :: FINANCE5:24
for Omega being non empty set
for Sigma being SigmaField of Omega
for S being non empty Subset of REAL
for MyFunc being Filtration of S,Sigma
for t2 being Element of [.0,+infty.] ex q being random_variable of Sigma, ExtBorelsubsets st
( q = Omega --> t2 & q is_StoppingTime_wrt MyFunc,S )
proof end;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let S be non empty Subset of REAL;
let Filt be Filtration of S,Sigma;
let k be random_variable of Sigma, ExtBorelsubsets ;
attr k is Filt -StoppingTime-like means :Def11111: :: FINANCE5:def 20
k is_StoppingTime_wrt Filt,S;
end;

:: deftheorem Def11111 defines -StoppingTime-like FINANCE5:def 20 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for S being non empty Subset of REAL
for Filt being Filtration of S,Sigma
for k being random_variable of Sigma, ExtBorelsubsets holds
( k is Filt -StoppingTime-like iff k is_StoppingTime_wrt Filt,S );

registration
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let S be non empty Subset of REAL;
let MyFunc be Filtration of S,Sigma;
cluster non empty Relation-like Omega -defined [.0,+infty.] -valued Function-like total V34(Omega,[.0,+infty.]) ext-real-valued Sigma, ExtBorelsubsets -random_variable-like MyFunc -StoppingTime-like for Element of K10(K11(Omega,[.0,+infty.]));
existence
ex b1 being random_variable of Sigma, ExtBorelsubsets st b1 is MyFunc -StoppingTime-like
proof end;
end;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let S be non empty Subset of REAL;
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 be non empty set ;
let Sigma be SigmaField of Omega;
let S be non empty Subset of REAL;
let MyFunc be Filtration of S,Sigma;
let tau be StoppingTime_Func of Sigma,MyFunc;
let A1 be SetSequence of Omega;
assume LOC1: 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 :Def8869: :: FINANCE5:def 21
((Complement A1) . n) /\ { w where w is Element of Omega : tau . w <= t } ;
correctness
coherence
((Complement A1) . n) /\ { w where w is Element of Omega : tau . w <= t } is Element of El_Filtration (t,MyFunc);
proof end;
end;

:: deftheorem Def8869 defines Sigma_tauhelp2 FINANCE5:def 21 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for S being non empty Subset of REAL
for MyFunc being Filtration of S,Sigma
for tau being StoppingTime_Func of Sigma,MyFunc
for A1 being SetSequence of Omega st 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 } holds
for t being Element of S
for n being Nat holds Sigma_tauhelp2 (MyFunc,tau,A1,n,t) = ((Complement A1) . n) /\ { w where w is Element of Omega : tau . w <= t } ;

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let S be non empty Subset of REAL;
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 :Def8868: :: FINANCE5:def 22
 for n being Nat holds it . n = Sigma_tauhelp2 (MyFunc,tau,A1,n,t);
existence
ex b1 being SetSequence of El_Filtration (t,MyFunc) st
for n being Nat holds b1 . n = Sigma_tauhelp2 (MyFunc,tau,A1,n,t)
proof end;
uniqueness
for b1, b2 being SetSequence of El_Filtration (t,MyFunc) st ( for n being Nat holds b1 . n = Sigma_tauhelp2 (MyFunc,tau,A1,n,t) ) & ( for n being Nat holds b2 . n = Sigma_tauhelp2 (MyFunc,tau,A1,n,t) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8868 defines Sigma_tauhelp3 FINANCE5:def 22 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for S being non empty Subset of REAL
for MyFunc being Filtration of S,Sigma
for tau being StoppingTime_Func of Sigma,MyFunc
for A1 being SetSequence of Omega
for t being Element of S
for b8 being SetSequence of El_Filtration (t,MyFunc) holds
( b8 = Sigma_tauhelp3 (MyFunc,tau,A1,t) iff for n being Nat holds b8 . n = Sigma_tauhelp2 (MyFunc,tau,A1,n,t) );

definition
let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let S be non empty Subset of REAL;
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 } ;
coherence
{ 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 } is SigmaField of Omega
proof end;
end;

:: deftheorem defines Sigma_tau FINANCE5:def 23 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for S being non empty Subset of REAL
for MyFunc being Filtration of S,Sigma
for tau being StoppingTime_Func of Sigma,MyFunc holds Sigma_tau (MyFunc,tau) = { 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 } ;

theorem :: FINANCE5:25
for Omega being non empty set
for Sigma being SigmaField of Omega
for S being non empty Subset of REAL
for MyFunc being Filtration of S,Sigma
for k1, k2 being StoppingTime_Func of Sigma,MyFunc st k1 <= k2 holds
Sigma_tau (MyFunc,k1) c= Sigma_tau (MyFunc,k2)
proof end;