:: Modelling Real World Using Stochastic Processes and Filtration
:: by Peter Jaeger
::
:: Received December 30, 2015
:: Copyright (c) 2015-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FINANCE1, SERIES_1, SEQ_1, RANDOM_3, FINANCE2, NUMBERS, XBOOLE_0,
PROB_1, SUBSET_1, REAL_1, TARSKI, RELAT_1, FUNCT_1, ARYTM_3, XXREAL_0,
VALUED_1, ARYTM_1, NAT_1, CARD_1, ZFMISC_1, RPR_1, SETFAM_1, FINANCE3,
EQREL_1, FUNCOP_1, KOLMOG01, FUNCT_7, MEMBERED, RANDOM_1;
notations TARSKI, SUBSET_1, XBOOLE_0, SERIES_1, SEQ_1, SETFAM_1, ENUMSET1,
RELAT_1, FINANCE1, RANDOM_3, NUMBERS, XREAL_0, XXREAL_0, XCMPLX_0,
MEMBERED,
FUNCT_1, VALUED_1, NAT_1, FUNCT_2, PROB_1, SEQ_4, FINANCE2, RELSET_1,
FUNCOP_1, KOLMOG01, RANDOM_1;
constructors SERIES_1, REAL_1, RELSET_1, SEQ_4, FINANCE2, ENUMSET1, RANDOM_2,
KOLMOG01, RANDOM_1, RANDOM_3;
registrations PROB_1, FINANCE1, SUBSET_1, NAT_1, XREAL_0, MEMBERED, ORDINAL1,
FUNCT_2, NUMBERS, VALUED_0, VALUED_1, RELSET_1, INT_1, XBOOLE_0;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, FINANCE1, RANDOM_3;
equalities FINANCE1, SUBSET_1, XCMPLX_0, FINANCE2;
expansions FUNCT_2, MEMBERED, TARSKI, XBOOLE_0, PROB_1, FINANCE1;
theorems SERIES_1, FINANCE1, RANDOM_3, TARSKI, XBOOLE_0, PROB_1, NAT_1,
FUNCT_2, VALUED_1, XREAL_0, FUNCT_1, NUMBERS, SUBSET_1, ZFMISC_1,
ENUMSET1, FINANCE2, FUNCOP_1, RELAT_1, KOLMOG01, XBOOLE_1, ORDINAL1;
schemes NAT_1, FUNCT_2;
begin
Lemacik:
for a,b,c being 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 being 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 being 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 being 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 being 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 being 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 being SetSequence of {1,2,3,4} st
(ex n being Nat st A1.n = {}) holds Intersection A1 = {}
proof
let A1 be SetSequence of {1,2,3,4};
given n being Nat such that
AB: A1.n = {};
assume Intersection A1 <> {}; then
consider x being 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
for a, b being object st a <> b holds
{a} c< {a,b} by ZFMISC_1:7,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 being 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 being 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 being 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 being 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
for T being Nat holds
{w where w is Element of NAT: w>0 & w<=T} c=
{w where w is Element of NAT: w<=T}
proof
let T be Nat;
let x be object;
assume x in {w where w is Element of NAT: w>0 & w<=T}; then
consider w being Element of NAT such that B1: x=w & w>0 & w<=T;
thus thesis by B1;
end;
theorem
for T being Nat holds
{w where w is Element of NAT: w <= T} is non empty Subset of NAT
proof
let T be Nat;
B1: {w where w is Element of NAT: w <= T} c= NAT
proof
let x be object;
assume x in {w where w is Element of NAT: w <= T};
then consider w being Element of NAT such that C1: x=w & w<=T;
thus thesis by C1;
end;
T in {w where w is Element of NAT: w <= T}
proof
T in NAT by ORDINAL1:def 12;
hence thesis;
end;
hence thesis by B1;
end;
theorem
for T being Nat st T>0 holds
{w where w is 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 is Element of NAT: w>0 & w <= T} c= NAT
proof
let x be object;
assume x in {w where w is Element of NAT: w>0 & w <= T};
then consider w being 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 is Element of NAT: w>0 & w <= T};
hence thesis by B1;
end;
:: Special Random-Variables
theorem
for d being Nat,
phi being Real_Sequence,
Omega being non empty set,
F being SigmaField of Omega,
X being non empty set,
G being sequence of X,
w being 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;
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;
func RVPortfolioValueFutExt(phi,F,G,d) -> Function of Omega,REAL
means :Def2:
for w being 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 being 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 being Element of Omega holds f1.w =
PortfolioValueFutExt(d,phi,F,G,w) and
A3: for w being Element of Omega holds f2.w =
PortfolioValueFutExt(d,phi,F,G,w);
for w being 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
for Omega be non empty set
for F be SigmaField of Omega
for G be sequence of set_of_random_variables_on(F,Borel_Sets)
for phi be Real_Sequence
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 being 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 being Nat st J[n] holds J[n+1]
proof
let n be Nat;
assume B1: J[n];
C0: for w being 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 being 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 being 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;
redefine 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 being 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 being 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 being 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 being 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;
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;
func RVPortfolioValueFut(phi,F,G,d) -> Function of Omega,REAL means :Def4:
for w being 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 being 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 being Element of Omega holds f1.w =
PortfolioValueFut(d+1,phi,F,G,w) and
A3: for w being Element of Omega holds f2.w =
PortfolioValueFut(d+1,phi,F,G,w);
for w being 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
for Omega be non empty set
for F be SigmaField of Omega
for G be sequence of set_of_random_variables_on(F,Borel_Sets)
for phi be Real_Sequence
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 being 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 being 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 being Nat st J[n] holds J[n+1]
proof
let n be Nat;
assume B1: J[n];
C0: for w being 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 being 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 being Nat holds J[n] from NAT_1:sch 2(J0,J1);
hence thesis;
end;
theorem
for d being 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
for Omega being non empty set,
F being SigmaField of Omega,
X being non empty set,
G being sequence of X,
phi being Real_Sequence,
d being 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 being 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 being 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 being 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 being 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 being 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 being non empty set,
F being Function of Omega, Omega2,
y being non empty set holds
{z where z is 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 is 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 1A5:
for Omega, Omega2 being non empty set,
Sigma being SigmaField of Omega,
Sigma2 being SigmaField of Omega2,
s being Element of Omega2 holds
Omega --> s is_random_variable_on Sigma,Sigma2
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 being object holds
q in {w where w is 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 is Element of Omega: X.w is Element of x}; then
ex w being 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 is 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
for Omega being non empty set,
Sigma being SigmaField of Omega,
RV being random_variable of Sigma,Borel_Sets,
K being 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,RANDOM_3:def 1;
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;
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;
func Call-Option(RV,K) -> Function of Omega,REAL means
for w being 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 being 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 being 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 being 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 being 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 being 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;
:: Special sigma-Fields
theorem SuperLemma1:
for A1 being SetSequence of {1,2,3,4},
w being Real st w = 1 or w = 3 holds
(for n being 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 being 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 being object st
(for n being Nat holds x in A1.n) & not x in {w}
proof
per cases;
suppose ex j being Nat st A1.j={};
then consider j being Nat such that J0: A1.j={};
thus thesis by The1,J0,SUPP1;
end;
suppose USUPP1: for n being Nat holds A1.n<>{};
per cases;
suppose P1: for j being Nat holds {1,2} c= A1.j;
set x=2;
Z1: not x in {w} by TARSKI:def 1,KX;
for n being 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 being Nat st not {1,2} c= A1.j; then
consider j being Nat such that BSUPP1: not {1,2} c= A1.j;
per cases;
suppose P1: for n being Nat holds {3,4} c= A1.n;
set x=4;
Z1: not x in {w} by TARSKI:def 1,KX;
for n being 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 being Nat st not {3,4} c= A1.k;
then consider k being 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 being 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 SuperLemma2:
for A1 being SetSequence of {1,2,3,4},
w being Real st w = 2 or w = 4 holds
(for n being 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 being 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 being object st (for n being Nat holds x in A1.n) & not x in {w}
proof
per cases;
suppose ex j being Nat st A1.j={}; then
consider j being Nat such that J0: A1.j={};
thus thesis by The1,J0,SUPP1;
end;
suppose USUPP1: for n being Nat holds A1.n<>{};
per cases;
suppose P1: for j being Nat holds {1,2} c= A1.j;
set x=1;
Z1: not x in {w} by TARSKI:def 1,KX;
for n being 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 being Nat st not {1,2} c= A1.j;
then consider j being Nat such that BSUPP1: not {1,2} c= A1.j;
per cases;
suppose P1: for n being Nat holds {3,4} c= A1.n;
set x=3;
Z1: not x in {w} by TARSKI:def 1,KX;
for n being 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 being Nat st not {3,4} c= A1.k; then
consider k being 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 being 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
for MySigmaField, A1, A2 being 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 Lm700000:
for A1 being SetSequence of {1,2,3,4} st
(for n being Nat,k being 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 being Nat,k being 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 being 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 being 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 being 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 being Nat holds A1.n={1,2,3,4};
Intersection A1 = {1,2,3,4}
proof
for x being object holds
x in Intersection A1 iff x in {1,2,3,4}
proof
let x be object;
(for n being Nat holds x in A1.n) iff x in {1,2,3,4}
proof
(for n being Nat holds x in A1.n) implies x in {1,2,3,4}
proof
assume for n being Nat holds x in A1.n; then
x in A1.0; then
consider k being 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 being Nat st A1.n <> {1,2,3,4}; then
consider n being 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
for A1 being SetSequence of {1,2,3,4},
MyOmega being 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
for A1 being SetSequence of {1,2,3,4},
MyOmega being 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
for A1 being SetSequence of {1,2,3,4},
MyOmega being 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
for A1 being SetSequence of {1,2,3,4},
MyOmega being set st
MyOmega = {{},{1,2},{3,4},{1,2,3,4}} & Intersection A1={} holds
Intersection A1 in MyOmega by ENUMSET1:def 2;
theorem Lm8:
for MyOmega being set,
A1 being 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 being Nat,k being Nat st A1.n /\ A1.k = {};
CASE0: ex n being Nat,k being Nat st A1.n misses A1.k
proof
consider n being Nat,k being Nat such that
BCASE0: A1.n /\ A1.k = {} by CASE000;
A1.n misses A1.k by BCASE0;
hence thesis;
end;
CASE1: for y being object holds
(for n being Nat,k being Nat holds y in A1.k & y in A1.n) iff y in {}
proof
let y be object;
(for n being Nat,k being Nat holds y in A1.k & y in A1.n) implies
y in {}
proof
assume G1: for n being Nat,k being Nat holds y in A1.k & y in A1.n;
ex n being Nat,k being Nat st y in A1.k & y in A1.n & y in {}
proof
consider n being Nat,k being 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 being Nat,k being 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 being Nat,k being 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 Lm9:
for MySigmaField, MySet being set,
A1 being 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 being 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 being Nat st A1.n={}) implies Intersection A1={}
proof
assume ex n being Nat st A1.n={}; then
for x being 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 being 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 being Nat holds x in {1,2,3,4}
proof
thus x in Intersection A1 implies
for n being Nat holds x in {1,2,3,4}
proof
assume G1: x in Intersection A1;
for n being Nat holds x in {1,2,3,4}
proof
let n be Nat;
for x being 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 being Nat holds x in {1,2,3,4};
for n being 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
for MySigmaField, MySet being set,
A1 being SetSequence of MySet st
MySet={1,2,3,4} &
rng A1 c= MySigmaField & MySigmaField = {{},{1,2,3,4}} holds
for k1 being Nat, k2 being 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
func Special_SigmaField1 -> SigmaField of {1,2,3,4} equals
{{},{1,2,3,4}}; ::: it is "trivial" SigmaField cobool ({{},X}) from TEX_1
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,5;
end; then
reconsider MySigmaField as Subset-Family of {1,2,3,4};
A1: MySigmaField is compl-closed
proof
for A being 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; then
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 being 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
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 being object st x in MyOmega holds x in bool {1,2,3,4}
proof
let x be object;
assume x in MyOmega; then
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 being 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;
then 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
::$CD
end;
theorem
for Omega being 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
for Omega being 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 being 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 being 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}};
then 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
Special_SigmaField1 c< Special_SigmaField2 &
Special_SigmaField2 c< Trivial-SigmaField {1,2,3,4} by XX1,XX2;
:: Construction of Filtration and Examples
theorem
ex Omega being non empty set st
ex F1,F2,F3 being SigmaField of Omega st
F1 c< F2 & F2 c< F3
proof
Special_SigmaField1 c< Special_SigmaField2 by XX1;
hence thesis by XX2;
end;
theorem
ex Omega1,Omega2,Omega3,Omega4 being non empty set st
Omega1 c< Omega2 & Omega2 c< Omega3 & Omega3 c< Omega4 &
(ex F1 being SigmaField of Omega1,
F2 being SigmaField of Omega2,
F3 being SigmaField of Omega3,
F4 being 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,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;
mode Filtration of I,Sigma -> ManySortedSigmaField of I,Sigma means:Def2000:
for s,t being 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 being 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 being 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;
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};
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};
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 being SigmaField of {1,2,3,4},
I being set st I={1,2,3} & Sigma=bool{1,2,3,4} holds
ex MyFunc being 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 being 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 being 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 MyNeed:
for Omega being non empty set,
Sigma being SigmaField of Omega,
I being non empty real-membered set st
I={1,2,3} & Sigma=bool {1,2,3,4} & Omega = {1,2,3,4} holds
ex MyFunc being 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 being 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 is 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 is 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 being non empty set,
Sigma4 being SigmaField of Omega,
Sigma5 being 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;
set X = Omega --> 1REAL;
X is_random_variable_on Sigma4,Sigma5
proof
let x be set;
per cases;
suppose
A1: 1 in x;
for q being object holds
q in {w where w is 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 is Element of Omega: X.w is Element of x}; then
ex w being 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 is Element of Omega: X.w is Element of x}=Omega by TARSKI:2;
{w where w is 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 by RANDOM_3:def 1;
end;
theorem THJ1:
for Omega being non empty set,
Sigma being SigmaField of Omega,
Sigma2 being SigmaField of {1} st
Omega={1,2,3,4} holds
ex X1 being 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 being 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;
:: The first example of the existence of a random-variable depends
:: on a special underlying sigma-field and given Filtration
theorem
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 being Function of Omega,Omega2 st
for i being 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 being 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 being non empty real-membered set such that A5: I={1,2,3};
consider MyFunc being 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 being 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 being 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;
:: Next theorem gives also the existence of random_variables
:: depending on arbitrary sigma-fields and filtrations
theorem
for Omega, Omega2 being non empty set,
Sigma being SigmaField of Omega,
Sigma2 being SigmaField of Omega2,
I being non empty real-membered set,
Q being ManySortedSigmaField of I,Sigma holds
ex rv being Function of Omega,Omega2 st
for i being 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 being 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 being Function of Omega, Omega2 such that
B3: myfunc=Omega-->myset;
take myfunc;
let i be Element of I;
myfunc is_random_variable_on El_Filtration(i,Q),Sigma2
proof
for x being 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 being 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 by RANDOM_3:def 1;
end;
:: Stochastic Process: adapted and predictable
:: The next statement is important for the usage of a probability measure
:: with Events depending on SigmaFields in a given filtration.
theorem
for Omega being non empty set,
Sigma being SigmaField of Omega,
Sigma2 being SigmaField of Omega st Sigma2 c= Sigma holds
for E2 being Event of Sigma2 holds E2 is Event of Sigma;
:: Next we define the stochastic process
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;
mode Stochastic_Process of I,Sigma,Sigma2 ->
Function of I,set_of_random_variables_on(Sigma,Sigma2) means :Def30000:
for k being Element of I holds
ex RV being Function of Omega,Omega2 st
it.k=RV & RV is_random_variable_on Sigma,Sigma2;
existence
proof
set q = the Element of Omega2;
set F=Omega-->q;
A1: F is_random_variable_on Sigma,Sigma2 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 being
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 being Element of I holds
ex RV being Function of Omega,Omega2 st
fI1.k=RV & RV is_random_variable_on Sigma,Sigma2 by A1,B1;
hence thesis;
end;
end;
:: Because adapted and predicted stochastic processes are very important for
:: Stochastic finance, we implement them now:
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;
func RVProcess(Stoch,k) -> random_variable of Sigma,Sigma2 equals
Stoch.k;
coherence
proof
consider RV being Function of Omega,Omega2 such that
A0: Stoch.k=RV & RV is_random_variable_on Sigma,Sigma2 by Def30000;
thus thesis by A0,RANDOM_3:def 1;
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;
mode Adapted_Stochastic_Process of Stoch ->
Function of I,set_of_random_variables_on(Sigma,Sigma2) means :Def30002:
ex k being Filtration of I,Sigma st
for i being Element of I holds
RVProcess(Stoch,i) is_random_variable_on El_Filtration(i,k),Sigma2;
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 being Element of I holds F.i=Sigma by FUNCOP_1:7;
for i being 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 being 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 being Filtration of I,Sigma such that
C0: for i being Element of I holds F.i=Sigma by W2;
for i being Element of I holds
RVProcess(Stoch,i) is_random_variable_on El_Filtration(i,F),Sigma2
proof
let i be Element of I;
ex RV being Function of Omega,Omega2 st
Stoch.i=RV & RV is_random_variable_on Sigma,Sigma2 by Def30000;
hence thesis by C0;
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;
mode Predictable_Stochastic_Process of I,J,Sigma,Sigma2,Stoch ->
Function of J,set_of_random_variables_on(Sigma,Sigma2) means
ex k being Filtration of In(I,bool REAL), Sigma st
for j being Element of In(J,bool REAL),
i being Element of In(I,bool REAL) st j-1=i holds
RVProcess(Stoch,j) is_random_variable_on El_Filtration(i,k),Sigma2;
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 being Element of In(I,bool REAL) holds F.i=Sigma by FUNCOP_1:7;
for i being 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 being 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 being Filtration of In(I,bool REAL),Sigma such that
C0: for i being Element of In(I,bool REAL) holds F.i=Sigma by W2;
for j being Element of In(J,bool REAL),
i being Element of In(I,bool REAL)st j-1=i holds
RVProcess(Stoch,j) is_random_variable_on El_Filtration(i,F),Sigma2
proof
let j be Element of In(J,bool REAL);
let i be Element of In(I,bool REAL);
assume j-1=i;
ex RV being Function of Omega,Omega2 st
Stoch.j=RV & RV is_random_variable_on Sigma,Sigma2 by Def30000;
hence thesis by C0;
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;
attr Stoch is (MyFunc)-stoch_proc_wrt_to_Filtration means
for i being Element of I holds
RVProcess(Stoch,i) is_random_variable_on El_Filtration(i,MyFunc),Sigma2;
end;
theorem
for Omega,Omega2 being non empty set,
Sigma being SigmaField of Omega,
Sigma2 being SigmaField of Omega2,
I being non empty real-membered set,
MyFunc being Filtration of I,Sigma,
Stoch being 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;
:: Example for a Stochastic Process
definition
let k1,k2 be Element of REAL;
let Omega be non empty set;
let k be Element of Omega;
func Set1_for_RandomVariable(k1,k2,k) -> Element of REAL equals
k1 if (k=1 or k=2) otherwise k2;
correctness;
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;
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;
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 MYF30:
for k1,k2,k3,k4 being Element of REAL holds
for Omega being set st Omega={1,2,3,4}
ex f being 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 being Function of Omega,REAL such that
B1: for d being Element of Omega holds f.d = U(d) from FUNCT_2:sch 4;
B2: f.1=k1
proof
consider k being 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 being 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 being 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 being 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 MyFunc5:
for k1,k2,k3,k4 be Element of REAL holds
for Omega being non empty set st Omega={1,2,3,4} holds
for Sigma being SigmaField of Omega,
I being non empty real-membered set,
MyFunc being ManySortedSigmaField of I,Sigma st
MyFunc.1=Special_SigmaField1 &
MyFunc.2=Special_SigmaField2 &
MyFunc.3=Trivial-SigmaField {1,2,3,4} holds
for eli being Element of I st eli=3 holds
ex f being Function of Omega,REAL st
f.1=k1 & f.2=k2 & f.3=k3 & f.4=k4 &
f is_random_variable_on El_Filtration(eli,MyFunc),Borel_Sets
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 being 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 being 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_random_variable_on El_Filtration(eli,MyFunc),Borel_Sets
proof
set i=eli;
for x being 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 being object holds
z in {1,2,3,4} iff ex y being object st [z,y] in f & y in x
proof
let z be object;
thus z in {1,2,3,4} implies
ex y being 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 being 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 being 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 being object holds
z in {1,2,3} iff ex y being object st [z,y] in f & y in x
proof
let z be object;
thus z in {1,2,3} implies
ex y being 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 being 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 being 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 being object holds
z in {1,2,4} iff ex y being object st [z,y] in f & y in x
proof
let z be object;
thus z in {1,2,4} implies
ex y being 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 being 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 being 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 being object holds z in {1,2} iff
ex y being object st [z,y] in f & y in x
proof
let z be object;
thus z in {1,2} implies
ex y being 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 being 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 being 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 being object holds
z in {1,3,4} iff ex y being object st [z,y] in f & y in x
proof
let z be object;
thus z in {1,3,4} implies
ex y being 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 being 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 being 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 being object holds
z in {1,3} iff ex y being object st [z,y] in f & y in x
proof
let z be object;
thus z in {1,3} implies
ex y being 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 being 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 being 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 being object holds
z in {1,4} iff ex y being object st [z,y] in f & y in x
proof
let z be object;
thus z in {1,4} implies
ex y being 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 being 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 being 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 being object holds
z in {1} iff ex y being object st [z,y] in f & y in x
proof
let z be object;
thus z in {1} implies
ex y being 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 being 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 being 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 being object holds z in {2,3,4} iff
ex y being object st [z,y] in f & y in x
proof
let z be object;
thus z in {2,3,4} implies
ex y being 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 being 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 being 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 being object holds
z in {2,3} iff ex y being object st [z,y] in f & y in x
proof
let z be object;
thus z in {2,3} implies
ex y being 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 being 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 being 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 being object holds z in {2,4} iff
ex y being object st [z,y] in f & y in x
proof
let z be object;
thus z in {2,4} implies
ex y being 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 being 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 being 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 being object holds
z in {2} iff ex y being object st [z,y] in f & y in x
proof
let z be object;
thus z in {2} implies
ex y being 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 being 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 being 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 being object holds
z in {3,4} iff ex y being object st [z,y] in f & y in x
proof
let z be object;
thus z in {3,4} implies
ex y being 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 being 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 being 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 being object holds
z in {3} iff ex y being object st [z,y] in f & y in x
proof
let z be object;
thus z in {3} implies
ex y being 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 being 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 being 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 being object holds
z in {4} iff ex y being object st [z,y] in f & y in x
proof
let z be object;
thus z in {4} implies
ex y being 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 being 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 being 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 being object holds
z in {} iff ex y being object st [z,y] in f & y in x
proof
let z be object;
(ex y being object st [z,y] in f & y in x) implies z in {}
proof
given y being 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 MyFunc6:
for k1,k2 being Element of REAL,
Omega being non empty set st Omega={1,2,3,4} holds
for Sigma being SigmaField of Omega,
I being non empty real-membered set,
MyFunc being ManySortedSigmaField of I,Sigma st
MyFunc.1=Special_SigmaField1 &
MyFunc.2=Special_SigmaField2 &
MyFunc.3=Trivial-SigmaField {1,2,3,4} holds
for eli being Element of I st eli=2 holds
ex f being Function of Omega,REAL st
f.1=k1 & f.2=k1 & f.3=k2 & f.4=k2 &
f is_random_variable_on El_Filtration(eli,MyFunc),Borel_Sets
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 being 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 being 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 being object holds z in {1,2,3,4} iff
ex y being object st [z,y] in f & y in x
proof
let z be object;
I1: z in {1,2,3,4} implies
ex y being 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 being object st [z,y] in f & y in x) implies
z in {1,2,3,4}
proof
given y being 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 being object holds
z in {1,2} iff ex y being object st [z,y] in f & y in x
proof
let z be object;
I1: z in {1,2} implies
ex y being 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 being object st [z,y] in f & y in x) implies z in {1,2}
proof
given y being 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 being object holds z in {3,4} iff
ex y being object st [z,y] in f & y in x
proof
let z be object;
I1: z in {3,4} implies ex y being 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 being object st [z,y] in f & y in x) implies
z in {3,4}
proof
given y being 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 being object holds
z in {} iff ex y being object st [z,y] in f & y in x
proof
let z be object;
(ex y being object st [z,y] in f & y in x) implies z in {}
proof
given y being 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 MyFunc7:
for k1 being Element of REAL,
Omega being non empty set st Omega={1,2,3,4} holds
for Sigma being SigmaField of Omega,
I being non empty real-membered set,
MyFunc being ManySortedSigmaField of I,Sigma st
MyFunc.1=Special_SigmaField1 &
MyFunc.2=Special_SigmaField2 &
MyFunc.3=Trivial-SigmaField {1,2,3,4} holds
for eli being Element of I st eli=1 holds
ex f being Function of Omega,REAL st
f.1=k1 & f.2=k1 & f.3=k1 & f.4=k1 &
f is_random_variable_on El_Filtration(eli,MyFunc),Borel_Sets
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 being 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 being 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 being object holds z in {1,2,3,4} iff
ex y being object st [z,y] in f & y in x
proof
let z be object;
I1: z in {1,2,3,4} implies
ex y being 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 being object st [z,y] in f & y in x) implies
z in {1,2,3,4}
proof
given y being 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 being object holds z in {} iff
ex y being object st [z,y] in f & y in x
proof
let z be object;
(ex y being object st [z,y] in f & y in x) implies z in {}
proof
given y being 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
for Omega being non empty set st Omega={1,2,3,4} holds
for Sigma being SigmaField of Omega,
I being non empty real-membered set
st I={1,2,3} & Sigma = bool {1,2,3,4} holds
for MyFunc being ManySortedSigmaField of I,Sigma st
MyFunc.1=Special_SigmaField1 &
MyFunc.2=Special_SigmaField2 &
MyFunc.3=Trivial-SigmaField {1,2,3,4} holds
for Prob being Function of Sigma, REAL holds
for i being Element of I holds
ex RV being Function of Omega,REAL st
RV is_random_variable_on El_Filtration(i,MyFunc),Borel_Sets
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 being Function of Omega,REAL st
f.1=100 & f.2=100 & f.3=100 & f.4=100 &
f is_random_variable_on El_Filtration(i,MyFunc),Borel_Sets
by A0,A2,MyFunc7,a1;
hence thesis;
end;
suppose a1: i=2;
80 in REAL & 120 in REAL by NUMBERS:19; then
ex f being Function of Omega,REAL st
f.1=80 & f.2=80 & f.3=120 & f.4=120 &
f is_random_variable_on El_Filtration(i,MyFunc),Borel_Sets
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 being Function of Omega,REAL st
f.1=60 & f.2=80 & f.3=100 & f.4=120 &
f is_random_variable_on El_Filtration(i,MyFunc),Borel_Sets
by A0,A2,MyFunc5,a1;
hence thesis;
end;
end;
definition
let I be non empty real-membered set such that A0000: I={1,2,3};
let i be Element of I such that MyI: i=2 or i=3;
let Omega be non empty set such that A000: Omega={1,2,3,4};
let Sigma be SigmaField of Omega such that A00: Sigma=bool Omega;
let f1 be Function of Omega,REAL such that
A0: f1.1=60 & f1.2=80 & f1.3=100 & f1.4=120;
let f2 be Function of Omega,REAL such that
A1: f2.1=80 & f2.2=80 & f2.3=120 & f2.4=120;
let f3 be Function of Omega,REAL;
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 being 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 being Function of Omega,REAL such that
B4: f.1=80 & f.2=80 & f.3=120 & f.4=120 &
f is_random_variable_on El_Filtration(i,MyFunc),Borel_Sets
by A000,B1,MyFunc6,SUPP;
f is_random_variable_on Sigma,Borel_Sets
proof
for x being set st x in Borel_Sets holds f"x in Sigma by A00;
hence thesis;
end; 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 being 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 being Function of Omega,REAL such that
B4: f.1=60 & f.2=80 & f.3=100 & f.4=120 &
f is_random_variable_on El_Filtration(i,MyFunc),Borel_Sets
by A000,B1,MyFunc5,MyI,F1;
f is_random_variable_on Sigma,Borel_Sets
proof
for x being set st x in Borel_Sets holds f"x in Sigma by A00;
hence thesis;
end; 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 being 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 such that A0000: I={1,2,3};
let i be Element of I;
let Omega be non empty set such that A000: Omega={1,2,3,4};
let Sigma be SigmaField of Omega such that A00: Sigma=bool Omega;
let f1,f2 be Function of Omega,REAL;
let f3 be Function of Omega,REAL such that
A2: f3.1=100 & f3.2=100 & f3.3=100 & f3.4=100;
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 being 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 being Function of Omega,REAL such that
B4: f.1=100 & f.2=100 & f.3=100 & f.4=100 &
f is_random_variable_on El_Filtration(i,MyFunc),Borel_Sets
by A000,B1,B3,MyFunc7;
f is_random_variable_on Sigma,Borel_Sets
proof
for x being set st x in Borel_Sets holds f"x in Sigma by A00;
hence thesis;
end; 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 being 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
for Omega, Omega2 being non empty set st Omega={1,2,3,4} holds
for Sigma being SigmaField of Omega,
I being non empty real-membered set st
I={1,2,3} & Sigma=bool{1,2,3,4} holds
for MyFunc being Filtration of I,Sigma st
MyFunc.1=Special_SigmaField1 &
MyFunc.2=Special_SigmaField2 &
MyFunc.3=Trivial-SigmaField {1,2,3,4}
ex Stoch being Stochastic_Process of I,Sigma,Borel_Sets st
(for k being Element of I holds
(ex RV being Function of Omega,REAL st
(Stoch.k=RV & RV is_random_variable_on Sigma,Borel_Sets &
RV is_random_variable_on El_Filtration(k,MyFunc),Borel_Sets)) &
(ex f being 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 being 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 being 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 being 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 being 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 being 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 being
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 being Element of I holds
ex RV being Function of Omega,REAL st
(fI1.k=RV & RV is_random_variable_on Sigma,Borel_Sets)
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 being Element of I holds
(ex RV being Function of Omega,REAL st
(fI1.k=RV & RV is_random_variable_on Sigma,Borel_Sets &
RV is_random_variable_on El_Filtration(k,MyFunc),Borel_Sets)) &
(ex f being 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 being 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 being 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 being Element of I holds
RVProcess(fI1,i) is_random_variable_on El_Filtration(i,MyFunc),Borel_Sets
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 being Function of Omega,REAL such that
Q1: f.1=100 & f.2=100 & f.3=100 & f.4=100 &
f is_random_variable_on El_Filtration(i,MyFunc),Borel_Sets
by SUPP,A00,A1,MyFunc7;
E1: dom f=Omega by FUNCT_2:def 1;
for x being 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 being Function of Omega,REAL such that
Q1: f.1=80 & f.2=80 & f.3=120 & f.4=120 &
f is_random_variable_on El_Filtration(i,MyFunc),Borel_Sets
by SUPP2,A00,A1,MyFunc6;
E1: dom f=Omega by FUNCT_2:def 1;
for x being 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 being Function of Omega,REAL such that
Q1: f.1=60 & f.2=80 & f.3=100 & f.4=120 &
f is_random_variable_on El_Filtration(i,MyFunc),Borel_Sets
by SUPP1,A00,A1,MyFunc5;
E1:dom f=Omega by FUNCT_2:def 1;
for x being 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 being Element of I holds
(ex RV being Function of Omega,REAL st
(fI1.k=RV & RV is_random_variable_on Sigma,Borel_Sets &
RV is_random_variable_on El_Filtration(k,MyFunc),Borel_Sets)) &
(ex f being 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 being 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 being 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 being Function of Omega,REAL such that O1:
fI1.k=RV & RV is_random_variable_on Sigma,Borel_Sets by Fin1;
o1: RV is_random_variable_on El_Filtration(k,MyFunc),Borel_Sets
proof
fI1.k=RVProcess(fI1,k) &
RVProcess(fI1,k) is_random_variable_on El_Filtration(k,MyFunc),Borel_Sets
by Fin3;
hence thesis by O1;
end;
GFin2: ex f being 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 being 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 being 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;