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

theorem Th1: :: MEASURE3:1

for F1, F2 being sequence of ExtREAL st ( for n being Element of NAT holds (Ser F1) . n <= (Ser F2) . n ) holds
SUM F1 <= SUM F2

proof end;

theorem :: MEASURE3:2

for F1, F2 being sequence of ExtREAL st ( for n being Element of NAT holds (Ser F1) . n = (Ser F2) . n ) holds
SUM F1 = SUM F2

proof end;

::
:: Some additional theorems about measures and functions
::

definition

let X be set ;
let S be SigmaField of X;
let F be sequence of 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:3

for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for F being sequence of 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 Th4: :: MEASURE3:4

for X being set
for S being SigmaField of X
for G, F being sequence of S st G . 0 = {} & ( for n being 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 Th5: :: MEASURE3:5

for X being set
for S being SigmaField of X
for G, F being sequence of S st G . 0 = {} & ( for n being 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 Th6: :: MEASURE3:6

for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for G, F being sequence of S st M . (F . 0) < +infty & G . 0 = {} & ( for n being 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 Th7: :: MEASURE3:7

for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for G, F being sequence of S st M . (F . 0) < +infty & G . 0 = {} & ( for n being 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:8

for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for G, F being sequence of S st M . (F . 0) < +infty & G . 0 = {} & ( for n being 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 Th9: :: MEASURE3:9

for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for G, F being sequence of S st M . (F . 0) < +infty & G . 0 = {} & ( for n being Nat holds
( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) holds
( M . (F . 0) in REAL & inf (rng (M * F)) in REAL & sup (rng (M * G)) in REAL )

proof end;

theorem Th10: :: MEASURE3:10

for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for G, F being sequence of S st M . (F . 0) < +infty & G . 0 = {} & ( for n being 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 Th11: :: MEASURE3:11

for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for G, F being sequence of S st M . (F . 0) < +infty & G . 0 = {} & ( for n being 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:12

for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for F being sequence of S st ( for n being Nat holds F . (n + 1) c= F . n ) & M . (F . 0) < +infty holds
M . (meet (rng F)) = inf (rng (M * F))

proof end;

theorem Th13: :: MEASURE3:13

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:14

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;

::
:: Completeness of sigma_additive Measure
::

definition

let X be set ;
let Sigma be SigmaField of X;
let M be sigma_Measure of Sigma;

attr M is complete means :: MEASURE3:def 1
for A being Subset of X
for B being set st B in Sigma & A c= B & M . B = 0. holds
A in Sigma;

end;

:: deftheorem defines complete MEASURE3:def 1 :
for X being set
for Sigma being SigmaField of X
for M being sigma_Measure of Sigma holds
( M is complete iff for A being Subset of X
for B being set st B in Sigma & A c= B & M . B = 0. holds
A in Sigma );

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 :Def2: :: MEASURE3:def 2
ex B being set st
( B in S & it c= B & M . B = 0. );

existence
ex b₁ being Subset of X ex B being set st
( B in S & b₁ c= B & M . B = 0. )

proof end;

end;

:: deftheorem Def2 defines thin MEASURE3:def 2 :
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for b₄ being Subset of X holds
( b₄ is thin of M iff ex B being set st
( B in S & b₄ 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 :Def3: :: MEASURE3:def 3
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 b₁ being non empty Subset-Family of X st
for A being set holds
( A in b₁ iff ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) )

proof end;

uniqueness
for b₁, b₂ being non empty Subset-Family of X st ( for A being set holds
( A in b₁ 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 b₂ iff ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines COM MEASURE3:def 3 :
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for b₄ being non empty Subset-Family of X holds
( b₄ = COM (S,M) iff for A being set holds
( A in b₄ 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 :Def4: :: MEASURE3:def 4
for B being set holds
( B in it iff ( B in S & B c= A & A \ B is thin of M ) );

existence
ex b₁ being non empty Subset-Family of X st
for B being set holds
( B in b₁ iff ( B in S & B c= A & A \ B is thin of M ) )

proof end;

uniqueness
for b₁, b₂ being non empty Subset-Family of X st ( for B being set holds
( B in b₁ iff ( B in S & B c= A & A \ B is thin of M ) ) ) & ( for B being set holds
( B in b₂ iff ( B in S & B c= A & A \ B is thin of M ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines MeasPart MEASURE3:def 4 :
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 b₅ being non empty Subset-Family of X holds
( b₅ = MeasPart A iff for B being set holds
( B in b₅ iff ( B in S & B c= A & A \ B is thin of M ) ) );

theorem Th15: :: MEASURE3:15

for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for F being sequence of (COM (S,M)) ex G being sequence of S st
for n being Element of NAT holds G . n in MeasPart (F . n)

proof end;

theorem Th16: :: MEASURE3:16

for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for F being sequence of (COM (S,M))
for G being sequence of S ex H being sequence of (bool X) st
for n being Element of NAT holds H . n = (F . n) \ (G . n)

proof end;

theorem Th17: :: MEASURE3:17

for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for F being sequence of (bool X) st ( for n being Element of NAT holds F . n is thin of M ) holds
ex G being sequence of S st
for n being Element of NAT holds
( F . n c= G . n & M . (G . n) = 0. )

proof end;

theorem Th18: :: MEASURE3:18

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 Th19: :: MEASURE3:19

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 :Def5: :: MEASURE3:def 5
for B being set st B in S holds
for C being thin of M holds it . (B \/ C) = M . B;

existence
ex b₁ being sigma_Measure of (COM (S,M)) st
for B being set st B in S holds
for C being thin of M holds b₁ . (B \/ C) = M . B

proof end;

uniqueness
for b₁, b₂ being sigma_Measure of (COM (S,M)) st ( for B being set st B in S holds
for C being thin of M holds b₁ . (B \/ C) = M . B ) & ( for B being set st B in S holds
for C being thin of M holds b₂ . (B \/ C) = M . B ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines COM MEASURE3:def 5 :
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for b₄ being sigma_Measure of (COM (S,M)) holds
( b₄ = COM M iff for B being set st B in S holds
for C being thin of M holds b₄ . (B \/ C) = M . B );

theorem :: MEASURE3:20

for X being set
for S being SigmaField of X
for M being sigma_Measure of S holds COM M is complete

proof end;