:: PROB_4 semantic presentation begin Lm1: for A, B, C being set st C c= B holds A \ C = (A \ B) \/ (A /\ (B \ C)) proof let A, B, C be set ; ::_thesis: ( C c= B implies A \ C = (A \ B) \/ (A /\ (B \ C)) ) assume A1: C c= B ; ::_thesis: A \ C = (A \ B) \/ (A /\ (B \ C)) thus A \ C c= (A \ B) \/ (A /\ (B \ C)) :: according to XBOOLE_0:def_10 ::_thesis: (A \ B) \/ (A /\ (B \ C)) c= A \ C proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A \ C or x in (A \ B) \/ (A /\ (B \ C)) ) assume x in A \ C ; ::_thesis: x in (A \ B) \/ (A /\ (B \ C)) then ( ( x in A & not x in B ) or ( x in A & x in B & not x in C ) ) by XBOOLE_0:def_5; then ( x in A \ B or ( x in A & x in B \ C ) ) by XBOOLE_0:def_5; then ( x in A \ B or x in A /\ (B \ C) ) by XBOOLE_0:def_4; hence x in (A \ B) \/ (A /\ (B \ C)) by XBOOLE_0:def_3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A \ B) \/ (A /\ (B \ C)) or x in A \ C ) assume x in (A \ B) \/ (A /\ (B \ C)) ; ::_thesis: x in A \ C then ( x in A \ B or x in A /\ (B \ C) ) by XBOOLE_0:def_3; then A2: ( x in A \ B or ( x in A & x in B \ C ) ) by XBOOLE_0:def_4; then not x in C by A1, XBOOLE_0:def_5; hence x in A \ C by A2, XBOOLE_0:def_5; ::_thesis: verum end; definition let X be set ; let Si be SigmaField of X; let XSeq be SetSequence of Si; let n be Element of NAT ; :: original: . redefine funcXSeq . n -> Element of Si; coherence XSeq . n is Element of Si proof thus XSeq . n is Element of Si ; ::_thesis: verum end; end; theorem Th1: :: 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 let X be set ; ::_thesis: for Si being SigmaField of X for XSeq being SetSequence of Si holds rng XSeq c= Si let Si be SigmaField of X; ::_thesis: for XSeq being SetSequence of Si holds rng XSeq c= Si let XSeq be SetSequence of Si; ::_thesis: rng XSeq c= Si let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng XSeq or x in Si ) assume x in rng XSeq ; ::_thesis: x in Si then ex n being Element of NAT st x = XSeq . n by SETLIM_1:4; hence x in Si ; ::_thesis: verum end; theorem Th2: :: 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 let X be set ; ::_thesis: for Si being SigmaField of X for f being Function holds ( f is SetSequence of Si iff f is Function of NAT,Si ) let Si be SigmaField of X; ::_thesis: for f being Function holds ( f is SetSequence of Si iff f is Function of NAT,Si ) let f be Function; ::_thesis: ( f is SetSequence of Si iff f is Function of NAT,Si ) thus ( f is SetSequence of Si implies f is Function of NAT,Si ) ::_thesis: ( f is Function of NAT,Si implies f is SetSequence of Si ) proof assume f is SetSequence of Si ; ::_thesis: f is Function of NAT,Si then reconsider f = f as SetSequence of Si ; ( rng f c= Si & dom f = NAT ) by Th1, FUNCT_2:def_1; hence f is Function of NAT,Si by FUNCT_2:2; ::_thesis: verum end; assume A1: f is Function of NAT,Si ; ::_thesis: f is SetSequence of Si then reconsider f = f as SetSequence of X by FUNCT_2:7; f is SetSequence of Si by A1; hence f is SetSequence of Si ; ::_thesis: verum end; scheme :: PROB_4:sch 1 LambdaSigmaSSeq{ F1() -> set , F2() -> SigmaField of F1(), F3( set ) -> Element of F2() } : ex f being SetSequence of F2() st for n being Element of NAT holds f . n = F3(n) proof ex f being SetSequence of F1() st for n being Element of NAT holds f . n = F3(n) from FUNCT_2:sch_4(); then consider f being SetSequence of F1() such that A1: for n being Element of NAT holds f . n = F3(n) ; for n being Nat holds f . n in F2() proof let n be Nat; ::_thesis: f . n in F2() n in NAT by ORDINAL1:def_12; then f . n = F3(n) by A1; hence f . n in F2() ; ::_thesis: verum end; then rng f c= F2() by NAT_1:52; then reconsider f = f as SetSequence of F2() by RELAT_1:def_19; take f ; ::_thesis: for n being Element of NAT holds f . n = F3(n) thus for n being Element of NAT holds f . n = F3(n) by A1; ::_thesis: verum end; registration let X be set ; cluster non empty V13() V16( NAT ) V17( bool X) Function-like V23( NAT ) V27( NAT , bool X) V118() for Element of bool [:NAT,(bool X):]; existence not for b1 being SetSequence of X holds b1 is V118() proof take A1 = NAT --> ({} X); ::_thesis: A1 is V118() for m, n being Nat st m <> n holds A1 . m misses A1 . n proof let m, n be Nat; ::_thesis: ( m <> n implies A1 . m misses A1 . n ) m in NAT by ORDINAL1:def_12; then A1 . m = {} by FUNCOP_1:7; hence ( m <> n implies A1 . m misses A1 . n ) by XBOOLE_1:65; ::_thesis: verum end; hence A1 is V118() by PROB_3:def_4; ::_thesis: verum end; end; registration let X be set ; let Si be SigmaField of X; cluster non empty V13() V16( NAT ) V17(Si) V17( bool X) Function-like V23( NAT ) V27( NAT , bool X) V118() for Element of bool [:NAT,(bool X):]; existence not for b1 being SetSequence of Si holds b1 is V118() proof reconsider MSi = Si as SigmaField of X ; set f = the disjoint_valued Function of NAT,MSi; reconsider f = the disjoint_valued Function of NAT,MSi as SetSequence of Si by Th2; take f ; ::_thesis: f is V118() thus f is V118() ; ::_thesis: verum end; end; theorem Th3: :: PROB_4:3 for X being set for A, B being Subset of X st A misses B holds (A,B) followed_by {} is disjoint_valued proof let X be set ; ::_thesis: for A, B being Subset of X st A misses B holds (A,B) followed_by {} is disjoint_valued let A, B be Subset of X; ::_thesis: ( A misses B implies (A,B) followed_by {} is disjoint_valued ) reconsider A1 = (A,B) followed_by ({} X) as SetSequence of X ; assume A1: A misses B ; ::_thesis: (A,B) followed_by {} is disjoint_valued A1 is V118() proof A2: A1 . 1 = B by FUNCT_7:123; let m, n be Nat; :: according to PROB_3:def_4 ::_thesis: ( m = n or A1 . m misses A1 . n ) assume A3: m <> n ; ::_thesis: A1 . m misses A1 . n A4: A1 . 0 = A by FUNCT_7:122; percases ( m = 0 or ( m <> 0 & m = 1 ) or ( m <> 0 & m <> 1 ) ) ; supposeA5: m = 0 ; ::_thesis: A1 . m misses A1 . n then n >= 1 by A3, NAT_1:14; then A6: n + 1 > 1 by NAT_1:13; percases ( n > 1 or n = 1 ) by A6, NAT_1:22; suppose n > 1 ; ::_thesis: A1 . m misses A1 . n then A1 . n = {} by FUNCT_7:124; hence A1 . m misses A1 . n by XBOOLE_1:65; ::_thesis: verum end; suppose n = 1 ; ::_thesis: A1 . m misses A1 . n hence A1 . m misses A1 . n by A1, A4, A5, FUNCT_7:123; ::_thesis: verum end; end; end; supposeA7: ( m <> 0 & m = 1 ) ; ::_thesis: A1 . m misses A1 . n ( n >= 1 or n <= 1 ) ; then A8: ( n + 1 > 1 or n < 1 + 1 ) by NAT_1:13; percases ( n > 1 or n = 0 ) by A3, A7, A8, NAT_1:14, NAT_1:22; suppose n > 1 ; ::_thesis: A1 . m misses A1 . n then A1 . n = {} by FUNCT_7:124; hence A1 . m misses A1 . n by XBOOLE_1:65; ::_thesis: verum end; suppose n = 0 ; ::_thesis: A1 . m misses A1 . n hence A1 . m misses A1 . n by A1, A4, A2, A7; ::_thesis: verum end; end; end; supposeA9: ( m <> 0 & m <> 1 ) ; ::_thesis: A1 . m misses A1 . n then m >= 1 by NAT_1:14; then m + 1 > 1 by NAT_1:13; then A1 . m = {} by A9, FUNCT_7:124, NAT_1:22; hence A1 . m misses A1 . n by XBOOLE_1:65; ::_thesis: verum end; end; end; hence (A,B) followed_by {} is disjoint_valued ; ::_thesis: verum end; theorem Th4: :: PROB_4:4 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 rng A1 c= S holds Union A1 in S ) & ( for A being Subset of X st A in S holds A ` in S ) ) ) proof let X be set ; ::_thesis: for S being non empty set holds ( S is SigmaField of X iff ( S c= bool X & ( for A1 being SetSequence of X st rng A1 c= S holds Union A1 in S ) & ( for A being Subset of X st A in S holds A ` in S ) ) ) let S be non empty set ; ::_thesis: ( S is SigmaField of X iff ( S c= bool X & ( for A1 being SetSequence of X st rng A1 c= S holds Union A1 in S ) & ( for A being Subset of X st A in S holds A ` in S ) ) ) thus ( S is SigmaField of X implies ( S c= bool X & ( for A1 being SetSequence of X st rng A1 c= S holds Union A1 in S ) & ( for A being Subset of X st A in S holds A ` in S ) ) ) ::_thesis: ( S c= bool X & ( for A1 being SetSequence of X st rng A1 c= S holds Union A1 in S ) & ( for A being Subset of X st A in S holds A ` in S ) implies S is SigmaField of X ) proof assume S is SigmaField of X ; ::_thesis: ( S c= bool X & ( for A1 being SetSequence of X st rng A1 c= S holds Union A1 in S ) & ( for A being Subset of X st A in S holds A ` in S ) ) then reconsider S = S as SigmaField of X ; for A1 being SetSequence of X st rng A1 c= S holds Union A1 in S proof let A1 be SetSequence of X; ::_thesis: ( rng A1 c= S implies Union A1 in S ) assume rng A1 c= S ; ::_thesis: Union A1 in S then reconsider A1 = A1 as SetSequence of S by RELAT_1:def_19; Union A1 in S by PROB_1:17; hence Union A1 in S ; ::_thesis: verum end; hence ( S c= bool X & ( for A1 being SetSequence of X st rng A1 c= S holds Union A1 in S ) & ( for A being Subset of X st A in S holds A ` in S ) ) by PROB_1:15; ::_thesis: verum end; assume that A1: S c= bool X and A2: for A1 being SetSequence of X st rng A1 c= S holds Union A1 in S and A3: for A being Subset of X st A in S holds A ` in S ; ::_thesis: S is SigmaField of X for A1 being SetSequence of X st rng A1 c= S holds Intersection A1 in S proof let A1 be SetSequence of X; ::_thesis: ( rng A1 c= S implies Intersection A1 in S ) assume A4: rng A1 c= S ; ::_thesis: Intersection A1 in S for n being Nat holds (Complement A1) . n in S proof let n be Nat; ::_thesis: (Complement A1) . n in S reconsider n1 = n as Element of NAT by ORDINAL1:def_12; A1 . n in rng A1 by NAT_1:51; then (A1 . n1) ` in S by A3, A4; hence (Complement A1) . n in S by PROB_1:def_2; ::_thesis: verum end; then rng (Complement A1) c= S by NAT_1:52; then (Union (Complement A1)) ` in S by A2, A3; hence Intersection A1 in S by PROB_1:def_3; ::_thesis: verum end; hence S is SigmaField of X by A1, A3, PROB_1:15; ::_thesis: verum end; theorem Th5: :: PROB_4:5 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 let Omega be non empty set ; ::_thesis: 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) let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma for A, B being Event of Sigma holds P . (A \ B) = (P . (A \/ B)) - (P . B) let P be Probability of Sigma; ::_thesis: for A, B being Event of Sigma holds P . (A \ B) = (P . (A \/ B)) - (P . B) let A, B be Event of Sigma; ::_thesis: P . (A \ B) = (P . (A \/ B)) - (P . B) (P . (A \/ B)) - (P . B) = ((P . B) + (P . (A \ B))) - (P . B) by PROB_1:36; hence P . (A \ B) = (P . (A \/ B)) - (P . B) ; ::_thesis: verum end; theorem Th6: :: 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 st A c= B & P . B = 0 holds P . A = 0 proof let Omega be non empty set ; ::_thesis: 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 let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma for A, B being Event of Sigma st A c= B & P . B = 0 holds P . A = 0 let P be Probability of Sigma; ::_thesis: for A, B being Event of Sigma st A c= B & P . B = 0 holds P . A = 0 let A, B be Event of Sigma; ::_thesis: ( A c= B & P . B = 0 implies P . A = 0 ) assume ( A c= B & P . B = 0 ) ; ::_thesis: P . A = 0 then P . A <= 0 by PROB_1:34; hence P . A = 0 by PROB_1:def_8; ::_thesis: verum end; theorem Th7: :: PROB_4:7 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 Element of NAT holds P . (ASeq . n) = 0 ) iff P . (Union ASeq) = 0 ) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for ASeq being SetSequence of Sigma for P being Probability of Sigma holds ( ( for n being Element of NAT holds P . (ASeq . n) = 0 ) iff P . (Union ASeq) = 0 ) let Sigma be SigmaField of Omega; ::_thesis: for ASeq being SetSequence of Sigma for P being Probability of Sigma holds ( ( for n being Element of NAT holds P . (ASeq . n) = 0 ) iff P . (Union ASeq) = 0 ) let ASeq be SetSequence of Sigma; ::_thesis: for P being Probability of Sigma holds ( ( for n being Element of NAT holds P . (ASeq . n) = 0 ) iff P . (Union ASeq) = 0 ) let P be Probability of Sigma; ::_thesis: ( ( for n being Element of NAT holds P . (ASeq . n) = 0 ) iff P . (Union ASeq) = 0 ) hereby ::_thesis: ( P . (Union ASeq) = 0 implies for n being Element of NAT holds P . (ASeq . n) = 0 ) assume A1: for n being Element of NAT holds P . (ASeq . n) = 0 ; ::_thesis: P . (Union ASeq) = 0 for n being Element of NAT holds (Partial_Sums (P * ASeq)) . n = 0 proof defpred S1[ Element of NAT ] means (Partial_Sums (P * ASeq)) . \$1 = 0 ; A2: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: S1[k] ; ::_thesis: S1[k + 1] thus (Partial_Sums (P * ASeq)) . (k + 1) = ((Partial_Sums (P * ASeq)) . k) + ((P * ASeq) . (k + 1)) by SERIES_1:def_1 .= 0 + (P . (ASeq . (k + 1))) by A3, FUNCT_2:15 .= 0 by A1 ; ::_thesis: verum end; (Partial_Sums (P * ASeq)) . 0 = (P * ASeq) . 0 by SERIES_1:def_1 .= P . (ASeq . 0) by FUNCT_2:15 .= 0 by A1 ; then A4: S1[ 0 ] ; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A2); ::_thesis: verum end; then for n being Element of NAT st 0 <= n holds (Partial_Sums (P * ASeq)) . n = 0 ; then A5: ( Partial_Sums (P * ASeq) is convergent & lim (Partial_Sums (P * ASeq)) = 0 ) by PROB_1:1; now__::_thesis:_for_n_being_Element_of_NAT_holds_(P_*_(Partial_Diff_Union_ASeq))_._n_<=_(P_*_ASeq)_._n let n be Element of NAT ; ::_thesis: (P * (Partial_Diff_Union ASeq)) . n <= (P * ASeq) . n (Partial_Diff_Union ASeq) . n c= ASeq . n by PROB_3:33; hence (P * (Partial_Diff_Union ASeq)) . n <= (P * ASeq) . n by PROB_3:5; ::_thesis: verum end; then A6: for n being Element of NAT holds (Partial_Sums (P * (Partial_Diff_Union ASeq))) . n <= (Partial_Sums (P * ASeq)) . n by SERIES_1:14; Partial_Sums (P * (Partial_Diff_Union ASeq)) is convergent by PROB_3:45; then Sum (P * (Partial_Diff_Union ASeq)) <= 0 by A5, A6, SEQ_2:18; then P . (Union (Partial_Diff_Union ASeq)) <= 0 by PROB_3:46; then A7: P . (Union ASeq) <= 0 by PROB_3:36; Union ASeq is Event of Sigma by PROB_1:26; hence P . (Union ASeq) = 0 by A7, PROB_1:def_8; ::_thesis: verum end; assume A8: P . (Union ASeq) = 0 ; ::_thesis: for n being Element of NAT holds P . (ASeq . n) = 0 hereby ::_thesis: verum reconsider Y2 = Union ASeq as Event of Sigma by PROB_1:26; let n be Element of NAT ; ::_thesis: P . (ASeq . n) = 0 reconsider Y1 = ASeq . n as Event of Sigma ; ASeq . n in rng ASeq by SETLIM_1:4; then ASeq . n c= union (rng ASeq) by ZFMISC_1:74; then Y1 c= Y2 by CARD_3:def_4; hence P . (ASeq . n) = 0 by A8, Th6; ::_thesis: verum end; end; theorem Th8: :: 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 A being set st A in rng ASeq holds P . A = 0 ) iff P . (union (rng ASeq)) = 0 ) proof let Omega be non empty set ; ::_thesis: 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 ) let Sigma be SigmaField of Omega; ::_thesis: 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 ) let ASeq be SetSequence of Sigma; ::_thesis: 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 ) let P be Probability of Sigma; ::_thesis: ( ( for A being set st A in rng ASeq holds P . A = 0 ) iff P . (union (rng ASeq)) = 0 ) hereby ::_thesis: ( P . (union (rng ASeq)) = 0 implies for A being set st A in rng ASeq holds P . A = 0 ) assume A1: for A being set st A in rng ASeq holds P . A = 0 ; ::_thesis: P . (union (rng ASeq)) = 0 for n being Element of NAT holds P . (ASeq . n) = 0 proof let n be Element of NAT ; ::_thesis: P . (ASeq . n) = 0 ASeq . n in rng ASeq by SETLIM_1:4; hence P . (ASeq . n) = 0 by A1; ::_thesis: verum end; then P . (Union ASeq) = 0 by Th7; hence P . (union (rng ASeq)) = 0 by CARD_3:def_4; ::_thesis: verum end; assume P . (union (rng ASeq)) = 0 ; ::_thesis: for A being set st A in rng ASeq holds P . A = 0 then A2: P . (Union ASeq) = 0 by CARD_3:def_4; hereby ::_thesis: verum let A be set ; ::_thesis: ( A in rng ASeq implies P . A = 0 ) assume A in rng ASeq ; ::_thesis: P . A = 0 then ex n1 being Element of NAT st A = ASeq . n1 by SETLIM_1:4; hence P . A = 0 by A2, Th7; ::_thesis: verum end; end; theorem Th9: :: PROB_4:9 for seq being Function of NAT,REAL for Eseq being Function of NAT,ExtREAL st seq = Eseq holds Partial_Sums seq = Ser Eseq proof let seq be Function of NAT,REAL; ::_thesis: for Eseq being Function of NAT,ExtREAL st seq = Eseq holds Partial_Sums seq = Ser Eseq let Eseq be Function of NAT,ExtREAL; ::_thesis: ( seq = Eseq implies Partial_Sums seq = Ser Eseq ) assume A1: seq = Eseq ; ::_thesis: Partial_Sums seq = Ser Eseq reconsider Ps = Partial_Sums seq as Function of NAT,ExtREAL by FUNCT_2:7, NUMBERS:31; defpred S1[ Element of NAT ] means Ps . \$1 = (Ser Eseq) . \$1; A2: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: Ps . k = (Ser Eseq) . k ; ::_thesis: S1[k + 1] Ps . k = (Partial_Sums seq) . k ; then reconsider Psk = Ps . k as Real ; ( Ps . (k + 1) = Psk + (seq . (k + 1)) & (Ser Eseq) . (k + 1) = ((Ser Eseq) . k) + (Eseq . (k + 1)) ) by SERIES_1:def_1, SUPINF_2:44; hence S1[k + 1] by A1, A3, SUPINF_2:1; ::_thesis: verum end; Ps . 0 = Eseq . 0 by A1, SERIES_1:def_1 .= (Ser Eseq) . 0 by SUPINF_2:44 ; then A4: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A2); hence Partial_Sums seq = Ser Eseq by FUNCT_2:63; ::_thesis: verum end; theorem Th10: :: PROB_4:10 for seq being Function of NAT,REAL for Eseq being Function of NAT,ExtREAL st seq = Eseq & seq is V101() holds upper_bound seq = sup (rng Eseq) proof let seq be Function of NAT,REAL; ::_thesis: for Eseq being Function of NAT,ExtREAL st seq = Eseq & seq is V101() holds upper_bound seq = sup (rng Eseq) let Eseq be Function of NAT,ExtREAL; ::_thesis: ( seq = Eseq & seq is V101() implies upper_bound seq = sup (rng Eseq) ) assume that A1: seq = Eseq and A2: seq is V101() ; ::_thesis: upper_bound seq = sup (rng Eseq) reconsider s = upper_bound seq as R_eal by XXREAL_0:def_1; A3: dom Eseq = NAT by FUNCT_2:def_1; A4: rng Eseq <> {-infty} proof assume rng Eseq = {-infty} ; ::_thesis: contradiction then reconsider k1 = -infty as Element of rng Eseq by TARSKI:def_1; consider n1 being set such that A5: n1 in NAT and Eseq . n1 = k1 by A3, FUNCT_1:def_3; reconsider n1 = n1 as Element of NAT by A5; seq . n1 = k1 by A1; hence contradiction ; ::_thesis: verum end; for x being ext-real number st x in rng Eseq holds x <= s proof let x be ext-real number ; ::_thesis: ( x in rng Eseq implies x <= s ) assume x in rng Eseq ; ::_thesis: x <= s then ex n1 being set st ( n1 in NAT & Eseq . n1 = x ) by A3, FUNCT_1:def_3; hence x <= s by A1, A2, RINFSUP1:7; ::_thesis: verum end; then A6: s is UpperBound of rng Eseq by XXREAL_2:def_1; then A7: rng Eseq is bounded_above by XXREAL_2:def_10; A8: s <= sup (rng Eseq) proof reconsider r1 = sup (rng Eseq) as Real by A7, A4, XXREAL_2:57; sup (rng Eseq) is UpperBound of rng Eseq by XXREAL_2:def_3; then for n being Element of NAT holds seq . n <= r1 by A1, A3, FUNCT_1:3, XXREAL_2:def_1; hence s <= sup (rng Eseq) by RINFSUP1:9; ::_thesis: verum end; sup (rng Eseq) <= s by A6, XXREAL_2:def_3; hence upper_bound seq = sup (rng Eseq) by A8, XXREAL_0:1; ::_thesis: verum end; theorem Th11: :: PROB_4:11 for seq being Function of NAT,REAL for Eseq being Function of NAT,ExtREAL st seq = Eseq & seq is V102() holds lower_bound seq = inf (rng Eseq) proof let seq be Function of NAT,REAL; ::_thesis: for Eseq being Function of NAT,ExtREAL st seq = Eseq & seq is V102() holds lower_bound seq = inf (rng Eseq) let Eseq be Function of NAT,ExtREAL; ::_thesis: ( seq = Eseq & seq is V102() implies lower_bound seq = inf (rng Eseq) ) assume that A1: seq = Eseq and A2: seq is V102() ; ::_thesis: lower_bound seq = inf (rng Eseq) reconsider s = lower_bound seq as R_eal by XXREAL_0:def_1; A3: dom Eseq = NAT by FUNCT_2:def_1; A4: rng Eseq <> {+infty} proof assume rng Eseq = {+infty} ; ::_thesis: contradiction then reconsider k1 = +infty as Element of rng Eseq by TARSKI:def_1; consider n1 being set such that A5: n1 in NAT and Eseq . n1 = k1 by A3, FUNCT_1:def_3; reconsider n1 = n1 as Element of NAT by A5; seq . n1 = k1 by A1; hence contradiction ; ::_thesis: verum end; for x being ext-real number st x in rng Eseq holds s <= x proof let x be ext-real number ; ::_thesis: ( x in rng Eseq implies s <= x ) assume x in rng Eseq ; ::_thesis: s <= x then ex n1 being set st ( n1 in NAT & Eseq . n1 = x ) by A3, FUNCT_1:def_3; hence s <= x by A1, A2, RINFSUP1:8; ::_thesis: verum end; then A6: s is LowerBound of rng Eseq by XXREAL_2:def_2; then A7: rng Eseq is bounded_below by XXREAL_2:def_9; A8: inf (rng Eseq) <= s proof reconsider r1 = inf (rng Eseq) as Real by A7, A4, XXREAL_2:58; inf (rng Eseq) is LowerBound of rng Eseq by XXREAL_2:def_4; then for n being Element of NAT holds r1 <= seq . n by A1, A3, FUNCT_1:3, XXREAL_2:def_2; hence inf (rng Eseq) <= s by RINFSUP1:10; ::_thesis: verum end; s <= inf (rng Eseq) by A6, XXREAL_2:def_4; hence lower_bound seq = inf (rng Eseq) by A8, XXREAL_0:1; ::_thesis: verum end; theorem Th12: :: PROB_4:12 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 let seq be Function of NAT,REAL; ::_thesis: for Eseq being Function of NAT,ExtREAL st seq = Eseq & seq is nonnegative & seq is summable holds Sum seq = SUM Eseq let Eseq be Function of NAT,ExtREAL; ::_thesis: ( seq = Eseq & seq is nonnegative & seq is summable implies Sum seq = SUM Eseq ) assume that A1: seq = Eseq and A2: ( seq is nonnegative & seq is summable ) ; ::_thesis: Sum seq = SUM Eseq A3: for n being Element of NAT holds seq . n >= 0 by A2, RINFSUP1:def_3; Partial_Sums seq is convergent by A2, SERIES_1:def_2; then A4: Partial_Sums seq is bounded ; then upper_bound (Partial_Sums seq) = sup (rng (Ser Eseq)) by A1, Th9, Th10; then upper_bound (Partial_Sums seq) = SUM Eseq by SUPINF_2:def_17; hence Sum seq = SUM Eseq by A4, A3, RINFSUP1:24, SERIES_1:16; ::_thesis: verum end; theorem Th13: :: PROB_4:13 for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma holds P is sigma_Measure of Sigma proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for P being Probability of Sigma holds P is sigma_Measure of Sigma let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma holds P is sigma_Measure of Sigma let P be Probability of Sigma; ::_thesis: P is sigma_Measure of Sigma set Z = Sigma; reconsider P1 = P as Function of Sigma,ExtREAL by FUNCT_2:7, NUMBERS:31; for x being R_eal st x in rng P1 holds 0. <= x proof let x be R_eal; ::_thesis: ( x in rng P1 implies 0. <= x ) assume A1: x in rng P1 ; ::_thesis: 0. <= x dom P1 = Sigma by FUNCT_2:def_1; then consider y being set such that A2: y in Sigma and A3: P1 . y = x by A1, FUNCT_1:def_3; reconsider y1 = y as Event of Sigma by A2; 0 <= P . y1 by PROB_1:def_8; hence 0. <= x by A3; ::_thesis: verum end; then A4: rng P1 is nonnegative by SUPINF_2:def_9; for F being Sep_Sequence of Sigma holds SUM (P1 * F) = P1 . (union (rng F)) proof let F be Sep_Sequence of Sigma; ::_thesis: SUM (P1 * F) = P1 . (union (rng F)) reconsider F2 = F as V118() SetSequence of Sigma by Th2; for n being Element of NAT holds (P * F2) . n >= 0 by PROB_3:4; then A5: P * F2 is nonnegative by RINFSUP1:def_3; Partial_Sums (P * F2) is convergent by PROB_3:45; then P * F2 is summable by SERIES_1:def_2; then ( P . (Union F2) = Sum (P * F2) & Sum (P * F2) = SUM (P1 * F) ) by A5, Th12, PROB_3:46; hence SUM (P1 * F) = P1 . (union (rng F)) by CARD_3:def_4; ::_thesis: verum end; hence P is sigma_Measure of Sigma by A4, MEASURE1:def_6, SUPINF_2:def_16; ::_thesis: verum 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 Sigma equals :: PROB_4:def 1 P; coherence P is sigma_Measure of Sigma by Th13; end; :: deftheorem defines P2M PROB_4:def_1_:_ for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma holds P2M P = P; theorem Th14: :: PROB_4:14 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S st M . X = R_EAL 1 holds M is Probability of S proof let X be non empty set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S st M . X = R_EAL 1 holds M is Probability of S let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S st M . X = R_EAL 1 holds M is Probability of S let M be sigma_Measure of S; ::_thesis: ( M . X = R_EAL 1 implies M is Probability of S ) assume A1: M . X = R_EAL 1 ; ::_thesis: M is Probability of S A2: for A being Element of S holds M . A <= R_EAL 1 proof reconsider X = X as Element of S by PROB_1:5; let A be Element of S; ::_thesis: M . A <= R_EAL 1 M . A <= M . X by MEASURE1:31; hence M . A <= R_EAL 1 by A1; ::_thesis: verum end; A3: for x being set st x in S holds M . x in REAL proof let x be set ; ::_thesis: ( x in S implies M . x in REAL ) assume x in S ; ::_thesis: M . x in REAL then reconsider x = x as Element of S ; A4: ( R_EAL 1 is Real & 0 is Real ) by MEASURE6:def_1; ( 0. <= M . x & M . x <= R_EAL 1 ) by A2, MEASURE1:def_2; hence M . x in REAL by A4, XXREAL_0:45; ::_thesis: verum end; dom M = S by FUNCT_2:def_1; then reconsider P1 = M as Function of S,REAL by A3, FUNCT_2:3; reconsider P1 = P1 as Function of S,REAL ; A5: for ASeq being SetSequence of S st ASeq is non-ascending holds ( P1 * ASeq is convergent & lim (P1 * ASeq) = P1 . (Intersection ASeq) ) proof let ASeq be SetSequence of S; ::_thesis: ( ASeq is non-ascending implies ( P1 * ASeq is convergent & lim (P1 * ASeq) = P1 . (Intersection ASeq) ) ) assume A6: ASeq is non-ascending ; ::_thesis: ( P1 * ASeq is convergent & lim (P1 * ASeq) = P1 . (Intersection ASeq) ) for n being Element of NAT holds 0 <= (P1 * ASeq) . n proof let n be Element of NAT ; ::_thesis: 0 <= (P1 * ASeq) . n reconsider A = ASeq . n as Event of S ; ( 0 <= P1 . A & dom (P1 * ASeq) = NAT ) by MEASURE1:def_2, SEQ_1:1; hence 0 <= (P1 * ASeq) . n by FUNCT_1:12; ::_thesis: verum end; then A7: P1 * ASeq is V102() by RINFSUP1:10; reconsider F = ASeq as Function of NAT,S by Th2; A8: for n being Element of NAT holds F . (n + 1) c= F . n by A6, PROB_2:6; A9: M . (F . 0) < +infty by A3, XXREAL_0:9; now__::_thesis:_for_n_being_Element_of_NAT_holds_(P1_*_ASeq)_._(n_+_1)_<=_(P1_*_ASeq)_._n let n be Element of NAT ; ::_thesis: (P1 * ASeq) . (n + 1) <= (P1 * ASeq) . n dom (M * F) = NAT by FUNCT_2:def_1; then A10: ( (M * F) . n = M . (F . n) & (M * F) . (n + 1) = M . (F . (n + 1)) ) by FUNCT_1:12; F . (n + 1) c= F . n by A6, PROB_2:6; hence (P1 * ASeq) . (n + 1) <= (P1 * ASeq) . n by A10, MEASURE1:31; ::_thesis: verum end; then A11: P1 * ASeq is non-increasing by SEQM_3:def_9; then lim (P1 * ASeq) = lower_bound (P1 * ASeq) by A7, RINFSUP1:25 .= inf (rng (M * F)) by A7, Th11 ; then lim (P1 * ASeq) = M . (meet (rng F)) by A8, A9, MEASURE3:12 .= P1 . (Intersection ASeq) by SETLIM_1:8 ; hence ( P1 * ASeq is convergent & lim (P1 * ASeq) = P1 . (Intersection ASeq) ) by A7, A11; ::_thesis: verum end; A12: for A, B being Event of S st A misses B holds P1 . (A \/ B) = (P1 . A) + (P1 . B) proof let A, B be Event of S; ::_thesis: ( A misses B implies P1 . (A \/ B) = (P1 . A) + (P1 . B) ) assume A13: A misses B ; ::_thesis: P1 . (A \/ B) = (P1 . A) + (P1 . B) reconsider A = A, B = B as Element of S ; reconsider A2 = A, B2 = B as Element of S ; P1 . (A \/ B) = (M . A2) + (M . B2) by A13, MEASURE1:30 .= (P1 . A) + (P1 . B) by SUPINF_2:1 ; hence P1 . (A \/ B) = (P1 . A) + (P1 . B) ; ::_thesis: verum end; ( ( for A being Event of S holds 0 <= P1 . A ) & P1 . X = 1 ) by A1, MEASURE1:def_2, MEASURE6:def_1; hence M is Probability of S by A12, A5, PROB_1:def_8; ::_thesis: verum end; definition let X be non empty set ; let S be SigmaField of X; let M be sigma_Measure of S; assume A1: M . X = R_EAL 1 ; func M2P M -> Probability of S equals :: PROB_4:def 2 M; coherence M is Probability of S by A1, Th14; end; :: deftheorem defines M2P PROB_4:def_2_:_ for X being non empty set for S being SigmaField of X for M being sigma_Measure of S st M . X = R_EAL 1 holds M2P M = M; Lm2: for X being set for A1 being SetSequence of X st A1 is non-descending holds for n being Element of NAT holds (Partial_Union A1) . n = A1 . n proof let X be set ; ::_thesis: for A1 being SetSequence of X st A1 is non-descending holds for n being Element of NAT holds (Partial_Union A1) . n = A1 . n let A1 be SetSequence of X; ::_thesis: ( A1 is non-descending implies for n being Element of NAT holds (Partial_Union A1) . n = A1 . n ) defpred S1[ Element of NAT ] means (Partial_Union A1) . \$1 = A1 . \$1; assume A1: A1 is non-descending ; ::_thesis: for n being Element of NAT holds (Partial_Union A1) . n = A1 . n A2: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: S1[k] ; ::_thesis: S1[k + 1] A4: A1 . k c= A1 . (k + 1) by A1, PROB_2:7; thus (Partial_Union A1) . (k + 1) = (A1 . k) \/ (A1 . (k + 1)) by A3, PROB_3:def_2 .= A1 . (k + 1) by A4, XBOOLE_1:12 ; ::_thesis: verum end; A5: S1[ 0 ] by PROB_3:def_2; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A5, A2); ::_thesis: verum end; theorem Th15: :: PROB_4:15 for X being set for A1 being SetSequence of X st A1 is non-descending holds Partial_Union A1 = A1 proof let X be set ; ::_thesis: for A1 being SetSequence of X st A1 is non-descending holds Partial_Union A1 = A1 let A1 be SetSequence of X; ::_thesis: ( A1 is non-descending implies Partial_Union A1 = A1 ) assume A1 is non-descending ; ::_thesis: Partial_Union A1 = A1 then for n being Element of NAT holds (Partial_Union A1) . n = A1 . n by Lm2; hence Partial_Union A1 = A1 by FUNCT_2:63; ::_thesis: verum end; theorem Th16: :: PROB_4:16 for X being set for A1 being SetSequence of X st A1 is non-descending holds ( (Partial_Diff_Union A1) . 0 = A1 . 0 & ( for n being Element of NAT holds (Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ (A1 . n) ) ) proof let X be set ; ::_thesis: for A1 being SetSequence of X st A1 is non-descending holds ( (Partial_Diff_Union A1) . 0 = A1 . 0 & ( for n being Element of NAT holds (Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ (A1 . n) ) ) let A1 be SetSequence of X; ::_thesis: ( A1 is non-descending implies ( (Partial_Diff_Union A1) . 0 = A1 . 0 & ( for n being Element of NAT holds (Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ (A1 . n) ) ) ) assume A1: A1 is non-descending ; ::_thesis: ( (Partial_Diff_Union A1) . 0 = A1 . 0 & ( for n being Element of NAT holds (Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ (A1 . n) ) ) thus (Partial_Diff_Union A1) . 0 = A1 . 0 by PROB_3:def_3; ::_thesis: for n being Element of NAT holds (Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ (A1 . n) thus for n being Element of NAT holds (Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ (A1 . n) ::_thesis: verum proof let n be Element of NAT ; ::_thesis: (Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ (A1 . n) thus (Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) by PROB_3:def_3 .= (A1 . (n + 1)) \ (A1 . n) by A1, Lm2 ; ::_thesis: verum end; end; theorem :: PROB_4:17 for X being set for A1 being SetSequence of X st A1 is non-descending holds for n being Element of NAT holds A1 . (n + 1) = ((Partial_Diff_Union A1) . (n + 1)) \/ (A1 . n) proof let X be set ; ::_thesis: for A1 being SetSequence of X st A1 is non-descending holds for n being Element of NAT holds A1 . (n + 1) = ((Partial_Diff_Union A1) . (n + 1)) \/ (A1 . n) let A1 be SetSequence of X; ::_thesis: ( A1 is non-descending implies for n being Element of NAT holds A1 . (n + 1) = ((Partial_Diff_Union A1) . (n + 1)) \/ (A1 . n) ) assume A1: A1 is non-descending ; ::_thesis: for n being Element of NAT holds A1 . (n + 1) = ((Partial_Diff_Union A1) . (n + 1)) \/ (A1 . n) thus for n being Element of NAT holds A1 . (n + 1) = ((Partial_Diff_Union A1) . (n + 1)) \/ (A1 . n) ::_thesis: verum proof let n be Element of NAT ; ::_thesis: A1 . (n + 1) = ((Partial_Diff_Union A1) . (n + 1)) \/ (A1 . n) A2: A1 . n c= A1 . (n + 1) by A1, PROB_2:7; thus ((Partial_Diff_Union A1) . (n + 1)) \/ (A1 . n) = ((A1 . (n + 1)) \ ((Partial_Union A1) . n)) \/ (A1 . n) by PROB_3:def_3 .= ((A1 . (n + 1)) \ (A1 . n)) \/ (A1 . n) by A1, Lm2 .= (A1 . (n + 1)) \/ (A1 . n) by XBOOLE_1:39 .= A1 . (n + 1) by A2, XBOOLE_1:12 ; ::_thesis: verum end; end; theorem Th18: :: PROB_4:18 for X being set for A1 being SetSequence of X st A1 is non-descending holds for n being Element of NAT holds (Partial_Diff_Union A1) . (n + 1) misses A1 . n proof let X be set ; ::_thesis: for A1 being SetSequence of X st A1 is non-descending holds for n being Element of NAT holds (Partial_Diff_Union A1) . (n + 1) misses A1 . n let A1 be SetSequence of X; ::_thesis: ( A1 is non-descending implies for n being Element of NAT holds (Partial_Diff_Union A1) . (n + 1) misses A1 . n ) assume A1: A1 is non-descending ; ::_thesis: for n being Element of NAT holds (Partial_Diff_Union A1) . (n + 1) misses A1 . n let n be Element of NAT ; ::_thesis: (Partial_Diff_Union A1) . (n + 1) misses A1 . n (Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ (A1 . n) by A1, Th16; hence (Partial_Diff_Union A1) . (n + 1) misses A1 . n by XBOOLE_1:79; ::_thesis: verum end; theorem :: PROB_4:19 for X being set for Si being SigmaField of X for XSeq being SetSequence of Si st XSeq is non-descending holds Partial_Union XSeq = XSeq by Th15; theorem :: PROB_4:20 for X being set for Si being SigmaField of X for XSeq being SetSequence of Si st XSeq is non-descending holds ( (Partial_Diff_Union XSeq) . 0 = XSeq . 0 & ( for n being Element of NAT holds (Partial_Diff_Union XSeq) . (n + 1) = (XSeq . (n + 1)) \ (XSeq . n) ) ) by Th16; theorem :: PROB_4:21 for X being set for Si being SigmaField of X for XSeq being SetSequence of Si st XSeq is non-descending holds for n being Element of NAT holds (Partial_Diff_Union XSeq) . (n + 1) misses XSeq . n by Th18; definition let Omega be non empty set ; let Sigma be SigmaField of Omega; let P be Probability of Sigma; predP is_complete Sigma means :Def3: :: PROB_4:def 3 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 Def3 defines is_complete PROB_4:def_3_:_ for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma holds ( P is_complete Sigma iff for A being Subset of Omega for B being set st B in Sigma & A c= B & P . B = 0 holds A in Sigma ); theorem :: PROB_4:22 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 Sigma ) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for P being Probability of Sigma holds ( P is_complete Sigma iff P2M P is_complete Sigma ) let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma holds ( P is_complete Sigma iff P2M P is_complete Sigma ) let P be Probability of Sigma; ::_thesis: ( P is_complete Sigma iff P2M P is_complete Sigma ) hereby ::_thesis: ( P2M P is_complete Sigma implies P is_complete Sigma ) assume P is_complete Sigma ; ::_thesis: P2M P is_complete Sigma then for A being Subset of Omega for B being set st B in Sigma & A c= B & (P2M P) . B = 0. holds A in Sigma by Def3; hence P2M P is_complete Sigma by MEASURE3:def_1; ::_thesis: verum end; assume P2M P is_complete Sigma ; ::_thesis: P is_complete Sigma then for A being Subset of Omega for B being set st B in Sigma & A c= B & P . B = 0 holds A in Sigma by MEASURE3:def_1; hence P is_complete Sigma by Def3; ::_thesis: verum 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 :Def4: :: PROB_4:def 4 ex A being set st ( A in Sigma & it c= A & P . A = 0 ); existence ex b1 being Subset of Omega ex A being set st ( A in Sigma & b1 c= A & P . A = 0 ) proof reconsider B = {} as Subset of Omega by XBOOLE_1:2; take B ; ::_thesis: ex A being set st ( A in Sigma & B c= A & P . A = 0 ) take A = {} ; ::_thesis: ( A in Sigma & B c= A & P . A = 0 ) thus A in Sigma by PROB_1:4; ::_thesis: ( B c= A & P . A = 0 ) thus B c= A ; ::_thesis: P . A = 0 thus P . A = 0 by VALUED_0:def_19; ::_thesis: verum end; end; :: deftheorem Def4 defines thin PROB_4:def_4_:_ for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma for b4 being Subset of Omega holds ( b4 is thin of P iff ex A being set st ( A in Sigma & b4 c= A & P . A = 0 ) ); theorem Th23: :: PROB_4:23 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 let Omega be non empty set ; ::_thesis: 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 ) let Sigma be SigmaField of Omega; ::_thesis: 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 ) let P be Probability of Sigma; ::_thesis: for Y being Subset of Omega holds ( Y is thin of P iff Y is thin of P2M P ) let Y be Subset of Omega; ::_thesis: ( Y is thin of P iff Y is thin of P2M P ) hereby ::_thesis: ( Y is thin of P2M P implies Y is thin of P ) assume Y is thin of P ; ::_thesis: Y is thin of P2M P then ex A being set st ( A in Sigma & Y c= A & P . A = 0 ) by Def4; hence Y is thin of P2M P by MEASURE3:def_2; ::_thesis: verum end; assume Y is thin of P2M P ; ::_thesis: Y is thin of P then ex B being set st ( B in Sigma & Y c= B & (P2M P) . B = 0. ) by MEASURE3:def_2; hence Y is thin of P by Def4; ::_thesis: verum end; theorem Th24: :: PROB_4:24 for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma holds {} is thin of P proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for P being Probability of Sigma holds {} is thin of P let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma holds {} is thin of P let P be Probability of Sigma; ::_thesis: {} is thin of P ( P . {} = 0 & {} in Sigma ) by PROB_1:4, VALUED_0:def_19; hence {} is thin of P by Def4; ::_thesis: verum end; theorem Th25: :: PROB_4:25 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 let Omega be non empty set ; ::_thesis: 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 let Sigma be SigmaField of Omega; ::_thesis: 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 let P be Probability of Sigma; ::_thesis: 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 let B1, B2 be set ; ::_thesis: ( B1 in Sigma & B2 in Sigma implies for C1, C2 being thin of P st B1 \/ C1 = B2 \/ C2 holds P . B1 = P . B2 ) assume A1: ( B1 in Sigma & B2 in Sigma ) ; ::_thesis: for C1, C2 being thin of P st B1 \/ C1 = B2 \/ C2 holds P . B1 = P . B2 let C1, C2 be thin of P; ::_thesis: ( B1 \/ C1 = B2 \/ C2 implies P . B1 = P . B2 ) assume A2: B1 \/ C1 = B2 \/ C2 ; ::_thesis: P . B1 = P . B2 then A3: B1 c= B2 \/ C2 by XBOOLE_1:7; A4: B2 c= B1 \/ C1 by A2, XBOOLE_1:7; consider D1 being set such that A5: D1 in Sigma and A6: C1 c= D1 and A7: P . D1 = 0 by Def4; A8: B1 \/ C1 c= B1 \/ D1 by A6, XBOOLE_1:9; consider D2 being set such that A9: D2 in Sigma and A10: C2 c= D2 and A11: P . D2 = 0 by Def4; A12: B2 \/ C2 c= B2 \/ D2 by A10, XBOOLE_1:9; reconsider B1 = B1, B2 = B2, D1 = D1, D2 = D2 as Event of Sigma by A1, A5, A9; A13: P . (B1 \/ D1) <= (P . B1) + (P . D1) by PROB_1:39; P . B2 <= P . (B1 \/ D1) by A4, A8, PROB_1:34, XBOOLE_1:1; then A14: P . B2 <= P . B1 by A7, A13, XXREAL_0:2; A15: P . (B2 \/ D2) <= (P . B2) + (P . D2) by PROB_1:39; P . B1 <= P . (B2 \/ D2) by A3, A12, PROB_1:34, XBOOLE_1:1; then P . B1 <= P . B2 by A11, A15, XXREAL_0:2; hence P . B1 = P . B2 by A14, XXREAL_0:1; ::_thesis: verum 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 :Def5: :: PROB_4:def 5 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 ex b1 being non empty Subset-Family of Omega st for A being set holds ( A in b1 iff ex B being set st ( B in Sigma & ex C being thin of P st A = B \/ C ) ) proof A1: {} is thin of P by Th24; A2: for A being set st A = {} holds ex B being set st ( B in Sigma & ex C being thin of P st A = B \/ C ) proof let A be set ; ::_thesis: ( A = {} implies ex B being set st ( B in Sigma & ex C being thin of P st A = B \/ C ) ) consider B being set such that A3: B = {} and A4: B in Sigma by PROB_1:4; consider C being thin of P such that A5: C = {} by A1; assume A = {} ; ::_thesis: ex B being set st ( B in Sigma & ex C being thin of P st A = B \/ C ) then A = B \/ C by A3, A5; hence ex B being set st ( B in Sigma & ex C being thin of P st A = B \/ C ) by A4; ::_thesis: verum end; defpred S1[ set ] means for A being set st A = \$1 holds ex B being set st ( B in Sigma & ex C being thin of P st A = B \/ C ); consider D being set such that A6: for y being set holds ( y in D iff ( y in bool Omega & S1[y] ) ) from XBOOLE_0:sch_1(); A7: 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 ) ) proof let A be set ; ::_thesis: ( A in D iff ex B being set st ( B in Sigma & ex C being thin of P st A = B \/ C ) ) A8: ( A in D iff ( A in bool Omega & ( for y being set st y = A holds ex B being set st ( B in Sigma & ex C being thin of P st y = B \/ C ) ) ) ) by A6; ( ex B being set st ( B in Sigma & ex C being thin of P st A = B \/ C ) implies A in D ) proof assume A9: ex B being set st ( B in Sigma & ex C being thin of P st A = B \/ C ) ; ::_thesis: A in D then A c= Omega by XBOOLE_1:8; hence A in D by A8, A9; ::_thesis: verum end; hence ( A in D iff ex B being set st ( B in Sigma & ex C being thin of P st A = B \/ C ) ) by A6; ::_thesis: verum end; A10: D c= bool Omega proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in bool Omega ) assume x in D ; ::_thesis: x in bool Omega hence x in bool Omega by A6; ::_thesis: verum end; {} c= Omega by XBOOLE_1:2; then reconsider D = D as non empty Subset-Family of Omega by A6, A10, A2; take D ; ::_thesis: 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 ) ) thus 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 ) ) by A7; ::_thesis: verum end; uniqueness for b1, b2 being non empty Subset-Family of Omega st ( for A being set holds ( A in b1 iff ex B being set st ( B in Sigma & ex C being thin of P st A = B \/ C ) ) ) & ( for A being set holds ( A in b2 iff ex B being set st ( B in Sigma & ex C being thin of P st A = B \/ C ) ) ) holds b1 = b2 proof let D1, D2 be non empty Subset-Family of Omega; ::_thesis: ( ( for A being set holds ( A in D1 iff ex B being set st ( B in Sigma & ex C being thin of P st A = B \/ C ) ) ) & ( for A being set holds ( A in D2 iff ex B being set st ( B in Sigma & ex C being thin of P st A = B \/ C ) ) ) implies D1 = D2 ) assume that A11: for A being set holds ( A in D1 iff ex B being set st ( B in Sigma & ex C being thin of P st A = B \/ C ) ) and A12: for A being set holds ( A in D2 iff ex B being set st ( B in Sigma & ex C being thin of P st A = B \/ C ) ) ; ::_thesis: D1 = D2 for A being set holds ( A in D1 iff A in D2 ) proof let A be set ; ::_thesis: ( A in D1 iff A in D2 ) thus ( A in D1 implies A in D2 ) ::_thesis: ( A in D2 implies A in D1 ) proof assume A in D1 ; ::_thesis: A in D2 then ex B being set st ( B in Sigma & ex C being thin of P st A = B \/ C ) by A11; hence A in D2 by A12; ::_thesis: verum end; assume A in D2 ; ::_thesis: A in D1 then ex B being set st ( B in Sigma & ex C being thin of P st A = B \/ C ) by A12; hence A in D1 by A11; ::_thesis: verum end; hence D1 = D2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def5 defines COM PROB_4:def_5_:_ for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma for b4 being non empty Subset-Family of Omega holds ( b4 = COM (Sigma,P) iff for A being set holds ( A in b4 iff ex B being set st ( B in Sigma & ex C being thin of P st A = B \/ C ) ) ); theorem Th26: :: PROB_4:26 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 let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for P being Probability of Sigma for C being thin of P holds C in COM (Sigma,P) let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma for C being thin of P holds C in COM (Sigma,P) let P be Probability of Sigma; ::_thesis: for C being thin of P holds C in COM (Sigma,P) let C be thin of P; ::_thesis: C in COM (Sigma,P) reconsider B = {} as Element of Sigma by PROB_1:4; B \/ C in COM (Sigma,P) by Def5; hence C in COM (Sigma,P) ; ::_thesis: verum end; theorem Th27: :: PROB_4:27 for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma holds COM (Sigma,P) = COM (Sigma,(P2M P)) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for P being Probability of Sigma holds COM (Sigma,P) = COM (Sigma,(P2M P)) let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma holds COM (Sigma,P) = COM (Sigma,(P2M P)) let P be Probability of Sigma; ::_thesis: COM (Sigma,P) = COM (Sigma,(P2M P)) A1: COM (Sigma,(P2M P)) c= COM (Sigma,P) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in COM (Sigma,(P2M P)) or x in COM (Sigma,P) ) assume x in COM (Sigma,(P2M P)) ; ::_thesis: x in COM (Sigma,P) then consider B being set such that A2: B in Sigma and A3: ex C being thin of P2M P st x = B \/ C by MEASURE3:def_3; consider C being thin of P2M P such that A4: x = B \/ C by A3; reconsider C1 = C as thin of P by Th23; x = B \/ C1 by A4; hence x in COM (Sigma,P) by A2, Def5; ::_thesis: verum end; COM (Sigma,P) c= COM (Sigma,(P2M P)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in COM (Sigma,P) or x in COM (Sigma,(P2M P)) ) assume x in COM (Sigma,P) ; ::_thesis: x in COM (Sigma,(P2M P)) then consider B being set such that A5: B in Sigma and A6: ex C being thin of P st x = B \/ C by Def5; consider C being thin of P such that A7: x = B \/ C by A6; reconsider C1 = C as thin of P2M P by Th23; x = B \/ C1 by A7; hence x in COM (Sigma,(P2M P)) by A5, MEASURE3:def_3; ::_thesis: verum end; hence COM (Sigma,P) = COM (Sigma,(P2M P)) by A1, XBOOLE_0:def_10; ::_thesis: verum 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 (Sigma,(P2M P)) equals :: PROB_4:def 6 A; correctness coherence A is Element of COM (Sigma,(P2M P)); by Th27; end; :: deftheorem defines P_COM2M_COM PROB_4:def_6_:_ 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 P_COM2M_COM A = A; theorem Th28: :: PROB_4:28 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 let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for P being Probability of Sigma holds Sigma c= COM (Sigma,P) let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma holds Sigma c= COM (Sigma,P) let P be Probability of Sigma; ::_thesis: Sigma c= COM (Sigma,P) reconsider C = {} as thin of P by Th24; let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in Sigma or A in COM (Sigma,P) ) assume A1: A in Sigma ; ::_thesis: A in COM (Sigma,P) A = A \/ C ; hence A in COM (Sigma,P) by A1, Def5; ::_thesis: verum 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 :Def7: :: PROB_4:def 7 for B being set holds ( B in it iff ( B in Sigma & B c= A & A \ B is thin of P ) ); existence ex b1 being non empty Subset-Family of Omega st for B being set holds ( B in b1 iff ( B in Sigma & B c= A & A \ B is thin of P ) ) proof defpred S1[ set ] means for t being set st t = \$1 holds ( t in Sigma & t c= A & A \ t is thin of P ); consider D being set such that A1: for t being set holds ( t in D iff ( t in bool Omega & S1[t] ) ) from XBOOLE_0:sch_1(); A2: for B being set holds ( B in D iff ( B in Sigma & B c= A & A \ B is thin of P ) ) proof let B be set ; ::_thesis: ( B in D iff ( B in Sigma & B c= A & A \ B is thin of P ) ) ( B in Sigma & B c= A & A \ B is thin of P implies B in D ) proof assume that A3: B in Sigma and A4: ( B c= A & A \ B is thin of P ) ; ::_thesis: B in D for t being set st t = B holds ( t in Sigma & t c= A & A \ t is thin of P ) by A3, A4; hence B in D by A1, A3; ::_thesis: verum end; hence ( B in D iff ( B in Sigma & B c= A & A \ B is thin of P ) ) by A1; ::_thesis: verum end; A5: D c= bool Omega proof let B be set ; :: according to TARSKI:def_3 ::_thesis: ( not B in D or B in bool Omega ) assume B in D ; ::_thesis: B in bool Omega then B in Sigma by A2; hence B in bool Omega ; ::_thesis: verum end; D <> {} proof consider B being set such that A6: B in Sigma and A7: ex C being thin of P st A = B \/ C by Def5; consider C being thin of P such that A8: A = B \/ C by A7; consider E being set such that A9: E in Sigma and A10: C c= E and A11: P . E = 0 by Def4; A \ B = C \ B by A8, XBOOLE_1:40; then A \ B c= C by XBOOLE_1:36; then A \ B c= E by A10, XBOOLE_1:1; then A12: A \ B is thin of P by A9, A11, Def4; B c= A by A8, XBOOLE_1:7; hence D <> {} by A2, A6, A12; ::_thesis: verum end; then reconsider D = D as non empty Subset-Family of Omega by A5; take D ; ::_thesis: for B being set holds ( B in D iff ( B in Sigma & B c= A & A \ B is thin of P ) ) thus for B being set holds ( B in D iff ( B in Sigma & B c= A & A \ B is thin of P ) ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being non empty Subset-Family of Omega st ( for B being set holds ( B in b1 iff ( B in Sigma & B c= A & A \ B is thin of P ) ) ) & ( for B being set holds ( B in b2 iff ( B in Sigma & B c= A & A \ B is thin of P ) ) ) holds b1 = b2 proof let D1, D2 be non empty Subset-Family of Omega; ::_thesis: ( ( for B being set holds ( B in D1 iff ( B in Sigma & B c= A & A \ B is thin of P ) ) ) & ( for B being set holds ( B in D2 iff ( B in Sigma & B c= A & A \ B is thin of P ) ) ) implies D1 = D2 ) assume that A13: for B being set holds ( B in D1 iff ( B in Sigma & B c= A & A \ B is thin of P ) ) and A14: for B being set holds ( B in D2 iff ( B in Sigma & B c= A & A \ B is thin of P ) ) ; ::_thesis: D1 = D2 for B being set holds ( B in D1 iff B in D2 ) proof let B be set ; ::_thesis: ( B in D1 iff B in D2 ) thus ( B in D1 implies B in D2 ) ::_thesis: ( B in D2 implies B in D1 ) proof assume A15: B in D1 ; ::_thesis: B in D2 then A16: A \ B is thin of P by A13; ( B in Sigma & B c= A ) by A13, A15; hence B in D2 by A14, A16; ::_thesis: verum end; assume A17: B in D2 ; ::_thesis: B in D1 then A18: A \ B is thin of P by A14; ( B in Sigma & B c= A ) by A14, A17; hence B in D1 by A13, A18; ::_thesis: verum end; hence D1 = D2 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def7 defines ProbPart PROB_4:def_7_:_ 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 b5 being non empty Subset-Family of Omega holds ( b5 = ProbPart A iff for B being set holds ( B in b5 iff ( B in Sigma & B c= A & A \ B is thin of P ) ) ); theorem :: PROB_4:29 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 let Omega be non empty set ; ::_thesis: 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) let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma for A being Element of COM (Sigma,P) holds ProbPart A = MeasPart (P_COM2M_COM A) let P be Probability of Sigma; ::_thesis: for A being Element of COM (Sigma,P) holds ProbPart A = MeasPart (P_COM2M_COM A) let A be Element of COM (Sigma,P); ::_thesis: ProbPart A = MeasPart (P_COM2M_COM A) A1: MeasPart (P_COM2M_COM A) c= ProbPart A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in MeasPart (P_COM2M_COM A) or x in ProbPart A ) assume A2: x in MeasPart (P_COM2M_COM A) ; ::_thesis: x in ProbPart A (P_COM2M_COM A) \ x is thin of P2M P by A2, MEASURE3:def_4; then A3: A \ x is thin of P by Th23; ( x in Sigma & x c= P_COM2M_COM A ) by A2, MEASURE3:def_4; hence x in ProbPart A by A3, Def7; ::_thesis: verum end; ProbPart A c= MeasPart (P_COM2M_COM A) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ProbPart A or x in MeasPart (P_COM2M_COM A) ) assume A4: x in ProbPart A ; ::_thesis: x in MeasPart (P_COM2M_COM A) A \ x is thin of P by A4, Def7; then A5: (P_COM2M_COM A) \ x is thin of P2M P by Th23; ( x in Sigma & x c= A ) by A4, Def7; hence x in MeasPart (P_COM2M_COM A) by A5, MEASURE3:def_4; ::_thesis: verum end; hence ProbPart A = MeasPart (P_COM2M_COM A) by A1, XBOOLE_0:def_10; ::_thesis: verum end; 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) for A1, A2 being set st A1 in ProbPart A & A2 in ProbPart A holds P . A1 = P . A2 proof let Omega be non empty set ; ::_thesis: 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 let Sigma be SigmaField of Omega; ::_thesis: 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 let P be Probability of Sigma; ::_thesis: 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 let A be Element of COM (Sigma,P); ::_thesis: for A1, A2 being set st A1 in ProbPart A & A2 in ProbPart A holds P . A1 = P . A2 let A1, A2 be set ; ::_thesis: ( A1 in ProbPart A & A2 in ProbPart A implies P . A1 = P . A2 ) assume that A1: A1 in ProbPart A and A2: A2 in ProbPart A ; ::_thesis: P . A1 = P . A2 reconsider C1 = A \ A1, C2 = A \ A2 as thin of P by A1, A2, Def7; A3: A2 c= A by A2, Def7; A1 c= A by A1, Def7; then A4: A1 \/ C1 = A by XBOOLE_1:45 .= A2 \/ C2 by A3, XBOOLE_1:45 ; ( A1 in Sigma & A2 in Sigma ) by A1, A2, Def7; hence P . A1 = P . A2 by A4, Th25; ::_thesis: verum end; theorem Th31: :: PROB_4:31 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 Element of NAT holds BSeq . n in ProbPart (F . n) proof let Omega be non empty set ; ::_thesis: 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 Element of NAT holds BSeq . n in ProbPart (F . n) let Sigma be SigmaField of Omega; ::_thesis: 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 Element of NAT holds BSeq . n in ProbPart (F . n) let P be Probability of Sigma; ::_thesis: for F being Function of NAT,(COM (Sigma,P)) ex BSeq being SetSequence of Sigma st for n being Element of NAT holds BSeq . n in ProbPart (F . n) let F be Function of NAT,(COM (Sigma,P)); ::_thesis: ex BSeq being SetSequence of Sigma st for n being Element of NAT holds BSeq . n in ProbPart (F . n) defpred S1[ Element of NAT , set ] means for n being Element of NAT for y being set st n = \$1 & y = \$2 holds y in ProbPart (F . n); A1: for t being Element of NAT ex A being Element of Sigma st S1[t,A] proof let t be Element of NAT ; ::_thesis: ex A being Element of Sigma st S1[t,A] set A = the Element of ProbPart (F . t); reconsider A = the Element of ProbPart (F . t) as Element of Sigma by Def7; take A ; ::_thesis: S1[t,A] thus S1[t,A] ; ::_thesis: verum end; ex G being Function of NAT,Sigma st for t being Element of NAT holds S1[t,G . t] from FUNCT_2:sch_3(A1); then consider G being Function of NAT,Sigma such that A2: for t, n being Element of NAT for y being set st n = t & y = G . t holds y in ProbPart (F . n) ; reconsider BSeq = G as SetSequence of Omega by FUNCT_2:7; reconsider BSeq = BSeq as SetSequence of Sigma ; take BSeq ; ::_thesis: for n being Element of NAT holds BSeq . n in ProbPart (F . n) thus for n being Element of NAT holds BSeq . n in ProbPart (F . n) by A2; ::_thesis: verum end; theorem Th32: :: 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)) for BSeq being SetSequence of Sigma ex CSeq being SetSequence of Omega st for n being Element of NAT holds CSeq . n = (F . n) \ (BSeq . n) proof let Omega be non empty set ; ::_thesis: 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 Element of NAT holds CSeq . n = (F . n) \ (BSeq . n) let Sigma be SigmaField of Omega; ::_thesis: 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 Element of NAT holds CSeq . n = (F . n) \ (BSeq . n) let P be Probability of Sigma; ::_thesis: 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 Element of NAT holds CSeq . n = (F . n) \ (BSeq . n) let F be Function of NAT,(COM (Sigma,P)); ::_thesis: for BSeq being SetSequence of Sigma ex CSeq being SetSequence of Omega st for n being Element of NAT holds CSeq . n = (F . n) \ (BSeq . n) let G be SetSequence of Sigma; ::_thesis: ex CSeq being SetSequence of Omega st for n being Element of NAT holds CSeq . n = (F . n) \ (G . n) defpred S1[ Element of NAT , set ] means for n being Element of NAT for y being set st n = \$1 & y = \$2 holds y = (F . n) \ (G . n); A1: for t being Element of NAT ex A being Element of bool Omega st S1[t,A] proof let t be Element of NAT ; ::_thesis: ex A being Element of bool Omega st S1[t,A] F . t is Element of COM (Sigma,P) ; then reconsider A = (F . t) \ (G . t) as Element of bool Omega by XBOOLE_1:1; take A ; ::_thesis: S1[t,A] thus S1[t,A] ; ::_thesis: verum end; ex H being Function of NAT,(bool Omega) st for t being Element of NAT holds S1[t,H . t] from FUNCT_2:sch_3(A1); then consider H being Function of NAT,(bool Omega) such that A2: for t, n being Element of NAT for y being set st n = t & y = H . t holds y = (F . n) \ (G . n) ; take H ; ::_thesis: for n being Element of NAT holds H . n = (F . n) \ (G . n) thus for n being Element of NAT holds H . n = (F . n) \ (G . n) by A2; ::_thesis: verum end; theorem Th33: :: PROB_4:33 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 Element of NAT holds BSeq . n is thin of P ) holds ex CSeq being SetSequence of Sigma st for n being Element of NAT holds ( BSeq . n c= CSeq . n & P . (CSeq . n) = 0 ) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for P being Probability of Sigma for BSeq being SetSequence of Omega st ( for n being Element of NAT holds BSeq . n is thin of P ) holds ex CSeq being SetSequence of Sigma st for n being Element of NAT holds ( BSeq . n c= CSeq . n & P . (CSeq . n) = 0 ) let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma for BSeq being SetSequence of Omega st ( for n being Element of NAT holds BSeq . n is thin of P ) holds ex CSeq being SetSequence of Sigma st for n being Element of NAT holds ( BSeq . n c= CSeq . n & P . (CSeq . n) = 0 ) let P be Probability of Sigma; ::_thesis: for BSeq being SetSequence of Omega st ( for n being Element of NAT holds BSeq . n is thin of P ) holds ex CSeq being SetSequence of Sigma st for n being Element of NAT holds ( BSeq . n c= CSeq . n & P . (CSeq . n) = 0 ) let BSeq be SetSequence of Omega; ::_thesis: ( ( for n being Element of NAT holds BSeq . n is thin of P ) implies ex CSeq being SetSequence of Sigma st for n being Element of NAT holds ( BSeq . n c= CSeq . n & P . (CSeq . n) = 0 ) ) defpred S1[ Element of NAT , set ] means for n being Element of NAT for y being set st n = \$1 & y = \$2 holds ( y in Sigma & BSeq . n c= y & P . y = 0 ); assume A1: for n being Element of NAT holds BSeq . n is thin of P ; ::_thesis: ex CSeq being SetSequence of Sigma st for n being Element of NAT holds ( BSeq . n c= CSeq . n & P . (CSeq . n) = 0 ) A2: for t being Element of NAT ex A being Element of Sigma st S1[t,A] proof let t be Element of NAT ; ::_thesis: ex A being Element of Sigma st S1[t,A] BSeq . t is thin of P by A1; then consider A being set such that A3: A in Sigma and A4: ( BSeq . t c= A & P . A = 0 ) by Def4; reconsider A = A as Element of Sigma by A3; take A ; ::_thesis: S1[t,A] thus S1[t,A] by A4; ::_thesis: verum end; ex G being Function of NAT,Sigma st for t being Element of NAT holds S1[t,G . t] from FUNCT_2:sch_3(A2); then consider G being Function of NAT,Sigma such that A5: for t, n being Element of NAT for y being set st n = t & y = G . t holds ( y in Sigma & BSeq . n c= y & P . y = 0 ) ; reconsider CSeq = G as SetSequence of Omega by FUNCT_2:7; reconsider CSeq = CSeq as SetSequence of Sigma ; take CSeq ; ::_thesis: for n being Element of NAT holds ( BSeq . n c= CSeq . n & P . (CSeq . n) = 0 ) thus for n being Element of NAT holds ( BSeq . n c= CSeq . n & P . (CSeq . n) = 0 ) by A5; ::_thesis: verum end; theorem Th34: :: PROB_4:34 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 let Omega be non empty set ; ::_thesis: 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 let Sigma be SigmaField of Omega; ::_thesis: 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 let P be Probability of Sigma; ::_thesis: 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 let D be non empty Subset-Family of Omega; ::_thesis: ( ( 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 ) ) ) implies D is SigmaField of Omega ) assume A1: 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 ) ) ; ::_thesis: D is SigmaField of Omega A2: for A1 being SetSequence of Omega st rng A1 c= D holds Union A1 in D proof let A1 be SetSequence of Omega; ::_thesis: ( rng A1 c= D implies Union A1 in D ) reconsider F = A1 as Function of NAT,(bool Omega) ; A3: dom F = NAT by FUNCT_2:def_1; assume A4: rng A1 c= D ; ::_thesis: Union A1 in D A5: for n being Element of NAT ex B being set st ( B in Sigma & ex C being thin of P st F . n = B \/ C ) proof let n be Element of NAT ; ::_thesis: ex B being set st ( B in Sigma & ex C being thin of P st F . n = B \/ C ) F . n in rng F by NAT_1:51; hence ex B being set st ( B in Sigma & ex C being thin of P st F . n = B \/ C ) by A1, A4; ::_thesis: verum end; for n being Element of NAT holds F . n in COM (Sigma,P) proof let n be Element of NAT ; ::_thesis: F . n in COM (Sigma,P) ex B being set st ( B in Sigma & ex C being thin of P st F . n = B \/ C ) by A5; hence F . n in COM (Sigma,P) by Def5; ::_thesis: verum end; then for n being set st n in NAT holds F . n in COM (Sigma,P) ; then reconsider F = F as Function of NAT,(COM (Sigma,P)) by A3, FUNCT_2:3; consider BSeq being SetSequence of Sigma such that A6: for n being Element of NAT holds BSeq . n in ProbPart (F . n) by Th31; consider CSeq being SetSequence of Omega such that A7: for n being Element of NAT holds CSeq . n = (F . n) \ (BSeq . n) by Th32; A8: for n being Element of NAT holds ( BSeq . n in Sigma & BSeq . n c= F . n & (F . n) \ (BSeq . n) is thin of P ) proof let n be Element of NAT ; ::_thesis: ( BSeq . n in Sigma & BSeq . n c= F . n & (F . n) \ (BSeq . n) is thin of P ) BSeq . n in ProbPart (F . n) by A6; hence ( BSeq . n in Sigma & BSeq . n c= F . n & (F . n) \ (BSeq . n) is thin of P ) by Def7; ::_thesis: verum end; for n being Element of NAT holds CSeq . n is thin of P proof let n be Element of NAT ; ::_thesis: CSeq . n is thin of P (F . n) \ (BSeq . n) is thin of P by A8; hence CSeq . n is thin of P by A7; ::_thesis: verum end; then consider DSeq being SetSequence of Sigma such that A9: for n being Element of NAT holds ( CSeq . n c= DSeq . n & P . (DSeq . n) = 0 ) by Th33; A10: Union A1 = union (rng A1) by CARD_3:def_4; ex B being set st ( B in Sigma & ex C being thin of P st Union A1 = B \/ C ) proof set B = union (rng BSeq); take union (rng BSeq) ; ::_thesis: ( union (rng BSeq) in Sigma & ex C being thin of P st Union A1 = (union (rng BSeq)) \/ C ) A11: union (rng BSeq) c= union (rng F) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng BSeq) or x in union (rng F) ) assume x in union (rng BSeq) ; ::_thesis: x in union (rng F) then consider Z being set such that A12: x in Z and A13: Z in rng BSeq by TARSKI:def_4; dom BSeq = NAT by FUNCT_2:def_1; then consider n being set such that A14: n in NAT and A15: Z = BSeq . n by A13, FUNCT_1:def_3; reconsider n = n as Element of NAT by A14; set P = F . n; A16: BSeq . n c= F . n by A8; ex P being set st ( P in rng F & x in P ) proof take F . n ; ::_thesis: ( F . n in rng F & x in F . n ) thus ( F . n in rng F & x in F . n ) by A3, A12, A15, A16, FUNCT_1:def_3; ::_thesis: verum end; hence x in union (rng F) by TARSKI:def_4; ::_thesis: verum end; A17: ex C being thin of P st Union A1 = (union (rng BSeq)) \/ C proof set C = (Union A1) \ (union (rng BSeq)); Union DSeq in Sigma by PROB_1:17; then A18: union (rng DSeq) in Sigma by CARD_3:def_4; A19: (Union A1) \ (union (rng BSeq)) c= union (rng CSeq) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Union A1) \ (union (rng BSeq)) or x in union (rng CSeq) ) assume A20: x in (Union A1) \ (union (rng BSeq)) ; ::_thesis: x in union (rng CSeq) then x in union (rng F) by A10, XBOOLE_0:def_5; then consider Z being set such that A21: x in Z and A22: Z in rng F by TARSKI:def_4; consider n being set such that A23: n in NAT and A24: Z = F . n by A3, A22, FUNCT_1:def_3; reconsider n = n as Element of NAT by A23; A25: not x in union (rng BSeq) by A20, XBOOLE_0:def_5; not x in BSeq . n proof dom BSeq = NAT by FUNCT_2:def_1; then A26: BSeq . n in rng BSeq by FUNCT_1:def_3; assume x in BSeq . n ; ::_thesis: contradiction hence contradiction by A25, A26, TARSKI:def_4; ::_thesis: verum end; then A27: x in (F . n) \ (BSeq . n) by A21, A24, XBOOLE_0:def_5; ex Z being set st ( x in Z & Z in rng CSeq ) proof take CSeq . n ; ::_thesis: ( x in CSeq . n & CSeq . n in rng CSeq ) dom CSeq = NAT by FUNCT_2:def_1; hence ( x in CSeq . n & CSeq . n in rng CSeq ) by A7, A27, FUNCT_1:def_3; ::_thesis: verum end; hence x in union (rng CSeq) by TARSKI:def_4; ::_thesis: verum end; for A being set st A in rng DSeq holds P . A = 0 proof let A be set ; ::_thesis: ( A in rng DSeq implies P . A = 0 ) A28: dom DSeq = NAT by FUNCT_2:def_1; assume A in rng DSeq ; ::_thesis: P . A = 0 then ex n being set st ( n in NAT & A = DSeq . n ) by A28, FUNCT_1:def_3; hence P . A = 0 by A9; ::_thesis: verum end; then A29: P . (union (rng DSeq)) = 0 by Th8; union (rng CSeq) c= union (rng DSeq) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng CSeq) or x in union (rng DSeq) ) assume x in union (rng CSeq) ; ::_thesis: x in union (rng DSeq) then consider Z being set such that A30: x in Z and A31: Z in rng CSeq by TARSKI:def_4; dom CSeq = NAT by FUNCT_2:def_1; then consider n being set such that A32: n in NAT and A33: Z = CSeq . n by A31, FUNCT_1:def_3; reconsider n = n as Element of NAT by A32; n in dom DSeq by A32, FUNCT_2:def_1; then A34: DSeq . n in rng DSeq by FUNCT_1:def_3; CSeq . n c= DSeq . n by A9; hence x in union (rng DSeq) by A30, A33, A34, TARSKI:def_4; ::_thesis: verum end; then (Union A1) \ (union (rng BSeq)) c= union (rng DSeq) by A19, XBOOLE_1:1; then A35: (Union A1) \ (union (rng BSeq)) is thin of P by A29, A18, Def4; Union A1 = ((Union A1) \ (union (rng BSeq))) \/ ((union (rng F)) /\ (union (rng BSeq))) by A10, XBOOLE_1:51 .= (union (rng BSeq)) \/ ((Union A1) \ (union (rng BSeq))) by A11, XBOOLE_1:28 ; then consider C being thin of P such that A36: Union A1 = (union (rng BSeq)) \/ C by A35; take C ; ::_thesis: Union A1 = (union (rng BSeq)) \/ C thus Union A1 = (union (rng BSeq)) \/ C by A36; ::_thesis: verum end; Union BSeq in Sigma by PROB_1:17; hence ( union (rng BSeq) in Sigma & ex C being thin of P st Union A1 = (union (rng BSeq)) \/ C ) by A17, CARD_3:def_4; ::_thesis: verum end; hence Union A1 in D by A1; ::_thesis: verum end; for A being Subset of Omega st A in D holds A ` in D proof let A be Subset of Omega; ::_thesis: ( A in D implies A ` in D ) assume A37: A in D ; ::_thesis: A ` in D ex Q being set st ( Q in Sigma & ex W being thin of P st Omega \ A = Q \/ W ) proof consider B being set such that A38: B in Sigma and A39: ex C being thin of P st A = B \/ C by A1, A37; consider C being thin of P such that A40: A = B \/ C by A39; reconsider B = B as Subset of Omega by A38; set H = Omega \ B; consider G being set such that A41: G in Sigma and A42: C c= G and A43: P . G = 0 by Def4; set Q = (Omega \ B) \ G; A44: Omega \ A = (Omega \ B) \ C by A40, XBOOLE_1:41; A45: ex W being thin of P st Omega \ A = ((Omega \ B) \ G) \/ W proof set W = (Omega \ B) /\ (G \ C); (Omega \ B) /\ (G \ C) c= Omega \ B by XBOOLE_1:17; then reconsider W = (Omega \ B) /\ (G \ C) as Subset of Omega by XBOOLE_1:1; reconsider W = W as thin of P by A41, A43, Def4; take W ; ::_thesis: Omega \ A = ((Omega \ B) \ G) \/ W thus Omega \ A = ((Omega \ B) \ G) \/ W by A42, A44, Lm1; ::_thesis: verum end; take (Omega \ B) \ G ; ::_thesis: ( (Omega \ B) \ G in Sigma & ex W being thin of P st Omega \ A = ((Omega \ B) \ G) \/ W ) B ` in Sigma by A38, PROB_1:def_1; hence ( (Omega \ B) \ G in Sigma & ex W being thin of P st Omega \ A = ((Omega \ B) \ G) \/ W ) by A41, A45, PROB_1:6; ::_thesis: verum end; hence A ` in D by A1; ::_thesis: verum end; hence D is SigmaField of Omega by A2, Th4; ::_thesis: verum end; registration let Omega be non empty set ; let Sigma be SigmaField of Omega; let P be Probability of Sigma; cluster COM (Sigma,P) -> non empty compl-closed sigma-multiplicative ; coherence ( COM (Sigma,P) is compl-closed & COM (Sigma,P) is sigma-multiplicative ) proof for A being set holds ( A in COM (Sigma,P) iff ex B being set st ( B in Sigma & ex C being thin of P st A = B \/ C ) ) by Def5; hence ( COM (Sigma,P) is compl-closed & COM (Sigma,P) is sigma-multiplicative ) by Th34; ::_thesis: verum 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 for b1 being thin of P holds b1 is Event of COM (Sigma,P) by Th26; end; theorem Th35: :: PROB_4:35 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 let Omega be non empty set ; ::_thesis: 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 ) ) let Sigma be SigmaField of Omega; ::_thesis: 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 ) ) let P be Probability of Sigma; ::_thesis: 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 ) ) let A be set ; ::_thesis: ( 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 ) ) thus ( A in COM (Sigma,P) implies ex A1, A2 being set st ( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) ) ::_thesis: ( ex A1, A2 being set st ( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) implies A in COM (Sigma,P) ) proof assume A in COM (Sigma,P) ; ::_thesis: ex A1, A2 being set st ( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) then consider B being set such that A1: B in Sigma and A2: ex C being thin of P st A = B \/ C by Def5; consider C being thin of P such that A3: A = B \/ C by A2; reconsider B = B as Event of Sigma by A1; consider D being set such that A4: D in Sigma and A5: C c= D and A6: P . D = 0 by Def4; reconsider D = D as Event of Sigma by A4; reconsider E = D \/ B as Event of Sigma ; A7: P . (D \/ B) <= (P . D) + (P . B) by PROB_1:39; P . (E \ B) = P . (D \ B) by XBOOLE_1:40 .= (P . (D \/ B)) - (P . B) by Th5 ; then P . (E \ B) <= 0 by A6, A7, XREAL_1:47; then A8: P . (E \ B) = 0 by PROB_1:def_8; A c= E by A3, A5, XBOOLE_1:9; hence ex A1, A2 being set st ( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) by A2, A8, XBOOLE_1:7; ::_thesis: verum end; thus ( ex A1, A2 being set st ( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) implies A in COM (Sigma,P) ) ::_thesis: verum proof given A1, A2 being set such that A9: A1 in Sigma and A10: A2 in Sigma and A11: A1 c= A and A12: A c= A2 and A13: P . (A2 \ A1) = 0 ; ::_thesis: A in COM (Sigma,P) reconsider A2 = A2 as Element of Sigma by A10; reconsider A1 = A1 as Element of Sigma by A9; set C = A \ A1; A14: A \ A1 is thin of P proof reconsider D = A2 \ A1 as Element of Sigma ; A15: A \ A1 c= D proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A \ A1 or x in D ) assume x in A \ A1 ; ::_thesis: x in D then ( x in A & not x in A1 ) by XBOOLE_0:def_5; hence x in D by A12, XBOOLE_0:def_5; ::_thesis: verum end; then A \ A1 c= Omega by XBOOLE_1:1; hence A \ A1 is thin of P by A13, A15, Def4; ::_thesis: verum end; A = A1 \/ (A \ A1) by A11, XBOOLE_1:45; hence A in COM (Sigma,P) by A14, Def5; ::_thesis: verum end; end; theorem :: PROB_4:36 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 let Omega be non empty set ; ::_thesis: 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) let Sigma be SigmaField of Omega; ::_thesis: 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) let P be Probability of Sigma; ::_thesis: 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) let C be non empty Subset-Family of Omega; ::_thesis: ( ( 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 ) ) ) implies C = COM (Sigma,P) ) assume A1: 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 ) ) ; ::_thesis: C = COM (Sigma,P) now__::_thesis:_for_A_being_set_holds_ (_A_in_C_iff_A_in_COM_(Sigma,P)_) let A be set ; ::_thesis: ( A in C iff A in COM (Sigma,P) ) ( 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 ) ) by A1; hence ( A in C iff A in COM (Sigma,P) ) by Th35; ::_thesis: verum end; hence C = COM (Sigma,P) by TARSKI:1; ::_thesis: verum 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 :Def8: :: PROB_4:def 8 for B being set st B in Sigma holds for C being thin of P holds it . (B \/ C) = P . B; existence ex b1 being Probability of COM (Sigma,P) st for B being set st B in Sigma holds for C being thin of P holds b1 . (B \/ C) = P . B proof reconsider C = {} as thin of P by Th24; defpred S1[ set , set ] means for x, y being set st x in COM (Sigma,P) & x = \$1 & y = \$2 holds for B being set st B in Sigma holds for C being thin of P st x = B \/ C holds y = P . B; set B = {} ; A1: {} is thin of P by Th24; A2: for x being set st x in COM (Sigma,P) holds ex y being set st ( y in REAL & S1[x,y] ) proof let x be set ; ::_thesis: ( x in COM (Sigma,P) implies ex y being set st ( y in REAL & S1[x,y] ) ) assume x in COM (Sigma,P) ; ::_thesis: ex y being set st ( y in REAL & S1[x,y] ) then consider B being set such that A3: ( B in Sigma & ex C being thin of P st x = B \/ C ) by Def5; take P . B ; ::_thesis: ( P . B in REAL & S1[x,P . B] ) thus ( P . B in REAL & S1[x,P . B] ) by A3, Th25, FUNCT_2:5; ::_thesis: verum end; consider comP being Function of (COM (Sigma,P)),REAL such that A4: for x being set st x in COM (Sigma,P) holds S1[x,comP . x] from FUNCT_2:sch_1(A2); A5: for B being set st B in Sigma holds for C being thin of P holds comP . (B \/ C) = P . B proof let B be set ; ::_thesis: ( B in Sigma implies for C being thin of P holds comP . (B \/ C) = P . B ) assume A6: B in Sigma ; ::_thesis: for C being thin of P holds comP . (B \/ C) = P . B let C be thin of P; ::_thesis: comP . (B \/ C) = P . B B \/ C in COM (Sigma,P) by A6, Def5; hence comP . (B \/ C) = P . B by A4, A6; ::_thesis: verum end; A7: for BSeq being SetSequence of COM (Sigma,P) st BSeq is V118() holds Sum (comP * BSeq) = comP . (Union BSeq) proof let BSeq be SetSequence of COM (Sigma,P); ::_thesis: ( BSeq is V118() implies Sum (comP * BSeq) = comP . (Union BSeq) ) assume A8: BSeq is V118() ; ::_thesis: Sum (comP * BSeq) = comP . (Union BSeq) reconsider F = BSeq as Function of NAT,(bool Omega) ; rng F c= COM (Sigma,P) by RELAT_1:def_19; then reconsider F = F as Function of NAT,(COM (Sigma,P)) by FUNCT_2:6; consider CSeq being SetSequence of Sigma such that A9: for n being Element of NAT holds CSeq . n in ProbPart (F . n) by Th31; consider B being set such that A10: B = union (rng CSeq) ; Union CSeq in Sigma by PROB_1:17; then reconsider B = B as Element of Sigma by A10, CARD_3:def_4; consider DSeq being SetSequence of Omega such that A11: for n being Element of NAT holds DSeq . n = (F . n) \ (CSeq . n) by Th32; A12: for n being Element of NAT holds ( CSeq . n in Sigma & CSeq . n c= F . n & (F . n) \ (CSeq . n) is thin of P ) proof let n be Element of NAT ; ::_thesis: ( CSeq . n in Sigma & CSeq . n c= F . n & (F . n) \ (CSeq . n) is thin of P ) CSeq . n in ProbPart (F . n) by A9; hence ( CSeq . n in Sigma & CSeq . n c= F . n & (F . n) \ (CSeq . n) is thin of P ) by Def7; ::_thesis: verum end; for n being Element of NAT holds DSeq . n is thin of P proof let n be Element of NAT ; ::_thesis: DSeq . n is thin of P (F . n) \ (CSeq . n) is thin of P by A12; hence DSeq . n is thin of P by A11; ::_thesis: verum end; then consider ESeq being SetSequence of Sigma such that A13: for n being Element of NAT holds ( DSeq . n c= ESeq . n & P . (ESeq . n) = 0 ) by Th33; A14: dom BSeq = NAT by FUNCT_2:def_1; A15: B c= union (rng F) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in union (rng F) ) assume x in B ; ::_thesis: x in union (rng F) then consider Z being set such that A16: x in Z and A17: Z in rng CSeq by A10, TARSKI:def_4; dom CSeq = NAT by FUNCT_2:def_1; then consider n being set such that A18: n in NAT and A19: Z = CSeq . n by A17, FUNCT_1:def_3; reconsider n = n as Element of NAT by A18; set P = F . n; A20: CSeq . n c= F . n by A12; ex P being set st ( P in rng F & x in P ) proof take F . n ; ::_thesis: ( F . n in rng F & x in F . n ) thus ( F . n in rng F & x in F . n ) by A14, A16, A19, A20, FUNCT_1:def_3; ::_thesis: verum end; hence x in union (rng F) by TARSKI:def_4; ::_thesis: verum end; A21: ex C being thin of P st union (rng F) = B \/ C proof set C = (union (rng F)) \ B; A22: union (rng F) = ((union (rng F)) \ B) \/ ((union (rng F)) /\ B) by XBOOLE_1:51 .= B \/ ((union (rng F)) \ B) by A15, XBOOLE_1:28 ; reconsider C = (union (rng F)) \ B as Subset of Omega ; A23: C c= union (rng DSeq) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C or x in union (rng DSeq) ) assume A24: x in C ; ::_thesis: x in union (rng DSeq) then x in union (rng F) by XBOOLE_0:def_5; then consider Z being set such that A25: x in Z and A26: Z in rng F by TARSKI:def_4; consider n being set such that A27: n in NAT and A28: Z = F . n by A14, A26, FUNCT_1:def_3; reconsider n = n as Element of NAT by A27; A29: not x in union (rng CSeq) by A10, A24, XBOOLE_0:def_5; not x in CSeq . n proof dom CSeq = NAT by FUNCT_2:def_1; then A30: CSeq . n in rng CSeq by FUNCT_1:def_3; assume x in CSeq . n ; ::_thesis: contradiction hence contradiction by A29, A30, TARSKI:def_4; ::_thesis: verum end; then A31: x in (F . n) \ (CSeq . n) by A25, A28, XBOOLE_0:def_5; ex Z being set st ( x in Z & Z in rng DSeq ) proof take DSeq . n ; ::_thesis: ( x in DSeq . n & DSeq . n in rng DSeq ) dom DSeq = NAT by FUNCT_2:def_1; hence ( x in DSeq . n & DSeq . n in rng DSeq ) by A11, A31, FUNCT_1:def_3; ::_thesis: verum end; hence x in union (rng DSeq) by TARSKI:def_4; ::_thesis: verum end; for A being set st A in rng ESeq holds P . A = 0 proof let A be set ; ::_thesis: ( A in rng ESeq implies P . A = 0 ) A32: dom ESeq = NAT by FUNCT_2:def_1; assume A in rng ESeq ; ::_thesis: P . A = 0 then ex n being set st ( n in NAT & A = ESeq . n ) by A32, FUNCT_1:def_3; hence P . A = 0 by A13; ::_thesis: verum end; then A33: P . (union (rng ESeq)) = 0 by Th8; Union ESeq in Sigma by PROB_1:17; then A34: union (rng ESeq) in Sigma by CARD_3:def_4; union (rng DSeq) c= union (rng ESeq) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng DSeq) or x in union (rng ESeq) ) assume x in union (rng DSeq) ; ::_thesis: x in union (rng ESeq) then consider Z being set such that A35: x in Z and A36: Z in rng DSeq by TARSKI:def_4; dom DSeq = NAT by FUNCT_2:def_1; then consider n being set such that A37: n in NAT and A38: Z = DSeq . n by A36, FUNCT_1:def_3; reconsider n = n as Element of NAT by A37; n in dom ESeq by A37, FUNCT_2:def_1; then A39: ESeq . n in rng ESeq by FUNCT_1:def_3; DSeq . n c= ESeq . n by A13; hence x in union (rng ESeq) by A35, A38, A39, TARSKI:def_4; ::_thesis: verum end; then C c= union (rng ESeq) by A23, XBOOLE_1:1; then C is thin of P by A34, A33, Def4; then consider C being thin of P such that A40: union (rng F) = B \/ C by A22; take C ; ::_thesis: union (rng F) = B \/ C thus union (rng F) = B \/ C by A40; ::_thesis: verum end; for n, m being set st n <> m holds CSeq . n misses CSeq . m proof let n, m be set ; ::_thesis: ( n <> m implies CSeq . n misses CSeq . m ) A41: dom F = NAT by FUNCT_2:def_1 .= dom CSeq by FUNCT_2:def_1 ; for n being set holds CSeq . n c= F . n proof let n be set ; ::_thesis: CSeq . n c= F . n percases ( n in dom F or not n in dom F ) ; suppose n in dom F ; ::_thesis: CSeq . n c= F . n hence CSeq . n c= F . n by A12; ::_thesis: verum end; supposeA42: not n in dom F ; ::_thesis: CSeq . n c= F . n then F . n = {} by FUNCT_1:def_2 .= CSeq . n by A41, A42, FUNCT_1:def_2 ; hence CSeq . n c= F . n ; ::_thesis: verum end; end; end; then A43: ( CSeq . n c= F . n & CSeq . m c= F . m ) ; assume n <> m ; ::_thesis: CSeq . n misses CSeq . m then F . n misses F . m by A8, PROB_2:def_2; then (F . n) /\ (F . m) = {} by XBOOLE_0:def_7; then (CSeq . n) /\ (CSeq . m) = {} by A43, XBOOLE_1:3, XBOOLE_1:27; hence CSeq . n misses CSeq . m by XBOOLE_0:def_7; ::_thesis: verum end; then A44: CSeq is V118() by PROB_2:def_2; Sum (comP * F) = comP . (Union F) proof A45: for n being Element of NAT holds comP . (F . n) = P . (CSeq . n) proof let n be Element of NAT ; ::_thesis: comP . (F . n) = P . (CSeq . n) (F . n) \ (CSeq . n) is thin of P by A12; then consider C being thin of P such that A46: C = (F . n) \ (CSeq . n) ; F . n = ((F . n) /\ (CSeq . n)) \/ ((F . n) \ (CSeq . n)) by XBOOLE_1:51 .= (CSeq . n) \/ C by A12, A46, XBOOLE_1:28 ; hence comP . (F . n) = P . (CSeq . n) by A5; ::_thesis: verum end; for x being Element of NAT holds (comP * F) . x = (P * CSeq) . x proof let x be Element of NAT ; ::_thesis: (comP * F) . x = (P * CSeq) . x (comP * F) . x = comP . (F . x) by FUNCT_2:15 .= P . (CSeq . x) by A45 .= (P * CSeq) . x by FUNCT_2:15 ; hence (comP * F) . x = (P * CSeq) . x ; ::_thesis: verum end; then A47: Sum (comP * F) = Sum (P * CSeq) by FUNCT_2:63; comP . (union (rng F)) = P . (union (rng CSeq)) by A5, A10, A21; then comP . (Union F) = P . (union (rng CSeq)) by CARD_3:def_4 .= P . (Union CSeq) by CARD_3:def_4 ; hence Sum (comP * F) = comP . (Union F) by A44, A47, PROB_3:46; ::_thesis: verum end; hence Sum (comP * BSeq) = comP . (Union BSeq) ; ::_thesis: verum end; A48: for x being Element of COM (Sigma,P) holds comP . x >= 0 proof let x be Element of COM (Sigma,P); ::_thesis: comP . x >= 0 consider B being set such that A49: B in Sigma and A50: ex C being thin of P st x = B \/ C by Def5; reconsider B = B as Element of Sigma by A49; comP . x = P . B by A4, A50; hence comP . x >= 0 by PROB_1:def_8; ::_thesis: verum end; {} = {} \/ C ; then A51: comP . {} = P . {} by A5, PROB_1:4 .= 0 by VALUED_0:def_19 ; A52: for A, B being Event of COM (Sigma,P) st A misses B holds comP . (A \/ B) = (comP . A) + (comP . B) proof let A, B be Event of COM (Sigma,P); ::_thesis: ( A misses B implies comP . (A \/ B) = (comP . A) + (comP . B) ) assume A53: A misses B ; ::_thesis: comP . (A \/ B) = (comP . A) + (comP . B) reconsider A1 = A, B1 = B as Subset of Omega ; reconsider BSeq = (A1,B1) followed_by ({} Omega) as SetSequence of Omega ; A54: BSeq . 1 = B by FUNCT_7:123; A55: BSeq . 0 = A by FUNCT_7:122; for n being Nat holds BSeq . n in COM (Sigma,P) proof let n be Nat; ::_thesis: BSeq . n in COM (Sigma,P) percases ( n = 0 or n <> 0 ) ; suppose n = 0 ; ::_thesis: BSeq . n in COM (Sigma,P) hence BSeq . n in COM (Sigma,P) by A55; ::_thesis: verum end; suppose n <> 0 ; ::_thesis: BSeq . n in COM (Sigma,P) then n >= 1 by NAT_1:14; then A56: n + 1 > 1 by NAT_1:13; percases ( n > 1 or n = 1 ) by A56, NAT_1:22; suppose n > 1 ; ::_thesis: BSeq . n in COM (Sigma,P) then BSeq . n = {} by FUNCT_7:124; hence BSeq . n in COM (Sigma,P) by PROB_1:4; ::_thesis: verum end; suppose n = 1 ; ::_thesis: BSeq . n in COM (Sigma,P) hence BSeq . n in COM (Sigma,P) by A54; ::_thesis: verum end; end; end; end; end; then rng BSeq c= COM (Sigma,P) by NAT_1:52; then reconsider BSeq = BSeq as SetSequence of COM (Sigma,P) by RELAT_1:def_19; for m being Element of NAT st 2 <= m holds (Partial_Sums (comP * BSeq)) . m = (comP . A) + (comP . B) proof A57: (Partial_Sums (comP * BSeq)) . 0 = (comP * BSeq) . 0 by SERIES_1:def_1 .= comP . A by A55, FUNCT_2:15 ; 0 + 1 = 1 ; then A58: (Partial_Sums (comP * BSeq)) . 1 = ((Partial_Sums (comP * BSeq)) . 0) + ((comP * BSeq) . 1) by SERIES_1:def_1 .= (comP . A) + (comP . B) by A54, A57, FUNCT_2:15 ; A59: for n being Element of NAT holds (Partial_Sums (comP * BSeq)) . (2 + n) = (comP . A) + (comP . B) proof defpred S2[ Element of NAT ] means (Partial_Sums (comP * BSeq)) . (2 + \$1) = (comP . A) + (comP . B); A60: for k being Element of NAT st S2[k] holds S2[k + 1] proof let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] ) assume A61: S2[k] ; ::_thesis: S2[k + 1] A62: (2 + k) + 1 > 0 + 1 by XREAL_1:8; thus (Partial_Sums (comP * BSeq)) . (2 + (k + 1)) = ((Partial_Sums (comP * BSeq)) . (2 + k)) + ((comP * BSeq) . ((2 + k) + 1)) by SERIES_1:def_1 .= ((comP . A) + (comP . B)) + (comP . (BSeq . ((2 + k) + 1))) by A61, FUNCT_2:15 .= ((comP . A) + (comP . B)) + (comP . {}) by A62, FUNCT_7:124 .= (comP . A) + (comP . B) by A51 ; ::_thesis: verum end; 2 = 1 + 1 ; then (Partial_Sums (comP * BSeq)) . (2 + 0) = ((Partial_Sums (comP * BSeq)) . 1) + ((comP * BSeq) . 2) by SERIES_1:def_1 .= ((comP . A) + (comP . B)) + (comP . (BSeq . 2)) by A58, FUNCT_2:15 .= ((comP . A) + (comP . B)) + (comP . {}) by FUNCT_7:124 .= (comP . A) + (comP . B) by A51 ; then A63: S2[ 0 ] ; thus for k being Element of NAT holds S2[k] from NAT_1:sch_1(A63, A60); ::_thesis: verum end; let m be Element of NAT ; ::_thesis: ( 2 <= m implies (Partial_Sums (comP * BSeq)) . m = (comP . A) + (comP . B) ) assume 2 <= m ; ::_thesis: (Partial_Sums (comP * BSeq)) . m = (comP . A) + (comP . B) then consider k being Nat such that A64: m = 2 + k by NAT_1:10; k in NAT by ORDINAL1:def_12; hence (Partial_Sums (comP * BSeq)) . m = (comP . A) + (comP . B) by A59, A64; ::_thesis: verum end; then A65: ( Union BSeq = A \/ B & Sum (comP * BSeq) = (comP . A) + (comP . B) ) by DYNKIN:3, PROB_1:1; BSeq is V118() by A53, Th3; hence comP . (A \/ B) = (comP . A) + (comP . B) by A7, A65; ::_thesis: verum end; A66: for A, B being Event of COM (Sigma,P) st A c= B holds comP . (B \ A) = (comP . B) - (comP . A) proof let A, B be Event of COM (Sigma,P); ::_thesis: ( A c= B implies comP . (B \ A) = (comP . B) - (comP . A) ) assume A67: A c= B ; ::_thesis: comP . (B \ A) = (comP . B) - (comP . A) (comP . A) + (comP . (B \ A)) = comP . (A \/ (B \ A)) by A52, XBOOLE_1:79 .= comP . B by A67, XBOOLE_1:45 ; hence comP . (B \ A) = (comP . B) - (comP . A) ; ::_thesis: verum end; A68: for A, B being Event of COM (Sigma,P) st A c= B holds comP . A <= comP . B proof let A, B be Event of COM (Sigma,P); ::_thesis: ( A c= B implies comP . A <= comP . B ) assume A c= B ; ::_thesis: comP . A <= comP . B then comP . (B \ A) = (comP . B) - (comP . A) by A66; then 0 <= (comP . B) - (comP . A) by A48; then 0 + (comP . A) <= comP . B by XREAL_1:19; hence comP . A <= comP . B ; ::_thesis: verum end; A69: for BSeq being SetSequence of COM (Sigma,P) st BSeq is non-descending holds comP * BSeq is non-decreasing proof let BSeq be SetSequence of COM (Sigma,P); ::_thesis: ( BSeq is non-descending implies comP * BSeq is non-decreasing ) assume A70: BSeq is non-descending ; ::_thesis: comP * BSeq is non-decreasing for n, m being Element of NAT st n <= m holds (comP * BSeq) . n <= (comP * BSeq) . m proof let n, m be Element of NAT ; ::_thesis: ( n <= m implies (comP * BSeq) . n <= (comP * BSeq) . m ) assume n <= m ; ::_thesis: (comP * BSeq) . n <= (comP * BSeq) . m then BSeq . n c= BSeq . m by A70, PROB_1:def_5; then comP . (BSeq . n) <= comP . (BSeq . m) by A68; then (comP * BSeq) . n <= comP . (BSeq . m) by FUNCT_2:15; hence (comP * BSeq) . n <= (comP * BSeq) . m by FUNCT_2:15; ::_thesis: verum end; hence comP * BSeq is non-decreasing by SEQM_3:6; ::_thesis: verum end; A71: comP . Omega = comP . ({} \/ Omega) .= P . Omega by A5, A1, PROB_1:5 .= 1 by PROB_1:def_8 ; A72: for A being Event of COM (Sigma,P) holds comP . A <= 1 proof reconsider B = Omega as Event of COM (Sigma,P) by PROB_1:23; let A be Event of COM (Sigma,P); ::_thesis: comP . A <= 1 comP . A <= comP . B by A68; hence comP . A <= 1 by A71; ::_thesis: verum end; A73: for BSeq being SetSequence of COM (Sigma,P) for n being Element of NAT holds (comP * BSeq) . n <= 1 proof let BSeq be SetSequence of COM (Sigma,P); ::_thesis: for n being Element of NAT holds (comP * BSeq) . n <= 1 let n be Element of NAT ; ::_thesis: (comP * BSeq) . n <= 1 (comP * BSeq) . n = comP . (BSeq . n) by FUNCT_2:15; hence (comP * BSeq) . n <= 1 by A72; ::_thesis: verum end; A74: for BSeq being SetSequence of COM (Sigma,P) st BSeq is non-descending holds ( comP * BSeq is V101() & comP * BSeq is convergent ) proof let BSeq be SetSequence of COM (Sigma,P); ::_thesis: ( BSeq is non-descending implies ( comP * BSeq is V101() & comP * BSeq is convergent ) ) assume BSeq is non-descending ; ::_thesis: ( comP * BSeq is V101() & comP * BSeq is convergent ) then A75: comP * BSeq is non-decreasing by A69; for n being Element of NAT holds (comP * BSeq) . n < 2 proof let n be Element of NAT ; ::_thesis: (comP * BSeq) . n < 2 ((comP * BSeq) . n) + 0 < 1 + 1 by A73, XREAL_1:8; hence (comP * BSeq) . n < 2 ; ::_thesis: verum end; hence comP * BSeq is V101() by SEQ_2:def_3; ::_thesis: comP * BSeq is convergent hence comP * BSeq is convergent by A75; ::_thesis: verum end; for BSeq being SetSequence of COM (Sigma,P) st BSeq is non-descending holds ( comP * BSeq is convergent & lim (comP * BSeq) = comP . (Union BSeq) ) proof let BSeq be SetSequence of COM (Sigma,P); ::_thesis: ( BSeq is non-descending implies ( comP * BSeq is convergent & lim (comP * BSeq) = comP . (Union BSeq) ) ) assume A76: BSeq is non-descending ; ::_thesis: ( comP * BSeq is convergent & lim (comP * BSeq) = comP . (Union BSeq) ) reconsider CSeq = Partial_Diff_Union BSeq as SetSequence of COM (Sigma,P) ; A77: for n being Element of NAT holds (Partial_Sums (comP * CSeq)) . n = (comP * BSeq) . n proof defpred S2[ Element of NAT ] means (Partial_Sums (comP * CSeq)) . \$1 = (comP * BSeq) . \$1; A78: for k being Element of NAT st S2[k] holds S2[k + 1] proof let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] ) assume A79: S2[k] ; ::_thesis: S2[k + 1] A80: BSeq . k c= BSeq . (k + 1) by A76, PROB_2:7; thus (Partial_Sums (comP * CSeq)) . (k + 1) = ((comP * BSeq) . k) + ((comP * CSeq) . (k + 1)) by A79, SERIES_1:def_1 .= (comP . (BSeq . k)) + ((comP * CSeq) . (k + 1)) by FUNCT_2:15 .= (comP . (BSeq . k)) + (comP . (CSeq . (k + 1))) by FUNCT_2:15 .= comP . ((BSeq . k) \/ (CSeq . (k + 1))) by A52, A76, Th18 .= comP . ((BSeq . k) \/ ((BSeq . (k + 1)) \ (BSeq . k))) by A76, Th16 .= comP . ((BSeq . k) \/ (BSeq . (k + 1))) by XBOOLE_1:39 .= comP . (BSeq . (k + 1)) by A80, XBOOLE_1:12 .= (comP * BSeq) . (k + 1) by FUNCT_2:15 ; ::_thesis: verum end; (Partial_Sums (comP * CSeq)) . 0 = (comP * CSeq) . 0 by SERIES_1:def_1 .= comP . (CSeq . 0) by FUNCT_2:15 .= comP . (BSeq . 0) by A76, Th16 .= (comP * BSeq) . 0 by FUNCT_2:15 ; then A81: S2[ 0 ] ; thus for k being Element of NAT holds S2[k] from NAT_1:sch_1(A81, A78); ::_thesis: verum end; comP . (Union BSeq) = comP . (Union CSeq) by PROB_3:36 .= Sum (comP * CSeq) by A7 .= lim (Partial_Sums (comP * CSeq)) ; hence ( comP * BSeq is convergent & lim (comP * BSeq) = comP . (Union BSeq) ) by A74, A76, A77, FUNCT_2:63; ::_thesis: verum end; then reconsider comP = comP as Probability of COM (Sigma,P) by A48, A71, A52, PROB_2:10; take comP ; ::_thesis: for B being set st B in Sigma holds for C being thin of P holds comP . (B \/ C) = P . B thus for B being set st B in Sigma holds for C being thin of P holds comP . (B \/ C) = P . B by A5; ::_thesis: verum end; uniqueness for b1, b2 being Probability of COM (Sigma,P) st ( for B being set st B in Sigma holds for C being thin of P holds b1 . (B \/ C) = P . B ) & ( for B being set st B in Sigma holds for C being thin of P holds b2 . (B \/ C) = P . B ) holds b1 = b2 proof let P1, P2 be Probability of COM (Sigma,P); ::_thesis: ( ( for B being set st B in Sigma holds for C being thin of P holds P1 . (B \/ C) = P . B ) & ( for B being set st B in Sigma holds for C being thin of P holds P2 . (B \/ C) = P . B ) implies P1 = P2 ) assume that A82: for B being set st B in Sigma holds for C being thin of P holds P1 . (B \/ C) = P . B and A83: for B being set st B in Sigma holds for C being thin of P holds P2 . (B \/ C) = P . B ; ::_thesis: P1 = P2 for x being set st x in COM (Sigma,P) holds P1 . x = P2 . x proof let x be set ; ::_thesis: ( x in COM (Sigma,P) implies P1 . x = P2 . x ) assume x in COM (Sigma,P) ; ::_thesis: P1 . x = P2 . x then consider B being set such that A84: ( B in Sigma & ex C being thin of P st x = B \/ C ) by Def5; P1 . x = P . B by A82, A84 .= P2 . x by A83, A84 ; hence P1 . x = P2 . x ; ::_thesis: verum end; hence P1 = P2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def8 defines COM PROB_4:def_8_:_ for Omega being non empty set for Sigma being SigmaField of Omega for P being Probability of Sigma for b4 being Probability of COM (Sigma,P) holds ( b4 = COM P iff for B being set st B in Sigma holds for C being thin of P holds b4 . (B \/ C) = P . B ); theorem :: PROB_4:37 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 let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for P being Probability of Sigma holds COM P = COM (P2M P) let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma holds COM P = COM (P2M P) let P be Probability of Sigma; ::_thesis: COM P = COM (P2M P) set Y = COM P; COM (Sigma,P) = COM (Sigma,(P2M P)) by Th27; then reconsider Y1 = P2M (COM P) as sigma_Measure of (COM (Sigma,(P2M P))) ; for B being set st B in Sigma holds for C being thin of P2M P holds Y1 . (B \/ C) = (P2M P) . B proof let B be set ; ::_thesis: ( B in Sigma implies for C being thin of P2M P holds Y1 . (B \/ C) = (P2M P) . B ) assume A1: B in Sigma ; ::_thesis: for C being thin of P2M P holds Y1 . (B \/ C) = (P2M P) . B let C be thin of P2M P; ::_thesis: Y1 . (B \/ C) = (P2M P) . B reconsider C1 = C as thin of P by Th23; (COM P) . (B \/ C1) = P . B by A1, Def8; hence Y1 . (B \/ C) = (P2M P) . B ; ::_thesis: verum end; hence COM P = COM (P2M P) by MEASURE3:def_5; ::_thesis: verum end; 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 is_complete COM (Sigma,P) proof let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for P being Probability of Sigma holds COM P is_complete COM (Sigma,P) let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma holds COM P is_complete COM (Sigma,P) let P be Probability of Sigma; ::_thesis: COM P is_complete COM (Sigma,P) for A being Subset of Omega for B being set st B in COM (Sigma,P) & A c= B & (COM P) . B = 0 holds A in COM (Sigma,P) proof let A be Subset of Omega; ::_thesis: for B being set st B in COM (Sigma,P) & A c= B & (COM P) . B = 0 holds A in COM (Sigma,P) let B be set ; ::_thesis: ( B in COM (Sigma,P) & A c= B & (COM P) . B = 0 implies A in COM (Sigma,P) ) assume A1: B in COM (Sigma,P) ; ::_thesis: ( not A c= B or not (COM P) . B = 0 or A in COM (Sigma,P) ) assume that A2: A c= B and A3: (COM P) . B = 0 ; ::_thesis: A in COM (Sigma,P) ex B1 being set st ( B1 in Sigma & ex C1 being thin of P st A = B1 \/ C1 ) proof take {} ; ::_thesis: ( {} in Sigma & ex C1 being thin of P st A = {} \/ C1 ) consider B2 being set such that A4: B2 in Sigma and A5: ex C2 being thin of P st B = B2 \/ C2 by A1, Def5; A6: P . B2 = 0 by A3, A4, A5, Def8; consider C2 being thin of P such that A7: B = B2 \/ C2 by A5; set C1 = (A /\ B2) \/ (A /\ C2); consider D2 being set such that A8: D2 in Sigma and A9: C2 c= D2 and A10: P . D2 = 0 by Def4; set O = B2 \/ D2; A /\ C2 c= C2 by XBOOLE_1:17; then A11: ( A /\ B2 c= B2 & A /\ C2 c= D2 ) by A9, XBOOLE_1:1, XBOOLE_1:17; ex O being set st ( O in Sigma & (A /\ B2) \/ (A /\ C2) c= O & P . O = 0 ) proof reconsider B2 = B2, D2 = D2 as Element of Sigma by A4, A8; take B2 \/ D2 ; ::_thesis: ( B2 \/ D2 in Sigma & (A /\ B2) \/ (A /\ C2) c= B2 \/ D2 & P . (B2 \/ D2) = 0 ) P . (B2 \/ D2) <= 0 + 0 by A6, A10, PROB_1:39; hence ( B2 \/ D2 in Sigma & (A /\ B2) \/ (A /\ C2) c= B2 \/ D2 & P . (B2 \/ D2) = 0 ) by A11, PROB_1:def_8, XBOOLE_1:13; ::_thesis: verum end; then A12: (A /\ B2) \/ (A /\ C2) is thin of P by Def4; A = A /\ (B2 \/ C2) by A2, A7, XBOOLE_1:28 .= {} \/ ((A /\ B2) \/ (A /\ C2)) by XBOOLE_1:23 ; hence ( {} in Sigma & ex C1 being thin of P st A = {} \/ C1 ) by A12, PROB_1:4; ::_thesis: verum end; hence A in COM (Sigma,P) by Def5; ::_thesis: verum end; hence COM P is_complete COM (Sigma,P) by Def3; ::_thesis: verum end; theorem Th39: :: PROB_4:39 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 let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for P being Probability of Sigma for A being Event of Sigma holds P . A = (COM P) . A let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma for A being Event of Sigma holds P . A = (COM P) . A let P be Probability of Sigma; ::_thesis: for A being Event of Sigma holds P . A = (COM P) . A reconsider C = {} as thin of P by Th24; let A be Event of Sigma; ::_thesis: P . A = (COM P) . A thus P . A = (COM P) . (A \/ C) by Def8 .= (COM P) . A ; ::_thesis: verum end; theorem Th40: :: PROB_4:40 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 let Omega be non empty set ; ::_thesis: for Sigma being SigmaField of Omega for P being Probability of Sigma for C being thin of P holds (COM P) . C = 0 let Sigma be SigmaField of Omega; ::_thesis: for P being Probability of Sigma for C being thin of P holds (COM P) . C = 0 let P be Probability of Sigma; ::_thesis: for C being thin of P holds (COM P) . C = 0 let C be thin of P; ::_thesis: (COM P) . C = 0 consider A being set such that A1: A in Sigma and A2: C c= A and A3: P . A = 0 by Def4; reconsider A = A as Event of Sigma by A1; A4: (COM P) . A = 0 by A3, Th39; Sigma c= COM (Sigma,P) by Th28; then reconsider A = A as Event of COM (Sigma,P) by A1; (COM P) . C <= (COM P) . A by A2, PROB_1:34; hence (COM P) . C = 0 by A4, PROB_1:def_8; ::_thesis: verum end; theorem :: PROB_4:41 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 let Omega be non empty set ; ::_thesis: 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 let Sigma be SigmaField of Omega; ::_thesis: 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 let P be Probability of Sigma; ::_thesis: for A being Element of COM (Sigma,P) for B being set st B in ProbPart A holds P . B = (COM P) . A let A be Element of COM (Sigma,P); ::_thesis: for B being set st B in ProbPart A holds P . B = (COM P) . A let B be set ; ::_thesis: ( B in ProbPart A implies P . B = (COM P) . A ) assume A1: B in ProbPart A ; ::_thesis: P . B = (COM P) . A reconsider C = A \ B as thin of P by A1, Def7; A2: B in Sigma by A1, Def7; B c= A by A1, Def7; then A3: A = B \/ C by XBOOLE_1:45; Sigma c= COM (Sigma,P) by Th28; then reconsider B = B as Event of COM (Sigma,P) by A2; reconsider A = A as Event of COM (Sigma,P) ; B misses C by XBOOLE_1:79; then A4: (COM P) . A = ((COM P) . B) + ((COM P) . C) by A3, PROB_1:def_8 .= ((COM P) . B) + 0 by Th40 .= (COM P) . B ; reconsider B = B as Event of Sigma by A1, Def7; (COM P) . A = P . B by A4, Th39; hence P . B = (COM P) . A ; ::_thesis: verum end;