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

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{ F₁() -> set , P₁[ set ] } :

ex F being non empty Subset-Family of F₁() st
for B being set holds
( B in F iff ( B c= F₁() & P₁[B] ) )

provided

A1: ex B being set st
( B c= F₁() & P₁[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 b₁ being Subset-Family of X st b₁ is cup-closed & b₁ is compl-closed holds
b₁ is cap-closed

proof end;

cluster cap-closed compl-closed -> cup-closed for Element of bool (bool X);

coherence
for b₁ being Subset-Family of X st b₁ is cap-closed & b₁ is compl-closed holds
b₁ 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 b₁ being Subset-Family of X st b₁ is compl-closed & b₁ is cap-closed holds
b₁ 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 non empty Subset-Family 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 & A \/ B in S holds
F . (A \/ B) = (F . A) + (F . B);

end;

:: deftheorem Def3 defines additive MEASURE1:def 3 :
for X being set
for S being non empty Subset-Family 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 & A \/ B in S 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 V94() additive for Element of bool [:S,ExtREAL:];

existence
ex b₁ being Function of S,ExtREAL st
( b₁ is V94() & b₁ is additive & b₁ is zeroed )

proof end;

end;

definition

let X be set ;
let S be Field_Subset of X;
mode Measure of S is zeroed V94() 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 b₁ being Subset-Family of X st
( not b₁ is empty & b₁ is compl-closed & b₁ 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 b₁ being Element of S st M . b₁ = 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 b₄ being Element of S holds
( b₄ is measure_zero of M iff M . b₄ = 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 sequence of (bool X) st rng F = {A}

proof end;

theorem Th16: :: MEASURE1:16

for A being set ex F being sequence of {A} st
for n being Element of NAT holds F . n = A

proof end;

registration

let X be set ;

cluster non empty V58() for Element of bool (bool X);

existence
ex b₁ being Subset-Family of X st
( not b₁ is empty & b₁ is V58() )

proof end;

end;

definition

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

end;

theorem Th17: :: MEASURE1:17

for X being set
for A, B, C being Subset of X ex F being sequence of (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 sequence of (bool X) st
( rng F = {A,B} & F . 0 = A & ( for n being 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 b₁ being Subset-Family of X st
( not b₁ is empty & b₁ is compl-closed & b₁ 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 b₁ being Subset-Family of X st b₁ is compl-closed & b₁ is sigma-multiplicative holds
b₁ is sigma-additive

proof end;

cluster compl-closed sigma-additive -> sigma-multiplicative for Element of bool (bool X);

coherence
for b₁ being Subset-Family of X st b₁ is compl-closed & b₁ is sigma-additive holds
b₁ 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 b₁ being SigmaField of X holds not b₁ 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 b₁ being sequence of S st b₁ 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 sequence of S;

end;

definition

let X be set ;
let S be SigmaField of X;
let F be sequence of 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 sequence of 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 sequence of 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 V94() holds
M * F is V94()

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 :: MEASURE1:def 6
for s being Sep_Sequence of S holds SUM (F * s) = F . (union (rng s));

end;

:: deftheorem 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 V94() sigma-additive for Element of bool [:S,ExtREAL:];

existence
ex b₁ being Function of S,ExtREAL st
( b₁ is V94() & b₁ is sigma-additive & b₁ is zeroed )

proof end;

end;

definition

let X be set ;
let S be SigmaField of X;
mode sigma_Measure of S is zeroed V94() 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 b₁ being non empty Subset-Family of X st b₁ is sigma-additive & b₁ is compl-closed holds
b₁ is cup-closed ;

end;

registration

let X be set ;
let S be SigmaField of X;

cluster Function-like V18(S, ExtREAL ) zeroed V94() sigma-additive -> zeroed V94() additive for Element of bool [:S,ExtREAL:];

coherence
for b₁ being zeroed V94() Function of S,ExtREAL st b₁ is sigma-additive holds
b₁ is additive

proof end;

end;

theorem :: 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 ;

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) by Def3;

theorem :: 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 by Th8;

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) by Th9;

theorem :: 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) by Th10;

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 b₁ being Element of S st M . b₁ = 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 b₄ being Element of S holds
( b₄ is measure_zero of M iff M . b₄ = 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;

definition

let X be set ;
let S be Field_Subset of X;
let F be Function of S,ExtREAL;

redefine attr F is additive means :: MEASURE1:def 8
for A, B being Element of S st A misses B holds
F . (A \/ B) = (F . A) + (F . B);

compatibility
( F is additive iff for A, B being Element of S st A misses B holds
F . (A \/ B) = (F . A) + (F . B) ) ;

end;

:: deftheorem defines additive MEASURE1:def 8 :
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) );