:: 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 b₁ being Function of Omega,ExtREAL st
for w being Element of Omega holds b₁ . w = max ((k1 . w),(k2 . w))

proof end;

uniqueness
for b₁, b₂ being Function of Omega,ExtREAL st ( for w being Element of Omega holds b₁ . w = max ((k1 . w),(k2 . w)) ) & ( for w being Element of Omega holds b₂ . w = max ((k1 . w),(k2 . w)) ) holds
b₁ = b₂

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 b₅ being Function of Omega,ExtREAL holds
( b₅ = max (k1,k2) iff for w being Element of Omega holds b₅ . 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 b₁ being Function of Omega,ExtREAL st
for w being Element of Omega holds b₁ . w = min ((k1 . w),(k2 . w))

proof end;

uniqueness
for b₁, b₂ being Function of Omega,ExtREAL st ( for w being Element of Omega holds b₁ . w = min ((k1 . w),(k2 . w)) ) & ( for w being Element of Omega holds b₂ . w = min ((k1 . w),(k2 . w)) ) holds
b₁ = b₂

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 b₅ being Function of Omega,ExtREAL holds
( b₅ = min (k1,k2) iff for w being Element of Omega holds b₅ . 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;