:: The Relevance of Measure and Probability and Definition of Completeness
:: of Probability
:: by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received November 23, 2005
:: Copyright (c) 2005-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, PROB_1, XBOOLE_0, TARSKI, FUNCT_1, RELAT_1,
NAT_1, PROB_2, FUNCOP_1, FUNCT_7, CARD_1, XXREAL_0, ARYTM_3, ZFMISC_1,
CARD_3, EQREL_1, RPR_1, ARYTM_1, SERIES_1, SEQ_2, ORDINAL2, PROB_3,
SUPINF_2, REAL_1, XXREAL_2, SUPINF_1, MEASURE1, VALUED_0, SETFAM_1,
MEASURE3, PROB_4, SEQ_4, REWRITE1;
notations TARSKI, XBOOLE_0, XREAL_0, CARD_3, ORDINAL1, MEASURE3, SUPINF_2,
XXREAL_0, XXREAL_2,
XXREAL_3, XCMPLX_0, NAT_1, SEQ_2, SETFAM_1, FUNCT_1, RELSET_1,
SUBSET_1, NUMBERS, SUPINF_1, PARTFUN1, FUNCT_2, FUNCT_7, PROB_1, PROB_3,
MEASURE1, FUNCOP_1, SEQM_3, SERIES_1, RINFSUP1, ZFMISC_1, MEASURE6,
PROB_2;
constructors REAL_1, SERIES_1, MEASURE3, MEASURE6, PARTFUN3, KURATO_0,
RINFSUP1, PROB_3, SUPINF_1, FUNCT_7, RELSET_1, COMSEQ_2;
registrations SUBSET_1, RELAT_1, ORDINAL1, FUNCT_2, NUMBERS, XREAL_0, NAT_1,
MEMBERED, MEASURE1, MEASURE3, VALUED_0, SEQ_2, SEQ_4, FUNCT_7, PROB_1,
RELSET_1, PROB_3;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0, PROB_3;
equalities XBOOLE_0, SERIES_1, SUBSET_1, SUPINF_2;
expansions TARSKI, XBOOLE_0, SERIES_1, PROB_3, FUNCT_2;
theorems FUNCT_1, FUNCT_2, SEQ_1, SEQ_2, XREAL_1, NAT_1, TARSKI, XBOOLE_0,
XBOOLE_1, PROB_2, RINFSUP1, SUPINF_2, SEQM_3, CARD_3, SETLIM_1, PROB_1,
SERIES_1, PROB_3, MEASURE1, MEASURE3, ZFMISC_1, XXREAL_0, ORDINAL1,
NUMBERS, XXREAL_2, FUNCT_7, DYNKIN, VALUED_0, FUNCOP_1, RELAT_1, XREAL_0;
schemes FUNCT_2, NAT_1, XFAMILY;
begin
reserve n,m,k for Element of NAT,
x,X for set,
A1 for SetSequence of X,
Si for SigmaField of X,
XSeq for SetSequence of Si;
reserve Omega for non empty set,
Sigma for SigmaField of Omega,
ASeq for SetSequence of Sigma,
P for Probability of Sigma;
Lm1: for A,B,C being set holds C c= B implies A \ C = (A \ B) \/ (A /\ (B \ C)
)
proof
let A,B,C be set;
assume
A1: C c= B;
thus A \ C c= (A \ B) \/ (A /\ (B \ C))
proof
let x be object;
assume x in A \ 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 thesis by XBOOLE_0:def 3;
end;
let x be object;
assume x in (A \ B) \/ (A /\ (B \ 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 thesis by A2,XBOOLE_0:def 5;
end;
definition
let X,Si,XSeq,n;
redefine func XSeq.n -> Element of Si; :: redefines . (FUNCT_1, definition)
coherence
proof
thus XSeq.n is Element of Si;
end;
end;
theorem Th1:
rng XSeq c= Si
proof
let x be object;
assume x in rng XSeq;
then ex n being Nat st x = XSeq.n by SETLIM_1:4;
hence thesis;
end;
theorem Th2:
for f being Function holds f is SetSequence of Si iff f is sequence of Si
proof
let f be Function;
thus f is SetSequence of Si implies f is sequence of Si
proof
assume f is SetSequence of Si;
then reconsider f as SetSequence of Si;
rng f c= Si & dom f = NAT by Th1,FUNCT_2:def 1;
hence thesis by FUNCT_2:2;
end;
assume
A1: f is sequence of Si;
then reconsider f as SetSequence of X by FUNCT_2:7;
f is SetSequence of Si by A1;
hence thesis;
end;
scheme
LambdaSigmaSSeq { X() -> set, Si() -> SigmaField of X(), F(set) -> Element
of Si() } : ex f being SetSequence of Si() st for n holds f.n = F(n) proof
ex f being SetSequence of X() st for n holds f.n = F(n) from FUNCT_2:sch
4;
then consider f be SetSequence of X() such that
A1: for n holds f.n = F(n);
for n being Nat holds f.n in Si()
proof
let n be Nat;
n in NAT by ORDINAL1:def 12;
then f.n = F(n) by A1;
hence thesis;
end;
then rng f c= Si() by NAT_1:52;
then reconsider f as SetSequence of Si() by RELAT_1:def 19;
take f;
thus thesis by A1;
end;
registration
let X;
cluster disjoint_valued for SetSequence of X;
existence
proof
take A1 = NAT --> {}X;
for m,n being Nat st m <> n holds A1.m misses A1.n
proof
let m,n be Nat;
m in NAT by ORDINAL1:def 12;
then A1.m = {} by FUNCOP_1:7;
hence thesis;
end;
hence thesis;
end;
end;
registration
let X,Si;
cluster disjoint_valued for SetSequence of Si;
existence
proof
reconsider MSi = Si as SigmaField of X;
set f = the disjoint_valued sequence of MSi;
reconsider f as SetSequence of Si by Th2;
take f;
thus thesis;
end;
end;
theorem Th3:
for A, B being Subset of X st A misses B holds (A,B) followed_by
{} is disjoint_valued
proof
let A,B be Subset of X;
reconsider A1 = (A,B) followed_by {}X as SetSequence of X;
assume
A1: A misses B;
A1 is disjoint_valued
proof
A2: A1.1 = B by FUNCT_7:123;
let m,n be Nat such that
A3: m <> n;
A4: A1.0 = A by FUNCT_7:122;
per cases;
suppose
A5: m = 0;
then n >= 1 by A3,NAT_1:14;
then
A6: n + 1 > 1 by NAT_1:13;
per cases by A6,NAT_1:22;
suppose
n > 1;
then A1.n = {} by FUNCT_7:124;
hence thesis;
end;
suppose
n = 1;
hence thesis by A1,A4,A5,FUNCT_7:123;
end;
end;
suppose
A7: m <> 0 & m = 1;
n >= 1 or n <= 1;
then
A8: n + 1 > 1 or n < 1 + 1 by NAT_1:13;
per cases by A3,A7,A8,NAT_1:14,22;
suppose
n > 1;
then A1.n = {} by FUNCT_7:124;
hence thesis;
end;
suppose
n = 0;
hence thesis by A1,A4,A2,A7;
end;
end;
suppose
A9: m <> 0 & m <> 1;
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 thesis;
end;
end;
hence thesis;
end;
theorem Th4:
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 S be non empty set;
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
proof
assume S is SigmaField of X;
then reconsider 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;
assume rng A1 c= S;
then reconsider A1 as SetSequence of S by RELAT_1:def 19;
Union A1 in S by PROB_1:17;
hence thesis;
end;
hence thesis by PROB_1:15;
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;
for A1 being SetSequence of X st rng A1 c= S holds Intersection A1 in S
proof
let A1 be SetSequence of X such that
A4: rng A1 c= S;
for n being Nat holds (Complement A1).n in S
proof
let n be Nat;
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 thesis by PROB_1:def 2;
end;
then rng Complement A1 c= S by NAT_1:52;
then (Union Complement A1)` in S by A2,A3;
hence thesis by PROB_1:def 3;
end;
hence thesis by A1,A3,PROB_1:15;
end;
theorem Th5:
for A,B being Event of Sigma holds P.(A \ B) = P.(A \/ B) - P.B
proof
let A,B be Event of Sigma;
P.(A \/ B) - P.B = P.B + P.(A \ B) - P.B by PROB_1:36;
hence thesis;
end;
theorem Th6:
for A,B being Event of Sigma st A c= B & P.B = 0 holds P.A = 0
proof
let A,B be Event of Sigma;
assume A c= B & P.B = 0;
then P.A <= 0 by PROB_1:34;
hence thesis by PROB_1:def 8;
end;
theorem Th7:
(for n holds P.(ASeq.n) = 0) iff P.(Union ASeq) = 0
proof
hereby
assume
A1: for n holds P.(ASeq.n) = 0;
for n being Nat holds Partial_Sums(P * ASeq).n = 0
proof
defpred P[Nat] means Partial_Sums(P * ASeq).$1 = 0;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A3: P[k];
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;
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: P[0];
thus for k being Nat holds P[k] from NAT_1:sch 2(A4,A2);
end;
then for n being 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
let n be Nat;
(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;
end;
then
A6: for n being 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;
end;
assume
A8: P.(Union ASeq) = 0;
hereby
reconsider Y2 = Union ASeq as Event of Sigma by PROB_1:26;
let n;
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;
end;
end;
theorem Th8:
(for A being set st A in rng ASeq holds P.A = 0) iff P.(union rng ASeq) = 0
proof
hereby
assume
A1: for A being set st A in rng ASeq holds P.A = 0;
for n holds P.(ASeq.n) = 0
by SETLIM_1:4,A1;
then P.(Union ASeq) = 0 by Th7;
hence P.(union rng ASeq) = 0 by CARD_3:def 4;
end;
assume P.(union rng ASeq) = 0;
then
A2: P.(Union ASeq) = 0 by CARD_3:def 4;
hereby
let A be set;
assume A in rng ASeq;
then consider n1 being Nat such that
A3: A = ASeq.n1 by SETLIM_1:4;
n1 in NAT by ORDINAL1:def 12;
hence P.A = 0 by A2,Th7,A3;
end;
end;
theorem Th9:
for seq being sequence of REAL, Eseq being sequence of
ExtREAL st seq = Eseq holds Partial_Sums seq = Ser Eseq
proof
let seq be sequence of REAL, Eseq be sequence of ExtREAL such that
A1: seq = Eseq;
reconsider Ps = Partial_Sums seq as sequence of ExtREAL by FUNCT_2:7
,NUMBERS:31;
defpred P[Nat] means Ps.$1 = (Ser Eseq).$1;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A3: Ps.k = (Ser Eseq).k;
reconsider Psk = Ps.k as Real;
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
Ps.(k+1) = Psk + seq.(k+1) & (Ser Eseq).(k+1)
= (Ser Eseq).kk + Eseq.(kk+1) by SERIES_1:def 1,SUPINF_2:def 11;
hence thesis by A1,A3,SUPINF_2:1;
end;
Ps.0 = Eseq.0 by A1,SERIES_1:def 1
.= (Ser Eseq).0 by SUPINF_2:def 11;
then
A4: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
theorem Th10:
for seq being sequence of REAL, Eseq being sequence of
ExtREAL st seq = Eseq & seq is bounded_above
holds upper_bound seq = sup rng Eseq
proof
let seq be sequence of REAL, Eseq be sequence of ExtREAL such that
A1: seq = Eseq and
A2: seq is bounded_above;
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};
then reconsider k1 = -infty as Element of rng Eseq by TARSKI:def 1;
consider n1 being object such that
A5: n1 in NAT and
Eseq.n1 = k1 by A3,FUNCT_1:def 3;
reconsider n1 as Element of NAT by A5;
seq.n1 = k1 by A1;
hence contradiction;
end;
for x being ExtReal holds x in rng Eseq implies x <= s
proof
let x be ExtReal;
assume x in rng Eseq;
then ex n1 being object st n1 in NAT & Eseq.n1 = x by A3,FUNCT_1:def 3;
hence thesis by A1,A2,RINFSUP1:7;
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 Element of REAL by A7,A4,XXREAL_2:57;
A9: sup rng Eseq is UpperBound of rng Eseq by XXREAL_2:def 3;
for n being Nat holds seq.n <= r1
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A1,A3,FUNCT_1:3,XXREAL_2:def 1,A9;
end;
hence thesis by RINFSUP1:9;
end;
sup rng Eseq <= s by A6,XXREAL_2:def 3;
hence thesis by A8,XXREAL_0:1;
end;
theorem Th11:
for seq being sequence of REAL, Eseq being sequence of
ExtREAL st seq = Eseq & seq is bounded_below
holds lower_bound seq = inf rng Eseq
proof
let seq be sequence of REAL, Eseq be sequence of ExtREAL such that
A1: seq = Eseq and
A2: seq is bounded_below;
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};
then reconsider k1 = +infty as Element of rng Eseq by TARSKI:def 1;
consider n1 being object such that
A5: n1 in NAT and
Eseq.n1 = k1 by A3,FUNCT_1:def 3;
reconsider n1 as Element of NAT by A5;
seq.n1 = k1 by A1;
hence contradiction;
end;
for x being ExtReal holds x in rng Eseq implies s <= x
proof
let x be ExtReal;
assume x in rng Eseq;
then ex n1 being object st n1 in NAT & Eseq.n1 = x by A3,FUNCT_1:def 3;
hence thesis by A1,A2,RINFSUP1:8;
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 Element of REAL by A7,A4,XXREAL_2:58;
A9: inf rng Eseq is LowerBound of rng Eseq by XXREAL_2:def 4;
for n being Nat holds r1 <= seq.n
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A1,A3,FUNCT_1:3,XXREAL_2:def 2,A9;
end;
hence thesis by RINFSUP1:10;
end;
s <= inf rng Eseq by A6,XXREAL_2:def 4;
hence thesis by A8,XXREAL_0:1;
end;
theorem Th12:
for seq being sequence of REAL, Eseq being sequence of
ExtREAL st seq = Eseq & seq is nonnegative summable holds Sum seq = SUM Eseq
proof
let seq be sequence of REAL, Eseq be sequence of ExtREAL such that
A1: seq = Eseq and
A2: seq is nonnegative summable;
A3: for n being Nat holds seq.n >= 0 by A2,RINFSUP1:def 3;
Partial_Sums seq is convergent by A2;
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;
hence thesis by A4,A3,RINFSUP1:24,SERIES_1:16;
end;
theorem Th13:
P is sigma_Measure of Sigma
proof
set Z = Sigma;
reconsider P1 = P as Function of Z,ExtREAL by FUNCT_2:7,NUMBERS:31;
for x being ExtReal holds x in rng P1 implies 0. <= x
proof
let x be ExtReal;
assume
A1: x in rng P1;
dom P1 = Sigma by FUNCT_2:def 1;
then consider y being object 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 thesis by A3;
end;
then
A4: rng P1 is nonnegative by SUPINF_2:def 9;
for F being Sep_Sequence of Z holds SUM(P1 * F) = P1.(union rng F)
proof
let F be Sep_Sequence of Z;
reconsider F2=F as disjoint_valued SetSequence of Sigma by Th2;
for n being 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;
then P.(Union F2) = Sum(P * F2) & Sum(P * F2) = SUM(P1 * F) by A5,Th12,
PROB_3:46;
hence thesis by CARD_3:def 4;
end;
hence thesis by A4,MEASURE1:def 6,SUPINF_2:def 12;
end;
definition
let Omega,Sigma,P;
func P2M(P) -> sigma_Measure of Sigma equals
P;
coherence by Th13;
end;
theorem Th14:
for X being non empty set, S being SigmaField of X, M being
sigma_Measure of S st M.X = 1 holds M is Probability of S
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S such
that
A1: M.X = 1;
A2: for A being Element of S holds M.A <= 1
proof
reconsider X as Element of S by PROB_1:5;
let A be Element of S;
M.A <= M.X by MEASURE1:31;
hence thesis by A1;
end;
A3: for x being object st x in S holds M.x in REAL
proof
let x be object;
assume x in S;
then reconsider x as Element of S;
A4: 1 in REAL & 0 in REAL by XREAL_0:def 1;
0. <= M.x & M.x <= 1 by A2,MEASURE1:def 2;
hence thesis by A4,XXREAL_0:45;
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 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 such that
A6: ASeq is non-ascending;
for n being Nat holds 0 <= (P1 * ASeq).n
proof
let n be Nat;
A7: n in NAT by ORDINAL1:def 12;
reconsider A = ASeq.n as Event of S;
0 <= P1.A & dom (P1 * ASeq) = NAT by MEASURE1:def 2,SEQ_1:1;
hence thesis by FUNCT_1:12,A7;
end;
then
A8: P1*ASeq is bounded_below by RINFSUP1:10;
reconsider F = ASeq as sequence of S by Th2;
A9: for n being Nat holds F.(n+1) c= F.n by A6,PROB_2:6;
A10: M.(F.0) <+infty by A3,XXREAL_0:9;
now
let n be Nat;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
dom (M*F) = NAT by FUNCT_2:def 1;
then
A11: (M*F).nn = M.(F.nn) & (M*F).(nn+1) = M.(F.(nn+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 A11,MEASURE1:31;
end;
then
A12: P1*ASeq is non-increasing by SEQM_3:def 9;
then lim (P1*ASeq) = lower_bound (P1*ASeq) by A8,RINFSUP1:25
.= inf(rng (M*F)) by A8,Th11;
then lim (P1 * ASeq) = M.(meet rng F) by A9,A10,MEASURE3:12
.= P1.Intersection ASeq by SETLIM_1:8;
hence thesis by A8,A12;
end;
A13: 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 such that
A14: A misses B;
reconsider A, B as Element of S;
reconsider A2 = A, B2 = B as Element of S;
P1.(A \/ B) = M.A2 + M.B2 by A14,MEASURE1:30
.= P1.A + P1.B by SUPINF_2:1;
hence thesis;
end;
( for A being Event of S holds 0 <= P1.A)& P1.X = 1 by A1,MEASURE1:def 2;
hence thesis by A13,A5,PROB_1:def 8;
end;
definition
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S;
assume
A1: M.X = 1;
func M2P(M) -> Probability of S equals
M;
coherence by A1,Th14;
end;
Lm2: A1 is non-descending implies
for n being Nat holds (Partial_Union A1).n = A1.n
proof
defpred P[Nat] means (Partial_Union A1).$1 = A1.$1;
assume
A1: A1 is non-descending;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A3: P[k];
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;
end;
A5: P[0] by PROB_3:def 2;
thus for k being Nat holds P[k] from NAT_1:sch 2(A5,A2);
end;
theorem Th15:
A1 is non-descending implies Partial_Union A1 = A1
by Lm2;
theorem Th16:
A1 is non-descending implies (Partial_Diff_Union A1).0 = A1.0 &
for n being Nat holds (Partial_Diff_Union A1).(n+1) = A1.(n+1) \ A1.n
proof
assume
A1: A1 is non-descending;
thus (Partial_Diff_Union A1).0 = A1.0 by PROB_3:def 3;
let n be Nat;
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;
end;
theorem
A1 is non-descending implies for n holds A1.(n+1) = (
Partial_Diff_Union A1).(n+1) \/ A1.n
proof
assume
A1: A1 is non-descending;
thus for n holds A1.(n+1) = (Partial_Diff_Union A1).(n+1) \/ A1.n
proof
let 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;
end;
end;
theorem Th18:
A1 is non-descending implies
for n being Nat holds (Partial_Diff_Union A1).(n+1) misses A1.n
proof
assume
A1: A1 is non-descending;
let n be Nat;
(Partial_Diff_Union A1).(n+1) = A1.(n+1) \ A1.n by A1,Th16;
hence thesis by XBOOLE_1:79;
end;
theorem
XSeq is non-descending implies Partial_Union XSeq = XSeq by Th15;
theorem
XSeq is non-descending implies (Partial_Diff_Union XSeq).0 = XSeq.0 &
for n holds (Partial_Diff_Union XSeq).(n+1) = XSeq.(n+1) \ XSeq.n by Th16;
theorem
XSeq is non-descending implies for n holds (Partial_Diff_Union XSeq).
(n+1) misses XSeq.n by Th18;
definition
let Omega,Sigma,P;
attr P is complete means
for A being Subset of Omega
for B being set st B in Sigma holds (A c= B & P.B=0 implies A in Sigma);
end;
theorem
P is complete iff P2M(P) is complete by MEASURE3:def 1;
definition
let Omega,Sigma,P;
mode thin of P -> Subset of Omega means :Def4:
ex A being set st A in Sigma & it c= A & P.A = 0;
existence
proof
reconsider B = {} as Subset of Omega by XBOOLE_1:2;
take B;
take A={};
thus A in Sigma by PROB_1:4;
thus B c= A;
thus thesis by VALUED_0:def 19;
end;
end;
theorem Th23:
for Y being Subset of Omega holds Y is thin of P iff Y is thin of P2M(P)
proof
let Y be Subset of Omega;
hereby
assume Y is thin of P;
then ex A be set st A in Sigma & Y c= A & P.A = 0 by Def4;
hence Y is thin of P2M(P) by MEASURE3:def 2;
end;
assume Y is thin of P2M(P);
then ex B be set st B in Sigma & Y c= B & (P2M(P)).B = 0. by MEASURE3:def 2;
hence thesis by Def4;
end;
theorem Th24:
{} is thin of P
proof
P.{} = 0 & {} in Sigma by PROB_1:4,VALUED_0:def 19;
hence thesis by Def4;
end;
theorem Th25:
for B1,B2 being set st B1 in Sigma & B2 in Sigma holds for C1,C2
being thin of P holds B1 \/ C1 = B2 \/ C2 implies P.B1 = P.B2
proof
let B1,B2 be set;
assume
A1: B1 in Sigma & B2 in Sigma;
let C1,C2 be thin of P;
assume
A2: B1 \/ C1 = B2 \/ C2;
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,B2,D1,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 thesis by A14,XXREAL_0:1;
end;
definition
let Omega,Sigma,P;
func COM(Sigma,P) -> non empty Subset-Family of Omega means
:Def5:
for A
being set holds A in it iff ex B being set st B in Sigma & ex C being thin of P
st A = B \/ C;
existence
proof
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;
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 = {};
then A = B \/ C by A3,A5;
hence thesis by A4;
end;
defpred P[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 & P[y] from
XFAMILY: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;
A8: A in D iff (A in bool Omega & for y being set holds (y = A implies
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);
then A c= Omega by XBOOLE_1:8;
hence thesis by A8,A9;
end;
hence thesis by A6;
end;
A10: D c= bool Omega
by A6;
{} c= Omega;
then reconsider D as non empty Subset-Family of Omega by A6,A10,A2;
take D;
thus thesis by A7;
end;
uniqueness
proof
let D1,D2 be non empty Subset-Family of Omega such 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) );
for A being object holds A in D1 iff A in D2
proof
let A be object;
thus A in D1 implies A in D2
proof
assume A in D1;
then ex B being set st (B in Sigma & ex C being thin of P st A = B \/
C) by A11;
hence thesis by A12;
end;
assume A in D2;
then
ex B being set st (B in Sigma & ex C being thin of P st A = B \/ C)
by A12;
hence thesis by A11;
end;
hence thesis by TARSKI:2;
end;
end;
theorem Th26:
for C being thin of P holds C in COM(Sigma,P)
proof
let C be thin of P;
reconsider B = {} as Element of Sigma by PROB_1:4;
B \/ C in COM(Sigma,P) by Def5;
hence thesis;
end;
theorem Th27:
COM(Sigma,P) = COM(Sigma,P2M P)
proof
A1: COM( Sigma,P2M P) c= COM(Sigma,P)
proof
let x be object;
assume x in COM( Sigma,P2M 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 thesis by A2,Def5;
end;
COM(Sigma,P) c= COM(Sigma,P2M P)
proof
let x be object;
assume x in COM(Sigma,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 thesis by A5,MEASURE3:def 3;
end;
hence thesis by A1;
end;
definition
let Omega,Sigma,P;
let A be Element of COM(Sigma,P);
func P_COM2M_COM(A) -> Element of COM(Sigma,P2M(P)) equals
A;
correctness by Th27;
end;
theorem Th28:
Sigma c= COM(Sigma,P)
proof
reconsider C={} as thin of P by Th24;
let A be object such that
A1: A in Sigma;
reconsider AA=A as set by TARSKI:1;
A = AA \/ C;
hence thesis by A1,Def5;
end;
definition
let Omega,Sigma,P;
let A be Element of COM(Sigma,P);
func ProbPart(A) -> non empty Subset-Family of Omega means
:Def7:
for B
being set holds (B in it iff B in Sigma & B c= A & A \ B is thin of P );
existence
proof
defpred P[set] means for t being set holds t = $1 implies 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 & P[t] from
XFAMILY: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;
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;
for t being set holds t = B implies t in Sigma & t c= A & A \ t is
thin of P by A3,A4;
hence thesis by A1,A3;
end;
hence thesis by A1;
end;
A5: D c= bool Omega
proof
let B be object;
assume B in D;
then B in Sigma by A2;
hence thesis;
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;
then
A12: A \ B is thin of P by A9,A11,Def4;
B c= A by A8,XBOOLE_1:7;
hence thesis by A2,A6,A12;
end;
then reconsider D as non empty Subset-Family of Omega by A5;
take D;
thus thesis by A2;
end;
uniqueness
proof
let D1,D2 be non empty Subset-Family of Omega such 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;
for B being object holds B in D1 iff B in D2
proof
let B be object;
reconsider BB=B as set by TARSKI:1;
thus B in D1 implies B in D2
proof
assume
A15: B in D1;
then
A16: A \ BB is thin of P by A13;
B in Sigma & BB c= A by A13,A15;
hence thesis by A14,A16;
end;
assume
A17: B in D2;
then
A18: A \ BB is thin of P by A14;
B in Sigma & BB c= A by A14,A17;
hence thesis by A13,A18;
end;
hence thesis by TARSKI:2;
end;
end;
theorem
for A being Element of COM(Sigma,P) holds ProbPart(A) = MeasPart(
P_COM2M_COM(A))
proof
let A be Element of COM(Sigma,P);
A1: MeasPart(P_COM2M_COM(A)) c= ProbPart(A)
proof
let x be object such that
A2: x in MeasPart(P_COM2M_COM A);
reconsider xx=x as set by TARSKI:1;
P_COM2M_COM(A) \ xx is thin of P2M(P) by A2,MEASURE3:def 4;
then
A3: A \ xx is thin of P by Th23;
x in Sigma & xx c= P_COM2M_COM(A) by A2,MEASURE3:def 4;
hence thesis by A3,Def7;
end;
ProbPart(A) c= MeasPart(P_COM2M_COM(A))
proof
let x be object such that
A4: x in ProbPart(A);
reconsider xx=x as set by TARSKI:1;
A \ xx is thin of P by A4,Def7;
then
A5: P_COM2M_COM(A) \ xx is thin of P2M(P) by Th23;
x in Sigma & xx c= A by A4,Def7;
hence thesis by A5,MEASURE3:def 4;
end;
hence thesis by A1;
end;
theorem
for A being Element of COM(Sigma,P) holds for A1,A2 being set st A1 in
ProbPart(A) & A2 in ProbPart(A) holds P.A1 = P.A2
proof
let A be Element of COM(Sigma,P);
let A1,A2 be set such that
A1: A1 in ProbPart(A) and
A2: A2 in ProbPart(A);
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 thesis by A4,Th25;
end;
theorem Th31:
for F being sequence of COM(Sigma,P) holds ex BSeq being
SetSequence of Sigma st for n holds BSeq.n in ProbPart(F.n)
proof
let F be sequence of COM(Sigma,P);
defpred P[Element of NAT, set] means for n being Element of NAT for y being
set holds (n = $1 & y = $2 implies y in ProbPart(F.n));
A1: for t being Element of NAT ex A being Element of Sigma st P[t,A]
proof
let t be Element of NAT;
set A = the Element of ProbPart(F.t);
reconsider A as Element of Sigma by Def7;
take A;
thus thesis;
end;
ex G being sequence of Sigma st for t being Element of NAT holds P[t
,G.t] from FUNCT_2:sch 3(A1);
then consider G being sequence of Sigma such that
A2: for t being Element of NAT holds for n being Element of NAT for y
being set holds (n = t & y = G.t implies y in ProbPart(F.n));
reconsider BSeq = G as SetSequence of Omega by FUNCT_2:7;
reconsider BSeq as SetSequence of Sigma;
take BSeq;
thus thesis by A2;
end;
theorem Th32:
for F being sequence of COM(Sigma,P), BSeq being SetSequence
of Sigma holds ex CSeq being SetSequence of Omega st for n holds CSeq.n = F.n \
BSeq.n
proof
let F be sequence of COM(Sigma,P), G be SetSequence of Sigma;
defpred P[Element of NAT, set] means for n being Element of NAT for y being
set holds (n = $1 & y = $2 implies y = F.n \ G.n);
A1: for t being Element of NAT ex A being Element of bool Omega st P[t,A]
proof
let t be Element of NAT;
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;
thus thesis;
end;
ex H being sequence of bool Omega st for t being Element of NAT
holds P[t,H.t] from FUNCT_2:sch 3(A1);
then consider H being sequence of bool Omega such that
A2: for t being Element of NAT holds for n being Element of NAT for y
being set holds n = t & y = H.t implies y = F.n \ G.n;
take H;
thus thesis by A2;
end;
theorem Th33:
for BSeq being SetSequence of Omega st (for n holds BSeq.n is
thin of P) holds ex CSeq being SetSequence of Sigma st for n holds BSeq.n c=
CSeq.n & P.(CSeq.n) = 0
proof
let BSeq be SetSequence of Omega;
defpred P[Element of NAT, set] means for n being Element of NAT for y being
set holds (n = $1 & y = $2 implies y in Sigma & BSeq.n c= y & P.y = 0);
assume
A1: for n holds BSeq.n is thin of P;
A2: for t being Element of NAT ex A being Element of Sigma st P[t,A]
proof
let t be Element of NAT;
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 as Element of Sigma by A3;
take A;
thus thesis by A4;
end;
ex G being sequence of Sigma st for t being Element of NAT holds P[t
,G.t] from FUNCT_2:sch 3(A2);
then consider G being sequence of Sigma such that
A5: for t being Element of NAT holds for n being Element of NAT for y
being set holds (n = t & y = G.t implies y in Sigma & BSeq.n c= y & P.y = 0);
reconsider CSeq = G as SetSequence of Omega by FUNCT_2:7;
reconsider CSeq as SetSequence of Sigma;
take CSeq;
thus thesis by A5;
end;
theorem Th34:
for D being non empty Subset-Family of Omega holds (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
proof
let D be non empty Subset-Family 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;
A2: for A1 being SetSequence of Omega st rng A1 c= D holds Union A1 in D
proof
let A1 be SetSequence of Omega;
reconsider F = A1 as sequence of bool Omega;
A3: dom F = NAT by FUNCT_2:def 1;
assume
A4: rng A1 c= D;
A5: for n holds ex B being set st B in Sigma & ex C being thin of P st F.
n = B \/ C
proof
let n;
F.n in rng F by NAT_1:51;
hence thesis by A1,A4;
end;
for n holds F.n in COM(Sigma,P)
proof
let n;
ex B being set st (B in Sigma & ex C being thin of P st F.n = B \/
C) by A5;
hence thesis by Def5;
end;
then for n being object st n in NAT holds F.n in COM(Sigma,P);
then reconsider F as sequence of COM(Sigma,P) by A3,FUNCT_2:3;
consider BSeq being SetSequence of Sigma such that
A6: for n holds BSeq.n in ProbPart(F.n) by Th31;
consider CSeq being SetSequence of Omega such that
A7: for n 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;
BSeq.n in ProbPart(F.n) by A6;
hence thesis by Def7;
end;
for n holds CSeq.n is thin of P
proof
let n be Element of NAT;
F.n \ BSeq.n is thin of P by A8;
hence thesis by A7;
end;
then consider DSeq being SetSequence of Sigma such that
A9: for n 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 B;
A11: union rng BSeq c= union rng F
proof
let x be object;
assume x in union rng BSeq;
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 object such that
A14: n in NAT and
A15: Z = BSeq.n by A13,FUNCT_1:def 3;
reconsider n as Element of NAT by A14;
set P = F.n;
A16: BSeq.n c= P by A8;
ex P being set st P in rng F & x in P
proof
take P;
thus thesis by A3,A12,A15,A16,FUNCT_1:def 3;
end;
hence thesis by TARSKI:def 4;
end;
A17: ex C being thin of P st Union A1 = B \/ C
proof
set C = Union A1 \ B;
Union DSeq in Sigma by PROB_1:17;
then
A18: union rng DSeq in Sigma by CARD_3:def 4;
A19: C c= union rng CSeq
proof
let x be object;
assume
A20: x in C;
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 object such that
A23: n in NAT and
A24: Z = F.n by A3,A22,FUNCT_1:def 3;
reconsider 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;
hence thesis by A25,A26,TARSKI:def 4;
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;
dom CSeq = NAT by FUNCT_2:def 1;
hence thesis by A7,A27,FUNCT_1:def 3;
end;
hence thesis by TARSKI:def 4;
end;
for A being set holds A in rng DSeq implies P.A = 0
proof
let A be set;
A28: dom DSeq = NAT by FUNCT_2:def 1;
assume A in rng DSeq;
then ex n being object st n in NAT & A = DSeq.n
by A28,FUNCT_1:def 3;
hence thesis by A9;
end;
then
A29: P.(union rng DSeq) = 0 by Th8;
union rng CSeq c= union rng DSeq
proof
let x be object;
assume x in union rng CSeq;
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 object such that
A32: n in NAT and
A33: Z = CSeq.n by A31,FUNCT_1:def 3;
reconsider 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 thesis by A30,A33,A34,TARSKI:def 4;
end;
then C c= union rng DSeq by A19;
then
A35: C is thin of P by A29,A18,Def4;
Union A1 = C \/ union rng F /\ union rng BSeq by A10,XBOOLE_1:51
.= B \/ C by A11,XBOOLE_1:28;
then consider C being thin of P such that
A36: Union A1 = B \/ C by A35;
take C;
thus thesis by A36;
end;
Union BSeq in Sigma by PROB_1:17;
hence thesis by A17,CARD_3:def 4;
end;
hence thesis by A1;
end;
for A being Subset of Omega holds A in D implies A` in D
proof
let A be Subset of Omega;
assume
A37: 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 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 = H \ G;
A44: Omega \ A = H \ C by A40,XBOOLE_1:41;
A45: ex W being thin of P st Omega \ A = Q \/ W
proof
set W = H /\ (G \ C);
W c= H by XBOOLE_1:17;
then reconsider W as Subset of Omega by XBOOLE_1:1;
reconsider W as thin of P by A41,A43,Def4;
take W;
thus thesis by A42,A44,Lm1;
end;
take Q;
B` in Sigma by A38,PROB_1:def 1;
hence thesis by A41,A45,PROB_1:6;
end;
hence thesis by A1;
end;
hence thesis by A2,Th4;
end;
registration
let Omega,Sigma,P;
cluster COM(Sigma,P) -> compl-closed sigma-multiplicative;
coherence
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 thesis by Th34;
end;
end;
definition
let Omega,Sigma,P;
redefine mode thin of P -> Event of COM(Sigma,P); :: redefines thin (PROB_4, definition)
coherence by Th26;
end;
theorem Th35:
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 A be set;
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
proof
assume A in COM(Sigma,P);
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 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 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 thesis by A2,A8,XBOOLE_1:7;
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)
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;
reconsider A2 as Element of Sigma by A10;
reconsider A1 as Element of Sigma by A9;
set C = A \ A1;
A14: C is thin of P
proof
reconsider D = A2 \ A1 as Element of Sigma;
A15: C c= D
proof
let x be object;
assume x in C;
then x in A & not x in A1 by XBOOLE_0:def 5;
hence thesis by A12,XBOOLE_0:def 5;
end;
then C c= Omega by XBOOLE_1:1;
hence thesis by A13,A15,Def4;
end;
A = A1 \/ C by A11,XBOOLE_1:45;
hence thesis by A14,Def5;
end;
end;
theorem
for C being non empty Subset-Family of Omega holds (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)
proof
let C be non empty Subset-Family of Omega;
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);
now
let A be object;
reconsider AA=A as set by TARSKI:1;
A in C iff ex A1,A2 being set st A1 in Sigma & A2 in Sigma & A1 c= AA &
AA c= A2 & P.(A2 \ A1) = 0 by A1;
hence A in C iff A in COM(Sigma,P) by Th35;
end;
hence thesis by TARSKI:2;
end;
definition
let Omega,Sigma,P;
func COM(P) -> Probability of COM(Sigma,P) means
:Def8:
for B being set st B in Sigma for C being thin of P holds it.(B \/ C) = P.B;
existence
proof
reconsider C = {} as thin of P by Th24;
defpred P[object,object] means
for x,y being set st x in COM(Sigma,P) holds (x =
$1 & y = $2 implies (for B being set st B in Sigma for C being thin of P holds
(x = B \/ C implies y = P.B)));
set B = {};
A1: {} is thin of P by Th24;
A2: for x being object st x in COM(Sigma,P)
ex y being object st y in REAL & P[x ,y]
proof
let x be object;
assume x in COM(Sigma,P);
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;
thus thesis by A3,Th25,FUNCT_2:5;
end;
consider comP being Function of COM(Sigma,P),REAL such that
A4: for x being object st x in COM(Sigma,P) holds P[x,comP.x] from
FUNCT_2:sch 1(A2);
A5: for B being set st B in Sigma for C being thin of P holds comP.(B \/ C
) = P.B
proof
let B be set;
assume
A6: B in Sigma;
let C be thin of P;
B \/ C in COM(Sigma,P) by A6,Def5;
hence thesis by A4,A6;
end;
A7: for BSeq being SetSequence of COM(Sigma,P) st BSeq is disjoint_valued
holds Sum(comP * BSeq) = comP.(Union BSeq)
proof
let BSeq be SetSequence of COM(Sigma,P) such that
A8: BSeq is disjoint_valued;
reconsider F = BSeq as sequence of bool Omega;
rng F c= COM(Sigma,P) by RELAT_1:def 19;
then reconsider F as sequence of COM(Sigma,P) by FUNCT_2:6;
consider CSeq being SetSequence of Sigma such that
A9: for n 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 as Element of Sigma by A10,CARD_3:def 4;
consider DSeq being SetSequence of Omega such that
A11: for n 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;
CSeq.n in ProbPart(F.n) by A9;
hence thesis by Def7;
end;
for n being Element of NAT holds DSeq.n is thin of P
proof
let n be Element of NAT;
F.n \ CSeq.n is thin of P by A12;
hence thesis by A11;
end;
then consider ESeq being SetSequence of Sigma such that
A13: for n 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 object;
assume x in B;
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 object such that
A18: n in NAT and
A19: Z = CSeq.n by A17,FUNCT_1:def 3;
reconsider n as Element of NAT by A18;
set P = F.n;
A20: CSeq.n c= P by A12;
ex P being set st P in rng F & x in P
proof
take P;
thus thesis by A14,A16,A19,A20,FUNCT_1:def 3;
end;
hence thesis by TARSKI:def 4;
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 = C \/ union rng F /\ B by XBOOLE_1:51
.= B \/ C by A15,XBOOLE_1:28;
reconsider C as Subset of Omega;
A23: C c= union rng DSeq
proof
let x be object;
assume
A24: x in C;
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 object such that
A27: n in NAT and
A28: Z = F.n by A14,A26,FUNCT_1:def 3;
reconsider 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;
hence thesis by A29,A30,TARSKI:def 4;
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;
dom DSeq = NAT by FUNCT_2:def 1;
hence thesis by A11,A31,FUNCT_1:def 3;
end;
hence thesis by TARSKI:def 4;
end;
for A being set holds A in rng ESeq implies P.A = 0
proof
let A be set;
A32: dom ESeq = NAT by FUNCT_2:def 1;
assume A in rng ESeq;
then ex n being object st n in NAT & A = ESeq.n
by A32,FUNCT_1:def 3;
hence thesis by A13;
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 object;
assume x in union rng DSeq;
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 object such that
A37: n in NAT and
A38: Z = DSeq.n by A36,FUNCT_1:def 3;
reconsider 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 thesis by A35,A38,A39,TARSKI:def 4;
end;
then C c= union rng ESeq by A23;
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;
thus thesis by A40;
end;
for n,m being object st n <> m holds CSeq.n misses CSeq.m
proof
let n,m be object;
A41: dom F = NAT by FUNCT_2:def 1
.= dom CSeq by FUNCT_2:def 1;
for n being object holds CSeq.n c= F.n
proof
let n be object;
per cases;
suppose
n in dom F;
hence thesis by A12;
end;
suppose
A42: not n in dom F;
then F.n = {} by FUNCT_1:def 2
.= CSeq.n by A41,A42,FUNCT_1:def 2;
hence thesis;
end;
end;
then
A43: CSeq.n c= F.n & CSeq.m c= F.m;
assume n <> m;
then F.n misses F.m by A8,PROB_2:def 2;
then F.n /\ F.m = {};
then CSeq.n /\ CSeq.m = {} by A43,XBOOLE_1:3,27;
hence thesis;
end;
then
A44: CSeq is disjoint_valued;
Sum(comP*F) = comP.(Union F)
proof
A45: for n holds comP.(F.n) = P.(CSeq.n)
proof
let 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 thesis by A5;
end;
for x being Element of NAT holds (comP*F).x = (P*CSeq).x
proof
let x be Element of NAT;
(comP*F).x = comP.(F.x) by FUNCT_2:15
.= P.(CSeq.x) by A45
.= (P*CSeq).x by FUNCT_2:15;
hence thesis;
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 thesis by A44,A47,PROB_3:46;
end;
hence thesis;
end;
A48: for x being Element of COM(Sigma,P) holds comP.x >= 0
proof
let x be Element of COM(Sigma,P);
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 as Element of Sigma by A49;
comP.x = P.B by A4,A50;
hence thesis by PROB_1:def 8;
end;
{} = B \/ 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) such that
A53: A misses 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;
per cases;
suppose
n = 0;
hence thesis by A55;
end;
suppose
n <> 0;
then n >= 1 by NAT_1:14;
then
A56: n + 1 > 1 by NAT_1:13;
per cases by A56,NAT_1:22;
suppose
n > 1;
then BSeq.n = {} by FUNCT_7:124;
hence thesis by PROB_1:4;
end;
suppose
n = 1;
hence thesis by A54;
end;
end;
end;
then rng BSeq c= COM(Sigma,P) by NAT_1:52;
then reconsider BSeq as SetSequence of COM(Sigma,P) by RELAT_1:def 19;
for m being 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 Nat
holds Partial_Sums(comP * BSeq).(2+n) = comP.A + comP.B
proof
defpred P[Nat] means
Partial_Sums(comP * BSeq).(2+$1) = comP.A + comP.B;
A60: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A61: P[k];
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;
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: P[0];
thus for k being Nat holds P[k] from NAT_1:sch 2(A63,A60);
end;
let m be Nat;
assume 2 <= m;
then consider k being Nat such that
A64: m=2+k by NAT_1:10;
thus thesis by A59,A64;
end;
then
A65: Union BSeq = A \/ B & Sum(comP * BSeq) = comP.A + comP.B by DYNKIN:3
,PROB_1:1;
BSeq is disjoint_valued by A53,Th3;
hence thesis by A7,A65;
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);
assume
A67: A c= B;
comP.A + comP.(B \ A) = comP.(A \/ (B \ A)) by A52,XBOOLE_1:79
.= comP.B by A67,XBOOLE_1:45;
hence thesis;
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);
assume A c= 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 thesis;
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) such that
A70: BSeq is non-descending;
for n,m being Nat st n <= m holds (comP * BSeq).n <= (comP * BSeq).m
proof
let n,m be Nat;
A71: n in NAT & m in NAT by ORDINAL1:def 12;
assume n <= 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,A71;
hence thesis by FUNCT_2:15,A71;
end;
hence thesis by SEQM_3:6;
end;
A72: comP.Omega = comP.(B \/ Omega) .= P.Omega by A5,A1,PROB_1:5
.= 1 by PROB_1:def 8;
A73: 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);
comP.A <= comP.B by A68;
hence thesis by A72;
end;
A74: for BSeq being SetSequence of COM(Sigma,P) for n holds (comP*BSeq).n <= 1
proof
let BSeq be SetSequence of COM(Sigma,P);
let n;
(comP*BSeq).n = comP.(BSeq.n) by FUNCT_2:15;
hence thesis by A73;
end;
A75: for BSeq being SetSequence of COM(Sigma,P) st BSeq is non-descending
holds comP * BSeq is bounded_above & comP * BSeq is convergent
proof
let BSeq be SetSequence of COM(Sigma,P);
assume BSeq is non-descending;
then
A76: comP * BSeq is non-decreasing by A69;
for n being Nat holds (comP * BSeq).n < 2
proof
let n be Nat;
n in NAT by ORDINAL1:def 12;
then (comP * BSeq).n + 0 < 1 + 1 by A74,XREAL_1:8;
hence thesis;
end;
hence comP * BSeq is bounded_above by SEQ_2:def 3;
hence thesis by A76;
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) such that
A77: BSeq is non-descending;
reconsider CSeq=Partial_Diff_Union(BSeq) as SetSequence of COM(Sigma,P);
A78: for n being Nat holds Partial_Sums(comP * CSeq).n = (comP * BSeq).n
proof
defpred P[Nat] means Partial_Sums(comP * CSeq).$1=(comP * BSeq).$1;
A79: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A80: P[k];
A81: BSeq.k c= BSeq.(k+1) by A77,PROB_2:7;
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
thus Partial_Sums(comP * CSeq).(k+1)
=(comP * BSeq).kk + (comP * CSeq).(k+1) by A80,SERIES_1:def 1
.=comP.(BSeq.kk) + (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,A77,Th18
.=comP.(BSeq.k \/ (BSeq.(k+1) \ BSeq.k)) by A77,Th16
.=comP.(BSeq.k \/ BSeq.(k+1)) by XBOOLE_1:39
.=comP.(BSeq.(k+1)) by A81,XBOOLE_1:12
.=(comP * BSeq).(k+1) by FUNCT_2:15;
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 A77,Th16
.= (comP * BSeq).0 by FUNCT_2:15;
then
A82: P[0];
thus for k being Nat holds P[k] from NAT_1:sch 2(A82,A79);
end;
A83: Partial_Sums(comP * CSeq) = comP * BSeq by A78;
comP.Union BSeq = comP.Union CSeq by PROB_3:36
.= Sum(comP * CSeq) by A7
.= lim Partial_Sums(comP * CSeq);
hence thesis by A75,A77,A83;
end;
then reconsider comP as Probability of COM(Sigma,P) by A48,A72,A52,
PROB_2:10;
take comP;
thus thesis by A5;
end;
uniqueness
proof
let P1,P2 be Probability of COM(Sigma,P) such that
A84: for B being set st B in Sigma for C being thin of P holds P1.(B
\/ C) = P.B and
A85: for B being set st B in Sigma for C being thin of P holds P2.(B
\/ C) = P.B;
for x being object holds x in COM(Sigma,P) implies P1.x = P2.x
proof
let x be object;
assume x in COM(Sigma,P);
then consider B being set such that
A86: B in Sigma & ex C being thin of P st x = B \/ C by Def5;
P1.x = P.B by A84,A86
.= P2.x by A85,A86;
hence thesis;
end;
hence thesis;
end;
end;
theorem
COM(P) = COM(P2M P)
proof
set Y = COM(P);
COM(Sigma,P) = COM(Sigma,P2M P) by Th27;
then reconsider Y1=P2M(Y) as sigma_Measure of COM(Sigma,P2M(P));
for B being set st B in Sigma for C being thin of P2M(P) holds Y1.(B \/
C) = (P2M(P)).B
proof
let B be set such that
A1: B in Sigma;
let C be thin of P2M(P);
reconsider C1=C as thin of P by Th23;
Y.(B \/ C1) = P.B by A1,Def8;
hence thesis;
end;
hence thesis by MEASURE3:def 5;
end;
theorem
COM(P) is complete
proof
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;
let B be set;
assume
A1: B in COM(Sigma,P);
assume that
A2: A c= B and
A3: (COM P).B = 0;
ex B1 being set st (B1 in Sigma & ex C1 being thin of P st A = B1 \/ C1 )
proof
take {};
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:17;
ex O being set st O in Sigma & C1 c= O & P.O = 0
proof
reconsider B2,D2 as Element of Sigma by A4,A8;
take O;
P.(B2 \/ D2) <= 0 + 0 by A6,A10,PROB_1:39;
hence thesis by A11,PROB_1:def 8,XBOOLE_1:13;
end;
then
A12: C1 is thin of P by Def4;
A = A /\ (B2 \/ C2) by A2,A7,XBOOLE_1:28
.= {} \/ C1 by XBOOLE_1:23;
hence thesis by A12,PROB_1:4;
end;
hence thesis by Def5;
end;
hence thesis;
end;
theorem Th39:
for A being Event of Sigma holds P.A = (COM P).A
proof
reconsider C = {} as thin of P by Th24;
let A be Event of Sigma;
thus P.A = (COM P).(A \/ C) by Def8
.= (COM P).A;
end;
theorem Th40:
for C being thin of P holds (COM P).C = 0
proof
let C be thin of P;
consider A being set such that
A1: A in Sigma and
A2: C c= A and
A3: P.A = 0 by Def4;
reconsider 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 as Event of COM(Sigma,P);
(COM P).C <= (COM P).A by A2,PROB_1:34;
hence thesis by A4,PROB_1:def 8;
end;
theorem
for A being Element of COM(Sigma,P), B being set st B in ProbPart(A)
holds P.B = (COM P).A
proof
let A be Element of COM(Sigma,P), B be set such that
A1: B in ProbPart(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 as Event of COM(Sigma,P) by A2;
reconsider 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 as Event of Sigma by A1,Def7;
(COM P).A = P.B by A4,Th39;
hence thesis;
end;