:: MEASURE3 semantic presentation

theorem :: MEASURE3:1

for x being R_eal st -infty <' x & x <' +infty holds
x is Real

proof end;

theorem Th2: :: MEASURE3:2

for x being R_eal st not x = -infty & not x = +infty holds
x is Real

proof end;

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

proof end;

theorem :: MEASURE3:4

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

proof end;

notation

let X be set ;
let S be sigma_Field_Subset of X;
synonym N_Sub_fam of S for N_Measure_fam of S;

end;

definition

let X be set ;
let S be sigma_Field_Subset of X;
let F be Function of NAT ,S;
:: original: rng
redefine func rng F -> N_Measure_fam of S;
coherence

proof end;

end;

theorem :: MEASURE3:5

for X being set
for S being sigma_Field_Subset of X
for M being sigma_Measure of S
for F being Function of NAT ,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 Th6: :: MEASURE3:6

for X being set
for S being sigma_Field_Subset of X
for G, F being Function of NAT ,S st G . 0 = {} & ( for n being Element of 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 Th7: :: MEASURE3:7

for X being set
for S being sigma_Field_Subset of X
for G, F being Function of NAT ,S st G . 0 = {} & ( for n being Element of 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 Th8: :: MEASURE3:8

for X being set
for S being sigma_Field_Subset of X
for M being sigma_Measure of S
for G, F being Function of NAT ,S st 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 ) ) holds
M . (meet (rng F)) = (M . (F . 0)) - (M . (union (rng G)))

proof end;

theorem Th9: :: MEASURE3:9

for X being set
for S being sigma_Field_Subset of X
for M being sigma_Measure of S
for G, F being Function of NAT ,S st 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 ) ) holds
M . (union (rng G)) = (M . (F . 0)) - (M . (meet (rng F)))

proof end;

theorem :: MEASURE3:10

proof end;

theorem Th11: :: MEASURE3:11

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

proof end;

theorem Th12: :: MEASURE3:12

for X being set
for S being sigma_Field_Subset of X
for M being sigma_Measure of S
for G, F being Function of NAT ,S st 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 ) ) holds
sup (rng (M * G)) = (M . (F . 0)) - (inf (rng (M * F)))

proof end;

theorem Th13: :: MEASURE3:13

for X being set
for S being sigma_Field_Subset of X
for M being sigma_Measure of S
for G, F being Function of NAT ,S st 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 ) ) holds
inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G)))

proof end;

theorem :: MEASURE3:14

for X being set
for S being sigma_Field_Subset of X
for M being sigma_Measure of S
for F being Function of NAT ,S st ( for n being Element of NAT holds F . (n + 1) c= F . n ) & M . (F . 0) <' +infty holds
M . (meet (rng F)) = inf (rng (M * F))

proof end;

theorem Th15: :: MEASURE3:15

for X being set
for S being sigma_Field_Subset of X
for M being Measure of S
for T being N_Measure_fam of S
for F being Sep_Sequence of S st T = rng F holds
SUM (M * F) <=' M . (union T)

proof end;

theorem :: MEASURE3:16

for X being set
for S being sigma_Field_Subset of X
for M being Measure of S
for F being Sep_Sequence of S holds SUM (M * F) <=' M . (union (rng F)) by Th15;

theorem :: MEASURE3:17

for X being set
for S being sigma_Field_Subset 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;

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 :Def2: :: MEASURE3:def 2
for A being Subset of X
for B being set st B in S & A c= B & M . B = 0. holds
A in S;

end;

:: deftheorem MEASURE3:def 1 :

:: deftheorem Def2 defines is_complete MEASURE3:def 2 :

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

proof end;

end;

:: deftheorem Def3 defines thin MEASURE3:def 3 :

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 :Def4: :: 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 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines COM MEASURE3:def 4 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines MeasPart MEASURE3:def 5 :

theorem Th18: :: MEASURE3:18

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

proof end;

theorem Th19: :: MEASURE3:19

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

proof end;

theorem Th20: :: MEASURE3:20

for X being set
for S being sigma_Field_Subset of X
for M being sigma_Measure of S
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. )

proof end;

Lm1: for P, G, C being set st C c= G holds
P \ C = (P \ G) \/ (P /\ (G \ C))

proof end;

theorem Th21: :: MEASURE3:21

for X being set
for S being sigma_Field_Subset 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 sigma_Field_Subset of X

proof end;

registration

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

proof end;

end;

theorem Th22: :: MEASURE3:22

for X being set
for S being sigma_Field_Subset 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 sigma_Field_Subset of X;
let M be sigma_Measure of S;
func COM M -> sigma_Measure of COM S,M means :Def6: :: MEASURE3:def 6
for B being set st B in S holds
for C being thin of M holds it . (B \/ C) = M . B;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines COM MEASURE3:def 6 :

theorem :: MEASURE3:23

for X being set
for S being sigma_Field_Subset of X
for M being sigma_Measure of S holds COM M is_complete COM S,M

proof end;