:: Introduction to Stopping Time in Stochastic Finance Theory
:: by Peter Jaeger
::
:: Received June 27, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users


theorem L: :: FINANCE4:1
for X being non empty set
for t being object
for f being Function st dom f = X holds
{ w where w is Element of X : f . w = t } = Coim (f,t)
proof end;

definition
let I be ext-real-membered set ;
func StoppingSetExt I -> Subset of ExtREAL equals :: FINANCE4:def 1
I \/ {+infty};
correctness
coherence
I \/ {+infty} is Subset of ExtREAL;
by MEMBERED:2;
end;

:: deftheorem defines StoppingSetExt FINANCE4:def 1 :
for I being ext-real-membered set holds StoppingSetExt I = I \/ {+infty};

registration
let I be ext-real-membered set ;
cluster StoppingSetExt I -> non empty ;
correctness
coherence
not StoppingSetExt I is empty ;
;
end;

:: Definition of stopping time
definition
let T be Nat;
func StoppingSet T -> Subset of REAL equals :: FINANCE4:def 2
 { t where t is Element of NAT : ( 0 <= t & t <= T ) } ;
correctness
coherence
{ t where t is Element of NAT : ( 0 <= t & t <= T ) } is Subset of REAL;
proof end;
end;

:: deftheorem defines StoppingSet FINANCE4:def 2 :
for T being Nat holds StoppingSet T = { t where t is Element of NAT : ( 0 <= t & t <= T ) } ;

registration
let T be Nat;
cluster StoppingSet T -> non empty ;
correctness
coherence
not StoppingSet T is empty ;
proof end;
end;

definition
let T be Nat;
func StoppingSetExt T -> Subset of ExtREAL equals :: FINANCE4:def 3
(StoppingSet T) \/ {+infty};
correctness
coherence
(StoppingSet T) \/ {+infty} is Subset of ExtREAL;
proof end;
end;

:: deftheorem defines StoppingSetExt FINANCE4:def 3 :
for T being Nat holds StoppingSetExt T = (StoppingSet T) \/ {+infty};

registration
let T be Nat;
cluster StoppingSetExt T -> non empty ;
coherence
not StoppingSetExt T is empty ;
end;

definition
let T be Nat;
let F be Function;
let R be Relation;
pred R is_StoppingTime_wrt F,T means :: FINANCE4:def 4
 for t being Element of StoppingSet T holds Coim (R,t) in F . t;
end;

:: deftheorem defines is_StoppingTime_wrt FINANCE4:def 4 :
for T being Nat
for F being Function
for R being Relation holds
( R is_StoppingTime_wrt F,T iff for t being Element of StoppingSet T holds Coim (R,t) in F . t );

definition
let Omega be non empty set ;
let T be Nat;
let MyFunc be Function;
let k be Function of Omega,(StoppingSetExt T);
:: original: is_StoppingTime_wrt
redefine pred k is_StoppingTime_wrt MyFunc,T means :: FINANCE4:def 5
 for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w = t } in MyFunc . t;
compatibility
( k is_StoppingTime_wrt MyFunc,T iff for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w = t } in MyFunc . t )
proof end;
end;

:: deftheorem defines is_StoppingTime_wrt FINANCE4:def 5 :
for Omega being non empty set
for T being Nat
for MyFunc being Function
for k being Function of Omega,(StoppingSetExt T) holds
( k is_StoppingTime_wrt MyFunc,T iff for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w = t } in MyFunc . t );

:: Alternative definition for stopping time
theorem KJK: :: FINANCE4:2
for Omega being non empty set
for Sigma being SigmaField of Omega
for T being Nat
for MyFunc being Filtration of StoppingSet T,Sigma
for k being Function of Omega,(StoppingSetExt T) holds
( k is_StoppingTime_wrt MyFunc,T iff for t being Element of StoppingSet T holds { w where w is Element of Omega : k . w <= t } in MyFunc . t )
proof end;

:: Examples of stopping times
theorem :: FINANCE4:3
for Omega being non empty set
for Sigma being SigmaField of Omega
for T being Nat
for TFix being Element of StoppingSetExt T
for MyFunc being Filtration of StoppingSet T,Sigma holds Omega --> TFix is_StoppingTime_wrt MyFunc,T
proof end;

definition
let Omega be non empty set ;
let T be Nat;
let k1, k2 be Function of Omega,(StoppingSetExt T);
func max (k1,k2) -> Function of Omega,ExtREAL means :Def20: :: FINANCE4:def 6
 for w being Element of Omega holds it . w = max ((k1 . w),(k2 . w));
existence
ex b1 being Function of Omega,ExtREAL st
for w being Element of Omega holds b1 . w = max ((k1 . w),(k2 . w))
proof end;
uniqueness
for b1, b2 being Function of Omega,ExtREAL st ( for w being Element of Omega holds b1 . w = max ((k1 . w),(k2 . w)) ) & ( for w being Element of Omega holds b2 . w = max ((k1 . w),(k2 . w)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines max FINANCE4:def 6 :
for Omega being non empty set
for T being Nat
for k1, k2 being Function of Omega,(StoppingSetExt T)
for b5 being Function of Omega,ExtREAL holds
( b5 = max (k1,k2) iff for w being Element of Omega holds b5 . w = max ((k1 . w),(k2 . w)) );

definition
let Omega be non empty set ;
let T be Nat;
let k1, k2 be Function of Omega,(StoppingSetExt T);
func min (k1,k2) -> Function of Omega,ExtREAL means :Def21: :: FINANCE4:def 7
 for w being Element of Omega holds it . w = min ((k1 . w),(k2 . w));
existence
ex b1 being Function of Omega,ExtREAL st
for w being Element of Omega holds b1 . w = min ((k1 . w),(k2 . w))
proof end;
uniqueness
for b1, b2 being Function of Omega,ExtREAL st ( for w being Element of Omega holds b1 . w = min ((k1 . w),(k2 . w)) ) & ( for w being Element of Omega holds b2 . w = min ((k1 . w),(k2 . w)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def21 defines min FINANCE4:def 7 :
for Omega being non empty set
for T being Nat
for k1, k2 being Function of Omega,(StoppingSetExt T)
for b5 being Function of Omega,ExtREAL holds
( b5 = min (k1,k2) iff for w being Element of Omega holds b5 . w = min ((k1 . w),(k2 . w)) );

theorem :: FINANCE4:4
for Omega being non empty set
for Sigma being SigmaField of Omega
for T being Nat
for MyFunc being Filtration of StoppingSet T,Sigma
for k1, k2 being Function of Omega,(StoppingSetExt T) st k1 is_StoppingTime_wrt MyFunc,T & k2 is_StoppingTime_wrt MyFunc,T holds
ex k3 being Function of Omega,(StoppingSetExt T) st
( k3 = max (k1,k2) & k3 is_StoppingTime_wrt MyFunc,T )
proof end;

theorem :: FINANCE4:5
for Omega being non empty set
for Sigma being SigmaField of Omega
for T being Nat
for MyFunc being Filtration of StoppingSet T,Sigma
for k1, k2 being Function of Omega,(StoppingSetExt T) st k1 is_StoppingTime_wrt MyFunc,T & k2 is_StoppingTime_wrt MyFunc,T holds
ex k3 being Function of Omega,(StoppingSetExt T) st
( k3 = min (k1,k2) & k3 is_StoppingTime_wrt MyFunc,T )
proof end;

Lemma1: 1 in StoppingSetExt 2
proof end;

Lemma2: 2 in StoppingSetExt 2
proof end;

definition
let t be object ;
func Special_StoppingSet t -> Element of StoppingSetExt 2 equals :: FINANCE4:def 8
 IFIN (t,{1,2},1,2);
correctness
coherence
IFIN (t,{1,2},1,2) is Element of StoppingSetExt 2;
proof end;
end;

:: deftheorem defines Special_StoppingSet FINANCE4:def 8 :
for t being object holds Special_StoppingSet t = IFIN (t,{1,2},1,2);

theorem :: FINANCE4:6
for Omega being non empty set
for Sigma being SigmaField of Omega st Omega = {1,2,3,4} holds
for MyFunc being Filtration of StoppingSet 2,Sigma st MyFunc . 0 = Special_SigmaField1 & MyFunc . 1 = Special_SigmaField2 & MyFunc . 2 = Trivial-SigmaField Omega holds
ex ST being Function of Omega,(StoppingSetExt 2) st
( ST is_StoppingTime_wrt MyFunc,2 & ST . 1 = 1 & ST . 2 = 1 & ST . 3 = 2 & ST . 4 = 2 & { w where w is Element of Omega : ST . w = 0 } = {} & { w where w is Element of Omega : ST . w = 1 } = {1,2} & { w where w is Element of Omega : ST . w = 2 } = {3,4} )
proof end;