:: Events of Borel Sets, Construction of Borel Sets and Random Variables for Stochastic Finance
:: by Peter Jaeger
::
:: Copyright (c) 2014-2019 Association of Mizar Users

:: We start with some theorems which are necessary to prove, that IRRAT is an
:: Event of the Borel-Sets
theorem Ko1: :: FINANCE2:1
( 1 in REAL & - 1 in REAL )
proof end;

theorem Th5: :: FINANCE2:2
proof end;

theorem Th6: :: FINANCE2:3
proof end;

theorem Th7: :: FINANCE2:4
proof end;

registration
cluster REAL \ RAT -> non empty ;
coherence
not REAL \ RAT is empty
by Th5;
cluster REAL \ INT -> non empty ;
coherence
not REAL \ INT is empty
by Th6;
cluster REAL \ NAT -> non empty ;
coherence
not REAL \ NAT is empty
by Th7;
end;

theorem Th1: :: FINANCE2:5
for k being Real holds {k} in Borel_Sets
proof end;

theorem :: FINANCE2:6
for k1, k2 being Real holds ].k1,k2.] is Event of Borel_Sets
proof end;

definition
func Family_of_halflines2 -> Subset-Family of REAL equals :: FINANCE2:def 1
{ where r is Element of REAL : verum } ;
coherence
{ where r is Element of REAL : verum } is Subset-Family of REAL
proof end;
end;

:: deftheorem defines Family_of_halflines2 FINANCE2:def 1 :
Family_of_halflines2 = { where r is Element of REAL : verum } ;

theorem :: FINANCE2:7
for Exy being ExtReal holds {Exy} is Subset of ExtREAL by ;

theorem :: FINANCE2:8
for Y being set
for k being Nat st Y = REAL \ {k} holds
Y is Event of Borel_Sets
proof end;

theorem :: FINANCE2:9
ex A being SetSequence of NAT st
for n being Nat holds A . n = {n}
proof end;

theorem :: FINANCE2:10
for A being SetSequence of NAT st ( for n being Nat holds A . n = {n} ) holds
for n being Nat holds () . n in Borel_Sets
proof end;

theorem :: FINANCE2:11
proof end;

Q00: ex A1 being SetSequence of REAL st
for n being Nat holds A1 . n = {n}

proof end;

Q0: ex A being SetSequence of Borel_Sets st
for n being Nat holds A . n = {n}

proof end;

H2: ex A being SetSequence of REAL st
for n being Nat holds A . n = {(- n)}

proof end;

theorem ZV5: :: FINANCE2:12
proof end;

theorem :: FINANCE2:13
proof end;

theorem ThA: :: FINANCE2:14
for AA being SetSequence of REAL ex A being SetSequence of REAL st
for n being Nat holds A . n = () . n
proof end;

theorem Th40: :: FINANCE2:15
proof end;

definition
let k be Nat;
let pm be Element of REAL ;
func GoCross_Seq_REAL (pm,k) -> SetSequence of REAL means :Def4: :: FINANCE2:def 2
for n being Nat holds it . n = {((pm * k) * ((n + 1) "))};
existence
ex b1 being SetSequence of REAL st
for n being Nat holds b1 . n = {((pm * k) * ((n + 1) "))}
proof end;
uniqueness
for b1, b2 being SetSequence of REAL st ( for n being Nat holds b1 . n = {((pm * k) * ((n + 1) "))} ) & ( for n being Nat holds b2 . n = {((pm * k) * ((n + 1) "))} ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines GoCross_Seq_REAL FINANCE2:def 2 :
for k being Nat
for pm being Element of REAL
for b3 being SetSequence of REAL holds
( b3 = GoCross_Seq_REAL (pm,k) iff for n being Nat holds b3 . n = {((pm * k) * ((n + 1) "))} );

definition
let k be Nat;
let pm be Element of REAL ;
:: original: GoCross_Seq_REAL
redefine func GoCross_Seq_REAL (pm,k) -> SetSequence of Borel_Sets ;
correctness
coherence
GoCross_Seq_REAL (pm,k) is SetSequence of Borel_Sets
;
proof end;
end;

registration
let k be Nat;
let pm be Element of REAL ;
coherence
GoCross_Seq_REAL (pm,k) is Borel_Sets -valued
;
end;

theorem :: FINANCE2:16
for pm being Element of REAL
for k being Nat st k > 0 & pm <> 0 holds
GoCross_Seq_REAL (pm,k) is one-to-one
proof end;

definition
let k be Nat;
let pm be Element of REAL ;
func GoCross_Partial_Union (pm,k) -> SetSequence of REAL means :Def5: :: FINANCE2:def 3
( it . 0 = (GoCross_Seq_REAL (pm,k)) . 0 & ( for n being Nat holds it . (n + 1) = (it . n) \/ ((GoCross_Seq_REAL (pm,k)) . (n + 1)) ) );
existence
ex b1 being SetSequence of REAL st
( b1 . 0 = (GoCross_Seq_REAL (pm,k)) . 0 & ( for n being Nat holds b1 . (n + 1) = (b1 . n) \/ ((GoCross_Seq_REAL (pm,k)) . (n + 1)) ) )
proof end;
uniqueness
for b1, b2 being SetSequence of REAL st b1 . 0 = (GoCross_Seq_REAL (pm,k)) . 0 & ( for n being Nat holds b1 . (n + 1) = (b1 . n) \/ ((GoCross_Seq_REAL (pm,k)) . (n + 1)) ) & b2 . 0 = (GoCross_Seq_REAL (pm,k)) . 0 & ( for n being Nat holds b2 . (n + 1) = (b2 . n) \/ ((GoCross_Seq_REAL (pm,k)) . (n + 1)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines GoCross_Partial_Union FINANCE2:def 3 :
for k being Nat
for pm being Element of REAL
for b3 being SetSequence of REAL holds
( b3 = GoCross_Partial_Union (pm,k) iff ( b3 . 0 = (GoCross_Seq_REAL (pm,k)) . 0 & ( for n being Nat holds b3 . (n + 1) = (b3 . n) \/ ((GoCross_Seq_REAL (pm,k)) . (n + 1)) ) ) );

definition
let k be Nat;
let pm be Element of REAL ;
:: original: GoCross_Partial_Union
redefine func GoCross_Partial_Union (pm,k) -> SetSequence of Borel_Sets ;
correctness
coherence
GoCross_Partial_Union (pm,k) is SetSequence of Borel_Sets
;
proof end;
end;

registration
let k be Nat;
let pm be Element of REAL ;
coherence ;
end;

registration
let k be Nat;
let pm be Element of REAL ;
coherence
GoCross_Partial_Union (pm,k) is non-descending
proof end;
end;

definition
let pm be Element of REAL ;
func GoCross_Union pm -> SetSequence of REAL means :Def6: :: FINANCE2:def 4
( it . 0 = Union () & ( for n being Nat holds it . (n + 1) = (it . n) \/ (Union (GoCross_Partial_Union (pm,(n + 1)))) ) );
existence
ex b1 being SetSequence of REAL st
( b1 . 0 = Union () & ( for n being Nat holds b1 . (n + 1) = (b1 . n) \/ (Union (GoCross_Partial_Union (pm,(n + 1)))) ) )
proof end;
uniqueness
for b1, b2 being SetSequence of REAL st b1 . 0 = Union () & ( for n being Nat holds b1 . (n + 1) = (b1 . n) \/ (Union (GoCross_Partial_Union (pm,(n + 1)))) ) & b2 . 0 = Union () & ( for n being Nat holds b2 . (n + 1) = (b2 . n) \/ (Union (GoCross_Partial_Union (pm,(n + 1)))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines GoCross_Union FINANCE2:def 4 :
for pm being Element of REAL
for b2 being SetSequence of REAL holds
( b2 = GoCross_Union pm iff ( b2 . 0 = Union () & ( for n being Nat holds b2 . (n + 1) = (b2 . n) \/ (Union (GoCross_Partial_Union (pm,(n + 1)))) ) ) );

definition
let pm be Element of REAL ;
:: original: GoCross_Union
redefine func GoCross_Union pm -> SetSequence of Borel_Sets ;
correctness
coherence ;
proof end;
end;

registration
let pm be Element of REAL ;
coherence ;
end;

registration
let pm be Element of REAL ;
coherence
proof end;
end;

theorem Th3: :: FINANCE2:17
for mym, myp being Element of REAL st mym = 1 & myp = - 1 holds
(Union ()) \/ (Union ()) = RAT
proof end;

theorem Th41: :: FINANCE2:18
proof end;

theorem :: FINANCE2:19
proof end;

theorem :: FINANCE2:20
proof end;

theorem :: FINANCE2:21
proof end;

:: Since the Borel-Sets can be constructed by different sets of intervals,
:: we show, that other sets can do this.
theorem :: FINANCE2:22
proof end;

theorem :: FINANCE2:23
for Omega being non empty set
for Sigma being SigmaField of Omega
for X, Y being random_variable of Sigma, Borel_Sets holds X + Y is random_variable of Sigma, Borel_Sets
proof end;

theorem :: FINANCE2:24
for Omega being non empty set
for Sigma being SigmaField of Omega
for X, Y being random_variable of Sigma, Borel_Sets holds X - Y is random_variable of Sigma, Borel_Sets
proof end;

theorem :: FINANCE2:25
for Omega being non empty set
for Sigma being SigmaField of Omega
for X, Y being random_variable of Sigma, Borel_Sets holds X (#) Y is random_variable of Sigma, Borel_Sets
proof end;

theorem Th8: :: FINANCE2:26
for Omega being non empty set
for Sigma being SigmaField of Omega
for r being Real
for X being random_variable of Sigma, Borel_Sets holds r (#) X is random_variable of Sigma, Borel_Sets
proof end;

theorem T: :: FINANCE2:27
for Omega, Omega2 being non empty set
for F being SigmaField of Omega
for F2 being SigmaField of Omega2
for k being Element of set_of_random_variables_on (F,F2) holds Change_Element_to_Func (F,F2,k) is random_variable of F,F2
proof end;

theorem T1: :: FINANCE2:28
for Omega being non empty set
for F being SigmaField of Omega
for k being Element of set_of_random_variables_on (F,Borel_Sets) holds ElementsOfPortfolioValueProb_fut (F,k) is random_variable of F, Borel_Sets
proof end;

theorem :: FINANCE2:29
for p being Nat
for Omega, Omega2 being non empty set
for F being SigmaField of Omega
for F2 being SigmaField of Omega2
for G being sequence of () holds Element_Of (F,F2,G,p) is random_variable of F,F2
proof 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 n be Nat;
func RVElementsOfPortfolioValue_fut (phi,F,G,n) -> Function of Omega,REAL means :Def5000: :: FINANCE2:def 5
for w being Element of Omega holds it . w = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n);
existence
ex b1 being Function of Omega,REAL st
for w being Element of Omega holds b1 . w = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n)
proof end;
uniqueness
for b1, b2 being Function of Omega,REAL st ( for w being Element of Omega holds b1 . w = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) ) & ( for w being Element of Omega holds b2 . w = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5000 defines RVElementsOfPortfolioValue_fut FINANCE2:def 5 :
for Omega being non empty set
for F being SigmaField of Omega
for X being non empty set
for G being sequence of X
for phi being Real_Sequence
for n being Nat
for b7 being Function of Omega,REAL holds
( b7 = RVElementsOfPortfolioValue_fut (phi,F,G,n) iff for w being Element of Omega holds b7 . w = ((ElementsOfPortfolioValueProb_fut (F,(G . n))) . w) * (phi . n) );

theorem :: FINANCE2:30
for Omega being non empty set
for F being SigmaField of Omega
for G being sequence of
for phi being Real_Sequence
for n being Nat holds RVElementsOfPortfolioValue_fut (phi,F,G,n) is random_variable of F, Borel_Sets
proof end;

definition
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;
func RVPortfolioValueFutExt_El (phi,F,G,w) -> Real_Sequence means :Def5001: :: FINANCE2:def 6
for n being Nat holds it . n = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w;
existence
ex b1 being Real_Sequence st
for n being Nat holds b1 . n = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w ) & ( for n being Nat holds b2 . n = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5001 defines RVPortfolioValueFutExt_El FINANCE2:def 6 :
for phi being Real_Sequence
for Omega being non empty set
for F being SigmaField of Omega
for X being non empty set
for G being sequence of X
for w being Element of Omega
for b7 being Real_Sequence holds
( b7 = RVPortfolioValueFutExt_El (phi,F,G,w) iff for n being Nat holds b7 . n = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w );

definition
let d be Nat;
let phi be Real_Sequence;
let Omega be non empty set ;
let F be SigmaField of Omega;
let X be non empty set ;
let G be sequence of X;
let w be Element of Omega;
:: original: PortfolioValueFutExt
redefine func PortfolioValueFutExt (d,phi,F,G,w) -> Real equals :: FINANCE2:def 7
(Partial_Sums (RVPortfolioValueFutExt_El (phi,F,G,w))) . d;
correctness
coherence
PortfolioValueFutExt (d,phi,F,G,w) is Real
;
compatibility
for b1 being Real holds
( b1 = PortfolioValueFutExt (d,phi,F,G,w) iff b1 = (Partial_Sums (RVPortfolioValueFutExt_El (phi,F,G,w))) . d )
;
proof end;
end;

:: deftheorem defines PortfolioValueFutExt FINANCE2:def 7 :
for d being Nat
for phi being Real_Sequence
for Omega being non empty set
for F being SigmaField of Omega
for X being non empty set
for G being sequence of X
for w being Element of Omega holds PortfolioValueFutExt (d,phi,F,G,w) = (Partial_Sums (RVPortfolioValueFutExt_El (phi,F,G,w))) . d;