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

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 ;

correctness

coherence

I \/ {+infty} is Subset of ExtREAL;

by MEMBERED:2;

end;
correctness

coherence

I \/ {+infty} is Subset of ExtREAL;

by MEMBERED:2;

:: deftheorem defines StoppingSetExt FINANCE4:def 1 :

for I being ext-real-membered set holds StoppingSetExt I = I \/ {+infty};

for I being ext-real-membered set holds StoppingSetExt I = I \/ {+infty};

registration
end;

:: Definition of stopping time

definition

let T be Nat;

coherence

{ t where t is Element of NAT : ( 0 <= t & t <= T ) } is Subset of REAL;

end;
func StoppingSet T -> Subset of REAL equals :: FINANCE4:def 2

{ t where t is Element of NAT : ( 0 <= t & t <= T ) } ;

correctness { t where t is Element of NAT : ( 0 <= t & t <= T ) } ;

coherence

{ t where t is Element of NAT : ( 0 <= t & t <= T ) } is Subset of REAL;

proof 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 ) } ;

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

definition
end;

:: deftheorem defines StoppingSetExt FINANCE4:def 3 :

for T being Nat holds StoppingSetExt T = (StoppingSet T) \/ {+infty};

for T being Nat holds StoppingSetExt T = (StoppingSet T) \/ {+infty};

registration
end;

definition

let T be Nat;

let F be Function;

let R be Relation;

end;
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;

for t being Element of StoppingSet T holds Coim (R,t) in F . t;

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

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

( 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 )

end;
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 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;

( 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;

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

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 )

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

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

ex b_{1} being Function of Omega,ExtREAL st

for w being Element of Omega holds b_{1} . w = max ((k1 . w),(k2 . w))

for b_{1}, b_{2} being Function of Omega,ExtREAL st ( for w being Element of Omega holds b_{1} . w = max ((k1 . w),(k2 . w)) ) & ( for w being Element of Omega holds b_{2} . w = max ((k1 . w),(k2 . w)) ) holds

b_{1} = b_{2}

end;
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 for w being Element of Omega holds it . w = max ((k1 . w),(k2 . w));

ex b

for w being Element of Omega holds b

proof end;

uniqueness for b

b

proof 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_{5} being Function of Omega,ExtREAL holds

( b_{5} = max (k1,k2) iff for w being Element of Omega holds b_{5} . w = max ((k1 . w),(k2 . w)) );

for Omega being non empty set

for T being Nat

for k1, k2 being Function of Omega,(StoppingSetExt T)

for b

( b

definition

let Omega be non empty set ;

let T be Nat;

let k1, k2 be Function of Omega,(StoppingSetExt T);

ex b_{1} being Function of Omega,ExtREAL st

for w being Element of Omega holds b_{1} . w = min ((k1 . w),(k2 . w))

for b_{1}, b_{2} being Function of Omega,ExtREAL st ( for w being Element of Omega holds b_{1} . w = min ((k1 . w),(k2 . w)) ) & ( for w being Element of Omega holds b_{2} . w = min ((k1 . w),(k2 . w)) ) holds

b_{1} = b_{2}

end;
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 for w being Element of Omega holds it . w = min ((k1 . w),(k2 . w));

ex b

for w being Element of Omega holds b

proof end;

uniqueness for b

b

proof 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_{5} being Function of Omega,ExtREAL holds

( b_{5} = min (k1,k2) iff for w being Element of Omega holds b_{5} . w = min ((k1 . w),(k2 . w)) );

for Omega being non empty set

for T being Nat

for k1, k2 being Function of Omega,(StoppingSetExt T)

for b

( b

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 )

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 )

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 ;

coherence

IFIN (t,{1,2},1,2) is Element of StoppingSetExt 2;

end;
func Special_StoppingSet t -> Element of StoppingSetExt 2 equals :: FINANCE4:def 8

IFIN (t,{1,2},1,2);

correctness IFIN (t,{1,2},1,2);

coherence

IFIN (t,{1,2},1,2) is Element of StoppingSetExt 2;

proof end;

:: deftheorem defines Special_StoppingSet FINANCE4:def 8 :

for t being object holds Special_StoppingSet t = IFIN (t,{1,2},1,2);

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} )

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;