Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

### Completeness of the $\sigma$-Additive Measure. Measure Theory

by
Jozef Bialas

MML identifier: MEASURE3
[ Mizar article, MML identifier index ]

environ

vocabulary SUPINF_1, FUNCT_1, SUPINF_2, ARYTM_3, ORDINAL2, RELAT_1, MEASURE1,
MEASURE2, SETFAM_1, BOOLE, TARSKI, ARYTM_1, RLVECT_1, PROB_1, MEASURE3;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, RELAT_1,
FUNCT_1, FUNCT_2, REAL_1, NAT_1, SETFAM_1, SUPINF_1, SUPINF_2, MEASURE1,
MEASURE2;
constructors NAT_1, REAL_1, SUPINF_2, MEASURE2, PROB_2, MEMBERED, XBOOLE_0;
clusters SUBSET_1, SUPINF_1, MEASURE1, RELSET_1, ARYTM_3, MEMBERED, ZFMISC_1,
XBOOLE_0, ORDINAL2;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;

begin
::
::

reserve X for set;

theorem :: MEASURE3:1
for x being R_eal holds
(-infty <'x & x <'+infty) implies x is Real;

theorem :: MEASURE3:2
for x being R_eal holds
((not x = -infty) & (not x = +infty)) implies x is Real;

theorem :: MEASURE3:3
for F1,F2 being Function of NAT,ExtREAL st
(for n being Nat holds Ser(F1).n <=' Ser(F2).n) holds
(SUM(F1) <=' SUM(F2));

theorem :: MEASURE3:4
for F1,F2 being Function of NAT,ExtREAL holds
((for n being Nat holds Ser(F1).n = Ser(F2).n) implies
(SUM(F1) = SUM(F2)));

::
::

definition
let X be set;
let S be sigma_Field_Subset of X;
redefine mode N_Measure_fam of S;
synonym N_Sub_fam of S;
end;

definition
let X be set;
let S be sigma_Field_Subset of X;
let F be Function of NAT,S;
redefine func rng F -> N_Measure_fam of S;
end;

theorem :: MEASURE3:5
for S being sigma_Field_Subset of X,
M being sigma_Measure of S,
F being Function of NAT,S,
A being Element of S holds
(meet rng F c= A & (for n being Element of NAT holds A c= F.n)) implies
M.A = M.(meet rng F);

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

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

theorem :: MEASURE3:8
for S being sigma_Field_Subset of X holds
for M being sigma_Measure of S holds
for G,F being Function of NAT,S holds
(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))
implies
M.(meet rng F) = M.(F.0) - M.(union rng G);

theorem :: MEASURE3:9
for S being sigma_Field_Subset of X holds
for M being sigma_Measure of S holds
for G,F being Function of NAT,S holds
(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))
implies
M.(union rng G) = M.(F.0) - M.(meet rng F);

theorem :: MEASURE3:10
for S being sigma_Field_Subset of X holds
for M being sigma_Measure of S holds
for G,F being Function of NAT,S holds
(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))
implies
M.(meet rng F) = M.(F.0) - sup(rng (M*G));

theorem :: MEASURE3:11
for S being sigma_Field_Subset of X holds
for M being sigma_Measure of S holds
for G,F being Function of NAT,S holds
(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))
implies
sup(rng (M*G)) is Real & M.(F.0) is Real & inf(rng (M*F)) is Real;

theorem :: MEASURE3:12
for S being sigma_Field_Subset of X holds
for M being sigma_Measure of S holds
for G,F being Function of NAT,S holds
(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))
implies
sup(rng (M*G)) = M.(F.0) - inf(rng (M*F));

theorem :: MEASURE3:13
for S being sigma_Field_Subset of X holds
for M being sigma_Measure of S holds
for G,F being Function of NAT,S holds
(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))
implies
inf(rng (M*F)) = M.(F.0) - sup(rng (M*G));

theorem :: MEASURE3:14
for S being sigma_Field_Subset of X holds
for M being sigma_Measure of S holds
for F being Function of NAT,S holds
((for n being Element of NAT holds F.(n+1) c= F.n) &
M.(F.0) <'+infty) implies
(M.(meet rng F) = inf(rng (M*F)));

theorem :: MEASURE3:15
for S being sigma_Field_Subset of X holds
for M being Measure of S holds
for T being N_Measure_fam of S holds
for F being Sep_Sequence of S holds
T = rng F implies
SUM(M*F) <=' M.(union T);

theorem :: MEASURE3:16
for S being sigma_Field_Subset of X holds
for M being Measure of S holds
for F being Sep_Sequence of S holds
SUM(M*F) <=' M.(union rng F);

theorem :: MEASURE3:17
for S being sigma_Field_Subset of X holds
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;

::
::

definition
let X be set;
let S be sigma_Field_Subset of X;
let M be sigma_Measure of S;
canceled;

pred M is_complete S means
:: MEASURE3:def 2
for A being Subset of X for B being set st B in S holds
(A c= B & M.B = 0.) implies A in S;
end;

definition
let X be set;
let S be sigma_Field_Subset of X;
let M be sigma_Measure of S;
mode thin of M -> Subset of X means
:: MEASURE3:def 3
ex B being set st B in S & it c= B & M.B = 0.;
end;

definition
let X be set;
let S be sigma_Field_Subset of X;
let M be sigma_Measure of S;
func COM(S,M) -> non empty Subset-Family of X means
:: 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));
end;

definition
let X be set;
let S be sigma_Field_Subset 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
:: MEASURE3:def 5
for B being set holds (B in it iff (B in S & B c= A &
A \ B is thin of M));
end;

theorem :: MEASURE3:18
for S being sigma_Field_Subset of X holds
for M being sigma_Measure of S holds
for F being Function of NAT,COM(S,M) holds
ex G being Function of NAT,S st
for n being Element of NAT holds G.n in MeasPart(F.n);

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

theorem :: MEASURE3:20
for S being sigma_Field_Subset of X holds
for M being sigma_Measure of S holds
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.);

theorem :: MEASURE3:21
for S being sigma_Field_Subset of X holds
for M being sigma_Measure of S holds
for D being non empty Subset-Family of X holds
(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))
implies D is sigma_Field_Subset of X;

definition
let X be set;
let S be sigma_Field_Subset of X;
let M be sigma_Measure of S;
cluster COM(S,M) -> sigma_Field_Subset-like compl-closed non empty;
end;

theorem :: MEASURE3:22
for S being sigma_Field_Subset of X,
M being sigma_Measure of S,
B1,B2 being set st B1 in S & B2 in S holds
for C1,C2 being thin of M holds
B1 \/ C1 = B2 \/ C2 implies M.B1 = M.B2;

definition
let X be set;
let S be sigma_Field_Subset of X;
let M be sigma_Measure of S;
func COM(M) -> sigma_Measure of COM(S,M) means
:: MEASURE3:def 6
for B being set st B in S
for C being thin of M holds it.(B \/ C) = M.B;
end;

theorem :: MEASURE3:23
for S being sigma_Field_Subset of X holds
for M being sigma_Measure of S holds
COM(M) is_complete COM(S,M);