:: Events of Borel Sets, Construction of Borel Sets and Random Variables
:: for Stochastic Finance
:: by Peter Jaeger
::
:: Received July 10, 2014
:: Copyright (c) 2014-2021 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, PROB_3, SERIES_1, SEQ_1, XXREAL_1, RANDOM_3, FINANCE2,
NUMBERS, XBOOLE_0, PROB_1, SUBSET_1, REAL_1, TARSKI, RELAT_1, FUNCT_1,
ARYTM_3, XXREAL_0, BORSUK_5, VALUED_1, ARYTM_1, NAT_1, CARD_3, CARD_1,
ZFMISC_1, RPR_1, POWER, RANDOM_1, FUNCT_7, SETFAM_1, INT_1, RAT_1,
LIMFUNC1;
notations TARSKI, SUBSET_1, XBOOLE_0, ORDINAL1, PROB_3, SERIES_1, SEQ_1,
XXREAL_1, RCOMP_1, SETFAM_1, RELAT_1, FINANCE1, RANDOM_3, NUMBERS,
XREAL_0, XXREAL_0, XCMPLX_0, FUNCT_1, REAL_1, VALUED_1, NAT_1, FUNCT_2,
PROB_1, LIMFUNC1, RANDOM_1, FINSUB_1, INT_1, RAT_1, IRRAT_1, SEQ_4,
BORSUK_5;
constructors PROB_3, SERIES_1, FINANCE1, RANDOM_3, REAL_1, RELSET_1, RCOMP_1,
SEQ_4, BORSUK_5, LIMFUNC1;
registrations PROB_1, FINANCE1, SUBSET_1, NAT_1, XREAL_0, XXREAL_0, MEMBERED,
ORDINAL1, FUNCT_2, NUMBERS, VALUED_0, VALUED_1, RELSET_1, FINSUB_1,
INT_1, BORSUK_5, RAT_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin :: Events of Borel-Sets
:: We start with some theorems which are necessary to prove, that IRRAT is an
:: Event of the Borel-Sets
theorem :: FINANCE2:1
1 in REAL & -1 in REAL;
theorem :: FINANCE2:2
number_e in REAL\RAT;
theorem :: FINANCE2:3
number_e in REAL\INT;
theorem :: FINANCE2:4
number_e in REAL\NAT;
registration
cluster REAL \ RAT -> non empty;
cluster REAL \ INT -> non empty;
cluster REAL \ NAT -> non empty;
end;
theorem :: FINANCE2:5
for k being Real holds {k} in Borel_Sets;
theorem :: FINANCE2:6
for k1,k2 being Real holds ].k1,k2.] is Event of Borel_Sets;
definition
func Family_of_halflines2 -> Subset-Family of REAL equals
:: FINANCE2:def 1
the set of all right_closed_halfline(r) where r is Element of REAL;
end;
theorem :: FINANCE2:7
for Exy being ExtReal holds
{Exy} is Subset of ExtREAL;
theorem :: FINANCE2:8
for Y being set, k being Nat st Y = REAL \ {k} holds
Y is Event of Borel_Sets;
reserve Exx for Real;
theorem :: FINANCE2:9
ex A being SetSequence of NAT st for n being Nat holds A.n = {n};
theorem :: FINANCE2:10
for A being SetSequence of NAT st
(for n being Nat holds A.n = {n}) holds
for n being Nat holds (Partial_Union A).n in Borel_Sets;
theorem :: FINANCE2:11
REAL is Event of Borel_Sets;
theorem :: FINANCE2:12
NAT is Event of Borel_Sets;
theorem :: FINANCE2:13
REAL \ NAT is Event of Borel_Sets;
theorem :: FINANCE2:14
for AA being SetSequence of REAL holds
ex A being SetSequence of REAL st
for n being Nat holds A.n=(Partial_Union AA).n;
theorem :: FINANCE2:15
INT is Event of Borel_Sets;
definition
let k be Nat;
let pm be Element of REAL;
func GoCross_Seq_REAL(pm,k) -> SetSequence of REAL means
:: FINANCE2:def 2
for n being Nat holds it.n = {pm*k*(n+1)"};
end;
definition
let k be Nat;
let pm be Element of REAL;
redefine func GoCross_Seq_REAL(pm,k) -> SetSequence of Borel_Sets;
end;
registration
let k be Nat;
let pm be Element of REAL;
cluster GoCross_Seq_REAL(pm,k) -> Borel_Sets-valued;
end;
theorem :: FINANCE2:16
for pm being Element of REAL, k being Nat st
k>0 & pm<>0 holds GoCross_Seq_REAL(pm,k) is one-to-one;
definition
let k be Nat;
let pm be Element of REAL;
func GoCross_Partial_Union(pm,k) -> SetSequence of REAL means
:: 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);
end;
definition
let k be Nat;
let pm be Element of REAL;
redefine func GoCross_Partial_Union(pm,k) -> SetSequence of Borel_Sets;
end;
registration
let k be Nat;
let pm be Element of REAL;
cluster GoCross_Partial_Union(pm,k) -> Borel_Sets-valued;
end;
registration
let k be Nat;
let pm be Element of REAL;
cluster GoCross_Partial_Union(pm,k) -> non-descending;
end;
definition
let pm be Element of REAL;
func GoCross_Union(pm) -> SetSequence of REAL means
:: FINANCE2:def 4
it.0 = Union GoCross_Partial_Union(pm,0) &
for n being Nat holds
it.(n+1) = it.n \/ Union GoCross_Partial_Union(pm,(n+1));
end;
definition
let pm be Element of REAL;
redefine func GoCross_Union(pm) -> SetSequence of Borel_Sets;
end;
registration
let pm be Element of REAL;
cluster GoCross_Union(pm) -> Borel_Sets-valued;
end;
registration
let pm be Element of REAL;
cluster GoCross_Union(pm) -> non-descending;
end;
theorem :: FINANCE2:17
for mym,myp being Element of REAL st mym=1 & myp=-1 holds
Union GoCross_Union(mym) \/ Union GoCross_Union(myp) = RAT;
theorem :: FINANCE2:18
RAT is Event of Borel_Sets;
theorem :: FINANCE2:19
REAL \ INT is Event of Borel_Sets;
theorem :: FINANCE2:20
REAL \ RAT is Event of Borel_Sets;
theorem :: FINANCE2:21
IRRAT is Event of Borel_Sets;
begin :: Construction of Borel-Sets
:: Since the Borel-Sets can be constructed by different sets of intervals,
:: we show, that other sets can do this.
theorem :: FINANCE2:22
Borel_Sets = sigma Family_of_halflines2;
begin :: Random-Variables for Stochastic Finance in Discrete Time
:: The aim is to show, that certain functions are Random-Variables, in order
:: to use theorems of Article RANDOM_3. An example for this application is the
:: definition of the arbitrage opportunity, which uses a Random-Variable
:: combined with a Probability-Measure.
reserve Omega,Omega2 for non empty set;
reserve Sigma for SigmaField of Omega;
reserve Sigma2 for SigmaField of Omega2;
reserve X,Y,Z for Function of Omega,REAL;
theorem :: FINANCE2:23
for X,Y being random_variable of Sigma,Borel_Sets holds
X+Y is random_variable of Sigma, Borel_Sets;
theorem :: FINANCE2:24
for X,Y being random_variable of Sigma,Borel_Sets holds
X-Y is random_variable of Sigma, Borel_Sets;
theorem :: FINANCE2:25
for X,Y being random_variable of Sigma,Borel_Sets holds
X(#)Y is random_variable of Sigma, Borel_Sets;
theorem :: FINANCE2:26
for r being Real,
X being random_variable of Sigma,Borel_Sets holds
r(#)X is random_variable of Sigma, Borel_Sets;
theorem :: FINANCE2:27
for Omega,Omega2 be non empty set
for F be SigmaField of Omega
for F2 be SigmaField of Omega2
for k be Element of set_of_random_variables_on(F,F2) holds
Change_Element_to_Func(F,F2,k) is random_variable of F,F2;
theorem :: FINANCE2:28
for Omega be non empty set
for F be SigmaField of Omega
for k be Element of set_of_random_variables_on(F,Borel_Sets) holds
ElementsOfPortfolioValueProb_fut(F,k) is
random_variable of F,Borel_Sets;
theorem :: FINANCE2:29
for p be Nat
for Omega, Omega2 be non empty set
for F be SigmaField of Omega
for F2 be SigmaField of Omega2
for G be sequence of set_of_random_variables_on(F,F2) holds
Element_Of(F,F2,G,p) is random_variable of F,F2;
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
:: FINANCE2:def 5
for w being Element of Omega holds
it.w = ElementsOfPortfolioValueProb_fut(F,G.n).w * phi.n;
end;
theorem :: FINANCE2:30
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 n be Nat holds
RVElementsOfPortfolioValue_fut(phi,F,G,n) is
random_variable of F,Borel_Sets;
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
:: FINANCE2:def 6
for n being Nat holds
it.n = (RVElementsOfPortfolioValue_fut(phi,F,G,n)).w;
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 PortfolioValueFutExt(d,phi,F,G,w) -> Real equals
:: FINANCE2:def 7
Partial_Sums((RVPortfolioValueFutExt_El(phi,F,G,w))).d;
end;