environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, PROB_1, MEASURE1, PARTFUN1, SUBSET_1, TARSKI, RELAT_1, FUNCT_1, ARYTM_3, XXREAL_0, XXREAL_1, LOPBAN_1, FUNCT_2, DIST_1, MSSUBFAM, VALUED_0, MESFUNC1, SUPINF_2, FINSEQ_1, NAT_1, CARD_3, CARD_1, ZFMISC_1, RPR_1, FINSET_1, PROB_4, EQREL_1, RANDOM_1, RANDOM_2, RANDOM_3, FUNCOP_1, FINANCE1, PBOOLE, REAL_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, PBOOLE, ENUMSET1, FINSET_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XXREAL_1, NAT_1, XREAL_0, VALUED_0, FINSEQ_1, RPR_1, SUPINF_2, PROB_1, PROB_2, MEASURE1, MEASURE6, MESFUNC1, PROB_4, MESFUNC6, RANDOM_1, DIST_1, RANDOM_2, FINANCE1;
definitions TARSKI, XBOOLE_0, FINSET_1;
theorems TARSKI, PARTFUN1, FUNCT_1, MESFUNC1, FINSEQ_1, XBOOLE_0, XBOOLE_1, PROB_2, XXREAL_0, PROB_1, RELAT_1, ZFMISC_1, FUNCT_2, MEASURE1, PROB_4, MESFUNC6, MEASURE6, ORDINAL1, VALUED_0, RCOMP_1, FUNCOP_1, RANDOM_1, FINANCE1;
schemes FUNCT_1, FUNCT_2, NAT_1, RECDEF_1;
registrations XBOOLE_0, SUBSET_1, NAT_1, XREAL_0, XXREAL_0, ORDINAL1, MEASURE1, FUNCOP_1, FINANCE1, VALUED_0, FINSEQ_1, FUNCT_2, RELAT_1, PROB_2, FINSET_1, NUMBERS, PROB_1, PARTFUN1, RELSET_1, CARD_1, PBOOLE, PRE_CIRC;
constructors HIDDEN, REAL_1, RPR_1, MESFUNC6, MESFUNC3, DIST_1, MEASURE6, INTEGRA2, PROB_4, MESFUNC1, RELSET_1, COMSEQ_2, RANDOM_2, FINANCE1, ENUMSET1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities RPR_1, SUBSET_1, RANDOM_2, PROB_4, PROB_1, RELAT_1, DIST_1, FINANCE1, CARD_3;
expansions TARSKI, XBOOLE_0, RELAT_1, FINANCE1;
Lm1:
for X, Y being non empty set
for S being SigmaField of Y
for M being Probability of S holds X --> M is S -Probability_valued
Lm2:
for Omega1, Omega2 being non empty set
for S1 being SigmaField of Omega1
for S2 being SigmaField of Omega2
for M being Measure of S1
for F being random_variable of S1,S2 ex N being Measure of S2 st
for y being Element of S2 holds N . y = M . (F " y)
definition
let D be
non-empty V26()
ManySortedSet of
NAT ;
let P be
Probability_sequence of
Trivial-SigmaField_sequence D;
existence
ex b1 being ManySortedSet of NAT st
( b1 . 0 = P . 0 & ( for i being Nat holds b1 . (i + 1) = Product-Probability (((Product_dom D) . i),(D . (i + 1)),(modetrans ((b1 . i),(Trivial-SigmaField ((Product_dom D) . i)))),(P . (i + 1))) ) )
uniqueness
for b1, b2 being ManySortedSet of NAT st b1 . 0 = P . 0 & ( for i being Nat holds b1 . (i + 1) = Product-Probability (((Product_dom D) . i),(D . (i + 1)),(modetrans ((b1 . i),(Trivial-SigmaField ((Product_dom D) . i)))),(P . (i + 1))) ) & b2 . 0 = P . 0 & ( for i being Nat holds b2 . (i + 1) = Product-Probability (((Product_dom D) . i),(D . (i + 1)),(modetrans ((b2 . i),(Trivial-SigmaField ((Product_dom D) . i)))),(P . (i + 1))) ) holds
b1 = b2
end;
theorem
for
D being
non-empty V26()
ManySortedSet of
NAT for
P being
Probability_sequence of
Trivial-SigmaField_sequence D holds
(
(Product-Probability (P,D)) . 0 = P . 0 &
(Product-Probability (P,D)) . 1
= Product-Probability (
(D . 0),
(D . 1),
(P . 0),
(P . 1)) & ex
P1 being
Probability of
Trivial-SigmaField [:(D . 0),(D . 1):] st
(
P1 = (Product-Probability (P,D)) . 1 &
(Product-Probability (P,D)) . 2
= Product-Probability (
[:(D . 0),(D . 1):],
(D . 2),
P1,
(P . 2)) ) & ex
P2 being
Probability of
Trivial-SigmaField [:(D . 0),(D . 1),(D . 2):] st
(
P2 = (Product-Probability (P,D)) . 2 &
(Product-Probability (P,D)) . 3
= Product-Probability (
[:(D . 0),(D . 1),(D . 2):],
(D . 3),
P2,
(P . 3)) ) & ex
P3 being
Probability of
Trivial-SigmaField [:(D . 0),(D . 1),(D . 2),(D . 3):] st
(
P3 = (Product-Probability (P,D)) . 3 &
(Product-Probability (P,D)) . 4
= Product-Probability (
[:(D . 0),(D . 1),(D . 2),(D . 3):],
(D . 4),
P3,
(P . 4)) ) )