:: 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 H₁( 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 b₁ being Function st
( dom b₁ = (dom f1) /\ (dom f2) & ( for x being object st x in dom b₁ holds
b₁ . x = (f1 . x) + (f2 . x) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = (dom f1) /\ (dom f2) & ( for x being object st x in dom b₁ holds
b₁ . x = (f1 . x) + (f2 . x) ) & dom b₂ = (dom f1) /\ (dom f2) & ( for x being object st x in dom b₂ holds
b₂ . x = (f1 . x) + (f2 . x) ) holds
b₁ = b₂

proof end;

commutativity
for b₁ being Function
for f1, f2 being ext-real-valued Function st dom b₁ = (dom f1) /\ (dom f2) & ( for x being object st x in dom b₁ holds
b₁ . x = (f1 . x) + (f2 . x) ) holds
( dom b₁ = (dom f2) /\ (dom f1) & ( for x being object st x in dom b₁ holds
b₁ . x = (f2 . x) + (f1 . x) ) ) ;

end;

:: deftheorem Def888 defines + FINANCE5:def 2 :
for f1, f2 being ext-real-valued Function
for b₃ being Function holds
( b₃ = f1 + f2 iff ( dom b₃ = (dom f1) /\ (dom f2) & ( for x being object st x in dom b₃ holds
b₃ . 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 b₁ being PartFunc of C,ExtREAL st b₁ = f1 + f2 holds
b₁ 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 b₁ being Function of Omega,(StoppingSetExt T) st b₁ 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 b₁ being Subset of REAL holds verum;
existence
( ( for b₁ being Subset of REAL holds verum ) & ( r <= 0 implies ex b₁ being Subset of REAL st b₁ = [.0,+infty.[ ) & ( not r <= 0 implies ex b₁ being Subset of REAL st b₁ = [.0,r.] ) );
;

end;

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

registration

let r be Real;

cluster -> non empty for TheEvent of r;

coherence
for b₁ being TheEvent of r holds not b₁ 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 b₁ being random_variable of Sigma, BorelSubsets I st b₁ 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 b₁ being SetSequence of El_Filtration (t,MyFunc) st
for n being Nat holds b₁ . n = Sigma_tauhelp2 (tau,A,n,t)

proof end;

uniqueness
for b₁, b₂ being SetSequence of El_Filtration (t,MyFunc) st ( for n being Nat holds b₁ . n = Sigma_tauhelp2 (tau,A,n,t) ) & ( for n being Nat holds b₂ . n = Sigma_tauhelp2 (tau,A,n,t) ) holds
b₁ = b₂

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 b₉ being SetSequence of El_Filtration (t,MyFunc) holds
( b₉ = Sigma_tauhelp3 (tau,A,t) iff for n being Nat holds b₉ . 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 b₁ being SetSequence of ExtREAL st
( b₁ . 0 = ].(b - 1),+infty.] & ( for n being Nat holds b₁ . (n + 1) = ].(b - (1 / (n + 1))),+infty.] ) )

proof end;

uniqueness
for b₁, b₂ being SetSequence of ExtREAL st b₁ . 0 = ].(b - 1),+infty.] & ( for n being Nat holds b₁ . (n + 1) = ].(b - (1 / (n + 1))),+infty.] ) & b₂ . 0 = ].(b - 1),+infty.] & ( for n being Nat holds b₂ . (n + 1) = ].(b - (1 / (n + 1))),+infty.] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def300 defines ext_half_open_sets FINANCE5:def 14 :
for b being Real
for b₂ being SetSequence of ExtREAL holds
( b₂ = ext_half_open_sets b iff ( b₂ . 0 = ].(b - 1),+infty.] & ( for n being Nat holds b₂ . (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 b₁ being SetSequence of ExtREAL st
for n being Nat holds b₁ . n = [.-infty,(b - n).]

proof end;

uniqueness
for b₁, b₂ being SetSequence of ExtREAL st ( for n being Nat holds b₁ . n = [.-infty,(b - n).] ) & ( for n being Nat holds b₂ . n = [.-infty,(b - n).] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3000 defines ext_right_closed_sets FINANCE5:def 15 :
for b being Real
for b₂ being SetSequence of ExtREAL holds
( b₂ = ext_right_closed_sets b iff for n being Nat holds b₂ . 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 b₁ being SetSequence of ExtREAL st
for n being Nat holds b₁ . n = [.(b + n),+infty.]

proof end;

uniqueness
for b₁, b₂ being SetSequence of ExtREAL st ( for n being Nat holds b₁ . n = [.(b + n),+infty.] ) & ( for n being Nat holds b₂ . n = [.(b + n),+infty.] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4000 defines ext_left_closed_sets FINANCE5:def 16 :
for b being Real
for b₂ being SetSequence of ExtREAL holds
( b₂ = ext_left_closed_sets b iff for n being Nat holds b₂ . 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 b₁ being random_variable of Sigma, ExtBorelsubsets st b₁ 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 b₁ being SetSequence of El_Filtration (t,MyFunc) st
for n being Nat holds b₁ . n = Sigma_tauhelp2 (MyFunc,tau,A1,n,t)

proof end;

uniqueness
for b₁, b₂ being SetSequence of El_Filtration (t,MyFunc) st ( for n being Nat holds b₁ . n = Sigma_tauhelp2 (MyFunc,tau,A1,n,t) ) & ( for n being Nat holds b₂ . n = Sigma_tauhelp2 (MyFunc,tau,A1,n,t) ) holds
b₁ = b₂

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 b₈ being SetSequence of El_Filtration (t,MyFunc) holds
( b₈ = Sigma_tauhelp3 (MyFunc,tau,A1,t) iff for n being Nat holds b₈ . 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;