:: by J\'ozef Bia{\l}as

::

:: Received February 22, 1992

:: Copyright (c) 1992-2017 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

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

SUM F1 = SUM F2

proof end;

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

end;
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;

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))

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))

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))

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)))

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)))

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)))

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 )

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)))

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)))

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))

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))

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

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;

:: deftheorem defines is_complete MEASURE3:def 1 :

for X being set

for S being SigmaField of X

for M being sigma_Measure of S holds

( M is_complete S iff for A being Subset of X

for B being set st B in S & A c= B & M . B = 0. holds

A in S );

for X being set

for S being SigmaField of X

for M being sigma_Measure of S holds

( M is_complete S iff for A being Subset of X

for B being set st B in S & A c= B & M . B = 0. holds

A in S );

definition

let X be set ;

let S be SigmaField of X;

let M be sigma_Measure of S;

ex b_{1} being Subset of X ex B being set st

( B in S & b_{1} c= B & M . B = 0. )

end;
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 set st

( B in S & it c= B & M . B = 0. );

ex b

( B in S & b

proof 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_{4} being Subset of X holds

( b_{4} is thin of M iff ex B being set st

( B in S & b_{4} c= B & M . B = 0. ) );

for X being set

for S being SigmaField of X

for M being sigma_Measure of S

for b

( b

( B in S & b

definition

let X be set ;

let S be SigmaField of X;

let M be sigma_Measure of S;

ex b_{1} being non empty Subset-Family of X st

for A being set holds

( A in b_{1} iff ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) )

for b_{1}, b_{2} being non empty Subset-Family of X st ( for A being set holds

( A in b_{1} 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_{2} iff ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) ) ) holds

b_{1} = b_{2}

end;
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 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 ) );

ex b

for A being set holds

( A in b

( B in S & ex C being thin of M st A = B \/ C ) )

proof end;

uniqueness for b

( A in b

( B in S & ex C being thin of M st A = B \/ C ) ) ) & ( for A being set holds

( A in b

( B in S & ex C being thin of M st A = B \/ C ) ) ) holds

b

proof 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_{4} being non empty Subset-Family of X holds

( b_{4} = COM (S,M) iff for A being set holds

( A in b_{4} iff ex B being set st

( B in S & ex C being thin of M st A = B \/ C ) ) );

for X being set

for S being SigmaField of X

for M being sigma_Measure of S

for b

( b

( A in b

( 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);

ex b_{1} being non empty Subset-Family of X st

for B being set holds

( B in b_{1} iff ( B in S & B c= A & A \ B is thin of M ) )

for b_{1}, b_{2} being non empty Subset-Family of X st ( for B being set holds

( B in b_{1} iff ( B in S & B c= A & A \ B is thin of M ) ) ) & ( for B being set holds

( B in b_{2} iff ( B in S & B c= A & A \ B is thin of M ) ) ) holds

b_{1} = b_{2}

end;
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 for B being set holds

( B in it iff ( B in S & B c= A & A \ B is thin of M ) );

ex b

for B being set holds

( B in b

proof end;

uniqueness for b

( B in b

( B in b

b

proof 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_{5} being non empty Subset-Family of X holds

( b_{5} = MeasPart A iff for B being set holds

( B in b_{5} iff ( B in S & B c= A & A \ B is thin of M ) ) );

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

( b

( B in b

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)

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)

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. )

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

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;

coherence

( COM (S,M) is sigma-additive & COM (S,M) is compl-closed & not COM (S,M) is empty )

end;
let S be SigmaField of X;

let M be sigma_Measure of S;

coherence

( COM (S,M) is sigma-additive & COM (S,M) is compl-closed & not COM (S,M) is empty )

proof 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

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;

ex b_{1} 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_{1} . (B \/ C) = M . B

for b_{1}, b_{2} 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_{1} . (B \/ C) = M . B ) & ( for B being set st B in S holds

for C being thin of M holds b_{2} . (B \/ C) = M . B ) holds

b_{1} = b_{2}

end;
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 for B being set st B in S holds

for C being thin of M holds it . (B \/ C) = M . B;

ex b

for B being set st B in S holds

for C being thin of M holds b

proof end;

uniqueness for b

for C being thin of M holds b

for C being thin of M holds b

b

proof 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_{4} being sigma_Measure of (COM (S,M)) holds

( b_{4} = COM M iff for B being set st B in S holds

for C being thin of M holds b_{4} . (B \/ C) = M . B );

for X being set

for S being SigmaField of X

for M being sigma_Measure of S

for b

( b

for C being thin of M holds 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 COM (S,M)

for S being SigmaField of X

for M being sigma_Measure of S holds COM M is_complete COM (S,M)

proof end;

:: Completeness of sigma_additive Measure

::