environ
vocabularies HIDDEN, 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 HIDDEN, TARSKI, SUBSET_1, XBOOLE_0, 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;
definitions TARSKI, FINANCE1;
theorems SERIES_1, PROB_3, XXREAL_1, FINANCE1, RANDOM_3, TARSKI, XBOOLE_0, XBOOLE_1, XCMPLX_1, XXREAL_0, PROB_1, NAT_1, FUNCT_2, ORDINAL1, VALUED_1, XREAL_0, FUNCT_1, NUMBERS, SUBSET_1, INT_1, ZFMISC_1, XCMPLX_0, RAT_1;
schemes NAT_1, RECDEF_1, FUNCT_2;
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, REAL_1;
constructors HIDDEN, PROB_3, SERIES_1, FINANCE1, RANDOM_3, REAL_1, RELSET_1, RCOMP_1, SEQ_4, BORSUK_5, LIMFUNC1;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities PROB_1, FINANCE1, SUBSET_1, BORSUK_5, XCMPLX_0, LIMFUNC1;
expansions FUNCT_2, MEMBERED, TARSKI, XBOOLE_0, PROB_1, FINANCE1;
Q00:
ex A1 being SetSequence of REAL st
for n being Nat holds A1 . n = {n}
Q0:
ex A being SetSequence of Borel_Sets st
for n being Nat holds A . n = {n}
H2:
ex A being SetSequence of REAL st
for n being Nat holds A . n = {(- n)}
definition
let p be
Nat;
let Omega,
Omega2 be non
empty set ;
let F be
SigmaField of
Omega;
let F2 be
SigmaField of
Omega2;
let X be
set ;
assume A1:
X = set_of_random_variables_on (
F,
F2)
;
let G be
sequence of
X;
Element_Ofredefine func Element_Of (
F,
F2,
G,
p)
-> random_variable of
F,
F2;
correctness
coherence
Element_Of (F,F2,G,p) is random_variable of F,F2;
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;
existence
ex b1 being Real_Sequence st
for n being Nat holds b1 . n = (RVElementsOfPortfolioValue_fut (phi,F,G,n)) . w
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
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;
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 );
end;
:: Event of the Borel-Sets