:: Completeness of the $\sigma$-Additive Measure. Measure Theory
:: by J\'ozef Bia{\l}as
::
:: Received February 22, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users


begin

theorem Th1: :: MEASURE3:1
for F1, F2 being Function of NAT,ExtREAL st ( for n being Element of NAT holds (Ser F1) . n <= (Ser F2) . n ) holds
SUM F1 <= SUM F2
proofend;

theorem :: MEASURE3:2
for F1, F2 being Function of NAT,ExtREAL st ( for n being Element of NAT holds (Ser F1) . n = (Ser F2) . n ) holds
SUM F1 = SUM F2
proofend;

notation
let X be set ;
let S be SigmaField of X;
synonym  N_Sub_fam of S for  N_Measure_fam of 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 ->  N_Measure_fam of S;
coherence
 rng F is N_Measure_fam of S
proofend;
end;

theorem :: MEASURE3:3
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for F being Function of NAT,S
for A being Element of S st meet (rng F) c= A &amp; ( for n being Element of NAT holds A c= F . n ) holds
M . A = M . (meet (rng F))
proofend;

theorem Th4: :: MEASURE3:4
for X being set
for S being SigmaField of X
for G, F being Function of NAT,S st G . 0 = {} &amp; ( for n being Element of NAT holds
( G . (n + 1) = (F . 0) \ (F . n) &amp; F . (n + 1) c= F . n ) ) holds
union (rng G) = (F . 0) \ (meet (rng F))
proofend;

theorem Th5: :: MEASURE3:5
for X being set
for S being SigmaField of X
for G, F being Function of NAT,S st G . 0 = {} &amp; ( for n being Element of NAT holds
( G . (n + 1) = (F . 0) \ (F . n) &amp; F . (n + 1) c= F . n ) ) holds
meet (rng F) = (F . 0) \ (union (rng G))
proofend;

theorem Th6: :: MEASURE3:6
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for G, F being Function of NAT,S st M . (F . 0) < +infty &amp; G . 0 = {} &amp; ( for n being Element of NAT holds
( G . (n + 1) = (F . 0) \ (F . n) &amp; F . (n + 1) c= F . n ) ) holds
M . (meet (rng F)) = (M . (F . 0)) - (M . (union (rng G)))
proofend;

theorem Th7: :: MEASURE3:7
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for G, F being Function of NAT,S st M . (F . 0) < +infty &amp; G . 0 = {} &amp; ( for n being Element of NAT holds
( G . (n + 1) = (F . 0) \ (F . n) &amp; F . (n + 1) c= F . n ) ) holds
M . (union (rng G)) = (M . (F . 0)) - (M . (meet (rng F)))
proofend;

theorem :: MEASURE3:8
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for G, F being Function of NAT,S st M . (F . 0) < +infty &amp; G . 0 = {} &amp; ( for n being Element of NAT holds
( G . (n + 1) = (F . 0) \ (F . n) &amp; F . (n + 1) c= F . n ) ) holds
M . (meet (rng F)) = (M . (F . 0)) - (sup (rng (M * G)))
proofend;

theorem Th9: :: MEASURE3:9
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for G, F being Function of NAT,S st M . (F . 0) < +infty &amp; G . 0 = {} &amp; ( for n being Element of NAT holds
( G . (n + 1) = (F . 0) \ (F . n) &amp; F . (n + 1) c= F . n ) ) holds
( M . (F . 0) is Real &amp; inf (rng (M * F)) is Real &amp; sup (rng (M * G)) is Real )
proofend;

theorem Th10: :: MEASURE3:10
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for G, F being Function of NAT,S st M . (F . 0) < +infty &amp; G . 0 = {} &amp; ( for n being Element of NAT holds
( G . (n + 1) = (F . 0) \ (F . n) &amp; F . (n + 1) c= F . n ) ) holds
sup (rng (M * G)) = (M . (F . 0)) - (inf (rng (M * F)))
proofend;

theorem Th11: :: MEASURE3:11
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for G, F being Function of NAT,S st M . (F . 0) < +infty &amp; G . 0 = {} &amp; ( for n being Element of NAT holds
( G . (n + 1) = (F . 0) \ (F . n) &amp; F . (n + 1) c= F . n ) ) holds
inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G)))
proofend;

theorem :: MEASURE3:12
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for F being Function of NAT,S st ( for n being Element of NAT holds F . (n + 1) c= F . n ) &amp; M . (F . 0) < +infty holds
M . (meet (rng F)) = inf (rng (M * F))
proofend;

theorem Th13: :: MEASURE3:13
for X being set
for S being SigmaField of X
for M being Measure of S
for F being Sep_Sequence of S holds SUM (M * F) <= M . (union (rng F))
proofend;

theorem :: MEASURE3:14
for X being set
for S being SigmaField of X
for M being Measure of S st ( for F being Sep_Sequence of S holds M . (union (rng F)) <= SUM (M * F) ) holds
M is sigma_Measure of S
proofend;

::
:: Completeness of sigma_additive Measure
::
definition
let X be set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
predM is_complete S means :Def1: :: MEASURE3:def 1
 for A being Subset of X
for B being set st B in S &amp; A c= B &amp; M . B = 0. holds
A in S;
end;

:: deftheorem Def1 defines is_complete MEASURE3:def_1_:_
 for X being set
for S being SigmaField of X
for M being sigma_Measure of S holds
( M is_complete S iff for A being Subset of X
for B being set st B in S &amp; A c= B &amp; M . B = 0. holds
A in S );

definition
let X be set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
mode thin of M ->  Subset of X means :Def2: :: MEASURE3:def 2
 ex B being set st
( B in S &amp; it c= B &amp; M . B = 0. );
existence
 ex b1 being Subset of X ex B being set st
( B in S &amp; b1 c= B &amp; M . B = 0. )
proofend;
end;

:: deftheorem Def2 defines thin MEASURE3:def_2_:_
 for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for b4 being Subset of X holds
( b4 is thin of M iff ex B being set st
( B in S &amp; b4 c= B &amp; M . B = 0. ) );

definition
let X be set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func COM (S,M) ->  non empty Subset-Family of X means :Def3: :: MEASURE3:def 3
 for A being set holds
( A in it iff ex B being set st
( B in S &amp; ex C being thin of M st A = B \/ C ) );
existence
 ex b1 being non empty Subset-Family of X st
for A being set holds
( A in b1 iff ex B being set st
( B in S &amp; ex C being thin of M st A = B \/ C ) )
proofend;
uniqueness
 for b1, b2 being non empty Subset-Family of X st ( for A being set holds
( A in b1 iff ex B being set st
( B in S &amp; ex C being thin of M st A = B \/ C ) ) ) &amp; ( for A being set holds
( A in b2 iff ex B being set st
( B in S &amp; ex C being thin of M st A = B \/ C ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines COM MEASURE3:def_3_:_
 for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for b4 being non empty Subset-Family of X holds
( b4 = COM (S,M) iff for A being set holds
( A in b4 iff ex B being set st
( B in S &amp; ex C being thin of M st A = B \/ C ) ) );

definition
let X be set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
let A be Element of COM (S,M);
func MeasPart A ->  non empty Subset-Family of X means :Def4: :: MEASURE3:def 4
 for B being set holds
( B in it iff ( B in S &amp; B c= A &amp; A \ B is thin of M ) );
existence
 ex b1 being non empty Subset-Family of X st
for B being set holds
( B in b1 iff ( B in S &amp; B c= A &amp; A \ B is thin of M ) )
proofend;
uniqueness
 for b1, b2 being non empty Subset-Family of X st ( for B being set holds
( B in b1 iff ( B in S &amp; B c= A &amp; A \ B is thin of M ) ) ) &amp; ( for B being set holds
( B in b2 iff ( B in S &amp; B c= A &amp; A \ B is thin of M ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines MeasPart MEASURE3:def_4_:_
 for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for A being Element of COM (S,M)
for b5 being non empty Subset-Family of X holds
( b5 = MeasPart A iff for B being set holds
( B in b5 iff ( B in S &amp; B c= A &amp; A \ B is thin of M ) ) );

theorem Th15: :: MEASURE3:15
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for F being Function of NAT,(COM (S,M)) ex G being Function of NAT,S st
for n being Element of NAT holds G . n in MeasPart (F . n)
proofend;

theorem Th16: :: MEASURE3:16
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for F being Function of NAT,(COM (S,M))
for G being Function of NAT,S ex H being Function of NAT,(bool X) st
for n being Element of NAT holds H . n = (F . n) \ (G . n)
proofend;

theorem Th17: :: MEASURE3:17
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for F being Function of NAT,(bool X) st ( for n being Element of NAT holds F . n is thin of M ) holds
ex G being Function of NAT,S st
for n being Element of NAT holds
( F . n c= G . n &amp; M . (G . n) = 0. )
proofend;

theorem Th18: :: MEASURE3:18
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for D being non empty Subset-Family of X st ( for A being set holds
( A in D iff ex B being set st
( B in S &amp; ex C being thin of M st A = B \/ C ) ) ) holds
D is SigmaField of X
proofend;

registration
let X be set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
cluster COM (S,M) ->  non empty compl-closed sigma-additive ;
coherence
 ( COM (S,M) is sigma-additive &amp; COM (S,M) is compl-closed &amp; not COM (S,M) is empty )
proofend;
end;

theorem Th19: :: MEASURE3:19
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for B1, B2 being set st B1 in S &amp; B2 in S holds
for C1, C2 being thin of M st B1 \/ C1 = B2 \/ C2 holds
M . B1 = M . B2
proofend;

definition
let X be set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
func COM M ->  sigma_Measure of (COM (S,M)) means :Def5: :: MEASURE3:def 5
 for B being set st B in S holds
for C being thin of M holds it . (B \/ C) = M . B;
existence
 ex b1 being sigma_Measure of (COM (S,M)) st
for B being set st B in S holds
for C being thin of M holds b1 . (B \/ C) = M . B
proofend;
uniqueness
 for b1, b2 being sigma_Measure of (COM (S,M)) st ( for B being set st B in S holds
for C being thin of M holds b1 . (B \/ C) = M . B ) &amp; ( for B being set st B in S holds
for C being thin of M holds b2 . (B \/ C) = M . B ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines COM MEASURE3:def_5_:_
 for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for b4 being sigma_Measure of (COM (S,M)) holds
( b4 = COM M iff for B being set st B in S holds
for C being thin of M holds b4 . (B \/ C) = M . B );

theorem :: MEASURE3:20
for X being set
for S being SigmaField of X
for M being sigma_Measure of S holds COM M is_complete COM (S,M)
proofend;