:: MEASURE3 semantic presentation
begin
theorem Th1: :: MEASURE3:1
for F1, F2 being Function of NAT,ExtREAL st ( for n being Element of NAT holds (Ser F1) . n <= (Ser F2) . n ) holds
SUM F1 <= SUM F2
proof
let F1, F2 be Function of NAT,ExtREAL; ::_thesis: ( ( for n being Element of NAT holds (Ser F1) . n <= (Ser F2) . n ) implies SUM F1 <= SUM F2 )
assume A1: for n being Element of NAT holds (Ser F1) . n <= (Ser F2) . n ; ::_thesis: SUM F1 <= SUM F2
A2: for x being ext-real number st x in rng (Ser F1) holds
ex y being ext-real number st
( y in rng (Ser F2) & x <= y )
proof
let x be ext-real number ; ::_thesis: ( x in rng (Ser F1) implies ex y being ext-real number st
( y in rng (Ser F2) & x <= y ) )
A3: dom (Ser F1) = NAT by FUNCT_2:def_1;
assume x in rng (Ser F1) ; ::_thesis: ex y being ext-real number st
( y in rng (Ser F2) & x <= y )
then consider n being set such that
A4: n in NAT and
A5: x = (Ser F1) . n by A3, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A4;
reconsider y = (Ser F2) . n as R_eal ;
take y ; ::_thesis: ( y in rng (Ser F2) & x <= y )
dom (Ser F2) = NAT by FUNCT_2:def_1;
hence ( y in rng (Ser F2) & x <= y ) by A1, A5, FUNCT_1:def_3; ::_thesis: verum
end;
( SUM F1 = sup (rng (Ser F1)) & SUM F2 = sup (rng (Ser F2)) ) by SUPINF_2:def_17;
hence SUM F1 <= SUM F2 by A2, XXREAL_2:63; ::_thesis: verum
end;
theorem :: MEASURE3:2
for F1, F2 being Function of NAT,ExtREAL st ( for n being Element of NAT holds (Ser F1) . n = (Ser F2) . n ) holds
SUM F1 = SUM F2
proof
let F1, F2 be Function of NAT,ExtREAL; ::_thesis: ( ( for n being Element of NAT holds (Ser F1) . n = (Ser F2) . n ) implies SUM F1 = SUM F2 )
assume A1: for n being Element of NAT holds (Ser F1) . n = (Ser F2) . n ; ::_thesis: SUM F1 = SUM F2
then for n being Element of NAT holds (Ser F2) . n <= (Ser F1) . n ;
then A2: SUM F2 <= SUM F1 by Th1;
for n being Element of NAT holds (Ser F1) . n <= (Ser F2) . n by A1;
then SUM F1 <= SUM F2 by Th1;
hence SUM F1 = SUM F2 by A2, XXREAL_0:1; ::_thesis: verum
end;
notation
let X be set ;
let S be SigmaField of X;
synonym N_Sub_fam of S for N_Measure_fam of S;
end;
definition
let X be set ;
let S be SigmaField of X;
let F be Function of NAT,S;
:: original: rng
redefine func rng F -> N_Measure_fam of S;
coherence
rng F is N_Measure_fam of S
proof
( rng F is N_Sub_set_fam of X & rng F c= S ) by MEASURE1:23, RELAT_1:def_19;
hence rng F is N_Measure_fam of S by MEASURE2:def_1; ::_thesis: verum
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 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
let X be set ; ::_thesis: for S being SigmaField 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))
let S be SigmaField of X; ::_thesis: 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))
let M be sigma_Measure of S; ::_thesis: 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))
let F be Function of NAT,S; ::_thesis: 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))
let A be Element of S; ::_thesis: ( meet (rng F) c= A & ( for n being Element of NAT holds A c= F . n ) implies M . A = M . (meet (rng F)) )
assume that
A1: meet (rng F) c= A and
A2: for n being Element of NAT holds A c= F . n ; ::_thesis: M . A = M . (meet (rng F))
A c= meet (rng F)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in meet (rng F) )
assume A3: x in A ; ::_thesis: x in meet (rng F)
for Y being set st Y in rng F holds
x in Y
proof
let Y be set ; ::_thesis: ( Y in rng F implies x in Y )
A4: dom F = NAT by FUNCT_2:def_1;
assume Y in rng F ; ::_thesis: x in Y
then ex n being set st
( n in NAT & Y = F . n ) by A4, FUNCT_1:def_3;
then A c= Y by A2;
hence x in Y by A3; ::_thesis: verum
end;
hence x in meet (rng F) by SETFAM_1:def_1; ::_thesis: verum
end;
then A5: M . A <= M . (meet (rng F)) by MEASURE1:31;
M . (meet (rng F)) <= M . A by A1, MEASURE1:31;
hence M . A = M . (meet (rng F)) by A5, XXREAL_0:1; ::_thesis: verum
end;
theorem Th4: :: MEASURE3:4
for X being set
for S being SigmaField 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
let X be set ; ::_thesis: for S being SigmaField 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))
let S be SigmaField of X; ::_thesis: 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))
let G, F be Function of NAT,S; ::_thesis: ( 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)) )
assume that
A1: G . 0 = {} and
A2: for n being Element of NAT holds
( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ; ::_thesis: union (rng G) = (F . 0) \ (meet (rng F))
A3: dom G = NAT by FUNCT_2:def_1;
thus union (rng G) c= (F . 0) \ (meet (rng F)) :: according to XBOOLE_0:def_10 ::_thesis: (F . 0) \ (meet (rng F)) c= union (rng G)
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in union (rng G) or A in (F . 0) \ (meet (rng F)) )
assume A in union (rng G) ; ::_thesis: A in (F . 0) \ (meet (rng F))
then consider Z being set such that
A4: A in Z and
A5: Z in rng G by TARSKI:def_4;
consider n being set such that
A6: n in NAT and
A7: Z = G . n by A3, A5, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A6;
consider k being Nat such that
A8: n = k + 1 by A1, A4, A7, NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
set Y = F . k;
A9: A in (F . 0) \ (F . k) by A2, A4, A7, A8;
then ( F . k in rng F & not A in F . k ) by FUNCT_2:4, XBOOLE_0:def_5;
then A10: not A in meet (rng F) by SETFAM_1:def_1;
A in F . 0 by A9, XBOOLE_0:def_5;
hence A in (F . 0) \ (meet (rng F)) by A10, XBOOLE_0:def_5; ::_thesis: verum
end;
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in (F . 0) \ (meet (rng F)) or A in union (rng G) )
assume A11: A in (F . 0) \ (meet (rng F)) ; ::_thesis: A in union (rng G)
then not A in meet (rng F) by XBOOLE_0:def_5;
then A12: ex Y being set st
( Y in rng F & not A in Y ) by SETFAM_1:def_1;
A in F . 0 by A11, XBOOLE_0:def_5;
then consider Y being set such that
A13: A in F . 0 and
A14: Y in rng F and
A15: not A in Y by A12;
dom F = NAT by FUNCT_2:def_1;
then consider n being set such that
A16: n in NAT and
A17: Y = F . n by A14, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A16;
A in (F . 0) \ (F . n) by A13, A15, A17, XBOOLE_0:def_5;
then A18: A in G . (n + 1) by A2;
G . (n + 1) in rng G by FUNCT_2:4;
hence A in union (rng G) by A18, TARSKI:def_4; ::_thesis: verum
end;
theorem Th5: :: MEASURE3:5
for X being set
for S being SigmaField 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
let X be set ; ::_thesis: for S being SigmaField 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))
let S be SigmaField of X; ::_thesis: 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))
let G, F be Function of NAT,S; ::_thesis: ( 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)) )
assume that
A1: G . 0 = {} and
A2: for n being Element of NAT holds
( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ; ::_thesis: meet (rng F) = (F . 0) \ (union (rng G))
A3: for n being Element of NAT holds F . n c= F . 0
proof
defpred S1[ Element of NAT ] means F . $1 c= F . 0;
A4: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A5: F . k c= F . 0 ; ::_thesis: S1[k + 1]
F . (k + 1) c= F . k by A2;
hence S1[k + 1] by A5, XBOOLE_1:1; ::_thesis: verum
end;
A6: S1[ 0 ] ;
thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A4); ::_thesis: verum
end;
A7: meet (rng F) c= F . 0
proof
set X = the Element of rng F;
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in meet (rng F) or A in F . 0 )
dom F = NAT by FUNCT_2:def_1;
then ex n being set st
( n in NAT & F . n = the Element of rng F ) by FUNCT_1:def_3;
then A8: the Element of rng F c= F . 0 by A3;
assume A in meet (rng F) ; ::_thesis: A in F . 0
then A in the Element of rng F by SETFAM_1:def_1;
hence A in F . 0 by A8; ::_thesis: verum
end;
A9: (F . 0) /\ (meet (rng F)) = (F . 0) \ ((F . 0) \ (meet (rng F))) by XBOOLE_1:48;
union (rng G) = (F . 0) \ (meet (rng F)) by A1, A2, Th4;
hence meet (rng F) = (F . 0) \ (union (rng G)) by A7, A9, XBOOLE_1:28; ::_thesis: verum
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 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
let X be set ; ::_thesis: for S being SigmaField 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)))
let S be SigmaField of X; ::_thesis: 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)))
let M be sigma_Measure of S; ::_thesis: 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)))
let G, F be Function of NAT,S; ::_thesis: ( 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))) )
assume that
A1: M . (F . 0) < +infty and
A2: ( G . 0 = {} & ( for n being Element of NAT holds
( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) ) ; ::_thesis: M . (meet (rng F)) = (M . (F . 0)) - (M . (union (rng G)))
A3: union (rng G) = (F . 0) \ (meet (rng F)) by A2, Th4;
A4: M . ((F . 0) \ (union (rng G))) = M . (meet (rng F)) by A2, Th5;
M . ((F . 0) \ (meet (rng F))) <> +infty by A1, MEASURE1:31, XBOOLE_1:36;
then M . (union (rng G)) < +infty by A3, XXREAL_0:4;
hence M . (meet (rng F)) = (M . (F . 0)) - (M . (union (rng G))) by A3, A4, MEASURE1:32, XBOOLE_1:36; ::_thesis: verum
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 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
let X be set ; ::_thesis: for S being SigmaField 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)))
let S be SigmaField of X; ::_thesis: 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)))
let M be sigma_Measure of S; ::_thesis: 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)))
let G, F be Function of NAT,S; ::_thesis: ( 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))) )
assume that
A1: M . (F . 0) < +infty and
A2: ( G . 0 = {} & ( for n being Element of NAT holds
( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) ) ; ::_thesis: M . (union (rng G)) = (M . (F . 0)) - (M . (meet (rng F)))
A3: meet (rng F) = (F . 0) \ (union (rng G)) by A2, Th5;
A4: M . ((F . 0) \ (meet (rng F))) = M . (union (rng G)) by A2, Th4;
M . ((F . 0) \ (union (rng G))) <> +infty by A1, MEASURE1:31, XBOOLE_1:36;
then M . (meet (rng F)) < +infty by A3, XXREAL_0:4;
hence M . (union (rng G)) = (M . (F . 0)) - (M . (meet (rng F))) by A3, A4, MEASURE1:32, XBOOLE_1:36; ::_thesis: verum
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 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)) - (sup (rng (M * G)))
proof
let X be set ; ::_thesis: for S being SigmaField 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)) - (sup (rng (M * G)))
let S be SigmaField of X; ::_thesis: 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)) - (sup (rng (M * G)))
let M be sigma_Measure of S; ::_thesis: 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)) - (sup (rng (M * G)))
let G, F be Function of NAT,S; ::_thesis: ( 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))) )
assume that
A1: M . (F . 0) < +infty and
A2: ( G . 0 = {} & ( for n being Element of NAT holds
( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ) ) ; ::_thesis: M . (meet (rng F)) = (M . (F . 0)) - (sup (rng (M * G)))
for n being Element of NAT holds G . n c= G . (n + 1) by A2, MEASURE2:13;
then M . (union (rng G)) = sup (rng (M * G)) by MEASURE2:23;
hence M . (meet (rng F)) = (M . (F . 0)) - (sup (rng (M * G))) by A1, A2, Th6; ::_thesis: verum
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 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 . (F . 0) is Real & inf (rng (M * F)) is Real & sup (rng (M * G)) is Real )
proof
let X be set ; ::_thesis: for S being SigmaField 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 . (F . 0) is Real & inf (rng (M * F)) is Real & sup (rng (M * G)) is Real )
let S be SigmaField of X; ::_thesis: 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 . (F . 0) is Real & inf (rng (M * F)) is Real & sup (rng (M * G)) is Real )
let M be sigma_Measure of S; ::_thesis: 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 . (F . 0) is Real & inf (rng (M * F)) is Real & sup (rng (M * G)) is Real )
let G, F be Function of NAT,S; ::_thesis: ( 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 . (F . 0) is Real & inf (rng (M * F)) is Real & sup (rng (M * G)) is Real ) )
assume that
A1: M . (F . 0) < +infty and
A2: G . 0 = {} and
A3: for n being Element of NAT holds
( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ; ::_thesis: ( M . (F . 0) is Real & inf (rng (M * F)) is Real & sup (rng (M * G)) is Real )
reconsider P = {} as Element of S by PROB_1:4;
M . P <= M . (F . 0) by MEASURE1:31, XBOOLE_1:2;
then 0. <= M . (F . 0) by VALUED_0:def_19;
hence A4: M . (F . 0) is Real by A1, XXREAL_0:46; ::_thesis: ( inf (rng (M * F)) is Real & sup (rng (M * G)) is Real )
for x being ext-real number st x in rng (M * G) holds
x <= M . (F . 0)
proof
let x be ext-real number ; ::_thesis: ( x in rng (M * G) implies x <= M . (F . 0) )
A5: dom (M * G) = NAT by FUNCT_2:def_1;
assume x in rng (M * G) ; ::_thesis: x <= M . (F . 0)
then consider n being set such that
A6: n in NAT and
A7: (M * G) . n = x by A5, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A6;
A8: x = M . (G . n) by A5, A7, FUNCT_1:12;
A9: ( ex k being Nat st n = k + 1 implies x <= M . (F . 0) )
proof
given k being Nat such that A10: n = k + 1 ; ::_thesis: x <= M . (F . 0)
reconsider k = k as Element of NAT by ORDINAL1:def_12;
G . n = (F . 0) \ (F . k) by A3, A10;
hence x <= M . (F . 0) by A8, MEASURE1:31, XBOOLE_1:36; ::_thesis: verum
end;
( n = 0 implies x <= M . (F . 0) ) by A2, A8, MEASURE1:31, XBOOLE_1:2;
hence x <= M . (F . 0) by A9, NAT_1:6; ::_thesis: verum
end;
then M . (F . 0) is UpperBound of rng (M * G) by XXREAL_2:def_1;
then A11: sup (rng (M * G)) <= M . (F . 0) by XXREAL_2:def_3;
for x being ext-real number st x in rng (M * F) holds
0. <= x
proof
let x be ext-real number ; ::_thesis: ( x in rng (M * F) implies 0. <= x )
A12: dom (M * F) = NAT by FUNCT_2:def_1;
A13: M * F is V87() by MEASURE2:1;
assume x in rng (M * F) ; ::_thesis: 0. <= x
then ex n being set st
( n in NAT & (M * F) . n = x ) by A12, FUNCT_1:def_3;
hence 0. <= x by A13, SUPINF_2:39; ::_thesis: verum
end;
then 0. is LowerBound of rng (M * F) by XXREAL_2:def_2;
then A14: inf (rng (M * F)) >= 0 by XXREAL_2:def_4;
ex x being R_eal st
( x in rng (M * F) & x = M . (F . 0) )
proof
take (M * F) . 0 ; ::_thesis: ( (M * F) . 0 in rng (M * F) & (M * F) . 0 = M . (F . 0) )
dom (M * F) = NAT by FUNCT_2:def_1;
hence ( (M * F) . 0 in rng (M * F) & (M * F) . 0 = M . (F . 0) ) by FUNCT_1:12, FUNCT_2:4; ::_thesis: verum
end;
then inf (rng (M * F)) <= M . (F . 0) by XXREAL_2:3;
hence inf (rng (M * F)) is Real by A4, A14, XXREAL_0:45; ::_thesis: sup (rng (M * G)) is Real
0. <= sup (rng (M * G))
proof
set x = (M * G) . 0;
for x being R_eal st x in rng (M * G) holds
0. <= x
proof
let x be R_eal; ::_thesis: ( x in rng (M * G) implies 0. <= x )
A15: dom (M * G) = NAT by FUNCT_2:def_1;
A16: M * G is V87() by MEASURE2:1;
assume x in rng (M * G) ; ::_thesis: 0. <= x
then ex n being set st
( n in NAT & (M * G) . n = x ) by A15, FUNCT_1:def_3;
hence 0. <= x by A16, SUPINF_2:39; ::_thesis: verum
end;
then A17: 0. <= (M * G) . 0 by FUNCT_2:4;
(M * G) . 0 <= sup (rng (M * G)) by FUNCT_2:4, XXREAL_2:4;
hence 0. <= sup (rng (M * G)) by A17, XXREAL_0:2; ::_thesis: verum
end;
hence sup (rng (M * G)) is Real by A4, A11, XXREAL_0:45; ::_thesis: verum
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 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
let X be set ; ::_thesis: for S being SigmaField 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)))
let S be SigmaField of X; ::_thesis: 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)))
let M be sigma_Measure of S; ::_thesis: 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)))
let G, F be Function of NAT,S; ::_thesis: ( 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))) )
assume that
A1: M . (F . 0) < +infty and
A2: G . 0 = {} and
A3: for n being Element of NAT holds
( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ; ::_thesis: sup (rng (M * G)) = (M . (F . 0)) - (inf (rng (M * F)))
set l = (M . (F . 0)) - (inf (rng (M * F)));
for x being ext-real number st x in rng (M * G) holds
x <= (M . (F . 0)) - (inf (rng (M * F)))
proof
let x be ext-real number ; ::_thesis: ( x in rng (M * G) implies x <= (M . (F . 0)) - (inf (rng (M * F))) )
A4: dom (M * G) = NAT by FUNCT_2:def_1;
assume x in rng (M * G) ; ::_thesis: x <= (M . (F . 0)) - (inf (rng (M * F)))
then consider n being set such that
A5: n in NAT and
A6: (M * G) . n = x by A4, FUNCT_1:def_3;
M * G is V87() by MEASURE2:1;
then x >= 0 by A5, A6, SUPINF_2:39;
then A7: x > -infty by XXREAL_0:2, XXREAL_0:12;
reconsider n = n as Element of NAT by A5;
A8: ( n = 0 implies G . n c= F . 0 ) by A2, XBOOLE_1:2;
A9: dom (M * F) = NAT by FUNCT_2:def_1;
A10: ( n = 0 implies M . ((F . 0) \ (G . n)) in rng (M * F) )
proof
assume A11: n = 0 ; ::_thesis: M . ((F . 0) \ (G . n)) in rng (M * F)
M . (F . 0) = (M * F) . 0 by A9, FUNCT_1:12;
hence M . ((F . 0) \ (G . n)) in rng (M * F) by A2, A11, FUNCT_2:4; ::_thesis: verum
end;
A12: ( ex k being Nat st n = k + 1 implies M . ((F . 0) \ (G . n)) in rng (M * F) )
proof
A13: for n being Element of NAT holds F . n c= F . 0
proof
defpred S1[ Element of NAT ] means F . $1 c= F . 0;
A14: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A15: F . k c= F . 0 ; ::_thesis: S1[k + 1]
F . (k + 1) c= F . k by A3;
hence S1[k + 1] by A15, XBOOLE_1:1; ::_thesis: verum
end;
A16: S1[ 0 ] ;
thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A16, A14); ::_thesis: verum
end;
given k being Nat such that A17: n = k + 1 ; ::_thesis: M . ((F . 0) \ (G . n)) in rng (M * F)
reconsider k = k as Element of NAT by ORDINAL1:def_12;
A18: M . (F . k) = (M * F) . k by A9, FUNCT_1:12;
(F . 0) \ (G . n) = (F . 0) \ ((F . 0) \ (F . k)) by A3, A17
.= (F . 0) /\ (F . k) by XBOOLE_1:48
.= F . k by A13, XBOOLE_1:28 ;
hence M . ((F . 0) \ (G . n)) in rng (M * F) by A18, FUNCT_2:4; ::_thesis: verum
end;
A19: ( ex k being Nat st n = k + 1 implies G . n c= F . 0 )
proof
given k being Nat such that A20: n = k + 1 ; ::_thesis: G . n c= F . 0
reconsider k = k as Element of NAT by ORDINAL1:def_12;
G . n = (F . 0) \ (F . k) by A3, A20;
hence G . n c= F . 0 by XBOOLE_1:36; ::_thesis: verum
end;
A21: x = M . (G . n) by A4, A6, FUNCT_1:12;
then x <> +infty by A1, A8, A19, MEASURE1:31, NAT_1:6;
then A22: x is Real by A7, XXREAL_0:14;
reconsider x = x as R_eal by XXREAL_0:def_1;
( M . (F . 0) is Real & inf (rng (M * F)) is Real ) by A1, A2, A3, Th9;
then consider a, b, c being Real such that
A23: a = M . (F . 0) and
A24: b = x and
A25: c = inf (rng (M * F)) by A22;
(M . (F . 0)) - x = a - b by A23, A24, SUPINF_2:3;
then A26: ((M . (F . 0)) - x) + x = (a - b) + b by A24, SUPINF_2:1
.= M . (F . 0) by A23 ;
(inf (rng (M * F))) + x = c + b by A24, A25, SUPINF_2:1;
then A27: ((inf (rng (M * F))) + x) - (inf (rng (M * F))) = (b + c) - c by A25, SUPINF_2:3
.= x by A24 ;
(M . (F . 0)) - x = M . ((F . 0) \ (G . n)) by A21, A8, A19, A22, MEASURE1:32, NAT_1:6, XXREAL_0:9;
then inf (rng (M * F)) <= (M . (F . 0)) - x by A10, A12, NAT_1:6, XXREAL_2:3;
then (inf (rng (M * F))) + x <= M . (F . 0) by A26, XXREAL_3:36;
hence x <= (M . (F . 0)) - (inf (rng (M * F))) by A27, XXREAL_3:37; ::_thesis: verum
end;
then A28: (M . (F . 0)) - (inf (rng (M * F))) is UpperBound of rng (M * G) by XXREAL_2:def_1;
A29: for n being Element of NAT holds G . n c= G . (n + 1) by A2, A3, MEASURE2:13;
for y being UpperBound of rng (M * G) holds (M . (F . 0)) - (inf (rng (M * F))) <= y
proof
let y be UpperBound of rng (M * G); ::_thesis: (M . (F . 0)) - (inf (rng (M * F))) <= y
(M . (F . 0)) - (inf (rng (M * F))) <= y
proof
for x being ext-real number st x in rng (M * F) holds
M . (meet (rng F)) <= x
proof
let x be ext-real number ; ::_thesis: ( x in rng (M * F) implies M . (meet (rng F)) <= x )
A30: dom (M * F) = NAT by FUNCT_2:def_1;
assume x in rng (M * F) ; ::_thesis: M . (meet (rng F)) <= x
then consider n being set such that
A31: n in NAT and
A32: (M * F) . n = x by A30, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A31;
A33: meet (rng F) c= F . n by FUNCT_2:4, SETFAM_1:3;
x = M . (F . n) by A30, A32, FUNCT_1:12;
hence M . (meet (rng F)) <= x by A33, MEASURE1:31; ::_thesis: verum
end;
then M . (meet (rng F)) is LowerBound of rng (M * F) by XXREAL_2:def_2;
then A34: M . (meet (rng F)) <= inf (rng (M * F)) by XXREAL_2:def_4;
set Q = union (rng G);
sup (rng (M * G)) = M . (union (rng G)) by A29, MEASURE2:23;
then A35: M . (union (rng G)) <= y by XXREAL_2:def_3;
(M . (F . 0)) - (M . (meet (rng F))) = M . (union (rng G)) by A1, A2, A3, Th7;
then (M . (F . 0)) - (inf (rng (M * F))) <= M . (union (rng G)) by A34, XXREAL_3:37;
hence (M . (F . 0)) - (inf (rng (M * F))) <= y by A35, XXREAL_0:2; ::_thesis: verum
end;
hence (M . (F . 0)) - (inf (rng (M * F))) <= y ; ::_thesis: verum
end;
hence sup (rng (M * G)) = (M . (F . 0)) - (inf (rng (M * F))) by A28, XXREAL_2:def_3; ::_thesis: verum
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 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
let X be set ; ::_thesis: for S being SigmaField 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)))
let S be SigmaField of X; ::_thesis: 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)))
let M be sigma_Measure of S; ::_thesis: 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)))
let G, F be Function of NAT,S; ::_thesis: ( 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))) )
assume that
A1: M . (F . 0) < +infty and
A2: G . 0 = {} and
A3: for n being Element of NAT holds
( G . (n + 1) = (F . 0) \ (F . n) & F . (n + 1) c= F . n ) ; ::_thesis: inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G)))
set l = (M . (F . 0)) - (sup (rng (M * G)));
for x being ext-real number st x in rng (M * F) holds
(M . (F . 0)) - (sup (rng (M * G))) <= x
proof
let x be ext-real number ; ::_thesis: ( x in rng (M * F) implies (M . (F . 0)) - (sup (rng (M * G))) <= x )
assume A4: x in rng (M * F) ; ::_thesis: (M . (F . 0)) - (sup (rng (M * G))) <= x
( x <> +infty implies (M . (F . 0)) - (sup (rng (M * G))) <= x )
proof
A5: dom (M * F) = NAT by FUNCT_2:def_1;
then consider n being set such that
A6: n in NAT and
A7: (M * F) . n = x by A4, FUNCT_1:def_3;
M * F is V87() by MEASURE2:1;
then A8: 0. <= x by A6, A7, SUPINF_2:39;
assume A9: x <> +infty ; ::_thesis: (M . (F . 0)) - (sup (rng (M * G))) <= x
reconsider x = x as R_eal by XXREAL_0:def_1;
x <= +infty by XXREAL_0:3;
then x < +infty by A9, XXREAL_0:1;
then A10: x is Real by A8, XXREAL_0:14, XXREAL_0:46;
( M . (F . 0) is Real & sup (rng (M * G)) is Real ) by A1, A2, A3, Th9;
then consider a, b, c being Real such that
A11: a = M . (F . 0) and
A12: b = x and
A13: c = sup (rng (M * G)) by A10;
(sup (rng (M * G))) + x = c + b by A12, A13, SUPINF_2:1;
then A14: ((sup (rng (M * G))) + x) - (sup (rng (M * G))) = (b + c) - c by A13, SUPINF_2:3
.= x by A12 ;
reconsider n = n as Element of NAT by A6;
A15: dom (M * G) = NAT by FUNCT_2:def_1;
A16: (M . (F . 0)) - x <= sup (rng (M * G))
proof
set k = n + 1;
A17: for n being Element of NAT holds F . n c= F . 0
proof
defpred S1[ Element of NAT ] means F . $1 c= F . 0;
A18: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A19: F . k c= F . 0 ; ::_thesis: S1[k + 1]
F . (k + 1) c= F . k by A3;
hence S1[k + 1] by A19, XBOOLE_1:1; ::_thesis: verum
end;
A20: S1[ 0 ] ;
thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A20, A18); ::_thesis: verum
end;
then M . (F . n) <= M . (F . 0) by MEASURE1:31;
then A21: M . (F . n) < +infty by A1, XXREAL_0:2;
(M . (F . 0)) - x = (M . (F . 0)) - (M . (F . n)) by A5, A7, FUNCT_1:12
.= M . ((F . 0) \ (F . n)) by A17, A21, MEASURE1:32
.= M . (G . (n + 1)) by A3 ;
then (M . (F . 0)) - x = (M * G) . (n + 1) by A15, FUNCT_1:12;
hence (M . (F . 0)) - x <= sup (rng (M * G)) by FUNCT_2:4, XXREAL_2:4; ::_thesis: verum
end;
(M . (F . 0)) - x = a - b by A11, A12, SUPINF_2:3;
then ((M . (F . 0)) - x) + x = (a - b) + b by A12, SUPINF_2:1
.= M . (F . 0) by A11 ;
then M . (F . 0) <= (sup (rng (M * G))) + x by A16, XXREAL_3:36;
hence (M . (F . 0)) - (sup (rng (M * G))) <= x by A14, XXREAL_3:37; ::_thesis: verum
end;
hence (M . (F . 0)) - (sup (rng (M * G))) <= x by XXREAL_0:4; ::_thesis: verum
end;
then A22: (M . (F . 0)) - (sup (rng (M * G))) is LowerBound of rng (M * F) by XXREAL_2:def_2;
for y being LowerBound of rng (M * F) holds y <= (M . (F . 0)) - (sup (rng (M * G)))
proof
A23: inf (rng (M * F)) is Real by A1, A2, A3, Th9;
( sup (rng (M * G)) is Real & M . (F . 0) is Real ) by A1, A2, A3, Th9;
then consider a, b, c being Real such that
A24: a = sup (rng (M * G)) and
A25: b = M . (F . 0) and
A26: c = inf (rng (M * F)) by A23;
(sup (rng (M * G))) + (inf (rng (M * F))) = a + c by A24, A26, SUPINF_2:1;
then A27: ((sup (rng (M * G))) + (inf (rng (M * F)))) - (sup (rng (M * G))) = (c + a) - a by A24, SUPINF_2:3
.= inf (rng (M * F)) by A26 ;
let y be LowerBound of rng (M * F); ::_thesis: y <= (M . (F . 0)) - (sup (rng (M * G)))
consider s, t, r being R_eal such that
s = sup (rng (M * G)) and
t = (M . (F . 0)) - (inf (rng (M * F))) and
A28: r = inf (rng (M * F)) ;
A29: sup (rng (M * G)) = (M . (F . 0)) - (inf (rng (M * F))) by A1, A2, A3, Th10;
(M . (F . 0)) - (inf (rng (M * F))) = b - c by A25, A26, SUPINF_2:3;
then ((M . (F . 0)) - (inf (rng (M * F)))) + r = (b - c) + c by A26, A28, SUPINF_2:1
.= M . (F . 0) by A25 ;
hence y <= (M . (F . 0)) - (sup (rng (M * G))) by A29, A28, A27, XXREAL_2:def_4; ::_thesis: verum
end;
hence inf (rng (M * F)) = (M . (F . 0)) - (sup (rng (M * G))) by A22, XXREAL_2:def_4; ::_thesis: verum
end;
theorem :: MEASURE3:12
for X being set
for S being SigmaField 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
let X be set ; ::_thesis: for S being SigmaField 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))
let S be SigmaField of X; ::_thesis: 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))
let M be sigma_Measure of S; ::_thesis: 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))
let F be Function of NAT,S; ::_thesis: ( ( 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)) )
assume that
A1: for n being Element of NAT holds F . (n + 1) c= F . n and
A2: M . (F . 0) < +infty ; ::_thesis: M . (meet (rng F)) = inf (rng (M * F))
consider G being Function of NAT,S such that
A3: ( G . 0 = {} & ( for n being Element of NAT holds G . (n + 1) = (F . 0) \ (F . n) ) ) by MEASURE2:9;
A4: union (rng G) = (F . 0) \ (meet (rng F)) by A1, A3, Th4;
A5: M . ((F . 0) \ (union (rng G))) = M . (meet (rng F)) by A1, A3, Th5;
A6: for A being Element of S st A = union (rng G) holds
M . (meet (rng F)) = (M . (F . 0)) - (M . A)
proof
let A be Element of S; ::_thesis: ( A = union (rng G) implies M . (meet (rng F)) = (M . (F . 0)) - (M . A) )
assume A7: A = union (rng G) ; ::_thesis: M . (meet (rng F)) = (M . (F . 0)) - (M . A)
M . ((F . 0) \ (meet (rng F))) <> +infty by A2, MEASURE1:31, XBOOLE_1:36;
then M . A < +infty by A4, A7, XXREAL_0:4;
hence M . (meet (rng F)) = (M . (F . 0)) - (M . A) by A4, A5, A7, MEASURE1:32, XBOOLE_1:36; ::_thesis: verum
end;
for n being Element of NAT holds G . n c= G . (n + 1) by A1, A3, MEASURE2:13;
then M . (union (rng G)) = sup (rng (M * G)) by MEASURE2:23;
then M . (meet (rng F)) = (M . (F . 0)) - (sup (rng (M * G))) by A6;
hence M . (meet (rng F)) = inf (rng (M * F)) by A1, A2, A3, Th11; ::_thesis: verum
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
let X be set ; ::_thesis: 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))
let S be SigmaField of X; ::_thesis: for M being Measure of S
for F being Sep_Sequence of S holds SUM (M * F) <= M . (union (rng F))
let M be Measure of S; ::_thesis: for F being Sep_Sequence of S holds SUM (M * F) <= M . (union (rng F))
let F be Sep_Sequence of S; ::_thesis: SUM (M * F) <= M . (union (rng F))
set T = rng F;
consider G being Function of NAT,S such that
A1: G . 0 = F . 0 and
A2: for n being Element of NAT holds G . (n + 1) = (F . (n + 1)) \/ (G . n) by MEASURE2:4;
{} is Subset of X by XBOOLE_1:2;
then consider H being Function of NAT,(bool X) such that
A3: rng H = {(union (rng F)),{}} and
A4: H . 0 = union (rng F) and
A5: for n being Element of NAT st 0 < n holds
H . n = {} by MEASURE1:19;
rng H c= S
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng H or a in S )
assume a in rng H ; ::_thesis: a in S
then ( a = union (rng F) or a = {} ) by A3, TARSKI:def_2;
hence a in S by PROB_1:4; ::_thesis: verum
end;
then reconsider H = H as Function of NAT,S by FUNCT_2:6;
defpred S1[ Element of NAT ] means (Ser (M * F)) . $1 = M . (G . $1);
A6: dom (M * F) = NAT by FUNCT_2:def_1;
A7: for n being Element of NAT holds (G . n) /\ (F . (n + 1)) = {}
proof
let n be Element of NAT ; ::_thesis: (G . n) /\ (F . (n + 1)) = {}
A8: for n, k being Element of NAT st n < k holds
(G . n) /\ (F . k) = {}
proof
defpred S2[ Element of NAT ] means for k being Element of NAT st $1 < k holds
(G . $1) /\ (F . k) = {} ;
A9: for n being Element of NAT st S2[n] holds
S2[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] )
assume A10: for k being Element of NAT st n < k holds
(G . n) /\ (F . k) = {} ; ::_thesis: S2[n + 1]
let k be Element of NAT ; ::_thesis: ( n + 1 < k implies (G . (n + 1)) /\ (F . k) = {} )
assume A11: n + 1 < k ; ::_thesis: (G . (n + 1)) /\ (F . k) = {}
then A12: n < k by NAT_1:13;
F . (n + 1) misses F . k by A11, PROB_2:def_2;
then A13: (F . (n + 1)) /\ (F . k) = {} by XBOOLE_0:def_7;
(G . (n + 1)) /\ (F . k) = ((F . (n + 1)) \/ (G . n)) /\ (F . k) by A2
.= ((F . (n + 1)) /\ (F . k)) \/ ((G . n) /\ (F . k)) by XBOOLE_1:23 ;
hence (G . (n + 1)) /\ (F . k) = {} by A10, A12, A13; ::_thesis: verum
end;
A14: S2[ 0 ]
proof
let k be Element of NAT ; ::_thesis: ( 0 < k implies (G . 0) /\ (F . k) = {} )
assume 0 < k ; ::_thesis: (G . 0) /\ (F . k) = {}
then F . 0 misses F . k by PROB_2:def_2;
hence (G . 0) /\ (F . k) = {} by A1, XBOOLE_0:def_7; ::_thesis: verum
end;
thus for n being Element of NAT holds S2[n] from NAT_1:sch_1(A14, A9); ::_thesis: verum
end;
n < n + 1 by NAT_1:13;
hence (G . n) /\ (F . (n + 1)) = {} by A8; ::_thesis: verum
end;
A15: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
(G . k) /\ (F . (k + 1)) = {} by A7;
then A16: G . k misses F . (k + 1) by XBOOLE_0:def_7;
assume (Ser (M * F)) . k = M . (G . k) ; ::_thesis: S1[k + 1]
then (Ser (M * F)) . (k + 1) = (M . (G . k)) + ((M * F) . (k + 1)) by SUPINF_2:44;
then (Ser (M * F)) . (k + 1) = (M . (G . k)) + (M . (F . (k + 1))) by A6, FUNCT_1:12
.= M . ((F . (k + 1)) \/ (G . k)) by A16, MEASURE1:def_3
.= M . (G . (k + 1)) by A2 ;
hence S1[k + 1] ; ::_thesis: verum
end;
(Ser (M * F)) . 0 = (M * F) . 0 by SUPINF_2:44;
then A17: S1[ 0 ] by A1, A6, FUNCT_1:12;
A18: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A17, A15);
defpred S2[ Element of NAT ] means (Ser (M * H)) . $1 = M . (union (rng F));
A19: for n being Element of NAT st S2[n] holds
S2[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] )
0 <= n by NAT_1:2;
then 0 < n + 1 by NAT_1:13;
then A20: H . (n + 1) = {} by A5;
dom (M * H) = NAT by FUNCT_2:def_1;
then (M * H) . (n + 1) = M . {} by A20, FUNCT_1:12;
then A21: (M * H) . (n + 1) = 0. by VALUED_0:def_19;
assume (Ser (M * H)) . n = M . (union (rng F)) ; ::_thesis: S2[n + 1]
then (Ser (M * H)) . (n + 1) = (M . (union (rng F))) + ((M * H) . (n + 1)) by SUPINF_2:44;
hence S2[n + 1] by A21, XXREAL_3:4; ::_thesis: verum
end;
( (Ser (M * H)) . 0 = (M * H) . 0 & dom (M * H) = NAT ) by FUNCT_2:def_1, SUPINF_2:44;
then A22: S2[ 0 ] by A4, FUNCT_1:12;
A23: for n being Element of NAT holds S2[n] from NAT_1:sch_1(A22, A19);
A24: for r being Element of NAT st 1 <= r holds
(M * H) . r = 0.
proof
let r be Element of NAT ; ::_thesis: ( 1 <= r implies (M * H) . r = 0. )
assume 1 <= r ; ::_thesis: (M * H) . r = 0.
then 0 + 1 <= r ;
then 0 < r by NAT_1:13;
then A25: H . r = {} by A5;
dom (M * H) = NAT by FUNCT_2:def_1;
then (M * H) . r = M . {} by A25, FUNCT_1:12;
hence (M * H) . r = 0. by VALUED_0:def_19; ::_thesis: verum
end;
A26: for n being Element of NAT holds G . n c= union (rng F)
proof
defpred S3[ Element of NAT ] means G . $1 c= union (rng F);
A27: for n being Element of NAT st S3[n] holds
S3[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S3[n] implies S3[n + 1] )
assume A28: G . n c= union (rng F) ; ::_thesis: S3[n + 1]
( G . (n + 1) = (F . (n + 1)) \/ (G . n) & F . (n + 1) c= union (rng F) ) by A2, FUNCT_2:4, ZFMISC_1:74;
hence S3[n + 1] by A28, XBOOLE_1:8; ::_thesis: verum
end;
A29: S3[ 0 ] by A1, FUNCT_2:4, ZFMISC_1:74;
thus for n being Element of NAT holds S3[n] from NAT_1:sch_1(A29, A27); ::_thesis: verum
end;
A30: for n being Element of NAT holds (Ser (M * F)) . n <= (Ser (M * H)) . n
proof
let n be Element of NAT ; ::_thesis: (Ser (M * F)) . n <= (Ser (M * H)) . n
(Ser (M * F)) . n = M . (G . n) by A18;
then (Ser (M * F)) . n <= M . (union (rng F)) by A26, MEASURE1:8;
hence (Ser (M * F)) . n <= (Ser (M * H)) . n by A23; ::_thesis: verum
end;
M * H is V87() by MEASURE1:25;
then SUM (M * H) = (Ser (M * H)) . 1 by A24, SUPINF_2:48;
then SUM (M * H) = M . (union (rng F)) by A23;
hence SUM (M * F) <= M . (union (rng F)) by A30, Th1; ::_thesis: verum
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
let X be set ; ::_thesis: 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
let S be SigmaField of X; ::_thesis: 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
let M be Measure of S; ::_thesis: ( ( for F being Sep_Sequence of S holds M . (union (rng F)) <= SUM (M * F) ) implies M is sigma_Measure of S )
assume A1: for F being Sep_Sequence of S holds M . (union (rng F)) <= SUM (M * F) ; ::_thesis: M is sigma_Measure of S
for F being Sep_Sequence of S holds SUM (M * F) = M . (union (rng F))
proof
let F be Sep_Sequence of S; ::_thesis: SUM (M * F) = M . (union (rng F))
( M . (union (rng F)) <= SUM (M * F) & SUM (M * F) <= M . (union (rng F)) ) by A1, Th13;
hence SUM (M * F) = M . (union (rng F)) by XXREAL_0:1; ::_thesis: verum
end;
hence M is sigma_Measure of S by MEASURE1:def_6; ::_thesis: verum
end;
definition
let X be set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
predM is_complete S means :Def1: :: MEASURE3:def 1
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 Def1 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 );
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 b1 being Subset of X ex B being set st
( B in S & b1 c= B & M . B = 0. )
proof
reconsider A = {} as Subset of X by XBOOLE_1:2;
take A ; ::_thesis: ex B being set st
( B in S & A c= B & M . B = 0. )
take B = {} ; ::_thesis: ( B in S & A c= B & M . B = 0. )
thus B in S by PROB_1:4; ::_thesis: ( A c= B & M . B = 0. )
thus A c= B ; ::_thesis: M . B = 0.
thus M . B = 0. by VALUED_0:def_19; ::_thesis: verum
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 b4 being Subset of X holds
( b4 is thin of M iff ex B being set st
( B in S & b4 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 b1 being non empty Subset-Family of X st
for A being set holds
( A in b1 iff ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) )
proof
A1: ex B being set st
( B in S & {} c= B & M . B = 0. )
proof
consider B being set such that
A2: ( B = {} & B in S ) by PROB_1:4;
take B ; ::_thesis: ( B in S & {} c= B & M . B = 0. )
thus ( B in S & {} c= B & M . B = 0. ) by A2, VALUED_0:def_19; ::_thesis: verum
end;
A3: {} is Subset of X by XBOOLE_1:2;
A4: for A being set st A = {} holds
ex B being set st
( B in S & ex C being thin of M st A = B \/ C )
proof
reconsider C = {} as thin of M by A3, A1, Def2;
let A be set ; ::_thesis: ( A = {} implies ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) )
consider B being set such that
A5: B = {} and
A6: B in S by PROB_1:4;
assume A = {} ; ::_thesis: ex B being set st
( B in S & ex C being thin of M st A = B \/ C )
then A = B \/ C by A5;
hence ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) by A6; ::_thesis: verum
end;
defpred S1[ set ] means for A being set st A = $1 holds
ex B being set st
( B in S & ex C being thin of M st A = B \/ C );
consider D being set such that
A7: for y being set holds
( y in D iff ( y in bool X & S1[y] ) ) from XBOOLE_0:sch_1();
A8: 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 ) )
proof
let A be set ; ::_thesis: ( A in D iff ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) )
A9: ( A in D iff ( A in bool X & ( for y being set st y = A holds
ex B being set st
( B in S & ex C being thin of M st y = B \/ C ) ) ) ) by A7;
( ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) implies A in D )
proof
assume A10: ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) ; ::_thesis: A in D
then A c= X by XBOOLE_1:8;
hence A in D by A9, A10; ::_thesis: verum
end;
hence ( A in D iff ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) ) by A7; ::_thesis: verum
end;
A11: D c= bool X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in bool X )
assume x in D ; ::_thesis: x in bool X
hence x in bool X by A7; ::_thesis: verum
end;
{} c= X by XBOOLE_1:2;
then reconsider D = D as non empty Subset-Family of X by A7, A11, A4;
take D ; ::_thesis: 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 ) )
thus 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 ) ) by A8; ::_thesis: verum
end;
uniqueness
for b1, b2 being non empty Subset-Family of X st ( for A being set holds
( A in b1 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 b2 iff ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) ) ) holds
b1 = b2
proof
let D1, D2 be non empty Subset-Family of X; ::_thesis: ( ( for A being set holds
( A in D1 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 D2 iff ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) ) ) implies D1 = D2 )
assume that
A12: for A being set holds
( A in D1 iff ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) ) and
A13: for A being set holds
( A in D2 iff ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) ) ; ::_thesis: D1 = D2
for A being set holds
( A in D1 iff A in D2 )
proof
let A be set ; ::_thesis: ( A in D1 iff A in D2 )
thus ( A in D1 implies A in D2 ) ::_thesis: ( A in D2 implies A in D1 )
proof
assume A in D1 ; ::_thesis: A in D2
then ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) by A12;
hence A in D2 by A13; ::_thesis: verum
end;
assume A in D2 ; ::_thesis: A in D1
then ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) by A13;
hence A in D1 by A12; ::_thesis: verum
end;
hence D1 = D2 by TARSKI:1; ::_thesis: verum
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 b4 being non empty Subset-Family of X holds
( b4 = COM (S,M) iff for A being set holds
( A in b4 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 b1 being non empty Subset-Family of X st
for B being set holds
( B in b1 iff ( B in S & B c= A & A \ B is thin of M ) )
proof
defpred S1[ set ] means for t being set st t = $1 holds
( t in S & t c= A & A \ t is thin of M );
consider D being set such that
A1: for t being set holds
( t in D iff ( t in bool X & S1[t] ) ) from XBOOLE_0:sch_1();
A2: for B being set holds
( B in D iff ( B in S & B c= A & A \ B is thin of M ) )
proof
let B be set ; ::_thesis: ( B in D iff ( B in S & B c= A & A \ B is thin of M ) )
( B in S & B c= A & A \ B is thin of M implies B in D )
proof
assume that
A3: B in S and
A4: ( B c= A & A \ B is thin of M ) ; ::_thesis: B in D
for t being set st t = B holds
( t in S & t c= A & A \ t is thin of M ) by A3, A4;
hence B in D by A1, A3; ::_thesis: verum
end;
hence ( B in D iff ( B in S & B c= A & A \ B is thin of M ) ) by A1; ::_thesis: verum
end;
A5: D c= bool X
proof
let B be set ; :: according to TARSKI:def_3 ::_thesis: ( not B in D or B in bool X )
assume B in D ; ::_thesis: B in bool X
then B in S by A2;
hence B in bool X ; ::_thesis: verum
end;
D <> {}
proof
consider B being set such that
A6: B in S and
A7: ex C being thin of M st A = B \/ C by Def3;
consider C being thin of M such that
A8: A = B \/ C by A7;
consider E being set such that
A9: E in S and
A10: C c= E and
A11: M . E = 0. by Def2;
A \ B = C \ B by A8, XBOOLE_1:40;
then A \ B c= C by XBOOLE_1:36;
then A \ B c= E by A10, XBOOLE_1:1;
then A12: A \ B is thin of M by A9, A11, Def2;
B c= A by A8, XBOOLE_1:7;
hence D <> {} by A2, A6, A12; ::_thesis: verum
end;
then reconsider D = D as non empty Subset-Family of X by A5;
take D ; ::_thesis: for B being set holds
( B in D iff ( B in S & B c= A & A \ B is thin of M ) )
thus for B being set holds
( B in D iff ( B in S & B c= A & A \ B is thin of M ) ) by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being non empty Subset-Family of X st ( for B being set holds
( B in b1 iff ( B in S & B c= A & A \ B is thin of M ) ) ) & ( for B being set holds
( B in b2 iff ( B in S & B c= A & A \ B is thin of M ) ) ) holds
b1 = b2
proof
let D1, D2 be non empty Subset-Family of X; ::_thesis: ( ( for B being set holds
( B in D1 iff ( B in S & B c= A & A \ B is thin of M ) ) ) & ( for B being set holds
( B in D2 iff ( B in S & B c= A & A \ B is thin of M ) ) ) implies D1 = D2 )
assume that
A13: for B being set holds
( B in D1 iff ( B in S & B c= A & A \ B is thin of M ) ) and
A14: for B being set holds
( B in D2 iff ( B in S & B c= A & A \ B is thin of M ) ) ; ::_thesis: D1 = D2
for B being set holds
( B in D1 iff B in D2 )
proof
let B be set ; ::_thesis: ( B in D1 iff B in D2 )
thus ( B in D1 implies B in D2 ) ::_thesis: ( B in D2 implies B in D1 )
proof
assume A15: B in D1 ; ::_thesis: B in D2
then A16: A \ B is thin of M by A13;
( B in S & B c= A ) by A13, A15;
hence B in D2 by A14, A16; ::_thesis: verum
end;
assume A17: B in D2 ; ::_thesis: B in D1
then A18: A \ B is thin of M by A14;
( B in S & B c= A ) by A14, A17;
hence B in D1 by A13, A18; ::_thesis: verum
end;
hence D1 = D2 by TARSKI:1; ::_thesis: verum
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 b5 being non empty Subset-Family of X holds
( b5 = MeasPart A iff for B being set holds
( B in b5 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 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
let X be set ; ::_thesis: for S being SigmaField 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)
let S be SigmaField of X; ::_thesis: 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)
let M be sigma_Measure of S; ::_thesis: 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)
let F be Function of NAT,(COM (S,M)); ::_thesis: ex G being Function of NAT,S st
for n being Element of NAT holds G . n in MeasPart (F . n)
defpred S1[ Element of NAT , set ] means for n being Element of NAT
for y being set st n = $1 & y = $2 holds
y in MeasPart (F . n);
A1: for t being Element of NAT ex A being Element of S st S1[t,A]
proof
let t be Element of NAT ; ::_thesis: ex A being Element of S st S1[t,A]
set A = the Element of MeasPart (F . t);
reconsider A = the Element of MeasPart (F . t) as Element of S by Def4;
take A ; ::_thesis: S1[t,A]
thus S1[t,A] ; ::_thesis: verum
end;
ex G being Function of NAT,S st
for t being Element of NAT holds S1[t,G . t] from FUNCT_2:sch_3(A1);
then consider G being Function of NAT,S such that
A2: for t, n being Element of NAT
for y being set st n = t & y = G . t holds
y in MeasPart (F . n) ;
take G ; ::_thesis: for n being Element of NAT holds G . n in MeasPart (F . n)
thus for n being Element of NAT holds G . n in MeasPart (F . n) by A2; ::_thesis: verum
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 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
let X be set ; ::_thesis: for S being SigmaField 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)
let S be SigmaField of X; ::_thesis: 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)
let M be sigma_Measure of S; ::_thesis: 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)
let F be Function of NAT,(COM (S,M)); ::_thesis: 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)
let G be Function of NAT,S; ::_thesis: ex H being Function of NAT,(bool X) st
for n being Element of NAT holds H . n = (F . n) \ (G . n)
defpred S1[ Element of NAT , set ] means for n being Element of NAT
for y being set st n = $1 & y = $2 holds
y = (F . n) \ (G . n);
A1: for t being Element of NAT ex A being Subset of X st S1[t,A]
proof
let t be Element of NAT ; ::_thesis: ex A being Subset of X st S1[t,A]
F . t is Element of COM (S,M) ;
then reconsider A = (F . t) \ (G . t) as Subset of X by XBOOLE_1:1;
take A ; ::_thesis: S1[t,A]
thus S1[t,A] ; ::_thesis: verum
end;
ex H being Function of NAT,(bool X) st
for t being Element of NAT holds S1[t,H . t] from FUNCT_2:sch_3(A1);
then consider H being Function of NAT,(bool X) such that
A2: for t, n being Element of NAT
for y being set st n = t & y = H . t holds
y = (F . n) \ (G . n) ;
take H ; ::_thesis: for n being Element of NAT holds H . n = (F . n) \ (G . n)
thus for n being Element of NAT holds H . n = (F . n) \ (G . n) by A2; ::_thesis: verum
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 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
let X be set ; ::_thesis: for S being SigmaField 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. )
let S be SigmaField of X; ::_thesis: 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. )
let M be sigma_Measure of S; ::_thesis: 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. )
let F be Function of NAT,(bool X); ::_thesis: ( ( for n being Element of NAT holds F . n is thin of M ) implies ex G being Function of NAT,S st
for n being Element of NAT holds
( F . n c= G . n & M . (G . n) = 0. ) )
defpred S1[ Element of NAT , set ] means for n being Element of NAT
for y being set st n = $1 & y = $2 holds
( y in S & F . n c= y & M . y = 0. );
assume A1: for n being Element of NAT holds F . n is thin of M ; ::_thesis: ex G being Function of NAT,S st
for n being Element of NAT holds
( F . n c= G . n & M . (G . n) = 0. )
A2: for t being Element of NAT ex A being Element of S st S1[t,A]
proof
let t be Element of NAT ; ::_thesis: ex A being Element of S st S1[t,A]
F . t is thin of M by A1;
then consider A being set such that
A3: A in S and
A4: ( F . t c= A & M . A = 0. ) by Def2;
reconsider A = A as Element of S by A3;
take A ; ::_thesis: S1[t,A]
thus S1[t,A] by A4; ::_thesis: verum
end;
ex G being Function of NAT,S st
for t being Element of NAT holds S1[t,G . t] from FUNCT_2:sch_3(A2);
then consider G being Function of NAT,S such that
A5: for t, n being Element of NAT
for y being set st n = t & y = G . t holds
( y in S & F . n c= y & M . y = 0. ) ;
take G ; ::_thesis: for n being Element of NAT holds
( F . n c= G . n & M . (G . n) = 0. )
thus for n being Element of NAT holds
( F . n c= G . n & M . (G . n) = 0. ) by A5; ::_thesis: verum
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
let X be set ; ::_thesis: 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
let S be SigmaField of X; ::_thesis: 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
let M be sigma_Measure of S; ::_thesis: 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
let D be non empty Subset-Family of X; ::_thesis: ( ( 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 SigmaField of X )
assume A1: 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 ) ) ; ::_thesis: D is SigmaField of X
A2: for K being N_Sub_set_fam of X st K c= D holds
union K in D
proof
let K be N_Sub_set_fam of X; ::_thesis: ( K c= D implies union K in D )
consider F being Function of NAT,(bool X) such that
A3: K = rng F by SUPINF_2:def_8;
assume A4: K c= D ; ::_thesis: union K in D
A5: for n being Element of NAT holds F . n in D
proof
let n be Element of NAT ; ::_thesis: F . n in D
F . n in K by A3, FUNCT_2:4;
hence F . n in D by A4; ::_thesis: verum
end;
A6: for n being Element of NAT ex B being set st
( B in S & ex C being thin of M st F . n = B \/ C )
proof
let n be Element of NAT ; ::_thesis: ex B being set st
( B in S & ex C being thin of M st F . n = B \/ C )
F . n in D by A5;
hence ex B being set st
( B in S & ex C being thin of M st F . n = B \/ C ) by A1; ::_thesis: verum
end;
for n being Element of NAT holds F . n in COM (S,M)
proof
let n be Element of NAT ; ::_thesis: F . n in COM (S,M)
ex B being set st
( B in S & ex C being thin of M st F . n = B \/ C ) by A6;
hence F . n in COM (S,M) by Def3; ::_thesis: verum
end;
then A7: for n being set st n in NAT holds
F . n in COM (S,M) ;
A8: dom F = NAT by FUNCT_2:def_1;
then reconsider F = F as Function of NAT,(COM (S,M)) by A7, FUNCT_2:3;
consider G being Function of NAT,S such that
A9: for n being Element of NAT holds G . n in MeasPart (F . n) by Th15;
consider H being Function of NAT,(bool X) such that
A10: for n being Element of NAT holds H . n = (F . n) \ (G . n) by Th16;
A11: for n being Element of NAT holds
( G . n in S & G . n c= F . n & (F . n) \ (G . n) is thin of M )
proof
let n be Element of NAT ; ::_thesis: ( G . n in S & G . n c= F . n & (F . n) \ (G . n) is thin of M )
G . n in MeasPart (F . n) by A9;
hence ( G . n in S & G . n c= F . n & (F . n) \ (G . n) is thin of M ) by Def4; ::_thesis: verum
end;
for n being Element of NAT holds H . n is thin of M
proof
let n be Element of NAT ; ::_thesis: H . n is thin of M
(F . n) \ (G . n) is thin of M by A11;
hence H . n is thin of M by A10; ::_thesis: verum
end;
then consider L being Function of NAT,S such that
A12: for n being Element of NAT holds
( H . n c= L . n & M . (L . n) = 0. ) by Th17;
ex B being set st
( B in S & ex C being thin of M st union K = B \/ C )
proof
set B = union (rng G);
take union (rng G) ; ::_thesis: ( union (rng G) in S & ex C being thin of M st union K = (union (rng G)) \/ C )
A13: union (rng G) c= union (rng F)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng G) or x in union (rng F) )
assume x in union (rng G) ; ::_thesis: x in union (rng F)
then consider Z being set such that
A14: x in Z and
A15: Z in rng G by TARSKI:def_4;
dom G = NAT by FUNCT_2:def_1;
then consider n being set such that
A16: n in NAT and
A17: Z = G . n by A15, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A16;
set P = F . n;
A18: G . n c= F . n by A11;
ex P being set st
( P in rng F & x in P )
proof
take F . n ; ::_thesis: ( F . n in rng F & x in F . n )
thus ( F . n in rng F & x in F . n ) by A8, A14, A17, A18, FUNCT_1:def_3; ::_thesis: verum
end;
hence x in union (rng F) by TARSKI:def_4; ::_thesis: verum
end;
ex C being thin of M st union K = (union (rng G)) \/ C
proof
for A being set st A in rng L holds
A is measure_zero of M
proof
let A be set ; ::_thesis: ( A in rng L implies A is measure_zero of M )
assume A19: A in rng L ; ::_thesis: A is measure_zero of M
dom L = NAT by FUNCT_2:def_1;
then A20: ex n being set st
( n in NAT & A = L . n ) by A19, FUNCT_1:def_3;
rng L c= S by MEASURE2:def_1;
then reconsider A = A as Element of S by A19;
M . A = 0. by A12, A20;
hence A is measure_zero of M by MEASURE1:def_7; ::_thesis: verum
end;
then union (rng L) is measure_zero of M by MEASURE2:14;
then A21: M . (union (rng L)) = 0. by MEASURE1:def_7;
set C = (union K) \ (union (rng G));
A22: union K = ((union K) \ (union (rng G))) \/ ((union (rng F)) /\ (union (rng G))) by A3, XBOOLE_1:51
.= (union (rng G)) \/ ((union K) \ (union (rng G))) by A13, XBOOLE_1:28 ;
reconsider C = (union K) \ (union (rng G)) as Subset of X ;
A23: C c= union (rng H)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C or x in union (rng H) )
assume A24: x in C ; ::_thesis: x in union (rng H)
then x in union (rng F) by A3, XBOOLE_0:def_5;
then consider Z being set such that
A25: x in Z and
A26: Z in rng F by TARSKI:def_4;
consider n being set such that
A27: n in NAT and
A28: Z = F . n by A8, A26, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A27;
A29: not x in union (rng G) by A24, XBOOLE_0:def_5;
not x in G . n
proof
dom G = NAT by FUNCT_2:def_1;
then A30: G . n in rng G by FUNCT_1:def_3;
assume x in G . n ; ::_thesis: contradiction
hence contradiction by A29, A30, TARSKI:def_4; ::_thesis: verum
end;
then A31: x in (F . n) \ (G . n) by A25, A28, XBOOLE_0:def_5;
ex Z being set st
( x in Z & Z in rng H )
proof
take H . n ; ::_thesis: ( x in H . n & H . n in rng H )
dom H = NAT by FUNCT_2:def_1;
hence ( x in H . n & H . n in rng H ) by A10, A31, FUNCT_1:def_3; ::_thesis: verum
end;
hence x in union (rng H) by TARSKI:def_4; ::_thesis: verum
end;
union (rng H) c= union (rng L)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng H) or x in union (rng L) )
assume x in union (rng H) ; ::_thesis: x in union (rng L)
then consider Z being set such that
A32: x in Z and
A33: Z in rng H by TARSKI:def_4;
dom H = NAT by FUNCT_2:def_1;
then consider n being set such that
A34: n in NAT and
A35: Z = H . n by A33, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A34;
n in dom L by A34, FUNCT_2:def_1;
then A36: L . n in rng L by FUNCT_1:def_3;
H . n c= L . n by A12;
hence x in union (rng L) by A32, A35, A36, TARSKI:def_4; ::_thesis: verum
end;
then C c= union (rng L) by A23, XBOOLE_1:1;
then C is thin of M by A21, Def2;
then consider C being thin of M such that
A37: union K = (union (rng G)) \/ C by A22;
take C ; ::_thesis: union K = (union (rng G)) \/ C
thus union K = (union (rng G)) \/ C by A37; ::_thesis: verum
end;
hence ( union (rng G) in S & ex C being thin of M st union K = (union (rng G)) \/ C ) ; ::_thesis: verum
end;
hence union K in D by A1; ::_thesis: verum
end;
for A being set st A in D holds
X \ A in D
proof
let A be set ; ::_thesis: ( A in D implies X \ A in D )
assume A38: A in D ; ::_thesis: X \ A in D
ex Q being set st
( Q in S & ex W being thin of M st X \ A = Q \/ W )
proof
consider B being set such that
A39: B in S and
A40: ex C being thin of M st A = B \/ C by A1, A38;
set P = X \ B;
consider C being thin of M such that
A41: A = B \/ C by A40;
consider G being set such that
A42: G in S and
A43: C c= G and
A44: M . G = 0. by Def2;
set Q = (X \ B) \ G;
A45: X \ A = (X \ B) \ C by A41, XBOOLE_1:41;
A46: ex W being thin of M st X \ A = ((X \ B) \ G) \/ W
proof
set W = (X \ B) /\ (G \ C);
(X \ B) /\ (G \ C) c= X \ B by XBOOLE_1:17;
then reconsider W = (X \ B) /\ (G \ C) as Subset of X by XBOOLE_1:1;
reconsider W = W as thin of M by A42, A44, Def2;
take W ; ::_thesis: X \ A = ((X \ B) \ G) \/ W
thus X \ A = ((X \ B) \ G) \/ W by A43, A45, XBOOLE_1:117; ::_thesis: verum
end;
take (X \ B) \ G ; ::_thesis: ( (X \ B) \ G in S & ex W being thin of M st X \ A = ((X \ B) \ G) \/ W )
X \ B in S by A39, MEASURE1:def_1;
hence ( (X \ B) \ G in S & ex W being thin of M st X \ A = ((X \ B) \ G) \/ W ) by A42, A46, MEASURE1:6; ::_thesis: verum
end;
hence X \ A in D by A1; ::_thesis: verum
end;
then reconsider D9 = D as non empty compl-closed sigma-additive Subset-Family of X by A2, MEASURE1:def_1, MEASURE1:def_5;
D9 is SigmaField of X ;
hence D is SigmaField of X ; ::_thesis: verum
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
for A being set holds
( A in COM (S,M) iff ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) ) by Def3;
hence ( COM (S,M) is sigma-additive & COM (S,M) is compl-closed & not COM (S,M) is empty ) by Th18; ::_thesis: verum
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
let X be set ; ::_thesis: 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
let S be SigmaField of X; ::_thesis: 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
let M be sigma_Measure of S; ::_thesis: 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
let B1, B2 be set ; ::_thesis: ( B1 in S & B2 in S implies for C1, C2 being thin of M st B1 \/ C1 = B2 \/ C2 holds
M . B1 = M . B2 )
assume A1: ( B1 in S & B2 in S ) ; ::_thesis: for C1, C2 being thin of M st B1 \/ C1 = B2 \/ C2 holds
M . B1 = M . B2
let C1, C2 be thin of M; ::_thesis: ( B1 \/ C1 = B2 \/ C2 implies M . B1 = M . B2 )
assume A2: B1 \/ C1 = B2 \/ C2 ; ::_thesis: M . B1 = M . B2
then A3: B1 c= B2 \/ C2 by XBOOLE_1:7;
A4: B2 c= B1 \/ C1 by A2, XBOOLE_1:7;
consider D1 being set such that
A5: D1 in S and
A6: C1 c= D1 and
A7: M . D1 = 0. by Def2;
A8: B1 \/ C1 c= B1 \/ D1 by A6, XBOOLE_1:9;
consider D2 being set such that
A9: D2 in S and
A10: C2 c= D2 and
A11: M . D2 = 0. by Def2;
A12: B2 \/ C2 c= B2 \/ D2 by A10, XBOOLE_1:9;
reconsider B1 = B1, B2 = B2, D1 = D1, D2 = D2 as Element of S by A1, A5, A9;
A13: ( M . (B1 \/ D1) <= (M . B1) + (M . D1) & (M . B1) + (M . D1) = M . B1 ) by A7, MEASURE1:33, XXREAL_3:4;
M . B2 <= M . (B1 \/ D1) by A4, A8, MEASURE1:31, XBOOLE_1:1;
then A14: M . B2 <= M . B1 by A13, XXREAL_0:2;
A15: ( M . (B2 \/ D2) <= (M . B2) + (M . D2) & (M . B2) + (M . D2) = M . B2 ) by A11, MEASURE1:33, XXREAL_3:4;
M . B1 <= M . (B2 \/ D2) by A3, A12, MEASURE1:31, XBOOLE_1:1;
then M . B1 <= M . B2 by A15, XXREAL_0:2;
hence M . B1 = M . B2 by A14, XXREAL_0:1; ::_thesis: verum
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 b1 being sigma_Measure of (COM (S,M)) st
for B being set st B in S holds
for C being thin of M holds b1 . (B \/ C) = M . B
proof
set B = {} ;
defpred S1[ set , set ] means for x, y being set st x in COM (S,M) & x = $1 & y = $2 holds
for B being set st B in S holds
for C being thin of M st x = B \/ C holds
y = M . B;
A1: ex B1 being set st
( B1 in S & {} c= B1 & M . B1 = 0. )
proof
take {} ; ::_thesis: ( {} in S & {} c= {} & M . {} = 0. )
thus ( {} in S & {} c= {} & M . {} = 0. ) by PROB_1:4, VALUED_0:def_19; ::_thesis: verum
end;
{} is Subset of X by XBOOLE_1:2;
then reconsider C = {} as thin of M by A1, Def2;
A2: for x being set st x in COM (S,M) holds
ex y being set st
( y in ExtREAL & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in COM (S,M) implies ex y being set st
( y in ExtREAL & S1[x,y] ) )
assume x in COM (S,M) ; ::_thesis: ex y being set st
( y in ExtREAL & S1[x,y] )
then consider B being set such that
A3: ( B in S & ex C being thin of M st x = B \/ C ) by Def3;
take M . B ; ::_thesis: ( M . B in ExtREAL & S1[x,M . B] )
thus ( M . B in ExtREAL & S1[x,M . B] ) by A3, Th19; ::_thesis: verum
end;
consider comM being Function of (COM (S,M)),ExtREAL such that
A4: for x being set st x in COM (S,M) holds
S1[x,comM . x] from FUNCT_2:sch_1(A2);
A5: for B being set st B in S holds
for C being thin of M holds comM . (B \/ C) = M . B
proof
let B be set ; ::_thesis: ( B in S implies for C being thin of M holds comM . (B \/ C) = M . B )
assume A6: B in S ; ::_thesis: for C being thin of M holds comM . (B \/ C) = M . B
let C be thin of M; ::_thesis: comM . (B \/ C) = M . B
B \/ C in COM (S,M) by A6, Def3;
hence comM . (B \/ C) = M . B by A4, A6; ::_thesis: verum
end;
A7: for F being Sep_Sequence of (COM (S,M)) holds SUM (comM * F) = comM . (union (rng F))
proof
let F be Sep_Sequence of (COM (S,M)); ::_thesis: SUM (comM * F) = comM . (union (rng F))
consider G being Function of NAT,S such that
A8: for n being Element of NAT holds G . n in MeasPart (F . n) by Th15;
consider H being Function of NAT,(bool X) such that
A9: for n being Element of NAT holds H . n = (F . n) \ (G . n) by Th16;
A10: for n being Element of NAT holds
( G . n in S & G . n c= F . n & (F . n) \ (G . n) is thin of M )
proof
let n be Element of NAT ; ::_thesis: ( G . n in S & G . n c= F . n & (F . n) \ (G . n) is thin of M )
G . n in MeasPart (F . n) by A8;
hence ( G . n in S & G . n c= F . n & (F . n) \ (G . n) is thin of M ) by Def4; ::_thesis: verum
end;
for n being Element of NAT holds H . n is thin of M
proof
let n be Element of NAT ; ::_thesis: H . n is thin of M
(F . n) \ (G . n) is thin of M by A10;
hence H . n is thin of M by A9; ::_thesis: verum
end;
then consider L being Function of NAT,S such that
A11: for n being Element of NAT holds
( H . n c= L . n & M . (L . n) = 0. ) by Th17;
A12: for n, m being set st n <> m holds
G . n misses G . m
proof
let n, m be set ; ::_thesis: ( n <> m implies G . n misses G . m )
A13: dom F = NAT by FUNCT_2:def_1
.= dom G by FUNCT_2:def_1 ;
for n being set holds G . n c= F . n
proof
let n be set ; ::_thesis: G . n c= F . n
percases ( n in dom F or not n in dom F ) ;
suppose n in dom F ; ::_thesis: G . n c= F . n
hence G . n c= F . n by A10; ::_thesis: verum
end;
supposeA14: not n in dom F ; ::_thesis: G . n c= F . n
then F . n = {} by FUNCT_1:def_2
.= G . n by A13, A14, FUNCT_1:def_2 ;
hence G . n c= F . n ; ::_thesis: verum
end;
end;
end;
then A15: ( G . n c= F . n & G . m c= F . m ) ;
assume n <> m ; ::_thesis: G . n misses G . m
then F . n misses F . m by PROB_2:def_2;
then (F . n) /\ (F . m) = {} by XBOOLE_0:def_7;
then (G . n) /\ (G . m) = {} by A15, XBOOLE_1:3, XBOOLE_1:27;
hence G . n misses G . m by XBOOLE_0:def_7; ::_thesis: verum
end;
consider B being set such that
A16: B = union (rng G) ;
A17: dom F = NAT by FUNCT_2:def_1;
A18: B c= union (rng F)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in union (rng F) )
assume x in B ; ::_thesis: x in union (rng F)
then consider Z being set such that
A19: x in Z and
A20: Z in rng G by A16, TARSKI:def_4;
dom G = NAT by FUNCT_2:def_1;
then consider n being set such that
A21: n in NAT and
A22: Z = G . n by A20, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A21;
set P = F . n;
A23: G . n c= F . n by A10;
ex P being set st
( P in rng F & x in P )
proof
take F . n ; ::_thesis: ( F . n in rng F & x in F . n )
thus ( F . n in rng F & x in F . n ) by A17, A19, A22, A23, FUNCT_1:def_3; ::_thesis: verum
end;
hence x in union (rng F) by TARSKI:def_4; ::_thesis: verum
end;
A24: ex C being thin of M st union (rng F) = B \/ C
proof
for A being set st A in rng L holds
A is measure_zero of M
proof
let A be set ; ::_thesis: ( A in rng L implies A is measure_zero of M )
assume A25: A in rng L ; ::_thesis: A is measure_zero of M
dom L = NAT by FUNCT_2:def_1;
then A26: ex n being set st
( n in NAT & A = L . n ) by A25, FUNCT_1:def_3;
rng L c= S by MEASURE2:def_1;
then reconsider A = A as Element of S by A25;
M . A = 0. by A11, A26;
hence A is measure_zero of M by MEASURE1:def_7; ::_thesis: verum
end;
then union (rng L) is measure_zero of M by MEASURE2:14;
then A27: M . (union (rng L)) = 0. by MEASURE1:def_7;
set C = (union (rng F)) \ B;
A28: union (rng F) = ((union (rng F)) \ B) \/ ((union (rng F)) /\ B) by XBOOLE_1:51
.= B \/ ((union (rng F)) \ B) by A18, XBOOLE_1:28 ;
reconsider C = (union (rng F)) \ B as Subset of X ;
A29: C c= union (rng H)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C or x in union (rng H) )
assume A30: x in C ; ::_thesis: x in union (rng H)
then x in union (rng F) by XBOOLE_0:def_5;
then consider Z being set such that
A31: x in Z and
A32: Z in rng F by TARSKI:def_4;
consider n being set such that
A33: n in NAT and
A34: Z = F . n by A17, A32, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A33;
A35: not x in union (rng G) by A16, A30, XBOOLE_0:def_5;
not x in G . n
proof
dom G = NAT by FUNCT_2:def_1;
then A36: G . n in rng G by FUNCT_1:def_3;
assume x in G . n ; ::_thesis: contradiction
hence contradiction by A35, A36, TARSKI:def_4; ::_thesis: verum
end;
then A37: x in (F . n) \ (G . n) by A31, A34, XBOOLE_0:def_5;
ex Z being set st
( x in Z & Z in rng H )
proof
take H . n ; ::_thesis: ( x in H . n & H . n in rng H )
dom H = NAT by FUNCT_2:def_1;
hence ( x in H . n & H . n in rng H ) by A9, A37, FUNCT_1:def_3; ::_thesis: verum
end;
hence x in union (rng H) by TARSKI:def_4; ::_thesis: verum
end;
union (rng H) c= union (rng L)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng H) or x in union (rng L) )
assume x in union (rng H) ; ::_thesis: x in union (rng L)
then consider Z being set such that
A38: x in Z and
A39: Z in rng H by TARSKI:def_4;
dom H = NAT by FUNCT_2:def_1;
then consider n being set such that
A40: n in NAT and
A41: Z = H . n by A39, FUNCT_1:def_3;
reconsider n = n as Element of NAT by A40;
n in dom L by A40, FUNCT_2:def_1;
then A42: L . n in rng L by FUNCT_1:def_3;
H . n c= L . n by A11;
hence x in union (rng L) by A38, A41, A42, TARSKI:def_4; ::_thesis: verum
end;
then C c= union (rng L) by A29, XBOOLE_1:1;
then C is thin of M by A27, Def2;
then consider C being thin of M such that
A43: union (rng F) = B \/ C by A28;
take C ; ::_thesis: union (rng F) = B \/ C
thus union (rng F) = B \/ C by A43; ::_thesis: verum
end;
reconsider G = G as Sep_Sequence of S by A12, PROB_2:def_2;
A44: for n being Element of NAT holds comM . (F . n) = M . (G . n)
proof
let n be Element of NAT ; ::_thesis: comM . (F . n) = M . (G . n)
(F . n) \ (G . n) is thin of M by A10;
then consider C being thin of M such that
A45: C = (F . n) \ (G . n) ;
F . n = ((F . n) /\ (G . n)) \/ ((F . n) \ (G . n)) by XBOOLE_1:51
.= (G . n) \/ C by A10, A45, XBOOLE_1:28 ;
hence comM . (F . n) = M . (G . n) by A5; ::_thesis: verum
end;
A46: for n being Element of NAT holds (comM * F) . n = (M * G) . n
proof
let n be Element of NAT ; ::_thesis: (comM * F) . n = (M * G) . n
(comM * F) . n = comM . (F . n) by FUNCT_2:15
.= M . (G . n) by A44
.= (M * G) . n by FUNCT_2:15 ;
hence (comM * F) . n = (M * G) . n ; ::_thesis: verum
end;
then for n being Element of NAT holds (M * G) . n <= (comM * F) . n ;
then A47: SUM (M * G) <= SUM (comM * F) by SUPINF_2:43;
for n being Element of NAT holds (comM * F) . n <= (M * G) . n by A46;
then SUM (comM * F) <= SUM (M * G) by SUPINF_2:43;
then ( SUM (M * G) = M . (union (rng G)) & SUM (comM * F) = SUM (M * G) ) by A47, MEASURE1:def_6, XXREAL_0:1;
hence SUM (comM * F) = comM . (union (rng F)) by A5, A16, A24; ::_thesis: verum
end;
A48: for x being Element of COM (S,M) holds 0. <= comM . x
proof
let x be Element of COM (S,M); ::_thesis: 0. <= comM . x
consider B being set such that
A49: B in S and
A50: ex C being thin of M st x = B \/ C by Def3;
reconsider B = B as Element of S by A49;
comM . x = M . B by A4, A50;
hence 0. <= comM . x by MEASURE1:def_2; ::_thesis: verum
end;
{} = {} \/ C ;
then comM . {} = M . {} by A5, PROB_1:4
.= 0. by VALUED_0:def_19 ;
then reconsider comM = comM as sigma_Measure of (COM (S,M)) by A48, A7, MEASURE1:def_2, MEASURE1:def_6, VALUED_0:def_19;
take comM ; ::_thesis: for B being set st B in S holds
for C being thin of M holds comM . (B \/ C) = M . B
thus for B being set st B in S holds
for C being thin of M holds comM . (B \/ C) = M . B by A5; ::_thesis: verum
end;
uniqueness
for b1, b2 being sigma_Measure of (COM (S,M)) st ( for B being set st B in S holds
for C being thin of M holds b1 . (B \/ C) = M . B ) & ( for B being set st B in S holds
for C being thin of M holds b2 . (B \/ C) = M . B ) holds
b1 = b2
proof
let M1, M2 be sigma_Measure of (COM (S,M)); ::_thesis: ( ( for B being set st B in S holds
for C being thin of M holds M1 . (B \/ C) = M . B ) & ( for B being set st B in S holds
for C being thin of M holds M2 . (B \/ C) = M . B ) implies M1 = M2 )
assume that
A51: for B being set st B in S holds
for C being thin of M holds M1 . (B \/ C) = M . B and
A52: for B being set st B in S holds
for C being thin of M holds M2 . (B \/ C) = M . B ; ::_thesis: M1 = M2
for x being set st x in COM (S,M) holds
M1 . x = M2 . x
proof
let x be set ; ::_thesis: ( x in COM (S,M) implies M1 . x = M2 . x )
assume x in COM (S,M) ; ::_thesis: M1 . x = M2 . x
then consider B being set such that
A53: ( B in S & ex C being thin of M st x = B \/ C ) by Def3;
M1 . x = M . B by A51, A53
.= M2 . x by A52, A53 ;
hence M1 . x = M2 . x ; ::_thesis: verum
end;
hence M1 = M2 by FUNCT_2:12; ::_thesis: verum
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 b4 being sigma_Measure of (COM (S,M)) holds
( b4 = COM M iff for B being set st B in S holds
for C being thin of M holds b4 . (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 COM (S,M)
proof
let X be set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S holds COM M is_complete COM (S,M)
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S holds COM M is_complete COM (S,M)
let M be sigma_Measure of S; ::_thesis: COM M is_complete COM (S,M)
for A being Subset of X
for B being set st B in COM (S,M) & A c= B & (COM M) . B = 0. holds
A in COM (S,M)
proof
let A be Subset of X; ::_thesis: for B being set st B in COM (S,M) & A c= B & (COM M) . B = 0. holds
A in COM (S,M)
let B be set ; ::_thesis: ( B in COM (S,M) & A c= B & (COM M) . B = 0. implies A in COM (S,M) )
assume A1: B in COM (S,M) ; ::_thesis: ( not A c= B or not (COM M) . B = 0. or A in COM (S,M) )
assume that
A2: A c= B and
A3: (COM M) . B = 0. ; ::_thesis: A in COM (S,M)
ex B1 being set st
( B1 in S & ex C1 being thin of M st A = B1 \/ C1 )
proof
take {} ; ::_thesis: ( {} in S & ex C1 being thin of M st A = {} \/ C1 )
consider B2 being set such that
A4: B2 in S and
A5: ex C2 being thin of M st B = B2 \/ C2 by A1, Def3;
A6: M . B2 = 0. by A3, A4, A5, Def5;
consider C2 being thin of M such that
A7: B = B2 \/ C2 by A5;
set C1 = (A /\ B2) \/ (A /\ C2);
consider D2 being set such that
A8: D2 in S and
A9: C2 c= D2 and
A10: M . D2 = 0. by Def2;
set O = B2 \/ D2;
A /\ C2 c= C2 by XBOOLE_1:17;
then A11: ( A /\ B2 c= B2 & A /\ C2 c= D2 ) by A9, XBOOLE_1:1, XBOOLE_1:17;
ex O being set st
( O in S & (A /\ B2) \/ (A /\ C2) c= O & M . O = 0. )
proof
reconsider B2 = B2, D2 = D2 as Element of S by A4, A8;
reconsider O1 = B2 \/ D2 as Element of S by A4, A8, FINSUB_1:def_1;
take B2 \/ D2 ; ::_thesis: ( B2 \/ D2 in S & (A /\ B2) \/ (A /\ C2) c= B2 \/ D2 & M . (B2 \/ D2) = 0. )
( M . (B2 \/ D2) <= 0. + 0. & 0. <= M . O1 ) by A6, A10, MEASURE1:33, MEASURE1:def_2;
hence ( B2 \/ D2 in S & (A /\ B2) \/ (A /\ C2) c= B2 \/ D2 & M . (B2 \/ D2) = 0. ) by A11, XBOOLE_1:13, XXREAL_0:1; ::_thesis: verum
end;
then A12: (A /\ B2) \/ (A /\ C2) is thin of M by Def2;
A = A /\ (B2 \/ C2) by A2, A7, XBOOLE_1:28
.= {} \/ ((A /\ B2) \/ (A /\ C2)) by XBOOLE_1:23 ;
hence ( {} in S & ex C1 being thin of M st A = {} \/ C1 ) by A12, PROB_1:4; ::_thesis: verum
end;
hence A in COM (S,M) by Def3; ::_thesis: verum
end;
hence COM M is_complete COM (S,M) by Def1; ::_thesis: verum
end;