finance5.miz
begin
reserve Omega for non
empty
set;
reserve Sigma for
SigmaField of Omega;
reserve S for non
empty
Subset of
REAL ;
reserve r for
Real;
reserve T for
Nat;
definition
let A be non
empty
set;
let I be
ext-real-membered
set;
let k1,k2 be
Function of A, I;
::
FINANCE5:def1
pred k1
<= k2 means for w be
Element of A holds (k1
. w)
<= (k2
. w);
end
registration
let f be
ext-real-valued
Function;
let x be
object;
cluster (f
. x) ->
ext-real;
coherence ;
end
definition
let f1,f2 be
ext-real-valued
Function;
deffunc
F(
object) = ((f1
. $1)
+ (f2
. $1));
set X = ((
dom f1)
/\ (
dom f2));
::
FINANCE5:def2
func f1
+ f2 ->
Function means
:
Def888: (
dom it )
= ((
dom f1)
/\ (
dom f2)) & for x be
object st x
in (
dom it ) holds (it
. x)
= ((f1
. x)
+ (f2
. x));
existence
proof
ex f be
Function st (
dom f)
= X & for x be
object st x
in X holds (f
. x)
=
F(x) from
FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let f,g be
Function such that
A1: (
dom f)
= X and
A2: for c be
object st c
in (
dom f) holds (f
. c)
=
F(c) and
A3: (
dom g)
= X and
A4: for c be
object st c
in (
dom g) holds (g
. c)
=
F(c);
now
let x be
object;
assume
A5: x
in (
dom f);
hence (f
. x)
=
F(x) by
A2
.= (g
. x) by
A1,
A3,
A4,
A5;
end;
hence thesis by
A1,
A3;
end;
commutativity ;
end
registration
let f1,f2 be
ext-real-valued
Function;
cluster (f1
+ f2) ->
ext-real-valued;
coherence
proof
let x be
object;
assume x
in (
dom (f1
+ f2));
then ((f1
+ f2)
. x)
= ((f1
. x)
+ (f2
. x)) by
Def888;
hence thesis;
end;
end
registration
let C be
set;
let D1,D2 be
ext-real-membered non
empty
set;
let f1 be
Function of C, D1;
let f2 be
Function of C, D2;
cluster (f1
+ f2) ->
total;
coherence
proof
(
dom f1)
= C & (
dom f2)
= C by
FUNCT_2:def 1;
then (
dom (f1
+ f2))
= (C
/\ C) by
Def888;
hence thesis by
PARTFUN1:def 2;
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
proof
(
dom (f1
+ f2))
= ((
dom f1)
/\ (
dom f2)) & (
rng (f1
+ f2))
c=
ExtREAL by
Def888,
VALUED_0:def 2;
hence thesis by
RELSET_1: 4;
end;
end
theorem ::
FINANCE5:1
for A,I,y be non
empty
set holds for F be
Function of A, I holds { z where z be
Element of A : (F
. z)
in y }
= (F
" y)
proof
let A,I,y be non
empty
set;
let F be
Function of A, I;
for x be
object holds x
in { z where z be
Element of A : (F
. z)
in y } iff x
in (F
" y)
proof
let x be
object;
hereby
assume x
in { z where z be
Element of A : (F
. z)
in y };
then
consider z be
Element of A such that
A1: x
= z & (F
. z)
in y;
z
in A;
then z
in (
dom F) by
FUNCT_2:def 1;
hence x
in (F
" y) by
FUNCT_1:def 7,
A1;
end;
assume x
in (F
" y);
then x
in (
dom F) & (F
. x)
in y by
FUNCT_1:def 7;
hence x
in { z where z be
Element of A : (F
. z)
in y };
end;
hence thesis by
TARSKI: 2;
end;
XX: for b be
Real holds
[.b,
+infty .]
c=
].(b
- 1),
+infty .]
proof
let b be
Real;
(b
- 1)
< b by
XREAL_1: 44;
hence thesis by
XXREAL_1: 39;
end;
Lemma2: for b be
Real, n be
Nat st n
>
0 holds
[.b,
+infty .]
c=
].(b
- (1
/ n)),
+infty .]
proof
let b be
Real, n be
Nat;
assume n
>
0 ;
then (b
- (1
/ n))
< b by
XREAL_1: 44;
hence thesis by
XXREAL_1: 39;
end;
theorem ::
FINANCE5:2
PP: for r be
Real st r
>
0 holds ex n be
Nat st (1
/ n)
< r & n
>
0
proof
let r be
Real;
assume
A1: r
>
0 ;
consider n be
Nat such that
A2: (1
/ r)
< n by
SEQ_4: 3;
take n;
SS: (r
" )
= (1
/ r) & (n
" )
= (1
/ n) by
XCMPLX_1: 215;
((r
" )
" )
> (n
" ) by
A2,
SS,
A1,
XREAL_1: 88;
hence (1
/ n)
< r by
XCMPLX_1: 215;
thus thesis by
A1,
A2;
end;
theorem ::
FINANCE5:3
CrossTh: for a,b be
Real holds (
[.
-infty , a.]
/\
[.b,
+infty .])
=
[.b, a.]
proof
let a,b be
Real;
thus (
[.
-infty , a.]
/\
[.b,
+infty .])
c=
[.b, a.]
proof
let x be
object;
assume x
in (
[.
-infty , a.]
/\
[.b,
+infty .]);
then x
in
[.
-infty , a.] & x
in
[.b,
+infty .] by
XBOOLE_0:def 4;
then
B1: x
in { c where c be
Element of
ExtREAL :
-infty
<= c & c
<= a } & x
in { c where c be
Element of
ExtREAL : b
<= c & c
<=
+infty } by
XXREAL_1:def 1;
consider c be
Element of
ExtREAL such that
B2: x
= c &
-infty
<= c & c
<= a by
B1;
ex d be
Element of
ExtREAL st x
= d & b
<= d & d
<=
+infty by
B1;
hence thesis by
XXREAL_1: 1,
B2;
end;
let x be
object;
assume x
in
[.b, a.];
then x
in { c where c be
Element of
ExtREAL : b
<= c & c
<= a } by
XXREAL_1:def 1;
then
consider c be
Element of
ExtREAL such that
B1: x
= c & b
<= c & c
<= a;
reconsider x as
Element of
ExtREAL by
B1;
B2:
-infty
<= x & x
<=
+infty by
XXREAL_0: 3,
XXREAL_0: 5;
then
F1: x
in
[.
-infty , a.] by
XXREAL_1: 1,
B1;
x
in
[.b,
+infty .] by
XXREAL_1: 1,
B2,
B1;
hence thesis by
XBOOLE_0:def 4,
F1;
end;
theorem ::
FINANCE5:4
for r be
Real st r
>=
0 holds (
[.
0 ,
+infty .]
\
[.
0 , r.[)
=
[.r,
+infty .]
proof
let r be
Real;
assume
A0: r
>=
0 ;
for x be
object holds x
in (
[.
0 ,
+infty .]
\
[.
0 , r.[) iff x
in
[.r,
+infty .]
proof
let x be
object;
thus x
in (
[.
0 ,
+infty .]
\
[.
0 , r.[) implies x
in
[.r,
+infty .]
proof
assume x
in (
[.
0 ,
+infty .]
\
[.
0 , r.[);
then
G1: x
in
[.
0 ,
+infty .] & ( not x
in
[.
0 , r.[) by
XBOOLE_0:def 5;
then x
in { w where w be
Element of
ExtREAL :
0
<= w & w
<=
+infty } by
XXREAL_1:def 1;
then
consider w be
Element of
ExtREAL such that
G2: x
= w &
0
<= w & w
<=
+infty ;
G3: not w
in { w where w be
Element of
ExtREAL :
0
<= w & w
< r } by
XXREAL_1:def 2,
G1,
G2;
0
> w or w
>= r by
G3;
hence thesis by
XXREAL_1: 1,
G2;
end;
assume x
in
[.r,
+infty .];
then x
in { w where w be
Element of
ExtREAL : r
<= w & w
<=
+infty } by
XXREAL_1:def 1;
then
consider w be
Element of
ExtREAL such that
H1: w
= x & w
>= r & w
<=
+infty ;
reconsider x as
Element of
ExtREAL by
H1;
H2: x
in
[.
0 ,
+infty .] by
A0,
XXREAL_1: 1,
H1;
not x
in
[.
0 , r.[ by
XXREAL_1: 3,
H1;
hence thesis by
H2,
XBOOLE_0:def 5;
end;
hence thesis;
end;
registration
let r be
ExtReal;
cluster
[.r,
+infty .] -> non
empty;
coherence
proof
r
<=
+infty by
XXREAL_0: 3;
hence thesis by
XXREAL_1: 1;
end;
end
theorem ::
FINANCE5:5
Th2: for k be
ExtReal holds (
ExtREAL
\
[.
-infty , k.])
=
].k,
+infty .]
proof
let k be
ExtReal;
for x be
object holds x
in (
ExtREAL
\
[.
-infty , k.]) iff x
in
].k,
+infty .]
proof
let x be
object;
hereby
assume
A2: x
in (
ExtREAL
\
[.
-infty , k.]);
A3: x
in
[.
-infty ,
+infty .] & not x
in
[.
-infty , k.] by
A2,
XBOOLE_0:def 5,
XXREAL_1: 209;
consider y be
Element of
ExtREAL such that
A4: x
= y by
A2;
y
in
[.
-infty ,
+infty .] & not (
-infty
<= y & y
<= k) by
A4,
A3,
XXREAL_1: 1;
hence x
in
].k,
+infty .] by
XXREAL_1: 2,
A4,
XXREAL_0: 3,
XXREAL_0: 5;
end;
assume
A6: x
in
].k,
+infty .];
then k
in
ExtREAL & x
in
].k,
+infty .] & x
in { a where a be
Element of
ExtREAL : k
< a & a
<=
+infty } by
XXREAL_0:def 1,
XXREAL_1:def 3;
then
consider a be
Element of
ExtREAL such that
A7: a
= x & k
< a & a
<=
+infty ;
consider y be
Element of
ExtREAL such that
A8: x
= y by
A7;
reconsider y as
Element of
ExtREAL ;
y
> k by
A6,
A8,
XXREAL_1: 2;
then y
in
ExtREAL & not y
in
[.
-infty , k.] by
XXREAL_1: 1;
hence thesis by
A8,
XBOOLE_0:def 5;
end;
hence thesis;
end;
registration
let a be
Real;
cluster
].a,
+infty .] -> non
empty;
coherence
proof
a
< (a
+ 1) by
XREAL_1: 29;
hence thesis by
XXREAL_0: 3,
XXREAL_1: 2;
end;
end
begin
definition
let Omega, Sigma, T;
let Filt be
Filtration of (
StoppingSet T), Sigma;
let k be
Function of Omega, (
StoppingSetExt T);
::
FINANCE5:def3
attr k is Filt
-StoppingTime-like means
:
Def1: k
is_StoppingTime_wrt (Filt,T);
end
registration
let Omega, Sigma, T;
let MyFunc be
Filtration of (
StoppingSet T), Sigma;
cluster MyFunc
-StoppingTime-like for
Function of Omega, (
StoppingSetExt T);
existence
proof
0
in (
StoppingSet T) or
0
in
{
+infty };
then
reconsider My1 =
0 as
Element of (
StoppingSetExt T) by
XBOOLE_0:def 3;
(Omega
--> My1)
is_StoppingTime_wrt (MyFunc,T) by
FINANCE4: 3;
hence thesis by
Def1;
end;
end
definition
let Omega, Sigma, T;
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 T be non
zero
Nat, MyFunc be
Filtration of (
StoppingSet T), Sigma holds not for k1,k2 be
StoppingTime_Func of MyFunc holds (k1
+ k2) is
StoppingTime_Func of MyFunc
proof
let T be non
zero
Nat;
let MyFunc be
Filtration of (
StoppingSet T), Sigma;
T
in
NAT by
ORDINAL1:def 12;
then T
in (
StoppingSet T) or T
in
{
+infty };
then
reconsider MyT = T as
Element of (
StoppingSetExt T) by
XBOOLE_0:def 3;
consider k1 be
Function of Omega, (
StoppingSetExt T) such that
A1: k1
= (Omega
--> MyT) & k1
is_StoppingTime_wrt (MyFunc,T) by
FINANCE4: 3;
reconsider k1 as
StoppingTime_Func of MyFunc by
A1,
Def1;
consider k2 be
Function of Omega, (
StoppingSetExt T) such that
A2: k2
= (Omega
--> MyT) & k2
is_StoppingTime_wrt (MyFunc,T) by
FINANCE4: 3;
reconsider k2 as
StoppingTime_Func of MyFunc by
A2,
Def1;
take k1, k2;
F1: not (T
+ T)
in
{
+infty } by
TARSKI:def 1;
ex w be
Element of (
dom (k1
+ k2)) st w
in (
dom (k1
+ k2)) & not ((k1
+ k2)
. w)
in (
StoppingSetExt T)
proof
consider w2 be
object such that
C1: w2
in (
dom (k1
+ k2)) by
XBOOLE_0:def 1;
reconsider w2 as
Element of Omega by
C1;
e3: (k1
. w2)
= T & (k2
. w2)
= T by
A1,
FUNCOP_1: 7,
A2;
XX: (T
+ T)
= ((k1
. w2)
+ (k2
. w2)) by
e3,
XXREAL_3:def 2
.= ((k1
+ k2)
. w2) by
C1,
Def888;
not ((k1
+ k2)
. w2)
in (
StoppingSetExt T)
proof
not (T
+ T)
in (
StoppingSetExt T)
proof
not (T
+ T)
in { t where t be
Element of
NAT :
0
<= t
<= T }
proof
not ex t2 be
Element of
NAT st t2
= (T
+ T) &
0
<= t2
<= T by
NAT_1: 16;
hence thesis;
end;
hence thesis by
F1,
XBOOLE_0:def 3;
end;
hence thesis by
XX;
end;
hence thesis by
C1;
end;
hence thesis by
FUNCT_2: 5;
end;
begin
definition
let r be
Real;
::
FINANCE5:def4
mode
TheEvent of r ->
Subset of
REAL means
:
Def555: it
=
[.
0 ,
+infty .[ if r
<=
0
otherwise it
=
[.
0 , r.];
correctness ;
end
registration
let r be
Real;
cluster -> non
empty for
TheEvent of r;
coherence
proof
let e be
TheEvent of r;
per cases ;
suppose r
<=
0 ;
then e
=
[.
0 ,
+infty .[ by
Def555;
hence thesis by
XXREAL_1: 3;
end;
suppose
A1: r
>
0 ;
then e
=
[.
0 , r.] by
Def555;
hence thesis by
A1,
XXREAL_1: 1;
end;
end;
end
reserve I for
TheEvent of r;
theorem ::
FINANCE5:7
I is
Event of
Borel_Sets
proof
per cases ;
suppose
S1: r
<=
0 ;
[.
0 ,
+infty .[ is
Element of
Borel_Sets by
FINANCE1: 3;
hence thesis by
S1,
Def555;
end;
suppose
S1: r
>
0 ;
[.
0 , r.] is
Element of
Borel_Sets by
FINANCE1: 8;
hence thesis by
S1,
Def555;
end;
end;
begin
definition
let r, I;
let A be
Element of
Borel_Sets ;
::
FINANCE5:def5
func
Borelsubsets_help (A,I) ->
Element of
Borel_Sets equals (A
/\ I);
coherence
proof
(r
<=
0 implies I
=
[.
0 ,
+infty .[) & (r
>
0 implies I
=
[.
0 , r.]) by
Def555;
then
reconsider I as
Element of
Borel_Sets by
FINANCE1: 3,
FINANCE1: 8;
A is
Event of
Borel_Sets & I is
Event of
Borel_Sets ;
hence thesis by
PROB_1: 19;
end;
end
definition
let r, I;
::
FINANCE5:def6
func
BorelSubsets I ->
SigmaField of I equals the set of all (
Borelsubsets_help (A,I)) where A be
Element of
Borel_Sets ;
coherence
proof
set BS = the set of all (
Borelsubsets_help (A,I)) where A be
Element of
Borel_Sets ;
BS is non
empty
Subset-Family of I
proof
reconsider RE =
REAL as
Element of
Borel_Sets by
PROB_1: 5;
d1: (
Borelsubsets_help (RE,I))
in BS;
BS
c= (
bool I)
proof
let x be
object;
assume x
in BS;
then
consider A be
Element of
Borel_Sets such that
D1: x
= (
Borelsubsets_help (A,I));
reconsider x as
set by
D1;
x
c= I by
D1,
XBOOLE_0:def 4;
hence thesis;
end;
hence thesis by
d1;
end;
then
reconsider BS as non
empty
Subset-Family of I;
A1: BS is
compl-closed
proof
for A be
Subset of I st A
in BS holds (A
` )
in BS
proof
let A be
Subset of I;
assume A
in BS;
then
consider A2 be
Element of
Borel_Sets such that
AF1: A
= (
Borelsubsets_help (A2,I));
F2: (I
\ A)
= ((A2
` )
/\ I)
proof
for x be
object holds x
in (I
\ A) iff x
in ((A2
` )
/\ I)
proof
let x be
object;
thus x
in (I
\ A) implies x
in ((A2
` )
/\ I)
proof
assume
ASS0: x
in (I
\ A);
reconsider I as
Subset of
REAL ;
x
in I & not x
in A by
ASS0,
XBOOLE_0:def 5;
then x
in I & ( not (x
in A2 & x
in I)) by
XBOOLE_0:def 4,
AF1;
then x
in I & x
in (
REAL
\ A2) by
XBOOLE_0:def 5;
hence thesis by
XBOOLE_0:def 4;
end;
assume x
in ((A2
` )
/\ I);
then x
in (A2
` ) & x
in I by
XBOOLE_0:def 4;
then x
in I & x
in
REAL & not x
in A2 by
XBOOLE_0:def 5;
then x
in I & not x
in (A2
/\ I) by
XBOOLE_0:def 4;
hence thesis by
XBOOLE_0:def 5,
AF1;
end;
hence thesis;
end;
reconsider CA2 = (A2
` ) as
Element of
Borel_Sets by
PROB_1: 20;
(CA2
/\ I)
= (
Borelsubsets_help (CA2,I));
hence thesis by
F2;
end;
hence thesis;
end;
BS is
sigma-multiplicative
proof
for A1 be
SetSequence of I st (
rng A1)
c= BS holds (
Intersection A1)
in BS
proof
let A1 be
SetSequence of I;
assume
G1: (
rng A1)
c= BS;
TT1: for n be
Nat holds (A1
. n)
in BS & (ex A2 be
Element of
Borel_Sets st (A1
. n)
= (
Borelsubsets_help (A2,I)))
proof
let n be
Nat;
(A1
. n)
in (
rng A1) by
FUNCT_2: 4,
ORDINAL1:def 12;
then (A1
. n)
in BS by
G1;
hence thesis;
end;
(
rng A1)
c= (
bool
REAL )
proof
let x be
object;
assume
d1: x
in (
rng A1);
(
bool I)
c= (
bool
REAL ) by
ZFMISC_1: 67;
hence thesis by
d1;
end;
then
reconsider A10 = A1 as
SetSequence of
REAL by
FUNCT_2: 6;
for n be
Nat holds (A10
. n) is
Event of
Borel_Sets
proof
let n be
Nat;
ex A2 be
Element of
Borel_Sets st (A10
. n)
= (
Borelsubsets_help (A2,I)) by
TT1;
hence thesis;
end;
then
reconsider A10 as
SetSequence of
Borel_Sets by
PROB_1: 25;
set UA1 = (
Union (
Complement A10));
for n be
Nat holds ((
Complement A10)
. n) is
Event of
Borel_Sets
proof
let n be
Nat;
consider A2 be
Element of
Borel_Sets such that
P1: (A10
. n)
= (
Borelsubsets_help (A2,I)) by
TT1;
reconsider A1n = (A10
. n) as
Element of
Borel_Sets by
P1;
(A1n
` ) is
Element of
Borel_Sets by
PROB_1: 20;
hence thesis by
PROB_1:def 2;
end;
then (
Complement A10) is
SetSequence of
Borel_Sets by
PROB_1: 25;
then
reconsider UA1 as
Event of
Borel_Sets by
PROB_1: 26;
k1: (UA1
` ) is
Event of
Borel_Sets by
PROB_1: 20;
reconsider IA1 = (
Intersection A10) as
Element of
Borel_Sets by
k1;
s0: IA1
in BS & IA1
= (
Borelsubsets_help (IA1,I))
proof
for x be
object holds x
in IA1 iff x
in (
Borelsubsets_help (IA1,I))
proof
let x be
object;
thus x
in IA1 implies x
in (
Borelsubsets_help (IA1,I))
proof
assume x
in IA1;
then x
in IA1 & x
in (A1
.
0 ) by
PROB_1: 13;
hence thesis by
XBOOLE_0:def 4;
end;
thus thesis by
XBOOLE_0:def 4;
end;
then IA1
= (
Borelsubsets_help (IA1,I)) by
TARSKI: 2;
hence thesis;
end;
(
Intersection A10)
= (
Intersection A1)
proof
for x be
object holds x
in (
Intersection A10) iff x
in (
Intersection A1)
proof
let x be
object;
x
in (
Intersection A10) iff for n be
Nat holds x
in (A10
. n) by
PROB_1: 13;
then x
in (
Intersection A10) iff for n be
Nat holds x
in (A1
. n);
hence thesis by
PROB_1: 13;
end;
hence thesis;
end;
hence thesis by
s0;
end;
hence thesis;
end;
hence thesis by
A1;
end;
end
definition
let Omega, Sigma, r, I;
let MyFunc be
Function;
let k be
random_variable of Sigma, (
BorelSubsets I);
::
FINANCE5:def7
pred k
is_StoppingTime_wrt MyFunc means for t be
Element of I holds { w where w be
Element of Omega : (k
. w)
<= t }
in (MyFunc
. t);
end
theorem ::
FINANCE5:8
Th1: for MyFunc be
Filtration of I, Sigma, t2 be
Element of I holds ex q be
random_variable of Sigma, (
BorelSubsets I) st q
= (Omega
--> t2) & q
is_StoppingTime_wrt MyFunc
proof
let MyFunc be
Filtration of I, Sigma;
let t2 be
Element of I;
set Sigma2 = (
BorelSubsets I);
Fin1: for t be
Element of I holds { w where w be
Element of Omega : ((Omega
--> t2)
. w)
<= t }
in (MyFunc
. t)
proof
let t be
Element of I;
set WW = { w where w be
Element of Omega : ((Omega
--> t2)
. w)
<= t };
reconsider MyFt = (MyFunc
. t) as
SigmaField of Omega by
KOLMOG01:def 2;
per cases ;
suppose
S1: t2
<= t;
H1: for x be
object st x
in WW holds x
in Omega
proof
let x be
object;
assume x
in WW;
then ex w3 be
Element of Omega st w3
= x & ((Omega
--> t2)
. w3)
<= t;
hence thesis;
end;
WW
= Omega
proof
for x be
object holds x
in Omega implies x
in WW
proof
let x be
object;
assume x
in Omega;
then
reconsider x as
Element of Omega;
((Omega
--> t2)
. x)
= t2 by
FUNCOP_1: 7;
hence thesis by
S1;
end;
hence thesis by
H1,
TARSKI: 2;
end;
then WW
in MyFt by
PROB_1: 5;
hence thesis;
end;
suppose
S1: t2
> t;
WW
c=
{}
proof
let x be
object;
assume x
in WW;
then ex w3 be
Element of Omega st w3
= x & ((Omega
--> t2)
. w3)
<= t;
hence thesis by
S1,
FUNCOP_1: 7;
end;
then WW
=
{} ;
then WW
in MyFt by
PROB_1: 4;
hence thesis;
end;
end;
set OC = (Omega
--> t2);
OC is
random_variable of Sigma, Sigma2 by
FINANCE3: 10;
then
reconsider OC as
random_variable of Sigma, Sigma2;
OC
is_StoppingTime_wrt MyFunc by
Fin1;
hence thesis;
end;
definition
let Omega, Sigma, r, I;
let Filt be
Filtration of I, Sigma;
let k be
random_variable of Sigma, (
BorelSubsets I);
::
FINANCE5:def8
attr k is Filt
-StoppingTime-like means
:
Def1111: k
is_StoppingTime_wrt Filt;
end
registration
let Omega, Sigma, r, I;
let MyFunc be
Filtration of I, Sigma;
cluster MyFunc
-StoppingTime-like for
random_variable of Sigma, (
BorelSubsets I);
existence
proof
consider t2 be
object such that
A0: t2
in I by
XBOOLE_0:def 1;
reconsider t2 as
Element of I by
A0;
ex q be
random_variable of Sigma, (
BorelSubsets I) st q
= (Omega
--> t2) & q
is_StoppingTime_wrt MyFunc by
Th1;
hence thesis by
Def1111;
end;
end
definition
let Omega, Sigma, r, I;
let MyFunc be
Filtration of I, Sigma;
mode
StoppingTime_Func of MyFunc is MyFunc
-StoppingTime-like
random_variable of Sigma, (
BorelSubsets I);
end
begin
definition
let Omega, Sigma, r, I;
let MyFunc be
Filtration of I, Sigma;
let tau be
StoppingTime_Func of MyFunc;
let A1 be
SetSequence of Omega;
let t be
Element of I;
let n be
Nat;
::
FINANCE5:def9
func
Sigma_tauhelp2 (tau,A1,n,t) ->
Element of (
El_Filtration (t,MyFunc)) equals
:
Def8869: (((
Complement A1)
. n)
/\ { w where w be
Element of Omega : (tau
. w)
<= t });
correctness
proof
reconsider n as
Element of
NAT by
ORDINAL1:def 12;
set MySigmatau = { A where A be
Element of Sigma : for t2 be
Element of I holds (A
/\ { w where w be
Element of Omega : (tau
. w)
<= t2 })
in (MyFunc
. t2) };
(A1
. n)
in (
rng A1) by
FUNCT_2: 4;
then (A1
. n)
in MySigmatau by
LOC1;
then
consider B be
Element of Sigma such that
GW1: (A1
. n)
= B & for t2 be
Element of I holds (B
/\ { w where w be
Element of Omega : (tau
. w)
<= t2 })
in (MyFunc
. t2);
reconsider A1n = (A1
. n) as
Element of Sigma by
GW1;
GW2: for t be
Element of I holds (((A1
. n)
` )
/\ { w where w be
Element of Omega : (tau
. w)
<= t })
in (MyFunc
. t)
proof
let t be
Element of I;
reconsider MyFt2 = (MyFunc
. t) as
SigmaField of Omega by
KOLMOG01:def 2;
E1: ({ w where w be
Element of Omega : (tau
. w)
<= t }
\ ((A1
. n)
/\ { w where w be
Element of Omega : (tau
. w)
<= t }))
= (((A1
. n)
` )
/\ { w where w be
Element of Omega : (tau
. w)
<= t })
proof
WW0: for j be
object holds j
in ({ w where w be
Element of Omega : (tau
. w)
<= t }
\ ((A1
. n)
/\ { w where w be
Element of Omega : (tau
. w)
<= t })) implies j
in (((A1
. n)
` )
/\ { w where w be
Element of Omega : (tau
. w)
<= t })
proof
let j be
object;
assume
h: j
in ({ w where w be
Element of Omega : (tau
. w)
<= t }
\ ((A1
. n)
/\ { w where w be
Element of Omega : (tau
. w)
<= t }));
then
Help0: j
in { w where w be
Element of Omega : (tau
. w)
<= t };
not j
in ((A1
. n)
/\ { w where w be
Element of Omega : (tau
. w)
<= t }) by
h,
XBOOLE_0:def 5;
then
Help2: not j
in (A1
. n) by
h,
XBOOLE_0:def 4;
j
in ((A1
. n)
` )
proof
ex w2 be
Element of Omega st j
= w2 & (tau
. w2)
<= t by
Help0;
hence thesis by
XBOOLE_0:def 5,
Help2;
end;
hence thesis by
XBOOLE_0:def 4,
h;
end;
for j be
object holds j
in (((A1
. n)
` )
/\ { w where w be
Element of Omega : (tau
. w)
<= t }) implies j
in ({ w where w be
Element of Omega : (tau
. w)
<= t }
\ ((A1
. n)
/\ { w where w be
Element of Omega : (tau
. w)
<= t }))
proof
let j be
object;
assume j
in (((A1
. n)
` )
/\ { w where w be
Element of Omega : (tau
. w)
<= t });
then
j: j
in (Omega
\ (A1
. n)) & j
in { w where w be
Element of Omega : (tau
. w)
<= t } by
XBOOLE_0:def 4;
then j
in Omega & not j
in (A1
. n) & j
in { w where w be
Element of Omega : (tau
. w)
<= t } by
XBOOLE_0:def 5;
then not j
in ((A1
. n)
/\ { w where w be
Element of Omega : (tau
. w)
<= t }) by
XBOOLE_0:def 4;
hence thesis by
j,
XBOOLE_0:def 5;
end;
hence thesis by
WW0,
TARSKI: 2;
end;
W2: ((A1
. n)
/\ { w where w be
Element of Omega : (tau
. w)
<= t }) is
Event of MyFt2 by
GW1;
tau
is_StoppingTime_wrt MyFunc by
Def1111;
then { w where w be
Element of Omega : (tau
. w)
<= t } is
Event of MyFt2;
then ({ w where w be
Element of Omega : (tau
. w)
<= t }
\ ((A1
. n)
/\ { w where w be
Element of Omega : (tau
. w)
<= t })) is
Event of MyFt2 by
W2,
PROB_1: 24;
hence thesis by
E1;
end;
((A1
. n)
` )
= ((
Complement A1)
. n) by
PROB_1:def 2;
hence thesis by
GW2;
end;
end
definition
let Omega, Sigma, r, I;
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;
::
FINANCE5:def10
func
Sigma_tauhelp3 (tau,A,t) ->
SetSequence of (
El_Filtration (t,MyFunc)) means
:
Def8868: for n be
Nat holds (it
. n)
= (
Sigma_tauhelp2 (tau,A,n,t));
existence
proof
deffunc
U(
Nat) = (
Sigma_tauhelp2 (tau,A,$1,t));
consider f be
sequence of (
El_Filtration (t,MyFunc)) such that
A1: for d be
Element of
NAT holds (f
. d)
=
U(d) from
FUNCT_2:sch 4;
reconsider f as
SetSequence of (
El_Filtration (t,MyFunc)) by
PROB_4: 2;
take f;
let n be
Nat;
n
in
NAT by
ORDINAL1:def 12;
hence thesis by
A1;
end;
uniqueness
proof
let f1,f2 be
SetSequence of (
El_Filtration (t,MyFunc));
assume that
A1: for d be
Nat holds (f1
. d)
= (
Sigma_tauhelp2 (tau,A,d,t)) and
A2: for d be
Nat holds (f2
. d)
= (
Sigma_tauhelp2 (tau,A,d,t));
for d be
Nat holds (f1
. d)
= (f2
. d)
proof
let d be
Nat;
(f1
. d)
= (
Sigma_tauhelp2 (tau,A,d,t)) by
A1;
hence thesis by
A2;
end;
hence thesis;
end;
end
definition
let Omega, Sigma, r, I;
let MyFunc be
Filtration of I, Sigma;
let tau be
StoppingTime_Func of MyFunc;
::
FINANCE5:def11
func
Sigma_tau (tau) ->
SigmaField of Omega equals { A where A be
Element of Sigma : for t be
Element of I holds (A
/\ { w where w be
Element of Omega : (tau
. w)
<= t })
in (MyFunc
. t) };
correctness
proof
set MySigmatau = { A where A be
Element of Sigma : for t be
Element of I holds (A
/\ { w where w be
Element of Omega : (tau
. w)
<= t })
in (MyFunc
. t) };
MySigmatau
c= (
bool Omega)
proof
let x be
object;
assume x
in MySigmatau;
then ex A be
Element of Sigma st x
= A & for t be
Element of I holds (A
/\ { w where w be
Element of Omega : (tau
. w)
<= t })
in (MyFunc
. t);
hence thesis;
end;
then
reconsider MySigmatau as
Subset-Family of Omega;
A1: MySigmatau is
compl-closed
proof
for A be
Subset of Omega st A
in MySigmatau holds (A
` )
in MySigmatau
proof
let A be
Subset of Omega;
assume A
in MySigmatau;
then
consider B be
Element of Sigma such that
GW1: A
= B & for t be
Element of I holds (B
/\ { w where w be
Element of Omega : (tau
. w)
<= t })
in (MyFunc
. t);
reconsider A as
Element of Sigma by
GW1;
GW2: for t be
Element of I holds ((A
` )
/\ { w where w be
Element of Omega : (tau
. w)
<= t })
in (MyFunc
. t)
proof
let t be
Element of I;
reconsider MyFt2 = (MyFunc
. t) as
SigmaField of Omega by
KOLMOG01:def 2;
WW0: for j be
object holds j
in ({ w where w be
Element of Omega : (tau
. w)
<= t }
\ (A
/\ { w where w be
Element of Omega : (tau
. w)
<= t })) implies j
in ((A
` )
/\ { w where w be
Element of Omega : (tau
. w)
<= t })
proof
let j be
object;
assume
h: j
in ({ w where w be
Element of Omega : (tau
. w)
<= t }
\ (A
/\ { w where w be
Element of Omega : (tau
. w)
<= t }));
then
Help00: j
in { w where w be
Element of Omega : (tau
. w)
<= t } & not j
in (A
/\ { w where w be
Element of Omega : (tau
. w)
<= t }) by
XBOOLE_0:def 5;
then
Help2: not j
in A by
XBOOLE_0:def 4;
j
in (A
` )
proof
ex w2 be
Element of Omega st j
= w2 & (tau
. w2)
<= t by
Help00;
hence thesis by
XBOOLE_0:def 5,
Help2;
end;
hence thesis by
XBOOLE_0:def 4,
h;
end;
E1: ({ w where w be
Element of Omega : (tau
. w)
<= t }
\ (A
/\ { w where w be
Element of Omega : (tau
. w)
<= t }))
= ((A
` )
/\ { w where w be
Element of Omega : (tau
. w)
<= t })
proof
for j be
object holds j
in ((A
` )
/\ { w where w be
Element of Omega : (tau
. w)
<= t }) implies j
in ({ w where w be
Element of Omega : (tau
. w)
<= t }
\ (A
/\ { w where w be
Element of Omega : (tau
. w)
<= t }))
proof
let j be
object;
assume j
in ((A
` )
/\ { w where w be
Element of Omega : (tau
. w)
<= t });
then
hh: j
in (Omega
\ A) & j
in { w where w be
Element of Omega : (tau
. w)
<= t } by
XBOOLE_0:def 4;
then j
in Omega & not j
in A & j
in { w where w be
Element of Omega : (tau
. w)
<= t } by
XBOOLE_0:def 5;
then not j
in (A
/\ { w where w be
Element of Omega : (tau
. w)
<= t }) by
XBOOLE_0:def 4;
hence thesis by
hh,
XBOOLE_0:def 5;
end;
hence thesis by
WW0,
TARSKI: 2;
end;
W2: (A
/\ { w where w be
Element of Omega : (tau
. w)
<= t }) is
Event of MyFt2 by
GW1;
tau
is_StoppingTime_wrt MyFunc by
Def1111;
then { w where w be
Element of Omega : (tau
. w)
<= t } is
Event of MyFt2;
then ({ w where w be
Element of Omega : (tau
. w)
<= t }
\ (A
/\ { w where w be
Element of Omega : (tau
. w)
<= t })) is
Event of MyFt2 by
W2,
PROB_1: 24;
hence thesis by
E1;
end;
Omega
in Sigma & A
in Sigma by
PROB_1: 5;
then (Omega
\ A)
in Sigma by
PROB_1: 6;
hence thesis by
GW2;
end;
hence thesis;
end;
A2: MySigmatau is
sigma-multiplicative
proof
let A1 be
SetSequence of Omega;
assume
ASSJ: (
rng A1)
c= MySigmatau;
TT1: for n be
Nat holds (A1
. n)
in MySigmatau
proof
let n be
Nat;
(A1
. n)
in (
rng A1) by
FUNCT_2: 4,
ORDINAL1:def 12;
hence thesis by
ASSJ;
end;
QQ1: for t be
Element of I holds ((
Union (
Complement A1))
/\ { w where w be
Element of Omega : (tau
. w)
<= t })
in (MyFunc
. t)
proof
let t be
Element of I;
X1: for x be
object holds x
in (
Union (
Sigma_tauhelp3 (tau,A1,t))) implies x
in ((
Union (
Complement A1))
/\ { w where w be
Element of Omega : (tau
. w)
<= t })
proof
let x be
object;
assume x
in (
Union (
Sigma_tauhelp3 (tau,A1,t)));
then
consider n be
Nat such that
V1: x
in ((
Sigma_tauhelp3 (tau,A1,t))
. n) by
PROB_1: 12;
x
in (
Sigma_tauhelp2 (tau,A1,n,t)) by
V1,
Def8868;
then x
in (((
Complement A1)
. n)
/\ { w where w be
Element of Omega : (tau
. w)
<= t }) by
ASSJ,
Def8869;
then
ZWJ1: x
in ((
Complement A1)
. n) & x
in { w where w be
Element of Omega : (tau
. w)
<= t } by
XBOOLE_0:def 4;
x
in (
Union (
Complement A1)) by
PROB_1: 12,
ZWJ1;
hence thesis by
XBOOLE_0:def 4,
ZWJ1;
end;
H: for x be
object holds x
in ((
Union (
Complement A1))
/\ { w where w be
Element of Omega : (tau
. w)
<= t }) implies x
in (
Union (
Sigma_tauhelp3 (tau,A1,t)))
proof
let x be
object;
assume x
in ((
Union (
Complement A1))
/\ { w where w be
Element of Omega : (tau
. w)
<= t });
then
ZWJ1: x
in (
Union (
Complement A1)) & x
in { w where w be
Element of Omega : (tau
. w)
<= t } by
XBOOLE_0:def 4;
then
consider n be
Nat such that
ZWJ2: x
in ((
Complement A1)
. n) by
PROB_1: 12;
x
in (((
Complement A1)
. n)
/\ { w where w be
Element of Omega : (tau
. w)
<= t }) by
XBOOLE_0:def 4,
ZWJ1,
ZWJ2;
then
ZWJ2: x
in (
Sigma_tauhelp2 (tau,A1,n,t)) by
ASSJ,
Def8869;
x
in ((
Sigma_tauhelp3 (tau,A1,t))
. n) by
ZWJ2,
Def8868;
hence thesis by
PROB_1: 12;
end;
(
Union (
Sigma_tauhelp3 (tau,A1,t)))
= ((
Union (
Complement A1))
/\ { w where w be
Element of Omega : (tau
. w)
<= t }) by
H,
X1,
TARSKI: 2;
hence thesis by
PROB_1: 17;
end;
for n be
Nat holds (A1
. n) is
Event of Sigma
proof
let n be
Nat;
(A1
. n)
in MySigmatau by
TT1;
then ex AJ be
Element of Sigma st AJ
= (A1
. n) & (for t be
Element of I holds (AJ
/\ { w2 where w2 be
Element of Omega : (tau
. w2)
<= t })
in (MyFunc
. t));
hence thesis;
end;
then
reconsider A1 as
SetSequence of Sigma by
PROB_1: 25;
set CA = (
Complement A1);
for n be
Nat holds (CA
. n) is
Event of Sigma
proof
let n be
Nat;
(A1
. n)
in MySigmatau by
TT1;
then
consider AJ be
Element of Sigma such that
AB1: AJ
= (A1
. n) & (for t be
Element of I holds (AJ
/\ { w2 where w2 be
Element of Omega : (tau
. w2)
<= t })
in (MyFunc
. t));
(A1
. n) is
Event of Sigma & Sigma is
compl-closed by
AB1;
then ((A1
. n)
` ) is
Event of Sigma;
hence thesis by
PROB_1:def 2;
end;
then
reconsider CA as
SetSequence of Sigma by
PROB_1: 25;
reconsider UCA = (
Union CA) as
Event of Sigma by
PROB_1: 26;
UCA
in MySigmatau by
QQ1;
hence thesis by
A1;
end;
K1: for t be
Element of I holds (Omega
/\ { w2 where w2 be
Element of Omega : (tau
. w2)
<= t })
in (MyFunc
. t)
proof
let t be
Element of I;
tau is MyFunc
-StoppingTime-like;
then tau
is_StoppingTime_wrt MyFunc;
then
N1: { w2 where w2 be
Element of Omega : (tau
. w2)
<= t }
in (MyFunc
. t);
reconsider MyFt = (MyFunc
. t) as
SigmaField of Omega by
KOLMOG01:def 2;
Omega is
Event of MyFt by
PROB_1: 5;
then (Omega
/\ { w2 where w2 be
Element of Omega : (tau
. w2)
<= t }) is
Event of MyFt by
PROB_1: 19,
N1;
hence thesis;
end;
Omega is
Element of Sigma & for t be
Element of I holds (Omega
/\ { w2 where w2 be
Element of Omega : (tau
. w2)
<= t })
in (MyFunc
. t) by
PROB_1: 5,
K1;
then Omega
in MySigmatau;
hence thesis by
A1,
A2;
end;
end
theorem ::
FINANCE5:9
for MyFunc be
Filtration of I, Sigma, k1,k2 be
StoppingTime_Func of MyFunc st k1
<= k2 holds (
Sigma_tau k1)
c= (
Sigma_tau k2)
proof
let MyFunc be
Filtration of I, Sigma;
let k1,k2 be
StoppingTime_Func of MyFunc;
assume
ASS0: k1
<= k2;
set Jsigk1 = (
Sigma_tau k1);
set Jsigk2 = (
Sigma_tau k2);
let x be
object;
assume x
in Jsigk1;
then
consider A be
Element of Sigma such that
Z1: x
= A & for t be
Element of I holds (A
/\ { w2 where w2 be
Element of Omega : (k1
. w2)
<= t })
in (MyFunc
. t);
reconsider x as
Element of Sigma by
Z1;
x
in { A where A be
Element of Sigma : for t be
Element of I holds (A
/\ { w2 where w2 be
Element of Omega : (k2
. w2)
<= t })
in (MyFunc
. t) }
proof
for t be
Element of I holds (x
/\ { w2 where w2 be
Element of Omega : (k2
. w2)
<= t })
in (MyFunc
. t)
proof
let t be
Element of I;
reconsider MyFt = (MyFunc
. t) as
SigmaField of Omega by
KOLMOG01:def 2;
set Imp0 = { w2 where w2 be
Element of Omega : (k2
. w2)
<= t };
set Imp1 = (x
/\ Imp0);
set Imp2 = ((x
/\ { w2 where w2 be
Element of Omega : (k1
. w2)
<= t })
/\ Imp0);
BU2: (x
/\ { w where w be
Element of Omega : (k1
. w)
<= t }) is
Event of MyFt by
Z1;
L1: Imp1
c= Imp2
proof
let y be
object;
assume
zw1: y
in Imp1;
then
ZW1: y
in x & y
in { w where w be
Element of Omega : (k2
. w)
<= t } by
XBOOLE_0:def 4;
then
consider w2 be
Element of Omega such that
ZW2: y
= w2 & (k2
. w2)
<= t;
(k1
. w2)
<= (k2
. w2) & (k2
. w2)
<= t by
ZW2,
ASS0;
then (k1
. w2)
<= t by
XXREAL_0: 2;
then y
in x & y
in { w where w be
Element of Omega : (k1
. w)
<= t } by
ZW2,
zw1,
XBOOLE_0:def 4;
then y
in (x
/\ { w where w be
Element of Omega : (k1
. w)
<= t }) by
XBOOLE_0:def 4;
hence thesis by
ZW1,
XBOOLE_0:def 4;
end;
P1: Imp1
= Imp2
proof
Imp2
c= Imp1
proof
let y be
object;
assume y
in Imp2;
then y
in (x
/\ { w where w be
Element of Omega : (k1
. w)
<= t }) & y
in Imp0 by
XBOOLE_0:def 4;
then y
in x & y
in { w where w be
Element of Omega : (k1
. w)
<= t } & y
in { w where w be
Element of Omega : (k2
. w)
<= t } by
XBOOLE_0:def 4;
hence thesis by
XBOOLE_0:def 4;
end;
hence thesis by
L1,
TARSKI: 2;
end;
Imp1 is
Event of MyFt
proof
k2
is_StoppingTime_wrt MyFunc by
Def1111;
then { w where w be
Element of Omega : (k2
. w)
<= t } is
Event of MyFt;
hence thesis by
P1,
BU2,
PROB_1: 19;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
definition
::
FINANCE5:def12
func
Ext_Family_of_halflines ->
Subset-Family of
ExtREAL equals the set of all
[.
-infty , r.] where r be
Real;
coherence
proof
the set of all
[.
-infty , r.] where r be
Real
c= (
bool
ExtREAL )
proof
let p be
object;
assume p
in the set of all
[.
-infty , r.] where r be
Real;
then
consider r be
Real such that
A1: p
=
[.
-infty , r.];
reconsider pp = p as
set by
A1;
pp
c=
ExtREAL by
A1,
MEMBERED: 2;
hence p
in (
bool
ExtREAL );
end;
hence thesis;
end;
end
definition
::
FINANCE5:def13
func
Ext_Borel_Sets ->
SigmaField of
ExtREAL equals (
sigma
Ext_Family_of_halflines );
correctness ;
end
theorem ::
FINANCE5:10
Th3: for k be
Real holds
].k,
+infty .] is
Element of
Ext_Borel_Sets &
[.
-infty , k.] is
Element of
Ext_Borel_Sets
proof
let k be
Real;
A3:
[.
-infty , k.]
in
Ext_Family_of_halflines ;
a2:
Ext_Family_of_halflines
c= (
sigma
Ext_Family_of_halflines ) by
PROB_1:def 9;
ExtREAL
in
Ext_Borel_Sets by
PROB_1: 5;
then (
ExtREAL
\
[.
-infty , k.])
in
Ext_Borel_Sets by
a2,
PROB_1: 6,
A3;
hence thesis by
Th2,
a2,
A3;
end;
definition
let b be
Real;
::
FINANCE5:def14
func
ext_half_open_sets (b) ->
SetSequence of
ExtREAL means
:
Def300: (it
.
0 )
=
].(b
- 1),
+infty .] & for n be
Nat holds (it
. (n
+ 1))
=
].(b
- (1
/ (n
+ 1))),
+infty .];
existence
proof
defpred
P[
set,
set,
set] means for x,y be
Subset of
ExtREAL , s be
Nat holds s
= $1 & x
= $2 & y
= $3 implies y
=
].(b
- (1
/ (s
+ 1))),
+infty .];
A1: for n be
Nat holds for x be
Subset of
ExtREAL holds ex y be
Subset of
ExtREAL st
P[n, x, y]
proof
let n be
Nat;
let x be
Subset of
ExtREAL ;
reconsider AA =
].(b
- (1
/ (n
+ 1))),
+infty .] as
Subset of
ExtREAL by
MEMBERED: 2;
take AA;
thus thesis;
end;
reconsider AB =
].(b
- 1),
+infty .] as
Subset of
ExtREAL by
MEMBERED: 2;
consider F be
SetSequence of
ExtREAL such that
A2: (F
.
0 )
= AB and
A3: for n be
Nat holds
P[n, (F
. n), (F
. (n
+ 1))] from
RECDEF_1:sch 2(
A1);
take F;
thus (F
.
0 )
=
].(b
- 1),
+infty .] by
A2;
let n be
Nat;
reconsider n as
Element of
NAT by
ORDINAL1:def 12;
P[n, (F
. n), (F
. (n
+ 1))] by
A3;
hence thesis;
end;
uniqueness
proof
let S1,S2 be
SetSequence of
ExtREAL such that
A4: (S1
.
0 )
=
].(b
- 1),
+infty .] & for n be
Nat holds (S1
. (n
+ 1))
=
].(b
- (1
/ (n
+ 1))),
+infty .] and
A5: (S2
.
0 )
=
].(b
- 1),
+infty .] & for n be
Nat holds (S2
. (n
+ 1))
=
].(b
- (1
/ (n
+ 1))),
+infty .];
defpred
P[
object] means (S1
. $1)
= (S2
. $1);
for n be
object holds n
in
NAT implies
P[n]
proof
let n be
object;
assume n
in
NAT ;
then
reconsider n as
Element of
NAT ;
A6:
P[
0 ] by
A4,
A5;
A7: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat;
assume (S1
. k)
= (S2
. k);
thus (S1
. (k
+ 1))
=
].(b
- (1
/ (k
+ 1))),
+infty .] by
A4
.= (S2
. (k
+ 1)) by
A5;
end;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
A6,
A7);
then (S1
. n)
= (S2
. n);
hence thesis;
end;
hence thesis;
end;
end
theorem ::
FINANCE5:11
Th50: for b be
Real holds (
Intersection (
ext_half_open_sets b)) is
Element of
Ext_Borel_Sets
proof
let b be
Real;
for n be
Nat holds ((
Complement (
ext_half_open_sets b))
. n) is
Element of
Ext_Borel_Sets
proof
let n be
Nat;
reconsider nn = n as
Element of
NAT by
ORDINAL1:def 12;
(((
ext_half_open_sets b)
. nn)
` ) is
Element of
Ext_Borel_Sets
proof
((
ext_half_open_sets b)
. n) is
Element of
Ext_Borel_Sets
proof
per cases by
NAT_1: 6;
suppose
A1: n
=
0 ;
((
ext_half_open_sets b)
.
0 )
=
].(b
- 1),
+infty .] by
Def300;
hence thesis by
A1,
Th3;
end;
suppose ex k be
Nat st n
= (k
+ 1);
then
consider k be
Nat such that
A2: n
= (k
+ 1);
reconsider k as
Element of
NAT by
ORDINAL1:def 12;
((
ext_half_open_sets b)
. (k
+ 1))
=
].(b
- (1
/ (k
+ 1))),
+infty .] by
Def300;
hence thesis by
A2,
Th3;
end;
end;
hence thesis by
PROB_1:def 1;
end;
hence thesis by
PROB_1:def 2;
end;
then (
Complement (
ext_half_open_sets b)) is
SetSequence of
Ext_Borel_Sets by
PROB_1: 25;
then (
Union (
Complement (
ext_half_open_sets b))) is
Element of
Ext_Borel_Sets by
PROB_1: 26;
hence thesis by
PROB_1:def 1;
end;
theorem ::
FINANCE5:12
Th60: for b be
Real holds (
Intersection (
ext_half_open_sets b))
=
[.b,
+infty .]
proof
let b be
Real;
for c be
object holds c
in (
Intersection (
ext_half_open_sets b)) iff c
in
[.b,
+infty .]
proof
let c be
object;
A1: not c
in
[.b,
+infty .] implies not c
in (
Intersection (
ext_half_open_sets b))
proof
assume
A2: not c
in
[.b,
+infty .];
per cases by
A2;
suppose not c
in
ExtREAL ;
hence thesis;
end;
suppose c
in
ExtREAL & not c
in
[.b,
+infty .];
then
reconsider c as
ExtReal;
W: c
<>
+infty
proof
reconsider b as
Element of
REAL by
XREAL_0:def 1;
not b
>
+infty by
XXREAL_0: 9;
hence thesis by
A2,
XXREAL_1: 1;
end;
per cases by
W,
XXREAL_0: 14;
suppose
S1: c
=
-infty ;
not c
in (
Intersection (
ext_half_open_sets b))
proof
c
in
].(b
- 1),
+infty .] iff (c
> (b
- 1) & c
<=
+infty ) by
XXREAL_1: 2;
then not c
in ((
ext_half_open_sets b)
.
0 ) by
Def300,
S1,
XXREAL_0: 5;
hence thesis by
PROB_1: 13;
end;
hence thesis;
end;
suppose c
in
REAL ;
then
reconsider c as
Element of
REAL ;
not for n be
Element of
NAT holds c
in ((
ext_half_open_sets b)
. n)
proof
set bc = (b
- c);
KK: bc
>
0
proof
c
>= b implies c
in
[.b,
+infty .]
proof
assume
ASS0: c
>= b;
reconsider c as
Element of
ExtREAL by
NUMBERS: 31;
b
<= c & c
<=
+infty by
XXREAL_0: 3,
ASS0;
then c
in { a where a be
Element of
ExtREAL : b
<= a & a
<=
+infty };
hence thesis by
XXREAL_1:def 1;
end;
then (c
- b)
<
0 by
XREAL_1: 49,
A2;
then ((
- 1)
* (c
+ (
- b)))
>
0 ;
hence thesis;
end;
consider n be
Nat such that
W1: (1
/ n)
< bc & n
>
0 by
KK,
PP;
reconsider spec = (1
/ n) as
Real;
F0: c
<= (b
- (1
/ n)) by
XREAL_1: 11,
W1;
n
< (n
+ 1) by
NAT_1: 13;
then ((n
+ 1)
" )
< (n
" ) by
W1,
XREAL_1: 88;
then (1
/ (n
+ 1))
< (n
" ) by
XCMPLX_1: 215;
then (1
/ (n
+ 1))
< (1
/ n) by
XCMPLX_1: 215;
then
f: (b
- (1
/ n))
< (b
- (1
/ (n
+ 1))) by
XREAL_1: 10;
f1: not c
in
].(b
- (1
/ (n
+ 1))),
+infty .]
proof
c
in
].(b
- (1
/ (n
+ 1))),
+infty .] implies c
>= (b
- (1
/ (n
+ 1)))
proof
assume c
in
].(b
- (1
/ (n
+ 1))),
+infty .];
then c
in { e where e be
Element of
ExtREAL : (b
- (1
/ (n
+ 1)))
< e & e
<=
+infty } by
XXREAL_1:def 3;
then
consider e be
Element of
ExtREAL such that
E1: e
= c & ((b
- (1
/ (n
+ 1)))
< e & e
<=
+infty );
thus thesis by
E1;
end;
hence thesis by
f,
F0,
XXREAL_0: 2;
end;
ex n be
Element of
NAT st not c
in ((
ext_half_open_sets b)
. n)
proof
take nn = (n
+ 1);
thus thesis by
ORDINAL1:def 12,
f1,
Def300;
end;
hence thesis;
end;
hence thesis by
PROB_1: 13;
end;
end;
end;
c
in
[.b,
+infty .] implies c
in (
Intersection (
ext_half_open_sets b))
proof
assume
A12: c
in
[.b,
+infty .];
for n be
Nat holds c
in ((
ext_half_open_sets b)
. n)
proof
let n be
Nat;
per cases ;
suppose n
=
0 ;
then
s2: ((
ext_half_open_sets b)
. n)
=
].(b
- 1),
+infty .] by
Def300;
[.b,
+infty .]
c=
].(b
- 1),
+infty .] by
XX;
hence thesis by
A12,
s2;
end;
suppose
S1: n
>
0 ;
then
reconsider nminus1 = (n
- 1) as
Nat by
NAT_1: 20;
s2: ((
ext_half_open_sets b)
. (nminus1
+ 1))
=
].(b
- (1
/ (nminus1
+ 1))),
+infty .] by
Def300;
[.b,
+infty .]
c=
].(b
- (1
/ n)),
+infty .] by
S1,
Lemma2;
hence thesis by
A12,
s2;
end;
end;
hence thesis by
PROB_1: 13;
end;
hence thesis by
A1;
end;
hence thesis;
end;
theorem ::
FINANCE5:13
Th70: for a,b be
Real holds
[.b, a.] is
Element of
Ext_Borel_Sets
proof
let a,b be
Real;
B1:
[.
-infty , a.] is
Element of
Ext_Borel_Sets by
Th3;
(
[.
-infty , a.]
/\
[.b,
+infty .]) is
Element of
Ext_Borel_Sets
proof
(
Intersection (
ext_half_open_sets b))
=
[.b,
+infty .] by
Th60;
then
[.b,
+infty .] is
Element of
Ext_Borel_Sets by
Th50;
hence thesis by
B1,
PROB_1: 19;
end;
hence thesis by
CrossTh;
end;
theorem ::
FINANCE5:14
Th71: for a be
Real holds
{a} is
Element of
Ext_Borel_Sets
proof
let a be
Real;
[.a, a.] is
Element of
Ext_Borel_Sets by
Th70;
hence thesis by
XXREAL_1: 17;
end;
theorem ::
FINANCE5:15
Th72: for r be
Real holds
[.r,
+infty .] is
Event of
Ext_Borel_Sets
proof
let r be
Real;
(
Intersection (
ext_half_open_sets r)) is
Element of
Ext_Borel_Sets by
Th50;
hence thesis by
Th60;
end;
definition
let b be
Real;
::
FINANCE5:def15
func
ext_right_closed_sets (b) ->
SetSequence of
ExtREAL means
:
Def3000: for n be
Nat holds (it
. n)
=
[.
-infty , (b
- n).];
existence
proof
deffunc
F(
Element of
NAT ) = (
In (
[.
-infty , (b
- $1).],(
bool
ExtREAL )));
consider F be
SetSequence of
ExtREAL such that
A3: for n be
Element of
NAT holds (F
. n)
=
F(n) from
FUNCT_2:sch 4;
take F;
let n be
Nat;
reconsider nn = n as
Element of
NAT by
ORDINAL1:def 12;
A1:
[.
-infty , (b
- nn).]
c=
ExtREAL by
MEMBERED: 2;
(F
. nn)
=
F(nn) by
A3
.=
[.
-infty , (b
- nn).] by
SUBSET_1:def 8,
A1;
hence thesis;
end;
uniqueness
proof
let S1,S2 be
SetSequence of
ExtREAL such that
A4: for n be
Nat holds (S1
. n)
=
[.
-infty , (b
- n).] and
A5: for n be
Nat holds (S2
. n)
=
[.
-infty , (b
- n).];
for n be
Element of
NAT holds (S1
. n)
= (S2
. n)
proof
let n be
Element of
NAT ;
(S1
. n)
=
[.
-infty , (b
- n).] by
A4
.= (S2
. n) by
A5;
hence thesis;
end;
hence thesis;
end;
end
theorem ::
FINANCE5:16
Th500: for b be
Real holds (
Intersection (
ext_right_closed_sets b)) is
Element of
Ext_Borel_Sets
proof
let b be
Real;
for n be
Nat holds ((
Complement (
ext_right_closed_sets b))
. n) is
Element of
Ext_Borel_Sets
proof
let n be
Nat;
reconsider nn = n as
Element of
NAT by
ORDINAL1:def 12;
(((
ext_right_closed_sets b)
. nn)
` ) is
Element of
Ext_Borel_Sets
proof
((
ext_right_closed_sets b)
. n) is
Element of
Ext_Borel_Sets
proof
((
ext_right_closed_sets b)
. n)
=
[.
-infty , (b
- n).] by
Def3000;
hence thesis by
Th3;
end;
hence thesis by
PROB_1:def 1;
end;
hence thesis by
PROB_1:def 2;
end;
then (
Complement (
ext_right_closed_sets b)) is
SetSequence of
Ext_Borel_Sets by
PROB_1: 25;
then (
Union (
Complement (
ext_right_closed_sets b))) is
Element of
Ext_Borel_Sets by
PROB_1: 26;
hence thesis by
PROB_1:def 1;
end;
theorem ::
FINANCE5:17
Th600: (
Intersection (
ext_right_closed_sets
0 ))
=
{
-infty }
proof
for c be
object holds c
in (
Intersection (
ext_right_closed_sets
0 )) iff c
in
{
-infty }
proof
let c be
object;
thus c
in (
Intersection (
ext_right_closed_sets
0 )) implies c
in
{
-infty }
proof
assume
Y: c
in (
Intersection (
ext_right_closed_sets
0 ));
assume not c
in
{
-infty };
then
WW: c
<>
-infty by
TARSKI:def 1;
reconsider c as
Element of
ExtREAL by
Y;
per cases by
XXREAL_0: 14,
WW;
suppose c
=
+infty ;
then not c
in
[.
-infty , (
0
-
0 ).] by
XXREAL_1: 1;
then not c
in ((
ext_right_closed_sets
0 )
. (
0
+
0 )) by
Def3000;
hence thesis by
Y,
PROB_1: 13;
end;
suppose c
in
REAL ;
then
reconsider c as
Element of
REAL ;
per cases ;
suppose c
>=
0 ;
then not c
in
[.
-infty , (
0
- (
0
+ 1)).] by
XXREAL_1: 1;
then not c
in ((
ext_right_closed_sets
0 )
. (
0
+ 1)) by
Def3000;
hence thesis by
Y,
PROB_1: 13;
end;
suppose
S1: c
<
0 ;
set finerg =
[\(((
- 1)
* c)
+ 1)/];
WQ: finerg
>
0
proof
((((
- 1)
* c)
+ 1)
- 1)
>
0 by
S1;
hence thesis by
INT_1:def 6;
end;
finerg is
Nat
proof
finerg
in
INT by
INT_1:def 2;
then
consider k be
Nat such that
ZZ: finerg
= k or finerg
= (
- k) by
INT_1:def 1;
thus thesis by
ZZ,
WQ;
end;
then
reconsider finerg as
Nat;
not c
in ((
ext_right_closed_sets
0 )
. (finerg
+ 1))
proof
z0: ((((
- 1)
* c)
+ 1)
- 1)
< finerg by
INT_1:def 6;
finerg
< (finerg
+ 1) by
XREAL_1: 29;
then (((
- 1)
* c)
+
0 )
< (finerg
+ 1) by
z0,
XXREAL_0: 2;
then (
- (((
- 1)
* c)
+
0 ))
> (
- (finerg
+ 1)) by
XREAL_1: 24;
then not c
in
[.
-infty , (
0
- (finerg
+ 1)).] by
XXREAL_1: 1;
hence thesis by
Def3000;
end;
hence thesis by
Y,
PROB_1: 13;
end;
end;
end;
assume
A12: c
in
{
-infty };
for n be
Nat holds c
in ((
ext_right_closed_sets
0 )
. n)
proof
let n be
Nat;
s2: ((
ext_right_closed_sets
0 )
. n)
=
[.
-infty , (
0
- n).] by
Def3000;
[.
-infty , (
0
- n).]
= (
{
-infty }
\/
].
-infty , (
0
- n).]) by
XXREAL_1: 421;
then
{
-infty }
c=
[.
-infty , (
0
- n).] by
XBOOLE_1: 7;
hence thesis by
A12,
s2;
end;
hence thesis by
PROB_1: 13;
end;
hence thesis;
end;
theorem ::
FINANCE5:18
{
-infty } is
Element of
Ext_Borel_Sets by
Th500,
Th600;
definition
let b be
Real;
::
FINANCE5:def16
func
ext_left_closed_sets (b) ->
SetSequence of
ExtREAL means
:
Def4000: for n be
Nat holds (it
. n)
=
[.(b
+ n),
+infty .];
existence
proof
deffunc
F(
Element of
NAT ) = (
In (
[.(b
+ $1),
+infty .],(
bool
ExtREAL )));
consider F be
SetSequence of
ExtREAL such that
A3: for n be
Element of
NAT holds (F
. n)
=
F(n) from
FUNCT_2:sch 4;
take F;
let n be
Nat;
reconsider nn = n as
Element of
NAT by
ORDINAL1:def 12;
A1:
[.(b
+ nn),
+infty .]
c=
ExtREAL by
MEMBERED: 2;
(F
. nn)
=
F(nn) by
A3
.=
[.(b
+ nn),
+infty .] by
SUBSET_1:def 8,
A1;
hence thesis;
end;
uniqueness
proof
let S1,S2 be
SetSequence of
ExtREAL such that
A4: for n be
Nat holds (S1
. n)
=
[.(b
+ n),
+infty .] and
A5: for n be
Nat holds (S2
. n)
=
[.(b
+ n),
+infty .];
for n be
Element of
NAT holds (S1
. n)
= (S2
. n)
proof
let n be
Element of
NAT ;
thus (S1
. n)
=
[.(b
+ n),
+infty .] by
A4
.= (S2
. n) by
A5;
end;
hence thesis;
end;
end
theorem ::
FINANCE5:19
Th5000: for b be
Real holds (
Intersection (
ext_left_closed_sets b)) is
Element of
Ext_Borel_Sets
proof
let b be
Real;
for n be
Nat holds ((
Complement (
ext_left_closed_sets b))
. n) is
Element of
Ext_Borel_Sets
proof
let n be
Nat;
reconsider nn = n as
Element of
NAT by
ORDINAL1:def 12;
(((
ext_left_closed_sets b)
. nn)
` ) is
Element of
Ext_Borel_Sets
proof
((
ext_left_closed_sets b)
. n) is
Element of
Ext_Borel_Sets
proof
((
ext_left_closed_sets b)
. n)
=
[.(b
+ n),
+infty .] by
Def4000;
hence thesis by
Th72;
end;
hence thesis by
PROB_1:def 1;
end;
hence thesis by
PROB_1:def 2;
end;
then (
Complement (
ext_left_closed_sets b)) is
SetSequence of
Ext_Borel_Sets by
PROB_1: 25;
then (
Union (
Complement (
ext_left_closed_sets b))) is
Element of
Ext_Borel_Sets by
PROB_1: 26;
hence thesis by
PROB_1:def 1;
end;
theorem ::
FINANCE5:20
Th6000: (
Intersection (
ext_left_closed_sets
0 ))
=
{
+infty }
proof
for c be
object holds c
in (
Intersection (
ext_left_closed_sets
0 )) iff c
in
{
+infty }
proof
let c be
object;
thus c
in (
Intersection (
ext_left_closed_sets
0 )) implies c
in
{
+infty }
proof
assume
Y: c
in (
Intersection (
ext_left_closed_sets
0 ));
assume not c
in
{
+infty };
then
WW: c
<>
+infty by
TARSKI:def 1;
reconsider c as
Element of
ExtREAL by
Y;
per cases by
XXREAL_0: 14,
WW;
suppose c
=
-infty ;
then not c
in
[.(
0
+
0 ),
+infty .] by
XXREAL_1: 1;
then not c
in ((
ext_left_closed_sets
0 )
.
0 ) by
Def4000;
hence thesis by
Y,
PROB_1: 13;
end;
suppose c
in
REAL ;
then
reconsider c as
Element of
REAL ;
per cases ;
suppose c
<
0 ;
then not c
in
[.(
0
+ 1),
+infty .] by
XXREAL_1: 1;
then not c
in ((
ext_left_closed_sets
0 )
. 1) by
Def4000;
hence thesis by
Y,
PROB_1: 13;
end;
suppose
S1: c
>=
0 ;
set finerg =
[\(c
+ (2
* 1))/];
WQ1: ((c
+ (2
* 1))
- 1)
< finerg by
INT_1:def 6;
WQ: finerg
>
0
proof
(c
+ ((1
+ 1)
- 1))
>
0 by
S1;
hence thesis by
WQ1;
end;
finerg is
Nat
proof
finerg
in
INT by
INT_1:def 2;
then
consider k be
Nat such that
ZZ: finerg
= k or finerg
= (
- k) by
INT_1:def 1;
thus thesis by
ZZ,
WQ;
end;
then
reconsider finerg as
Nat;
W0: ((c
+ (2
* 1))
- 1)
< finerg by
INT_1:def 6;
((c
+ (2
* 1))
- 1)
= (c
+ 1);
then
W1: c
< ((c
+ (2
* 1))
- 1) by
XREAL_1: 29;
W2: finerg
< (
0
+ (finerg
+ 1)) by
XREAL_1: 29;
c
< finerg by
W0,
W1,
XXREAL_0: 2;
then c
< (
0
+ (finerg
+ 1)) by
W2,
XXREAL_0: 2;
then not c
in
[.(
0
+ (finerg
+ 1)),
+infty .] by
XXREAL_1: 1;
then not c
in ((
ext_left_closed_sets
0 )
. (finerg
+ 1)) by
Def4000;
hence thesis by
Y,
PROB_1: 13;
end;
end;
end;
assume
A12: c
in
{
+infty };
for n be
Nat holds c
in ((
ext_left_closed_sets
0 )
. n)
proof
let n be
Nat;
s2: ((
ext_left_closed_sets
0 )
. n)
=
[.(
0
+ n),
+infty .] by
Def4000;
(
0
+ n)
<=
+infty by
XXREAL_0: 3;
then
{
+infty }
c=
[.(
0
+ n),
+infty .] by
ZFMISC_1: 31,
XXREAL_1: 1;
hence thesis by
A12,
s2;
end;
hence thesis by
PROB_1: 13;
end;
hence thesis;
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
reconsider Set1 =
ExtREAL as
Element of
Ext_Borel_Sets by
PROB_1: 23;
reconsider Set2 =
{
+infty } as
Element of
Ext_Borel_Sets by
Th5000,
Th6000;
reconsider Set3 =
{
-infty } as
Element of
Ext_Borel_Sets by
Th500,
Th600;
reconsider Set4 = (Set1
\ Set2) as
Element of
Ext_Borel_Sets ;
Set4
= (
[.
-infty ,
+infty .[
\/
].
+infty ,
+infty .]) by
XXREAL_1: 388,
XXREAL_1: 209
.=
[.
-infty ,
+infty .[;
then
PP: (Set4
\ Set3)
= (
[.
-infty ,
-infty .[
\/
].
-infty ,
+infty .[) by
XXREAL_1: 387
.=
].
-infty ,
+infty .[;
reconsider Set5 = (Set4
\ Set3) as
Element of
Ext_Borel_Sets ;
thus thesis by
XXREAL_1: 224,
PP;
end;
theorem ::
FINANCE5:23
Family_of_halflines
c=
Ext_Borel_Sets
proof
let x be
object;
assume x
in
Family_of_halflines ;
then
consider r be
Element of
REAL such that
A1: x
= (
halfline r);
reconsider Set1 =
[.
-infty , r.] as
Element of
Ext_Borel_Sets by
Th3;
reconsider Set2 =
{r} as
Element of
Ext_Borel_Sets by
Th71;
reconsider Set3 = (Set1
\ Set2) as
Element of
Ext_Borel_Sets ;
A3: Set3
=
[.
-infty , r.[ by
XXREAL_1: 135,
XXREAL_0: 5;
reconsider Set4 =
{
-infty } as
Element of
Ext_Borel_Sets by
Th500,
Th600;
reconsider Set5 = (Set3
\ Set4) as
Element of
Ext_Borel_Sets ;
Set5
=
].
-infty , r.[ by
XXREAL_1: 136,
A3,
XXREAL_0: 12;
hence thesis by
A1;
end;
definition
let A be
Element of
Ext_Borel_Sets ;
::
FINANCE5:def17
func
Ext_Borelsubsets_help (A) ->
Element of
Ext_Borel_Sets equals (A
/\
[.
0 ,
+infty .]);
coherence
proof
(
Intersection (
ext_half_open_sets
0 ))
=
[.
0 ,
+infty .] by
Th60;
then
[.
0 ,
+infty .] is
Element of
Ext_Borel_Sets by
Th50;
hence thesis by
PROB_1: 19;
end;
end
definition
::
FINANCE5:def18
func
ExtBorelsubsets ->
SigmaField of
[.
0 ,
+infty .] equals the set of all (
Ext_Borelsubsets_help A) where A be
Element of
Ext_Borel_Sets ;
coherence
proof
set BS = the set of all (
Ext_Borelsubsets_help A) where A be
Element of
Ext_Borel_Sets ;
reconsider I =
[.
0 ,
+infty .] as
Subset of
ExtREAL by
MEMBERED: 2;
BS is non
empty
Subset-Family of I
proof
reconsider RE =
ExtREAL as
Element of
Ext_Borel_Sets by
PROB_1: 5;
d1: (
Ext_Borelsubsets_help RE)
in BS;
BS
c= (
bool I)
proof
let x be
object;
assume x
in BS;
then
consider A be
Element of
Ext_Borel_Sets such that
D1: x
= (
Ext_Borelsubsets_help A);
reconsider x as
set by
D1;
x
c= I by
D1,
XBOOLE_0:def 4;
hence thesis;
end;
hence thesis by
d1;
end;
then
reconsider BS as non
empty
Subset-Family of I;
A1: BS is
compl-closed
proof
let A be
Subset of I;
assume A
in BS;
then
consider A2 be
Element of
Ext_Borel_Sets such that
AF1: A
= (
Ext_Borelsubsets_help A2);
F2: (I
\ A)
= (I
\ A2) by
AF1,
XBOOLE_1: 47
.= ((A2
` )
/\ I) by
SUBSET_1: 13;
reconsider CA2 = (A2
` ) as
Element of
Ext_Borel_Sets by
PROB_1: 20;
(CA2
/\ I)
= (
Ext_Borelsubsets_help CA2);
hence thesis by
F2;
end;
BS is
sigma-multiplicative
proof
let A1 be
SetSequence of I;
assume
G1: (
rng A1)
c= BS;
TT1: for n be
Nat holds (A1
. n)
in BS & (ex A2 be
Element of
Ext_Borel_Sets st (A1
. n)
= (
Ext_Borelsubsets_help A2))
proof
let n be
Nat;
reconsider n as
Element of
NAT by
ORDINAL1:def 12;
(A1
. n)
in (
rng A1) by
FUNCT_2: 4;
then (A1
. n)
in BS by
G1;
hence thesis;
end;
(
rng A1)
c= (
bool
ExtREAL )
proof
let x be
object;
assume
d1: x
in (
rng A1);
(
bool I)
c= (
bool
ExtREAL ) by
ZFMISC_1: 67;
hence thesis by
d1;
end;
then
reconsider A10 = A1 as
SetSequence of
ExtREAL by
FUNCT_2: 6;
for n be
Nat holds (A10
. n) is
Event of
Ext_Borel_Sets
proof
let n be
Nat;
ex A2 be
Element of
Ext_Borel_Sets st (A10
. n)
= (
Ext_Borelsubsets_help A2) by
TT1;
hence thesis;
end;
then
reconsider A10 as
SetSequence of
Ext_Borel_Sets by
PROB_1: 25;
set UA1 = (
Union (
Complement A10));
for n be
Nat holds ((
Complement A10)
. n) is
Event of
Ext_Borel_Sets
proof
let n be
Nat;
consider A2 be
Element of
Ext_Borel_Sets such that
P1: (A10
. n)
= (
Ext_Borelsubsets_help A2) by
TT1;
reconsider A1n = (A10
. n) as
Element of
Ext_Borel_Sets by
P1;
(A1n
` ) is
Element of
Ext_Borel_Sets by
PROB_1: 20;
hence thesis by
PROB_1:def 2;
end;
then (
Complement A10) is
SetSequence of
Ext_Borel_Sets by
PROB_1: 25;
then
reconsider UA1 as
Event of
Ext_Borel_Sets by
PROB_1: 26;
k1: (UA1
` ) is
Event of
Ext_Borel_Sets by
PROB_1: 20;
reconsider IA1 = (
Intersection A10) as
Element of
Ext_Borel_Sets by
k1;
for x be
object holds x
in IA1 iff x
in (
Ext_Borelsubsets_help IA1)
proof
let x be
object;
thus x
in IA1 implies x
in (
Ext_Borelsubsets_help IA1)
proof
assume x
in IA1;
then x
in IA1 & x
in (A1
.
0 ) by
PROB_1: 13;
hence thesis by
XBOOLE_0:def 4;
end;
thus thesis by
XBOOLE_0:def 4;
end;
then
s0: IA1
= (
Ext_Borelsubsets_help IA1) by
TARSKI: 2;
(
Intersection A10)
= (
Intersection A1)
proof
for x be
object holds x
in (
Intersection A10) iff x
in (
Intersection A1)
proof
let x be
object;
x
in (
Intersection A10) iff for n be
Nat holds x
in (A10
. n) by
PROB_1: 13;
then x
in (
Intersection A10) iff for n be
Nat holds x
in (A1
. n);
hence thesis by
PROB_1: 13;
end;
hence thesis;
end;
hence thesis by
s0;
end;
hence thesis by
A1;
end;
end
definition
let Omega, Sigma;
let MyFunc be
Function;
let S be non
empty
ext-real-membered
set;
let k be
random_variable of Sigma,
ExtBorelsubsets ;
::
FINANCE5:def19
pred k
is_StoppingTime_wrt MyFunc,S means for t be
Element of S holds { w where w be
Element of Omega : (k
. w)
<= t }
in (MyFunc
. t);
end
theorem ::
FINANCE5:24
Th1: for MyFunc be
Filtration of S, Sigma, t2 be
Element of
[.
0 ,
+infty .] holds ex q be
random_variable of Sigma,
ExtBorelsubsets st q
= (Omega
--> t2) & q
is_StoppingTime_wrt (MyFunc,S)
proof
let MyFunc be
Filtration of S, Sigma;
let t2 be
Element of
[.
0 ,
+infty .];
Fin1: for t be
Element of S holds { w where w be
Element of Omega : ((Omega
--> t2)
. w)
<= t }
in (MyFunc
. t)
proof
let t be
Element of S;
reconsider MyFt = (MyFunc
. t) as
SigmaField of Omega by
KOLMOG01:def 2;
set R = { w where w be
Element of Omega : ((Omega
--> t2)
. w)
<= t };
H1: for x be
object st x
in R holds x
in Omega
proof
let x be
object;
assume x
in R;
then ex w3 be
Element of Omega st w3
= x & ((Omega
--> t2)
. w3)
<= t;
hence thesis;
end;
per cases ;
suppose
S1: t2
<= t;
R
= Omega
proof
for x be
object st x
in Omega holds x
in R
proof
let x be
object;
assume x
in Omega;
then
reconsider x as
Element of Omega;
((Omega
--> t2)
. x)
= t2 by
FUNCOP_1: 7;
hence thesis by
S1;
end;
hence thesis by
H1,
TARSKI: 2;
end;
then R
in MyFt by
PROB_1: 5;
hence thesis;
end;
suppose
S1: t2
> t;
R
c=
{}
proof
let x be
object;
assume x
in R;
then ex w3 be
Element of Omega st w3
= x & ((Omega
--> t2)
. w3)
<= t;
hence thesis by
S1,
FUNCOP_1: 7;
end;
then R
=
{} ;
then R
in MyFt by
PROB_1: 4;
hence thesis;
end;
end;
set OC = (Omega
--> t2);
OC is
random_variable of Sigma,
ExtBorelsubsets by
FINANCE3: 10;
then
reconsider OC as
random_variable of Sigma,
ExtBorelsubsets ;
OC
is_StoppingTime_wrt (MyFunc,S) by
Fin1;
hence thesis;
end;
definition
let Omega, Sigma, S;
let Filt be
Filtration of S, Sigma;
let k be
random_variable of Sigma,
ExtBorelsubsets ;
::
FINANCE5:def20
attr k is Filt
-StoppingTime-like means
:
Def11111: k
is_StoppingTime_wrt (Filt,S);
end
registration
let Omega, Sigma, S;
let MyFunc be
Filtration of S, Sigma;
cluster MyFunc
-StoppingTime-like for
random_variable of Sigma,
ExtBorelsubsets ;
existence
proof
set t2 = the
Element of
[.
0 ,
+infty .];
ex q be
random_variable of Sigma,
ExtBorelsubsets st q
= (Omega
--> t2) & q
is_StoppingTime_wrt (MyFunc,S) by
Th1;
hence thesis by
Def11111;
end;
end
definition
let Omega, Sigma, S;
let MyFunc be
Filtration of S, Sigma;
mode
StoppingTime_Func of Sigma,MyFunc is MyFunc
-StoppingTime-like
random_variable of Sigma,
ExtBorelsubsets ;
end
definition
let Omega, Sigma, S;
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;
let n be
Nat;
::
FINANCE5:def21
func
Sigma_tauhelp2 (MyFunc,tau,A1,n,t) ->
Element of (
El_Filtration (t,MyFunc)) equals
:
Def8869: (((
Complement A1)
. n)
/\ { w where w be
Element of Omega : (tau
. w)
<= t });
correctness
proof
set MySigmatau = { A where A be
Element of Sigma : for t2 be
Element of S holds (A
/\ { w where w be
Element of Omega : (tau
. w)
<= t2 })
in (MyFunc
. t2) };
(A1
. n)
in (
rng A1) by
FUNCT_2: 4,
ORDINAL1:def 12;
then (A1
. n)
in MySigmatau by
LOC1;
then
consider B be
Element of Sigma such that
GW1: (A1
. n)
= B & for t2 be
Element of S holds (B
/\ { w where w be
Element of Omega : (tau
. w)
<= t2 })
in (MyFunc
. t2);
reconsider A1n = (A1
. n) as
Element of Sigma by
GW1;
GW2: for t be
Element of S holds (((A1
. n)
` )
/\ { w where w be
Element of Omega : (tau
. w)
<= t })
in (MyFunc
. t)
proof
let t be
Element of S;
reconsider MyFt2 = (MyFunc
. t) as
SigmaField of Omega by
KOLMOG01:def 2;
set F = { w where w be
Element of Omega : (tau
. w)
<= t };
J1: F
c= Omega
proof
let b be
object;
assume b
in F;
then
consider ww be
Element of Omega such that
L1: ww
= b & (tau
. ww)
<= t;
thus thesis by
L1;
end;
E1: (F
\ ((A1
. n)
/\ F))
= (F
\ (A1
. n)) by
XBOOLE_1: 47
.= (F
/\ ((A1
. n)
` )) by
J1,
SUBSET_1: 13;
W2: ((A1
. n)
/\ F) is
Event of MyFt2 by
GW1;
tau
is_StoppingTime_wrt (MyFunc,S) by
Def11111;
then F is
Event of MyFt2;
then (F
\ ((A1
. n)
/\ F)) is
Event of MyFt2 by
W2,
PROB_1: 24;
hence thesis by
E1;
end;
((A1
. n)
` )
= ((
Complement A1)
. n) by
PROB_1:def 2;
hence thesis by
GW2;
end;
end
definition
let Omega, Sigma, S;
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;
::
FINANCE5:def22
func
Sigma_tauhelp3 (MyFunc,tau,A1,t) ->
SetSequence of (
El_Filtration (t,MyFunc)) means
:
Def8868: for n be
Nat holds (it
. n)
= (
Sigma_tauhelp2 (MyFunc,tau,A1,n,t));
existence
proof
deffunc
U(
Nat) = (
Sigma_tauhelp2 (MyFunc,tau,A1,$1,t));
consider f be
sequence of (
El_Filtration (t,MyFunc)) such that
A1: for d be
Element of
NAT holds (f
. d)
=
U(d) from
FUNCT_2:sch 4;
reconsider f as
SetSequence of (
El_Filtration (t,MyFunc)) by
PROB_4: 2;
take f;
let n be
Nat;
n
in
NAT by
ORDINAL1:def 12;
hence thesis by
A1;
end;
uniqueness
proof
let f1,f2 be
SetSequence of (
El_Filtration (t,MyFunc));
assume that
A1: for d be
Nat holds (f1
. d)
= (
Sigma_tauhelp2 (MyFunc,tau,A1,d,t)) and
A2: for d be
Nat holds (f2
. d)
= (
Sigma_tauhelp2 (MyFunc,tau,A1,d,t));
for d be
Nat holds (f1
. d)
= (f2
. d)
proof
let d be
Nat;
(f1
. d)
= (
Sigma_tauhelp2 (MyFunc,tau,A1,d,t)) by
A1;
hence thesis by
A2;
end;
hence thesis;
end;
end
definition
let Omega, Sigma, S;
let MyFunc be
Filtration of S, Sigma;
let tau be
StoppingTime_Func of Sigma, MyFunc;
::
FINANCE5:def23
func
Sigma_tau (MyFunc,tau) ->
SigmaField of Omega equals { A where A be
Element of Sigma : for t be
Element of S holds (A
/\ { w where w be
Element of Omega : (tau
. w)
<= t })
in (MyFunc
. t) };
coherence
proof
set MySigmatau = { A where A be
Element of Sigma : for t be
Element of S holds (A
/\ { w where w be
Element of Omega : (tau
. w)
<= t })
in (MyFunc
. t) };
MySigmatau
c= (
bool Omega)
proof
let x be
object;
assume x
in MySigmatau;
then ex A be
Element of Sigma st x
= A & for t be
Element of S holds (A
/\ { w where w be
Element of Omega : (tau
. w)
<= t })
in (MyFunc
. t);
hence thesis;
end;
then
reconsider MySigmatau as
Subset-Family of Omega;
A1: MySigmatau is
compl-closed
proof
let A be
Subset of Omega;
assume A
in MySigmatau;
then
consider B be
Element of Sigma such that
GW1: A
= B & for t be
Element of S holds (B
/\ { w where w be
Element of Omega : (tau
. w)
<= t })
in (MyFunc
. t);
reconsider A as
Element of Sigma by
GW1;
GW2: for t be
Element of S holds ((A
` )
/\ { w where w be
Element of Omega : (tau
. w)
<= t })
in (MyFunc
. t)
proof
let t be
Element of S;
set F = { w where w be
Element of Omega : (tau
. w)
<= t };
reconsider MyFt2 = (MyFunc
. t) as
SigmaField of Omega by
KOLMOG01:def 2;
LL: F
c= Omega
proof
let b be
object;
assume b
in F;
then ex ww be
Element of Omega st ww
= b & (tau
. ww)
<= t;
hence thesis;
end;
E1: (F
\ (A
/\ F))
= (F
\ A) by
XBOOLE_1: 47
.= (F
/\ (A
` )) by
SUBSET_1: 13,
LL;
W2: (A
/\ F) is
Event of MyFt2 by
GW1;
tau
is_StoppingTime_wrt (MyFunc,S) by
Def11111;
then F is
Event of MyFt2;
then (F
\ (A
/\ F)) is
Event of MyFt2 by
W2,
PROB_1: 24;
hence thesis by
E1;
end;
Omega
in Sigma & A
in Sigma by
PROB_1: 5;
then (Omega
\ A)
in Sigma by
PROB_1: 6;
hence thesis by
GW2;
end;
A2: MySigmatau is
sigma-multiplicative
proof
let A1 be
SetSequence of Omega;
assume
ASSJ: (
rng A1)
c= MySigmatau;
TT1: for n be
Nat holds (A1
. n)
in MySigmatau
proof
let n be
Nat;
(A1
. n)
in (
rng A1) by
FUNCT_2: 4,
ORDINAL1:def 12;
hence thesis by
ASSJ;
end;
for n be
Nat holds (A1
. n) is
Event of Sigma
proof
let n be
Nat;
(A1
. n)
in MySigmatau by
TT1;
then ex AJ be
Element of Sigma st AJ
= (A1
. n) & (for t be
Element of S holds (AJ
/\ { w2 where w2 be
Element of Omega : (tau
. w2)
<= t })
in (MyFunc
. t));
hence thesis;
end;
then
reconsider A1 as
SetSequence of Sigma by
PROB_1: 25;
set CA = (
Complement A1);
for n be
Nat holds (CA
. n) is
Event of Sigma
proof
let n be
Nat;
(A1
. n)
in MySigmatau by
TT1;
then ex AJ be
Element of Sigma st AJ
= (A1
. n) & (for t be
Element of S holds (AJ
/\ { w2 where w2 be
Element of Omega : (tau
. w2)
<= t })
in (MyFunc
. t));
then (A1
. n) is
Event of Sigma & Sigma is
compl-closed;
then ((A1
. n)
` ) is
Event of Sigma;
hence thesis by
PROB_1:def 2;
end;
then
reconsider CA as
SetSequence of Sigma by
PROB_1: 25;
QQ1: for t be
Element of S holds ((
Union (
Complement A1))
/\ { w where w be
Element of Omega : (tau
. w)
<= t })
in (MyFunc
. t)
proof
let t be
Element of S;
set R = { w where w be
Element of Omega : (tau
. w)
<= t };
(
Union (
Sigma_tauhelp3 (MyFunc,tau,A1,t)))
= ((
Union (
Complement A1))
/\ R)
proof
thus (
Union (
Sigma_tauhelp3 (MyFunc,tau,A1,t)))
c= ((
Union (
Complement A1))
/\ R)
proof
let x be
object;
assume x
in (
Union (
Sigma_tauhelp3 (MyFunc,tau,A1,t)));
then
consider n be
Nat such that
V1: x
in ((
Sigma_tauhelp3 (MyFunc,tau,A1,t))
. n) by
PROB_1: 12;
x
in (
Sigma_tauhelp2 (MyFunc,tau,A1,n,t)) by
V1,
Def8868;
then x
in (((
Complement A1)
. n)
/\ { w where w be
Element of Omega : (tau
. w)
<= t }) by
ASSJ,
Def8869;
then
ZWJ1: x
in ((
Complement A1)
. n) & x
in { w where w be
Element of Omega : (tau
. w)
<= t } by
XBOOLE_0:def 4;
then x
in (
Union (
Complement A1)) by
PROB_1: 12;
hence thesis by
XBOOLE_0:def 4,
ZWJ1;
end;
let x be
object;
assume x
in ((
Union (
Complement A1))
/\ R);
then
ZWJ1: x
in (
Union (
Complement A1)) & x
in R by
XBOOLE_0:def 4;
then
consider n be
Nat such that
ZWJ2: x
in ((
Complement A1)
. n) by
PROB_1: 12;
x
in (((
Complement A1)
. n)
/\ R) by
XBOOLE_0:def 4,
ZWJ1,
ZWJ2;
then x
in (
Sigma_tauhelp2 (MyFunc,tau,A1,n,t)) by
ASSJ,
Def8869;
then x
in ((
Sigma_tauhelp3 (MyFunc,tau,A1,t))
. n) by
Def8868;
hence thesis by
PROB_1: 12;
end;
hence thesis by
PROB_1: 17;
end;
set CA = (
Complement A1);
for n be
Nat holds (CA
. n) is
Event of Sigma
proof
let n be
Nat;
(A1
. n)
in MySigmatau by
TT1;
then
consider AJ be
Element of Sigma such that
AB1: AJ
= (A1
. n) & (for t be
Element of S holds (AJ
/\ { w2 where w2 be
Element of Omega : (tau
. w2)
<= t })
in (MyFunc
. t));
(A1
. n) is
Event of Sigma & Sigma is
compl-closed by
AB1;
then ((A1
. n)
` ) is
Event of Sigma;
hence thesis by
PROB_1:def 2;
end;
then
reconsider CA as
SetSequence of Sigma by
PROB_1: 25;
reconsider UCA = (
Union CA) as
Event of Sigma by
PROB_1: 26;
UCA
in MySigmatau by
QQ1;
hence thesis by
A1;
end;
K0: for t be
Element of S holds { w2 where w2 be
Element of Omega : (tau
. w2)
<= t }
in (MyFunc
. t)
proof
let t be
Element of S;
tau is MyFunc
-StoppingTime-like;
then tau
is_StoppingTime_wrt (MyFunc,S);
hence thesis;
end;
K1: for t be
Element of S holds (Omega
/\ { w2 where w2 be
Element of Omega : (tau
. w2)
<= t })
in (MyFunc
. t)
proof
let t be
Element of S;
N1: { w2 where w2 be
Element of Omega : (tau
. w2)
<= t }
in (MyFunc
. t) by
K0;
reconsider MyFt = (MyFunc
. t) as
SigmaField of Omega by
KOLMOG01:def 2;
Omega is
Event of MyFt by
PROB_1: 5;
then (Omega
/\ { w2 where w2 be
Element of Omega : (tau
. w2)
<= t }) is
Event of MyFt by
PROB_1: 19,
N1;
hence thesis;
end;
Omega is
Element of Sigma & for t be
Element of S holds (Omega
/\ { w2 where w2 be
Element of Omega : (tau
. w2)
<= t })
in (MyFunc
. t) by
PROB_1: 5,
K1;
then Omega
in MySigmatau;
hence thesis by
A1,
A2;
end;
end
theorem ::
FINANCE5:25
for MyFunc be
Filtration of S, Sigma, k1,k2 be
StoppingTime_Func of Sigma, MyFunc st k1
<= k2 holds (
Sigma_tau (MyFunc,k1))
c= (
Sigma_tau (MyFunc,k2))
proof
let MyFunc be
Filtration of S, Sigma;
let k1,k2 be
StoppingTime_Func of Sigma, MyFunc;
assume
ASS0: k1
<= k2;
let x be
object;
assume x
in (
Sigma_tau (MyFunc,k1));
then
consider A be
Element of Sigma such that
Z1: x
= A & for t be
Element of S holds (A
/\ { w2 where w2 be
Element of Omega : (k1
. w2)
<= t })
in (MyFunc
. t);
reconsider x as
Element of Sigma by
Z1;
for t be
Element of S holds (x
/\ { w2 where w2 be
Element of Omega : (k2
. w2)
<= t })
in (MyFunc
. t)
proof
let t be
Element of S;
reconsider MyFt = (MyFunc
. t) as
SigmaField of Omega by
KOLMOG01:def 2;
set Imp0 = { w2 where w2 be
Element of Omega : (k2
. w2)
<= t };
set Imp1 = (x
/\ Imp0);
set Imp2 = ((x
/\ { w2 where w2 be
Element of Omega : (k1
. w2)
<= t })
/\ Imp0);
BU2: (x
/\ { w where w be
Element of Omega : (k1
. w)
<= t }) is
Event of MyFt by
Z1;
P1: Imp1
= Imp2
proof
thus Imp1
c= Imp2
proof
let y be
object;
assume
zw1: y
in Imp1;
then
ZW1: y
in x & y
in { w where w be
Element of Omega : (k2
. w)
<= t } by
XBOOLE_0:def 4;
then
consider w2 be
Element of Omega such that
ZW2: y
= w2 & (k2
. w2)
<= t;
(k1
. w2)
<= (k2
. w2) & (k2
. w2)
<= t by
ZW2,
ASS0;
then (k1
. w2)
<= t by
XXREAL_0: 2;
then y
in x & y
in { w where w be
Element of Omega : (k1
. w)
<= t } by
ZW2,
zw1,
XBOOLE_0:def 4;
then y
in (x
/\ { w where w be
Element of Omega : (k1
. w)
<= t }) by
XBOOLE_0:def 4;
hence thesis by
ZW1,
XBOOLE_0:def 4;
end;
let y be
object;
assume y
in Imp2;
then y
in (x
/\ { w where w be
Element of Omega : (k1
. w)
<= t }) & y
in Imp0 by
XBOOLE_0:def 4;
then y
in x & y
in { w where w be
Element of Omega : (k1
. w)
<= t } & y
in { w where w be
Element of Omega : (k2
. w)
<= t } by
XBOOLE_0:def 4;
hence thesis by
XBOOLE_0:def 4;
end;
Imp1 is
Event of MyFt
proof
k2
is_StoppingTime_wrt (MyFunc,S) by
Def11111;
then { w where w be
Element of Omega : (k2
. w)
<= t } is
Event of MyFt;
hence thesis by
P1,
BU2,
PROB_1: 19;
end;
hence thesis;
end;
hence thesis;
end;