:: Properties of Caratheodory's Measure
:: by J\'ozef Bia{\l}as
::
:: Received June 25, 1992
:: Copyright (c) 1992-2021 Association of Mizar Users

theorem Th1: :: MEASURE4:1

for X being set
for S being non empty Subset-Family of X
for F, G being sequence of S
for A being Element of S st ( for n being Element of NAT holds G . n = A /\ (F . n) ) holds
union (rng G) = A /\ (union (rng F))

proof end;

theorem Th2: :: MEASURE4:2

for X being set
for S being non empty Subset-Family of X
for F, G being sequence of S st G . 0 = F . 0 & ( for n being Nat holds G . (n + 1) = (F . (n + 1)) \/ (G . n) ) holds
for H being sequence of S st H . 0 = F . 0 & ( for n being Nat holds H . (n + 1) = (F . (n + 1)) \ (G . n) ) holds
union (rng F) = union (rng H)

proof end;

theorem Th3: :: MEASURE4:3

for X being set holds bool X is SigmaField of X

proof end;

definition

let X be set ;

mode C_Measure of X -> Function of (bool X),ExtREAL means :Def1: :: MEASURE4:def 1
( it is V92() & it is zeroed & ( for A, B being Subset of X st A c= B holds
( it . A <= it . B & ( for F being sequence of (bool X) holds it . (union (rng F)) <= SUM (it * F) ) ) ) );

existence
ex b₁ being Function of (bool X),ExtREAL st
( b₁ is V92() & b₁ is zeroed & ( for A, B being Subset of X st A c= B holds
( b₁ . A <= b₁ . B & ( for F being sequence of (bool X) holds b₁ . (union (rng F)) <= SUM (b₁ * F) ) ) ) )

proof end;

end;

:: deftheorem Def1 defines C_Measure MEASURE4:def 1 :
for X being set
for b₂ being Function of (bool X),ExtREAL holds
( b₂ is C_Measure of X iff ( b₂ is V92() & b₂ is zeroed & ( for A, B being Subset of X st A c= B holds
( b₂ . A <= b₂ . B & ( for F being sequence of (bool X) holds b₂ . (union (rng F)) <= SUM (b₂ * F) ) ) ) ) );

definition

let X be set ;
let C be C_Measure of X;

func sigma_Field C -> non empty Subset-Family of X means :Def2: :: MEASURE4:def 2
for A being Subset of X holds
( A in it iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) );

existence
ex b₁ being non empty Subset-Family of X st
for A being Subset of X holds
( A in b₁ iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) )

proof end;

uniqueness
for b₁, b₂ being non empty Subset-Family of X st ( for A being Subset of X holds
( A in b₁ iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) ) ) & ( for A being Subset of X holds
( A in b₂ iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines sigma_Field MEASURE4:def 2 :
for X being set
for C being C_Measure of X
for b₃ being non empty Subset-Family of X holds
( b₃ = sigma_Field C iff for A being Subset of X holds
( A in b₃ iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z) ) );

theorem Th4: :: MEASURE4:4

for X being set
for C being C_Measure of X
for W, Z being Subset of X holds C . (W \/ Z) <= (C . W) + (C . Z)

proof end;

theorem Th5: :: MEASURE4:5

for X being set
for C being C_Measure of X
for A being Subset of X holds
( A in sigma_Field C iff for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) = C . (W \/ Z) )

proof end;

theorem Th6: :: MEASURE4:6

for X being set
for C being C_Measure of X
for W, Z being Subset of X st W in sigma_Field C & Z misses W holds
C . (W \/ Z) = (C . W) + (C . Z)

proof end;

theorem Th7: :: MEASURE4:7

for A, X being set
for C being C_Measure of X st A in sigma_Field C holds
X \ A in sigma_Field C

proof end;

theorem Th8: :: MEASURE4:8

for A, B, X being set
for C being C_Measure of X st A in sigma_Field C & B in sigma_Field C holds
A \/ B in sigma_Field C

proof end;

theorem Th9: :: MEASURE4:9

for A, B, X being set
for C being C_Measure of X st A in sigma_Field C & B in sigma_Field C holds
A /\ B in sigma_Field C

proof end;

theorem Th10: :: MEASURE4:10

for A, B, X being set
for C being C_Measure of X st A in sigma_Field C & B in sigma_Field C holds
A \ B in sigma_Field C

proof end;

theorem Th11: :: MEASURE4:11

for X being set
for S being SigmaField of X
for N being sequence of S
for A being Element of S ex F being sequence of S st
for n being Element of NAT holds F . n = A /\ (N . n)

proof end;

theorem Th12: :: MEASURE4:12

for X being set
for C being C_Measure of X holds sigma_Field C is SigmaField of X

proof end;

registration

let X be set ;
let C be C_Measure of X;

cluster sigma_Field C -> non empty compl-closed sigma-additive ;

coherence
( sigma_Field C is sigma-additive & sigma_Field C is compl-closed & not sigma_Field C is empty ) by Th12;

end;

definition

let X be set ;
let S be SigmaField of X;
let A be N_Measure_fam of S;
:: original: union
redefine func union A -> Element of S;
coherence
union A is Element of S by MEASURE2:def 1, MEASURE1:def 5;

end;

definition

let X be set ;
let C be C_Measure of X;

func sigma_Meas C -> Function of (sigma_Field C),ExtREAL means :Def3: :: MEASURE4:def 3
for A being Subset of X st A in sigma_Field C holds
it . A = C . A;

existence
ex b₁ being Function of (sigma_Field C),ExtREAL st
for A being Subset of X st A in sigma_Field C holds
b₁ . A = C . A

proof end;

uniqueness
for b₁, b₂ being Function of (sigma_Field C),ExtREAL st ( for A being Subset of X st A in sigma_Field C holds
b₁ . A = C . A ) & ( for A being Subset of X st A in sigma_Field C holds
b₂ . A = C . A ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines sigma_Meas MEASURE4:def 3 :
for X being set
for C being C_Measure of X
for b₃ being Function of (sigma_Field C),ExtREAL holds
( b₃ = sigma_Meas C iff for A being Subset of X st A in sigma_Field C holds
b₃ . A = C . A );

theorem Th13: :: MEASURE4:13

for X being set
for C being C_Measure of X holds sigma_Meas C is Measure of (sigma_Field C)

proof end;

:: Caratheodory's Theorem

theorem Th14: :: MEASURE4:14

for X being set
for C being C_Measure of X holds sigma_Meas C is sigma_Measure of (sigma_Field C)

proof end;

registration

let X be set ;
let C be C_Measure of X;

cluster sigma_Meas C -> zeroed V92() sigma-additive ;

coherence
( sigma_Meas C is nonnegative & sigma_Meas C is sigma-additive & sigma_Meas C is zeroed ) by Th14;

end;

theorem Th15: :: MEASURE4:15

for X being set
for C being C_Measure of X
for A being Subset of X st C . A = 0. holds
A in sigma_Field C

proof end;

theorem :: MEASURE4:16

for X being set
for C being C_Measure of X holds sigma_Meas C is complete

proof end;