:: 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;