:: PROB_4 semantic presentation

A0: for A, B, C being set st C c= B holds
A \ C = (A \ B) \/ (A /\ (B \ C))

proof end;

definition

let X be set ;
let Si be SigmaField of X;
let XSeq be SetSequence of Si;
let n be Nat;
:: original: .
redefine func XSeq . n -> Element of Si;
coherence by PROB_1:def 9;

end;

theorem Th495: :: PROB_4:1

for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds rng XSeq c= Si

proof end;

theorem Th005: :: PROB_4:2

for X being set
for Si being SigmaField of X
for f being Function holds
( f is SetSequence of Si iff f is Function of NAT ,Si )

proof end;

scheme :: PROB_4:sch 1
LambdaSigmaSSeq{ F₁() -> set , F₂() -> SigmaField of F₁(), F₃( set ) -> Element of F₂() } :

ex f being SetSequence of F₂() st
for n being Nat holds f . n = F₃(n)

proof end;

registration

let X be set ;
cluster disjoint_valued Relation of NAT , bool X;
existence

proof end;

end;

registration

let X be set ;
let Si be SigmaField of X;
cluster disjoint_valued SetSequence of Si;
existence

proof end;

end;

theorem Th600: :: PROB_4:3

for X being set
for A, B being Subset of X ex A1 being SetSequence of X st
( A1 . 0 = A & A1 . 1 = B & ( for n being Nat st n > 1 holds
A1 . n = {} ) )

proof end;

theorem Th601: :: PROB_4:4

for X being set
for A1 being SetSequence of X
for A, B being Subset of X st A misses B & A1 . 0 = A & A1 . 1 = B & ( for n being Nat st n > 1 holds
A1 . n = {} ) holds
( A1 is disjoint_valued & Union A1 = A \/ B )

proof end;

theorem Th500: :: PROB_4:5

for X being set
for S being non empty set holds
( S is SigmaField of X iff ( S c= bool X & ( for A1 being SetSequence of X st ( for n being Nat holds A1 . n in S ) holds
Union A1 in S ) & ( for A being Subset of X st A in S holds
A ` in S ) ) )

proof end;

theorem Th700: :: PROB_4:6

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, B being Event of Sigma holds P . (A \ B) = (P . (A \/ B)) - (P . B)

proof end;

theorem Th650: :: PROB_4:7

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A, B being Event of Sigma st A c= B & P . B = 0 holds
P . A = 0

proof end;

theorem Th598: :: PROB_4:8

for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds
( ( for n being Nat holds P . (ASeq . n) = 0 ) iff P . (Union ASeq) = 0 )

proof end;

theorem Th599: :: PROB_4:9

for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds
( ( for A being set st A in rng ASeq holds
P . A = 0 ) iff P . (union (rng ASeq)) = 0 )

proof end;

definition

let X be set ;
let Si be SigmaField of X;
func SF2SFS Si -> sigma_Field_Subset of X equals :: PROB_4:def 1
Si;
coherence by TOPGEN_4:62;

end;

:: deftheorem defines SF2SFS PROB_4:def 1 :

definition

let X be set ;
let MSi be sigma_Field_Subset of X;
func SFS2SF MSi -> SigmaField of X equals :: PROB_4:def 2
MSi;
coherence by TOPGEN_4:62;

end;

:: deftheorem defines SFS2SF PROB_4:def 2 :

theorem Th016: :: PROB_4:10

for seq being Function of NAT , REAL
for Eseq being Function of NAT , ExtREAL st seq = Eseq holds
Partial_Sums seq = Ser Eseq

proof end;

theorem Th017: :: PROB_4:11

for seq being Function of NAT , REAL
for Eseq being Function of NAT , ExtREAL st seq = Eseq & seq is bounded_above holds
sup seq = sup (rng Eseq)

proof end;

theorem Th027: :: PROB_4:12

for seq being Function of NAT , REAL
for Eseq being Function of NAT , ExtREAL st seq = Eseq & seq is bounded_below holds
inf seq = inf (rng Eseq)

proof end;

theorem Th018: :: PROB_4:13

for seq being Function of NAT , REAL
for Eseq being Function of NAT , ExtREAL st seq = Eseq & seq is nonnegative & seq is summable holds
Sum seq = SUM Eseq

proof end;

theorem Th002: :: PROB_4:14

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds P is sigma_Measure of SF2SFS Sigma

proof end;

definition

let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
func P2M P -> sigma_Measure of SF2SFS Sigma equals :: PROB_4:def 3
P;
coherence by Th002;

end;

:: deftheorem defines P2M PROB_4:def 3 :

theorem Th051: :: PROB_4:15

for X being non empty set
for S being sigma_Field_Subset of X
for M being sigma_Measure of S st M . X = R_EAL 1 holds
M is Probability of SFS2SF S

proof end;

definition

let X be non empty set ;
let S be sigma_Field_Subset of X;
let M be sigma_Measure of S;
assume A1: M . X = R_EAL 1 ;
func M2P M -> Probability of SFS2SF S equals :: PROB_4:def 4
M;
coherence by A1, Th051;

end;

:: deftheorem defines M2P PROB_4:def 4 :

Th701: for X being set
for A1 being SetSequence of X st A1 is non-decreasing holds
for n being Nat holds (Partial_Union A1) . n = A1 . n

proof end;

theorem Th702: :: PROB_4:16

for X being set
for A1 being SetSequence of X st A1 is non-decreasing holds
Partial_Union A1 = A1

proof end;

theorem Th703: :: PROB_4:17

for X being set
for A1 being SetSequence of X st A1 is non-decreasing holds
( (Partial_Diff_Union A1) . 0 = A1 . 0 & ( for n being Nat holds (Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ (A1 . n) ) )

proof end;

theorem Th704: :: PROB_4:18

for X being set
for A1 being SetSequence of X st A1 is non-decreasing holds
for n being Nat holds A1 . (n + 1) = ((Partial_Diff_Union A1) . (n + 1)) \/ (A1 . n)

proof end;

theorem Th705: :: PROB_4:19

for X being set
for A1 being SetSequence of X st A1 is non-decreasing holds
for n being Nat holds (Partial_Diff_Union A1) . (n + 1) misses A1 . n

proof end;

theorem :: PROB_4:20

for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si st XSeq is non-decreasing holds
@Partial_Union XSeq = XSeq

proof end;

theorem Th713: :: PROB_4:21

for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si st XSeq is non-decreasing holds
( (@Partial_Diff_Union XSeq) . 0 = XSeq . 0 & ( for n being Nat holds (@Partial_Diff_Union XSeq) . (n + 1) = (XSeq . (n + 1)) \ (XSeq . n) ) )

proof end;

theorem Th715: :: PROB_4:22

for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si st XSeq is non-decreasing holds
for n being Nat holds (@Partial_Diff_Union XSeq) . (n + 1) misses XSeq . n

proof end;

definition

let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
pred P is_complete Sigma means :def112: :: PROB_4:def 5
for A being Subset of Omega
for B being set st B in Sigma & A c= B & P . B = 0 holds
A in Sigma;

end;

:: deftheorem def112 defines is_complete PROB_4:def 5 :

theorem :: PROB_4:23

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds
( P is_complete Sigma iff P2M P is_complete SF2SFS Sigma )

proof end;

definition

let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
mode thin of P -> Subset of Omega means :def113: :: PROB_4:def 6
ex A being set st
( A in Sigma & it c= A & P . A = 0 );
existence

proof end;

end;

:: deftheorem def113 defines thin PROB_4:def 6 :

theorem Th003: :: PROB_4:24

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for Y being Subset of Omega holds
( Y is thin of P iff Y is thin of P2M P )

proof end;

theorem Th1200: :: PROB_4:25

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds {} is thin of P

proof end;

theorem Th122: :: PROB_4:26

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for B1, B2 being set st B1 in Sigma & B2 in Sigma holds
for C1, C2 being thin of P st B1 \/ C1 = B2 \/ C2 holds
P . B1 = P . B2

proof end;

definition

let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
func COM Sigma,P -> non empty Subset-Family of Omega means :def114: :: PROB_4:def 7
for A being set holds
( A in it iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem def114 defines COM PROB_4:def 7 :

theorem Th1202: :: PROB_4:27

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for C being thin of P holds C in COM Sigma,P

proof end;

theorem Th004: :: PROB_4:28

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds COM Sigma,P = COM (SF2SFS Sigma),(P2M P)

proof end;

definition

let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
let A be Element of COM Sigma,P;
func P_COM2M_COM A -> Element of COM (SF2SFS Sigma),(P2M P) equals :: PROB_4:def 8
A;
correctness by Th004;

end;

:: deftheorem defines P_COM2M_COM PROB_4:def 8 :

theorem Th1210: :: PROB_4:29

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds Sigma c= COM Sigma,P

proof end;

definition

let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
let A be Element of COM Sigma,P;
func ProbPart A -> non empty Subset-Family of Omega means :def115: :: PROB_4:def 9
for B being set holds
( B in it iff ( B in Sigma & B c= A & A \ B is thin of P ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem def115 defines ProbPart PROB_4:def 9 :

theorem :: PROB_4:30

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being Element of COM Sigma,P holds ProbPart A = MeasPart (P_COM2M_COM A)

proof end;

theorem :: PROB_4:31

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being Element of COM Sigma,P
for A1, A2 being set st A1 in ProbPart A & A2 in ProbPart A holds
P . A1 = P . A2

proof end;

theorem Th118: :: PROB_4:32

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for F being Function of NAT , COM Sigma,P ex BSeq being SetSequence of Sigma st
for n being Nat holds BSeq . n in ProbPart (F . n)

proof end;

theorem Th119: :: PROB_4:33

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for F being Function of NAT , COM Sigma,P
for BSeq being SetSequence of Sigma ex CSeq being SetSequence of Omega st
for n being Nat holds CSeq . n = (F . n) \ (BSeq . n)

proof end;

theorem Th120: :: PROB_4:34

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for BSeq being SetSequence of Omega st ( for n being Nat holds BSeq . n is thin of P ) holds
ex CSeq being SetSequence of Sigma st
for n being Nat holds
( BSeq . n c= CSeq . n & P . (CSeq . n) = 0 )

proof end;

theorem Th121: :: PROB_4:35

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for D being non empty Subset-Family of Omega st ( for A being set holds
( A in D iff ex B being set st
( B in Sigma & ex C being thin of P st A = B \/ C ) ) ) holds
D is SigmaField of Omega

proof end;

definition

let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
:: original: COM
redefine func COM Sigma,P -> SigmaField of Omega;
coherence

proof end;

end;

definition

let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
:: original: thin
redefine mode thin of P -> Event of COM Sigma,P;
coherence

proof end;

end;

theorem Th1211: :: PROB_4:36

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being set holds
( A in COM Sigma,P iff ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) )

proof end;

theorem :: PROB_4:37

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for C being non empty Subset-Family of Omega st ( for A being set holds
( A in C iff ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) ) ) holds
C = COM Sigma,P

proof end;

definition

let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let P be Probability of Sigma;
func COM P -> Probability of COM Sigma,P means :def116: :: PROB_4:def 10
for B being set st B in Sigma holds
for C being thin of P holds it . (B \/ C) = P . B;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem def116 defines COM PROB_4:def 10 :

theorem :: PROB_4:38

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds COM P = COM (P2M P)

proof end;

theorem :: PROB_4:39

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma holds COM P is_complete COM Sigma,P

proof end;

theorem Th124: :: PROB_4:40

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being Event of Sigma holds P . A = (COM P) . A

proof end;

theorem Th1240: :: PROB_4:41

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for C being thin of P holds (COM P) . C = 0

proof end;

theorem :: PROB_4:42

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being Element of COM Sigma,P
for B being set st B in ProbPart A holds
P . B = (COM P) . A

proof end;