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

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

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

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

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;
cluster X \ S -> non empty ;
coherence
not X \ S is empty
proof end;
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)) )
proof end;

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

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

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
proof end;
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 attr F 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;
attr F 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() & b1 is additive & b1 is zeroed )
proof end;
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
proof end;

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 & M . A < +infty holds
M . (B \ A) = (M . B) - (M . A)
proof end;

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 & b1 is compl-closed & b1 is cap-closed )
proof end;
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 func A \/ 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 func A /\ B -> Element of S;
coherence
A /\ B is Element of S by FINSUB_1:def 2;
:: original: \
redefine func A \ 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)
proof end;

theorem :: MEASURE1:11
for X being set
for S being Field_Subset of X
for M being Measure of S holds
( {} in S & X in S & ( for A, B being set st A in S & B in S holds
( X \ A in S & A \/ B in S & 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.
proof end;
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
proof end;

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 & A /\ B is measure_zero of M & A \ B is measure_zero of M )
proof end;

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 & M . (A /\ B) = 0. & M . (A \ B) = M . A )
proof end;

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

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

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 & b1 is V53() )
proof end;
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} & F . 0 = A & F . 1 = B & ( for n being Element of NAT st 1 < n holds
F . n = C ) )
proof end;

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

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} & F . 0 = A & ( for n being Element of NAT st 0 < n holds
F . n = B ) )
proof end;

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

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

definition
let X be set ;
let IT be Subset-Family of X;
attr IT 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 & b1 is compl-closed & b1 is sigma-additive )
proof end;
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 & b1 is sigma-multiplicative holds
b1 is sigma-additive
proof end;
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 & b1 is sigma-additive holds
b1 is sigma-multiplicative
proof end;
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 ) & ( for M being N_Sub_set_fam of X st M c= S holds
meet M in S ) ) iff S is SigmaField of X )
proof end;

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

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

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

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 ) & ( A <> {} implies M . A = b ) )
proof end;

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. ) & ( 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.
proof end;

definition
let X be set ;
let S be SigmaField of X;
let F be Function of S,ExtREAL;
attr F 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() & b1 is sigma-additive & b1 is zeroed )
proof end;
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 & 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
proof end;

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

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

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 & M . A < +infty holds
M . (B \ A) = (M . B) - (M . A)
proof end;

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

theorem :: MEASURE1:34
for X being set
for S being SigmaField of X
for M being sigma_Measure of S holds
( {} in S & X in S & ( for A, B being set st A in S & B in S holds
( X \ A in S & A \/ B in S & 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 & meet T in S )
proof end;

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

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 & A /\ B is measure_zero of M & A \ B is measure_zero of M )
proof end;

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 & M . (A /\ B) = 0. & M . (A \ B) = M . A )
proof end;