:: The $\sigma$-additive Measure Theory
:: by J\'ozef Bia{\l}as
::
:: Received October 15, 1990
:: Copyright (c) 1990-2011 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
canceled;

theorem :: MEASURE1:3
canceled;

theorem :: MEASURE1:4
canceled;

theorem :: MEASURE1:5
canceled;

theorem :: MEASURE1:6
canceled;

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

theorem :: MEASURE1:8
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 :: MEASURE1:9
canceled;

theorem :: MEASURE1:10
canceled;

theorem :: MEASURE1:11
canceled;

theorem :: MEASURE1:12
canceled;

theorem :: MEASURE1:13
canceled;

theorem :: MEASURE1:14
canceled;

theorem Th15: :: MEASURE1:15
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;

definition
let X be set ;
let IT be Subset-Family of X;
canceled;
canceled;
redefine attr IT is compl-closed means :Def3: :: MEASURE1:def 3
 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 MEASURE1:def 1 :
canceled;

:: deftheorem MEASURE1:def 2 :
canceled;

:: deftheorem Def3 defines compl-closed MEASURE1:def 3 :
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 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 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:16
canceled;

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

theorem :: MEASURE1:18
canceled;

theorem :: MEASURE1:19
canceled;

registration
let X be set ;
cluster cap-closed compl-closed -> diff-closed 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:20
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:21
for X being set
for S being Field_Subset of X holds
( {} in S & X in S ) by PROB_1:10, PROB_1:11;

definition
let X be non empty set ;
let F be Function of X,ExtREAL;
:: original: nonnegative
redefine attr F is nonnegative means :Def4: :: MEASURE1:def 4
 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:58;
end;

:: deftheorem Def4 defines nonnegative MEASURE1:def 4 :
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 );

theorem :: MEASURE1:22
canceled;

theorem :: MEASURE1:23
canceled;

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

:: deftheorem Def5 defines additive MEASURE1:def 5 :
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) V15(S, ExtREAL ) ext-real-valued zeroed V86() additive Element of bool [:S,ExtREAL:];
existence
ex b1 being Function of S,ExtREAL st
( b1 is nonnegative & 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 V86() additive Function of S,ExtREAL;
end;

theorem :: MEASURE1:24
canceled;

theorem Th25: :: MEASURE1:25
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 Th26: :: MEASURE1:26
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 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 Th27: :: MEASURE1:27
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:28
canceled;

theorem :: MEASURE1:29
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 Def3, FINSUB_1:def 1, FINSUB_1:def 2, PROB_1:10, PROB_1:11;

definition
canceled;
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 :Def7: :: MEASURE1:def 7
M . it = 0. ;
existence
ex b1 being Element of S st M . b1 = 0.
proof end;
end;

:: deftheorem MEASURE1:def 6 :
canceled;

:: deftheorem Def7 defines measure_zero MEASURE1:def 7 :
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:30
canceled;

theorem :: MEASURE1:31
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:32
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:33
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;

theorem Th34: :: MEASURE1:34
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 Th35: :: MEASURE1:35
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 V48() Element of bool (bool X);
existence
ex b1 being Subset-Family of X st
( not b1 is empty & b1 is V48() )
proof end;
end;

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

theorem :: MEASURE1:36
canceled;

theorem :: MEASURE1:37
canceled;

theorem Th38: :: MEASURE1:38
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:39
for X being set
for A, B being Subset of X holds {A,B,{}} is N_Sub_set_fam of X
proof end;

theorem Th40: :: MEASURE1:40
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:41
for X being set
for A, B being Subset of X holds {A,B} is N_Sub_set_fam of X
proof end;

theorem Th42: :: MEASURE1:42
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;
canceled;
attr IT is sigma-additive means :Def9: :: MEASURE1:def 9
 for M being N_Sub_set_fam of X st M c= IT holds
union M in IT;
end;

:: deftheorem MEASURE1:def 8 :
canceled;

:: deftheorem Def9 defines sigma-additive MEASURE1:def 9 :
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 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 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 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 -> Element of bool (bool X);
coherence
for b1 being SigmaField of X holds not b1 is empty ;
end;

theorem :: MEASURE1:43
canceled;

theorem :: MEASURE1:44
canceled;

theorem :: MEASURE1:45
canceled;

theorem :: MEASURE1:46
canceled;

theorem :: MEASURE1:47
canceled;

theorem :: MEASURE1:48
canceled;

theorem Th49: :: MEASURE1:49
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 ) V15( NAT ,S) disjoint_valued 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: proj2
redefine func rng F -> non empty Subset-Family of X;
coherence
proj2 F is non empty Subset-Family of X
proof end;
end;

theorem :: MEASURE1:50
canceled;

theorem :: MEASURE1:51
canceled;

theorem Th52: :: MEASURE1:52
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 Th53: :: MEASURE1:53
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 Th54: :: MEASURE1:54
for Y, S being non empty set
for F being Function of Y,S
for M being Function of S,ExtREAL st M is nonnegative holds
M * F is nonnegative
proof end;

theorem Th55: :: MEASURE1:55
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:56
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 Th55;

theorem Th57: :: MEASURE1:57
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;
canceled;
attr F is sigma-additive means :Def11: :: MEASURE1:def 11
 for s being Sep_Sequence of S holds SUM (F * s) = F . (union (rng s));
end;

:: deftheorem MEASURE1:def 10 :
canceled;

:: deftheorem Def11 defines sigma-additive MEASURE1:def 11 :
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) V15(S, ExtREAL ) ext-real-valued zeroed V86() sigma-additive Element of bool [:S,ExtREAL:];
existence
ex b1 being Function of S,ExtREAL st
( b1 is nonnegative & 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 V86() sigma-additive Function of S,ExtREAL;
end;

registration
let X be set ;
cluster non empty compl-closed sigma-additive -> non empty cup-closed 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 :: MEASURE1:58
canceled;

theorem :: MEASURE1:59
canceled;

theorem Th60: :: MEASURE1:60
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:61
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 Th62: :: MEASURE1:62
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:63
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 Th64: :: MEASURE1:64
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:65
canceled;

theorem :: MEASURE1:66
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 Def3, FINSUB_1:def 1, FINSUB_1:def 2, PROB_1:10, PROB_1:11;

theorem :: MEASURE1:67
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
canceled;
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 :Def13: :: MEASURE1:def 13
M . it = 0. ;
existence
ex b1 being Element of S st M . b1 = 0.
proof end;
end;

:: deftheorem MEASURE1:def 12 :
canceled;

:: deftheorem Def13 defines measure_zero MEASURE1:def 13 :
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:68
canceled;

theorem :: MEASURE1:69
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:70
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:71
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;