:: The $\sigma$-additive Measure Theory
:: by J\'ozef Bia{\l}as
::
:: Received October 15, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

theorem Th1: :: MEASURE1:1
for X, Y being set holds union {X,Y,{}} = union {X,Y}
proofend;

theorem :: MEASURE1:2
for X being set
for A, B being Subset of X holds {A,B} is Subset-Family of X
proofend;

theorem :: MEASURE1:3
for X being set
for A, B, C being Subset of X holds {A,B,C} is Subset-Family of X
proofend;

scheme :: MEASURE1:sch 1
DomsetFamEx{ F1() ->  set , P1[ set ] } :
 ex F being non empty Subset-Family of F1() st
for B being set holds
( B in F iff ( B c= F1() & P1[B] ) )
provided
A1: ex B being set st
( B c= F1() & P1[B] )
proofend;

notation
let X be set ;
let S be non empty Subset-Family of X;
synonym X \ S for  COMPLEMENT S;
end;

registration
let X be set ;
let S be non empty Subset-Family of X;
clusterX \ S ->  non empty ;
coherence
 not X \ S is empty
proofend;
end;

theorem Th4: :: MEASURE1:4
for X being set
for S being non empty Subset-Family of X holds
( meet S = X \ (union (X \ S)) & union S = X \ (meet (X \ S)) )
proofend;

::
:: Field Subset of X and nonnegative measure
::
definition
let X be set ;
let IT be Subset-Family of X;
redefine attr IT is compl-closed  means :Def1: :: MEASURE1:def 1
 for A being set st A in IT holds
X \ A in IT;
compatibility
 ( IT is compl-closed iff for A being set st A in IT holds
X \ A in IT )
proofend;
end;

:: deftheorem Def1 defines compl-closed MEASURE1:def_1_:_
 for X being set
for IT being Subset-Family of X holds
( IT is compl-closed iff for A being set st A in IT holds
X \ A in IT );

registration
let X be set ;
cluster cup-closed compl-closed  ->  cap-closed for Element of bool (bool X);
coherence
 for b1 being Subset-Family of X st b1 is cup-closed & b1 is compl-closed holds
b1 is cap-closed
proofend;
cluster cap-closed compl-closed  ->  cup-closed for Element of bool (bool X);
coherence
 for b1 being Subset-Family of X st b1 is cap-closed & b1 is compl-closed holds
b1 is cup-closed
proofend;
end;

theorem :: MEASURE1:5
for X being set
for S being Field_Subset of X holds S = X \ S
proofend;

registration
let X be set ;
cluster cap-closed compl-closed  ->  diff-closed for Element of bool (bool X);
coherence
 for b1 being Subset-Family of X st b1 is compl-closed & b1 is cap-closed holds
b1 is diff-closed
proofend;
end;

theorem :: MEASURE1:6
for X being set
for S being Field_Subset of X
for A, B being set st A in S & B in S holds
A \ B in S by FINSUB_1:def_3;

theorem :: MEASURE1:7
for X being set
for S being Field_Subset of X holds
( {} in S & X in S ) by PROB_1:4, PROB_1:5;

definition
let X be non empty set ;
let F be Function of X,ExtREAL;
:: original:nonnegative
redefine attrF is nonnegative  means :Def2: :: MEASURE1:def 2
 for A being Element of X holds 0. <= F . A;
compatibility
 ( F is nonnegative iff for A being Element of X holds 0. <= F . A ) by SUPINF_2:39;
end;

:: deftheorem Def2 defines nonnegative MEASURE1:def_2_:_
 for X being non empty set
for F being Function of X,ExtREAL holds
( F is nonnegative iff for A being Element of X holds 0. <= F . A );

definition
let X be set ;
let S be Field_Subset of X;
let F be Function of S,ExtREAL;
attrF is additive  means :Def3: :: MEASURE1:def 3
 for A, B being Element of S st A misses B holds
F . (A \/ B) = (F . A) + (F . B);
end;

:: deftheorem Def3 defines additive MEASURE1:def_3_:_
 for X being set
for S being Field_Subset of X
for F being Function of S,ExtREAL holds
( F is additive iff for A, B being Element of S st A misses B holds
F . (A \/ B) = (F . A) + (F . B) );

registration
let X be set ;
let S be Field_Subset of X;
cluster Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) ext-real-valued zeroed V89() additive for Element of bool [:S,ExtREAL:];
existence
 ex b1 being Function of S,ExtREAL st
( b1 is V89() &amp; b1 is additive &amp; b1 is zeroed )
proofend;
end;

definition
let X be set ;
let S be Field_Subset of X;
mode Measure of S is zeroed V89() additive Function of S,ExtREAL;
end;

theorem Th8: :: MEASURE1:8
for X being set
for S being Field_Subset of X
for M being Measure of S
for A, B being Element of S st A c= B holds
M . A <= M . B
proofend;

theorem Th9: :: MEASURE1:9
for X being set
for S being Field_Subset of X
for M being Measure of S
for A, B being Element of S st A c= B &amp; M . A < +infty holds
M . (B \ A) = (M . B) - (M . A)
proofend;

registration
let X be set ;
cluster non empty cap-closed compl-closed for Element of bool (bool X);
existence
 ex b1 being Subset-Family of X st
( not b1 is empty &amp; b1 is compl-closed &amp; b1 is cap-closed )
proofend;
end;

definition
let X be set ;
let S be non empty cup-closed Subset-Family of X;
let A, B be Element of S;
:: original:\/
redefine funcA \/ B ->  Element of S;
coherence
 A \/ B is Element of S by FINSUB_1:def_1;
end;

definition
let X be set ;
let S be Field_Subset of X;
let A, B be Element of S;
:: original:/\
redefine funcA /\ B ->  Element of S;
coherence
 A /\ B is Element of S by FINSUB_1:def_2;
:: original:\
redefine funcA \ B ->  Element of S;
coherence
 A \ B is Element of S by FINSUB_1:def_3;
end;

theorem Th10: :: MEASURE1:10
for X being set
for S being Field_Subset of X
for M being Measure of S
for A, B being Element of S holds M . (A \/ B) <= (M . A) + (M . B)
proofend;

theorem :: MEASURE1:11
for X being set
for S being Field_Subset of X
for M being Measure of S holds
( {} in S &amp; X in S &amp; ( for A, B being set st A in S &amp; B in S holds
( X \ A in S &amp; A \/ B in S &amp; A /\ B in S ) ) ) by Def1, FINSUB_1:def_1, FINSUB_1:def_2, PROB_1:4, PROB_1:5;

definition
let X be set ;
let S be Field_Subset of X;
let M be Measure of S;
mode measure_zero of M ->  Element of S means :Def4: :: MEASURE1:def 4
M . it = 0. ;
existence
 ex b1 being Element of S st M . b1 = 0.
proofend;
end;

:: deftheorem Def4 defines measure_zero MEASURE1:def_4_:_
 for X being set
for S being Field_Subset of X
for M being Measure of S
for b4 being Element of S holds
( b4 is measure_zero of M iff M . b4 = 0. );

theorem :: MEASURE1:12
for X being set
for S being Field_Subset of X
for M being Measure of S
for A being Element of S
for B being measure_zero of M st A c= B holds
A is measure_zero of M
proofend;

theorem :: MEASURE1:13
for X being set
for S being Field_Subset of X
for M being Measure of S
for A, B being measure_zero of M holds
( A \/ B is measure_zero of M &amp; A /\ B is measure_zero of M &amp; A \ B is measure_zero of M )
proofend;

theorem :: MEASURE1:14
for X being set
for S being Field_Subset of X
for M being Measure of S
for A being Element of S
for B being measure_zero of M holds
( M . (A \/ B) = M . A &amp; M . (A /\ B) = 0. &amp; M . (A \ B) = M . A )
proofend;

::
:: sigma_Field Subset of X and sigma_additive nonnegative measure
::
theorem Th15: :: MEASURE1:15
for X being set
for A being Subset of X ex F being Function of NAT,(bool X) st rng F = {A}
proofend;

theorem Th16: :: MEASURE1:16
for A being set ex F being Function of NAT,{A} st
for n being Element of NAT holds F . n = A
proofend;

registration
let X be set ;
cluster non empty V53() for Element of bool (bool X);
existence
 ex b1 being Subset-Family of X st
( not b1 is empty &amp; b1 is V53() )
proofend;
end;

definition
let X be set ;
mode N_Sub_set_fam of X is non empty V53() Subset-Family of X;
end;

theorem Th17: :: MEASURE1:17
for X being set
for A, B, C being Subset of X ex F being Function of NAT,(bool X) st
( rng F = {A,B,C} &amp; F . 0 = A &amp; F . 1 = B &amp; ( for n being Element of NAT st 1 < n holds
F . n = C ) )
proofend;

theorem :: MEASURE1:18
for X being set
for A, B being Subset of X holds {A,B,{}} is N_Sub_set_fam of X
proofend;

theorem Th19: :: MEASURE1:19
for X being set
for A, B being Subset of X ex F being Function of NAT,(bool X) st
( rng F = {A,B} &amp; F . 0 = A &amp; ( for n being Element of NAT st 0 < n holds
F . n = B ) )
proofend;

theorem :: MEASURE1:20
for X being set
for A, B being Subset of X holds {A,B} is N_Sub_set_fam of X
proofend;

theorem Th21: :: MEASURE1:21
for X being set
for S being N_Sub_set_fam of X holds X \ S is N_Sub_set_fam of X
proofend;

definition
let X be set ;
let IT be Subset-Family of X;
attrIT is sigma-additive  means :Def5: :: MEASURE1:def 5
 for M being N_Sub_set_fam of X st M c= IT holds
union M in IT;
end;

:: deftheorem Def5 defines sigma-additive MEASURE1:def_5_:_
 for X being set
for IT being Subset-Family of X holds
( IT is sigma-additive iff for M being N_Sub_set_fam of X st M c= IT holds
union M in IT );

registration
let X be set ;
cluster non empty compl-closed sigma-additive for Element of bool (bool X);
existence
 ex b1 being Subset-Family of X st
( not b1 is empty &amp; b1 is compl-closed &amp; b1 is sigma-additive )
proofend;
end;

registration
let X be set ;
cluster compl-closed sigma-multiplicative  ->  sigma-additive for Element of bool (bool X);
coherence
 for b1 being Subset-Family of X st b1 is compl-closed &amp; b1 is sigma-multiplicative holds
b1 is sigma-additive
proofend;
cluster compl-closed sigma-additive  ->  sigma-multiplicative for Element of bool (bool X);
coherence
 for b1 being Subset-Family of X st b1 is compl-closed &amp; b1 is sigma-additive holds
b1 is sigma-multiplicative
proofend;
end;

registration
let X be set ;
cluster non empty compl-closed sigma-multiplicative  ->  for Element of bool (bool X);
coherence
 for b1 being SigmaField of X holds not b1 is empty ;
end;

theorem Th22: :: MEASURE1:22
for X being set
for S being non empty Subset-Family of X holds
( ( ( for A being set st A in S holds
X \ A in S ) &amp; ( for M being N_Sub_set_fam of X st M c= S holds
meet M in S ) ) iff S is SigmaField of X )
proofend;

registration
let X be set ;
let S be SigmaField of X;
cluster Relation-like NAT -defined S -valued Function-like non empty V14( NAT ) V18( NAT ,S) disjoint_valued for Element of bool [:NAT,S:];
existence
 ex b1 being Function of NAT,S st b1 is disjoint_valued
proofend;
end;

definition
let X be set ;
let S be SigmaField of X;
mode Sep_Sequence of S is disjoint_valued Function of NAT,S;
end;

definition
let X be set ;
let S be SigmaField of X;
let F be Function of NAT,S;
:: original:rng
redefine func rng F ->  non empty Subset-Family of X;
coherence
 rng F is non empty Subset-Family of X
proofend;
end;

theorem Th23: :: MEASURE1:23
for X being set
for S being SigmaField of X
for F being Function of NAT,S holds rng F is N_Sub_set_fam of X
proofend;

theorem Th24: :: MEASURE1:24
for X being set
for S being SigmaField of X
for F being Function of NAT,S holds union (rng F) is Element of S
proofend;

theorem Th25: :: MEASURE1:25
for Y, S being non empty set
for F being Function of Y,S
for M being Function of S,ExtREAL st M is V89() holds
M * F is V89()
proofend;

theorem Th26: :: MEASURE1:26
for X being set
for S being SigmaField of X
for a, b being R_eal ex M being Function of S,ExtREAL st
for A being Element of S holds
( ( A = {} implies M . A = a ) &amp; ( A <> {} implies M . A = b ) )
proofend;

theorem :: MEASURE1:27
for X being set
for S being SigmaField of X ex M being Function of S,ExtREAL st
for A being Element of S holds
( ( A = {} implies M . A = 0. ) &amp; ( A <> {} implies M . A = +infty ) ) by Th26;

theorem Th28: :: MEASURE1:28
for X being set
for S being SigmaField of X ex M being Function of S,ExtREAL st
for A being Element of S holds M . A = 0.
proofend;

definition
let X be set ;
let S be SigmaField of X;
let F be Function of S,ExtREAL;
attrF is sigma-additive  means :Def6: :: MEASURE1:def 6
 for s being Sep_Sequence of S holds SUM (F * s) = F . (union (rng s));
end;

:: deftheorem Def6 defines sigma-additive MEASURE1:def_6_:_
 for X being set
for S being SigmaField of X
for F being Function of S,ExtREAL holds
( F is sigma-additive iff for s being Sep_Sequence of S holds SUM (F * s) = F . (union (rng s)) );

registration
let X be set ;
let S be SigmaField of X;
cluster Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) ext-real-valued zeroed V89() sigma-additive for Element of bool [:S,ExtREAL:];
existence
 ex b1 being Function of S,ExtREAL st
( b1 is V89() &amp; b1 is sigma-additive &amp; b1 is zeroed )
proofend;
end;

definition
let X be set ;
let S be SigmaField of X;
mode sigma_Measure of S is zeroed V89() sigma-additive Function of S,ExtREAL;
end;

registration
let X be set ;
cluster non empty compl-closed sigma-additive  ->  non empty cup-closed for Element of bool (bool X);
coherence
 for b1 being non empty Subset-Family of X st b1 is sigma-additive &amp; b1 is compl-closed holds
b1 is cup-closed ;
end;

theorem Th29: :: MEASURE1:29
for X being set
for S being SigmaField of X
for M being sigma_Measure of S holds M is Measure of S
proofend;

theorem :: MEASURE1:30
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for A, B being Element of S st A misses B holds
M . (A \/ B) = (M . A) + (M . B)
proofend;

theorem Th31: :: MEASURE1:31
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for A, B being Element of S st A c= B holds
M . A <= M . B
proofend;

theorem :: MEASURE1:32
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for A, B being Element of S st A c= B &amp; M . A < +infty holds
M . (B \ A) = (M . B) - (M . A)
proofend;

theorem Th33: :: MEASURE1:33
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for A, B being Element of S holds M . (A \/ B) <= (M . A) + (M . B)
proofend;

theorem :: MEASURE1:34
for X being set
for S being SigmaField of X
for M being sigma_Measure of S holds
( {} in S &amp; X in S &amp; ( for A, B being set st A in S &amp; B in S holds
( X \ A in S &amp; A \/ B in S &amp; A /\ B in S ) ) ) by Def1, FINSUB_1:def_1, FINSUB_1:def_2, PROB_1:4, PROB_1:5;

theorem :: MEASURE1:35
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for T being N_Sub_set_fam of X st ( for A being set st A in T holds
A in S ) holds
( union T in S &amp; meet T in S )
proofend;

definition
let X be set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
mode measure_zero of M ->  Element of S means :Def7: :: MEASURE1:def 7
M . it = 0. ;
existence
 ex b1 being Element of S st M . b1 = 0.
proofend;
end;

:: deftheorem Def7 defines measure_zero MEASURE1:def_7_:_
 for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for b4 being Element of S holds
( b4 is measure_zero of M iff M . b4 = 0. );

theorem :: MEASURE1:36
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for A being Element of S
for B being measure_zero of M st A c= B holds
A is measure_zero of M
proofend;

theorem :: MEASURE1:37
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for A, B being measure_zero of M holds
( A \/ B is measure_zero of M &amp; A /\ B is measure_zero of M &amp; A \ B is measure_zero of M )
proofend;

theorem :: MEASURE1:38
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for A being Element of S
for B being measure_zero of M holds
( M . (A \/ B) = M . A &amp; M . (A /\ B) = 0. &amp; M . (A \ B) = M . A )
proofend;