:: by Peter Jaeger

::

:: Received November 29, 2017

:: Copyright (c) 2017-2021 Association of Mizar Users

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

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

definition

let f1, f2 be ext-real-valued Function;

deffunc H_{1}( object ) -> object = (f1 . $1) + (f2 . $1);

set X = (dom f1) /\ (dom f2);

ex b_{1} being Function st

( dom b_{1} = (dom f1) /\ (dom f2) & ( for x being object st x in dom b_{1} holds

b_{1} . x = (f1 . x) + (f2 . x) ) )

for b_{1}, b_{2} being Function st dom b_{1} = (dom f1) /\ (dom f2) & ( for x being object st x in dom b_{1} holds

b_{1} . x = (f1 . x) + (f2 . x) ) & dom b_{2} = (dom f1) /\ (dom f2) & ( for x being object st x in dom b_{2} holds

b_{2} . x = (f1 . x) + (f2 . x) ) holds

b_{1} = b_{2}

for b_{1} being Function

for f1, f2 being ext-real-valued Function st dom b_{1} = (dom f1) /\ (dom f2) & ( for x being object st x in dom b_{1} holds

b_{1} . x = (f1 . x) + (f2 . x) ) holds

( dom b_{1} = (dom f2) /\ (dom f1) & ( for x being object st x in dom b_{1} holds

b_{1} . x = (f2 . x) + (f1 . x) ) )
;

end;
deffunc H

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 ( dom it = (dom f1) /\ (dom f2) & ( for x being object st x in dom it holds

it . x = (f1 . x) + (f2 . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

commutativity for b

for f1, f2 being ext-real-valued Function st dom b

b

( dom b

b

:: deftheorem Def888 defines + FINANCE5:def 2 :

for f1, f2 being ext-real-valued Function

for b_{3} being Function holds

( b_{3} = f1 + f2 iff ( dom b_{3} = (dom f1) /\ (dom f2) & ( for x being object st x in dom b_{3} holds

b_{3} . x = (f1 . x) + (f2 . x) ) ) );

for f1, f2 being ext-real-valued Function

for b

( b

b

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

coherence

for b_{1} being PartFunc of C,ExtREAL st b_{1} = f1 + f2 holds

b_{1} is total

end;
let D1, D2 be non empty ext-real-membered set ;

let f1 be Function of C,D1;

let f2 be Function of C,D2;

coherence

for b

b

proof 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

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

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

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;

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

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

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

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;

ex b_{1} being Function of Omega,(StoppingSetExt T) st b_{1} is MyFunc -StoppingTime-like

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

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

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

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;

consistency

for b_{1} being Subset of REAL holds verum;

existence

( ( for b_{1} being Subset of REAL holds verum ) & ( r <= 0 implies ex b_{1} being Subset of REAL st b_{1} = [.0,+infty.[ ) & ( not r <= 0 implies ex b_{1} being Subset of REAL st b_{1} = [.0,r.] ) );

;

end;
:: 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 it = [.0,+infty.[ if r <= 0

otherwise it = [.0,r.];

consistency

for b

existence

( ( for b

;

:: deftheorem Def555 defines TheEvent FINANCE5:def 4 :

for r being Real

for b_{2} being Subset of REAL holds

( ( r <= 0 implies ( b_{2} is TheEvent of r iff b_{2} = [.0,+infty.[ ) ) & ( not r <= 0 implies ( b_{2} is TheEvent of r iff b_{2} = [.0,r.] ) ) );

for r being Real

for b

( ( r <= 0 implies ( b

registration
end;

definition

let r be Real;

let I be TheEvent of r;

let A be Element of Borel_Sets ;

coherence

A /\ I is Element of Borel_Sets

end;
let I be TheEvent of r;

let A be Element of Borel_Sets ;

coherence

A /\ I is Element of Borel_Sets

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

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;

{ (Borelsubsets_help (A,I)) where A is Element of Borel_Sets : verum } is SigmaField of I

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

{ (Borelsubsets_help (A,I)) where A is Element of Borel_Sets : verum } is SigmaField of I

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

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;

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

for t being Element of I holds { w where w is Element of Omega : k . w <= t } in MyFunc . t;

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

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 )

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;

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

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

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;

ex b_{1} being random_variable of Sigma, BorelSubsets I st b_{1} is MyFunc -StoppingTime-like

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

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 MyFunc be Filtration of I,Sigma;

mode StoppingTime_Func of MyFunc is MyFunc -StoppingTime-like random_variable of Sigma, BorelSubsets I;

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

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;

coherence

((Complement A1) . n) /\ { w where w is Element of Omega : tau . w <= t } is Element of El_Filtration (t,MyFunc);

end;
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 ((Complement A1) . n) /\ { w where w is Element of Omega : tau . w <= t } ;

coherence

((Complement A1) . n) /\ { w where w is Element of Omega : tau . w <= t } is Element of El_Filtration (t,MyFunc);

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

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;

ex b_{1} being SetSequence of El_Filtration (t,MyFunc) st

for n being Nat holds b_{1} . n = Sigma_tauhelp2 (tau,A,n,t)

for b_{1}, b_{2} being SetSequence of El_Filtration (t,MyFunc) st ( for n being Nat holds b_{1} . n = Sigma_tauhelp2 (tau,A,n,t) ) & ( for n being Nat holds b_{2} . n = Sigma_tauhelp2 (tau,A,n,t) ) holds

b_{1} = b_{2}

end;
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 for n being Nat holds it . n = Sigma_tauhelp2 (tau,A,n,t);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof 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_{9} being SetSequence of El_Filtration (t,MyFunc) holds

( b_{9} = Sigma_tauhelp3 (tau,A,t) iff for n being Nat holds b_{9} . n = Sigma_tauhelp2 (tau,A,n,t) );

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

( b

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;

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;

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

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;

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

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

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

{ [.-infty,r.] where r is Real : verum } is Subset-Family of ExtREAL
end;

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

{ [.-infty,r.] where r is Real : verum } is Subset-Family of ExtREAL

proof end;

:: deftheorem defines Ext_Family_of_halflines FINANCE5:def 12 :

Ext_Family_of_halflines = { [.-infty,r.] where r is Real : verum } ;

Ext_Family_of_halflines = { [.-infty,r.] where r is Real : verum } ;

definition

coherence

sigma Ext_Family_of_halflines is SigmaField of ExtREAL;

;

end;

func Ext_Borel_Sets -> SigmaField of ExtREAL equals :: FINANCE5:def 13

sigma Ext_Family_of_halflines;

correctness sigma Ext_Family_of_halflines;

coherence

sigma Ext_Family_of_halflines is SigmaField of ExtREAL;

;

:: deftheorem defines Ext_Borel_Sets FINANCE5:def 13 :

Ext_Borel_Sets = sigma Ext_Family_of_halflines;

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 )

( ].k,+infty.] is Element of Ext_Borel_Sets & [.-infty,k.] is Element of Ext_Borel_Sets )

proof end;

definition

let b be Real;

ex b_{1} being SetSequence of ExtREAL st

( b_{1} . 0 = ].(b - 1),+infty.] & ( for n being Nat holds b_{1} . (n + 1) = ].(b - (1 / (n + 1))),+infty.] ) )

for b_{1}, b_{2} being SetSequence of ExtREAL st b_{1} . 0 = ].(b - 1),+infty.] & ( for n being Nat holds b_{1} . (n + 1) = ].(b - (1 / (n + 1))),+infty.] ) & b_{2} . 0 = ].(b - 1),+infty.] & ( for n being Nat holds b_{2} . (n + 1) = ].(b - (1 / (n + 1))),+infty.] ) holds

b_{1} = b_{2}

end;
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 ( it . 0 = ].(b - 1),+infty.] & ( for n being Nat holds it . (n + 1) = ].(b - (1 / (n + 1))),+infty.] ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def300 defines ext_half_open_sets FINANCE5:def 14 :

for b being Real

for b_{2} being SetSequence of ExtREAL holds

( b_{2} = ext_half_open_sets b iff ( b_{2} . 0 = ].(b - 1),+infty.] & ( for n being Nat holds b_{2} . (n + 1) = ].(b - (1 / (n + 1))),+infty.] ) ) );

for b being Real

for b

( b

definition

let b be Real;

ex b_{1} being SetSequence of ExtREAL st

for n being Nat holds b_{1} . n = [.-infty,(b - n).]

for b_{1}, b_{2} being SetSequence of ExtREAL st ( for n being Nat holds b_{1} . n = [.-infty,(b - n).] ) & ( for n being Nat holds b_{2} . n = [.-infty,(b - n).] ) holds

b_{1} = b_{2}

end;
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 for n being Nat holds it . n = [.-infty,(b - n).];

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3000 defines ext_right_closed_sets FINANCE5:def 15 :

for b being Real

for b_{2} being SetSequence of ExtREAL holds

( b_{2} = ext_right_closed_sets b iff for n being Nat holds b_{2} . n = [.-infty,(b - n).] );

for b being Real

for b

( b

definition

let b be Real;

ex b_{1} being SetSequence of ExtREAL st

for n being Nat holds b_{1} . n = [.(b + n),+infty.]

for b_{1}, b_{2} being SetSequence of ExtREAL st ( for n being Nat holds b_{1} . n = [.(b + n),+infty.] ) & ( for n being Nat holds b_{2} . n = [.(b + n),+infty.] ) holds

b_{1} = b_{2}

end;
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 for n being Nat holds it . n = [.(b + n),+infty.];

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4000 defines ext_left_closed_sets FINANCE5:def 16 :

for b being Real

for b_{2} being SetSequence of ExtREAL holds

( b_{2} = ext_left_closed_sets b iff for n being Nat holds b_{2} . n = [.(b + n),+infty.] );

for b being Real

for b

( b

:: Ext-Borel-Sets

definition

let A be Element of Ext_Borel_Sets ;

A /\ [.0,+infty.] is Element of Ext_Borel_Sets

end;
func Ext_Borelsubsets_help A -> Element of Ext_Borel_Sets equals :: FINANCE5:def 17

A /\ [.0,+infty.];

coherence A /\ [.0,+infty.];

A /\ [.0,+infty.] is Element of Ext_Borel_Sets

proof 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.];

for A being Element of Ext_Borel_Sets holds Ext_Borelsubsets_help A = A /\ [.0,+infty.];

definition

{ (Ext_Borelsubsets_help A) where A is Element of Ext_Borel_Sets : verum } is SigmaField of [.0,+infty.]
end;

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

{ (Ext_Borelsubsets_help A) where A is Element of Ext_Borel_Sets : verum } is SigmaField of [.0,+infty.]

proof end;

:: deftheorem defines ExtBorelsubsets FINANCE5:def 18 :

ExtBorelsubsets = { (Ext_Borelsubsets_help A) where A is Element of Ext_Borel_Sets : verum } ;

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 ;

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

for t being Element of S holds { w where w is Element of Omega : k . w <= t } in MyFunc . t;

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

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 )

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 ;

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

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

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;

ex b_{1} being random_variable of Sigma, ExtBorelsubsets st b_{1} is MyFunc -StoppingTime-like

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

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

:: $\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;

coherence

((Complement A1) . n) /\ { w where w is Element of Omega : tau . w <= t } is Element of El_Filtration (t,MyFunc);

end;
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 ((Complement A1) . n) /\ { w where w is Element of Omega : tau . w <= t } ;

coherence

((Complement A1) . n) /\ { w where w is Element of Omega : tau . w <= t } is Element of El_Filtration (t,MyFunc);

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

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;

ex b_{1} being SetSequence of El_Filtration (t,MyFunc) st

for n being Nat holds b_{1} . n = Sigma_tauhelp2 (MyFunc,tau,A1,n,t)

for b_{1}, b_{2} being SetSequence of El_Filtration (t,MyFunc) st ( for n being Nat holds b_{1} . n = Sigma_tauhelp2 (MyFunc,tau,A1,n,t) ) & ( for n being Nat holds b_{2} . n = Sigma_tauhelp2 (MyFunc,tau,A1,n,t) ) holds

b_{1} = b_{2}

end;
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 for n being Nat holds it . n = Sigma_tauhelp2 (MyFunc,tau,A1,n,t);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof 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_{8} being SetSequence of El_Filtration (t,MyFunc) holds

( b_{8} = Sigma_tauhelp3 (MyFunc,tau,A1,t) iff for n being Nat holds b_{8} . n = Sigma_tauhelp2 (MyFunc,tau,A1,n,t) );

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

( b

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;

{ 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

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

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

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

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)

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;