Loading [MathJax]/jax/output/HTML-CSS/config.js
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
by FUNCOP_1:7;
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)) ) )