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


begin

theorem :: MEASURE3:1
canceled;

theorem :: MEASURE3:2
canceled;

theorem Th3: :: MEASURE3:3
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
proof end;

theorem :: MEASURE3:4
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
proof end;

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
proof end;
end;

theorem :: MEASURE3:5
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 & ( for n being Element of NAT holds A c= F . n ) holds
M . A = M . (meet (rng F))
proof end;

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

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

theorem Th8: :: 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 & G . 0 = {} & ( for n being Element of NAT holds
( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds
M . (meet (rng F)) = (M . (F . 0)) - (M . (union (rng G)))
proof end;

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 & G . 0 = {} & ( for n being Element of NAT holds
( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds
M . (union (rng G)) = (M . (F . 0)) - (M . (meet (rng F)))
proof end;

theorem :: 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 & G . 0 = {} & ( for n being Element of NAT holds
( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds
M . (meet (rng F)) = (M . (F . 0)) - (sup (rng (M * G)))
proof end;

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 & G . 0 = {} & ( for n being Element of NAT holds
( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds
( M . (F . 0) is Real & inf (rng (M * F)) is Real & sup (rng (M * G)) is Real )
proof end;

theorem Th12: :: MEASURE3:12
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 & G . 0 = {} & ( for n being Element of NAT holds
( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds
sup (rng (M * G)) = (M . (F . 0)) - (inf (rng (M * F)))
proof end;

theorem Th13: :: MEASURE3:13
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 & G . 0 = {} & ( for n being Element of NAT holds
( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds
inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G)))
proof end;

theorem :: MEASURE3:14
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 ) & M . (F . 0) < +infty holds
M . (meet (rng F)) = inf (rng (M * F))
proof end;

theorem Th15: :: MEASURE3:15
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))
proof end;

theorem :: MEASURE3:16
canceled;

theorem :: MEASURE3:17
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
proof end;

definition
let X be set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
canceled;
pred M is_complete S means :Def2: :: MEASURE3:def 2
 for A being Subset of X
for B being set st B in S & A c= B & M . B = 0. holds
A in S;
end;

:: deftheorem MEASURE3:def 1 :
canceled;

:: deftheorem Def2 defines is_complete MEASURE3:def 2 :
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 & A c= B & 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 :Def3: :: MEASURE3:def 3
 ex B being set st
( B in S & it c= B & M . B = 0. );
existence
ex b1 being Subset of X ex B being set st
( B in S & b1 c= B & M . B = 0. )
proof end;
end;

:: deftheorem Def3 defines thin MEASURE3:def 3 :
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 & b4 c= B & 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 :Def4: :: MEASURE3:def 4
 for A being set holds
( A in it iff ex B being set st
( B in S & 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 & ex C being thin of M st A = B \/ C ) )
proof end;
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 & ex C being thin of M st A = B \/ C ) ) ) & ( for A being set holds
( A in b2 iff ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines COM MEASURE3:def 4 :
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 & 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 :Def5: :: MEASURE3:def 5
 for B being set holds
( B in it iff ( B in S & B c= A & 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 & B c= A & A \ B is thin of M ) )
proof end;
uniqueness
for b1, b2 being non empty Subset-Family of X st ( for B being set holds
( B in b1 iff ( B in S & B c= A & A \ B is thin of M ) ) ) & ( for B being set holds
( B in b2 iff ( B in S & B c= A & A \ B is thin of M ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines MeasPart MEASURE3:def 5 :
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 & B c= A & A \ B is thin of M ) ) );

theorem Th18: :: MEASURE3:18
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)
proof end;

theorem Th19: :: MEASURE3:19
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)
proof end;

theorem Th20: :: MEASURE3:20
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 & M . (G . n) = 0. )
proof end;

theorem Th21: :: MEASURE3:21
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 & ex C being thin of M st A = B \/ C ) ) ) holds
D is SigmaField of X
proof end;

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 & COM (S,M) is compl-closed & not COM (S,M) is empty )
proof end;
end;

theorem Th22: :: MEASURE3:22
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 & B2 in S holds
for C1, C2 being thin of M st B1 \/ C1 = B2 \/ C2 holds
M . B1 = M . B2
proof end;

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 :Def6: :: MEASURE3:def 6
 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
proof end;
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 ) & ( for B being set st B in S holds
for C being thin of M holds b2 . (B \/ C) = M . B ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines COM MEASURE3:def 6 :
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:23
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)
proof end;