finance3.miz
begin
Lemacik: for a,b,c be
set st (a
= 1 or a
= 2 or a
= 3 or a
= 4) & (b
= 1 or b
= 2 or b
= 3 or b
= 4) & (c
= 1 or c
= 2 or c
= 3 or c
= 4) holds
{a, b, c}
c=
{1, 2, 3, 4}
proof
let a,b,c be
set;
assume
A1: (a
= 1 or a
= 2 or a
= 3 or a
= 4) & (b
= 1 or b
= 2 or b
= 3 or b
= 4) & (c
= 1 or c
= 2 or c
= 3 or c
= 4);
for x be
object st x
in
{a, b, c} holds x
in
{1, 2, 3, 4}
proof
let x be
object;
assume x
in
{a, b, c};
then x
= a or x
= b or x
= c by
ENUMSET1:def 1;
hence thesis by
ENUMSET1:def 2,
A1;
end;
hence thesis;
end;
Lemacik2: for a,b be
set st (a
= 1 or a
= 2 or a
= 3 or a
= 4) & (b
= 1 or b
= 2 or b
= 3 or b
= 4) holds
{a, b}
c=
{1, 2, 3, 4}
proof
let a,b be
set;
assume
A1: (a
= 1 or a
= 2 or a
= 3 or a
= 4) & (b
= 1 or b
= 2 or b
= 3 or b
= 4);
for x be
object st x
in
{a, b} holds x
in
{1, 2, 3, 4}
proof
let x be
object;
assume x
in
{a, b};
then x
= a or x
= b by
TARSKI:def 2;
hence thesis by
ENUMSET1:def 2,
A1;
end;
hence thesis;
end;
Lemacik3: for a be
set st a
= 1 or a
= 2 or a
= 3 or a
= 4 holds
{a}
c=
{1, 2, 3, 4}
proof
let a be
set;
assume
A1: a
= 1 or a
= 2 or a
= 3 or a
= 4;
for x be
object st x
in
{a} holds x
in
{1, 2, 3, 4}
proof
let x be
object;
assume x
in
{a};
then x
= a by
TARSKI:def 1;
hence thesis by
ENUMSET1:def 2,
A1;
end;
hence thesis;
end;
The1: for A1 be
SetSequence of
{1, 2, 3, 4} st (ex n be
Nat st (A1
. n)
=
{} ) holds (
Intersection A1)
=
{}
proof
let A1 be
SetSequence of
{1, 2, 3, 4};
given n be
Nat such that
AB: (A1
. n)
=
{} ;
assume (
Intersection A1)
<>
{} ;
then
consider x be
object such that
AA: x
in (
Intersection A1) by
XBOOLE_0:def 1;
thus thesis by
AB,
PROB_1: 13,
AA;
end;
EnLm1:
{1}
c=
{1, 2, 3, 4} by
Lemacik3;
EnLm2:
{2}
c=
{1, 2, 3, 4} by
Lemacik3;
EnLm3:
{3}
c=
{1, 2, 3, 4} by
Lemacik3;
EnLm4:
{4}
c=
{1, 2, 3, 4} by
Lemacik3;
theorem ::
FINANCE3:1
for a,b be
object st a
<> b holds
{a}
c<
{a, b} by
ZFMISC_1: 7,
ZFMISC_1: 20;
Lm1:
{3, 4}
c=
{1, 2, 3, 4} by
Lemacik2;
Lm2:
{1, 2}
c=
{1, 2, 3, 4} by
Lemacik2;
Lm3: (
{1, 2}
/\
{3, 4})
=
{}
proof
(
{1, 2}
/\
{3, 4})
c=
{}
proof
let x be
object;
x
in (
{1, 2}
/\
{3, 4}) iff (x
in
{1, 2} & x
in
{3, 4}) by
XBOOLE_0:def 4;
then x
in (
{1, 2}
/\
{3, 4}) iff ((x
= 1 or x
= 2) & (x
= 3 or x
= 4)) by
TARSKI:def 2;
hence thesis;
end;
hence thesis;
end;
Lem1: (
{1, 2, 3, 4}
\
{1, 2})
=
{3, 4}
proof
for x be
object holds x
in (
{1, 2, 3, 4}
\
{1, 2}) iff x
in
{3, 4}
proof
let x be
object;
thus x
in (
{1, 2, 3, 4}
\
{1, 2}) implies x
in
{3, 4}
proof
assume x
in (
{1, 2, 3, 4}
\
{1, 2});
then x
in
{1, 2, 3, 4} & not x
in
{1, 2} by
XBOOLE_0:def 5;
then (x
= 1 or x
= 2 or x
= 3 or x
= 4) & (x
<> 1 & x
<> 2) by
TARSKI:def 2,
ENUMSET1:def 2;
hence thesis by
TARSKI:def 2;
end;
assume x
in
{3, 4};
then x
= 3 or x
= 4 by
TARSKI:def 2;
then x
in
{1, 2, 3, 4} & not x
in
{1, 2} by
TARSKI:def 2,
ENUMSET1:def 2;
hence thesis by
XBOOLE_0:def 5;
end;
hence thesis by
TARSKI: 2;
end;
Lem2: (
{1, 2, 3, 4}
\
{3, 4})
=
{1, 2}
proof
for x be
object holds x
in (
{1, 2, 3, 4}
\
{3, 4}) iff x
in
{1, 2}
proof
let x be
object;
thus x
in (
{1, 2, 3, 4}
\
{3, 4}) implies x
in
{1, 2}
proof
assume x
in (
{1, 2, 3, 4}
\
{3, 4});
then x
in
{1, 2, 3, 4} & not x
in
{3, 4} by
XBOOLE_0:def 5;
then (x
= 1 or x
= 2 or x
= 3 or x
= 4) & (x
<> 3 & x
<> 4) by
TARSKI:def 2,
ENUMSET1:def 2;
hence thesis by
TARSKI:def 2;
end;
assume x
in
{1, 2};
then x
= 1 or x
= 2 by
TARSKI:def 2;
then x
in
{1, 2, 3, 4} & not x
in
{3, 4} by
TARSKI:def 2,
ENUMSET1:def 2;
hence thesis by
XBOOLE_0:def 5;
end;
hence thesis by
TARSKI: 2;
end;
B13:
{1, 3}
in (
bool
{1, 2, 3, 4})
proof
{1, 3}
c=
{1, 2, 3, 4} by
Lemacik2;
hence thesis;
end;
B14:
{1, 4}
in (
bool
{1, 2, 3, 4})
proof
{1, 4}
c=
{1, 2, 3, 4} by
Lemacik2;
hence thesis;
end;
B124:
{1, 2, 4}
in (
bool
{1, 2, 3, 4})
proof
{1, 2, 4}
c=
{1, 2, 3, 4} by
Lemacik;
hence thesis;
end;
B134:
{1, 3, 4}
in (
bool
{1, 2, 3, 4})
proof
{1, 3, 4}
c=
{1, 2, 3, 4} by
Lemacik;
hence thesis;
end;
B234:
{2, 3, 4}
in (
bool
{1, 2, 3, 4})
proof
{2, 3, 4}
c=
{1, 2, 3, 4} by
Lemacik;
hence thesis;
end;
B123:
{1, 2, 3}
in (
bool
{1, 2, 3, 4})
proof
{1, 2, 3}
c=
{1, 2, 3, 4} by
Lemacik;
hence thesis;
end;
B23:
{2, 3}
in (
bool
{1, 2, 3, 4})
proof
{2, 3}
c=
{1, 2, 3, 4} by
Lemacik2;
hence thesis;
end;
B24:
{2, 4}
in (
bool
{1, 2, 3, 4})
proof
{2, 4}
c=
{1, 2, 3, 4} by
Lemacik2;
hence thesis;
end;
B25:
{1, 2}
in (
bool
{1, 2, 3, 4})
proof
{1, 2}
c=
{1, 2, 3, 4} by
Lemacik2;
hence thesis;
end;
B26:
{3, 4}
in (
bool
{1, 2, 3, 4})
proof
{3, 4}
c=
{1, 2, 3, 4} by
Lemacik2;
hence thesis;
end;
WW1:
{1, 2, 3}
<>
{3, 4}
proof
set z = 4;
not z
in
{1, 2, 3} by
ENUMSET1:def 1;
hence thesis by
TARSKI:def 2;
end;
The0:
{
{} ,
{1, 2},
{3, 4},
{1, 2, 3, 4}}
<> (
bool
{1, 2, 3, 4})
proof
set y =
{1, 2, 3};
not 4
in
{1, 2, 3} by
ENUMSET1:def 1;
then
b1: y
<>
{1, 2, 3, 4} by
ENUMSET1:def 2;
3
in
{1, 2, 3} by
ENUMSET1:def 1;
then
K1: y
<>
{1, 2} by
TARSKI:def 2;
not (y
in
{
{} ,
{1, 2}} or y
in
{
{3, 4}})
proof
( not y
in
{
{} }) & not y
in
{
{1, 2}} by
K1,
TARSKI:def 1;
then not y
in (
{
{} }
\/
{
{1, 2}}) by
XBOOLE_0:def 3;
hence thesis by
TARSKI:def 1,
WW1,
ENUMSET1: 1;
end;
then not y
in (
{
{} ,
{1, 2}}
\/
{
{3, 4}}) by
XBOOLE_0:def 3;
then not (y
in
{
{} ,
{1, 2},
{3, 4}} or y
in
{
{1, 2, 3, 4}}) by
b1,
ENUMSET1: 3,
TARSKI:def 1;
then not y
in (
{
{} ,
{1, 2},
{3, 4}}
\/
{
{1, 2, 3, 4}}) by
XBOOLE_0:def 3;
hence thesis by
B123,
ENUMSET1: 6;
end;
set Omega3 =
{1, 2, 3}, Omega4 =
{1, 2, 3, 4};
ATh102:
{1, 2, 3}
c<
{1, 2, 3, 4}
proof
for x be
object st x
in Omega3 holds x
in Omega4
proof
let x be
object;
assume x
in Omega3;
then x
= 1 or x
= 2 or x
= 3 or x
= 4 by
ENUMSET1:def 1;
hence thesis by
ENUMSET1:def 2;
end;
then
T1: Omega3
c= Omega4;
Omega3
<> Omega4
proof
4
in
{1, 2, 3, 4} by
ENUMSET1:def 2;
hence thesis by
ENUMSET1:def 1;
end;
hence thesis by
T1;
end;
set Omega2 =
{1, 2};
ATh101:
{1, 2}
c<
{1, 2, 3}
proof
for x be
object st x
in Omega2 holds x
in Omega3
proof
let x be
object;
assume x
in Omega2;
then x
= 1 or x
= 2 by
TARSKI:def 2;
hence thesis by
ENUMSET1:def 1;
end;
then
T1: Omega2
c= Omega3;
Omega2
<> Omega3
proof
3
in
{1, 2, 3} by
ENUMSET1:def 1;
hence thesis by
TARSKI:def 2;
end;
hence thesis by
T1;
end;
registration
let I be non
empty
Subset of
NAT ;
cluster (
In (I,(
bool
REAL ))) -> non
empty;
coherence
proof
I
c=
REAL by
NUMBERS: 19;
hence thesis by
SUBSET_1:def 8;
end;
end
theorem ::
FINANCE3:2
for T be
Nat holds { w where w be
Element of
NAT : w
>
0 & w
<= T }
c= { w where w be
Element of
NAT : w
<= T }
proof
let T be
Nat;
let x be
object;
assume x
in { w where w be
Element of
NAT : w
>
0 & w
<= T };
then
consider w be
Element of
NAT such that
B1: x
= w & w
>
0 & w
<= T;
thus thesis by
B1;
end;
theorem ::
FINANCE3:3
for T be
Nat holds { w where w be
Element of
NAT : w
<= T } is non
empty
Subset of
NAT
proof
let T be
Nat;
B1: { w where w be
Element of
NAT : w
<= T }
c=
NAT
proof
let x be
object;
assume x
in { w where w be
Element of
NAT : w
<= T };
then
consider w be
Element of
NAT such that
C1: x
= w & w
<= T;
thus thesis by
C1;
end;
T
in { w where w be
Element of
NAT : w
<= T }
proof
T
in
NAT by
ORDINAL1:def 12;
hence thesis;
end;
hence thesis by
B1;
end;
theorem ::
FINANCE3:4
for T be
Nat st T
>
0 holds { w where w be
Element of
NAT : w
>
0 & w
<= T } is non
empty
Subset of
NAT
proof
let T be
Nat;
assume
A0: T
>
0 ;
B1: { w where w be
Element of
NAT : w
>
0 & w
<= T }
c=
NAT
proof
let x be
object;
assume x
in { w where w be
Element of
NAT : w
>
0 & w
<= T };
then
consider w be
Element of
NAT such that
C1: x
= w & w
>
0 & w
<= T;
thus thesis by
C1;
end;
1
>
0 & 1
<= T
proof
T
>
0 & T
= (1
* T) by
A0;
hence thesis by
NAT_1: 24;
end;
then 1
in { w where w be
Element of
NAT : w
>
0 & w
<= T };
hence thesis by
B1;
end;
theorem ::
FINANCE3:5
for d be
Nat, phi be
Real_Sequence, Omega be non
empty
set, F be
SigmaField of Omega, X be non
empty
set, G be
sequence of X, w be
Element of Omega holds
{(
PortfolioValueFutExt (d,phi,F,G,w))} is
Event of
Borel_Sets by
FINANCE2: 5;
definition
let d be
Nat;
let phi be
Real_Sequence;
let Omega be non
empty
set;
let F be
SigmaField of Omega;
let X be non
empty
set;
let G be
sequence of X;
let w be
Element of Omega;
:: original:
PortfolioValueFutExt
redefine
func
PortfolioValueFutExt (d,phi,F,G,w) ->
Element of
REAL ;
coherence ;
end
definition
let Omega be non
empty
set;
let F be
SigmaField of Omega;
let X be non
empty
set;
let G be
sequence of X;
let phi be
Real_Sequence;
let d be
Nat;
::
FINANCE3:def1
func
RVPortfolioValueFutExt (phi,F,G,d) ->
Function of Omega,
REAL means
:
Def2: for w be
Element of Omega holds (it
. w)
= (
PortfolioValueFutExt (d,phi,F,G,w));
existence
proof
deffunc
U(
Element of Omega) = (
PortfolioValueFutExt (d,phi,F,G,$1));
consider f be
Function of Omega,
REAL such that
A1: for d be
Element of Omega holds (f
. d)
=
U(d) from
FUNCT_2:sch 4;
take f;
let n be
Element of Omega;
thus thesis by
A1;
end;
uniqueness
proof
let f1,f2 be
Function of Omega,
REAL ;
assume that
A2: for w be
Element of Omega holds (f1
. w)
= (
PortfolioValueFutExt (d,phi,F,G,w)) and
A3: for w be
Element of Omega holds (f2
. w)
= (
PortfolioValueFutExt (d,phi,F,G,w));
for w be
Element of Omega holds (f1
. w)
= (f2
. w)
proof
let w be
Element of Omega;
(f2
. w)
= (
PortfolioValueFutExt (d,phi,F,G,w)) by
A3;
hence thesis by
A2;
end;
hence thesis;
end;
end
theorem ::
FINANCE3:6
for Omega be non
empty
set holds for F be
SigmaField of Omega holds for G be
sequence of (
set_of_random_variables_on (F,
Borel_Sets )) holds for phi be
Real_Sequence holds for d be
Nat holds (
RVPortfolioValueFutExt (phi,F,G,d)) is
random_variable of F,
Borel_Sets
proof
let Omega be non
empty
set;
let F be
SigmaField of Omega;
let G be
sequence of (
set_of_random_variables_on (F,
Borel_Sets ));
let phi be
Real_Sequence;
let d be
Nat;
defpred
J[
Nat] means (
RVPortfolioValueFutExt (phi,F,G,$1)) is
random_variable of F,
Borel_Sets ;
(
ElementsOfPortfolioValueProb_fut (F,(G
.
0 ))) is
random_variable of F,
Borel_Sets by
FINANCE2: 28;
then
A1: ((phi
.
0 )
(#) (
ElementsOfPortfolioValueProb_fut (F,(G
.
0 )))) is
random_variable of F,
Borel_Sets by
FINANCE2: 26;
(
RVPortfolioValueFutExt (phi,F,G,
0 )) is
random_variable of F,
Borel_Sets
proof
for w be
Element of Omega holds ((
RVPortfolioValueFutExt (phi,F,G,
0 ))
. w)
= (((phi
.
0 )
(#) (
ElementsOfPortfolioValueProb_fut (F,(G
.
0 ))))
. w)
proof
let w be
Element of Omega;
((
RVPortfolioValueFutExt (phi,F,G,
0 ))
. w)
= (
PortfolioValueFutExt (
0 ,phi,F,G,w)) by
Def2;
then ((
RVPortfolioValueFutExt (phi,F,G,
0 ))
. w)
= ((
RVPortfolioValueFutExt_El (phi,F,G,w))
.
0 ) by
SERIES_1:def 1
.= ((
RVElementsOfPortfolioValue_fut (phi,F,G,
0 ))
. w) by
FINANCE2:def 6
.= ((phi
.
0 )
* ((
ElementsOfPortfolioValueProb_fut (F,(G
.
0 )))
. w)) by
FINANCE2:def 5;
hence thesis by
VALUED_1: 6;
end;
hence thesis by
A1,
FUNCT_2: 63;
end;
then
J0:
J[
0 ];
J1: for n be
Nat st
J[n] holds
J[(n
+ 1)]
proof
let n be
Nat;
assume
B1:
J[n];
C0: for w be
Element of Omega holds ((
RVPortfolioValueFutExt (phi,F,G,(n
+ 1)))
. w)
= (((
RVPortfolioValueFutExt (phi,F,G,n))
. w)
+ ((
RVElementsOfPortfolioValue_fut (phi,F,G,(n
+ 1)))
. w))
proof
let w be
Element of Omega;
((
RVPortfolioValueFutExt (phi,F,G,(n
+ 1)))
. w)
= (
PortfolioValueFutExt ((n
+ 1),phi,F,G,w)) by
Def2;
then
D1: ((
RVPortfolioValueFutExt (phi,F,G,(n
+ 1)))
. w)
= (((
Partial_Sums (
RVPortfolioValueFutExt_El (phi,F,G,w)))
. n)
+ ((
RVPortfolioValueFutExt_El (phi,F,G,w))
. (n
+ 1))) by
SERIES_1:def 1;
((
RVPortfolioValueFutExt (phi,F,G,n))
. w)
= (
PortfolioValueFutExt (n,phi,F,G,w)) by
Def2;
hence thesis by
FINANCE2:def 6,
D1;
end;
K2: (
RVElementsOfPortfolioValue_fut (phi,F,G,(n
+ 1))) is
random_variable of F,
Borel_Sets by
FINANCE2: 30;
C2: (
dom (
RVPortfolioValueFutExt (phi,F,G,n)))
= Omega by
FUNCT_2:def 1;
(
dom (
RVElementsOfPortfolioValue_fut (phi,F,G,(n
+ 1))))
= Omega by
FUNCT_2:def 1;
then (
dom (
RVPortfolioValueFutExt (phi,F,G,(n
+ 1))))
= ((
dom (
RVPortfolioValueFutExt (phi,F,G,n)))
/\ (
dom (
RVElementsOfPortfolioValue_fut (phi,F,G,(n
+ 1))))) & for c be
object st c
in (
dom (
RVPortfolioValueFutExt (phi,F,G,(n
+ 1)))) holds ((
RVPortfolioValueFutExt (phi,F,G,(n
+ 1)))
. c)
= (((
RVPortfolioValueFutExt (phi,F,G,n))
. c)
+ ((
RVElementsOfPortfolioValue_fut (phi,F,G,(n
+ 1)))
. c)) by
C0,
FUNCT_2:def 1,
C2;
then (
RVPortfolioValueFutExt (phi,F,G,(n
+ 1)))
= ((
RVPortfolioValueFutExt (phi,F,G,n))
+ (
RVElementsOfPortfolioValue_fut (phi,F,G,(n
+ 1)))) by
VALUED_1:def 1;
hence thesis by
B1,
K2,
FINANCE2: 23;
end;
for n be
Nat holds
J[n] from
NAT_1:sch 2(
J0,
J1);
hence thesis;
end;
definition
let d be
Nat;
let phi be
Real_Sequence;
let Omega be non
empty
set;
let F be
SigmaField of Omega;
let X be non
empty
set;
let G be
sequence of X;
let w be
Element of Omega;
:: original:
PortfolioValueFut
redefine
::
FINANCE3:def2
func
PortfolioValueFut (d,phi,F,G,w) ->
Real equals ((
Partial_Sums ((
RVPortfolioValueFutExt_El (phi,F,G,w))
^\ 1))
. (d
- 1));
correctness
proof
per cases ;
suppose
A0: d
=
0 ;
then not (d
- 1)
in (
dom (
Partial_Sums ((
ElementsOfPortfolioValue_fut (phi,F,w,G))
^\ 1)));
then
A1: ((
Partial_Sums ((
ElementsOfPortfolioValue_fut (phi,F,w,G))
^\ 1))
. (d
- 1))
=
{} by
FUNCT_1:def 2;
not (d
- 1)
in (
dom (
Partial_Sums ((
RVPortfolioValueFutExt_El (phi,F,G,w))
^\ 1))) by
A0;
hence thesis by
A1,
FUNCT_1:def 2;
end;
suppose
A0: d
<>
0 ;
for k be
Nat holds ((
Partial_Sums ((
ElementsOfPortfolioValue_fut (phi,F,w,G))
^\ 1))
. k)
= ((
Partial_Sums ((
RVPortfolioValueFutExt_El (phi,F,G,w))
^\ 1))
. k)
proof
let k be
Nat;
defpred
J[
Nat] means ((
Partial_Sums ((
ElementsOfPortfolioValue_fut (phi,F,w,G))
^\ 1))
. $1)
= ((
Partial_Sums ((
RVPortfolioValueFutExt_El (phi,F,G,w))
^\ 1))
. $1);
consider k be
Nat such that
B0: k
=
0 ;
((
Partial_Sums ((
ElementsOfPortfolioValue_fut (phi,F,w,G))
^\ 1))
. k)
= (((
ElementsOfPortfolioValue_fut (phi,F,w,G))
^\ 1)
. k) by
B0,
SERIES_1:def 1;
then
B1: ((
Partial_Sums ((
ElementsOfPortfolioValue_fut (phi,F,w,G))
^\ 1))
. k)
= ((
ElementsOfPortfolioValue_fut (phi,F,w,G))
. (k
+ 1)) by
NAT_1:def 3;
((
Partial_Sums ((
RVPortfolioValueFutExt_El (phi,F,G,w))
^\ 1))
. k)
= (((
RVPortfolioValueFutExt_El (phi,F,G,w))
^\ 1)
. k) by
B0,
SERIES_1:def 1
.= ((
RVPortfolioValueFutExt_El (phi,F,G,w))
. (k
+ 1)) by
NAT_1:def 3
.= ((
RVElementsOfPortfolioValue_fut (phi,F,G,(k
+ 1)))
. w) by
FINANCE2:def 6;
then ((
Partial_Sums ((
RVPortfolioValueFutExt_El (phi,F,G,w))
^\ 1))
. k)
= (((
ElementsOfPortfolioValueProb_fut (F,(G
. (k
+ 1))))
. w)
* (phi
. (k
+ 1))) by
FINANCE2:def 5;
then
J0:
J[
0 ] by
FINANCE1:def 10,
B1,
B0;
J1: for n be
Nat st
J[n] holds
J[(n
+ 1)]
proof
let n be
Nat;
assume
C0:
J[n];
(((
ElementsOfPortfolioValue_fut (phi,F,w,G))
^\ 1)
. (n
+ 1))
= ((
ElementsOfPortfolioValue_fut (phi,F,w,G))
. ((n
+ 1)
+ 1)) by
NAT_1:def 3
.= (((
ElementsOfPortfolioValueProb_fut (F,(G
. ((n
+ 1)
+ 1))))
. w)
* (phi
. ((n
+ 1)
+ 1))) by
FINANCE1:def 10
.= ((
RVElementsOfPortfolioValue_fut (phi,F,G,((n
+ 1)
+ 1)))
. w) by
FINANCE2:def 5
.= ((
RVPortfolioValueFutExt_El (phi,F,G,w))
. ((n
+ 1)
+ 1)) by
FINANCE2:def 6;
then (((
ElementsOfPortfolioValue_fut (phi,F,w,G))
^\ 1)
. (n
+ 1))
= (((
RVPortfolioValueFutExt_El (phi,F,G,w))
^\ 1)
. (n
+ 1)) by
NAT_1:def 3;
then ((
Partial_Sums ((
ElementsOfPortfolioValue_fut (phi,F,w,G))
^\ 1))
. (n
+ 1))
= (((
Partial_Sums ((
RVPortfolioValueFutExt_El (phi,F,G,w))
^\ 1))
. n)
+ (((
RVPortfolioValueFutExt_El (phi,F,G,w))
^\ 1)
. (n
+ 1))) by
SERIES_1:def 1,
C0
.= ((
Partial_Sums ((
RVPortfolioValueFutExt_El (phi,F,G,w))
^\ 1))
. (n
+ 1)) by
SERIES_1:def 1;
hence thesis;
end;
for n be
Nat holds
J[n] from
NAT_1:sch 2(
J0,
J1);
hence thesis;
end;
hence thesis by
A0;
end;
end;
end
definition
let d be
Nat;
let phi be
Real_Sequence;
let Omega be non
empty
set;
let F be
SigmaField of Omega;
let X be non
empty
set;
let G be
sequence of X;
let w be
Element of Omega;
:: original:
PortfolioValueFut
redefine
func
PortfolioValueFut (d,phi,F,G,w) ->
Element of
REAL ;
coherence by
XREAL_0:def 1;
end
definition
let Omega be non
empty
set;
let F be
SigmaField of Omega;
let X be non
empty
set;
let G be
sequence of X;
let phi be
Real_Sequence;
let d be
Nat;
::
FINANCE3:def3
func
RVPortfolioValueFut (phi,F,G,d) ->
Function of Omega,
REAL means
:
Def4: for w be
Element of Omega holds (it
. w)
= (
PortfolioValueFut ((d
+ 1),phi,F,G,w));
existence
proof
deffunc
U(
Element of Omega) = (
PortfolioValueFut ((d
+ 1),phi,F,G,$1));
consider f be
Function of Omega,
REAL such that
A1: for d be
Element of Omega holds (f
. d)
=
U(d) from
FUNCT_2:sch 4;
take f;
let n be
Element of Omega;
thus thesis by
A1;
end;
uniqueness
proof
let f1,f2 be
Function of Omega,
REAL ;
assume that
A2: for w be
Element of Omega holds (f1
. w)
= (
PortfolioValueFut ((d
+ 1),phi,F,G,w)) and
A3: for w be
Element of Omega holds (f2
. w)
= (
PortfolioValueFut ((d
+ 1),phi,F,G,w));
for w be
Element of Omega holds (f1
. w)
= (f2
. w)
proof
let w be
Element of Omega;
(f2
. w)
= (
PortfolioValueFut ((d
+ 1),phi,F,G,w)) by
A3;
hence thesis by
A2;
end;
hence thesis;
end;
end
theorem ::
FINANCE3:7
for Omega be non
empty
set holds for F be
SigmaField of Omega holds for G be
sequence of (
set_of_random_variables_on (F,
Borel_Sets )) holds for phi be
Real_Sequence holds for d be
Nat holds (
RVPortfolioValueFut (phi,F,G,d)) is
random_variable of F,
Borel_Sets
proof
let Omega be non
empty
set;
let F be
SigmaField of Omega;
let G be
sequence of (
set_of_random_variables_on (F,
Borel_Sets ));
let phi be
Real_Sequence;
let d be
Nat;
defpred
J[
Nat] means (
RVPortfolioValueFut (phi,F,G,$1)) is
random_variable of F,
Borel_Sets ;
(
ElementsOfPortfolioValueProb_fut (F,(G
. (
0
+ 1)))) is
random_variable of F,
Borel_Sets by
FINANCE2: 28;
then
A1: ((phi
. (
0
+ 1))
(#) (
ElementsOfPortfolioValueProb_fut (F,(G
. (
0
+ 1))))) is
random_variable of F,
Borel_Sets by
FINANCE2: 26;
(
RVPortfolioValueFut (phi,F,G,
0 )) is
random_variable of F,
Borel_Sets
proof
for w be
Element of Omega holds ((
RVPortfolioValueFut (phi,F,G,
0 ))
. w)
= (((phi
. (
0
+ 1))
(#) (
ElementsOfPortfolioValueProb_fut (F,(G
. (
0
+ 1)))))
. w)
proof
let w be
Element of Omega;
consider k be
Nat such that
B0: k
=
0 ;
((
RVPortfolioValueFut (phi,F,G,k))
. w)
= (
PortfolioValueFut ((k
+ 1),phi,F,G,w)) by
Def4
.= (((
RVPortfolioValueFutExt_El (phi,F,G,w))
^\ 1)
. k) by
B0,
SERIES_1:def 1
.= ((
RVPortfolioValueFutExt_El (phi,F,G,w))
. (k
+ 1)) by
NAT_1:def 3
.= ((
RVElementsOfPortfolioValue_fut (phi,F,G,(k
+ 1)))
. w) by
FINANCE2:def 6;
then ((
RVPortfolioValueFut (phi,F,G,
0 ))
. w)
= (((
ElementsOfPortfolioValueProb_fut (F,(G
. (
0
+ 1))))
. w)
* (phi
. (
0
+ 1))) by
FINANCE2:def 5,
B0;
hence thesis by
VALUED_1: 6;
end;
hence thesis by
A1,
FUNCT_2: 63;
end;
then
J0:
J[
0 ];
J1: for n be
Nat st
J[n] holds
J[(n
+ 1)]
proof
let n be
Nat;
assume
B1:
J[n];
C0: for w be
Element of Omega holds ((
RVPortfolioValueFut (phi,F,G,(n
+ 1)))
. w)
= (((
RVPortfolioValueFut (phi,F,G,n))
. w)
+ ((
RVElementsOfPortfolioValue_fut (phi,F,G,((n
+ 1)
+ 1)))
. w))
proof
let w be
Element of Omega;
set k = (n
+ 1);
((
RVPortfolioValueFut (phi,F,G,k))
. w)
= (
PortfolioValueFut ((k
+ 1),phi,F,G,w)) by
Def4;
then ((
RVPortfolioValueFut (phi,F,G,k))
. w)
= ((
PortfolioValueFut ((n
+ 1),phi,F,G,w))
+ (((
RVPortfolioValueFutExt_El (phi,F,G,w))
^\ 1)
. (n
+ 1))) by
SERIES_1:def 1;
then ((
RVPortfolioValueFut (phi,F,G,k))
. w)
= (((
RVPortfolioValueFut (phi,F,G,n))
. w)
+ (((
RVPortfolioValueFutExt_El (phi,F,G,w))
^\ 1)
. (n
+ 1))) by
Def4
.= (((
RVPortfolioValueFut (phi,F,G,n))
. w)
+ ((
RVPortfolioValueFutExt_El (phi,F,G,w))
. ((n
+ 1)
+ 1))) by
NAT_1:def 3;
hence thesis by
FINANCE2:def 6;
end;
K1: (
RVElementsOfPortfolioValue_fut (phi,F,G,((n
+ 1)
+ 1))) is
random_variable of F,
Borel_Sets by
FINANCE2: 30;
C2: (
dom (
RVPortfolioValueFut (phi,F,G,n)))
= Omega by
FUNCT_2:def 1;
(
dom (
RVElementsOfPortfolioValue_fut (phi,F,G,((n
+ 1)
+ 1))))
= Omega by
FUNCT_2:def 1;
then (
dom (
RVPortfolioValueFut (phi,F,G,(n
+ 1))))
= ((
dom (
RVPortfolioValueFut (phi,F,G,n)))
/\ (
dom (
RVElementsOfPortfolioValue_fut (phi,F,G,((n
+ 1)
+ 1))))) & for c be
object st c
in (
dom (
RVPortfolioValueFut (phi,F,G,(n
+ 1)))) holds ((
RVPortfolioValueFut (phi,F,G,(n
+ 1)))
. c)
= (((
RVPortfolioValueFut (phi,F,G,n))
. c)
+ ((
RVElementsOfPortfolioValue_fut (phi,F,G,((n
+ 1)
+ 1)))
. c)) by
C0,
FUNCT_2:def 1,
C2;
then (
RVPortfolioValueFut (phi,F,G,(n
+ 1)))
= ((
RVPortfolioValueFut (phi,F,G,n))
+ (
RVElementsOfPortfolioValue_fut (phi,F,G,((n
+ 1)
+ 1)))) by
VALUED_1:def 1;
hence thesis by
B1,
K1,
FINANCE2: 23;
end;
for n be
Nat holds
J[n] from
NAT_1:sch 2(
J0,
J1);
hence thesis;
end;
theorem ::
FINANCE3:8
for d be
Nat, phi be
Real_Sequence, Omega be non
empty
set, F be
SigmaField of Omega, X be non
empty
set, G be
sequence of X, w be
Element of Omega holds (
PortfolioValueFut ((d
+ 1),phi,F,G,w))
= ((
RVPortfolioValueFut (phi,F,G,d))
. w) &
{(
PortfolioValueFut ((d
+ 1),phi,F,G,w))} is
Event of
Borel_Sets by
Def4,
FINANCE2: 5;
theorem ::
FINANCE3:9
for Omega be non
empty
set, F be
SigmaField of Omega, X be non
empty
set, G be
sequence of X, phi be
Real_Sequence, d be
Nat holds (
RVPortfolioValueFutExt (phi,F,G,(d
+ 1)))
= ((
RVPortfolioValueFut (phi,F,G,d))
+ (
RVElementsOfPortfolioValue_fut (phi,F,G,
0 )))
proof
let Omega be non
empty
set;
let F be
SigmaField of Omega;
let X be non
empty
set;
let G be
sequence of X;
let phi be
Real_Sequence;
let d be
Nat;
C0: for w be
Element of Omega holds ((
RVPortfolioValueFutExt (phi,F,G,(d
+ 1)))
. w)
= (((
RVPortfolioValueFut (phi,F,G,d))
. w)
+ ((
RVElementsOfPortfolioValue_fut (phi,F,G,
0 ))
. w))
proof
let w be
Element of Omega;
A01: ((
RVPortfolioValueFut (phi,F,G,d))
. w)
= (
PortfolioValueFut ((d
+ 1),phi,F,G,w)) by
Def4;
for d be
Nat holds ((
Partial_Sums ((
RVPortfolioValueFutExt_El (phi,F,G,w))
^\ 1))
. d)
= (((
Partial_Sums (
RVPortfolioValueFutExt_El (phi,F,G,w)))
. (d
+ 1))
- ((
RVPortfolioValueFutExt_El (phi,F,G,w))
.
0 ))
proof
defpred
J[
Nat] means ((
Partial_Sums ((
RVPortfolioValueFutExt_El (phi,F,G,w))
^\ 1))
. $1)
= (((
Partial_Sums (
RVPortfolioValueFutExt_El (phi,F,G,w)))
. ($1
+ 1))
- ((
RVPortfolioValueFutExt_El (phi,F,G,w))
.
0 ));
B1: ((
Partial_Sums ((
RVPortfolioValueFutExt_El (phi,F,G,w))
^\ 1))
.
0 )
= (((
RVPortfolioValueFutExt_El (phi,F,G,w))
^\ 1)
.
0 ) by
SERIES_1:def 1;
((
Partial_Sums ((
RVPortfolioValueFutExt_El (phi,F,G,w))
^\ 1))
.
0 )
= (((
Partial_Sums (
RVPortfolioValueFutExt_El (phi,F,G,w)))
. (
0
+ 1))
- ((
RVPortfolioValueFutExt_El (phi,F,G,w))
.
0 ))
proof
((
Partial_Sums (
RVPortfolioValueFutExt_El (phi,F,G,w)))
. (
0
+ 1))
= (((
Partial_Sums (
RVPortfolioValueFutExt_El (phi,F,G,w)))
.
0 )
+ ((
RVPortfolioValueFutExt_El (phi,F,G,w))
. (
0
+ 1))) by
SERIES_1:def 1;
then ((
Partial_Sums ((
RVPortfolioValueFutExt_El (phi,F,G,w))
^\ 1))
.
0 )
= (((
Partial_Sums (
RVPortfolioValueFutExt_El (phi,F,G,w)))
. (
0
+ 1))
- ((
Partial_Sums (
RVPortfolioValueFutExt_El (phi,F,G,w)))
.
0 )) by
NAT_1:def 3,
B1;
hence thesis by
SERIES_1:def 1;
end;
then
J0:
J[
0 ];
J1: for n be
Nat st
J[n] holds
J[(n
+ 1)]
proof
let n be
Nat;
assume
Q0:
J[n];
((
Partial_Sums ((
RVPortfolioValueFutExt_El (phi,F,G,w))
^\ 1))
. (n
+ 1))
= (((
Partial_Sums ((
RVPortfolioValueFutExt_El (phi,F,G,w))
^\ 1))
. n)
+ (((
RVPortfolioValueFutExt_El (phi,F,G,w))
^\ 1)
. (n
+ 1))) by
SERIES_1:def 1
.= ((((
Partial_Sums (
RVPortfolioValueFutExt_El (phi,F,G,w)))
. (n
+ 1))
+ (((
RVPortfolioValueFutExt_El (phi,F,G,w))
^\ 1)
. (n
+ 1)))
- ((
RVPortfolioValueFutExt_El (phi,F,G,w))
.
0 )) by
Q0
.= ((((
Partial_Sums (
RVPortfolioValueFutExt_El (phi,F,G,w)))
. (n
+ 1))
+ ((
RVPortfolioValueFutExt_El (phi,F,G,w))
. ((n
+ 1)
+ 1)))
- ((
RVPortfolioValueFutExt_El (phi,F,G,w))
.
0 )) by
NAT_1:def 3;
hence thesis by
SERIES_1:def 1;
end;
for n be
Nat holds
J[n] from
NAT_1:sch 2(
J0,
J1);
hence thesis;
end;
then ((
RVPortfolioValueFut (phi,F,G,d))
. w)
= ((
PortfolioValueFutExt ((d
+ 1),phi,F,G,w))
- ((
RVPortfolioValueFutExt_El (phi,F,G,w))
.
0 )) by
A01
.= ((
PortfolioValueFutExt ((d
+ 1),phi,F,G,w))
- ((
RVElementsOfPortfolioValue_fut (phi,F,G,
0 ))
. w)) by
FINANCE2:def 6;
hence thesis by
Def2;
end;
C2: (
dom (
RVPortfolioValueFut (phi,F,G,d)))
= Omega by
FUNCT_2:def 1;
(
dom (
RVElementsOfPortfolioValue_fut (phi,F,G,
0 )))
= Omega by
FUNCT_2:def 1;
then (
dom (
RVPortfolioValueFutExt (phi,F,G,(d
+ 1))))
= ((
dom (
RVPortfolioValueFut (phi,F,G,d)))
/\ (
dom (
RVElementsOfPortfolioValue_fut (phi,F,G,
0 )))) & for c be
object st c
in (
dom (
RVPortfolioValueFutExt (phi,F,G,(d
+ 1)))) holds ((
RVPortfolioValueFutExt (phi,F,G,(d
+ 1)))
. c)
= (((
RVPortfolioValueFut (phi,F,G,d))
. c)
+ ((
RVElementsOfPortfolioValue_fut (phi,F,G,
0 ))
. c)) by
C0,
FUNCT_2:def 1,
C2;
hence thesis by
VALUED_1:def 1;
end;
Lm1B: for Omega,Omega2 be non
empty
set, F be
Function of Omega, Omega2, y be non
empty
set holds { z where z be
Element of Omega : (F
. z) is
Element of y }
= (F
" y)
proof
let Omega,Omega2 be non
empty
set, F be
Function of Omega, Omega2, y be non
empty
set;
set D = { z where z be
Element of Omega : (F
. z) is
Element of y };
for x be
object holds x
in D iff x
in (F
" y)
proof
let x be
object;
hereby
assume x
in D;
then
consider z be
Element of Omega such that
A1: x
= z & (F
. z) is
Element of y;
z
in Omega;
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 D;
end;
hence thesis by
TARSKI: 2;
end;
theorem ::
FINANCE3:10
1A5: for Omega,Omega2 be non
empty
set, Sigma be
SigmaField of Omega, Sigma2 be
SigmaField of Omega2, s be
Element of Omega2 holds (Omega
--> s) is Sigma, Sigma2
-random_variable-like
proof
let Omega,Omega2 be non
empty
set;
let Sigma be
SigmaField of Omega;
let Sigma2 be
SigmaField of Omega2;
let s be
Element of Omega2;
set X = (Omega
--> s);
let x be
set;
per cases ;
suppose
A1: s
in x;
for q be
object holds q
in { w where w be
Element of Omega : (X
. w) is
Element of x } iff q
in Omega
proof
let q be
object;
hereby
assume q
in { w where w be
Element of Omega : (X
. w) is
Element of x };
then ex w be
Element of Omega st w
= q & (X
. w) is
Element of x;
hence q
in Omega;
end;
assume q
in Omega;
then
reconsider w = q as
Element of Omega;
(X
. w) is
Element of x by
A1,
FUNCOP_1: 7;
hence thesis;
end;
then { w where w be
Element of Omega : (X
. w) is
Element of x }
= Omega by
TARSKI: 2;
then (X
" x)
= Omega by
A1,
Lm1B;
then (X
" x) is
Element of Sigma by
PROB_1: 23;
hence thesis;
end;
suppose
A3: not s
in x;
(X
" x)
c=
{}
proof
let q be
object;
assume q
in (X
" x);
then q
in (
dom X) & (X
. q)
in x by
FUNCT_1:def 7;
hence q
in
{} by
A3,
FUNCOP_1: 7;
end;
then (X
" x)
=
{} ;
then (X
" x) is
Element of Sigma by
PROB_1: 22;
hence thesis;
end;
end;
theorem ::
FINANCE3:11
for Omega be non
empty
set, Sigma be
SigmaField of Omega, RV be
random_variable of Sigma,
Borel_Sets , K be
Real holds (RV
- (Omega
--> K)) is
random_variable of Sigma,
Borel_Sets
proof
let Omega be non
empty
set, Sigma be
SigmaField of Omega, RV be
random_variable of Sigma,
Borel_Sets , K be
Real;
reconsider KK = K as
Element of
REAL by
XREAL_0:def 1;
(Omega
--> KK) is
random_variable of Sigma,
Borel_Sets by
1A5;
hence thesis by
FINANCE2: 24;
end;
definition
let Omega be non
empty
set;
let RV be
Function of Omega,
REAL ;
let w be
Element of Omega;
::
FINANCE3:def4
func
SetForCall-Option (RV,w) ->
Element of
REAL equals
:
Def89: (RV
. w) if (RV
. w)
>=
0
otherwise
0 ;
correctness by
NUMBERS: 19;
end
definition
let Omega be non
empty
set;
let Sigma be
SigmaField of Omega;
let RV be
random_variable of Sigma,
Borel_Sets ;
let K be
Real;
::
FINANCE3:def5
func
Call-Option (RV,K) ->
Function of Omega,
REAL means for w be
Element of Omega holds (((RV
- (Omega
--> K))
. w)
>=
0 implies (it
. w)
= ((RV
- (Omega
--> K))
. w)) & (((RV
- (Omega
--> K))
. w)
<
0 implies (it
. w)
=
0 );
existence
proof
reconsider MyFunc = (RV
- (Omega
--> K)) as
Function of Omega,
REAL ;
deffunc
U(
Element of Omega) = (
SetForCall-Option (MyFunc,$1));
consider f be
Function of Omega,
REAL such that
A1: for d be
Element of Omega holds (f
. d)
=
U(d) from
FUNCT_2:sch 4;
for w be
Element of Omega holds ((MyFunc
. w)
>=
0 implies (f
. w)
= ((RV
- (Omega
--> K))
. w)) & ((MyFunc
. w)
<
0 implies (f
. w)
=
0 )
proof
let w be
Element of Omega;
thus (MyFunc
. w)
>=
0 implies (f
. w)
= ((RV
- (Omega
--> K))
. w)
proof
assume
B1: (MyFunc
. w)
>=
0 ;
(f
. w)
= (
SetForCall-Option (MyFunc,w)) by
A1;
hence thesis by
Def89,
B1;
end;
assume
B1: (MyFunc
. w)
<
0 ;
(f
. w)
= (
SetForCall-Option (MyFunc,w)) by
A1;
hence thesis by
Def89,
B1;
end;
hence thesis;
end;
uniqueness
proof
let f1,f2 be
Function of Omega,
REAL ;
assume that
A2: for w be
Element of Omega holds (((RV
- (Omega
--> K))
. w)
>=
0 implies (f1
. w)
= ((RV
- (Omega
--> K))
. w)) & (((RV
- (Omega
--> K))
. w)
<
0 implies (f1
. w)
=
0 ) and
A3: for w be
Element of Omega holds (((RV
- (Omega
--> K))
. w)
>=
0 implies (f2
. w)
= ((RV
- (Omega
--> K))
. w)) & (((RV
- (Omega
--> K))
. w)
<
0 implies (f2
. w)
=
0 );
for w be
Element of Omega holds (f1
. w)
= (f2
. w)
proof
let w be
Element of Omega;
per cases ;
suppose
A0: ((RV
- (Omega
--> K))
. w)
>=
0 ;
then (f1
. w)
= ((RV
- (Omega
--> K))
. w) by
A2;
hence thesis by
A0,
A3;
end;
suppose
A0: not ((RV
- (Omega
--> K))
. w)
>=
0 ;
then (f1
. w)
=
0 by
A2;
hence thesis by
A0,
A3;
end;
end;
hence thesis;
end;
end
theorem ::
FINANCE3:12
SuperLemma1: for A1 be
SetSequence of
{1, 2, 3, 4}, w be
Real st w
= 1 or w
= 3 holds (for n be
Nat holds (A1
. n)
=
{} or (A1
. n)
=
{1, 2} or (A1
. n)
=
{3, 4} or (A1
. n)
=
{1, 2, 3, 4}) implies
{w}
<> (
Intersection A1)
proof
let A1 be
SetSequence of
{1, 2, 3, 4};
let w be
Real;
assume
KX: w
= 1 or w
= 3;
assume
S2: for n be
Nat holds (A1
. n)
=
{} or (A1
. n)
=
{1, 2} or (A1
. n)
=
{3, 4} or (A1
. n)
=
{1, 2, 3, 4};
per cases ;
suppose (
Intersection A1)
=
{} ;
hence thesis;
end;
suppose
SUPP1: (
Intersection A1)
<>
{} ;
ex x be
object st (for n be
Nat holds x
in (A1
. n)) & not x
in
{w}
proof
per cases ;
suppose ex j be
Nat st (A1
. j)
=
{} ;
then
consider j be
Nat such that
J0: (A1
. j)
=
{} ;
thus thesis by
The1,
J0,
SUPP1;
end;
suppose
USUPP1: for n be
Nat holds (A1
. n)
<>
{} ;
per cases ;
suppose
P1: for j be
Nat holds
{1, 2}
c= (A1
. j);
set x = 2;
Z1: not x
in
{w} by
TARSKI:def 1,
KX;
for n be
Nat holds x
in (A1
. n)
proof
let n be
Nat;
per cases by
S2;
suppose (A1
. n)
=
{} ;
hence thesis by
USUPP1;
end;
suppose (A1
. n)
=
{1, 2};
hence thesis by
TARSKI:def 2;
end;
suppose
J0: (A1
. n)
=
{3, 4};
x
in
{1, 2} by
TARSKI:def 2;
then not
{1, 2}
c= (A1
. n) by
J0,
TARSKI:def 2;
hence thesis by
P1;
end;
suppose (A1
. n)
=
{1, 2, 3, 4};
hence thesis by
ENUMSET1:def 2;
end;
end;
hence thesis by
Z1;
end;
suppose ex j be
Nat st not
{1, 2}
c= (A1
. j);
then
consider j be
Nat such that
BSUPP1: not
{1, 2}
c= (A1
. j);
per cases ;
suppose
P1: for n be
Nat holds
{3, 4}
c= (A1
. n);
set x = 4;
Z1: not x
in
{w} by
TARSKI:def 1,
KX;
for n be
Nat holds x
in (A1
. n)
proof
let n be
Nat;
per cases by
S2;
suppose (A1
. n)
=
{} ;
hence thesis by
USUPP1;
end;
suppose (A1
. n)
=
{3, 4};
hence thesis by
TARSKI:def 2;
end;
suppose
J0: (A1
. n)
=
{1, 2};
x
in
{3, 4} by
TARSKI:def 2;
then not
{3, 4}
c= (A1
. n) by
J0,
TARSKI:def 2;
hence thesis by
P1;
end;
suppose (A1
. n)
=
{1, 2, 3, 4};
hence thesis by
ENUMSET1:def 2;
end;
end;
hence thesis by
Z1;
end;
suppose ex k be
Nat st not
{3, 4}
c= (A1
. k);
then
consider k be
Nat such that
CSUPP1: not
{3, 4}
c= (A1
. k);
ZW1: ((A1
. k)
/\ (A1
. j))
=
{}
proof
per cases by
S2,
Lm2,
BSUPP1;
suppose
DSUPP1: (A1
. j)
=
{3, 4};
(A1
. k)
=
{1, 2} or (A1
. k)
=
{} by
S2,
CSUPP1,
Lm1;
hence thesis by
Lm3,
DSUPP1;
end;
suppose (A1
. j)
=
{} ;
hence thesis;
end;
end;
(
Intersection A1)
=
{}
proof
(
Intersection A1)
c= ((A1
. k)
/\ (A1
. j))
proof
for x be
object st x
in (
Intersection A1) holds x
in ((A1
. k)
/\ (A1
. j))
proof
let x be
object;
assume x
in (
Intersection A1);
then x
in (A1
. k) & x
in (A1
. j) by
PROB_1: 13;
hence thesis by
XBOOLE_0:def 4;
end;
hence thesis;
end;
hence thesis by
ZW1;
end;
hence thesis by
SUPP1;
end;
end;
end;
end;
hence thesis by
PROB_1: 13;
end;
end;
theorem ::
FINANCE3:13
SuperLemma2: for A1 be
SetSequence of
{1, 2, 3, 4}, w be
Real st w
= 2 or w
= 4 holds (for n be
Nat holds (A1
. n)
=
{} or (A1
. n)
=
{1, 2} or (A1
. n)
=
{3, 4} or (A1
. n)
=
{1, 2, 3, 4}) implies
{w}
<> (
Intersection A1)
proof
let A1 be
SetSequence of
{1, 2, 3, 4};
let w be
Real;
assume
KX: w
= 2 or w
= 4;
assume
S2: for n be
Nat holds (A1
. n)
=
{} or (A1
. n)
=
{1, 2} or (A1
. n)
=
{3, 4} or (A1
. n)
=
{1, 2, 3, 4};
per cases ;
suppose (
Intersection A1)
=
{} ;
hence thesis;
end;
suppose
SUPP1: (
Intersection A1)
<>
{} ;
ex x be
object st (for n be
Nat holds x
in (A1
. n)) & not x
in
{w}
proof
per cases ;
suppose ex j be
Nat st (A1
. j)
=
{} ;
then
consider j be
Nat such that
J0: (A1
. j)
=
{} ;
thus thesis by
The1,
J0,
SUPP1;
end;
suppose
USUPP1: for n be
Nat holds (A1
. n)
<>
{} ;
per cases ;
suppose
P1: for j be
Nat holds
{1, 2}
c= (A1
. j);
set x = 1;
Z1: not x
in
{w} by
TARSKI:def 1,
KX;
for n be
Nat holds x
in (A1
. n)
proof
let n be
Nat;
per cases by
S2;
suppose (A1
. n)
=
{} ;
hence thesis by
USUPP1;
end;
suppose (A1
. n)
=
{1, 2};
hence thesis by
TARSKI:def 2;
end;
suppose
J0: (A1
. n)
=
{3, 4};
x
in
{1, 2} by
TARSKI:def 2;
then not
{1, 2}
c= (A1
. n) by
J0,
TARSKI:def 2;
hence thesis by
P1;
end;
suppose (A1
. n)
=
{1, 2, 3, 4};
hence thesis by
ENUMSET1:def 2;
end;
end;
hence thesis by
Z1;
end;
suppose ex j be
Nat st not
{1, 2}
c= (A1
. j);
then
consider j be
Nat such that
BSUPP1: not
{1, 2}
c= (A1
. j);
per cases ;
suppose
P1: for n be
Nat holds
{3, 4}
c= (A1
. n);
set x = 3;
Z1: not x
in
{w} by
TARSKI:def 1,
KX;
for n be
Nat holds x
in (A1
. n)
proof
let n be
Nat;
per cases by
S2;
suppose (A1
. n)
=
{} ;
hence thesis by
USUPP1;
end;
suppose (A1
. n)
=
{3, 4};
hence thesis by
TARSKI:def 2;
end;
suppose
J0: (A1
. n)
=
{1, 2};
x
in
{3, 4} by
TARSKI:def 2;
then not
{3, 4}
c= (A1
. n) by
J0,
TARSKI:def 2;
hence thesis by
P1;
end;
suppose (A1
. n)
=
{1, 2, 3, 4};
hence thesis by
ENUMSET1:def 2;
end;
end;
hence thesis by
Z1;
end;
suppose ex k be
Nat st not
{3, 4}
c= (A1
. k);
then
consider k be
Nat such that
CSUPP1: not
{3, 4}
c= (A1
. k);
ZW1: ((A1
. k)
/\ (A1
. j))
=
{}
proof
per cases by
S2,
Lm2,
BSUPP1;
suppose
DSUPP1: (A1
. j)
=
{3, 4};
per cases by
CSUPP1,
Lm1,
S2;
suppose (A1
. k)
=
{1, 2};
hence thesis by
Lm3,
DSUPP1;
end;
suppose (A1
. k)
=
{} ;
hence thesis;
end;
end;
suppose (A1
. j)
=
{} ;
hence thesis;
end;
end;
(
Intersection A1)
=
{}
proof
(
Intersection A1)
c= ((A1
. k)
/\ (A1
. j))
proof
for x be
object st x
in (
Intersection A1) holds x
in ((A1
. k)
/\ (A1
. j))
proof
let x be
object;
assume x
in (
Intersection A1);
then x
in (A1
. k) & x
in (A1
. j) by
PROB_1: 13;
hence thesis by
XBOOLE_0:def 4;
end;
hence thesis;
end;
hence thesis by
ZW1;
end;
hence thesis by
SUPP1;
end;
end;
end;
end;
hence thesis by
PROB_1: 13;
end;
end;
theorem ::
FINANCE3:14
for MySigmaField,A1,A2 be
set st MySigmaField
=
{
{} ,
{1, 2, 3, 4}} & A1
in MySigmaField & A2
in MySigmaField holds (A1
/\ A2)
in MySigmaField
proof
let MySigmaField,A1,A2 be
set;
assume
A0: MySigmaField
=
{
{} ,
{1, 2, 3, 4}} & A1
in MySigmaField & A2
in MySigmaField;
then (A1
=
{} or A1
=
{1, 2, 3, 4}) & (A2
=
{} or A2
=
{1, 2, 3, 4}) by
TARSKI:def 2;
hence thesis by
A0;
end;
theorem ::
FINANCE3:15
Lm700000: for A1 be
SetSequence of
{1, 2, 3, 4} st (for n be
Nat, k be
Nat holds not (((A1
. n)
/\ (A1
. k))
=
{} )) & (
rng A1)
c=
{
{} ,
{1, 2},
{3, 4},
{1, 2, 3, 4}} holds ((
Intersection A1)
=
{} or (
Intersection A1)
=
{1, 2} or (
Intersection A1)
=
{3, 4} or (
Intersection A1)
=
{1, 2, 3, 4})
proof
let A1 be
SetSequence of
{1, 2, 3, 4};
assume
GENASS0: (for n be
Nat, k be
Nat holds not ((A1
. n)
/\ (A1
. k))
=
{} ) & (
rng A1)
c=
{
{} ,
{1, 2},
{3, 4},
{1, 2, 3, 4}};
set MyOmega =
{
{} ,
{1, 2},
{3, 4},
{1, 2, 3, 4}};
D1: (
dom A1)
=
NAT by
FUNCT_2:def 1;
S20: for n be
Nat holds (A1
. n)
in
{
{} ,
{1, 2},
{3, 4},
{1, 2, 3, 4}}
proof
let n be
Nat;
n
in (
dom A1) by
D1,
ORDINAL1:def 12;
hence thesis by
FUNCT_1: 3,
GENASS0;
end;
S2: for n be
Nat holds (A1
. n)
=
{} or (A1
. n)
=
{1, 2} or (A1
. n)
=
{3, 4} or (A1
. n)
=
{1, 2, 3, 4}
proof
let n be
Nat;
(A1
. n)
in
{
{} ,
{1, 2},
{3, 4},
{1, 2, 3, 4}} by
S20;
hence thesis by
ENUMSET1:def 2;
end;
Fin1: for n be
Nat holds (
Intersection A1)
c= (A1
. n) by
PROB_1: 13;
per cases ;
suppose (
Intersection A1)
=
{1, 2, 3, 4};
hence thesis;
end;
suppose
MYSUPP0: (
Intersection A1)
<>
{1, 2, 3, 4};
W0: (
Intersection A1)
c=
{} or (
Intersection A1)
c=
{1, 2} or (
Intersection A1)
c=
{3, 4}
proof
(
Intersection A1)
=
{} or (
Intersection A1)
=
{1, 2} or (
Intersection A1)
=
{3, 4}
proof
per cases ;
suppose
ASS1: for n be
Nat holds (A1
. n)
=
{1, 2, 3, 4};
(
Intersection A1)
=
{1, 2, 3, 4}
proof
for x be
object holds x
in (
Intersection A1) iff x
in
{1, 2, 3, 4}
proof
let x be
object;
(for n be
Nat holds x
in (A1
. n)) iff x
in
{1, 2, 3, 4}
proof
(for n be
Nat holds x
in (A1
. n)) implies x
in
{1, 2, 3, 4}
proof
assume for n be
Nat holds x
in (A1
. n);
then x
in (A1
.
0 );
then
consider k be
Nat such that
N10: x
in (A1
. k);
thus thesis by
N10;
end;
hence thesis by
ASS1;
end;
hence thesis by
PROB_1: 13;
end;
hence thesis by
TARSKI: 2;
end;
hence thesis by
MYSUPP0;
end;
suppose ex n be
Nat st (A1
. n)
<>
{1, 2, 3, 4};
then
consider n be
Nat such that
KK: (A1
. n)
<>
{1, 2, 3, 4};
per cases by
S2;
suppose (A1
. n)
=
{} ;
hence thesis by
The1;
end;
suppose
JSUPP1: (A1
. n)
=
{1, 2};
(
Intersection A1)
=
{} or (
Intersection A1)
=
{1, 2}
proof
per cases ;
suppose (
Intersection A1)
=
{1, 2};
hence thesis;
end;
suppose (
Intersection A1)
<>
{1, 2};
then (
Intersection A1)
=
{1} or (
Intersection A1)
=
{2} or (
Intersection A1)
=
{} by
ZFMISC_1: 36,
JSUPP1,
Fin1;
hence thesis by
SuperLemma2,
SuperLemma1,
S2;
end;
end;
hence thesis;
end;
suppose
SUPP1: (A1
. n)
=
{3, 4};
(
Intersection A1)
=
{} or (
Intersection A1)
=
{3, 4}
proof
per cases ;
suppose (
Intersection A1)
=
{3, 4};
hence thesis;
end;
suppose (
Intersection A1)
<>
{3, 4};
then (
Intersection A1)
=
{3} or (
Intersection A1)
=
{4} or (
Intersection A1)
=
{} by
SUPP1,
Fin1,
ZFMISC_1: 36;
hence thesis by
SuperLemma1,
S2,
SuperLemma2;
end;
end;
hence thesis;
end;
suppose (A1
. n)
=
{1, 2, 3, 4};
hence thesis by
KK;
end;
end;
end;
hence thesis;
end;
per cases by
W0;
suppose (
Intersection A1)
c=
{} ;
hence thesis;
end;
suppose
ZW10: (
Intersection A1)
c=
{1, 2};
per cases ;
suppose (
Intersection A1)
=
{1, 2};
hence thesis;
end;
suppose (
Intersection A1)
<>
{1, 2};
then (
Intersection A1)
=
{1} or (
Intersection A1)
=
{2} or (
Intersection A1)
=
{} by
ZW10,
ZFMISC_1: 36;
hence thesis by
SuperLemma1,
S2,
SuperLemma2;
end;
end;
suppose
ZW10: (
Intersection A1)
c=
{3, 4};
per cases ;
suppose (
Intersection A1)
=
{3, 4};
hence thesis;
end;
suppose (
Intersection A1)
<>
{3, 4};
then (
Intersection A1)
=
{3} or (
Intersection A1)
=
{4} or (
Intersection A1)
=
{} by
ZW10,
ZFMISC_1: 36;
hence thesis by
SuperLemma1,
S2,
SuperLemma2;
end;
end;
end;
end;
theorem ::
FINANCE3:16
for A1 be
SetSequence of
{1, 2, 3, 4}, MyOmega be
set st MyOmega
=
{
{} ,
{1, 2},
{3, 4},
{1, 2, 3, 4}} & (
Intersection A1)
=
{1, 2, 3, 4} holds (
Intersection A1)
in MyOmega by
ENUMSET1:def 2;
theorem ::
FINANCE3:17
for A1 be
SetSequence of
{1, 2, 3, 4}, MyOmega be
set st MyOmega
=
{
{} ,
{1, 2},
{3, 4},
{1, 2, 3, 4}} & (
Intersection A1)
=
{3, 4} holds (
Intersection A1)
in MyOmega by
ENUMSET1:def 2;
theorem ::
FINANCE3:18
for A1 be
SetSequence of
{1, 2, 3, 4}, MyOmega be
set st MyOmega
=
{
{} ,
{1, 2},
{3, 4},
{1, 2, 3, 4}} & (
Intersection A1)
=
{1, 2} holds (
Intersection A1)
in MyOmega by
ENUMSET1:def 2;
theorem ::
FINANCE3:19
for A1 be
SetSequence of
{1, 2, 3, 4}, MyOmega be
set st MyOmega
=
{
{} ,
{1, 2},
{3, 4},
{1, 2, 3, 4}} & (
Intersection A1)
=
{} holds (
Intersection A1)
in MyOmega by
ENUMSET1:def 2;
theorem ::
FINANCE3:20
Lm8: for MyOmega be
set, A1 be
SetSequence of
{1, 2, 3, 4} st (
rng A1)
c= MyOmega & MyOmega
=
{
{} ,
{1, 2},
{3, 4},
{1, 2, 3, 4}} holds (
Intersection A1)
in MyOmega
proof
let MyOmega be
set;
let A1 be
SetSequence of
{1, 2, 3, 4};
assume
A0: (
rng A1)
c= MyOmega & MyOmega
=
{
{} ,
{1, 2},
{3, 4},
{1, 2, 3, 4}};
(
Intersection A1)
in
{
{} ,
{1, 2},
{3, 4},
{1, 2, 3, 4}}
proof
per cases ;
suppose
CASE000: ex n be
Nat, k be
Nat st ((A1
. n)
/\ (A1
. k))
=
{} ;
CASE0: ex n be
Nat, k be
Nat st (A1
. n)
misses (A1
. k)
proof
consider n be
Nat, k be
Nat such that
BCASE0: ((A1
. n)
/\ (A1
. k))
=
{} by
CASE000;
(A1
. n)
misses (A1
. k) by
BCASE0;
hence thesis;
end;
CASE1: for y be
object holds (for n be
Nat, k be
Nat holds y
in (A1
. k) & y
in (A1
. n)) iff y
in
{}
proof
let y be
object;
(for n be
Nat, k be
Nat holds y
in (A1
. k) & y
in (A1
. n)) implies y
in
{}
proof
assume
G1: for n be
Nat, k be
Nat holds y
in (A1
. k) & y
in (A1
. n);
ex n be
Nat, k be
Nat st y
in (A1
. k) & y
in (A1
. n) & y
in
{}
proof
consider n be
Nat, k be
Nat such that
H1: (A1
. n)
misses (A1
. k) by
CASE0;
(y
in (A1
. k) & y
in (A1
. n)) iff y
in
{} by
H1,
XBOOLE_0: 3;
hence thesis by
G1;
end;
hence thesis;
end;
hence thesis;
end;
(
Intersection A1)
c=
{}
proof
let y be
object;
y
in (
Intersection A1) iff (for n be
Nat, k be
Nat holds y
in (A1
. k) & y
in (A1
. n)) by
PROB_1: 13;
hence thesis by
CASE1;
end;
then (
Intersection A1)
=
{} ;
hence thesis by
ENUMSET1:def 2;
end;
suppose
CASE0: not ex n be
Nat, k be
Nat st ((A1
. n)
/\ (A1
. k))
=
{} ;
(
Intersection A1)
in
{
{} ,
{1, 2},
{3, 4},
{1, 2, 3, 4}}
proof
(
Intersection A1)
=
{} or (
Intersection A1)
=
{1, 2} or (
Intersection A1)
=
{3, 4} or (
Intersection A1)
=
{1, 2, 3, 4} by
CASE0,
A0,
Lm700000;
hence thesis by
ENUMSET1:def 2;
end;
hence thesis;
end;
end;
hence thesis by
A0;
end;
theorem ::
FINANCE3:21
Lm9: for MySigmaField,MySet be
set, A1 be
SetSequence of MySet st MySet
=
{1, 2, 3, 4} & (
rng A1)
c= MySigmaField & MySigmaField
=
{
{} ,
{1, 2, 3, 4}} holds (
Intersection A1)
<>
{} implies (
Intersection A1)
in MySigmaField
proof
let MySigmaField,MySet be
set;
let A1 be
SetSequence of MySet;
assume
A0: MySet
=
{1, 2, 3, 4} & (
rng A1)
c= MySigmaField & MySigmaField
=
{
{} ,
{1, 2, 3, 4}};
assume
A5: (
Intersection A1)
<>
{} ;
D1: (
dom A1)
=
NAT by
FUNCT_2:def 1;
A4: for n be
Nat holds (A1
. n)
=
{} or (A1
. n)
=
{1, 2, 3, 4}
proof
let n be
Nat;
(A1
. n)
in MySigmaField
proof
n
in (
dom A1) by
D1,
ORDINAL1:def 12;
hence thesis by
FUNCT_1: 3,
A0;
end;
hence thesis by
A0,
TARSKI:def 2;
end;
H1: (ex n be
Nat st (A1
. n)
=
{} ) implies (
Intersection A1)
=
{}
proof
assume ex n be
Nat st (A1
. n)
=
{} ;
then for x be
object holds x
in (
Intersection A1) iff x
in
{} by
PROB_1: 13;
hence thesis by
TARSKI:def 3;
end;
(
Intersection A1)
=
{1, 2, 3, 4}
proof
for x be
object holds x
in (
Intersection A1) iff x
in
{1, 2, 3, 4}
proof
let x be
object;
x
in (
Intersection A1) iff for n be
Nat holds x
in
{1, 2, 3, 4}
proof
thus x
in (
Intersection A1) implies for n be
Nat holds x
in
{1, 2, 3, 4}
proof
assume
G1: x
in (
Intersection A1);
for n be
Nat holds x
in
{1, 2, 3, 4}
proof
let n be
Nat;
for x be
object holds x
in (A1
. n) iff x
in
{1, 2, 3, 4} by
H1,
A4,
A5;
hence thesis by
PROB_1: 13,
G1;
end;
hence thesis;
end;
assume
G1: for n be
Nat holds x
in
{1, 2, 3, 4};
for n be
Nat holds x
in (A1
. n)
proof
let n be
Nat;
x
in
{1, 2, 3, 4} by
G1;
hence thesis by
H1,
A4,
A5;
end;
hence thesis by
PROB_1: 13;
end;
hence thesis;
end;
hence thesis by
TARSKI:def 3;
end;
hence thesis by
A0,
TARSKI:def 2;
end;
theorem ::
FINANCE3:22
for MySigmaField,MySet be
set, A1 be
SetSequence of MySet st MySet
=
{1, 2, 3, 4} & (
rng A1)
c= MySigmaField & MySigmaField
=
{
{} ,
{1, 2, 3, 4}} holds for k1 be
Nat, k2 be
Nat holds ((A1
. k1)
/\ (A1
. k2))
in MySigmaField
proof
let MySigmaField,MySet be
set;
let A1 be
SetSequence of MySet;
assume
A0: MySet
=
{1, 2, 3, 4} & (
rng A1)
c= MySigmaField & MySigmaField
=
{
{} ,
{1, 2, 3, 4}};
let k1,k2 be
Nat;
D1: (
dom A1)
=
NAT by
FUNCT_2:def 1;
then k1
in (
dom A1) by
ORDINAL1:def 12;
then
B1: (A1
. k1)
in MySigmaField by
FUNCT_1: 3,
A0;
k2
in (
dom A1) by
D1,
ORDINAL1:def 12;
then
B2: (A1
. k2)
in MySigmaField by
FUNCT_1: 3,
A0;
((A1
. k1)
/\ (A1
. k2))
in MySigmaField
proof
((A1
. k1)
=
{} or (A1
. k1)
=
{1, 2, 3, 4}) & ((A1
. k2)
=
{} or (A1
. k2)
=
{1, 2, 3, 4}) by
B2,
B1,
A0,
TARSKI:def 2;
hence thesis by
A0,
TARSKI:def 2;
end;
hence thesis;
end;
definition
::
FINANCE3:def6
func
Special_SigmaField1 ->
SigmaField of
{1, 2, 3, 4} equals
{
{} ,
{1, 2, 3, 4}};
correctness
proof
set MySigmaField =
{
{} ,
{1, 2, 3, 4}};
set ThisSigma = (
bool
{1, 2, 3, 4});
MySigmaField
c= (
bool
{1, 2, 3, 4})
proof
let x be
object;
assume
a1: x
in MySigmaField;
x
=
{} or x
=
{1, 2, 3, 4} by
a1,
TARSKI:def 2;
hence thesis by
PROB_1: 4,
PROB_1: 5;
end;
then
reconsider MySigmaField as
Subset-Family of
{1, 2, 3, 4};
A1: MySigmaField is
compl-closed
proof
for A be
Subset of
{1, 2, 3, 4} st A
in MySigmaField holds (A
` )
in MySigmaField
proof
let A be
Subset of
{1, 2, 3, 4};
assume A
in MySigmaField;
per cases by
TARSKI:def 2;
suppose A
=
{} ;
hence thesis by
TARSKI:def 2;
end;
suppose
B1: A
=
{1, 2, 3, 4};
(A
` )
=
{} by
B1,
XBOOLE_1: 37;
hence thesis by
TARSKI:def 2;
end;
end;
hence thesis;
end;
MySigmaField is
sigma-multiplicative
proof
for A1 be
SetSequence of
{1, 2, 3, 4} st (
rng A1)
c= MySigmaField holds (
Intersection A1)
in MySigmaField
proof
let A1 be
SetSequence of
{1, 2, 3, 4};
assume
B1: (
rng A1)
c= MySigmaField;
per cases ;
suppose (
Intersection A1)
=
{} ;
hence thesis by
TARSKI:def 2;
end;
suppose (
Intersection A1)
<>
{} ;
hence thesis by
B1,
Lm9;
end;
end;
hence thesis;
end;
hence thesis by
A1;
end;
end
definition
::
FINANCE3:def7
func
Special_SigmaField2 ->
SigmaField of
{1, 2, 3, 4} equals
{
{} ,
{1, 2},
{3, 4},
{1, 2, 3, 4}};
correctness
proof
set MyOmega =
{
{} ,
{1, 2},
{3, 4},
{1, 2, 3, 4}};
MyOmega is
Subset-Family of
{1, 2, 3, 4}
proof
for x be
object st x
in MyOmega holds x
in (
bool
{1, 2, 3, 4})
proof
let x be
object;
assume x
in MyOmega;
per cases by
ENUMSET1:def 2;
suppose x
=
{} ;
hence thesis by
PROB_1: 4;
end;
suppose x
=
{1, 2};
hence thesis by
Lm2;
end;
suppose x
=
{3, 4};
hence thesis by
Lm1;
end;
suppose x
=
{1, 2, 3, 4};
hence thesis by
ZFMISC_1:def 1;
end;
end;
hence thesis by
TARSKI:def 3;
end;
then
reconsider MyOmega as
Subset-Family of
{1, 2, 3, 4};
A1: MyOmega is
compl-closed
proof
for A be
Subset of
{1, 2, 3, 4} st A
in MyOmega holds (A
` )
in MyOmega
proof
let A be
Subset of
{1, 2, 3, 4};
assume A
in MyOmega;
per cases by
ENUMSET1:def 2;
suppose A
=
{} ;
hence thesis by
ENUMSET1:def 2;
end;
suppose A
=
{1, 2};
hence thesis by
Lem1,
ENUMSET1:def 2;
end;
suppose A
=
{3, 4};
hence thesis by
Lem2,
ENUMSET1:def 2;
end;
suppose
B300: A
=
{1, 2, 3, 4};
(A
` )
=
{}
proof
reconsider B =
{} as
Subset of
{1, 2, 3, 4} by
SUBSET_1: 1;
A
= (B
` ) by
B300;
hence thesis;
end;
hence thesis by
ENUMSET1:def 2;
end;
end;
hence thesis;
end;
MyOmega is
sigma-multiplicative by
Lm8;
hence thesis by
A1;
end;
end
definition
::$Canceled
end
theorem ::
FINANCE3:23
for Omega be
set st Omega
=
{1, 2, 3, 4} holds
{1}
c= Omega &
{2}
c= Omega &
{3}
c= Omega &
{4}
c= Omega &
{1, 2}
c= Omega &
{3, 4}
c= Omega &
{}
c= Omega & Omega
c= Omega
proof
let Omega be
set;
assume
A0: Omega
=
{1, 2, 3, 4};
then 1
in Omega & 2
in Omega & 3
in Omega & 4
in Omega by
ENUMSET1:def 2;
hence thesis by
A0,
Lemacik2,
ZFMISC_1: 31;
end;
theorem ::
FINANCE3:24
for Omega be
set st Omega
=
{1, 2, 3, 4} holds Omega
in
Special_SigmaField1 &
{}
in
Special_SigmaField1 &
{1, 2}
in
Special_SigmaField2 &
{3, 4}
in
Special_SigmaField2 & Omega
in
Special_SigmaField2 &
{}
in
Special_SigmaField2 & Omega
in (
Trivial-SigmaField
{1, 2, 3, 4}) &
{}
in (
Trivial-SigmaField
{1, 2, 3, 4}) &
{1}
in (
Trivial-SigmaField
{1, 2, 3, 4}) &
{2}
in (
Trivial-SigmaField
{1, 2, 3, 4}) &
{3}
in (
Trivial-SigmaField
{1, 2, 3, 4}) &
{4}
in (
Trivial-SigmaField
{1, 2, 3, 4}) by
EnLm1,
EnLm2,
EnLm3,
PROB_1: 5,
EnLm4,
PROB_1: 4,
ENUMSET1:def 2;
XX1:
{
{} ,
{1, 2, 3, 4}}
c<
{
{} ,
{1, 2},
{3, 4},
{1, 2, 3, 4}}
proof
{
{} ,
{1, 2, 3, 4}}
c= (
{
{} ,
{1, 2, 3, 4}}
\/
{
{1, 2}}) by
XBOOLE_0:def 3;
then
{
{} ,
{1, 2, 3, 4}}
c=
{
{} ,
{1, 2, 3, 4},
{1, 2}} by
ENUMSET1: 3;
then
{
{} ,
{1, 2, 3, 4}}
c= (
{
{} ,
{1, 2, 3, 4},
{1, 2}}
\/
{
{3, 4}}) by
XBOOLE_0:def 3;
then
Zw1:
{
{} ,
{1, 2, 3, 4}}
c=
{
{} ,
{1, 2, 3, 4},
{1, 2},
{3, 4}} by
ENUMSET1: 6;
T1:
{
{} ,
{1, 2, 3, 4}}
c=
{
{} ,
{1, 2},
{3, 4},
{1, 2, 3, 4}}
proof
for x be
object st x
in
{
{} ,
{1, 2, 3, 4}} holds x
in
{
{} ,
{1, 2},
{3, 4},
{1, 2, 3, 4}}
proof
let x be
object;
assume
ASS1: x
in
{
{} ,
{1, 2, 3, 4}};
x
=
{} or x
=
{1, 2, 3, 4} or x
=
{1, 2} or x
=
{3, 4} by
ASS1,
Zw1,
ENUMSET1:def 2;
hence thesis by
ENUMSET1:def 2;
end;
hence thesis;
end;
set y =
{1, 2};
C1: y
in
{
{} ,
{1, 2},
{3, 4},
{1, 2, 3, 4}} by
ENUMSET1:def 2;
{1, 2}
<>
{1, 2, 3, 4}
proof
3
in
{1, 2, 3, 4} & not 3
in
{1, 2} by
ENUMSET1:def 2,
TARSKI:def 2;
hence thesis;
end;
hence thesis by
T1,
C1,
TARSKI:def 2;
end;
XX2:
{
{} ,
{1, 2},
{3, 4},
{1, 2, 3, 4}}
c< (
bool
{1, 2, 3, 4})
proof
A2:
{
{1, 2, 3, 4}}
c= (
bool
{1, 2, 3, 4}) by
ZFMISC_1: 68;
{
{} ,
{1, 2},
{3, 4},
{1, 2, 3, 4}}
c= (
bool
{1, 2, 3, 4})
proof
set MyBool = (
bool
{1, 2, 3, 4});
reconsider MyBool as
SigmaField of
{1, 2, 3, 4};
for x be
object st x
in
{
{} ,
{1, 2},
{3, 4},
{1, 2, 3, 4}} holds x
in (
bool
{1, 2, 3, 4})
proof
let x be
object;
assume x
in
{
{} ,
{1, 2},
{3, 4},
{1, 2, 3, 4}};
per cases by
ENUMSET1:def 2;
suppose x
=
{} ;
hence thesis by
PROB_1: 4;
end;
suppose x
=
{1, 2};
hence thesis by
B25;
end;
suppose x
=
{3, 4};
hence thesis by
B26;
end;
suppose x
=
{1, 2, 3, 4};
then x
in
{
{1, 2, 3, 4}} by
TARSKI:def 1;
hence thesis by
A2;
end;
end;
hence thesis;
end;
hence thesis by
The0;
end;
theorem ::
FINANCE3:25
Special_SigmaField1
c<
Special_SigmaField2 &
Special_SigmaField2
c< (
Trivial-SigmaField
{1, 2, 3, 4}) by
XX1,
XX2;
theorem ::
FINANCE3:26
ex Omega be non
empty
set st ex F1,F2,F3 be
SigmaField of Omega st F1
c< F2 & F2
c< F3
proof
Special_SigmaField1
c<
Special_SigmaField2 by
XX1;
hence thesis by
XX2;
end;
theorem ::
FINANCE3:27
ex Omega1,Omega2,Omega3,Omega4 be non
empty
set st Omega1
c< Omega2 & Omega2
c< Omega3 & Omega3
c< Omega4 & (ex F1 be
SigmaField of Omega1, F2 be
SigmaField of Omega2, F3 be
SigmaField of Omega3, F4 be
SigmaField of Omega4 st F1
c= F2 & F2
c= F3 & F3
c= F4)
proof
set Omega1 =
{1};
set Omega2 =
{1, 2};
set Omega3 =
{1, 2, 3};
set Omega4 =
{1, 2, 3, 4};
reconsider F1 = (
bool Omega1) as
SigmaField of Omega1;
reconsider F2 = (
bool Omega2) as
SigmaField of Omega2;
reconsider F3 = (
bool Omega3) as
SigmaField of Omega3;
reconsider F4 = (
bool Omega4) as
SigmaField of Omega4;
ATh100: Omega1
c< Omega2 by
ZFMISC_1: 7,
ZFMISC_1: 20;
E10: F1
c= F2 by
ZFMISC_1: 7,
ZFMISC_1: 67;
E11: F2
c= F3 by
ATh101,
ZFMISC_1: 67;
F3
c= F4 by
ATh102,
ZFMISC_1: 67;
hence thesis by
ATh100,
ATh101,
ATh102,
E10,
E11;
end;
definition
let Omega be non
empty
set;
let Sigma be
SigmaField of Omega;
let I be non
empty
real-membered
set;
::
FINANCE3:def9
mode
Filtration of I,Sigma ->
ManySortedSigmaField of I, Sigma means
:
Def2000: for s,t be
Element of I st s
<= t holds (it
. s) is
Subset of (it
. t);
existence
proof
set C = Sigma;
A1:
{Sigma}
c= (
bool Sigma) by
ZFMISC_1: 68;
C is
Element of (
bool Sigma)
proof
Sigma
in
{Sigma} by
TARSKI:def 1;
hence thesis by
A1;
end;
then
reconsider C as
Element of (
bool Sigma);
set const = (I
--> C);
reconsider const as
Function of I, (
bool Sigma);
Z1: for i be
set st i
in I holds (const
. i) is
SigmaField of Omega by
FUNCOP_1: 7;
T1: const is
ManySortedSigmaField of I, Sigma by
Z1,
KOLMOG01:def 2;
for x,y be
Element of I st x
<= y holds (const
. x) is
Subset of (const
. y)
proof
let x,y be
Element of I;
assume x
<= y;
(const
. x)
= C & (const
. y)
= C by
FUNCOP_1: 7;
hence thesis;
end;
hence thesis by
T1;
end;
end
definition
let I,Omega be non
empty
set;
let Sigma be
SigmaField of Omega;
let Filt be
ManySortedSigmaField of I, Sigma;
let i be
Element of I;
::
FINANCE3:def10
func
El_Filtration (i,Filt) ->
SigmaField of Omega equals (Filt
. i);
correctness by
KOLMOG01:def 2;
end
definition
let k be
Element of
{1, 2, 3};
::
FINANCE3:def11
func
Set1_of_SigmaField3 (k) ->
Subset of (
bool
{1, 2, 3, 4}) equals
:
Def8:
Special_SigmaField1 if k
= 1
otherwise
Special_SigmaField2 ;
correctness ;
end
definition
let k be
Element of
{1, 2, 3};
::
FINANCE3:def12
func
Set2_of_SigmaField3 (k) ->
Subset of (
bool
{1, 2, 3, 4}) equals
:
Def9: (
Set1_of_SigmaField3 k) if k
<= 2
otherwise (
Trivial-SigmaField
{1, 2, 3, 4});
correctness ;
end
Th3: for Sigma be
SigmaField of
{1, 2, 3, 4}, I be
set st I
=
{1, 2, 3} & Sigma
= (
bool
{1, 2, 3, 4}) holds ex MyFunc be
ManySortedSigmaField of I, Sigma st (MyFunc
. 1)
=
Special_SigmaField1 & (MyFunc
. 2)
=
Special_SigmaField2 & (MyFunc
. 3)
= (
Trivial-SigmaField
{1, 2, 3, 4})
proof
let Sigma be
SigmaField of
{1, 2, 3, 4};
let I be
set;
assume
ASS2: I
=
{1, 2, 3} & Sigma
= (
bool
{1, 2, 3, 4});
deffunc
U(
Element of
{1, 2, 3}) = (
Set2_of_SigmaField3 $1);
consider fI1 be
Function of
{1, 2, 3}, (
bool (
bool
{1, 2, 3, 4})) such that
A1: for d be
Element of
{1, 2, 3} holds (fI1
. d)
=
U(d) from
FUNCT_2:sch 4;
reconsider fI1 as
Function of I, (
bool Sigma) by
ASS2;
reconsider El1 = 1 as
Element of
{1, 2, 3} by
ENUMSET1:def 1;
A20: (fI1
. 1)
= (
Set2_of_SigmaField3 El1) by
A1;
F1: (
Set2_of_SigmaField3 El1)
= (
Set1_of_SigmaField3 El1) by
Def9;
reconsider El1 = 2 as
Element of
{1, 2, 3} by
ENUMSET1:def 1;
A200: (fI1
. 2)
= (
Set2_of_SigmaField3 El1) by
A1;
F2: (
Set2_of_SigmaField3 El1)
= (
Set1_of_SigmaField3 El1) by
Def9;
reconsider El1 = 3 as
Element of
{1, 2, 3} by
ENUMSET1:def 1;
A2: (fI1
. 3)
= (
Set2_of_SigmaField3 El1) by
A1;
reconsider fI1 as
Function of I, (
bool Sigma);
for i be
set st i
in I holds (fI1
. i) is
SigmaField of
{1, 2, 3, 4}
proof
let i be
set;
assume
B1: i
in I;
(fI1
. i) is
SigmaField of
{1, 2, 3, 4}
proof
per cases by
B1,
ASS2,
ENUMSET1:def 1;
suppose i
= 1;
hence thesis by
F1,
Def8,
A20;
end;
suppose i
= 2;
hence thesis by
F2,
Def8,
A200;
end;
suppose i
= 3;
hence thesis by
Def9,
A2;
end;
end;
hence thesis;
end;
then
reconsider fI1 as
ManySortedSigmaField of I, Sigma by
KOLMOG01:def 2;
take fI1;
thus thesis by
F1,
Def8,
A20,
F2,
A200,
Def9,
A2;
end;
theorem ::
FINANCE3:28
MyNeed: for Omega be non
empty
set, Sigma be
SigmaField of Omega, I be non
empty
real-membered
set st I
=
{1, 2, 3} & Sigma
= (
bool
{1, 2, 3, 4}) & Omega
=
{1, 2, 3, 4} holds ex MyFunc be
Filtration of I, Sigma st (MyFunc
. 1)
=
Special_SigmaField1 & (MyFunc
. 2)
=
Special_SigmaField2 & (MyFunc
. 3)
= (
Trivial-SigmaField
{1, 2, 3, 4})
proof
let Omega be non
empty
set;
let Sigma be
SigmaField of Omega;
let I be non
empty
real-membered
set;
assume
A0: I
=
{1, 2, 3} & Sigma
= (
bool
{1, 2, 3, 4}) & Omega
=
{1, 2, 3, 4};
consider MyFunc be
ManySortedSigmaField of I, Sigma such that
A1: (MyFunc
. 1)
=
Special_SigmaField1 & (MyFunc
. 2)
=
Special_SigmaField2 & (MyFunc
. 3)
= (
Trivial-SigmaField
{1, 2, 3, 4}) by
A0,
Th3;
A3: for s,t be
Element of I st s
<= t holds (MyFunc
. s) is
Subset of (MyFunc
. t)
proof
let s,t be
Element of I;
assume
B1: s
<= t;
per cases by
A0,
ENUMSET1:def 1;
suppose
SUPP1: s
= 1;
per cases by
A0,
ENUMSET1:def 1;
suppose t
= 1;
then (MyFunc
. t)
= (MyFunc
. 1) & (MyFunc
. s)
= (MyFunc
. 1) by
SUPP1;
hence thesis;
end;
suppose t
= 2 or t
= 3;
hence thesis by
SUPP1,
A1,
XX1;
end;
end;
suppose
SUPP1: s
= 2;
per cases by
A0,
ENUMSET1:def 1;
suppose t
= 1;
hence thesis by
SUPP1,
B1;
end;
suppose t
= 2;
then (MyFunc
. t)
= (MyFunc
. 2) & (MyFunc
. s)
= (MyFunc
. 2) by
SUPP1;
hence thesis;
end;
suppose t
= 3;
hence thesis by
SUPP1,
A1;
end;
end;
suppose
SUPP1: s
= 3;
per cases by
A0,
ENUMSET1:def 1;
suppose t
= 1 or t
= 2;
hence thesis by
SUPP1,
B1;
end;
suppose t
= 3;
then (MyFunc
. t)
= (MyFunc
. 3) & (MyFunc
. s)
= (MyFunc
. 3) by
SUPP1;
hence thesis;
end;
end;
end;
MyFunc is
Filtration of I, Sigma by
A3,
Def2000;
hence thesis by
A1;
end;
Lm1A: for Omega,Omega2 be non
empty
set, F be
Function of Omega, Omega2, y be non
empty
set holds { z where z be
Element of Omega : (F
. z) is
Element of y }
= (F
" y)
proof
let Omega,Omega2 be non
empty
set, F be
Function of Omega, Omega2, y be non
empty
set;
set D = { z where z be
Element of Omega : (F
. z) is
Element of y };
for x be
object holds x
in D iff x
in (F
" y)
proof
let x be
object;
hereby
assume x
in D;
then
consider z be
Element of Omega such that
A1: x
= z & (F
. z) is
Element of y;
z
in Omega;
then z
in (
dom F) by
FUNCT_2:def 1;
hence x
in (F
" y) by
A1,
FUNCT_1:def 7;
end;
assume x
in (F
" y);
then x
in (
dom F) & (F
. x)
in y by
FUNCT_1:def 7;
hence x
in D;
end;
hence thesis by
TARSKI: 2;
end;
Lm2A: for Omega be non
empty
set, Sigma4 be
SigmaField of Omega, Sigma5 be
SigmaField of
{1} holds (Omega
--> 1) is
random_variable of Sigma4, Sigma5
proof
let Omega be non
empty
set;
let Sigma4 be
SigmaField of Omega;
let Sigma5 be
SigmaField of
{1};
set 1REAL = 1;
reconsider 1REAL as
Real;
reconsider X = (Omega
--> 1REAL) as
Function of Omega,
{1};
X is Sigma4, Sigma5
-random_variable-like
proof
let x be
set;
per cases ;
suppose
A1: 1
in x;
for q be
object holds q
in { w where w be
Element of Omega : (X
. w) is
Element of x } iff q
in Omega
proof
let q be
object;
hereby
assume q
in { w where w be
Element of Omega : (X
. w) is
Element of x };
then ex w be
Element of Omega st w
= q & (X
. w) is
Element of x;
hence q
in Omega;
end;
assume q
in Omega;
then
reconsider w = q as
Element of Omega;
(X
. w) is
Element of x by
A1,
FUNCOP_1: 7;
hence thesis;
end;
then
A2: { w where w be
Element of Omega : (X
. w) is
Element of x }
= Omega by
TARSKI: 2;
{ w where w be
Element of Omega : (X
. w) is
Element of x }
= (X
" x) by
A1,
Lm1A;
then (X
" x) is
Element of Sigma4 by
A2,
PROB_1: 23;
hence thesis;
end;
suppose
A3: not 1
in x;
(X
" x)
c=
{}
proof
let q be
object;
assume q
in (X
" x);
then q
in (
dom X) & (X
. q)
in x by
FUNCT_1:def 7;
hence q
in
{} by
A3,
FUNCOP_1: 7;
end;
then (X
" x)
=
{} ;
then (X
" x) is
Element of Sigma4 by
PROB_1: 22;
hence thesis;
end;
end;
hence thesis;
end;
theorem ::
FINANCE3:29
THJ1: for Omega be non
empty
set, Sigma be
SigmaField of Omega, Sigma2 be
SigmaField of
{1} st Omega
=
{1, 2, 3, 4} holds ex X1 be
Function of Omega,
{1} st X1 is
random_variable of
Special_SigmaField1 , Sigma2 & X1 is
random_variable of
Special_SigmaField2 , Sigma2 & X1 is
random_variable of (
Trivial-SigmaField
{1, 2, 3, 4}), Sigma2
proof
let Omega be non
empty
set;
let Sigma be
SigmaField of Omega;
let Sigma2 be
SigmaField of
{1};
assume
A1: Omega
=
{1, 2, 3, 4};
reconsider 1REAL = 1 as
Real;
consider X1 be
Function of Omega,
{1REAL} such that
F4: X1
= (Omega
--> 1REAL);
reconsider X1 as
Function of Omega,
{1};
take X1;
thus thesis by
A1,
Lm2A,
F4;
end;
theorem ::
FINANCE3:30
ex Omega,Omega2 be non
empty
set, Sigma be
SigmaField of Omega, Sigma2 be
SigmaField of Omega2, I be non
empty
real-membered
set, Q be
Filtration of I, Sigma st ex rv be
Function of Omega, Omega2 st for i be
Element of I holds rv is
random_variable of (
El_Filtration (i,Q)), Sigma2
proof
set Omega =
{1, 2, 3, 4};
set Omega2 =
{1};
consider Sigma be
SigmaField of Omega such that
A3: Sigma
= (
bool Omega);
reconsider Sigma2 = (
bool Omega2) as non
empty
set;
reconsider Sigma2 as
SigmaField of Omega2;
consider I be non
empty
real-membered
set such that
A5: I
=
{1, 2, 3};
consider MyFunc be
Filtration of I, Sigma such that
A6: (MyFunc
. 1)
=
Special_SigmaField1 & (MyFunc
. 2)
=
Special_SigmaField2 & (MyFunc
. 3)
= (
Trivial-SigmaField
{1, 2, 3, 4}) by
A3,
A5,
MyNeed;
consider X1 be
Function of Omega,
{1} such that
A7: X1 is
random_variable of
Special_SigmaField1 , Sigma2 & X1 is
random_variable of
Special_SigmaField2 , Sigma2 & X1 is
random_variable of (
Trivial-SigmaField
{1, 2, 3, 4}), Sigma2 by
THJ1;
F2: for i be
Element of I holds X1 is
random_variable of (
El_Filtration (i,MyFunc)), Sigma2
proof
let i be
Element of I;
i
= 1 or i
= 2 or i
= 3 by
A5,
ENUMSET1:def 1;
hence thesis by
A6,
A7;
end;
take Omega, Omega2, Sigma, Sigma2;
thus thesis by
F2;
end;
theorem ::
FINANCE3:31
for Omega,Omega2 be non
empty
set, Sigma be
SigmaField of Omega, Sigma2 be
SigmaField of Omega2, I be non
empty
real-membered
set, Q be
ManySortedSigmaField of I, Sigma holds ex rv be
Function of Omega, Omega2 st for i be
Element of I holds rv is
random_variable of (
El_Filtration (i,Q)), Sigma2
proof
let Omega,Omega2 be non
empty
set;
let Sigma be
SigmaField of Omega;
let Sigma2 be
SigmaField of Omega2;
let I be non
empty
real-membered
set;
let Q be
ManySortedSigmaField of I, Sigma;
consider w be
object such that
A00: w
in Omega2 by
XBOOLE_0:def 1;
reconsider w as
Element of Omega2 by
A00;
set myset = w;
deffunc
U(
Element of Omega) = myset;
consider myfunc be
Function of Omega, Omega2 such that
B3: myfunc
= (Omega
--> myset);
take myfunc;
let i be
Element of I;
myfunc is (
El_Filtration (i,Q)), Sigma2
-random_variable-like
proof
for x be
set st x
in Sigma2 holds (myfunc
" x)
in (
El_Filtration (i,Q))
proof
let x be
set;
assume x
in Sigma2;
per cases ;
suppose
CAS0: myset
in x;
H1: (myfunc
" x)
= Omega
proof
for y be
object holds y
in (myfunc
" x) iff y
in Omega
proof
let y be
object;
y
in Omega implies y
in (myfunc
" x)
proof
assume
I0: y
in Omega;
then
I1: y
in (
dom myfunc) by
FUNCT_2:def 1;
(myfunc
. y)
in x by
I0,
B3,
FUNCOP_1: 7,
CAS0;
hence thesis by
I1,
FUNCT_1:def 7;
end;
hence thesis;
end;
hence thesis by
TARSKI:def 3;
end;
(myfunc
" x)
in (Q
. i)
proof
(Q
. i) is
SigmaField of Omega by
KOLMOG01:def 2;
hence thesis by
H1,
PROB_1: 5;
end;
hence thesis;
end;
suppose
CAS1: not myset
in x;
(myfunc
" x)
c=
{}
proof
let z be
object;
assume z
in (myfunc
" x);
then z
in (
dom myfunc) & (myfunc
. z)
in x & (myfunc
. z)
= myset by
FUNCT_1:def 7,
B3,
FUNCOP_1: 7;
hence thesis by
CAS1;
end;
then (myfunc
" x)
=
{} ;
hence thesis by
PROB_1: 4;
end;
end;
hence thesis;
end;
hence thesis;
end;
theorem ::
FINANCE3:32
for Omega be non
empty
set, Sigma be
SigmaField of Omega, Sigma2 be
SigmaField of Omega st Sigma2
c= Sigma holds for E2 be
Event of Sigma2 holds E2 is
Event of Sigma;
definition
let Omega,Omega2 be non
empty
set, Sigma be
SigmaField of Omega, Sigma2 be
SigmaField of Omega2, I be non
empty
real-membered
set;
::
FINANCE3:def13
mode
Stochastic_Process of I,Sigma,Sigma2 ->
Function of I, (
set_of_random_variables_on (Sigma,Sigma2)) means
:
Def30000: for k be
Element of I holds ex RV be
Function of Omega, Omega2 st (it
. k)
= RV & RV is Sigma, Sigma2
-random_variable-like;
existence
proof
set q = the
Element of Omega2;
set F = (Omega
--> q);
A1: F is Sigma, Sigma2
-random_variable-like by
1A5;
F
in (
set_of_random_variables_on (Sigma,Sigma2)) by
A1;
then
reconsider F as
Element of (
set_of_random_variables_on (Sigma,Sigma2));
deffunc
U(
Element of I) = F;
consider fI1 be
Function of I, (
set_of_random_variables_on (Sigma,Sigma2)) such that
B1: for d be
Element of I holds (fI1
. d)
=
U(d) from
FUNCT_2:sch 4;
for k be
Element of I holds ex RV be
Function of Omega, Omega2 st (fI1
. k)
= RV & RV is Sigma, Sigma2
-random_variable-like by
A1,
B1;
hence thesis;
end;
end
definition
let Omega,Omega2 be non
empty
set, Sigma be
SigmaField of Omega, Sigma2 be
SigmaField of Omega2, I be non
empty
real-membered
set, Stoch be
Stochastic_Process of I, Sigma, Sigma2, k be
Element of I;
::
FINANCE3:def14
func
RVProcess (Stoch,k) ->
random_variable of Sigma, Sigma2 equals (Stoch
. k);
coherence
proof
consider RV be
Function of Omega, Omega2 such that
A0: (Stoch
. k)
= RV & RV is Sigma, Sigma2
-random_variable-like by
Def30000;
thus thesis by
A0;
end;
end
definition
let Omega,Omega2 be non
empty
set, Sigma be
SigmaField of Omega, Sigma2 be
SigmaField of Omega2, I be non
empty
real-membered
set, Stoch be
Stochastic_Process of I, Sigma, Sigma2;
::
FINANCE3:def15
mode
Adapted_Stochastic_Process of Stoch ->
Function of I, (
set_of_random_variables_on (Sigma,Sigma2)) means
:
Def30002: ex k be
Filtration of I, Sigma st for i be
Element of I holds (
RVProcess (Stoch,i)) is (
El_Filtration (i,k)), Sigma2
-random_variable-like;
existence
proof
set MyBool = (
bool Sigma);
D0:
{Sigma}
c= (
bool Sigma) by
ZFMISC_1: 68;
Sigma
in
{Sigma} by
TARSKI:def 1;
then
reconsider Sigma as
Element of MyBool by
D0;
set F = (I
--> Sigma);
reconsider Sigma as
SigmaField of Omega;
W2: for i be
Element of I holds (F
. i)
= Sigma by
FUNCOP_1: 7;
for i be
set st i
in I holds (F
. i) is
SigmaField of Omega by
FUNCOP_1: 7;
then
reconsider F as
ManySortedSigmaField of I, Sigma by
KOLMOG01:def 2;
WW1: for s,t be
Element of I st s
<= t holds (F
. s) is
Subset of (F
. t)
proof
let s,t be
Element of I;
assume s
<= t;
(F
. s)
= Sigma by
FUNCOP_1: 7;
hence thesis by
FUNCOP_1: 7;
end;
F is
Filtration of I, Sigma by
WW1,
Def2000;
then
consider F be
Filtration of I, Sigma such that
C0: for i be
Element of I holds (F
. i)
= Sigma by
W2;
for i be
Element of I holds (
RVProcess (Stoch,i)) is (
El_Filtration (i,F)), Sigma2
-random_variable-like
proof
let i be
Element of I;
(
El_Filtration (i,F))
= Sigma by
C0;
hence thesis;
end;
hence thesis;
end;
end
definition
let Omega,Omega2 be non
empty
set;
let Sigma be
SigmaField of Omega;
let Sigma2 be
SigmaField of Omega2;
let I,J be non
empty
Subset of
NAT ;
let Stoch be
Stochastic_Process of (
In (J,(
bool
REAL ))), Sigma, Sigma2;
::
FINANCE3:def16
mode
Predictable_Stochastic_Process of I,J,Sigma,Sigma2,Stoch ->
Function of J, (
set_of_random_variables_on (Sigma,Sigma2)) means ex k be
Filtration of (
In (I,(
bool
REAL ))), Sigma st for j be
Element of (
In (J,(
bool
REAL ))), i be
Element of (
In (I,(
bool
REAL ))) st (j
- 1)
= i holds (
RVProcess (Stoch,j)) is (
El_Filtration (i,k)), Sigma2
-random_variable-like;
existence
proof
set MyBool = (
bool Sigma);
D0:
{Sigma}
c= (
bool Sigma) by
ZFMISC_1: 68;
Sigma
in
{Sigma} by
TARSKI:def 1;
then
reconsider Sigma as
Element of MyBool by
D0;
set F = ((
In (I,(
bool
REAL )))
--> Sigma);
reconsider Sigma as
SigmaField of Omega;
W2: for i be
Element of (
In (I,(
bool
REAL ))) holds (F
. i)
= Sigma by
FUNCOP_1: 7;
for i be
set st i
in (
In (I,(
bool
REAL ))) holds (F
. i) is
SigmaField of Omega by
FUNCOP_1: 7;
then
reconsider F as
ManySortedSigmaField of (
In (I,(
bool
REAL ))), Sigma by
KOLMOG01:def 2;
for s,t be
Element of (
In (I,(
bool
REAL ))) st s
<= t holds (F
. s) is
Subset of (F
. t)
proof
let s,t be
Element of (
In (I,(
bool
REAL )));
assume s
<= t;
(F
. s)
= Sigma by
FUNCOP_1: 7;
hence thesis by
FUNCOP_1: 7;
end;
then F is
Filtration of (
In (I,(
bool
REAL ))), Sigma by
Def2000;
then
consider F be
Filtration of (
In (I,(
bool
REAL ))), Sigma such that
C0: for i be
Element of (
In (I,(
bool
REAL ))) holds (F
. i)
= Sigma by
W2;
for j be
Element of (
In (J,(
bool
REAL ))), i be
Element of (
In (I,(
bool
REAL ))) st (j
- 1)
= i holds (
RVProcess (Stoch,j)) is (
El_Filtration (i,F)), Sigma2
-random_variable-like
proof
let j be
Element of (
In (J,(
bool
REAL )));
let i be
Element of (
In (I,(
bool
REAL )));
assume (j
- 1)
= i;
Sigma
= (
El_Filtration (i,F)) by
C0;
hence thesis;
end;
hence thesis;
end;
end
definition
let Omega,Omega2 be non
empty
set;
let Sigma be
SigmaField of Omega;
let Sigma2 be
SigmaField of Omega2;
let I be non
empty
real-membered
set;
let MyFunc be
ManySortedSigmaField of I, Sigma;
let Stoch be
Stochastic_Process of I, Sigma, Sigma2;
::
FINANCE3:def17
attr Stoch is MyFunc
-stoch_proc_wrt_to_Filtration means for i be
Element of I holds (
RVProcess (Stoch,i)) is (
El_Filtration (i,MyFunc)), Sigma2
-random_variable-like;
end
theorem ::
FINANCE3:33
for Omega,Omega2 be non
empty
set, Sigma be
SigmaField of Omega, Sigma2 be
SigmaField of Omega2, I be non
empty
real-membered
set, MyFunc be
Filtration of I, Sigma, Stoch be
Stochastic_Process of I, Sigma, Sigma2 st Stoch is MyFunc
-stoch_proc_wrt_to_Filtration holds Stoch is
Adapted_Stochastic_Process of Stoch by
Def30002;
definition
let k1,k2 be
Element of
REAL ;
let Omega be non
empty
set;
let k be
Element of Omega;
::
FINANCE3:def18
func
Set1_for_RandomVariable (k1,k2,k) ->
Element of
REAL equals k1 if (k
= 1 or k
= 2)
otherwise k2;
correctness ;
::
FINANCE3:def19
func
Set4_for_RandomVariable (k1,k2,k) ->
Element of
REAL equals
:
Def79: k1 if k
= 3
otherwise k2;
correctness ;
end
definition
let k2,k3,k4 be
Element of
REAL ;
let Omega be non
empty
set;
let k be
Element of Omega;
::
FINANCE3:def20
func
Set3_for_RandomVariable (k2,k3,k4,k) ->
Element of
REAL equals
:
Def78: k2 if k
= 2
otherwise (
Set4_for_RandomVariable (k3,k4,k));
correctness ;
end
definition
let k1,k2,k3,k4 be
Element of
REAL ;
let Omega be non
empty
set;
let k be
Element of Omega;
::
FINANCE3:def21
func
Set2_for_RandomVariable (k1,k2,k3,k4,k) ->
Element of
REAL equals
:
Def77: k1 if k
= 1
otherwise (
Set3_for_RandomVariable (k2,k3,k4,k));
correctness ;
end
theorem ::
FINANCE3:34
MYF30: for k1,k2,k3,k4 be
Element of
REAL holds for Omega be
set st Omega
=
{1, 2, 3, 4} holds ex f be
Function of Omega,
REAL st (f
. 1)
= k1 & (f
. 2)
= k2 & (f
. 3)
= k3 & (f
. 4)
= k4
proof
let k1,k2,k3,k4 be
Element of
REAL ;
let Omega be
set;
assume
ASS: Omega
=
{1, 2, 3, 4};
A1: 1
in Omega by
ENUMSET1:def 2,
ASS;
A2: 2
in Omega by
ENUMSET1:def 2,
ASS;
A3: 3
in Omega by
ENUMSET1:def 2,
ASS;
A4: 4
in Omega by
ENUMSET1:def 2,
ASS;
reconsider Omega as non
empty
set by
ASS;
deffunc
U(
Element of Omega) = (
Set2_for_RandomVariable (k1,k2,k3,k4,$1));
consider f be
Function of Omega,
REAL such that
B1: for d be
Element of Omega holds (f
. d)
=
U(d) from
FUNCT_2:sch 4;
B2: (f
. 1)
= k1
proof
consider k be
Element of Omega such that
C1: k
= 1 by
A1;
(f
. k)
= (
Set2_for_RandomVariable (k1,k2,k3,k4,k)) by
B1;
hence thesis by
C1,
Def77;
end;
B3: (f
. 2)
= k2
proof
consider k be
Element of Omega such that
C1: k
= 2 by
A2;
(f
. 2)
= (
Set2_for_RandomVariable (k1,k2,k3,k4,k)) & k
= 2 by
B1,
C1;
then (f
. 2)
= (
Set3_for_RandomVariable (k2,k3,k4,k)) & k
= 2 by
Def77;
hence thesis by
Def78;
end;
B4: (f
. 3)
= k3
proof
consider k be
Element of Omega such that
C1: k
= 3 by
A3;
(f
. k)
= (
Set2_for_RandomVariable (k1,k2,k3,k4,k)) by
B1;
then (f
. 3)
= (
Set3_for_RandomVariable (k2,k3,k4,k)) & k
= 3 by
C1,
Def77;
then (f
. 3)
= (
Set4_for_RandomVariable (k3,k4,k)) & k
= 3 by
Def78;
hence thesis by
Def79;
end;
(f
. 4)
= k4
proof
consider k be
Element of Omega such that
C1: k
= 4 by
A4;
(f
. k)
= (
Set2_for_RandomVariable (k1,k2,k3,k4,k)) by
B1;
then (f
. 4)
= (
Set3_for_RandomVariable (k2,k3,k4,k)) & k
= 4 by
C1,
Def77;
then (f
. 4)
= (
Set4_for_RandomVariable (k3,k4,k)) & k
= 4 by
Def78;
hence thesis by
Def79;
end;
hence thesis by
B2,
B3,
B4;
end;
theorem ::
FINANCE3:35
MyFunc5: for k1,k2,k3,k4 be
Element of
REAL holds for Omega be non
empty
set st Omega
=
{1, 2, 3, 4} holds for Sigma be
SigmaField of Omega, I be non
empty
real-membered
set, MyFunc be
ManySortedSigmaField of I, Sigma st (MyFunc
. 1)
=
Special_SigmaField1 & (MyFunc
. 2)
=
Special_SigmaField2 & (MyFunc
. 3)
= (
Trivial-SigmaField
{1, 2, 3, 4}) holds for eli be
Element of I st eli
= 3 holds ex f be
Function of Omega,
REAL st (f
. 1)
= k1 & (f
. 2)
= k2 & (f
. 3)
= k3 & (f
. 4)
= k4 & f is (
El_Filtration (eli,MyFunc)),
Borel_Sets
-random_variable-like
proof
let k1,k2,k3,k4 be
Element of
REAL ;
let Omega be non
empty
set;
assume
A0: Omega
=
{1, 2, 3, 4};
let Sigma be
SigmaField of Omega;
let I be non
empty
real-membered
set;
let MyFunc be
ManySortedSigmaField of I, Sigma;
assume
A2: (MyFunc
. 1)
=
Special_SigmaField1 & (MyFunc
. 2)
=
Special_SigmaField2 & (MyFunc
. 3)
= (
Trivial-SigmaField
{1, 2, 3, 4});
let eli be
Element of I;
assume
A4: eli
= 3;
consider f be
Function of Omega,
REAL such that
A3: (f
. 1)
= k1 & (f
. 2)
= k2 & (f
. 3)
= k3 & (f
. 4)
= k4 by
A0,
MYF30;
II0: for x be
object holds x
in (
dom f) implies (x
= 1 or x
= 2 or x
= 3 or x
= 4) by
A0,
ENUMSET1:def 2;
II: 1
in (
dom f) & 2
in (
dom f) & 3
in (
dom f) & 4
in (
dom f)
proof
(
dom f)
=
{1, 2, 3, 4} by
FUNCT_2:def 1,
A0;
hence thesis by
ENUMSET1:def 2;
end;
f is (
El_Filtration (eli,MyFunc)),
Borel_Sets
-random_variable-like
proof
set i = eli;
for x be
set holds (f
" x)
in (
El_Filtration (i,MyFunc))
proof
let x be
set;
(f
" x)
in (MyFunc
. i)
proof
(f
" x)
in (
bool
{1, 2, 3, 4})
proof
per cases ;
suppose
ASUPP1: k1
in x;
per cases ;
suppose
BSUPP1: k2
in x;
per cases ;
suppose
CSUPP1: k3
in x;
per cases ;
suppose
DSUPP1: k4
in x;
for z be
object holds z
in
{1, 2, 3, 4} iff ex y be
object st
[z, y]
in f & y
in x
proof
let z be
object;
thus z
in
{1, 2, 3, 4} implies ex y be
object st
[z, y]
in f & y
in x
proof
assume z
in
{1, 2, 3, 4};
then z
in (
dom f) by
FUNCT_2:def 1,
A0;
then
consider y be
object such that
K01: y
= (f
. z) & z
in (
dom f);
Fin1:
[z, y]
in f by
K01,
FUNCT_1: 1;
y
in x by
K01,
A0,
ENUMSET1:def 2,
A3,
ASUPP1,
BSUPP1,
CSUPP1,
DSUPP1;
hence thesis by
Fin1;
end;
given y be
object such that
U000:
[z, y]
in f & y
in x;
z
= 1 or z
= 2 or z
= 3 or z
= 4 by
U000,
FUNCT_1: 1,
II0;
hence thesis by
ENUMSET1:def 2;
end;
then (f
" x)
=
{1, 2, 3, 4} by
RELAT_1:def 14;
hence thesis;
end;
suppose
DSUPP2: not k4
in x;
for z be
object holds z
in
{1, 2, 3} iff ex y be
object st
[z, y]
in f & y
in x
proof
let z be
object;
thus z
in
{1, 2, 3} implies ex y be
object st
[z, y]
in f & y
in x
proof
assume z
in
{1, 2, 3};
then
SS: z
= 1 or z
= 2 or z
= 3 by
ENUMSET1:def 1;
then
consider y be
object such that
K01: y
= (f
. z) & z
in (
dom f) by
II;
[z, y]
in f by
K01,
FUNCT_1: 1;
hence thesis by
A3,
ASUPP1,
K01,
BSUPP1,
CSUPP1,
SS;
end;
given y be
object such that
U000:
[z, y]
in f & y
in x;
z
<> 4 by
A3,
U000,
FUNCT_1: 1,
DSUPP2;
then z
= 1 or z
= 2 or z
= 3 by
U000,
FUNCT_1: 1,
II0;
hence thesis by
ENUMSET1:def 1;
end;
hence thesis by
B123,
RELAT_1:def 14;
end;
end;
suppose
CSUPP2: not k3
in x;
per cases ;
suppose
DSUPP1: k4
in x;
for z be
object holds z
in
{1, 2, 4} iff ex y be
object st
[z, y]
in f & y
in x
proof
let z be
object;
thus z
in
{1, 2, 4} implies ex y be
object st
[z, y]
in f & y
in x
proof
assume z
in
{1, 2, 4};
then
SS: z
= 1 or z
= 2 or z
= 4 by
ENUMSET1:def 1;
then
consider y be
object such that
K01: y
= (f
. z) & z
in (
dom f) by
II;
[z, y]
in f by
K01,
FUNCT_1: 1;
hence thesis by
SS,
A3,
ASUPP1,
K01,
BSUPP1,
DSUPP1;
end;
given y be
object such that
U000:
[z, y]
in f & y
in x;
z
<> 3 by
A3,
U000,
FUNCT_1: 1,
CSUPP2;
then z
= 1 or z
= 2 or z
= 4 by
II0,
U000,
FUNCT_1: 1;
hence thesis by
ENUMSET1:def 1;
end;
hence thesis by
B124,
RELAT_1:def 14;
end;
suppose
DSUPP2: not k4
in x;
Fin1: for z be
object holds z
in
{1, 2} iff ex y be
object st
[z, y]
in f & y
in x
proof
let z be
object;
thus z
in
{1, 2} implies ex y be
object st
[z, y]
in f & y
in x
proof
assume z
in
{1, 2};
then
SS: z
= 1 or z
= 2 by
TARSKI:def 2;
then
consider y be
object such that
K01: y
= (f
. z) & z
in (
dom f) by
II;
[z, y]
in f by
K01,
FUNCT_1: 1;
hence thesis by
A3,
ASUPP1,
K01,
BSUPP1,
SS;
end;
given y be
object such that
U000:
[z, y]
in f & y
in x;
z
<> 3 & z
<> 4 by
A3,
U000,
FUNCT_1: 1,
CSUPP2,
DSUPP2;
then z
= 1 or z
= 2 by
U000,
FUNCT_1: 1,
II0;
hence thesis by
TARSKI:def 2;
end;
{1, 2}
in (
bool
{1, 2, 3, 4}) by
Lm2;
hence thesis by
Fin1,
RELAT_1:def 14;
end;
end;
end;
suppose
BSUPP1: not k2
in x;
per cases ;
suppose
CSUPP1: k3
in x;
per cases ;
suppose
DSUPP1: k4
in x;
for z be
object holds z
in
{1, 3, 4} iff ex y be
object st
[z, y]
in f & y
in x
proof
let z be
object;
thus z
in
{1, 3, 4} implies ex y be
object st
[z, y]
in f & y
in x
proof
assume z
in
{1, 3, 4};
then
SS: z
= 1 or z
= 3 or z
= 4 by
ENUMSET1:def 1;
then
consider y be
object such that
K01: y
= (f
. z) & z
in (
dom f) by
II;
[z, y]
in f by
K01,
FUNCT_1: 1;
hence thesis by
A3,
ASUPP1,
K01,
SS,
CSUPP1,
DSUPP1;
end;
given y be
object such that
U000:
[z, y]
in f & y
in x;
z
<> 2 by
A3,
U000,
FUNCT_1: 1,
BSUPP1;
then z
= 1 or z
= 3 or z
= 4 by
U000,
FUNCT_1: 1,
II0;
hence thesis by
ENUMSET1:def 1;
end;
hence thesis by
B134,
RELAT_1:def 14;
end;
suppose
DSUPP2: not k4
in x;
for z be
object holds z
in
{1, 3} iff ex y be
object st
[z, y]
in f & y
in x
proof
let z be
object;
thus z
in
{1, 3} implies ex y be
object st
[z, y]
in f & y
in x
proof
assume z
in
{1, 3};
then
SS: z
= 1 or z
= 3 by
TARSKI:def 2;
then
consider y be
object such that
K01: y
= (f
. z) & z
in (
dom f) by
II;
[z, y]
in f by
K01,
FUNCT_1: 1;
hence thesis by
A3,
ASUPP1,
K01,
CSUPP1,
SS;
end;
given y be
object such that
U000:
[z, y]
in f & y
in x;
z
<> 2 & z
<> 4 by
A3,
U000,
FUNCT_1: 1,
BSUPP1,
DSUPP2;
then z
= 1 or z
= 3 by
U000,
FUNCT_1: 1,
II0;
hence thesis by
TARSKI:def 2;
end;
hence thesis by
B13,
RELAT_1:def 14;
end;
end;
suppose
CSUPP2: not k3
in x;
per cases ;
suppose
DSUPP1: k4
in x;
for z be
object holds z
in
{1, 4} iff ex y be
object st
[z, y]
in f & y
in x
proof
let z be
object;
thus z
in
{1, 4} implies ex y be
object st
[z, y]
in f & y
in x
proof
assume z
in
{1, 4};
then
SS: z
= 1 or z
= 4 by
TARSKI:def 2;
then
consider y be
object such that
K01: y
= (f
. z) & z
in (
dom f) by
II;
[z, y]
in f by
K01,
FUNCT_1: 1;
hence thesis by
A3,
ASUPP1,
K01,
SS,
DSUPP1;
end;
given y be
object such that
U000:
[z, y]
in f & y
in x;
z
<> 2 & z
<> 3 by
A3,
U000,
FUNCT_1: 1,
BSUPP1,
CSUPP2;
then z
= 1 or z
= 4 by
U000,
FUNCT_1: 1,
II0;
hence thesis by
TARSKI:def 2;
end;
hence thesis by
B14,
RELAT_1:def 14;
end;
suppose
DSUPP2: not k4
in x;
Fin1: for z be
object holds z
in
{1} iff ex y be
object st
[z, y]
in f & y
in x
proof
let z be
object;
thus z
in
{1} implies ex y be
object st
[z, y]
in f & y
in x
proof
assume
K000: z
in
{1};
then z
in (
dom f) by
TARSKI:def 1,
II;
then
consider y be
object such that
K01: y
= (f
. z) & z
in (
dom f);
Fin1:
[z, y]
in f by
K01,
FUNCT_1: 1;
z
= 1 by
K000,
TARSKI:def 1;
hence thesis by
A3,
ASUPP1,
Fin1,
K01;
end;
given y be
object such that
U000:
[z, y]
in f & y
in x;
z
<> 2 & z
<> 3 & z
<> 4 by
A3,
FUNCT_1: 1,
U000,
DSUPP2,
BSUPP1,
CSUPP2;
then z
= 1 by
U000,
FUNCT_1: 1,
II0;
hence thesis by
TARSKI:def 1;
end;
{1}
in (
bool
{1, 2, 3, 4}) by
EnLm1;
hence thesis by
Fin1,
RELAT_1:def 14;
end;
end;
end;
end;
suppose
ASUPP2: not k1
in x;
per cases ;
suppose
BSUPP1: k2
in x;
per cases ;
suppose
CSUPP1: k3
in x;
per cases ;
suppose
DSUPP1: k4
in x;
for z be
object holds z
in
{2, 3, 4} iff ex y be
object st
[z, y]
in f & y
in x
proof
let z be
object;
thus z
in
{2, 3, 4} implies ex y be
object st
[z, y]
in f & y
in x
proof
assume z
in
{2, 3, 4};
then
SS: z
= 2 or z
= 3 or z
= 4 by
ENUMSET1:def 1;
then
consider y be
object such that
K01: y
= (f
. z) & z
in (
dom f) by
II;
[z, y]
in f by
K01,
FUNCT_1: 1;
hence thesis by
A3,
BSUPP1,
K01,
SS,
CSUPP1,
DSUPP1;
end;
given y be
object such that
U000:
[z, y]
in f & y
in x;
z
<> 1 by
A3,
FUNCT_1: 1,
U000,
ASUPP2;
then z
= 2 or z
= 3 or z
= 4 by
U000,
FUNCT_1: 1,
II0;
hence thesis by
ENUMSET1:def 1;
end;
hence thesis by
B234,
RELAT_1:def 14;
end;
suppose
DSUPP2: not k4
in x;
for z be
object holds z
in
{2, 3} iff ex y be
object st
[z, y]
in f & y
in x
proof
let z be
object;
thus z
in
{2, 3} implies ex y be
object st
[z, y]
in f & y
in x
proof
assume z
in
{2, 3};
then
SS: z
= 2 or z
= 3 by
TARSKI:def 2;
then
consider y be
object such that
K01: y
= (f
. z) & z
in (
dom f) by
II;
[z, y]
in f by
K01,
FUNCT_1: 1;
hence thesis by
A3,
BSUPP1,
K01,
CSUPP1,
SS;
end;
given y be
object such that
U000:
[z, y]
in f & y
in x;
z
<> 1 & z
<> 4 by
A3,
U000,
FUNCT_1: 1,
ASUPP2,
DSUPP2;
then z
= 2 or z
= 3 by
U000,
FUNCT_1: 1,
II0;
hence thesis by
TARSKI:def 2;
end;
hence thesis by
B23,
RELAT_1:def 14;
end;
end;
suppose
CSUPP1: not k3
in x;
per cases ;
suppose
DSUPP1: k4
in x;
for z be
object holds z
in
{2, 4} iff ex y be
object st
[z, y]
in f & y
in x
proof
let z be
object;
thus z
in
{2, 4} implies ex y be
object st
[z, y]
in f & y
in x
proof
assume z
in
{2, 4};
then
SS: z
= 2 or z
= 4 by
TARSKI:def 2;
then
consider y be
object such that
K01: y
= (f
. z) & z
in (
dom f) by
II;
[z, y]
in f by
K01,
FUNCT_1: 1;
hence thesis by
A3,
BSUPP1,
K01,
DSUPP1,
SS;
end;
given y be
object such that
U000:
[z, y]
in f & y
in x;
z
<> 3 & z
<> 1 by
A3,
U000,
FUNCT_1: 1,
ASUPP2,
CSUPP1;
then z
= 2 or z
= 4 by
U000,
FUNCT_1: 1,
II0;
hence thesis by
TARSKI:def 2;
end;
hence thesis by
B24,
RELAT_1:def 14;
end;
suppose
DSUPP2: not k4
in x;
Fin1: for z be
object holds z
in
{2} iff ex y be
object st
[z, y]
in f & y
in x
proof
let z be
object;
thus z
in
{2} implies ex y be
object st
[z, y]
in f & y
in x
proof
assume
K000: z
in
{2};
then z
in (
dom f) by
TARSKI:def 1,
II;
then
consider y be
object such that
K01: y
= (f
. z) & z
in (
dom f);
Fin1:
[z, y]
in f by
K01,
FUNCT_1: 1;
z
= 2 by
K000,
TARSKI:def 1;
hence thesis by
A3,
BSUPP1,
Fin1,
K01;
end;
given y be
object such that
U000:
[z, y]
in f & y
in x;
z
<> 1 & z
<> 3 & z
<> 4 by
A3,
U000,
FUNCT_1: 1,
ASUPP2,
DSUPP2,
CSUPP1;
then z
= 2 by
U000,
FUNCT_1: 1,
II0;
hence thesis by
TARSKI:def 1;
end;
{2}
in (
bool
{1, 2, 3, 4}) by
EnLm2;
hence thesis by
Fin1,
RELAT_1:def 14;
end;
end;
end;
suppose
BSUPP2: not k2
in x;
per cases ;
suppose
CSUPP1: k3
in x;
per cases ;
suppose
DSUPP1: k4
in x;
Fin1: for z be
object holds z
in
{3, 4} iff ex y be
object st
[z, y]
in f & y
in x
proof
let z be
object;
thus z
in
{3, 4} implies ex y be
object st
[z, y]
in f & y
in x
proof
assume z
in
{3, 4};
then
SS: z
= 3 or z
= 4 by
TARSKI:def 2;
then
consider y be
object such that
K01: y
= (f
. z) & z
in (
dom f) by
II;
[z, y]
in f by
K01,
FUNCT_1: 1;
hence thesis by
A3,
CSUPP1,
K01,
DSUPP1,
SS;
end;
given y be
object such that
U000:
[z, y]
in f & y
in x;
z
<> 1 & z
<> 2 by
A3,
U000,
FUNCT_1: 1,
BSUPP2,
ASUPP2;
then z
= 3 or z
= 4 by
U000,
FUNCT_1: 1,
II0;
hence thesis by
TARSKI:def 2;
end;
{3, 4}
in (
bool
{1, 2, 3, 4}) by
Lm1;
hence thesis by
Fin1,
RELAT_1:def 14;
end;
suppose
DSUPP2: not k4
in x;
Fin1: for z be
object holds z
in
{3} iff ex y be
object st
[z, y]
in f & y
in x
proof
let z be
object;
thus z
in
{3} implies ex y be
object st
[z, y]
in f & y
in x
proof
assume
K000: z
in
{3};
then z
in (
dom f) by
TARSKI:def 1,
II;
then
consider y be
object such that
K01: y
= (f
. z) & z
in (
dom f);
Fin1:
[z, y]
in f by
K01,
FUNCT_1: 1;
z
= 3 by
K000,
TARSKI:def 1;
hence thesis by
A3,
CSUPP1,
Fin1,
K01;
end;
given y be
object such that
U000:
[z, y]
in f & y
in x;
z
<> 1 & z
<> 2 & z
<> 4 by
A3,
U000,
FUNCT_1: 1,
BSUPP2,
DSUPP2,
ASUPP2;
then z
= 3 by
U000,
FUNCT_1: 1,
II0;
hence thesis by
TARSKI:def 1;
end;
{3}
in (
bool
{1, 2, 3, 4}) by
EnLm3;
hence thesis by
Fin1,
RELAT_1:def 14;
end;
end;
suppose
CSUPP2: not k3
in x;
per cases ;
suppose
DSUPP1: k4
in x;
Fin1: for z be
object holds z
in
{4} iff ex y be
object st
[z, y]
in f & y
in x
proof
let z be
object;
thus z
in
{4} implies ex y be
object st
[z, y]
in f & y
in x
proof
assume
K000: z
in
{4};
then z
in (
dom f) by
TARSKI:def 1,
II;
then
consider y be
object such that
K01: y
= (f
. z) & z
in (
dom f);
Fin1:
[z, y]
in f by
K01,
FUNCT_1: 1;
z
= 4 by
K000,
TARSKI:def 1;
hence thesis by
A3,
DSUPP1,
Fin1,
K01;
end;
given y be
object such that
U000:
[z, y]
in f & y
in x;
z
<> 1 & z
<> 2 & z
<> 3 by
A3,
U000,
FUNCT_1: 1,
CSUPP2,
ASUPP2,
BSUPP2;
then z
= 4 by
II0,
U000,
FUNCT_1: 1;
hence thesis by
TARSKI:def 1;
end;
{4}
in (
bool
{1, 2, 3, 4}) by
EnLm4;
hence thesis by
Fin1,
RELAT_1:def 14;
end;
suppose
DSUPP2: not k4
in x;
for z be
object holds z
in
{} iff ex y be
object st
[z, y]
in f & y
in x
proof
let z be
object;
(ex y be
object st
[z, y]
in f & y
in x) implies z
in
{}
proof
given y be
object such that
W1:
[z, y]
in f & y
in x;
z
in (
dom f) & y
= (f
. z) by
W1,
FUNCT_1: 1;
hence thesis by
A3,
W1,
ASUPP2,
BSUPP2,
CSUPP2,
DSUPP2,
A0,
ENUMSET1:def 2;
end;
hence thesis;
end;
then (f
" x)
=
{} by
RELAT_1:def 14;
hence thesis by
PROB_1: 4;
end;
end;
end;
end;
end;
hence thesis by
A4,
A2;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis by
A3;
end;
theorem ::
FINANCE3:36
MyFunc6: for k1,k2 be
Element of
REAL , Omega be non
empty
set st Omega
=
{1, 2, 3, 4} holds for Sigma be
SigmaField of Omega, I be non
empty
real-membered
set, MyFunc be
ManySortedSigmaField of I, Sigma st (MyFunc
. 1)
=
Special_SigmaField1 & (MyFunc
. 2)
=
Special_SigmaField2 & (MyFunc
. 3)
= (
Trivial-SigmaField
{1, 2, 3, 4}) holds for eli be
Element of I st eli
= 2 holds ex f be
Function of Omega,
REAL st (f
. 1)
= k1 & (f
. 2)
= k1 & (f
. 3)
= k2 & (f
. 4)
= k2 & f is (
El_Filtration (eli,MyFunc)),
Borel_Sets
-random_variable-like
proof
let k1,k2 be
Element of
REAL ;
let Omega be non
empty
set;
assume
A0: Omega
=
{1, 2, 3, 4};
let Sigma be
SigmaField of Omega;
let I be non
empty
real-membered
set;
let MyFunc be
ManySortedSigmaField of I, Sigma;
assume
A2: (MyFunc
. 1)
=
Special_SigmaField1 & (MyFunc
. 2)
=
Special_SigmaField2 & (MyFunc
. 3)
= (
Trivial-SigmaField
{1, 2, 3, 4});
let eli be
Element of I;
assume
A4: eli
= 2;
consider f be
Function of Omega,
REAL such that
A3: (f
. 1)
= k1 & (f
. 2)
= k1 & (f
. 3)
= k2 & (f
. 4)
= k2 by
A0,
MYF30;
take f;
set i = eli;
for x be
set holds (f
" x)
in (
El_Filtration (i,MyFunc))
proof
let x be
set;
(f
" x)
in (MyFunc
. i)
proof
(f
" x)
in
{
{} ,
{1, 2},
{3, 4},
{1, 2, 3, 4}}
proof
(f
" x)
=
{} or (f
" x)
=
{1, 2} or (f
" x)
=
{3, 4} or (f
" x)
=
{1, 2, 3, 4}
proof
per cases ;
suppose
INITSUPP: k1
in x;
per cases ;
suppose
JSUPP1: k2
in x;
for z be
object holds z
in
{1, 2, 3, 4} iff ex y be
object st
[z, y]
in f & y
in x
proof
let z be
object;
I1: z
in
{1, 2, 3, 4} implies ex y be
object st
[z, y]
in f & y
in x
proof
assume
ASSJ0: z
in
{1, 2, 3, 4};
then
L1: z
in (
dom f) by
FUNCT_2:def 1,
A0;
per cases by
ASSJ0,
ENUMSET1:def 2;
suppose z
= 1 or z
= 2;
then
[z, k1]
in f & k1
in x by
A3,
INITSUPP,
L1,
FUNCT_1: 1;
hence thesis;
end;
suppose z
= 3 or z
= 4;
then (f
. z)
= k2 & k2
in x & z
in (
dom f) by
A3,
JSUPP1,
ASSJ0,
FUNCT_2:def 1,
A0;
then
[z, k2]
in f & k2
in x by
FUNCT_1: 1;
hence thesis;
end;
end;
(ex y be
object st
[z, y]
in f & y
in x) implies z
in
{1, 2, 3, 4}
proof
given y be
object such that
ASSJ0:
[z, y]
in f & y
in x;
z
in (
dom f) & y
= (f
. z) by
ASSJ0,
FUNCT_1: 1;
hence thesis by
A0;
end;
hence thesis by
I1;
end;
hence thesis by
RELAT_1:def 14;
end;
suppose
JSUPP2: not k2
in x;
for z be
object holds z
in
{1, 2} iff ex y be
object st
[z, y]
in f & y
in x
proof
let z be
object;
I1: z
in
{1, 2} implies ex y be
object st
[z, y]
in f & y
in x
proof
assume z
in
{1, 2};
then
S2: z
= 1 or z
= 2 by
TARSKI:def 2;
then z
in Omega by
ENUMSET1:def 2,
A0;
then
S1: z
in (
dom f) by
FUNCT_2:def 1;
[z, k1]
in f by
S1,
S2,
A3,
FUNCT_1: 1;
hence thesis by
INITSUPP;
end;
(ex y be
object st
[z, y]
in f & y
in x) implies z
in
{1, 2}
proof
given y be
object such that
M1:
[z, y]
in f & y
in x;
z
in (
dom f) by
M1,
FUNCT_1: 1;
then z
= 1 or z
= 2 or z
= 3 or z
= 4 by
A0,
ENUMSET1:def 2;
hence thesis by
JSUPP2,
M1,
FUNCT_1: 1,
A3,
TARSKI:def 2;
end;
hence thesis by
I1;
end;
hence thesis by
RELAT_1:def 14;
end;
end;
suppose
INITSUPP: not k1
in x;
per cases ;
suppose
JSUPP1: k2
in x;
for z be
object holds z
in
{3, 4} iff ex y be
object st
[z, y]
in f & y
in x
proof
let z be
object;
I1: z
in
{3, 4} implies ex y be
object st
[z, y]
in f & y
in x
proof
assume z
in
{3, 4};
then
J1: z
= 3 or z
= 4 by
TARSKI:def 2;
then z
in
{1, 2, 3, 4} by
ENUMSET1:def 2;
then z
in (
dom f) by
FUNCT_2:def 1,
A0;
then
[z, k2]
in f by
J1,
A3,
FUNCT_1: 1;
hence thesis by
JSUPP1;
end;
(ex y be
object st
[z, y]
in f & y
in x) implies z
in
{3, 4}
proof
given y be
object such that
ASSJ0:
[z, y]
in f & y
in x;
OO0: y
= k1 or y
= k2
proof
z
in (
dom f) by
ASSJ0,
FUNCT_1: 1;
then z
= 1 or z
= 2 or z
= 3 or z
= 4 by
ENUMSET1:def 2,
A0;
hence thesis by
A3,
ASSJ0,
FUNCT_1: 1;
end;
Z10: k2
= (f
. z)
proof
per cases by
OO0;
suppose y
= k1;
hence thesis by
INITSUPP,
ASSJ0;
end;
suppose y
= k2;
hence thesis by
ASSJ0,
FUNCT_1: 1;
end;
end;
z
= 3 or z
= 4
proof
assume
ZZ1: z
<> 3 & z
<> 4;
z
in (
dom f) by
ASSJ0,
FUNCT_1: 1;
hence thesis by
Z10,
ZZ1,
A3,
INITSUPP,
JSUPP1,
ENUMSET1:def 2,
A0;
end;
hence thesis by
TARSKI:def 2;
end;
hence thesis by
I1;
end;
hence thesis by
RELAT_1:def 14;
end;
suppose
JSUPP2: not k2
in x;
for z be
object holds z
in
{} iff ex y be
object st
[z, y]
in f & y
in x
proof
let z be
object;
(ex y be
object st
[z, y]
in f & y
in x) implies z
in
{}
proof
given y be
object such that
M1:
[z, y]
in f & y
in x;
z
in (
dom f) & y
= (f
. z) & y
<> k2 by
M1,
FUNCT_1: 1,
JSUPP2;
hence thesis by
INITSUPP,
M1,
A3,
A0,
ENUMSET1:def 2;
end;
hence thesis;
end;
hence thesis by
RELAT_1:def 14;
end;
end;
end;
hence thesis by
ENUMSET1:def 2;
end;
hence thesis by
A4,
A2;
end;
hence thesis;
end;
hence thesis by
A3;
end;
theorem ::
FINANCE3:37
MyFunc7: for k1 be
Element of
REAL , Omega be non
empty
set st Omega
=
{1, 2, 3, 4} holds for Sigma be
SigmaField of Omega, I be non
empty
real-membered
set, MyFunc be
ManySortedSigmaField of I, Sigma st (MyFunc
. 1)
=
Special_SigmaField1 & (MyFunc
. 2)
=
Special_SigmaField2 & (MyFunc
. 3)
= (
Trivial-SigmaField
{1, 2, 3, 4}) holds for eli be
Element of I st eli
= 1 holds ex f be
Function of Omega,
REAL st (f
. 1)
= k1 & (f
. 2)
= k1 & (f
. 3)
= k1 & (f
. 4)
= k1 & f is (
El_Filtration (eli,MyFunc)),
Borel_Sets
-random_variable-like
proof
let k1 be
Element of
REAL ;
let Omega be non
empty
set;
assume
A0: Omega
=
{1, 2, 3, 4};
let Sigma be
SigmaField of Omega;
let I be non
empty
real-membered
set;
let MyFunc be
ManySortedSigmaField of I, Sigma;
assume
A2: (MyFunc
. 1)
=
Special_SigmaField1 & (MyFunc
. 2)
=
Special_SigmaField2 & (MyFunc
. 3)
= (
Trivial-SigmaField
{1, 2, 3, 4});
let eli be
Element of I;
assume
A4: eli
= 1;
consider f be
Function of Omega,
REAL such that
A3: (f
. 1)
= k1 & (f
. 2)
= k1 & (f
. 3)
= k1 & (f
. 4)
= k1 by
A0,
MYF30;
take f;
set i = eli;
for x be
set holds (f
" x)
in (
El_Filtration (i,MyFunc))
proof
let x be
set;
(f
" x)
in (MyFunc
. i)
proof
(f
" x)
in
{
{} ,
{1, 2, 3, 4}}
proof
(f
" x)
=
{} or (f
" x)
=
{1, 2, 3, 4}
proof
per cases ;
suppose
JSUPP1: k1
in x;
for z be
object holds z
in
{1, 2, 3, 4} iff ex y be
object st
[z, y]
in f & y
in x
proof
let z be
object;
I1: z
in
{1, 2, 3, 4} implies ex y be
object st
[z, y]
in f & y
in x
proof
assume
ASSJ0: z
in
{1, 2, 3, 4};
[z, k1]
in f
proof
z
in (
dom f) & k1
= (f
. z) by
ENUMSET1:def 2,
A3,
ASSJ0,
FUNCT_2:def 1,
A0;
hence thesis by
FUNCT_1: 1;
end;
hence thesis by
JSUPP1;
end;
(ex y be
object st
[z, y]
in f & y
in x) implies z
in
{1, 2, 3, 4}
proof
given y be
object such that
ASSJ0:
[z, y]
in f & y
in x;
z
in (
dom f) & y
= (f
. z) by
ASSJ0,
FUNCT_1: 1;
hence thesis by
A0;
end;
hence thesis by
I1;
end;
hence thesis by
RELAT_1:def 14;
end;
suppose
JSUPP2: not k1
in x;
for z be
object holds z
in
{} iff ex y be
object st
[z, y]
in f & y
in x
proof
let z be
object;
(ex y be
object st
[z, y]
in f & y
in x) implies z
in
{}
proof
given y be
object such that
M1:
[z, y]
in f & y
in x;
z
in (
dom f) & y
= (f
. z) & not y
= k1 by
M1,
FUNCT_1: 1,
JSUPP2;
hence thesis by
A3,
A0,
ENUMSET1:def 2;
end;
hence thesis;
end;
hence thesis by
RELAT_1:def 14;
end;
end;
hence thesis by
TARSKI:def 2;
end;
hence thesis by
A4,
A2;
end;
hence thesis;
end;
hence thesis by
A3;
end;
theorem ::
FINANCE3:38
for Omega be non
empty
set st Omega
=
{1, 2, 3, 4} holds for Sigma be
SigmaField of Omega, I be non
empty
real-membered
set st I
=
{1, 2, 3} & Sigma
= (
bool
{1, 2, 3, 4}) holds for MyFunc be
ManySortedSigmaField of I, Sigma st (MyFunc
. 1)
=
Special_SigmaField1 & (MyFunc
. 2)
=
Special_SigmaField2 & (MyFunc
. 3)
= (
Trivial-SigmaField
{1, 2, 3, 4}) holds for Prob be
Function of Sigma,
REAL holds for i be
Element of I holds ex RV be
Function of Omega,
REAL st RV is (
El_Filtration (i,MyFunc)),
Borel_Sets
-random_variable-like
proof
let Omega be non
empty
set;
assume
A0: Omega
=
{1, 2, 3, 4};
let Sigma be
SigmaField of Omega;
let I be non
empty
real-membered
set;
assume
A1: I
=
{1, 2, 3} & Sigma
= (
bool
{1, 2, 3, 4});
let MyFunc be
ManySortedSigmaField of I, Sigma;
assume
A2: (MyFunc
. 1)
=
Special_SigmaField1 & (MyFunc
. 2)
=
Special_SigmaField2 & (MyFunc
. 3)
= (
Trivial-SigmaField
{1, 2, 3, 4});
let Prob be
Function of Sigma,
REAL ;
let i be
Element of I;
per cases by
A1,
ENUMSET1:def 1;
suppose
a1: i
= 1;
100
in
REAL by
NUMBERS: 19;
then ex f be
Function of Omega,
REAL st (f
. 1)
= 100 & (f
. 2)
= 100 & (f
. 3)
= 100 & (f
. 4)
= 100 & f is (
El_Filtration (i,MyFunc)),
Borel_Sets
-random_variable-like by
A0,
A2,
MyFunc7,
a1;
hence thesis;
end;
suppose
a1: i
= 2;
80
in
REAL & 120
in
REAL by
NUMBERS: 19;
then ex f be
Function of Omega,
REAL st (f
. 1)
= 80 & (f
. 2)
= 80 & (f
. 3)
= 120 & (f
. 4)
= 120 & f is (
El_Filtration (i,MyFunc)),
Borel_Sets
-random_variable-like by
A0,
A2,
MyFunc6,
a1;
hence thesis;
end;
suppose
a1: i
= 3;
60
in
REAL & 80
in
REAL & 100
in
REAL & 120
in
REAL by
NUMBERS: 19;
then ex f be
Function of Omega,
REAL st (f
. 1)
= 60 & (f
. 2)
= 80 & (f
. 3)
= 100 & (f
. 4)
= 120 & f is (
El_Filtration (i,MyFunc)),
Borel_Sets
-random_variable-like by
A0,
A2,
MyFunc5,
a1;
hence thesis;
end;
end;
definition
let I be non
empty
real-membered
set;
let i be
Element of I;
let Omega be non
empty
set;
let Sigma be
SigmaField of Omega;
let f1 be
Function of Omega,
REAL ;
let f2 be
Function of Omega,
REAL ;
let f3 be
Function of Omega,
REAL ;
::
FINANCE3:def22
func
FunctionRV1 (i,Sigma,f1,f2,f3) ->
Element of (
set_of_random_variables_on (Sigma,
Borel_Sets )) equals
:
Def1211: f2 if i
= 2
otherwise f1;
correctness
proof
consider MyFunc be
Filtration of I, Sigma such that
B1: (MyFunc
. 1)
=
Special_SigmaField1 & (MyFunc
. 2)
=
Special_SigmaField2 & (MyFunc
. 3)
= (
Trivial-SigmaField
{1, 2, 3, 4}) by
A0000,
A00,
A000,
MyNeed;
per cases ;
suppose
SUPP: i
= 2;
80
in
REAL & 120
in
REAL by
NUMBERS: 19;
then
consider f be
Function of Omega,
REAL such that
B4: (f
. 1)
= 80 & (f
. 2)
= 80 & (f
. 3)
= 120 & (f
. 4)
= 120 & f is (
El_Filtration (i,MyFunc)),
Borel_Sets
-random_variable-like by
A000,
B1,
MyFunc6,
SUPP;
f is Sigma,
Borel_Sets
-random_variable-like by
A00;
then
ZW1: f
in (
set_of_random_variables_on (Sigma,
Borel_Sets ));
(
dom f)
= Omega by
FUNCT_2:def 1;
then
KK: (
dom f)
= (
dom f2) by
FUNCT_2:def 1;
for x be
object st x
in (
dom f) holds (f
. x)
= (f2
. x)
proof
let x be
object;
assume x
in (
dom f);
then
reconsider x as
Element of Omega;
x
= 1 or x
= 2 or x
= 3 or x
= 4 by
A000,
ENUMSET1:def 2;
hence thesis by
B4,
A1;
end;
hence thesis by
ZW1,
SUPP,
FUNCT_1: 2,
KK;
end;
suppose
F1: i
<> 2;
60
in
REAL & 80
in
REAL & 100
in
REAL & 120
in
REAL by
NUMBERS: 19;
then
consider f be
Function of Omega,
REAL such that
B4: (f
. 1)
= 60 & (f
. 2)
= 80 & (f
. 3)
= 100 & (f
. 4)
= 120 & f is (
El_Filtration (i,MyFunc)),
Borel_Sets
-random_variable-like by
A000,
B1,
MyFunc5,
MyI,
F1;
f is Sigma,
Borel_Sets
-random_variable-like by
A00;
then
ZW1: f
in (
set_of_random_variables_on (Sigma,
Borel_Sets ));
(
dom f)
= Omega by
FUNCT_2:def 1;
then
KK: (
dom f)
= (
dom f1) by
FUNCT_2:def 1;
for x be
object st x
in (
dom f) holds (f
. x)
= (f1
. x)
proof
let x be
object;
assume x
in (
dom f);
then
reconsider x as
Element of Omega;
x
= 1 or x
= 2 or x
= 3 or x
= 4 by
A000,
ENUMSET1:def 2;
hence thesis by
B4,
A0;
end;
hence thesis by
ZW1,
F1,
KK,
FUNCT_1: 2;
end;
end;
end
definition
let I be non
empty
real-membered
set;
let i be
Element of I;
let Omega be non
empty
set;
let Sigma be
SigmaField of Omega;
let f1,f2 be
Function of Omega,
REAL ;
let f3 be
Function of Omega,
REAL ;
::
FINANCE3:def23
func
FunctionRV2 (i,Sigma,f1,f2,f3) ->
Element of (
set_of_random_variables_on (Sigma,
Borel_Sets )) equals
:
Def1212: (
FunctionRV1 (i,Sigma,f1,f2,f3)) if (i
= 2 or i
= 3)
otherwise f3;
correctness
proof
per cases ;
suppose
F1: not (i
= 2 or i
= 3);
consider MyFunc be
Filtration of I, Sigma such that
B1: (MyFunc
. 1)
=
Special_SigmaField1 & (MyFunc
. 2)
=
Special_SigmaField2 & (MyFunc
. 3)
= (
Trivial-SigmaField
{1, 2, 3, 4}) by
A0000,
A00,
A000,
MyNeed;
B3: i
= 1 by
F1,
A0000,
ENUMSET1:def 1;
100
in
REAL by
NUMBERS: 19;
then
consider f be
Function of Omega,
REAL such that
B4: (f
. 1)
= 100 & (f
. 2)
= 100 & (f
. 3)
= 100 & (f
. 4)
= 100 & f is (
El_Filtration (i,MyFunc)),
Borel_Sets
-random_variable-like by
A000,
B1,
B3,
MyFunc7;
f is Sigma,
Borel_Sets
-random_variable-like by
A00;
then
ZW1: f
in (
set_of_random_variables_on (Sigma,
Borel_Sets ));
(
dom f)
= Omega by
FUNCT_2:def 1;
then
KK: (
dom f)
= (
dom f3) by
FUNCT_2:def 1;
for x be
object st x
in (
dom f) holds (f
. x)
= (f3
. x)
proof
let x be
object;
assume x
in (
dom f);
then
reconsider x as
Element of Omega;
x
= 1 or x
= 2 or x
= 3 or x
= 4 by
A000,
ENUMSET1:def 2;
hence thesis by
B4,
A2;
end;
hence thesis by
KK,
ZW1,
FUNCT_1: 2;
end;
suppose i
= 2 or i
= 3;
hence thesis;
end;
end;
end
theorem ::
FINANCE3:39
for Omega,Omega2 be non
empty
set st Omega
=
{1, 2, 3, 4} holds for Sigma be
SigmaField of Omega, I be non
empty
real-membered
set st I
=
{1, 2, 3} & Sigma
= (
bool
{1, 2, 3, 4}) holds for MyFunc be
Filtration of I, Sigma st (MyFunc
. 1)
=
Special_SigmaField1 & (MyFunc
. 2)
=
Special_SigmaField2 & (MyFunc
. 3)
= (
Trivial-SigmaField
{1, 2, 3, 4}) holds ex Stoch be
Stochastic_Process of I, Sigma,
Borel_Sets st (for k be
Element of I holds (ex RV be
Function of Omega,
REAL st ((Stoch
. k)
= RV & RV is Sigma,
Borel_Sets
-random_variable-like) & RV is (
El_Filtration (k,MyFunc)),
Borel_Sets
-random_variable-like) & (ex f be
Function of Omega,
REAL st k
= 1 implies (f
. 1)
= 100 & (f
. 2)
= 100 & (f
. 3)
= 100 & (f
. 4)
= 100 & (Stoch
. k)
= f) & (ex f be
Function of Omega,
REAL st k
= 2 implies (f
. 1)
= 80 & (f
. 2)
= 80 & (f
. 3)
= 120 & (f
. 4)
= 120 & (Stoch
. k)
= f) & (ex f be
Function of Omega,
REAL st k
= 3 implies (f
. 1)
= 60 & (f
. 2)
= 80 & (f
. 3)
= 100 & (f
. 4)
= 120 & (Stoch
. k)
= f) & Stoch is MyFunc
-stoch_proc_wrt_to_Filtration) & Stoch is
Adapted_Stochastic_Process of Stoch
proof
let Omega,Omega2 be non
empty
set;
assume
A00: Omega
=
{1, 2, 3, 4};
let Sigma be
SigmaField of Omega;
let I be non
empty
real-membered
set;
assume that
A0: I
=
{1, 2, 3} and
a0: Sigma
= (
bool
{1, 2, 3, 4});
let MyFunc be
Filtration of I, Sigma;
assume
A1: (MyFunc
. 1)
=
Special_SigmaField1 & (MyFunc
. 2)
=
Special_SigmaField2 & (MyFunc
. 3)
= (
Trivial-SigmaField
{1, 2, 3, 4});
a1: 100
in
REAL by
NUMBERS: 19;
then
consider f3 be
Function of Omega,
REAL such that
F1: (f3
. 1)
= 100 & (f3
. 2)
= 100 & (f3
. 3)
= 100 & (f3
. 4)
= 100 by
A00,
MYF30;
a2: 80
in
REAL & 120
in
REAL by
NUMBERS: 19;
then
consider f2 be
Function of Omega,
REAL such that
F2: (f2
. 1)
= 80 & (f2
. 2)
= 80 & (f2
. 3)
= 120 & (f2
. 4)
= 120 by
A00,
MYF30;
60
in
REAL by
NUMBERS: 19;
then
consider f1 be
Function of Omega,
REAL such that
F3: (f1
. 1)
= 60 & (f1
. 2)
= 80 & (f1
. 3)
= 100 & (f1
. 4)
= 120 by
A00,
MYF30,
a1,
a2;
deffunc
U(
Element of I) = (
FunctionRV2 ($1,Sigma,f1,f2,f3));
consider fI1 be
Function of I, (
set_of_random_variables_on (Sigma,
Borel_Sets )) such that
B1: for d be
Element of I holds (fI1
. d)
=
U(d) from
FUNCT_2:sch 4;
Fin1: for k be
Element of I holds ex RV be
Function of Omega,
REAL st ((fI1
. k)
= RV & RV is Sigma,
Borel_Sets
-random_variable-like)
proof
let k be
Element of I;
(fI1
. k)
in (
set_of_random_variables_on (Sigma,
Borel_Sets ));
hence thesis;
end;
then
reconsider fI1 as
Stochastic_Process of I, Sigma,
Borel_Sets by
Def30000;
take fI1;
for k be
Element of I holds (ex RV be
Function of Omega,
REAL st ((fI1
. k)
= RV & RV is Sigma,
Borel_Sets
-random_variable-like) & RV is (
El_Filtration (k,MyFunc)),
Borel_Sets
-random_variable-like) & (ex f be
Function of Omega,
REAL st k
= 1 implies (f
. 1)
= 100 & (f
. 2)
= 100 & (f
. 3)
= 100 & (f
. 4)
= 100 & (fI1
. k)
= f) & (ex f be
Function of Omega,
REAL st k
= 2 implies (f
. 1)
= 80 & (f
. 2)
= 80 & (f
. 3)
= 120 & (f
. 4)
= 120 & (fI1
. k)
= f) & (ex f be
Function of Omega,
REAL st k
= 3 implies (f
. 1)
= 60 & (f
. 2)
= 80 & (f
. 3)
= 100 & (f
. 4)
= 120 & (fI1
. k)
= f) & fI1 is MyFunc
-stoch_proc_wrt_to_Filtration & fI1 is
Adapted_Stochastic_Process of fI1
proof
let k be
Element of I;
Fin3: fI1 is MyFunc
-stoch_proc_wrt_to_Filtration
proof
for i be
Element of I holds (
RVProcess (fI1,i)) is (
El_Filtration (i,MyFunc)),
Borel_Sets
-random_variable-like
proof
let i be
Element of I;
per cases by
A0,
ENUMSET1:def 1;
suppose
SUPP: i
= 1;
then
X1: (
FunctionRV2 (i,Sigma,f1,f2,f3))
= f3 by
a0,
A0,
A00,
F1,
Def1212;
100
in
REAL by
NUMBERS: 19;
then
consider f be
Function of Omega,
REAL such that
Q1: (f
. 1)
= 100 & (f
. 2)
= 100 & (f
. 3)
= 100 & (f
. 4)
= 100 & f is (
El_Filtration (i,MyFunc)),
Borel_Sets
-random_variable-like by
SUPP,
A00,
A1,
MyFunc7;
E1: (
dom f)
= Omega by
FUNCT_2:def 1;
for x be
object st x
in (
dom f) holds (f
. x)
= (f3
. x)
proof
let x be
object;
assume x
in (
dom f);
then
reconsider x as
Element of Omega;
x
= 1 or x
= 2 or x
= 3 or x
= 4 by
A00,
ENUMSET1:def 2;
hence thesis by
Q1,
F1;
end;
then f3
= f by
E1;
hence thesis by
X1,
B1,
Q1;
end;
suppose
SUPP2: i
= 2;
then (
FunctionRV2 (i,Sigma,f1,f2,f3))
= (
FunctionRV1 (i,Sigma,f1,f2,f3)) by
A0,
a0,
A00,
F1,
Def1212;
then
X1: (
FunctionRV2 (i,Sigma,f1,f2,f3))
= f2 by
a0,
A0,
A00,
F2,
F3,
SUPP2,
Def1211;
80
in
REAL & 120
in
REAL by
NUMBERS: 19;
then
consider f be
Function of Omega,
REAL such that
Q1: (f
. 1)
= 80 & (f
. 2)
= 80 & (f
. 3)
= 120 & (f
. 4)
= 120 & f is (
El_Filtration (i,MyFunc)),
Borel_Sets
-random_variable-like by
SUPP2,
A00,
A1,
MyFunc6;
E1: (
dom f)
= Omega by
FUNCT_2:def 1;
for x be
object st x
in (
dom f) holds (f
. x)
= (f2
. x)
proof
let x be
object;
assume x
in (
dom f);
then
reconsider x as
Element of Omega;
x
= 1 or x
= 2 or x
= 3 or x
= 4 by
A00,
ENUMSET1:def 2;
hence thesis by
Q1,
F2;
end;
then f2
= f by
E1;
hence thesis by
X1,
B1,
Q1;
end;
suppose
SUPP1: i
= 3;
then (
FunctionRV2 (i,Sigma,f1,f2,f3))
= (
FunctionRV1 (i,Sigma,f1,f2,f3)) by
A0,
A00,
a0,
F1,
Def1212;
then
x1: (
FunctionRV2 (i,Sigma,f1,f2,f3))
= f1 by
a0,
A0,
A00,
F2,
F3,
SUPP1,
Def1211;
60
in
REAL & 80
in
REAL & 100
in
REAL & 120
in
REAL by
NUMBERS: 19;
then
consider f be
Function of Omega,
REAL such that
Q1: (f
. 1)
= 60 & (f
. 2)
= 80 & (f
. 3)
= 100 & (f
. 4)
= 120 & f is (
El_Filtration (i,MyFunc)),
Borel_Sets
-random_variable-like by
SUPP1,
A00,
A1,
MyFunc5;
E1: (
dom f)
= Omega by
FUNCT_2:def 1;
for x be
object st x
in (
dom f) holds (f
. x)
= (f1
. x)
proof
let x be
object;
assume x
in (
dom f);
then
reconsider x as
Element of Omega;
x
= 1 or x
= 2 or x
= 3 or x
= 4 by
A00,
ENUMSET1:def 2;
hence thesis by
Q1,
F3;
end;
then f1
= f by
E1;
hence thesis by
x1,
B1,
Q1;
end;
end;
hence thesis;
end;
for k be
Element of I holds (ex RV be
Function of Omega,
REAL st ((fI1
. k)
= RV & RV is Sigma,
Borel_Sets
-random_variable-like & RV is (
El_Filtration (k,MyFunc)),
Borel_Sets
-random_variable-like)) & (ex f be
Function of Omega,
REAL st k
= 1 implies (f
. 1)
= 100 & (f
. 2)
= 100 & (f
. 3)
= 100 & (f
. 4)
= 100 & (fI1
. k)
= f) & (ex f be
Function of Omega,
REAL st k
= 2 implies (f
. 1)
= 80 & (f
. 2)
= 80 & (f
. 3)
= 120 & (f
. 4)
= 120 & (fI1
. k)
= f) & (ex f be
Function of Omega,
REAL st k
= 3 implies (f
. 1)
= 60 & (f
. 2)
= 80 & (f
. 3)
= 100 & (f
. 4)
= 120 & (fI1
. k)
= f)
proof
let k be
Element of I;
consider RV be
Function of Omega,
REAL such that
O1: (fI1
. k)
= RV & RV is Sigma,
Borel_Sets
-random_variable-like by
Fin1;
o1: RV is (
El_Filtration (k,MyFunc)),
Borel_Sets
-random_variable-like
proof
(fI1
. k)
= (
RVProcess (fI1,k)) & (
RVProcess (fI1,k)) is (
El_Filtration (k,MyFunc)),
Borel_Sets
-random_variable-like by
Fin3;
hence thesis by
O1;
end;
GFin2: ex f be
Function of Omega,
REAL st k
= 1 implies (fI1
. k)
= f & (f
. 1)
= 100 & (f
. 2)
= 100 & (f
. 3)
= 100 & (f
. 4)
= 100 & (fI1
. k)
= f
proof
k
= 1 implies (fI1
. k)
= f3
proof
assume
K1: k
= 1;
(fI1
. k)
= (
FunctionRV2 (k,Sigma,f1,f2,f3)) by
B1;
hence thesis by
a0,
A0,
A00,
F1,
K1,
Def1212;
end;
hence thesis by
F1;
end;
GFin3: ex f be
Function of Omega,
REAL st k
= 2 implies (fI1
. k)
= f & (f
. 1)
= 80 & (f
. 2)
= 80 & (f
. 3)
= 120 & (f
. 4)
= 120 & (fI1
. k)
= f
proof
k
= 2 implies (fI1
. k)
= f2
proof
assume
K1: k
= 2;
(fI1
. k)
= (
FunctionRV2 (k,Sigma,f1,f2,f3)) by
B1;
then (fI1
. k)
= (
FunctionRV1 (k,Sigma,f1,f2,f3)) by
a0,
A0,
A00,
F1,
K1,
Def1212;
hence thesis by
a0,
A0,
A00,
F2,
F3,
K1,
Def1211;
end;
hence thesis by
F2;
end;
ex f be
Function of Omega,
REAL st k
= 3 implies (fI1
. k)
= f & (f
. 1)
= 60 & (f
. 2)
= 80 & (f
. 3)
= 100 & (f
. 4)
= 120 & (fI1
. k)
= f
proof
k
= 3 implies (fI1
. k)
= f1
proof
assume
K1: k
= 3;
(fI1
. k)
= (
FunctionRV2 (k,Sigma,f1,f2,f3)) by
B1;
then (fI1
. k)
= (
FunctionRV1 (k,Sigma,f1,f2,f3)) by
a0,
A0,
A00,
F1,
K1,
Def1212;
hence thesis by
a0,
A0,
A00,
F2,
F3,
K1,
Def1211;
end;
hence thesis by
F3;
end;
hence thesis by
o1,
O1,
GFin2,
GFin3;
end;
hence thesis by
Fin3,
Def30002;
end;
hence thesis;
end;