:: MEASURE8 semantic presentation
begin
theorem Th1: :: MEASURE8:1
for seq being ExtREAL_sequence holds Ser seq = Partial_Sums seq
proof
let seq be ExtREAL_sequence; ::_thesis: Ser seq = Partial_Sums seq
for x being set st x in NAT holds
(Ser seq) . x = (Partial_Sums seq) . x
proof
defpred S1[ Nat] means (Ser seq) . $1 = (Partial_Sums seq) . $1;
let x be set ; ::_thesis: ( x in NAT implies (Ser seq) . x = (Partial_Sums seq) . x )
A1: 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 S1[k] ; ::_thesis: S1[k + 1]
then (Ser seq) . (k + 1) = ((Partial_Sums seq) . k) + (seq . (k + 1)) by SUPINF_2:44;
hence S1[k + 1] by MESFUNC9:def_1; ::_thesis: verum
end;
assume x in NAT ; ::_thesis: (Ser seq) . x = (Partial_Sums seq) . x
then reconsider n = x as Element of NAT ;
(Ser seq) . 0 = seq . 0 by SUPINF_2:44
.= (Partial_Sums seq) . 0 by MESFUNC9:def_1 ;
then A2: S1[ 0 ] ;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A2, A1);
then (Ser seq) . x = (Partial_Sums seq) . n ;
hence (Ser seq) . x = (Partial_Sums seq) . x ; ::_thesis: verum
end;
hence Ser seq = Partial_Sums seq by FUNCT_2:12; ::_thesis: verum
end;
theorem Th2: :: MEASURE8:2
for seq being ExtREAL_sequence st seq is nonnegative holds
( seq is summable & SUM seq = Sum seq )
proof
let seq be ExtREAL_sequence; ::_thesis: ( seq is nonnegative implies ( seq is summable & SUM seq = Sum seq ) )
assume seq is nonnegative ; ::_thesis: ( seq is summable & SUM seq = Sum seq )
then A1: Partial_Sums seq is non-decreasing by MESFUNC9:16;
then Partial_Sums seq is convergent by RINFSUP2:37;
hence seq is summable by MESFUNC9:def_2; ::_thesis: SUM seq = Sum seq
lim (Partial_Sums seq) = sup (Partial_Sums seq) by A1, RINFSUP2:37;
hence Sum seq = SUM seq by Th1; ::_thesis: verum
end;
theorem Th3: :: MEASURE8:3
for seq1, seq2, seq being ExtREAL_sequence st seq1 is nonnegative & seq2 is nonnegative & ( for n being Nat holds seq . n = (seq1 . n) + (seq2 . n) ) holds
( seq is nonnegative & SUM seq = (SUM seq1) + (SUM seq2) & Sum seq = (Sum seq1) + (Sum seq2) )
proof
let seq1, seq2, seq be ExtREAL_sequence; ::_thesis: ( seq1 is nonnegative & seq2 is nonnegative & ( for n being Nat holds seq . n = (seq1 . n) + (seq2 . n) ) implies ( seq is nonnegative & SUM seq = (SUM seq1) + (SUM seq2) & Sum seq = (Sum seq1) + (Sum seq2) ) )
assume that
A1: seq1 is nonnegative and
A2: seq2 is nonnegative ; ::_thesis: ( ex n being Nat st not seq . n = (seq1 . n) + (seq2 . n) or ( seq is nonnegative & SUM seq = (SUM seq1) + (SUM seq2) & Sum seq = (Sum seq1) + (Sum seq2) ) )
reconsider Hseq = Ser seq2 as ExtREAL_sequence ;
reconsider Gseq = Ser seq1 as ExtREAL_sequence ;
reconsider Fseq = Ser seq as ExtREAL_sequence ;
assume A3: for n being Nat holds seq . n = (seq1 . n) + (seq2 . n) ; ::_thesis: ( seq is nonnegative & SUM seq = (SUM seq1) + (SUM seq2) & Sum seq = (Sum seq1) + (Sum seq2) )
then A4: for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) ;
A5: for k being Nat holds Fseq . k = (Gseq . k) + (Hseq . k)
proof
let k be Nat; ::_thesis: Fseq . k = (Gseq . k) + (Hseq . k)
k in NAT by ORDINAL1:def_12;
hence Fseq . k = (Gseq . k) + (Hseq . k) by A1, A2, A4, MEASURE7:3; ::_thesis: verum
end;
for m, n being ext-real number st m in dom Fseq & n in dom Fseq & m <= n holds
Fseq . m <= Fseq . n
proof
let m, n be ext-real number ; ::_thesis: ( m in dom Fseq & n in dom Fseq & m <= n implies Fseq . m <= Fseq . n )
assume that
A6: m in dom Fseq and
A7: n in dom Fseq and
A8: m <= n ; ::_thesis: Fseq . m <= Fseq . n
( Gseq . m <= Gseq . n & Hseq . m <= Hseq . n ) by A1, A2, A6, A7, A8, MEASURE7:8;
then (Gseq . m) + (Hseq . m) <= (Gseq . n) + (Hseq . n) by XXREAL_3:36;
then Fseq . m <= (Gseq . n) + (Hseq . n) by A1, A2, A4, A6, MEASURE7:3;
hence Fseq . m <= Fseq . n by A1, A2, A4, A7, MEASURE7:3; ::_thesis: verum
end;
then Fseq is non-decreasing by VALUED_0:def_15;
then A9: lim Fseq = sup Fseq by RINFSUP2:37;
Partial_Sums seq1 is non-decreasing by A1, MESFUNC9:16;
then Gseq is non-decreasing by Th1;
then A10: ( Gseq is convergent & lim Gseq = sup Gseq ) by RINFSUP2:37;
Partial_Sums seq2 is nonnegative by A2, MESFUNC9:16;
then A11: Hseq is nonnegative by Th1;
now__::_thesis:_for_n_being_set_st_n_in_dom_seq_holds_
seq_._n_>=_0
let n be set ; ::_thesis: ( n in dom seq implies seq . n >= 0 )
assume n in dom seq ; ::_thesis: seq . n >= 0
then reconsider n9 = n as Element of NAT ;
A12: seq2 . n9 >= 0 by A2, SUPINF_2:51;
( seq . n = (seq1 . n9) + (seq2 . n9) & seq1 . n9 >= 0 ) by A1, A3, SUPINF_2:51;
hence seq . n >= 0 by A12; ::_thesis: verum
end;
hence A13: seq is nonnegative by SUPINF_2:52; ::_thesis: ( SUM seq = (SUM seq1) + (SUM seq2) & Sum seq = (Sum seq1) + (Sum seq2) )
Partial_Sums seq2 is non-decreasing by A2, MESFUNC9:16;
then Hseq is non-decreasing by Th1;
then A14: ( Hseq is convergent & lim Hseq = sup Hseq ) by RINFSUP2:37;
Partial_Sums seq1 is nonnegative by A1, MESFUNC9:16;
then Gseq is nonnegative by Th1;
hence SUM seq = (SUM seq1) + (SUM seq2) by A10, A11, A14, A5, A9, MESFUNC9:11; ::_thesis: Sum seq = (Sum seq1) + (Sum seq2)
then Sum seq = (SUM seq1) + (SUM seq2) by A13, Th2;
then Sum seq = (Sum seq1) + (SUM seq2) by A1, Th2;
hence Sum seq = (Sum seq1) + (Sum seq2) by A2, Th2; ::_thesis: verum
end;
registration
let X be set ;
let F be Field_Subset of X;
cluster non empty Relation-like NAT -defined F -valued Function-like V27( NAT ) quasi_total disjoint_valued for Element of bool [:NAT,F:];
existence
ex b1 being Function of NAT,F st b1 is disjoint_valued
proof
consider f being Function of NAT,{{}} such that
A1: for n being Element of NAT holds f . n = {} by MEASURE1:16;
{} in F by PROB_1:4;
then {{}} c= F by ZFMISC_1:31;
then reconsider f = f as Function of NAT,F by FUNCT_2:7;
take f ; ::_thesis: f is disjoint_valued
A2: for x being set holds f . x = {}
proof
let x be set ; ::_thesis: f . x = {}
( x in dom f implies f . x = {} ) by A1;
hence f . x = {} by FUNCT_1:def_2; ::_thesis: verum
end;
thus for x, y being set st x <> y holds
f . x misses f . y :: according to PROB_2:def_2 ::_thesis: verum
proof
let x, y be set ; ::_thesis: ( x <> y implies f . x misses f . y )
f . x = {} by A2;
hence ( x <> y implies f . x misses f . y ) by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
definition
let X be set ;
let F be Field_Subset of X;
mode FinSequence of F -> FinSequence of bool X means :Def1: :: MEASURE8:def 1
for k being Nat st k in dom it holds
it . k in F;
existence
ex b1 being FinSequence of bool X st
for k being Nat st k in dom b1 holds
b1 . k in F
proof
consider f being FinSequence of bool X such that
A1: for k being Nat st k in dom f holds
f . k = X by PROB_3:47;
take f ; ::_thesis: for k being Nat st k in dom f holds
f . k in F
hereby ::_thesis: verum
let k be Nat; ::_thesis: ( k in dom f implies f . k in F )
assume k in dom f ; ::_thesis: f . k in F
then f . k = X by A1;
hence f . k in F by PROB_1:5; ::_thesis: verum
end;
end;
end;
:: deftheorem Def1 defines FinSequence MEASURE8:def_1_:_
for X being set
for F being Field_Subset of X
for b3 being FinSequence of bool X holds
( b3 is FinSequence of F iff for k being Nat st k in dom b3 holds
b3 . k in F );
registration
let X be set ;
let F be Field_Subset of X;
cluster Relation-like NAT -defined bool X -valued Function-like FinSequence-like disjoint_valued for FinSequence of F;
existence
ex b1 being FinSequence of F st b1 is disjoint_valued
proof
{} c= X by XBOOLE_1:2;
then reconsider f = <*{}*> as FinSequence of bool X by FINSEQ_1:74;
for k being Nat st k in dom f holds
f . k in F
proof
let k be Nat; ::_thesis: ( k in dom f implies f . k in F )
assume k in dom f ; ::_thesis: f . k in F
then k in Seg 1 by FINSEQ_1:def_8;
then k = 1 by FINSEQ_1:2, TARSKI:def_1;
then f . k = {} by FINSEQ_1:def_8;
hence f . k in F by PROB_1:4; ::_thesis: verum
end;
then reconsider f = <*{}*> as FinSequence of F by Def1;
take f ; ::_thesis: f is disjoint_valued
A1: for n being set holds f . n = {}
proof
let n be set ; ::_thesis: f . n = {}
now__::_thesis:_(_n_in_dom_f_implies_f_._n_=_{}_)
assume n in dom f ; ::_thesis: f . n = {}
then n in Seg 1 by FINSEQ_1:def_8;
then n = 1 by FINSEQ_1:2, TARSKI:def_1;
hence f . n = {} by FINSEQ_1:def_8; ::_thesis: verum
end;
hence f . n = {} by FUNCT_1:def_2; ::_thesis: verum
end;
thus for x, y being set st x <> y holds
f . x misses f . y :: according to PROB_2:def_2 ::_thesis: verum
proof
let x, y be set ; ::_thesis: ( x <> y implies f . x misses f . y )
f . x = {} by A1;
hence ( x <> y implies f . x misses f . y ) by XBOOLE_1:65; ::_thesis: verum
end;
end;
end;
definition
let X be set ;
let F be Field_Subset of X;
mode Sep_FinSequence of F is disjoint_valued FinSequence of F;
end;
definition
let X be set ;
let F be Field_Subset of X;
mode Sep_Sequence of F is disjoint_valued Function of NAT,F;
end;
definition
let X be set ;
let F be Field_Subset of X;
mode Set_Sequence of F -> SetSequence of X means :Def2: :: MEASURE8:def 2
for n being Nat holds it . n in F;
existence
ex b1 being SetSequence of X st
for n being Nat holds b1 . n in F
proof
X in bool X by ZFMISC_1:def_1;
then reconsider A = NAT --> X as SetSequence of X by FUNCOP_1:45;
take A ; ::_thesis: for n being Nat holds A . n in F
let n be Nat; ::_thesis: A . n in F
n is Element of NAT by ORDINAL1:def_12;
then A . n = X by FUNCOP_1:7;
hence A . n in F by PROB_1:5; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines Set_Sequence MEASURE8:def_2_:_
for X being set
for F being Field_Subset of X
for b3 being SetSequence of X holds
( b3 is Set_Sequence of F iff for n being Nat holds b3 . n in F );
definition
let X be set ;
let A be Subset of X;
let F be Field_Subset of X;
mode Covering of A,F -> Set_Sequence of F means :Def3: :: MEASURE8:def 3
A c= union (rng it);
existence
ex b1 being Set_Sequence of F st A c= union (rng b1)
proof
X in bool X by ZFMISC_1:def_1;
then reconsider IT = NAT --> X as SetSequence of X by FUNCOP_1:45;
for n being Nat holds IT . n in F
proof
let n be Nat; ::_thesis: IT . n in F
n in NAT by ORDINAL1:def_12;
then IT . n = X by FUNCOP_1:7;
hence IT . n in F by PROB_1:5; ::_thesis: verum
end;
then reconsider IT = IT as Set_Sequence of F by Def2;
take IT ; ::_thesis: A c= union (rng IT)
rng IT = {X} by FUNCOP_1:8;
then X c= union (rng IT) by ZFMISC_1:25;
hence A c= union (rng IT) by XBOOLE_1:1; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines Covering MEASURE8:def_3_:_
for X being set
for A being Subset of X
for F being Field_Subset of X
for b4 being Set_Sequence of F holds
( b4 is Covering of A,F iff A c= union (rng b4) );
definition
let X be set ;
let F be Field_Subset of X;
let FSets be Set_Sequence of F;
let n be Nat;
:: original: .
redefine funcFSets . n -> Element of F;
correctness
coherence
FSets . n is Element of F;
by Def2;
end;
Lm1: for X being set
for F being Field_Subset of X holds NAT --> X is Set_Sequence of F
proof
let X be set ; ::_thesis: for F being Field_Subset of X holds NAT --> X is Set_Sequence of F
let F be Field_Subset of X; ::_thesis: NAT --> X is Set_Sequence of F
X in bool X by ZFMISC_1:def_1;
then reconsider G0 = NAT --> X as SetSequence of X by FUNCOP_1:45;
A1: rng (NAT --> X) = {X} by FUNCOP_1:8;
for n being Nat holds G0 . n in F
proof
let n be Nat; ::_thesis: G0 . n in F
n in NAT by ORDINAL1:def_12;
then G0 . n in {X} by A1, FUNCT_2:4;
then G0 . n = X by TARSKI:def_1;
hence G0 . n in F by PROB_1:5; ::_thesis: verum
end;
hence NAT --> X is Set_Sequence of F by Def2; ::_thesis: verum
end;
definition
let X be set ;
let F be Field_Subset of X;
let Sets be SetSequence of X;
mode Covering of Sets,F -> Function of NAT,(Funcs (NAT,(bool X))) means :Def4: :: MEASURE8:def 4
for n being Nat holds it . n is Covering of Sets . n,F;
existence
ex b1 being Function of NAT,(Funcs (NAT,(bool X))) st
for n being Nat holds b1 . n is Covering of Sets . n,F
proof
reconsider G0 = NAT --> X as Set_Sequence of F by Lm1;
reconsider G = G0 as Element of Funcs (NAT,(bool X)) by FUNCT_2:8;
reconsider H = NAT --> G as Function of NAT,(Funcs (NAT,(bool X))) ;
take H ; ::_thesis: for n being Nat holds H . n is Covering of Sets . n,F
hereby ::_thesis: verum
let n be Nat; ::_thesis: H . n is Covering of Sets . n,F
rng (NAT --> X) = {X} by FUNCOP_1:8;
then X c= union (rng (NAT --> X)) by ZFMISC_1:25;
then A1: Sets . n c= union (rng (NAT --> X)) by XBOOLE_1:1;
n in NAT by ORDINAL1:def_12;
then H . n = NAT --> X by FUNCOP_1:7;
hence H . n is Covering of Sets . n,F by A1, Def3; ::_thesis: verum
end;
end;
end;
:: deftheorem Def4 defines Covering MEASURE8:def_4_:_
for X being set
for F being Field_Subset of X
for Sets being SetSequence of X
for b4 being Function of NAT,(Funcs (NAT,(bool X))) holds
( b4 is Covering of Sets,F iff for n being Nat holds b4 . n is Covering of Sets . n,F );
definition
let X be set ;
let F be Field_Subset of X;
let M be Measure of F;
let FSets be Set_Sequence of F;
func vol (M,FSets) -> ExtREAL_sequence means :Def5: :: MEASURE8:def 5
for n being Nat holds it . n = M . (FSets . n);
existence
ex b1 being ExtREAL_sequence st
for n being Nat holds b1 . n = M . (FSets . n)
proof
deffunc H1( Element of NAT ) -> Element of ExtREAL = M . (FSets . $1);
consider IT being Function of NAT,ExtREAL such that
A1: for n being Element of NAT holds IT . n = H1(n) from FUNCT_2:sch_4();
take IT ; ::_thesis: for n being Nat holds IT . n = M . (FSets . n)
hereby ::_thesis: verum
let n be Nat; ::_thesis: IT . n = M . (FSets . n)
n in NAT by ORDINAL1:def_12;
hence IT . n = M . (FSets . n) by A1; ::_thesis: verum
end;
end;
uniqueness
for b1, b2 being ExtREAL_sequence st ( for n being Nat holds b1 . n = M . (FSets . n) ) & ( for n being Nat holds b2 . n = M . (FSets . n) ) holds
b1 = b2
proof
let V1, V2 be Function of NAT,ExtREAL; ::_thesis: ( ( for n being Nat holds V1 . n = M . (FSets . n) ) & ( for n being Nat holds V2 . n = M . (FSets . n) ) implies V1 = V2 )
assume that
A2: for n being Nat holds V1 . n = M . (FSets . n) and
A3: for n being Nat holds V2 . n = M . (FSets . n) ; ::_thesis: V1 = V2
now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
V1_._x_=_V2_._x
let x be set ; ::_thesis: ( x in NAT implies V1 . x = V2 . x )
assume x in NAT ; ::_thesis: V1 . x = V2 . x
then reconsider n = x as Nat ;
thus V1 . x = M . (FSets . n) by A2
.= V2 . x by A3 ; ::_thesis: verum
end;
hence V1 = V2 by FUNCT_2:12; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines vol MEASURE8:def_5_:_
for X being set
for F being Field_Subset of X
for M being Measure of F
for FSets being Set_Sequence of F
for b5 being ExtREAL_sequence holds
( b5 = vol (M,FSets) iff for n being Nat holds b5 . n = M . (FSets . n) );
theorem Th4: :: MEASURE8:4
for X being set
for F being Field_Subset of X
for M being Measure of F
for FSets being Set_Sequence of F holds vol (M,FSets) is nonnegative
proof
let X be set ; ::_thesis: for F being Field_Subset of X
for M being Measure of F
for FSets being Set_Sequence of F holds vol (M,FSets) is nonnegative
let F be Field_Subset of X; ::_thesis: for M being Measure of F
for FSets being Set_Sequence of F holds vol (M,FSets) is nonnegative
let M be Measure of F; ::_thesis: for FSets being Set_Sequence of F holds vol (M,FSets) is nonnegative
let FSets be Set_Sequence of F; ::_thesis: vol (M,FSets) is nonnegative
for n being Element of NAT holds 0 <= (vol (M,FSets)) . n
proof
let n be Element of NAT ; ::_thesis: 0 <= (vol (M,FSets)) . n
( (vol (M,FSets)) . n = M . (FSets . n) & {} in F ) by Def5, PROB_1:4;
then M . {} <= (vol (M,FSets)) . n by MEASURE1:8, XBOOLE_1:2;
hence 0 <= (vol (M,FSets)) . n by VALUED_0:def_19; ::_thesis: verum
end;
hence vol (M,FSets) is nonnegative by SUPINF_2:39; ::_thesis: verum
end;
definition
let X be set ;
let F be Field_Subset of X;
let Sets be SetSequence of X;
let Cvr be Covering of Sets,F;
let n be Nat;
:: original: .
redefine funcCvr . n -> Covering of Sets . n,F;
correctness
coherence
Cvr . n is Covering of Sets . n,F;
by Def4;
end;
definition
let X be set ;
let F be Field_Subset of X;
let Sets be SetSequence of X;
let M be Measure of F;
let Cvr be Covering of Sets,F;
func Volume (M,Cvr) -> ExtREAL_sequence means :Def6: :: MEASURE8:def 6
for n being Nat holds it . n = SUM (vol (M,(Cvr . n)));
existence
ex b1 being ExtREAL_sequence st
for n being Nat holds b1 . n = SUM (vol (M,(Cvr . n)))
proof
defpred S1[ Element of NAT , Element of ExtREAL ] means $2 = SUM (vol (M,(Cvr . $1)));
A1: for n being Element of NAT ex y being Element of ExtREAL st S1[n,y] ;
consider G0 being Function of NAT,ExtREAL such that
A2: for n being Element of NAT holds S1[n,G0 . n] from FUNCT_2:sch_3(A1);
take G0 ; ::_thesis: for n being Nat holds G0 . n = SUM (vol (M,(Cvr . n)))
hereby ::_thesis: verum
let n be Nat; ::_thesis: G0 . n = SUM (vol (M,(Cvr . n)))
n in NAT by ORDINAL1:def_12;
hence G0 . n = SUM (vol (M,(Cvr . n))) by A2; ::_thesis: verum
end;
end;
uniqueness
for b1, b2 being ExtREAL_sequence st ( for n being Nat holds b1 . n = SUM (vol (M,(Cvr . n))) ) & ( for n being Nat holds b2 . n = SUM (vol (M,(Cvr . n))) ) holds
b1 = b2
proof
let G1, G2 be Function of NAT,ExtREAL; ::_thesis: ( ( for n being Nat holds G1 . n = SUM (vol (M,(Cvr . n))) ) & ( for n being Nat holds G2 . n = SUM (vol (M,(Cvr . n))) ) implies G1 = G2 )
assume that
A3: for n being Nat holds G1 . n = SUM (vol (M,(Cvr . n))) and
A4: for n being Nat holds G2 . n = SUM (vol (M,(Cvr . n))) ; ::_thesis: G1 = G2
now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_
G1_._x_=_G2_._x
let x be set ; ::_thesis: ( x in NAT implies G1 . x = G2 . x )
assume x in NAT ; ::_thesis: G1 . x = G2 . x
then reconsider n = x as Nat ;
thus G1 . x = SUM (vol (M,(Cvr . n))) by A3
.= G2 . x by A4 ; ::_thesis: verum
end;
hence G1 = G2 by FUNCT_2:12; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines Volume MEASURE8:def_6_:_
for X being set
for F being Field_Subset of X
for Sets being SetSequence of X
for M being Measure of F
for Cvr being Covering of Sets,F
for b6 being ExtREAL_sequence holds
( b6 = Volume (M,Cvr) iff for n being Nat holds b6 . n = SUM (vol (M,(Cvr . n))) );
theorem Th5: :: MEASURE8:5
for X being set
for F being Field_Subset of X
for M being Measure of F
for Sets being SetSequence of X
for n being Nat
for Cvr being Covering of Sets,F holds 0 <= (Volume (M,Cvr)) . n
proof
let X be set ; ::_thesis: for F being Field_Subset of X
for M being Measure of F
for Sets being SetSequence of X
for n being Nat
for Cvr being Covering of Sets,F holds 0 <= (Volume (M,Cvr)) . n
let F be Field_Subset of X; ::_thesis: for M being Measure of F
for Sets being SetSequence of X
for n being Nat
for Cvr being Covering of Sets,F holds 0 <= (Volume (M,Cvr)) . n
let M be Measure of F; ::_thesis: for Sets being SetSequence of X
for n being Nat
for Cvr being Covering of Sets,F holds 0 <= (Volume (M,Cvr)) . n
let Sets be SetSequence of X; ::_thesis: for n being Nat
for Cvr being Covering of Sets,F holds 0 <= (Volume (M,Cvr)) . n
let n be Nat; ::_thesis: for Cvr being Covering of Sets,F holds 0 <= (Volume (M,Cvr)) . n
let Cvr be Covering of Sets,F; ::_thesis: 0 <= (Volume (M,Cvr)) . n
for k being Element of NAT holds 0 <= (vol (M,(Cvr . n))) . k
proof
let k be Element of NAT ; ::_thesis: 0 <= (vol (M,(Cvr . n))) . k
0 <= M . ((Cvr . n) . k) by SUPINF_2:51;
hence 0 <= (vol (M,(Cvr . n))) . k by Def5; ::_thesis: verum
end;
then A1: vol (M,(Cvr . n)) is nonnegative by SUPINF_2:39;
(Volume (M,Cvr)) . n = SUM (vol (M,(Cvr . n))) by Def6;
hence 0 <= (Volume (M,Cvr)) . n by A1, MEASURE6:2; ::_thesis: verum
end;
definition
let X be set ;
let F be Field_Subset of X;
let M be Measure of F;
let A be Subset of X;
func Svc (M,A) -> Subset of ExtREAL means :Def7: :: MEASURE8:def 7
for x being R_eal holds
( x in it iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) );
existence
ex b1 being Subset of ExtREAL st
for x being R_eal holds
( x in b1 iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) )
proof
defpred S1[ set ] means ex CA being Covering of A,F st $1 = SUM (vol (M,CA));
consider D being set such that
A1: for x being set holds
( x in D iff ( x in ExtREAL & S1[x] ) ) from XBOOLE_0:sch_1();
for z being set st z in D holds
z in ExtREAL by A1;
then reconsider D = D as Subset of ExtREAL by TARSKI:def_3;
take D ; ::_thesis: for x being R_eal holds
( x in D iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) )
thus for x being R_eal holds
( x in D iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset of ExtREAL st ( for x being R_eal holds
( x in b1 iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ) ) & ( for x being R_eal holds
( x in b2 iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ) ) holds
b1 = b2
proof
defpred S1[ set ] means ex CA being Covering of A,F st $1 = SUM (vol (M,CA));
let D1, D2 be Subset of ExtREAL; ::_thesis: ( ( for x being R_eal holds
( x in D1 iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ) ) & ( for x being R_eal holds
( x in D2 iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ) ) implies D1 = D2 )
assume that
A2: for x being R_eal holds
( x in D1 iff S1[x] ) and
A3: for x being R_eal holds
( x in D2 iff S1[x] ) ; ::_thesis: D1 = D2
thus D1 = D2 from SUBSET_1:sch_2(A2, A3); ::_thesis: verum
end;
end;
:: deftheorem Def7 defines Svc MEASURE8:def_7_:_
for X being set
for F being Field_Subset of X
for M being Measure of F
for A being Subset of X
for b5 being Subset of ExtREAL holds
( b5 = Svc (M,A) iff for x being R_eal holds
( x in b5 iff ex CA being Covering of A,F st x = SUM (vol (M,CA)) ) );
registration
let X be set ;
let A be Subset of X;
let F be Field_Subset of X;
let M be Measure of F;
cluster Svc (M,A) -> non empty ;
coherence
not Svc (M,A) is empty
proof
( X c= X & {} c= X ) by XBOOLE_1:2;
then consider CA being Function of NAT,(bool X) such that
A1: rng CA = {X,{}} and
CA . 0 = X and
for n being Element of NAT st 0 < n holds
CA . n = {} by MEASURE1:19;
for n being Nat holds CA . n in F
proof
let n be Nat; ::_thesis: CA . n in F
n in NAT by ORDINAL1:def_12;
then A2: CA . n in rng CA by FUNCT_2:4;
( X in F & {} in F ) by PROB_1:4, PROB_1:5;
then rng CA c= F by A1, ZFMISC_1:32;
hence CA . n in F by A2; ::_thesis: verum
end;
then ( union {X,{}} = X \/ {} & CA is Set_Sequence of F ) by Def2, ZFMISC_1:75;
then reconsider CA = CA as Covering of A,F by A1, Def3;
defpred S1[ set ] means ex G being Covering of A,F st X = SUM (vol (M,G));
consider D being set such that
A3: for x being set holds
( x in D iff ( x in ExtREAL & S1[x] ) ) from XBOOLE_0:sch_1();
SUM (vol (M,CA)) in D by A3;
hence not Svc (M,A) is empty by Def7; ::_thesis: verum
end;
end;
definition
let X be set ;
let F be Field_Subset of X;
let M be Measure of F;
func C_Meas M -> Function of (bool X),ExtREAL means :Def8: :: MEASURE8:def 8
for A being Subset of X holds it . A = inf (Svc (M,A));
existence
ex b1 being Function of (bool X),ExtREAL st
for A being Subset of X holds b1 . A = inf (Svc (M,A))
proof
deffunc H1( Element of bool X) -> Element of ExtREAL = inf (Svc (M,$1));
thus ex G being Function of (bool X),ExtREAL st
for A being Subset of X holds G . A = H1(A) from FUNCT_2:sch_4(); ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (bool X),ExtREAL st ( for A being Subset of X holds b1 . A = inf (Svc (M,A)) ) & ( for A being Subset of X holds b2 . A = inf (Svc (M,A)) ) holds
b1 = b2
proof
deffunc H1( Subset of X) -> Element of ExtREAL = inf (Svc (M,$1));
thus for F1, F2 being Function of (bool X),ExtREAL st ( for A being Subset of X holds F1 . A = H1(A) ) & ( for A being Subset of X holds F2 . A = H1(A) ) holds
F1 = F2 from BINOP_2:sch_1(); ::_thesis: verum
end;
end;
:: deftheorem Def8 defines C_Meas MEASURE8:def_8_:_
for X being set
for F being Field_Subset of X
for M being Measure of F
for b4 being Function of (bool X),ExtREAL holds
( b4 = C_Meas M iff for A being Subset of X holds b4 . A = inf (Svc (M,A)) );
definition
func InvPairFunc -> Function of NAT,[:NAT,NAT:] equals :: MEASURE8:def 9
PairFunc " ;
correctness
coherence
PairFunc " is Function of NAT,[:NAT,NAT:];
by FUNCTOR1:2, NAGATA_2:2;
end;
:: deftheorem defines InvPairFunc MEASURE8:def_9_:_
InvPairFunc = PairFunc " ;
definition
let X be set ;
let F be Field_Subset of X;
let Sets be SetSequence of X;
let Cvr be Covering of Sets,F;
func On Cvr -> Covering of union (rng Sets),F means :Def10: :: MEASURE8:def 10
for n being Nat holds it . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n);
existence
ex b1 being Covering of union (rng Sets),F st
for n being Nat holds b1 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n)
proof
defpred S1[ Element of NAT , Subset of X] means $2 = (Cvr . ((pr1 InvPairFunc) . $1)) . ((pr2 InvPairFunc) . $1);
A1: for n being Element of NAT ex y being Subset of X st S1[n,y] ;
consider Seq0 being Function of NAT,(bool X) such that
A2: for n being Element of NAT holds S1[n,Seq0 . n] from FUNCT_2:sch_3(A1);
reconsider Seq0 = Seq0 as SetSequence of X ;
for n being Nat holds Seq0 . n in F
proof
let n be Nat; ::_thesis: Seq0 . n in F
n in NAT by ORDINAL1:def_12;
then Seq0 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) by A2;
hence Seq0 . n in F ; ::_thesis: verum
end;
then reconsider Seq0 = Seq0 as Set_Sequence of F by Def2;
union (rng Sets) c= union (rng Seq0)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (rng Sets) or x in union (rng Seq0) )
assume x in union (rng Sets) ; ::_thesis: x in union (rng Seq0)
then consider A being set such that
A3: x in A and
A4: A in rng Sets by TARSKI:def_4;
consider n1 being Element of NAT such that
A5: A = Sets . n1 by A4, FUNCT_2:113;
Sets . n1 c= union (rng (Cvr . n1)) by Def3;
then consider AA being set such that
A6: x in AA and
A7: AA in rng (Cvr . n1) by A3, A5, TARSKI:def_4;
consider n2 being Element of NAT such that
A8: AA = (Cvr . n1) . n2 by A7, FUNCT_2:113;
dom PairFunc = rng InvPairFunc by FUNCT_1:33, NAGATA_2:2;
then rng InvPairFunc = [:NAT,NAT:] by FUNCT_2:def_1;
then [n1,n2] in rng InvPairFunc by ZFMISC_1:def_2;
then consider n being Element of NAT such that
A9: [n1,n2] = InvPairFunc . n by FUNCT_2:113;
[((pr1 InvPairFunc) . n),((pr2 InvPairFunc) . n)] = [n1,n2] by A9, FUNCT_2:119;
then ( (pr1 InvPairFunc) . n = n1 & (pr2 InvPairFunc) . n = n2 ) by XTUPLE_0:1;
then A10: x in Seq0 . n by A2, A6, A8;
Seq0 . n in rng Seq0 by FUNCT_2:4;
hence x in union (rng Seq0) by A10, TARSKI:def_4; ::_thesis: verum
end;
then reconsider Seq0 = Seq0 as Covering of union (rng Sets),F by Def3;
take Seq0 ; ::_thesis: for n being Nat holds Seq0 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n)
hereby ::_thesis: verum
let n be Nat; ::_thesis: Seq0 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n)
n in NAT by ORDINAL1:def_12;
hence Seq0 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) by A2; ::_thesis: verum
end;
end;
uniqueness
for b1, b2 being Covering of union (rng Sets),F st ( for n being Nat holds b1 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) ) & ( for n being Nat holds b2 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) ) holds
b1 = b2
proof
let Seq1, Seq2 be Covering of union (rng Sets),F; ::_thesis: ( ( for n being Nat holds Seq1 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) ) & ( for n being Nat holds Seq2 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) ) implies Seq1 = Seq2 )
assume that
A11: for n being Nat holds Seq1 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) and
A12: for n being Nat holds Seq2 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) ; ::_thesis: Seq1 = Seq2
for n being set st n in NAT holds
Seq1 . n = Seq2 . n
proof
let n be set ; ::_thesis: ( n in NAT implies Seq1 . n = Seq2 . n )
assume n in NAT ; ::_thesis: Seq1 . n = Seq2 . n
then reconsider n = n as Element of NAT ;
Seq1 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) by A11;
hence Seq1 . n = Seq2 . n by A12; ::_thesis: verum
end;
hence Seq1 = Seq2 by FUNCT_2:12; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines On MEASURE8:def_10_:_
for X being set
for F being Field_Subset of X
for Sets being SetSequence of X
for Cvr being Covering of Sets,F
for b5 being Covering of union (rng Sets),F holds
( b5 = On Cvr iff for n being Nat holds b5 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) );
theorem Th6: :: MEASURE8:6
for X being set
for F being Field_Subset of X
for M being Measure of F
for k being Element of NAT ex m being Nat st
for Sets being SetSequence of X
for Cvr being Covering of Sets,F holds (Partial_Sums (vol (M,(On Cvr)))) . k <= (Partial_Sums (Volume (M,Cvr))) . m
proof
let X be set ; ::_thesis: for F being Field_Subset of X
for M being Measure of F
for k being Element of NAT ex m being Nat st
for Sets being SetSequence of X
for Cvr being Covering of Sets,F holds (Partial_Sums (vol (M,(On Cvr)))) . k <= (Partial_Sums (Volume (M,Cvr))) . m
let F be Field_Subset of X; ::_thesis: for M being Measure of F
for k being Element of NAT ex m being Nat st
for Sets being SetSequence of X
for Cvr being Covering of Sets,F holds (Partial_Sums (vol (M,(On Cvr)))) . k <= (Partial_Sums (Volume (M,Cvr))) . m
let M be Measure of F; ::_thesis: for k being Element of NAT ex m being Nat st
for Sets being SetSequence of X
for Cvr being Covering of Sets,F holds (Partial_Sums (vol (M,(On Cvr)))) . k <= (Partial_Sums (Volume (M,Cvr))) . m
defpred S1[ Element of NAT ] means ex m being Nat st
for Sets being SetSequence of X
for Cvr being Covering of Sets,F holds (Partial_Sums (vol (M,(On Cvr)))) . $1 <= (Partial_Sums (Volume (M,Cvr))) . m;
{} c= X by XBOOLE_1:2;
then reconsider D = NAT --> {} as Function of NAT,(bool X) by FUNCOP_1:45;
reconsider y = D as Element of Funcs (NAT,(bool X)) by FUNCT_2:8;
A1: 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] )
set a = (pr1 InvPairFunc) . (k + 1);
set b = (pr2 InvPairFunc) . (k + 1);
set N0 = { s where s is Element of NAT : (pr1 InvPairFunc) . (k + 1) = (pr1 InvPairFunc) . s } ;
A2: { s where s is Element of NAT : (pr1 InvPairFunc) . (k + 1) = (pr1 InvPairFunc) . s } c= NAT
proof
let s1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not s1 in { s where s is Element of NAT : (pr1 InvPairFunc) . (k + 1) = (pr1 InvPairFunc) . s } or s1 in NAT )
assume s1 in { s where s is Element of NAT : (pr1 InvPairFunc) . (k + 1) = (pr1 InvPairFunc) . s } ; ::_thesis: s1 in NAT
then ex s being Element of NAT st
( s = s1 & (pr1 InvPairFunc) . (k + 1) = (pr1 InvPairFunc) . s ) ;
hence s1 in NAT ; ::_thesis: verum
end;
k + 1 in { s where s is Element of NAT : (pr1 InvPairFunc) . (k + 1) = (pr1 InvPairFunc) . s } ;
then reconsider N0 = { s where s is Element of NAT : (pr1 InvPairFunc) . (k + 1) = (pr1 InvPairFunc) . s } as non empty Subset of NAT by A2;
given m0 being Nat such that A3: for Sets being SetSequence of X
for Cvr being Covering of Sets,F holds (Partial_Sums (vol (M,(On Cvr)))) . k <= (Partial_Sums (Volume (M,Cvr))) . m0 ; ::_thesis: S1[k + 1]
take m = m0 + ((pr1 InvPairFunc) . (k + 1)); ::_thesis: for Sets being SetSequence of X
for Cvr being Covering of Sets,F holds (Partial_Sums (vol (M,(On Cvr)))) . (k + 1) <= (Partial_Sums (Volume (M,Cvr))) . m
let Sets be SetSequence of X; ::_thesis: for Cvr being Covering of Sets,F holds (Partial_Sums (vol (M,(On Cvr)))) . (k + 1) <= (Partial_Sums (Volume (M,Cvr))) . m
let Cvr be Covering of Sets,F; ::_thesis: (Partial_Sums (vol (M,(On Cvr)))) . (k + 1) <= (Partial_Sums (Volume (M,Cvr))) . m
defpred S2[ Element of NAT , Function] means ( ( $1 = (pr1 InvPairFunc) . (k + 1) implies for m being Element of NAT holds $2 . m = (Cvr . $1) . m ) & ( $1 <> (pr1 InvPairFunc) . (k + 1) implies for m being Element of NAT holds $2 . m = {} ) );
defpred S3[ Element of NAT , Function] means ( ( $1 <> (pr1 InvPairFunc) . (k + 1) implies for m being Element of NAT holds $2 . m = (Cvr . $1) . m ) & ( $1 = (pr1 InvPairFunc) . (k + 1) implies for m being Element of NAT holds $2 . m = {} ) );
A4: for n being Element of NAT ex y being Element of Funcs (NAT,(bool X)) st S2[n,y]
proof
let n be Element of NAT ; ::_thesis: ex y being Element of Funcs (NAT,(bool X)) st S2[n,y]
A5: now__::_thesis:_(_n_=_(pr1_InvPairFunc)_._(k_+_1)_implies_ex_y_being_Element_of_Funcs_(NAT,(bool_X))_st_S2[n,y]_)
reconsider y = Cvr . n as Element of Funcs (NAT,(bool X)) by FUNCT_2:8;
assume A6: n = (pr1 InvPairFunc) . (k + 1) ; ::_thesis: ex y being Element of Funcs (NAT,(bool X)) st S2[n,y]
take y = y; ::_thesis: S2[n,y]
thus S2[n,y] by A6; ::_thesis: verum
end;
( n <> (pr1 InvPairFunc) . (k + 1) implies S2[n,y] ) by FUNCOP_1:7;
hence ex y being Element of Funcs (NAT,(bool X)) st S2[n,y] by A5; ::_thesis: verum
end;
consider Cvr0 being Function of NAT,(Funcs (NAT,(bool X))) such that
A7: for n being Element of NAT holds S2[n,Cvr0 . n] from FUNCT_2:sch_3(A4);
A8: for n being Nat holds Cvr0 . n is Covering of D . n,F
proof
let n be Nat; ::_thesis: Cvr0 . n is Covering of D . n,F
consider FSets0 being Function such that
A9: Cvr0 . n = FSets0 and
A10: ( dom FSets0 = NAT & rng FSets0 c= bool X ) by FUNCT_2:def_2;
reconsider FSets0 = FSets0 as SetSequence of X by A10, FUNCT_2:2;
for s being Nat holds FSets0 . s in F
proof
let s be Nat; ::_thesis: FSets0 . s in F
A11: s in NAT by ORDINAL1:def_12;
A12: now__::_thesis:_(_n_=_(pr1_InvPairFunc)_._(k_+_1)_implies_FSets0_._s_in_F_)
assume n = (pr1 InvPairFunc) . (k + 1) ; ::_thesis: FSets0 . s in F
then FSets0 . s = (Cvr . n) . s by A7, A9, A11;
hence FSets0 . s in F ; ::_thesis: verum
end;
n in NAT by ORDINAL1:def_12;
then ( n <> (pr1 InvPairFunc) . (k + 1) implies FSets0 . s = {} ) by A7, A9, A11;
hence FSets0 . s in F by A12, PROB_1:4; ::_thesis: verum
end;
then A13: FSets0 is Set_Sequence of F by Def2;
n in NAT by ORDINAL1:def_12;
then D . n = {} by FUNCOP_1:7;
then D . n c= union (rng FSets0) by XBOOLE_1:2;
hence Cvr0 . n is Covering of D . n,F by A9, A13, Def3; ::_thesis: verum
end;
A14: for n being Element of NAT ex y being Element of Funcs (NAT,(bool X)) st S3[n,y]
proof
let n be Element of NAT ; ::_thesis: ex y being Element of Funcs (NAT,(bool X)) st S3[n,y]
A15: now__::_thesis:_(_n_<>_(pr1_InvPairFunc)_._(k_+_1)_implies_ex_y_being_Element_of_Funcs_(NAT,(bool_X))_st_S3[n,y]_)
reconsider y = Cvr . n as Element of Funcs (NAT,(bool X)) by FUNCT_2:8;
assume A16: n <> (pr1 InvPairFunc) . (k + 1) ; ::_thesis: ex y being Element of Funcs (NAT,(bool X)) st S3[n,y]
take y = y; ::_thesis: S3[n,y]
thus S3[n,y] by A16; ::_thesis: verum
end;
( n = (pr1 InvPairFunc) . (k + 1) implies S3[n,y] ) by FUNCOP_1:7;
hence ex y being Element of Funcs (NAT,(bool X)) st S3[n,y] by A15; ::_thesis: verum
end;
consider Cvr1 being Function of NAT,(Funcs (NAT,(bool X))) such that
A17: for n being Element of NAT holds S3[n,Cvr1 . n] from FUNCT_2:sch_3(A14);
for n being Nat holds Cvr1 . n is Covering of D . n,F
proof
let n be Nat; ::_thesis: Cvr1 . n is Covering of D . n,F
consider FSets1 being Function such that
A18: Cvr1 . n = FSets1 and
A19: ( dom FSets1 = NAT & rng FSets1 c= bool X ) by FUNCT_2:def_2;
reconsider FSets1 = FSets1 as Function of NAT,(bool X) by A19, FUNCT_2:2;
for s being Nat holds FSets1 . s in F
proof
let s be Nat; ::_thesis: FSets1 . s in F
A20: s in NAT by ORDINAL1:def_12;
A21: n in NAT by ORDINAL1:def_12;
A22: now__::_thesis:_(_n_<>_(pr1_InvPairFunc)_._(k_+_1)_implies_FSets1_._s_in_F_)
assume n <> (pr1 InvPairFunc) . (k + 1) ; ::_thesis: FSets1 . s in F
then FSets1 . s = (Cvr . n) . s by A17, A18, A21, A20;
hence FSets1 . s in F ; ::_thesis: verum
end;
( n = (pr1 InvPairFunc) . (k + 1) implies FSets1 . s = {} ) by A17, A18, A20;
hence FSets1 . s in F by A22, PROB_1:4; ::_thesis: verum
end;
then A23: FSets1 is Set_Sequence of F by Def2;
n in NAT by ORDINAL1:def_12;
then D . n = {} by FUNCOP_1:7;
then D . n c= union (rng FSets1) by XBOOLE_1:2;
hence Cvr1 . n is Covering of D . n,F by A18, A23, Def3; ::_thesis: verum
end;
then reconsider Cvr1 = Cvr1 as Covering of D,F by Def4;
reconsider Cvr0 = Cvr0 as Covering of D,F by A8, Def4;
set PSv1 = Partial_Sums (vol (M,(On Cvr1)));
(On Cvr1) . (k + 1) = (Cvr1 . ((pr1 InvPairFunc) . (k + 1))) . ((pr2 InvPairFunc) . (k + 1)) by Def10
.= {} by A17 ;
then A24: (vol (M,(On Cvr1))) . (k + 1) = M . {} by Def5
.= 0 by VALUED_0:def_19 ;
set PSv0 = Partial_Sums (vol (M,(On Cvr0)));
set PSv = Partial_Sums (vol (M,(On Cvr)));
defpred S4[ Element of N0, Element of NAT ] means $2 = (pr2 InvPairFunc) . $1;
A25: for s being Element of N0 ex y being Element of NAT st S4[s,y] ;
consider SOS being Function of N0,NAT such that
A26: for s being Element of N0 holds S4[s,SOS . s] from FUNCT_2:sch_3(A25);
A27: for s being Element of NAT holds
( ( s in N0 implies (vol (M,(On Cvr0))) . s = ((vol (M,(Cvr0 . ((pr1 InvPairFunc) . (k + 1))))) * SOS) . s ) & ( not s in N0 implies (vol (M,(On Cvr0))) . s = 0 ) )
proof
let s be Element of NAT ; ::_thesis: ( ( s in N0 implies (vol (M,(On Cvr0))) . s = ((vol (M,(Cvr0 . ((pr1 InvPairFunc) . (k + 1))))) * SOS) . s ) & ( not s in N0 implies (vol (M,(On Cvr0))) . s = 0 ) )
thus ( s in N0 implies (vol (M,(On Cvr0))) . s = ((vol (M,(Cvr0 . ((pr1 InvPairFunc) . (k + 1))))) * SOS) . s ) ::_thesis: ( not s in N0 implies (vol (M,(On Cvr0))) . s = 0 )
proof
A28: (vol (M,(On Cvr0))) . s = M . ((On Cvr0) . s) by Def5;
assume A29: s in N0 ; ::_thesis: (vol (M,(On Cvr0))) . s = ((vol (M,(Cvr0 . ((pr1 InvPairFunc) . (k + 1))))) * SOS) . s
then ( ex s1 being Element of NAT st
( s1 = s & (pr1 InvPairFunc) . (k + 1) = (pr1 InvPairFunc) . s1 ) & (pr2 InvPairFunc) . s = SOS . s ) by A26;
then (vol (M,(On Cvr0))) . s = M . ((Cvr0 . ((pr1 InvPairFunc) . (k + 1))) . (SOS . s)) by A28, Def10;
then (vol (M,(On Cvr0))) . s = (vol (M,(Cvr0 . ((pr1 InvPairFunc) . (k + 1))))) . (SOS . s) by Def5;
hence (vol (M,(On Cvr0))) . s = ((vol (M,(Cvr0 . ((pr1 InvPairFunc) . (k + 1))))) * SOS) . s by A29, FUNCT_2:15; ::_thesis: verum
end;
assume not s in N0 ; ::_thesis: (vol (M,(On Cvr0))) . s = 0
then A30: not (pr1 InvPairFunc) . (k + 1) = (pr1 InvPairFunc) . s ;
(vol (M,(On Cvr0))) . s = M . ((On Cvr0) . s) by Def5
.= M . ((Cvr0 . ((pr1 InvPairFunc) . s)) . ((pr2 InvPairFunc) . s)) by Def10
.= M . {} by A7, A30 ;
hence (vol (M,(On Cvr0))) . s = 0 by VALUED_0:def_19; ::_thesis: verum
end;
now__::_thesis:_for_s1,_s2_being_set_st_s1_in_N0_&_s2_in_N0_&_SOS_._s1_=_SOS_._s2_holds_
s1_=_s2
let s1, s2 be set ; ::_thesis: ( s1 in N0 & s2 in N0 & SOS . s1 = SOS . s2 implies s1 = s2 )
assume that
A31: ( s1 in N0 & s2 in N0 ) and
A32: SOS . s1 = SOS . s2 ; ::_thesis: s1 = s2
A33: ( ex s11 being Element of NAT st
( s11 = s1 & (pr1 InvPairFunc) . (k + 1) = (pr1 InvPairFunc) . s11 ) & ex s22 being Element of NAT st
( s22 = s2 & (pr1 InvPairFunc) . (k + 1) = (pr1 InvPairFunc) . s22 ) ) by A31;
A34: ( InvPairFunc . s1 = [((pr1 InvPairFunc) . s1),((pr2 InvPairFunc) . s1)] & InvPairFunc . s2 = [((pr1 InvPairFunc) . s2),((pr2 InvPairFunc) . s2)] ) by A31, FUNCT_2:119;
( SOS . s1 = (pr2 InvPairFunc) . s1 & SOS . s2 = (pr2 InvPairFunc) . s2 ) by A26, A31;
hence s1 = s2 by A32, A33, A34, FUNCT_2:19, NAGATA_2:2; ::_thesis: verum
end;
then A35: SOS is one-to-one by FUNCT_2:19;
(Ser (vol (M,(On Cvr1)))) . (k + 1) = ((Ser (vol (M,(On Cvr1)))) . k) + ((vol (M,(On Cvr1))) . (k + 1)) by SUPINF_2:44
.= (Ser (vol (M,(On Cvr1)))) . k by A24, XXREAL_3:4 ;
then (Partial_Sums (vol (M,(On Cvr1)))) . (k + 1) = (Ser (vol (M,(On Cvr1)))) . k by Th1;
then A36: (Partial_Sums (vol (M,(On Cvr1)))) . (k + 1) = (Partial_Sums (vol (M,(On Cvr1)))) . k by Th1;
for s being Element of NAT holds 0. <= (Volume (M,Cvr0)) . s by Th5;
then A37: Volume (M,Cvr0) is nonnegative by SUPINF_2:39;
then (Volume (M,Cvr0)) . ((pr1 InvPairFunc) . (k + 1)) <= (Ser (Volume (M,Cvr0))) . ((pr1 InvPairFunc) . (k + 1)) by MEASURE7:2;
then A38: SUM (vol (M,(Cvr0 . ((pr1 InvPairFunc) . (k + 1))))) <= (Ser (Volume (M,Cvr0))) . ((pr1 InvPairFunc) . (k + 1)) by Def6;
A39: m0 is Element of NAT by ORDINAL1:def_12;
then (Ser (Volume (M,Cvr0))) . ((pr1 InvPairFunc) . (k + 1)) <= (Ser (Volume (M,Cvr0))) . m by A37, SUPINF_2:41;
then A40: SUM (vol (M,(Cvr0 . ((pr1 InvPairFunc) . (k + 1))))) <= (Ser (Volume (M,Cvr0))) . m by A38, XXREAL_0:2;
vol (M,(Cvr0 . ((pr1 InvPairFunc) . (k + 1)))) is nonnegative by Th4;
then SUM (vol (M,(On Cvr0))) <= SUM (vol (M,(Cvr0 . ((pr1 InvPairFunc) . (k + 1))))) by A35, A27, MEASURE7:11;
then A41: SUM (vol (M,(On Cvr0))) <= (Ser (Volume (M,Cvr0))) . m by A40, XXREAL_0:2;
(Ser (vol (M,(On Cvr0)))) . (k + 1) <= SUM (vol (M,(On Cvr0))) by Th4, MEASURE7:6;
then (Ser (vol (M,(On Cvr0)))) . (k + 1) <= (Ser (Volume (M,Cvr0))) . m by A41, XXREAL_0:2;
then (Partial_Sums (vol (M,(On Cvr0)))) . (k + 1) <= (Ser (Volume (M,Cvr0))) . m by Th1;
then A42: (Partial_Sums (vol (M,(On Cvr0)))) . (k + 1) <= (Partial_Sums (Volume (M,Cvr0))) . m by Th1;
for s being Element of NAT holds 0. <= (Volume (M,Cvr1)) . s by Th5;
then A43: Volume (M,Cvr1) is nonnegative by SUPINF_2:39;
then ( m0 <= m & Partial_Sums (Volume (M,Cvr1)) is non-decreasing ) by MESFUNC9:16, NAT_1:11;
then A44: (Partial_Sums (Volume (M,Cvr1))) . m0 <= (Partial_Sums (Volume (M,Cvr1))) . m by A39, RINFSUP2:7;
A45: for n being Element of NAT holds (vol (M,(On Cvr))) . n = ((vol (M,(On Cvr0))) . n) + ((vol (M,(On Cvr1))) . n)
proof
let n be Element of NAT ; ::_thesis: (vol (M,(On Cvr))) . n = ((vol (M,(On Cvr0))) . n) + ((vol (M,(On Cvr1))) . n)
set n1 = (pr1 InvPairFunc) . n;
set n2 = (pr2 InvPairFunc) . n;
A46: ( (vol (M,(On Cvr0))) . n = M . ((On Cvr0) . n) & (vol (M,(On Cvr1))) . n = M . ((On Cvr1) . n) ) by Def5;
(vol (M,(On Cvr))) . n = M . ((On Cvr) . n) by Def5;
then A47: (vol (M,(On Cvr))) . n = M . ((Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n)) by Def10;
percases ( (pr1 InvPairFunc) . n = (pr1 InvPairFunc) . (k + 1) or (pr1 InvPairFunc) . n <> (pr1 InvPairFunc) . (k + 1) ) ;
supposeA48: (pr1 InvPairFunc) . n = (pr1 InvPairFunc) . (k + 1) ; ::_thesis: (vol (M,(On Cvr))) . n = ((vol (M,(On Cvr0))) . n) + ((vol (M,(On Cvr1))) . n)
(On Cvr1) . n = (Cvr1 . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) by Def10
.= {} by A17, A48 ;
then A49: M . ((On Cvr1) . n) = 0 by VALUED_0:def_19;
(On Cvr0) . n = (Cvr0 . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) by Def10
.= (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) by A7, A48 ;
hence (vol (M,(On Cvr))) . n = ((vol (M,(On Cvr0))) . n) + ((vol (M,(On Cvr1))) . n) by A46, A47, A49, XXREAL_3:4; ::_thesis: verum
end;
supposeA50: (pr1 InvPairFunc) . n <> (pr1 InvPairFunc) . (k + 1) ; ::_thesis: (vol (M,(On Cvr))) . n = ((vol (M,(On Cvr0))) . n) + ((vol (M,(On Cvr1))) . n)
(On Cvr0) . n = (Cvr0 . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) by Def10
.= {} by A7, A50 ;
then A51: M . ((On Cvr0) . n) = 0 by VALUED_0:def_19;
(On Cvr1) . n = (Cvr1 . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) by Def10
.= (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) by A17, A50 ;
hence (vol (M,(On Cvr))) . n = ((vol (M,(On Cvr0))) . n) + ((vol (M,(On Cvr1))) . n) by A46, A47, A51, XXREAL_3:4; ::_thesis: verum
end;
end;
end;
( vol (M,(On Cvr0)) is nonnegative & vol (M,(On Cvr1)) is nonnegative ) by Th4;
then (Ser (vol (M,(On Cvr)))) . (k + 1) = ((Ser (vol (M,(On Cvr0)))) . (k + 1)) + ((Ser (vol (M,(On Cvr1)))) . (k + 1)) by A45, MEASURE7:3;
then (Partial_Sums (vol (M,(On Cvr)))) . (k + 1) = ((Ser (vol (M,(On Cvr0)))) . (k + 1)) + ((Ser (vol (M,(On Cvr1)))) . (k + 1)) by Th1;
then (Partial_Sums (vol (M,(On Cvr)))) . (k + 1) = ((Partial_Sums (vol (M,(On Cvr0)))) . (k + 1)) + ((Ser (vol (M,(On Cvr1)))) . (k + 1)) by Th1;
then A52: (Partial_Sums (vol (M,(On Cvr)))) . (k + 1) = ((Partial_Sums (vol (M,(On Cvr0)))) . (k + 1)) + ((Partial_Sums (vol (M,(On Cvr1)))) . (k + 1)) by Th1;
(Partial_Sums (vol (M,(On Cvr1)))) . k <= (Partial_Sums (Volume (M,Cvr1))) . m0 by A3;
then A53: (Partial_Sums (vol (M,(On Cvr1)))) . (k + 1) <= (Partial_Sums (Volume (M,Cvr1))) . m by A36, A44, XXREAL_0:2;
for n being Element of NAT holds (Volume (M,Cvr)) . n = ((Volume (M,Cvr0)) . n) + ((Volume (M,Cvr1)) . n)
proof
let n be Element of NAT ; ::_thesis: (Volume (M,Cvr)) . n = ((Volume (M,Cvr0)) . n) + ((Volume (M,Cvr1)) . n)
A54: now__::_thesis:_(_n_<>_(pr1_InvPairFunc)_._(k_+_1)_implies_SUM_(vol_(M,(Cvr_._n)))_=_(SUM_(vol_(M,(Cvr0_._n))))_+_(SUM_(vol_(M,(Cvr1_._n))))_)
assume A55: n <> (pr1 InvPairFunc) . (k + 1) ; ::_thesis: SUM (vol (M,(Cvr . n))) = (SUM (vol (M,(Cvr0 . n)))) + (SUM (vol (M,(Cvr1 . n))))
for s being Element of NAT holds (vol (M,(Cvr0 . n))) . s = 0.
proof
let s be Element of NAT ; ::_thesis: (vol (M,(Cvr0 . n))) . s = 0.
(Cvr0 . n) . s = {} by A7, A55;
then M . ((Cvr0 . n) . s) = 0 by VALUED_0:def_19;
hence (vol (M,(Cvr0 . n))) . s = 0. by Def5; ::_thesis: verum
end;
then A56: SUM (vol (M,(Cvr0 . n))) = 0. by MEASURE7:1;
for s being Element of NAT holds
( (vol (M,(Cvr1 . n))) . s <= (vol (M,(Cvr . n))) . s & (vol (M,(Cvr . n))) . s <= (vol (M,(Cvr1 . n))) . s )
proof
let s be Element of NAT ; ::_thesis: ( (vol (M,(Cvr1 . n))) . s <= (vol (M,(Cvr . n))) . s & (vol (M,(Cvr . n))) . s <= (vol (M,(Cvr1 . n))) . s )
( (vol (M,(Cvr1 . n))) . s = M . ((Cvr1 . n) . s) & (vol (M,(Cvr . n))) . s = M . ((Cvr . n) . s) ) by Def5;
hence ( (vol (M,(Cvr1 . n))) . s <= (vol (M,(Cvr . n))) . s & (vol (M,(Cvr . n))) . s <= (vol (M,(Cvr1 . n))) . s ) by A17, A55; ::_thesis: verum
end;
then ( SUM (vol (M,(Cvr1 . n))) <= SUM (vol (M,(Cvr . n))) & SUM (vol (M,(Cvr . n))) <= SUM (vol (M,(Cvr1 . n))) ) by SUPINF_2:43;
then SUM (vol (M,(Cvr . n))) = SUM (vol (M,(Cvr1 . n))) by XXREAL_0:1;
hence SUM (vol (M,(Cvr . n))) = (SUM (vol (M,(Cvr0 . n)))) + (SUM (vol (M,(Cvr1 . n)))) by A56, XXREAL_3:4; ::_thesis: verum
end;
A57: now__::_thesis:_(_n_=_(pr1_InvPairFunc)_._(k_+_1)_implies_SUM_(vol_(M,(Cvr_._n)))_=_(SUM_(vol_(M,(Cvr0_._n))))_+_(SUM_(vol_(M,(Cvr1_._n))))_)
assume A58: n = (pr1 InvPairFunc) . (k + 1) ; ::_thesis: SUM (vol (M,(Cvr . n))) = (SUM (vol (M,(Cvr0 . n)))) + (SUM (vol (M,(Cvr1 . n))))
for s being Element of NAT holds (vol (M,(Cvr1 . n))) . s = 0
proof
let s be Element of NAT ; ::_thesis: (vol (M,(Cvr1 . n))) . s = 0
(Cvr1 . n) . s = {} by A17, A58;
then M . ((Cvr1 . n) . s) = 0 by VALUED_0:def_19;
hence (vol (M,(Cvr1 . n))) . s = 0 by Def5; ::_thesis: verum
end;
then A59: SUM (vol (M,(Cvr1 . n))) = 0 by MEASURE7:1;
for s being Element of NAT holds
( (vol (M,(Cvr . n))) . s <= (vol (M,(Cvr0 . n))) . s & (vol (M,(Cvr0 . n))) . s <= (vol (M,(Cvr . n))) . s )
proof
let s be Element of NAT ; ::_thesis: ( (vol (M,(Cvr . n))) . s <= (vol (M,(Cvr0 . n))) . s & (vol (M,(Cvr0 . n))) . s <= (vol (M,(Cvr . n))) . s )
(vol (M,(Cvr0 . n))) . s = M . ((Cvr0 . n) . s) by Def5
.= M . ((Cvr . n) . s) by A7, A58 ;
hence ( (vol (M,(Cvr . n))) . s <= (vol (M,(Cvr0 . n))) . s & (vol (M,(Cvr0 . n))) . s <= (vol (M,(Cvr . n))) . s ) by Def5; ::_thesis: verum
end;
then ( SUM (vol (M,(Cvr . n))) <= SUM (vol (M,(Cvr0 . n))) & SUM (vol (M,(Cvr0 . n))) <= SUM (vol (M,(Cvr . n))) ) by SUPINF_2:43;
then SUM (vol (M,(Cvr . n))) = SUM (vol (M,(Cvr0 . n))) by XXREAL_0:1;
hence SUM (vol (M,(Cvr . n))) = (SUM (vol (M,(Cvr0 . n)))) + (SUM (vol (M,(Cvr1 . n)))) by A59, XXREAL_3:4; ::_thesis: verum
end;
( (Volume (M,Cvr)) . n = SUM (vol (M,(Cvr . n))) & (Volume (M,Cvr0)) . n = SUM (vol (M,(Cvr0 . n))) ) by Def6;
hence (Volume (M,Cvr)) . n = ((Volume (M,Cvr0)) . n) + ((Volume (M,Cvr1)) . n) by A57, A54, Def6; ::_thesis: verum
end;
then (Ser (Volume (M,Cvr))) . m = ((Ser (Volume (M,Cvr0))) . m) + ((Ser (Volume (M,Cvr1))) . m) by A37, A43, MEASURE7:3;
then (Partial_Sums (Volume (M,Cvr))) . m = ((Ser (Volume (M,Cvr0))) . m) + ((Ser (Volume (M,Cvr1))) . m) by Th1
.= ((Partial_Sums (Volume (M,Cvr0))) . m) + ((Ser (Volume (M,Cvr1))) . m) by Th1
.= ((Partial_Sums (Volume (M,Cvr0))) . m) + ((Partial_Sums (Volume (M,Cvr1))) . m) by Th1 ;
hence (Partial_Sums (vol (M,(On Cvr)))) . (k + 1) <= (Partial_Sums (Volume (M,Cvr))) . m by A42, A53, A52, XXREAL_3:36; ::_thesis: verum
end;
A60: S1[ 0 ]
proof
take m = (pr1 InvPairFunc) . 0; ::_thesis: for Sets being SetSequence of X
for Cvr being Covering of Sets,F holds (Partial_Sums (vol (M,(On Cvr)))) . 0 <= (Partial_Sums (Volume (M,Cvr))) . m
let Sets be SetSequence of X; ::_thesis: for Cvr being Covering of Sets,F holds (Partial_Sums (vol (M,(On Cvr)))) . 0 <= (Partial_Sums (Volume (M,Cvr))) . m
let Cvr be Covering of Sets,F; ::_thesis: (Partial_Sums (vol (M,(On Cvr)))) . 0 <= (Partial_Sums (Volume (M,Cvr))) . m
for n being Element of NAT holds 0 <= (Volume (M,Cvr)) . n by Th5;
then Volume (M,Cvr) is nonnegative by SUPINF_2:39;
then (Volume (M,Cvr)) . m <= (Ser (Volume (M,Cvr))) . m by MEASURE7:2;
then A61: (Volume (M,Cvr)) . m <= (Partial_Sums (Volume (M,Cvr))) . m by Th1;
( (vol (M,(On Cvr))) . 0 = M . ((On Cvr) . 0) & (vol (M,(Cvr . ((pr1 InvPairFunc) . 0)))) . ((pr2 InvPairFunc) . 0) = M . ((Cvr . ((pr1 InvPairFunc) . 0)) . ((pr2 InvPairFunc) . 0)) ) by Def5;
then (vol (M,(On Cvr))) . 0 <= (vol (M,(Cvr . ((pr1 InvPairFunc) . 0)))) . ((pr2 InvPairFunc) . 0) by Def10;
then (vol (M,(On Cvr))) . 0 <= SUM (vol (M,(Cvr . ((pr1 InvPairFunc) . 0)))) by Th4, MEASURE6:3;
then ( (Partial_Sums (vol (M,(On Cvr)))) . 0 = (vol (M,(On Cvr))) . 0 & (vol (M,(On Cvr))) . 0 <= (Volume (M,Cvr)) . ((pr1 InvPairFunc) . 0) ) by Def6, MESFUNC9:def_1;
hence (Partial_Sums (vol (M,(On Cvr)))) . 0 <= (Partial_Sums (Volume (M,Cvr))) . m by A61, XXREAL_0:2; ::_thesis: verum
end;
thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A60, A1); ::_thesis: verum
end;
theorem Th7: :: MEASURE8:7
for X being set
for F being Field_Subset of X
for M being Measure of F
for Sets being SetSequence of X
for Cvr being Covering of Sets,F holds inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr))
proof
let X be set ; ::_thesis: for F being Field_Subset of X
for M being Measure of F
for Sets being SetSequence of X
for Cvr being Covering of Sets,F holds inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr))
let F be Field_Subset of X; ::_thesis: for M being Measure of F
for Sets being SetSequence of X
for Cvr being Covering of Sets,F holds inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr))
let M be Measure of F; ::_thesis: for Sets being SetSequence of X
for Cvr being Covering of Sets,F holds inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr))
let Sets be SetSequence of X; ::_thesis: for Cvr being Covering of Sets,F holds inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr))
let Cvr be Covering of Sets,F; ::_thesis: inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr))
set Q = SUM (vol (M,(On Cvr)));
for x being ext-real number st x in rng (Ser (vol (M,(On Cvr)))) holds
ex y being ext-real number st
( y in rng (Ser (Volume (M,Cvr))) & x <= y )
proof
let x be ext-real number ; ::_thesis: ( x in rng (Ser (vol (M,(On Cvr)))) implies ex y being ext-real number st
( y in rng (Ser (Volume (M,Cvr))) & x <= y ) )
assume x in rng (Ser (vol (M,(On Cvr)))) ; ::_thesis: ex y being ext-real number st
( y in rng (Ser (Volume (M,Cvr))) & x <= y )
then consider n being Element of NAT such that
A1: x = (Ser (vol (M,(On Cvr)))) . n by FUNCT_2:113;
consider m being Nat such that
A2: for Sets being SetSequence of X
for G being Covering of Sets,F holds (Partial_Sums (vol (M,(On G)))) . n <= (Partial_Sums (Volume (M,G))) . m by Th6;
take (Ser (Volume (M,Cvr))) . m ; ::_thesis: ( (Ser (Volume (M,Cvr))) . m in rng (Ser (Volume (M,Cvr))) & x <= (Ser (Volume (M,Cvr))) . m )
A3: for Sets being SetSequence of X
for G being Covering of Sets,F holds (Ser (vol (M,(On G)))) . n <= (Ser (Volume (M,G))) . m
proof
let Sets be SetSequence of X; ::_thesis: for G being Covering of Sets,F holds (Ser (vol (M,(On G)))) . n <= (Ser (Volume (M,G))) . m
let G be Covering of Sets,F; ::_thesis: (Ser (vol (M,(On G)))) . n <= (Ser (Volume (M,G))) . m
(Partial_Sums (vol (M,(On G)))) . n <= (Partial_Sums (Volume (M,G))) . m by A2;
then (Ser (vol (M,(On G)))) . n <= (Partial_Sums (Volume (M,G))) . m by Th1;
hence (Ser (vol (M,(On G)))) . n <= (Ser (Volume (M,G))) . m by Th1; ::_thesis: verum
end;
m in NAT by ORDINAL1:def_12;
hence ( (Ser (Volume (M,Cvr))) . m in rng (Ser (Volume (M,Cvr))) & x <= (Ser (Volume (M,Cvr))) . m ) by A1, A3, FUNCT_2:4; ::_thesis: verum
end;
then A4: SUM (vol (M,(On Cvr))) <= SUM (Volume (M,Cvr)) by XXREAL_2:63;
SUM (vol (M,(On Cvr))) in Svc (M,(union (rng Sets))) by Def7;
then inf (Svc (M,(union (rng Sets)))) <= SUM (vol (M,(On Cvr))) by XXREAL_2:3;
hence inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,Cvr)) by A4, XXREAL_0:2; ::_thesis: verum
end;
theorem Th8: :: MEASURE8:8
for X being set
for F being Field_Subset of X
for A being Subset of X st A in F holds
(A,({} X)) followed_by ({} X) is Covering of A,F
proof
let X be set ; ::_thesis: for F being Field_Subset of X
for A being Subset of X st A in F holds
(A,({} X)) followed_by ({} X) is Covering of A,F
let F be Field_Subset of X; ::_thesis: for A being Subset of X st A in F holds
(A,({} X)) followed_by ({} X) is Covering of A,F
let A be Subset of X; ::_thesis: ( A in F implies (A,({} X)) followed_by ({} X) is Covering of A,F )
reconsider Sets = (A,({} X)) followed_by ({} X) as SetSequence of X ;
A1: Sets . 0 = A by FUNCT_7:122;
A2: Sets . 1 = {} X by FUNCT_7:123;
assume A3: A in F ; ::_thesis: (A,({} X)) followed_by ({} X) is Covering of A,F
for n being Nat holds Sets . n in F
proof
let n be Nat; ::_thesis: Sets . n in F
percases ( n = 0 or n = 1 or n > 1 ) by NAT_1:25;
suppose n = 0 ; ::_thesis: Sets . n in F
hence Sets . n in F by A3, FUNCT_7:122; ::_thesis: verum
end;
suppose n = 1 ; ::_thesis: Sets . n in F
hence Sets . n in F by A2, PROB_1:4; ::_thesis: verum
end;
suppose n > 1 ; ::_thesis: Sets . n in F
then Sets . n = {} by FUNCT_7:124;
hence Sets . n in F by PROB_1:4; ::_thesis: verum
end;
end;
end;
then reconsider Sets = Sets as Set_Sequence of F by Def2;
A c= union (rng Sets)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in union (rng Sets) )
dom Sets = NAT by FUNCT_2:def_1;
then A4: Sets . 0 in rng Sets by FUNCT_1:3;
assume x in A ; ::_thesis: x in union (rng Sets)
hence x in union (rng Sets) by A1, A4, TARSKI:def_4; ::_thesis: verum
end;
hence (A,({} X)) followed_by ({} X) is Covering of A,F by Def3; ::_thesis: verum
end;
theorem Th9: :: MEASURE8:9
for X being set
for F being Field_Subset of X
for M being Measure of F
for A being set st A in F holds
(C_Meas M) . A <= M . A
proof
let X be set ; ::_thesis: for F being Field_Subset of X
for M being Measure of F
for A being set st A in F holds
(C_Meas M) . A <= M . A
let F be Field_Subset of X; ::_thesis: for M being Measure of F
for A being set st A in F holds
(C_Meas M) . A <= M . A
let M be Measure of F; ::_thesis: for A being set st A in F holds
(C_Meas M) . A <= M . A
let A9 be set ; ::_thesis: ( A9 in F implies (C_Meas M) . A9 <= M . A9 )
assume A1: A9 in F ; ::_thesis: (C_Meas M) . A9 <= M . A9
then reconsider A = A9 as Subset of X ;
reconsider Aseq = (A,({} X)) followed_by ({} X) as Set_Sequence of F by A1, Th8;
A2: Aseq . 1 = {} X by FUNCT_7:123;
A3: Aseq . 0 = A by FUNCT_7:122;
A c= union (rng Aseq)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in union (rng Aseq) )
dom Aseq = NAT by FUNCT_2:def_1;
then A4: Aseq . 0 in rng Aseq by FUNCT_1:3;
assume x in A ; ::_thesis: x in union (rng Aseq)
hence x in union (rng Aseq) by A3, A4, TARSKI:def_4; ::_thesis: verum
end;
then reconsider Aseq = Aseq as Covering of A,F by Def3;
A5: for n being Element of NAT st n <> 0 holds
(vol (M,Aseq)) . n = 0
proof
let n be Element of NAT ; ::_thesis: ( n <> 0 implies (vol (M,Aseq)) . n = 0 )
assume n <> 0 ; ::_thesis: (vol (M,Aseq)) . n = 0
then Aseq . n = {} by A2, FUNCT_7:124, NAT_1:25;
then (vol (M,Aseq)) . n = M . {} by Def5;
hence (vol (M,Aseq)) . n = 0 by VALUED_0:def_19; ::_thesis: verum
end;
then for n being Element of NAT st 1 <= n holds
(vol (M,Aseq)) . n = 0 ;
then SUM (vol (M,Aseq)) = (Ser (vol (M,Aseq))) . 1 by Th4, SUPINF_2:48
.= (vol (M,Aseq)) . 0 by A5, MEASURE7:9 ;
then SUM (vol (M,Aseq)) = M . (Aseq . 0) by Def5;
then A6: M . A in Svc (M,A) by A3, Def7;
(C_Meas M) . A = inf (Svc (M,A)) by Def8;
hence (C_Meas M) . A9 <= M . A9 by A6, XXREAL_2:3; ::_thesis: verum
end;
theorem Th10: :: MEASURE8:10
for X being set
for F being Field_Subset of X
for M being Measure of F holds C_Meas M is nonnegative
proof
let X be set ; ::_thesis: for F being Field_Subset of X
for M being Measure of F holds C_Meas M is nonnegative
let F be Field_Subset of X; ::_thesis: for M being Measure of F holds C_Meas M is nonnegative
let M be Measure of F; ::_thesis: C_Meas M is nonnegative
for r being ext-real number st r in rng (C_Meas M) holds
0 <= r
proof
let r be ext-real number ; ::_thesis: ( r in rng (C_Meas M) implies 0 <= r )
assume r in rng (C_Meas M) ; ::_thesis: 0 <= r
then consider A being set such that
A1: A in bool X and
A2: (C_Meas M) . A = r by FUNCT_2:11;
reconsider A = A as Subset of X by A1;
now__::_thesis:_for_p_being_ext-real_number_st_p_in_Svc_(M,A)_holds_
0_<=_p
let p be ext-real number ; ::_thesis: ( p in Svc (M,A) implies 0 <= p )
assume p in Svc (M,A) ; ::_thesis: 0 <= p
then ex G being Covering of A,F st p = SUM (vol (M,G)) by Def7;
hence 0 <= p by Th4, MEASURE6:2; ::_thesis: verum
end;
then 0 is LowerBound of Svc (M,A) by XXREAL_2:def_2;
then 0 <= inf (Svc (M,A)) by XXREAL_2:def_4;
hence 0 <= r by A2, Def8; ::_thesis: verum
end;
then for r being R_eal st r in rng (C_Meas M) holds
0 <= r ;
then rng (C_Meas M) is nonnegative by SUPINF_2:def_9;
hence C_Meas M is nonnegative by SUPINF_2:def_16; ::_thesis: verum
end;
theorem Th11: :: MEASURE8:11
for X being set
for F being Field_Subset of X
for M being Measure of F holds (C_Meas M) . {} = 0
proof
let X be set ; ::_thesis: for F being Field_Subset of X
for M being Measure of F holds (C_Meas M) . {} = 0
let F be Field_Subset of X; ::_thesis: for M being Measure of F holds (C_Meas M) . {} = 0
let M be Measure of F; ::_thesis: (C_Meas M) . {} = 0
(C_Meas M) . {} <= M . {} by Th9, PROB_1:4;
then A1: (C_Meas M) . {} <= 0 by VALUED_0:def_19;
{} X in bool X ;
then {} in dom (C_Meas M) by FUNCT_2:def_1;
then A2: (C_Meas M) . {} in rng (C_Meas M) by FUNCT_1:3;
C_Meas M is nonnegative by Th10;
then rng (C_Meas M) is nonnegative by SUPINF_2:def_16;
hence (C_Meas M) . {} = 0. by A1, A2, SUPINF_2:def_9; ::_thesis: verum
end;
theorem Th12: :: MEASURE8:12
for X being set
for F being Field_Subset of X
for M being Measure of F
for A, B being Subset of X st A c= B holds
(C_Meas M) . A <= (C_Meas M) . B
proof
let X be set ; ::_thesis: for F being Field_Subset of X
for M being Measure of F
for A, B being Subset of X st A c= B holds
(C_Meas M) . A <= (C_Meas M) . B
let F be Field_Subset of X; ::_thesis: for M being Measure of F
for A, B being Subset of X st A c= B holds
(C_Meas M) . A <= (C_Meas M) . B
let M be Measure of F; ::_thesis: for A, B being Subset of X st A c= B holds
(C_Meas M) . A <= (C_Meas M) . B
let A, B be Subset of X; ::_thesis: ( A c= B implies (C_Meas M) . A <= (C_Meas M) . B )
assume A1: A c= B ; ::_thesis: (C_Meas M) . A <= (C_Meas M) . B
now__::_thesis:_for_r_being_set_st_r_in_Svc_(M,B)_holds_
r_in_Svc_(M,A)
let r be set ; ::_thesis: ( r in Svc (M,B) implies r in Svc (M,A) )
assume r in Svc (M,B) ; ::_thesis: r in Svc (M,A)
then consider G being Covering of B,F such that
A2: SUM (vol (M,G)) = r by Def7;
B c= union (rng G) by Def3;
then A c= union (rng G) by A1, XBOOLE_1:1;
then reconsider G1 = G as Covering of A,F by Def3;
SUM (vol (M,G)) = SUM (vol (M,G1)) ;
hence r in Svc (M,A) by A2, Def7; ::_thesis: verum
end;
then A3: Svc (M,B) c= Svc (M,A) by TARSKI:def_3;
( (C_Meas M) . A = inf (Svc (M,A)) & (C_Meas M) . B = inf (Svc (M,B)) ) by Def8;
hence (C_Meas M) . A <= (C_Meas M) . B by A3, XXREAL_2:60; ::_thesis: verum
end;
Lm2: for X being set
for F being Field_Subset of X
for M being Measure of F
for Sets being SetSequence of X st ex n being Nat st (C_Meas M) . (Sets . n) = +infty holds
(C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)
proof
let X be set ; ::_thesis: for F being Field_Subset of X
for M being Measure of F
for Sets being SetSequence of X st ex n being Nat st (C_Meas M) . (Sets . n) = +infty holds
(C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)
let F be Field_Subset of X; ::_thesis: for M being Measure of F
for Sets being SetSequence of X st ex n being Nat st (C_Meas M) . (Sets . n) = +infty holds
(C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)
let M be Measure of F; ::_thesis: for Sets being SetSequence of X st ex n being Nat st (C_Meas M) . (Sets . n) = +infty holds
(C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)
let Sets be SetSequence of X; ::_thesis: ( ex n being Nat st (C_Meas M) . (Sets . n) = +infty implies (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) )
assume ex n being Nat st (C_Meas M) . (Sets . n) = +infty ; ::_thesis: (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)
then consider N being Nat such that
A1: (C_Meas M) . (Sets . N) = +infty ;
reconsider N = N as Element of NAT by ORDINAL1:def_12;
A2: (C_Meas M) * Sets is nonnegative by Th10, MEASURE1:25;
dom Sets = NAT by FUNCT_2:def_1;
then ((C_Meas M) * Sets) . N = (C_Meas M) . (Sets . N) by FUNCT_1:13;
then SUM ((C_Meas M) * Sets) = +infty by A1, A2, SUPINF_2:45;
hence (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) by XXREAL_0:3; ::_thesis: verum
end;
theorem Th13: :: MEASURE8:13
for X being set
for F being Field_Subset of X
for M being Measure of F
for Sets being SetSequence of X holds (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)
proof
let X be set ; ::_thesis: for F being Field_Subset of X
for M being Measure of F
for Sets being SetSequence of X holds (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)
let F be Field_Subset of X; ::_thesis: for M being Measure of F
for Sets being SetSequence of X holds (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)
let M be Measure of F; ::_thesis: for Sets being SetSequence of X holds (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)
let Sets be SetSequence of X; ::_thesis: (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)
A1: now__::_thesis:_(_(_for_n_being_Element_of_NAT_holds_Svc_(M,(Sets_._n))_<>_{+infty}_)_implies_(C_Meas_M)_._(union_(rng_Sets))_<=_SUM_((C_Meas_M)_*_Sets)_)
assume A2: for n being Element of NAT holds Svc (M,(Sets . n)) <> {+infty} ; ::_thesis: (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)
inf (Svc (M,(union (rng Sets)))) <= sup (rng (Ser ((C_Meas M) * Sets)))
proof
set y = inf (Svc (M,(union (rng Sets))));
set x = sup (rng (Ser ((C_Meas M) * Sets)));
A3: (Ser ((C_Meas M) * Sets)) . 0 <= sup (rng (Ser ((C_Meas M) * Sets))) by FUNCT_2:4, XXREAL_2:4;
A4: (C_Meas M) * Sets is nonnegative by Th10, MEASURE1:25;
then 0 <= ((C_Meas M) * Sets) . 0 by SUPINF_2:39;
then A5: 0 <= (Ser ((C_Meas M) * Sets)) . 0 by SUPINF_2:44;
assume not inf (Svc (M,(union (rng Sets)))) <= sup (rng (Ser ((C_Meas M) * Sets))) ; ::_thesis: contradiction
then consider eps being real number such that
A6: 0 < eps and
A7: (sup (rng (Ser ((C_Meas M) * Sets)))) + eps < inf (Svc (M,(union (rng Sets)))) by A5, A3, XXREAL_3:49;
eps in ExtREAL by XXREAL_0:def_1;
then consider E being Function of NAT,ExtREAL such that
A8: for n being Element of NAT holds 0 < E . n and
A9: SUM E < eps by A6, MEASURE6:4;
for n being Element of NAT holds 0 <= E . n by A8;
then A10: E is nonnegative by SUPINF_2:39;
defpred S1[ Element of NAT , set ] means ex F0 being Covering of Sets . $1,F st
( $2 = F0 & SUM (vol (M,F0)) < (inf (Svc (M,(Sets . $1)))) + (E . $1) );
A11: for n being Element of NAT ex F0 being Element of Funcs (NAT,(bool X)) st S1[n,F0]
proof
let n be Element of NAT ; ::_thesis: ex F0 being Element of Funcs (NAT,(bool X)) st S1[n,F0]
( C_Meas M is nonnegative & (C_Meas M) . (Sets . n) = inf (Svc (M,(Sets . n))) ) by Def8, Th10;
then A12: ( 0 is Real & 0. <= inf (Svc (M,(Sets . n))) ) by SUPINF_2:51;
Svc (M,(Sets . n)) <> {+infty} by A2;
then not Svc (M,(Sets . n)) c= {+infty} by ZFMISC_1:33;
then (Svc (M,(Sets . n))) \ {+infty} <> {} by XBOOLE_1:37;
then consider x being set such that
A13: x in (Svc (M,(Sets . n))) \ {+infty} by XBOOLE_0:def_1;
reconsider x = x as R_eal by A13;
not x in {+infty} by A13, XBOOLE_0:def_5;
then A14: x <> +infty by TARSKI:def_1;
x in Svc (M,(Sets . n)) by A13, XBOOLE_0:def_5;
then inf (Svc (M,(Sets . n))) <= x by XXREAL_2:3;
then inf (Svc (M,(Sets . n))) < +infty by A14, XXREAL_0:2, XXREAL_0:4;
then inf (Svc (M,(Sets . n))) is Real by A12, XXREAL_0:46;
then consider S1 being ext-real number such that
A15: S1 in Svc (M,(Sets . n)) and
A16: S1 < (inf (Svc (M,(Sets . n)))) + (E . n) by A8, MEASURE6:5;
consider FS being Covering of Sets . n,F such that
A17: S1 = SUM (vol (M,FS)) by A15, Def7;
reconsider FS = FS as Element of Funcs (NAT,(bool X)) by FUNCT_2:8;
take FS ; ::_thesis: S1[n,FS]
thus S1[n,FS] by A16, A17; ::_thesis: verum
end;
consider FF being Function of NAT,(Funcs (NAT,(bool X))) such that
A18: for n being Element of NAT holds S1[n,FF . n] from FUNCT_2:sch_3(A11);
A19: for n being Nat holds FF . n is Covering of Sets . n,F
proof
let n be Nat; ::_thesis: FF . n is Covering of Sets . n,F
n in NAT by ORDINAL1:def_12;
then ex F0 being Covering of Sets . n,F st
( F0 = FF . n & SUM (vol (M,F0)) < (inf (Svc (M,(Sets . n)))) + (E . n) ) by A18;
hence FF . n is Covering of Sets . n,F ; ::_thesis: verum
end;
deffunc H1( Element of NAT ) -> set = (((C_Meas M) * Sets) . $1) + (E . $1);
A20: for x being Element of NAT holds H1(x) is Element of ExtREAL by XXREAL_0:def_1;
consider G0 being Function of NAT,ExtREAL such that
A21: for n being Element of NAT holds G0 . n = H1(n) from FUNCT_2:sch_9(A20);
reconsider FF = FF as Covering of Sets,F by A19, Def4;
for n being Element of NAT holds (Volume (M,FF)) . n <= G0 . n
proof
let n be Element of NAT ; ::_thesis: (Volume (M,FF)) . n <= G0 . n
( ex F0 being Covering of Sets . n,F st
( F0 = FF . n & SUM (vol (M,F0)) < (inf (Svc (M,(Sets . n)))) + (E . n) ) & ((C_Meas M) * Sets) . n = (C_Meas M) . (Sets . n) ) by A18, FUNCT_2:15;
then SUM (vol (M,(FF . n))) < (((C_Meas M) * Sets) . n) + (E . n) by Def8;
then (Volume (M,FF)) . n < (((C_Meas M) * Sets) . n) + (E . n) by Def6;
hence (Volume (M,FF)) . n <= G0 . n by A21; ::_thesis: verum
end;
then A22: SUM (Volume (M,FF)) <= SUM G0 by SUPINF_2:43;
A23: now__::_thesis:_for_n_being_Nat_holds_G0_._n_=_(((C_Meas_M)_*_Sets)_._n)_+_(E_._n)
let n be Nat; ::_thesis: G0 . n = (((C_Meas M) * Sets) . n) + (E . n)
n is Element of NAT by ORDINAL1:def_12;
hence G0 . n = (((C_Meas M) * Sets) . n) + (E . n) by A21; ::_thesis: verum
end;
(SUM ((C_Meas M) * Sets)) + (SUM E) <= (SUM ((C_Meas M) * Sets)) + eps by A9, XXREAL_3:36;
then SUM G0 <= (SUM ((C_Meas M) * Sets)) + eps by A4, A10, A23, Th3;
then A24: SUM (Volume (M,FF)) <= (SUM ((C_Meas M) * Sets)) + eps by A22, XXREAL_0:2;
inf (Svc (M,(union (rng Sets)))) <= SUM (Volume (M,FF)) by Th7;
hence contradiction by A7, A24, XXREAL_0:2; ::_thesis: verum
end;
hence (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) by Def8; ::_thesis: verum
end;
now__::_thesis:_(_ex_n_being_Element_of_NAT_st_Svc_(M,(Sets_._n))_=_{+infty}_implies_(C_Meas_M)_._(union_(rng_Sets))_<=_SUM_((C_Meas_M)_*_Sets)_)
assume ex n being Element of NAT st Svc (M,(Sets . n)) = {+infty} ; ::_thesis: (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets)
then consider n being Element of NAT such that
A25: Svc (M,(Sets . n)) = {+infty} ;
inf {+infty} = +infty by XXREAL_2:13;
then (C_Meas M) . (Sets . n) = +infty by A25, Def8;
hence (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) by Lm2; ::_thesis: verum
end;
hence (C_Meas M) . (union (rng Sets)) <= SUM ((C_Meas M) * Sets) by A1; ::_thesis: verum
end;
theorem Th14: :: MEASURE8:14
for X being set
for F being Field_Subset of X
for M being Measure of F holds C_Meas M is C_Measure of X
proof
let X be set ; ::_thesis: for F being Field_Subset of X
for M being Measure of F holds C_Meas M is C_Measure of X
let F be Field_Subset of X; ::_thesis: for M being Measure of F holds C_Meas M is C_Measure of X
let M be Measure of F; ::_thesis: C_Meas M is C_Measure of X
(C_Meas M) . {} = 0. by Th11;
then A1: C_Meas M is zeroed by VALUED_0:def_19;
( C_Meas M is nonnegative & ( for A, B being Subset of X st A c= B holds
( (C_Meas M) . A <= (C_Meas M) . B & ( for F being Function of NAT,(bool X) holds (C_Meas M) . (union (rng F)) <= SUM ((C_Meas M) * F) ) ) ) ) by Th10, Th12, Th13;
hence C_Meas M is C_Measure of X by A1, MEASURE4:def_1; ::_thesis: verum
end;
definition
let X be set ;
let F be Field_Subset of X;
let M be Measure of F;
:: original: C_Meas
redefine func C_Meas M -> C_Measure of X;
correctness
coherence
C_Meas M is C_Measure of X;
by Th14;
end;
begin
definition
let X be set ;
let F be Field_Subset of X;
let M be Measure of F;
attrM is completely-additive means :Def11: :: MEASURE8:def 11
for FSets being Sep_Sequence of F st union (rng FSets) in F holds
SUM (M * FSets) = M . (union (rng FSets));
end;
:: deftheorem Def11 defines completely-additive MEASURE8:def_11_:_
for X being set
for F being Field_Subset of X
for M being Measure of F holds
( M is completely-additive iff for FSets being Sep_Sequence of F st union (rng FSets) in F holds
SUM (M * FSets) = M . (union (rng FSets)) );
theorem Th15: :: MEASURE8:15
for X being set
for F being Field_Subset of X
for FSets being Set_Sequence of F holds Partial_Union FSets is Set_Sequence of F
proof
let X be set ; ::_thesis: for F being Field_Subset of X
for FSets being Set_Sequence of F holds Partial_Union FSets is Set_Sequence of F
let F be Field_Subset of X; ::_thesis: for FSets being Set_Sequence of F holds Partial_Union FSets is Set_Sequence of F
let FSets be Set_Sequence of F; ::_thesis: Partial_Union FSets is Set_Sequence of F
defpred S1[ Nat] means (Partial_Union FSets) . $1 in F;
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
A2: (Partial_Union FSets) . (k + 1) = ((Partial_Union FSets) . k) \/ (FSets . (k + 1)) by PROB_3:def_2;
assume S1[k] ; ::_thesis: S1[k + 1]
hence S1[k + 1] by A2, PROB_1:3; ::_thesis: verum
end;
(Partial_Union FSets) . 0 = FSets . 0 by PROB_3:def_2;
then A3: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1);
hence Partial_Union FSets is Set_Sequence of F by Def2; ::_thesis: verum
end;
theorem Th16: :: MEASURE8:16
for X being set
for F being Field_Subset of X
for FSets being Set_Sequence of F holds Partial_Diff_Union FSets is Set_Sequence of F
proof
let X be set ; ::_thesis: for F being Field_Subset of X
for FSets being Set_Sequence of F holds Partial_Diff_Union FSets is Set_Sequence of F
let F be Field_Subset of X; ::_thesis: for FSets being Set_Sequence of F holds Partial_Diff_Union FSets is Set_Sequence of F
let FSets be Set_Sequence of F; ::_thesis: Partial_Diff_Union FSets is Set_Sequence of F
defpred S1[ Nat] means (Partial_Diff_Union FSets) . $1 in F;
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; ::_thesis: S1[k + 1]
Partial_Union FSets is Set_Sequence of F by Th15;
then A2: (Partial_Union FSets) . k in F by Def2;
(Partial_Diff_Union FSets) . (k + 1) = (FSets . (k + 1)) \ ((Partial_Union FSets) . k) by PROB_3:def_3;
hence S1[k + 1] by A2, PROB_1:6; ::_thesis: verum
end;
(Partial_Diff_Union FSets) . 0 = FSets . 0 by PROB_3:def_3;
then A3: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch_2(A3, A1);
hence Partial_Diff_Union FSets is Set_Sequence of F by Def2; ::_thesis: verum
end;
theorem Th17: :: MEASURE8:17
for X being set
for F being Field_Subset of X
for A being Subset of X
for CA being Covering of A,F st A in F holds
ex FSets being Sep_Sequence of F st
( A = union (rng FSets) & ( for n being Nat holds FSets . n c= CA . n ) )
proof
let X be set ; ::_thesis: for F being Field_Subset of X
for A being Subset of X
for CA being Covering of A,F st A in F holds
ex FSets being Sep_Sequence of F st
( A = union (rng FSets) & ( for n being Nat holds FSets . n c= CA . n ) )
let F be Field_Subset of X; ::_thesis: for A being Subset of X
for CA being Covering of A,F st A in F holds
ex FSets being Sep_Sequence of F st
( A = union (rng FSets) & ( for n being Nat holds FSets . n c= CA . n ) )
let A be Subset of X; ::_thesis: for CA being Covering of A,F st A in F holds
ex FSets being Sep_Sequence of F st
( A = union (rng FSets) & ( for n being Nat holds FSets . n c= CA . n ) )
let CA be Covering of A,F; ::_thesis: ( A in F implies ex FSets being Sep_Sequence of F st
( A = union (rng FSets) & ( for n being Nat holds FSets . n c= CA . n ) ) )
deffunc H1( Element of NAT ) -> Element of bool X = ((Partial_Diff_Union CA) . $1) /\ A;
consider FSets being Function of NAT,(bool X) such that
A1: for n being Element of NAT holds FSets . n = H1(n) from FUNCT_2:sch_4();
reconsider FSets = FSets as SetSequence of X ;
assume A2: A in F ; ::_thesis: ex FSets being Sep_Sequence of F st
( A = union (rng FSets) & ( for n being Nat holds FSets . n c= CA . n ) )
now__::_thesis:_for_y_being_set_st_y_in_rng_FSets_holds_
y_in_F
let y be set ; ::_thesis: ( y in rng FSets implies y in F )
assume y in rng FSets ; ::_thesis: y in F
then consider x being set such that
A3: x in NAT and
A4: FSets . x = y by FUNCT_2:11;
reconsider n = x as Element of NAT by A3;
A5: FSets . n = ((Partial_Diff_Union CA) . n) /\ A by A1;
Partial_Diff_Union CA is Set_Sequence of F by Th16;
then (Partial_Diff_Union CA) . n in F by Def2;
hence y in F by A2, A4, A5, FINSUB_1:def_2; ::_thesis: verum
end;
then rng FSets c= F by TARSKI:def_3;
then reconsider FSets = FSets as Function of NAT,F by FUNCT_2:6;
for m, n being Nat st m <> n holds
FSets . m misses FSets . n
proof
let m, n be Nat; ::_thesis: ( m <> n implies FSets . m misses FSets . n )
n in NAT by ORDINAL1:def_12;
then FSets . n = ((Partial_Diff_Union CA) . n) /\ A by A1;
then A6: FSets . n c= (Partial_Diff_Union CA) . n by XBOOLE_1:17;
m in NAT by ORDINAL1:def_12;
then FSets . m = ((Partial_Diff_Union CA) . m) /\ A by A1;
then A7: FSets . m c= (Partial_Diff_Union CA) . m by XBOOLE_1:17;
assume m <> n ; ::_thesis: FSets . m misses FSets . n
then (Partial_Diff_Union CA) . m misses (Partial_Diff_Union CA) . n by PROB_3:def_4;
hence FSets . m misses FSets . n by A7, A6, XBOOLE_1:64; ::_thesis: verum
end;
then reconsider FSets = FSets as Sep_Sequence of F by PROB_3:def_4;
now__::_thesis:_for_x_being_set_st_x_in_A_holds_
x_in_union_(rng_FSets)
let x be set ; ::_thesis: ( x in A implies x in union (rng FSets) )
assume A8: x in A ; ::_thesis: x in union (rng FSets)
A c= union (rng CA) by Def3;
then x in union (rng CA) by A8;
then x in Union CA by CARD_3:def_4;
then x in Union (Partial_Diff_Union CA) by PROB_3:20;
then x in union (rng (Partial_Diff_Union CA)) by CARD_3:def_4;
then consider E being set such that
A9: x in E and
A10: E in rng (Partial_Diff_Union CA) by TARSKI:def_4;
consider n being set such that
A11: n in NAT and
A12: (Partial_Diff_Union CA) . n = E by A10, FUNCT_2:11;
reconsider n = n as Element of NAT by A11;
x in ((Partial_Diff_Union CA) . n) /\ A by A8, A9, A12, XBOOLE_0:def_4;
then A13: x in FSets . n by A1;
FSets . n in rng FSets by FUNCT_2:4;
hence x in union (rng FSets) by A13, TARSKI:def_4; ::_thesis: verum
end;
then A14: A c= union (rng FSets) by TARSKI:def_3;
take FSets ; ::_thesis: ( A = union (rng FSets) & ( for n being Nat holds FSets . n c= CA . n ) )
now__::_thesis:_for_x_being_set_st_x_in_union_(rng_FSets)_holds_
x_in_A
let x be set ; ::_thesis: ( x in union (rng FSets) implies x in A )
assume x in union (rng FSets) ; ::_thesis: x in A
then consider E being set such that
A15: x in E and
A16: E in rng FSets by TARSKI:def_4;
consider n being set such that
A17: n in NAT and
A18: FSets . n = E by A16, FUNCT_2:11;
reconsider n = n as Element of NAT by A17;
x in ((Partial_Diff_Union CA) . n) /\ A by A1, A15, A18;
hence x in A by XBOOLE_0:def_4; ::_thesis: verum
end;
then union (rng FSets) c= A by TARSKI:def_3;
hence A = union (rng FSets) by A14, XBOOLE_0:def_10; ::_thesis: for n being Nat holds FSets . n c= CA . n
hereby ::_thesis: verum
let n be Nat; ::_thesis: FSets . n c= CA . n
n in NAT by ORDINAL1:def_12;
then FSets . n = ((Partial_Diff_Union CA) . n) /\ A by A1;
then A19: FSets . n c= (Partial_Diff_Union CA) . n by XBOOLE_1:17;
(Partial_Diff_Union CA) . n c= CA . n by PROB_3:17;
hence FSets . n c= CA . n by A19, XBOOLE_1:1; ::_thesis: verum
end;
end;
theorem Th18: :: MEASURE8:18
for X being set
for F being Field_Subset of X
for M being Measure of F st M is completely-additive holds
for A being set st A in F holds
M . A = (C_Meas M) . A
proof
let X be set ; ::_thesis: for F being Field_Subset of X
for M being Measure of F st M is completely-additive holds
for A being set st A in F holds
M . A = (C_Meas M) . A
let F be Field_Subset of X; ::_thesis: for M being Measure of F st M is completely-additive holds
for A being set st A in F holds
M . A = (C_Meas M) . A
let M be Measure of F; ::_thesis: ( M is completely-additive implies for A being set st A in F holds
M . A = (C_Meas M) . A )
assume A1: M is completely-additive ; ::_thesis: for A being set st A in F holds
M . A = (C_Meas M) . A
let A be set ; ::_thesis: ( A in F implies M . A = (C_Meas M) . A )
assume A2: A in F ; ::_thesis: M . A = (C_Meas M) . A
then reconsider A9 = A as Subset of X ;
for x being ext-real number st x in Svc (M,A9) holds
M . A <= x
proof
let x be ext-real number ; ::_thesis: ( x in Svc (M,A9) implies M . A <= x )
assume x in Svc (M,A9) ; ::_thesis: M . A <= x
then consider Aseq being Covering of A9,F such that
A3: x = SUM (vol (M,Aseq)) by Def7;
consider Bseq being Sep_Sequence of F such that
A4: A = union (rng Bseq) and
A5: for n being Nat holds Bseq . n c= Aseq . n by A2, Th17;
for n being Element of NAT holds (M * Bseq) . n <= (vol (M,Aseq)) . n
proof
let n be Element of NAT ; ::_thesis: (M * Bseq) . n <= (vol (M,Aseq)) . n
M . (Bseq . n) <= M . (Aseq . n) by A5, MEASURE1:8;
then (M * Bseq) . n <= M . (Aseq . n) by FUNCT_2:15;
hence (M * Bseq) . n <= (vol (M,Aseq)) . n by Def5; ::_thesis: verum
end;
then SUM (M * Bseq) <= SUM (vol (M,Aseq)) by SUPINF_2:43;
hence M . A <= x by A1, A2, A3, A4, Def11; ::_thesis: verum
end;
then M . A is LowerBound of Svc (M,A9) by XXREAL_2:def_2;
then M . A <= inf (Svc (M,A9)) by XXREAL_2:def_4;
then A6: M . A <= (C_Meas M) . A9 by Def8;
(C_Meas M) . A <= M . A by A2, Th9;
hence M . A = (C_Meas M) . A by A6, XXREAL_0:1; ::_thesis: verum
end;
theorem Th19: :: MEASURE8:19
for X being set
for A being Subset of X
for C being C_Measure of X st ( for B being Subset of X holds (C . (B /\ A)) + (C . (B /\ (X \ A))) <= C . B ) holds
A in sigma_Field C
proof
let X be set ; ::_thesis: for A being Subset of X
for C being C_Measure of X st ( for B being Subset of X holds (C . (B /\ A)) + (C . (B /\ (X \ A))) <= C . B ) holds
A in sigma_Field C
let A be Subset of X; ::_thesis: for C being C_Measure of X st ( for B being Subset of X holds (C . (B /\ A)) + (C . (B /\ (X \ A))) <= C . B ) holds
A in sigma_Field C
let C be C_Measure of X; ::_thesis: ( ( for B being Subset of X holds (C . (B /\ A)) + (C . (B /\ (X \ A))) <= C . B ) implies A in sigma_Field C )
assume A1: for B being Subset of X holds (C . (B /\ A)) + (C . (B /\ (X \ A))) <= C . B ; ::_thesis: A in sigma_Field C
for W, Z being Subset of X st W c= A & Z c= X \ A holds
(C . W) + (C . Z) <= C . (W \/ Z)
proof
let W, Z be Subset of X; ::_thesis: ( W c= A & Z c= X \ A implies (C . W) + (C . Z) <= C . (W \/ Z) )
assume that
A2: W c= A and
A3: Z c= X \ A ; ::_thesis: (C . W) + (C . Z) <= C . (W \/ Z)
set Y = W \/ Z;
A4: Z misses A by A3, XBOOLE_1:106;
A5: (W \/ Z) /\ (X \ A) = ((W \/ Z) /\ X) \ A by XBOOLE_1:49
.= ((X /\ W) \/ (X /\ Z)) \ A by XBOOLE_1:23
.= (W \/ (X /\ Z)) \ A by XBOOLE_1:28
.= (W \/ Z) \ A by XBOOLE_1:28
.= (W \ A) \/ (Z \ A) by XBOOLE_1:42
.= {} \/ (Z \ A) by A2, XBOOLE_1:37
.= {} \/ Z by A4, XBOOLE_1:83 ;
(W \/ Z) /\ A = (A /\ W) \/ (A /\ Z) by XBOOLE_1:23
.= W \/ (A /\ Z) by A2, XBOOLE_1:28
.= W \/ {} by A4, XBOOLE_0:def_7 ;
hence (C . W) + (C . Z) <= C . (W \/ Z) by A1, A5; ::_thesis: verum
end;
hence A in sigma_Field C by MEASURE4:def_2; ::_thesis: verum
end;
theorem Th20: :: MEASURE8:20
for X being set
for F being Field_Subset of X
for M being Measure of F holds F c= sigma_Field (C_Meas M)
proof
let X be set ; ::_thesis: for F being Field_Subset of X
for M being Measure of F holds F c= sigma_Field (C_Meas M)
let F be Field_Subset of X; ::_thesis: for M being Measure of F holds F c= sigma_Field (C_Meas M)
let M be Measure of F; ::_thesis: F c= sigma_Field (C_Meas M)
set C = C_Meas M;
now__::_thesis:_for_E_being_set_st_E_in_F_holds_
E_in_sigma_Field_(C_Meas_M)
let E be set ; ::_thesis: ( E in F implies E in sigma_Field (C_Meas M) )
assume A1: E in F ; ::_thesis: E in sigma_Field (C_Meas M)
then reconsider E9 = E as Subset of X ;
for A being Subset of X holds ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= (C_Meas M) . A
proof
let A be Subset of X; ::_thesis: ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= (C_Meas M) . A
set CA = ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9)));
A2: for seq being Covering of A,F holds ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= SUM (vol (M,seq))
proof
let seq be Covering of A,F; ::_thesis: ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= SUM (vol (M,seq))
deffunc H1( Element of NAT ) -> Element of bool X = (seq . $1) /\ E;
consider Bseq being Function of NAT,(bool X) such that
A3: for n being Element of NAT holds Bseq . n = H1(n) from FUNCT_2:sch_4();
reconsider Bseq = Bseq as SetSequence of X ;
for n being Nat holds Bseq . n in F
proof
let n be Nat; ::_thesis: Bseq . n in F
n in NAT by ORDINAL1:def_12;
then Bseq . n = (seq . n) /\ E by A3;
hence Bseq . n in F by A1, FINSUB_1:def_2; ::_thesis: verum
end;
then reconsider Bseq = Bseq as Set_Sequence of F by Def2;
A4: for x being set st x in A holds
ex n being Element of NAT st x in seq . n
proof
let x be set ; ::_thesis: ( x in A implies ex n being Element of NAT st x in seq . n )
assume A5: x in A ; ::_thesis: ex n being Element of NAT st x in seq . n
A c= union (rng seq) by Def3;
then consider B being set such that
A6: x in B and
A7: B in rng seq by A5, TARSKI:def_4;
ex n being Element of NAT st B = seq . n by A7, FUNCT_2:113;
hence ex n being Element of NAT st x in seq . n by A6; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_A_/\_E9_holds_
x_in_union_(rng_Bseq)
let x be set ; ::_thesis: ( x in A /\ E9 implies x in union (rng Bseq) )
assume A8: x in A /\ E9 ; ::_thesis: x in union (rng Bseq)
then x in A by XBOOLE_0:def_4;
then consider n being Element of NAT such that
A9: x in seq . n by A4;
x in E9 by A8, XBOOLE_0:def_4;
then x in (seq . n) /\ E by A9, XBOOLE_0:def_4;
then A10: x in Bseq . n by A3;
Bseq . n in rng Bseq by FUNCT_2:4;
hence x in union (rng Bseq) by A10, TARSKI:def_4; ::_thesis: verum
end;
then A /\ E9 c= union (rng Bseq) by TARSKI:def_3;
then reconsider Bseq = Bseq as Covering of A /\ E9,F by Def3;
deffunc H2( Element of NAT ) -> Element of bool X = (seq . $1) /\ (X \ E);
consider Cseq being Function of NAT,(bool X) such that
A11: for n being Element of NAT holds Cseq . n = H2(n) from FUNCT_2:sch_4();
reconsider Cseq = Cseq as SetSequence of X ;
for n being Nat holds Cseq . n in F
proof
let n be Nat; ::_thesis: Cseq . n in F
X in F by PROB_1:5;
then A12: X \ E in F by A1, PROB_1:6;
n in NAT by ORDINAL1:def_12;
then Cseq . n = (seq . n) /\ (X \ E) by A11;
hence Cseq . n in F by A12, FINSUB_1:def_2; ::_thesis: verum
end;
then reconsider Cseq = Cseq as Set_Sequence of F by Def2;
now__::_thesis:_for_x_being_set_st_x_in_A_/\_(X_\_E9)_holds_
x_in_union_(rng_Cseq)
let x be set ; ::_thesis: ( x in A /\ (X \ E9) implies x in union (rng Cseq) )
assume A13: x in A /\ (X \ E9) ; ::_thesis: x in union (rng Cseq)
then x in A by XBOOLE_0:def_4;
then consider n being Element of NAT such that
A14: x in seq . n by A4;
x in X \ E9 by A13, XBOOLE_0:def_4;
then x in (seq . n) /\ (X \ E) by A14, XBOOLE_0:def_4;
then A15: x in Cseq . n by A11;
Cseq . n in rng Cseq by FUNCT_2:4;
hence x in union (rng Cseq) by A15, TARSKI:def_4; ::_thesis: verum
end;
then A /\ (X \ E9) c= union (rng Cseq) by TARSKI:def_3;
then reconsider Cseq = Cseq as Covering of A /\ (X \ E9),F by Def3;
A16: for n being Nat holds (vol (M,seq)) . n = ((vol (M,Bseq)) . n) + ((vol (M,Cseq)) . n)
proof
let n be Nat; ::_thesis: (vol (M,seq)) . n = ((vol (M,Bseq)) . n) + ((vol (M,Cseq)) . n)
A17: ( M . (seq . n) = (vol (M,seq)) . n & M . (Bseq . n) = (vol (M,Bseq)) . n ) by Def5;
A18: M . (Cseq . n) = (vol (M,Cseq)) . n by Def5;
n is Element of NAT by ORDINAL1:def_12;
then A19: ( Bseq . n = (seq . n) /\ E & Cseq . n = (seq . n) /\ (X \ E) ) by A3, A11;
then (Bseq . n) \/ (Cseq . n) = (seq . n) /\ (E \/ (X \ E)) by XBOOLE_1:23;
then (Bseq . n) \/ (Cseq . n) = (seq . n) /\ (E \/ X) by XBOOLE_1:39;
then (Bseq . n) \/ (Cseq . n) = (seq . n) /\ X by XBOOLE_1:12;
then A20: (Bseq . n) \/ (Cseq . n) = seq . n by XBOOLE_1:28;
Bseq . n misses Cseq . n by A19, XBOOLE_1:76, XBOOLE_1:79;
hence (vol (M,seq)) . n = ((vol (M,Bseq)) . n) + ((vol (M,Cseq)) . n) by A20, A17, A18, MEASURE1:def_3; ::_thesis: verum
end;
( (C_Meas M) . (A /\ (X \ E9)) = inf (Svc (M,(A /\ (X \ E9)))) & SUM (vol (M,Cseq)) in Svc (M,(A /\ (X \ E9))) ) by Def7, Def8;
then A21: (C_Meas M) . (A /\ (X \ E9)) <= SUM (vol (M,Cseq)) by XXREAL_2:3;
( (C_Meas M) . (A /\ E9) = inf (Svc (M,(A /\ E9))) & SUM (vol (M,Bseq)) in Svc (M,(A /\ E9)) ) by Def7, Def8;
then A22: (C_Meas M) . (A /\ E9) <= SUM (vol (M,Bseq)) by XXREAL_2:3;
( vol (M,Bseq) is nonnegative & vol (M,Cseq) is nonnegative ) by Th4;
then SUM (vol (M,seq)) = (SUM (vol (M,Bseq))) + (SUM (vol (M,Cseq))) by A16, Th3;
hence ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= SUM (vol (M,seq)) by A22, A21, XXREAL_3:36; ::_thesis: verum
end;
for r being ext-real number st r in Svc (M,A) holds
((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= r
proof
let r be ext-real number ; ::_thesis: ( r in Svc (M,A) implies ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= r )
assume r in Svc (M,A) ; ::_thesis: ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= r
then ex G being Covering of A,F st r = SUM (vol (M,G)) by Def7;
hence ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= r by A2; ::_thesis: verum
end;
then ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) is LowerBound of Svc (M,A) by XXREAL_2:def_2;
then ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= inf (Svc (M,A)) by XXREAL_2:def_4;
hence ((C_Meas M) . (A /\ E9)) + ((C_Meas M) . (A /\ (X \ E9))) <= (C_Meas M) . A by Def8; ::_thesis: verum
end;
hence E in sigma_Field (C_Meas M) by Th19; ::_thesis: verum
end;
hence F c= sigma_Field (C_Meas M) by TARSKI:def_3; ::_thesis: verum
end;
theorem Th21: :: MEASURE8:21
for X being set
for F being Field_Subset of X
for FSets being Set_Sequence of F
for M being Function of F,ExtREAL holds M * FSets is ExtREAL_sequence
proof
let X be set ; ::_thesis: for F being Field_Subset of X
for FSets being Set_Sequence of F
for M being Function of F,ExtREAL holds M * FSets is ExtREAL_sequence
let F be Field_Subset of X; ::_thesis: for FSets being Set_Sequence of F
for M being Function of F,ExtREAL holds M * FSets is ExtREAL_sequence
let FSets be Set_Sequence of F; ::_thesis: for M being Function of F,ExtREAL holds M * FSets is ExtREAL_sequence
let M be Function of F,ExtREAL; ::_thesis: M * FSets is ExtREAL_sequence
now__::_thesis:_for_y_being_set_st_y_in_rng_FSets_holds_
y_in_F
let y be set ; ::_thesis: ( y in rng FSets implies y in F )
assume y in rng FSets ; ::_thesis: y in F
then ex x being set st
( x in NAT & FSets . x = y ) by FUNCT_2:11;
hence y in F by Def2; ::_thesis: verum
end;
then rng FSets c= F by TARSKI:def_3;
then rng FSets c= dom M by FUNCT_2:def_1;
then dom (M * FSets) = dom FSets by RELAT_1:27;
then dom (M * FSets) = NAT by FUNCT_2:def_1;
hence M * FSets is ExtREAL_sequence by FUNCT_2:def_1; ::_thesis: verum
end;
definition
let X be set ;
let F be Field_Subset of X;
let FSets be Set_Sequence of F;
let g be Function of F,ExtREAL;
:: original: *
redefine funcg * FSets -> ExtREAL_sequence;
correctness
coherence
FSets * g is ExtREAL_sequence;
by Th21;
end;
theorem Th22: :: MEASURE8:22
for X being set
for S being SigmaField of X
for SSets being SetSequence of S
for M being Function of S,ExtREAL holds M * SSets is ExtREAL_sequence
proof
let X be set ; ::_thesis: for S being SigmaField of X
for SSets being SetSequence of S
for M being Function of S,ExtREAL holds M * SSets is ExtREAL_sequence
let S be SigmaField of X; ::_thesis: for SSets being SetSequence of S
for M being Function of S,ExtREAL holds M * SSets is ExtREAL_sequence
let SSets be SetSequence of S; ::_thesis: for M being Function of S,ExtREAL holds M * SSets is ExtREAL_sequence
let M be Function of S,ExtREAL; ::_thesis: M * SSets is ExtREAL_sequence
rng SSets c= S ;
then rng SSets c= dom M by FUNCT_2:def_1;
then dom (M * SSets) = dom SSets by RELAT_1:27;
then dom (M * SSets) = NAT by FUNCT_2:def_1;
hence M * SSets is ExtREAL_sequence by FUNCT_2:def_1; ::_thesis: verum
end;
definition
let X be set ;
let S be SigmaField of X;
let SSets be SetSequence of S;
let g be Function of S,ExtREAL;
:: original: *
redefine funcg * SSets -> ExtREAL_sequence;
correctness
coherence
SSets * g is ExtREAL_sequence;
by Th22;
end;
theorem Th23: :: MEASURE8:23
for F, G being Function of NAT,ExtREAL
for n being Nat st ( for m being Nat st m <= n holds
F . m <= G . m ) holds
(Ser F) . n <= (Ser G) . n
proof
let F, G be Function of NAT,ExtREAL; ::_thesis: for n being Nat st ( for m being Nat st m <= n holds
F . m <= G . m ) holds
(Ser F) . n <= (Ser G) . n
let n be Nat; ::_thesis: ( ( for m being Nat st m <= n holds
F . m <= G . m ) implies (Ser F) . n <= (Ser G) . n )
assume A1: for m being Nat st m <= n holds
F . m <= G . m ; ::_thesis: (Ser F) . n <= (Ser G) . n
defpred S1[ Nat] means ( ( for m being Nat st m <= $1 holds
F . m <= G . m ) implies (Ser F) . $1 <= (Ser G) . $1 );
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
A3: k is Element of NAT by ORDINAL1:def_12;
assume A4: S1[k] ; ::_thesis: S1[k + 1]
now__::_thesis:_(_(_for_m_being_Nat_st_m_<=_k_+_1_holds_
F_._m_<=_G_._m_)_implies_(Ser_F)_._(k_+_1)_<=_(Ser_G)_._(k_+_1)_)
assume A5: for m being Nat st m <= k + 1 holds
F . m <= G . m ; ::_thesis: (Ser F) . (k + 1) <= (Ser G) . (k + 1)
A6: now__::_thesis:_for_m_being_Nat_st_m_<=_k_holds_
F_._m_<=_G_._m
let m be Nat; ::_thesis: ( m <= k implies F . m <= G . m )
assume m <= k ; ::_thesis: F . m <= G . m
then m < k + 1 by NAT_1:13;
hence F . m <= G . m by A5; ::_thesis: verum
end;
F . (k + 1) <= G . (k + 1) by A5;
then ((Ser F) . k) + (F . (k + 1)) <= ((Ser G) . k) + (G . (k + 1)) by A4, A6, XXREAL_3:36;
then (Ser F) . (k + 1) <= ((Ser G) . k) + (G . (k + 1)) by A3, SUPINF_2:44;
hence (Ser F) . (k + 1) <= (Ser G) . (k + 1) by A3, SUPINF_2:44; ::_thesis: verum
end;
hence S1[k + 1] ; ::_thesis: verum
end;
now__::_thesis:_(_(_for_m_being_Nat_st_m_<=_0_holds_
F_._m_<=_G_._m_)_implies_(Ser_F)_._0_<=_(Ser_G)_._0_)
A7: ( (Ser F) . 0 = F . 0 & (Ser G) . 0 = G . 0 ) by SUPINF_2:44;
assume for m being Nat st m <= 0 holds
F . m <= G . m ; ::_thesis: (Ser F) . 0 <= (Ser G) . 0
hence (Ser F) . 0 <= (Ser G) . 0 by A7; ::_thesis: verum
end;
then A8: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch_2(A8, A2);
hence (Ser F) . n <= (Ser G) . n by A1; ::_thesis: verum
end;
theorem Th24: :: MEASURE8:24
for X being set
for C being C_Measure of X
for seq being Sep_Sequence of (sigma_Field C) holds
( union (rng seq) in sigma_Field C & C . (union (rng seq)) = Sum (C * seq) )
proof
let X be set ; ::_thesis: for C being C_Measure of X
for seq being Sep_Sequence of (sigma_Field C) holds
( union (rng seq) in sigma_Field C & C . (union (rng seq)) = Sum (C * seq) )
let C be C_Measure of X; ::_thesis: for seq being Sep_Sequence of (sigma_Field C) holds
( union (rng seq) in sigma_Field C & C . (union (rng seq)) = Sum (C * seq) )
let seq be Sep_Sequence of (sigma_Field C); ::_thesis: ( union (rng seq) in sigma_Field C & C . (union (rng seq)) = Sum (C * seq) )
A1: rng seq c= sigma_Field C by RELAT_1:def_19;
then reconsider seq1 = seq as Function of NAT,(bool X) by FUNCT_2:6;
A2: for A being Subset of X
for n being Element of NAT holds ((Ser (C * (A (/\) seq1))) . n) + (C . (A /\ (X \ (union (rng seq))))) <= C . A
proof
defpred S1[ Nat] means for A being Subset of X holds C . A >= ((Ser (C * (A (/\) seq1))) . $1) + (C . (A /\ (X \ (union (rng seq)))));
let A be Subset of X; ::_thesis: for n being Element of NAT holds ((Ser (C * (A (/\) seq1))) . n) + (C . (A /\ (X \ (union (rng seq))))) <= C . A
let n be Element of NAT ; ::_thesis: ((Ser (C * (A (/\) seq1))) . n) + (C . (A /\ (X \ (union (rng seq))))) <= C . A
A3: 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 A4: S1[k] ; ::_thesis: S1[k + 1]
A5: now__::_thesis:_for_A_being_Subset_of_X_holds_C_._(A_/\_(X_\_(seq1_._(k_+_1))))_>=_((Ser_(C_*_(A_(/\)_seq1)))_._k)_+_(C_._(A_/\_(X_\_(union_(rng_seq)))))
let A be Subset of X; ::_thesis: C . (A /\ (X \ (seq1 . (k + 1)))) >= ((Ser (C * (A (/\) seq1))) . k) + (C . (A /\ (X \ (union (rng seq)))))
A6: C . (A /\ (X \ (seq1 . (k + 1)))) >= ((Ser (C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1))) . k) + (C . ((A /\ (X \ (seq1 . (k + 1)))) /\ (X \ (union (rng seq))))) by A4;
for m being Nat st m <= k holds
(C * (A (/\) seq1)) . m <= (C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1)) . m
proof
let m be Nat; ::_thesis: ( m <= k implies (C * (A (/\) seq1)) . m <= (C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1)) . m )
reconsider m1 = m as Element of NAT by ORDINAL1:def_12;
assume m <= k ; ::_thesis: (C * (A (/\) seq1)) . m <= (C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1)) . m
then m < k + 1 by NAT_1:13;
then seq1 . m misses seq1 . (k + 1) by PROB_2:def_2;
then A7: (seq1 . m) /\ (X \ (seq1 . (k + 1))) = seq1 . m by XBOOLE_1:28, XBOOLE_1:86;
((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1) . m = (A /\ (X \ (seq1 . (k + 1)))) /\ (seq1 . m1) by SETLIM_2:def_5
.= A /\ ((seq1 . m) /\ (X \ (seq1 . (k + 1)))) by XBOOLE_1:16 ;
then ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1) . m = (A (/\) seq1) . m1 by A7, SETLIM_2:def_5;
then (C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1)) . m1 = C . ((A (/\) seq1) . m1) by FUNCT_2:15;
hence (C * (A (/\) seq1)) . m <= (C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1)) . m by FUNCT_2:15; ::_thesis: verum
end;
then A8: (Ser (C * (A (/\) seq1))) . k <= (Ser (C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1))) . k by Th23;
seq1 . (k + 1) c= union (rng seq) by FUNCT_2:4, ZFMISC_1:74;
then (X \ (seq1 . (k + 1))) /\ (X \ (union (rng seq))) = X \ (union (rng seq)) by XBOOLE_1:28, XBOOLE_1:34;
then (A /\ (X \ (seq1 . (k + 1)))) /\ (X \ (union (rng seq))) = A /\ (X \ (union (rng seq))) by XBOOLE_1:16;
then ((Ser (C * ((A /\ (X \ (seq1 . (k + 1)))) (/\) seq1))) . k) + (C . ((A /\ (X \ (seq1 . (k + 1)))) /\ (X \ (union (rng seq))))) >= ((Ser (C * (A (/\) seq1))) . k) + (C . (A /\ (X \ (union (rng seq))))) by A8, XXREAL_3:36;
hence C . (A /\ (X \ (seq1 . (k + 1)))) >= ((Ser (C * (A (/\) seq1))) . k) + (C . (A /\ (X \ (union (rng seq))))) by A6, XXREAL_0:2; ::_thesis: verum
end;
let A be Subset of X; ::_thesis: C . A >= ((Ser (C * (A (/\) seq1))) . (k + 1)) + (C . (A /\ (X \ (union (rng seq)))))
A /\ (X \ (seq1 . (k + 1))) = (A /\ X) \ (seq1 . (k + 1)) by XBOOLE_1:49
.= A \ (seq1 . (k + 1)) by XBOOLE_1:28 ;
then A9: C . (A \ (seq1 . (k + 1))) >= ((Ser (C * (A (/\) seq1))) . k) + (C . (A /\ (X \ (union (rng seq))))) by A5;
A10: A \ (seq1 . (k + 1)) c= X \ (seq1 . (k + 1)) by XBOOLE_1:33;
A11: A \/ (A \ (seq1 . (k + 1))) = A by XBOOLE_1:12, XBOOLE_1:36;
( seq1 . (k + 1) in rng seq & A /\ (seq1 . (k + 1)) c= seq1 . (k + 1) ) by FUNCT_2:4, XBOOLE_1:17;
then (C . (A /\ (seq1 . (k + 1)))) + (C . (A \ (seq1 . (k + 1)))) = C . ((A /\ (seq1 . (k + 1))) \/ (A \ (seq1 . (k + 1)))) by A1, A10, MEASURE4:5
.= C . ((A \/ (A \ (seq1 . (k + 1)))) /\ ((seq1 . (k + 1)) \/ (A \ (seq1 . (k + 1))))) by XBOOLE_1:24
.= C . ((A \/ (A \ (seq1 . (k + 1)))) /\ ((seq1 . (k + 1)) \/ A)) by XBOOLE_1:39 ;
then (C . (A /\ (seq1 . (k + 1)))) + (C . (A \ (seq1 . (k + 1)))) = C . A by A11, XBOOLE_1:7, XBOOLE_1:28;
then A12: C . A >= (((Ser (C * (A (/\) seq1))) . k) + (C . (A /\ (X \ (union (rng seq)))))) + (C . (A /\ (seq1 . (k + 1)))) by A9, XXREAL_3:36;
A13: ((Ser (C * (A (/\) seq1))) . k) + (C . (A /\ (seq1 . (k + 1)))) = ((Ser (C * (A (/\) seq1))) . k) + (C . ((A (/\) seq1) . (k + 1))) by SETLIM_2:def_5
.= ((Ser (C * (A (/\) seq1))) . k) + ((C * (A (/\) seq1)) . (k + 1)) by FUNCT_2:15
.= (Ser (C * (A (/\) seq1))) . (k + 1) by SUPINF_2:44 ;
A14: C is nonnegative by MEASURE4:def_1;
then A15: C * (A (/\) seq1) is nonnegative by MEASURE1:25;
then (C * (A (/\) seq1)) . k >= 0 by SUPINF_2:51;
then A16: (Ser (C * (A (/\) seq1))) . k > -infty by A15, MEASURE7:2;
( C . (A /\ (X \ (union (rng seq)))) > -infty & C . (A /\ (seq1 . (k + 1))) > -infty ) by A14, SUPINF_2:51;
hence C . A >= ((Ser (C * (A (/\) seq1))) . (k + 1)) + (C . (A /\ (X \ (union (rng seq))))) by A16, A12, A13, XXREAL_3:29; ::_thesis: verum
end;
A17: seq . 0 in sigma_Field C ;
now__::_thesis:_for_A_being_Subset_of_X_holds_C_._A_>=_((Ser_(C_*_(A_(/\)_seq1)))_._0)_+_(C_._(A_/\_(X_\_(union_(rng_seq)))))
let A be Subset of X; ::_thesis: C . A >= ((Ser (C * (A (/\) seq1))) . 0) + (C . (A /\ (X \ (union (rng seq)))))
( A /\ (seq1 . 0) c= seq1 . 0 & A /\ (X \ (seq1 . 0)) c= X \ (seq1 . 0) ) by XBOOLE_1:17;
then A18: (C . (A /\ (seq1 . 0))) + (C . (A /\ (X \ (seq1 . 0)))) = C . ((A /\ (seq1 . 0)) \/ (A /\ (X \ (seq1 . 0)))) by A17, MEASURE4:5
.= C . ((A /\ (seq1 . 0)) \/ ((A /\ X) \ (seq1 . 0))) by XBOOLE_1:49
.= C . ((A /\ (seq1 . 0)) \/ (A \ (seq1 . 0))) by XBOOLE_1:28
.= C . A by XBOOLE_1:51 ;
seq1 . 0 c= Union seq1 by ABCMIZ_1:1;
then seq . 0 c= union (rng seq) by CARD_3:def_4;
then X \ (union (rng seq)) c= X \ (seq . 0) by XBOOLE_1:34;
then A /\ (X \ (union (rng seq))) c= A /\ (X \ (seq . 0)) by XBOOLE_1:26;
then A19: C . (A /\ (X \ (union (rng seq)))) <= C . (A /\ (X \ (seq . 0))) by MEASURE4:def_1;
(Ser (C * (A (/\) seq1))) . 0 = (C * (A (/\) seq1)) . 0 by SUPINF_2:44
.= C . ((A (/\) seq1) . 0) by FUNCT_2:15
.= C . (A /\ (seq1 . 0)) by SETLIM_2:def_5 ;
hence C . A >= ((Ser (C * (A (/\) seq1))) . 0) + (C . (A /\ (X \ (union (rng seq))))) by A18, A19, XXREAL_3:36; ::_thesis: verum
end;
then A20: S1[ 0 ] ;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A20, A3);
hence ((Ser (C * (A (/\) seq1))) . n) + (C . (A /\ (X \ (union (rng seq))))) <= C . A ; ::_thesis: verum
end;
A21: for A being Subset of X holds
( (SUM (C * (A (/\) seq1))) + (C . (A /\ (X \ (union (rng seq))))) <= C . A & C . (A /\ (Union seq1)) <= SUM (C * (A (/\) seq1)) )
proof
let A be Subset of X; ::_thesis: ( (SUM (C * (A (/\) seq1))) + (C . (A /\ (X \ (union (rng seq))))) <= C . A & C . (A /\ (Union seq1)) <= SUM (C * (A (/\) seq1)) )
A22: C is nonnegative by MEASURE4:def_1;
then A23: C * (A (/\) seq1) is nonnegative by MEASURE1:25;
A24: C . (A /\ (X \ (union (rng seq)))) > -infty by A22, SUPINF_2:51;
( ( not C . A = +infty or not C . (A /\ (X \ (union (rng seq)))) = +infty ) implies (SUM (C * (A (/\) seq1))) + (C . (A /\ (X \ (union (rng seq))))) <= C . A )
proof
assume A25: ( not C . A = +infty or not C . (A /\ (X \ (union (rng seq)))) = +infty ) ; ::_thesis: (SUM (C * (A (/\) seq1))) + (C . (A /\ (X \ (union (rng seq))))) <= C . A
for x being ext-real number st x in rng (Ser (C * (A (/\) seq1))) holds
x <= (C . A) - (C . (A /\ (X \ (union (rng seq)))))
proof
let x be ext-real number ; ::_thesis: ( x in rng (Ser (C * (A (/\) seq1))) implies x <= (C . A) - (C . (A /\ (X \ (union (rng seq))))) )
assume x in rng (Ser (C * (A (/\) seq1))) ; ::_thesis: x <= (C . A) - (C . (A /\ (X \ (union (rng seq)))))
then consider i being set such that
A26: i in NAT and
A27: (Ser (C * (A (/\) seq1))) . i = x by FUNCT_2:11;
reconsider i = i as Element of NAT by A26;
(C * (A (/\) seq1)) . i >= 0 by A23, SUPINF_2:51;
then A28: x > -infty by A23, A27, MEASURE7:2;
( C . (A /\ (X \ (union (rng seq)))) > -infty & ((Ser (C * (A (/\) seq1))) . i) + (C . (A /\ (X \ (union (rng seq))))) <= C . A ) by A2, A22, SUPINF_2:51;
hence x <= (C . A) - (C . (A /\ (X \ (union (rng seq))))) by A25, A27, A28, XXREAL_3:56; ::_thesis: verum
end;
then (C . A) - (C . (A /\ (X \ (union (rng seq))))) is UpperBound of rng (Ser (C * (A (/\) seq1))) by XXREAL_2:def_1;
then A29: SUM (C * (A (/\) seq1)) <= (C . A) - (C . (A /\ (X \ (union (rng seq))))) by XXREAL_2:def_3;
SUM (C * (A (/\) seq1)) >= 0 by A23, MEASURE6:2;
hence (SUM (C * (A (/\) seq1))) + (C . (A /\ (X \ (union (rng seq))))) <= C . A by A24, A29, XXREAL_3:55; ::_thesis: verum
end;
hence (SUM (C * (A (/\) seq1))) + (C . (A /\ (X \ (union (rng seq))))) <= C . A by XXREAL_0:3; ::_thesis: C . (A /\ (Union seq1)) <= SUM (C * (A (/\) seq1))
C . (union (rng (A (/\) seq1))) <= SUM (C * (A (/\) seq1)) by MEASURE4:def_1;
then C . (Union (A (/\) seq1)) <= SUM (C * (A (/\) seq1)) by CARD_3:def_4;
hence C . (A /\ (Union seq1)) <= SUM (C * (A (/\) seq1)) by SETLIM_2:38; ::_thesis: verum
end;
then A30: C . ((union (rng seq)) /\ (Union seq1)) <= SUM (C * ((union (rng seq)) (/\) seq1)) ;
for W, Z being Subset of X st W c= Union seq1 & Z c= X \ (Union seq1) holds
(C . W) + (C . Z) <= C . (W \/ Z)
proof
let W, Z be Subset of X; ::_thesis: ( W c= Union seq1 & Z c= X \ (Union seq1) implies (C . W) + (C . Z) <= C . (W \/ Z) )
assume that
A31: W c= Union seq1 and
A32: Z c= X \ (Union seq1) ; ::_thesis: (C . W) + (C . Z) <= C . (W \/ Z)
set A = W \/ Z;
A33: (W \/ Z) /\ (X \ (Union seq1)) = Z \/ (W /\ (X \ (Union seq1))) by A32, XBOOLE_1:30;
X \ (Union seq1) misses Union seq1 by XBOOLE_1:79;
then A34: (X \ (Union seq1)) /\ (Union seq1) = {} by XBOOLE_0:def_7;
W /\ (X \ (Union seq1)) c= (Union seq1) /\ (X \ (Union seq1)) by A31, XBOOLE_1:26;
then W /\ (X \ (Union seq1)) = {} by A34;
then A35: C . Z = C . ((W \/ Z) /\ (X \ (union (rng seq)))) by A33, CARD_3:def_4;
Z /\ (Union seq1) c= (X \ (Union seq1)) /\ (Union seq1) by A32, XBOOLE_1:26;
then A36: Z /\ (Union seq1) = {} by A34;
(W \/ Z) /\ (Union seq1) = W \/ (Z /\ (Union seq1)) by A31, XBOOLE_1:30;
then C . W <= SUM (C * ((W \/ Z) (/\) seq1)) by A21, A36;
then A37: (C . W) + (C . Z) <= (SUM (C * ((W \/ Z) (/\) seq1))) + (C . ((W \/ Z) /\ (X \ (union (rng seq))))) by A35, XXREAL_3:36;
(SUM (C * ((W \/ Z) (/\) seq1))) + (C . ((W \/ Z) /\ (X \ (union (rng seq))))) <= C . (W \/ Z) by A21;
hence (C . W) + (C . Z) <= C . (W \/ Z) by A37, XXREAL_0:2; ::_thesis: verum
end;
then Union seq1 in sigma_Field C by MEASURE4:def_2;
hence union (rng seq) in sigma_Field C by CARD_3:def_4; ::_thesis: C . (union (rng seq)) = Sum (C * seq)
set Sseq = Ser (C * seq1);
union (rng seq) misses X \ (union (rng seq)) by XBOOLE_1:79;
then A38: (union (rng seq)) /\ (X \ (union (rng seq))) = {} by XBOOLE_0:def_7;
C is zeroed by MEASURE4:def_1;
then A39: C . ((union (rng seq)) /\ (X \ (union (rng seq)))) = 0 by A38, VALUED_0:def_19;
for n being set st n in NAT holds
((union (rng seq)) (/\) seq1) . n = seq . n
proof
let n be set ; ::_thesis: ( n in NAT implies ((union (rng seq)) (/\) seq1) . n = seq . n )
assume n in NAT ; ::_thesis: ((union (rng seq)) (/\) seq1) . n = seq . n
then reconsider n1 = n as Element of NAT ;
seq1 . n1 c= union (rng seq) by FUNCT_2:4, ZFMISC_1:74;
then (union (rng seq)) /\ (seq1 . n1) = seq . n by XBOOLE_1:28;
hence ((union (rng seq)) (/\) seq1) . n = seq . n by SETLIM_2:def_5; ::_thesis: verum
end;
then A40: SUM (C * ((union (rng seq)) (/\) seq1)) = sup (Ser (C * seq1)) by FUNCT_2:12;
C is nonnegative by MEASURE4:def_1;
then C * seq1 is nonnegative by MEASURE1:25;
then for m, n being ext-real number st m in dom (Ser (C * seq1)) & n in dom (Ser (C * seq1)) & m <= n holds
(Ser (C * seq1)) . m <= (Ser (C * seq1)) . n by MEASURE7:8;
then Ser (C * seq1) is non-decreasing by VALUED_0:def_15;
then SUM (C * ((union (rng seq)) (/\) seq1)) = lim (Ser (C * seq1)) by A40, RINFSUP2:37;
then A41: SUM (C * ((union (rng seq)) (/\) seq1)) = lim (Partial_Sums (C * seq1)) by Th1;
(SUM (C * ((union (rng seq)) (/\) seq1))) + (C . ((union (rng seq)) /\ (X \ (union (rng seq))))) <= C . (union (rng seq)) by A21;
then ( union (rng seq) = Union seq1 & C . (union (rng seq)) >= Sum (C * seq) ) by A39, A41, CARD_3:def_4, XXREAL_3:4;
hence C . (union (rng seq)) = Sum (C * seq) by A30, A41, XXREAL_0:1; ::_thesis: verum
end;
theorem :: MEASURE8:25
for X being set
for C being C_Measure of X
for seq being SetSequence of sigma_Field C holds Union seq in sigma_Field C
proof
let X be set ; ::_thesis: for C being C_Measure of X
for seq being SetSequence of sigma_Field C holds Union seq in sigma_Field C
let C be C_Measure of X; ::_thesis: for seq being SetSequence of sigma_Field C holds Union seq in sigma_Field C
let seq be SetSequence of sigma_Field C; ::_thesis: Union seq in sigma_Field C
set Aseq = Partial_Diff_Union seq;
rng (Partial_Diff_Union seq) c= sigma_Field C by RELAT_1:def_19;
then reconsider Aseq9 = Partial_Diff_Union seq as Function of NAT,(sigma_Field C) by FUNCT_2:6;
reconsider Aseq9 = Aseq9 as Sep_Sequence of (sigma_Field C) ;
union (rng Aseq9) in sigma_Field C by Th24;
then Union (Partial_Diff_Union seq) in sigma_Field C by CARD_3:def_4;
hence Union seq in sigma_Field C by PROB_3:36; ::_thesis: verum
end;
theorem Th26: :: MEASURE8:26
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for SSets being SetSequence of S st SSets is non-descending holds
lim (M * SSets) = M . (lim SSets)
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for SSets being SetSequence of S st SSets is non-descending holds
lim (M * SSets) = M . (lim SSets)
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for SSets being SetSequence of S st SSets is non-descending holds
lim (M * SSets) = M . (lim SSets)
let M be sigma_Measure of S; ::_thesis: for SSets being SetSequence of S st SSets is non-descending holds
lim (M * SSets) = M . (lim SSets)
let SSets be SetSequence of S; ::_thesis: ( SSets is non-descending implies lim (M * SSets) = M . (lim SSets) )
assume A1: SSets is non-descending ; ::_thesis: lim (M * SSets) = M . (lim SSets)
then A2: Partial_Union SSets = SSets by PROB_4:19;
rng (Partial_Diff_Union SSets) c= S ;
then reconsider Bseq = Partial_Diff_Union SSets as Sep_Sequence of S by FUNCT_2:6;
for n being set st n in NAT holds
(Ser (M * Bseq)) . n = (M * (Partial_Union SSets)) . n
proof
defpred S1[ Nat] means (Ser (M * Bseq)) . $1 = (M * (Partial_Union SSets)) . $1;
let n be set ; ::_thesis: ( n in NAT implies (Ser (M * Bseq)) . n = (M * (Partial_Union SSets)) . n )
A3: 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 A4: S1[k] ; ::_thesis: S1[k + 1]
A5: ( (Partial_Union (Partial_Diff_Union SSets)) . k = (Partial_Union SSets) . k & (Partial_Diff_Union SSets) . (k + 1) = (SSets . (k + 1)) \ ((Partial_Union SSets) . k) ) by PROB_3:35, PROB_3:def_3;
(Ser (M * Bseq)) . (k + 1) = ((Ser (M * Bseq)) . k) + ((M * Bseq) . (k + 1)) by SUPINF_2:44
.= ((M * (Partial_Union SSets)) . k) + (M . ((Partial_Diff_Union SSets) . (k + 1))) by A4, FUNCT_2:15
.= (M . ((Partial_Union SSets) . k)) + (M . ((Partial_Diff_Union SSets) . (k + 1))) by FUNCT_2:15
.= (M . ((Partial_Union (Partial_Diff_Union SSets)) . k)) + (M . ((Partial_Diff_Union SSets) . (k + 1))) by PROB_3:35 ;
then (Ser (M * Bseq)) . (k + 1) = M . (((Partial_Union (Partial_Diff_Union SSets)) . k) \/ ((Partial_Diff_Union SSets) . (k + 1))) by A5, MEASURE1:30, XBOOLE_1:79
.= M . ((Partial_Union (Partial_Diff_Union SSets)) . (k + 1)) by PROB_3:def_2
.= M . ((Partial_Union SSets) . (k + 1)) by PROB_3:35 ;
hence (Ser (M * Bseq)) . (k + 1) = (M * (Partial_Union SSets)) . (k + 1) by FUNCT_2:15; ::_thesis: verum
end;
assume n in NAT ; ::_thesis: (Ser (M * Bseq)) . n = (M * (Partial_Union SSets)) . n
then reconsider n1 = n as Element of NAT ;
(Ser (M * Bseq)) . 0 = (M * Bseq) . 0 by SUPINF_2:44
.= M . ((Partial_Diff_Union SSets) . 0) by FUNCT_2:15
.= M . (SSets . 0) by PROB_3:31
.= M . ((Partial_Union SSets) . 0) by PROB_3:22 ;
then A6: S1[ 0 ] by FUNCT_2:15;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A6, A3);
then (Ser (M * Bseq)) . n1 = (M * (Partial_Union SSets)) . n1 ;
hence (Ser (M * Bseq)) . n = (M * (Partial_Union SSets)) . n ; ::_thesis: verum
end;
then A7: Ser (M * Bseq) = M * SSets by A2, FUNCT_2:12;
reconsider Gseq = Ser (M * Bseq) as ExtREAL_sequence ;
M * Bseq is nonnegative by MEASURE1:25;
then for m, n being ext-real number st m in dom Gseq & n in dom Gseq & m <= n holds
Gseq . m <= Gseq . n by MEASURE7:8;
then Gseq is non-decreasing by VALUED_0:def_15;
then A8: ( SUM (M * Bseq) = M . (union (rng Bseq)) & lim Gseq = sup Gseq ) by MEASURE1:def_6, RINFSUP2:37;
Partial_Union (Partial_Diff_Union SSets) = SSets by A2, PROB_3:35;
then Union SSets = Union (Partial_Diff_Union SSets) by PROB_3:30;
then lim Gseq = M . (Union SSets) by A8, CARD_3:def_4;
hence lim (M * SSets) = M . (lim SSets) by A1, A7, SETLIM_1:63; ::_thesis: verum
end;
theorem :: MEASURE8:27
for X being set
for F being Field_Subset of X
for M being Measure of F
for FSets being Set_Sequence of F st FSets is non-descending holds
M * FSets is non-decreasing
proof
let X be set ; ::_thesis: for F being Field_Subset of X
for M being Measure of F
for FSets being Set_Sequence of F st FSets is non-descending holds
M * FSets is non-decreasing
let F be Field_Subset of X; ::_thesis: for M being Measure of F
for FSets being Set_Sequence of F st FSets is non-descending holds
M * FSets is non-decreasing
let M be Measure of F; ::_thesis: for FSets being Set_Sequence of F st FSets is non-descending holds
M * FSets is non-decreasing
let FSets be Set_Sequence of F; ::_thesis: ( FSets is non-descending implies M * FSets is non-decreasing )
A1: dom (M * FSets) = NAT by FUNCT_2:def_1;
assume A2: FSets is non-descending ; ::_thesis: M * FSets is non-decreasing
now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<=_m_holds_
(M_*_FSets)_._n_<=_(M_*_FSets)_._m
let n, m be Element of NAT ; ::_thesis: ( n <= m implies (M * FSets) . n <= (M * FSets) . m )
assume n <= m ; ::_thesis: (M * FSets) . n <= (M * FSets) . m
then A3: FSets . n c= FSets . m by A2, PROB_1:def_5;
( (M * FSets) . n = M . (FSets . n) & (M * FSets) . m = M . (FSets . m) ) by A1, FUNCT_1:12;
hence (M * FSets) . n <= (M * FSets) . m by A3, MEASURE1:8; ::_thesis: verum
end;
then for n, m being Element of NAT st m <= n holds
(M * FSets) . m <= (M * FSets) . n ;
hence M * FSets is non-decreasing by RINFSUP2:7; ::_thesis: verum
end;
theorem :: MEASURE8:28
for X being set
for F being Field_Subset of X
for M being Measure of F
for FSets being Set_Sequence of F st FSets is non-ascending holds
M * FSets is non-increasing
proof
let X be set ; ::_thesis: for F being Field_Subset of X
for M being Measure of F
for FSets being Set_Sequence of F st FSets is non-ascending holds
M * FSets is non-increasing
let F be Field_Subset of X; ::_thesis: for M being Measure of F
for FSets being Set_Sequence of F st FSets is non-ascending holds
M * FSets is non-increasing
let M be Measure of F; ::_thesis: for FSets being Set_Sequence of F st FSets is non-ascending holds
M * FSets is non-increasing
let FSets be Set_Sequence of F; ::_thesis: ( FSets is non-ascending implies M * FSets is non-increasing )
A1: dom (M * FSets) = NAT by FUNCT_2:def_1;
assume A2: FSets is non-ascending ; ::_thesis: M * FSets is non-increasing
now__::_thesis:_for_n,_m_being_Element_of_NAT_st_m_<=_n_holds_
(M_*_FSets)_._n_<=_(M_*_FSets)_._m
let n, m be Element of NAT ; ::_thesis: ( m <= n implies (M * FSets) . n <= (M * FSets) . m )
assume m <= n ; ::_thesis: (M * FSets) . n <= (M * FSets) . m
then A3: FSets . n c= FSets . m by A2, PROB_1:def_4;
( (M * FSets) . n = M . (FSets . n) & (M * FSets) . m = M . (FSets . m) ) by A1, FUNCT_1:12;
hence (M * FSets) . n <= (M * FSets) . m by A3, MEASURE1:8; ::_thesis: verum
end;
hence M * FSets is non-increasing by RINFSUP2:7; ::_thesis: verum
end;
theorem Th29: :: MEASURE8:29
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for SSets being SetSequence of S st SSets is non-descending holds
M * SSets is non-decreasing
proof
let X be set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for SSets being SetSequence of S st SSets is non-descending holds
M * SSets is non-decreasing
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for SSets being SetSequence of S st SSets is non-descending holds
M * SSets is non-decreasing
let M be sigma_Measure of S; ::_thesis: for SSets being SetSequence of S st SSets is non-descending holds
M * SSets is non-decreasing
let SSets be SetSequence of S; ::_thesis: ( SSets is non-descending implies M * SSets is non-decreasing )
A1: dom (M * SSets) = NAT by FUNCT_2:def_1;
assume A2: SSets is non-descending ; ::_thesis: M * SSets is non-decreasing
now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<=_m_holds_
(M_*_SSets)_._n_<=_(M_*_SSets)_._m
let n, m be Element of NAT ; ::_thesis: ( n <= m implies (M * SSets) . n <= (M * SSets) . m )
A3: (M * SSets) . m = M . (SSets . m) by A1, FUNCT_1:12;
assume n <= m ; ::_thesis: (M * SSets) . n <= (M * SSets) . m
then A4: SSets . n c= SSets . m by A2, PROB_1:def_5;
( rng SSets c= S & (M * SSets) . n = M . (SSets . n) ) by A1, FUNCT_1:12;
hence (M * SSets) . n <= (M * SSets) . m by A4, A3, MEASURE1:31; ::_thesis: verum
end;
then for n, m being Element of NAT st m <= n holds
(M * SSets) . m <= (M * SSets) . n ;
hence M * SSets is non-decreasing by RINFSUP2:7; ::_thesis: verum
end;
theorem Th30: :: MEASURE8:30
for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for SSets being SetSequence of S st SSets is non-ascending holds
M * SSets is non-increasing
proof
let X be set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for SSets being SetSequence of S st SSets is non-ascending holds
M * SSets is non-increasing
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for SSets being SetSequence of S st SSets is non-ascending holds
M * SSets is non-increasing
let M be sigma_Measure of S; ::_thesis: for SSets being SetSequence of S st SSets is non-ascending holds
M * SSets is non-increasing
let SSets be SetSequence of S; ::_thesis: ( SSets is non-ascending implies M * SSets is non-increasing )
A1: dom (M * SSets) = NAT by FUNCT_2:def_1;
assume A2: SSets is non-ascending ; ::_thesis: M * SSets is non-increasing
now__::_thesis:_for_n,_m_being_Element_of_NAT_st_m_<=_n_holds_
(M_*_SSets)_._n_<=_(M_*_SSets)_._m
let n, m be Element of NAT ; ::_thesis: ( m <= n implies (M * SSets) . n <= (M * SSets) . m )
A3: (M * SSets) . m = M . (SSets . m) by A1, FUNCT_1:12;
assume m <= n ; ::_thesis: (M * SSets) . n <= (M * SSets) . m
then A4: SSets . n c= SSets . m by A2, PROB_1:def_4;
( rng SSets c= S & (M * SSets) . n = M . (SSets . n) ) by A1, FUNCT_1:12;
hence (M * SSets) . n <= (M * SSets) . m by A4, A3, MEASURE1:31; ::_thesis: verum
end;
hence M * SSets is non-increasing by RINFSUP2:7; ::_thesis: verum
end;
theorem :: MEASURE8:31
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for SSets being SetSequence of S st SSets is non-ascending & M . (SSets . 0) < +infty holds
lim (M * SSets) = M . (lim SSets)
proof
let X be non empty set ; ::_thesis: for S being SigmaField of X
for M being sigma_Measure of S
for SSets being SetSequence of S st SSets is non-ascending & M . (SSets . 0) < +infty holds
lim (M * SSets) = M . (lim SSets)
let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S
for SSets being SetSequence of S st SSets is non-ascending & M . (SSets . 0) < +infty holds
lim (M * SSets) = M . (lim SSets)
let M be sigma_Measure of S; ::_thesis: for SSets being SetSequence of S st SSets is non-ascending & M . (SSets . 0) < +infty holds
lim (M * SSets) = M . (lim SSets)
let SSets be SetSequence of S; ::_thesis: ( SSets is non-ascending & M . (SSets . 0) < +infty implies lim (M * SSets) = M . (lim SSets) )
assume that
A1: SSets is non-ascending and
A2: M . (SSets . 0) < +infty ; ::_thesis: lim (M * SSets) = M . (lim SSets)
A3: M . ((SSets . 0) \ (lim SSets)) >= 0 by SUPINF_2:51;
now__::_thesis:_for_y_being_set_st_y_in_rng_((SSets_._0)_(\)_SSets)_holds_
y_in_S
let y be set ; ::_thesis: ( y in rng ((SSets . 0) (\) SSets) implies y in S )
assume y in rng ((SSets . 0) (\) SSets) ; ::_thesis: y in S
then consider x being set such that
A4: x in NAT and
A5: ((SSets . 0) (\) SSets) . x = y by FUNCT_2:11;
reconsider x = x as Element of NAT by A4;
(SSets . 0) \ (SSets . x) in S ;
hence y in S by A5, SETLIM_2:def_7; ::_thesis: verum
end;
then rng ((SSets . 0) (\) SSets) c= S by TARSKI:def_3;
then reconsider Bseq = (SSets . 0) (\) SSets as SetSequence of S by RELAT_1:def_19;
deffunc H1( Element of NAT ) -> Element of ExtREAL = (M * SSets) . 0;
consider seq1 being Function of NAT,ExtREAL such that
A6: for n being Element of NAT holds seq1 . n = H1(n) from FUNCT_2:sch_4();
A7: now__::_thesis:_for_k_being_Nat_holds_seq1_._k_=_((M_*_SSets)_._k)_+_((M_*_Bseq)_._k)
let k be Nat; ::_thesis: seq1 . k = ((M * SSets) . k) + ((M * Bseq) . k)
reconsider k1 = k as Element of NAT by ORDINAL1:def_12;
A8: ( SSets . k1 in S & Bseq . k1 in S ) ;
A9: k is Element of NAT by ORDINAL1:def_12;
then ( (SSets . k) \/ ((SSets . 0) \ (SSets . k)) = (SSets . 0) \/ (SSets . k) & SSets . k c= SSets . 0 ) by A1, PROB_1:def_4, XBOOLE_1:39;
then (SSets . k) \/ ((SSets . 0) \ (SSets . k)) = SSets . 0 by XBOOLE_1:12;
then A10: (SSets . k) \/ (Bseq . k) = SSets . 0 by A9, SETLIM_2:def_7;
SSets . k misses (SSets . 0) \ (SSets . k) by XBOOLE_1:79;
then SSets . k misses Bseq . k by A9, SETLIM_2:def_7;
then M . (SSets . 0) = (M . (SSets . k)) + (M . (Bseq . k)) by A10, A8, MEASURE1:30;
then (M * SSets) . 0 = (M . (SSets . k)) + (M . (Bseq . k)) by FUNCT_2:15;
then seq1 . k = (M . (SSets . k)) + (M . (Bseq . k)) by A6, A9;
then seq1 . k = ((M * SSets) . k) + (M . (Bseq . k)) by A9, FUNCT_2:15;
hence seq1 . k = ((M * SSets) . k) + ((M * Bseq) . k) by A9, FUNCT_2:15; ::_thesis: verum
end;
M * SSets is non-increasing by A1, Th30;
then A11: M * SSets is convergent by RINFSUP2:36;
rng Bseq c= S ;
then Bseq is Function of NAT,S by FUNCT_2:6;
then A12: M * Bseq is nonnegative by MEASURE2:1;
A13: for n being Nat holds seq1 . n = (M * SSets) . 0
proof
let n be Nat; ::_thesis: seq1 . n = (M * SSets) . 0
n is Element of NAT by ORDINAL1:def_12;
hence seq1 . n = (M * SSets) . 0 by A6; ::_thesis: verum
end;
A14: rng SSets c= S ;
then SSets is Function of NAT,S by FUNCT_2:6;
then A15: M * SSets is nonnegative by MEASURE2:1;
then A16: -infty < (M * SSets) . 0 by SUPINF_2:51;
(inferior_setsequence SSets) . (0 + 1) c= SSets . 0 by A1, SETLIM_1:50;
then Intersection SSets c= SSets . 0 by A1, SETLIM_1:52;
then lim SSets c= SSets . 0 by A1, SETLIM_1:61;
then A17: (SSets . 0) \/ (lim SSets) = SSets . 0 by XBOOLE_1:12;
Intersection SSets in S by A14, PROB_1:def_6;
then A18: lim SSets in S by A1, SETLIM_1:61;
then A19: (SSets . 0) \ (lim SSets) is Element of S by PROB_1:6;
then M . (((SSets . 0) \ (lim SSets)) \/ (lim SSets)) = (M . ((SSets . 0) \ (lim SSets))) + (M . (lim SSets)) by A18, MEASURE1:30, XBOOLE_1:79;
then A20: M . ((SSets . 0) \/ (lim SSets)) = (M . ((SSets . 0) \ (lim SSets))) + (M . (lim SSets)) by XBOOLE_1:39;
(M * SSets) . 0 < +infty by A2, FUNCT_2:15;
then A21: (M * SSets) . 0 in REAL by A16, XXREAL_0:14;
for n, m being Element of NAT st n <= m holds
Bseq . n c= Bseq . m
proof
let n, m be Element of NAT ; ::_thesis: ( n <= m implies Bseq . n c= Bseq . m )
assume n <= m ; ::_thesis: Bseq . n c= Bseq . m
then SSets . m c= SSets . n by A1, PROB_1:def_4;
then (SSets . 0) \ (SSets . n) c= (SSets . 0) \ (SSets . m) by XBOOLE_1:34;
then Bseq . n c= (SSets . 0) \ (SSets . m) by SETLIM_2:def_7;
hence Bseq . n c= Bseq . m by SETLIM_2:def_7; ::_thesis: verum
end;
then A22: Bseq is non-descending by PROB_1:def_5;
then M * Bseq is non-decreasing by Th29;
then M * Bseq is convergent by RINFSUP2:37;
then lim seq1 = (lim (M * Bseq)) + (lim (M * SSets)) by A11, A12, A15, A7, MESFUNC9:11;
then A23: (M * SSets) . 0 = (lim (M * Bseq)) + (lim (M * SSets)) by A21, A13, MESFUNC5:52;
lim (M * Bseq) = M . (lim Bseq) by A22, Th26
.= M . ((SSets . 0) \ (lim SSets)) by A1, SETLIM_1:64, SETLIM_2:86 ;
then A24: (M . ((SSets . 0) \ (lim SSets))) + (M . (lim SSets)) = (lim (M * SSets)) + (M . ((SSets . 0) \ (lim SSets))) by A20, A17, A23, FUNCT_2:15;
A25: M . ((SSets . 0) \ (lim SSets)) <= M . (SSets . 0) by A19, MEASURE1:31, XBOOLE_1:36;
then M . ((SSets . 0) \ (lim SSets)) < +infty by A2, XXREAL_0:2;
then A26: M . (lim SSets) = ((lim (M * SSets)) + (M . ((SSets . 0) \ (lim SSets)))) - (M . ((SSets . 0) \ (lim SSets))) by A3, A24, XXREAL_3:28;
M . ((SSets . 0) \ (lim SSets)) is Real by A2, A25, A3, XXREAL_0:14;
hence M . (lim SSets) = lim (M * SSets) by A26, XXREAL_3:22; ::_thesis: verum
end;
definition
let X be set ;
let F be Field_Subset of X;
let S be SigmaField of X;
let m be Measure of F;
let M be sigma_Measure of S;
predM is_extension_of m means :Def12: :: MEASURE8:def 12
for A being set st A in F holds
M . A = m . A;
end;
:: deftheorem Def12 defines is_extension_of MEASURE8:def_12_:_
for X being set
for F being Field_Subset of X
for S being SigmaField of X
for m being Measure of F
for M being sigma_Measure of S holds
( M is_extension_of m iff for A being set st A in F holds
M . A = m . A );
theorem :: MEASURE8:32
for X being non empty set
for F being Field_Subset of X
for m being Measure of F st ex M being sigma_Measure of (sigma F) st M is_extension_of m holds
m is completely-additive
proof
let X be non empty set ; ::_thesis: for F being Field_Subset of X
for m being Measure of F st ex M being sigma_Measure of (sigma F) st M is_extension_of m holds
m is completely-additive
let F be Field_Subset of X; ::_thesis: for m being Measure of F st ex M being sigma_Measure of (sigma F) st M is_extension_of m holds
m is completely-additive
let m be Measure of F; ::_thesis: ( ex M being sigma_Measure of (sigma F) st M is_extension_of m implies m is completely-additive )
given M being sigma_Measure of (sigma F) such that A1: M is_extension_of m ; ::_thesis: m is completely-additive
A2: F c= sigma F by PROB_1:def_9;
for Aseq being Sep_Sequence of F st union (rng Aseq) in F holds
SUM (m * Aseq) = m . (union (rng Aseq))
proof
let Aseq be Sep_Sequence of F; ::_thesis: ( union (rng Aseq) in F implies SUM (m * Aseq) = m . (union (rng Aseq)) )
reconsider Bseq = Aseq as Function of NAT,(sigma F) by A2, FUNCT_2:7;
reconsider Bseq = Bseq as Sep_Sequence of (sigma F) ;
A3: now__::_thesis:_for_n_being_set_st_n_in_NAT_holds_
(M_*_Bseq)_._n_=_(m_*_Aseq)_._n
let n be set ; ::_thesis: ( n in NAT implies (M * Bseq) . n = (m * Aseq) . n )
assume n in NAT ; ::_thesis: (M * Bseq) . n = (m * Aseq) . n
then reconsider n9 = n as Element of NAT ;
(M * Bseq) . n = M . (Bseq . n9) by FUNCT_2:15;
then (M * Bseq) . n = m . (Aseq . n9) by A1, Def12;
hence (M * Bseq) . n = (m * Aseq) . n by FUNCT_2:15; ::_thesis: verum
end;
assume union (rng Aseq) in F ; ::_thesis: SUM (m * Aseq) = m . (union (rng Aseq))
then m . (union (rng Aseq)) = M . (union (rng Aseq)) by A1, Def12;
then m . (union (rng Aseq)) = SUM (M * Bseq) by MEASURE1:def_6;
hence SUM (m * Aseq) = m . (union (rng Aseq)) by A3, FUNCT_2:12; ::_thesis: verum
end;
hence m is completely-additive by Def11; ::_thesis: verum
end;
theorem Th33: :: MEASURE8:33
for X being non empty set
for F being Field_Subset of X
for m being Measure of F st m is completely-additive holds
ex M being sigma_Measure of (sigma F) st
( M is_extension_of m & M = (sigma_Meas (C_Meas m)) | (sigma F) )
proof
let X be non empty set ; ::_thesis: for F being Field_Subset of X
for m being Measure of F st m is completely-additive holds
ex M being sigma_Measure of (sigma F) st
( M is_extension_of m & M = (sigma_Meas (C_Meas m)) | (sigma F) )
let F be Field_Subset of X; ::_thesis: for m being Measure of F st m is completely-additive holds
ex M being sigma_Measure of (sigma F) st
( M is_extension_of m & M = (sigma_Meas (C_Meas m)) | (sigma F) )
let m be Measure of F; ::_thesis: ( m is completely-additive implies ex M being sigma_Measure of (sigma F) st
( M is_extension_of m & M = (sigma_Meas (C_Meas m)) | (sigma F) ) )
assume A1: m is completely-additive ; ::_thesis: ex M being sigma_Measure of (sigma F) st
( M is_extension_of m & M = (sigma_Meas (C_Meas m)) | (sigma F) )
set M = (sigma_Meas (C_Meas m)) | (sigma F);
A2: F c= sigma_Field (C_Meas m) by Th20;
then A3: sigma F c= sigma_Field (C_Meas m) by PROB_1:def_9;
then reconsider M = (sigma_Meas (C_Meas m)) | (sigma F) as Function of (sigma F),ExtREAL by FUNCT_2:32;
A4: for SS being Sep_Sequence of (sigma F) holds SUM (M * SS) = M . (union (rng SS))
proof
let SS be Sep_Sequence of (sigma F); ::_thesis: SUM (M * SS) = M . (union (rng SS))
reconsider SS9 = SS as Sep_Sequence of (sigma_Field (C_Meas m)) by A3, FUNCT_2:7;
A5: rng SS c= sigma F by RELAT_1:def_19;
M * SS = (sigma_Meas (C_Meas m)) * ((sigma F) |` SS) by MONOID_1:1
.= (sigma_Meas (C_Meas m)) * SS9 by A5, RELAT_1:94 ;
then A6: SUM (M * SS) = (sigma_Meas (C_Meas m)) . (union (rng SS9)) by MEASURE1:def_6;
union (rng SS) is Element of sigma F by MEASURE1:24;
hence SUM (M * SS) = M . (union (rng SS)) by A6, FUNCT_1:49; ::_thesis: verum
end;
M . {} = (sigma_Meas (C_Meas m)) . {} by FUNCT_1:49, PROB_1:4
.= 0 by VALUED_0:def_19 ;
then reconsider M = M as sigma_Measure of (sigma F) by A4, MEASURE1:def_6, MESFUNC5:15, VALUED_0:def_19;
take M ; ::_thesis: ( M is_extension_of m & M = (sigma_Meas (C_Meas m)) | (sigma F) )
A7: F c= sigma F by PROB_1:def_9;
for A being set st A in F holds
M . A = m . A
proof
let A be set ; ::_thesis: ( A in F implies M . A = m . A )
assume A8: A in F ; ::_thesis: M . A = m . A
then reconsider A9 = A as Subset of X ;
M . A = (sigma_Meas (C_Meas m)) . A by A7, A8, FUNCT_1:49
.= (C_Meas m) . A9 by A2, A8, MEASURE4:def_3 ;
hence M . A = m . A by A1, A8, Th18; ::_thesis: verum
end;
hence ( M is_extension_of m & M = (sigma_Meas (C_Meas m)) | (sigma F) ) by Def12; ::_thesis: verum
end;
theorem Th34: :: MEASURE8:34
for X being set
for F being Field_Subset of X
for M being Measure of F
for k being Nat
for FSets being Set_Sequence of F st ( for n being Nat holds M . (FSets . n) < +infty ) holds
M . ((Partial_Union FSets) . k) < +infty
proof
let X be set ; ::_thesis: for F being Field_Subset of X
for M being Measure of F
for k being Nat
for FSets being Set_Sequence of F st ( for n being Nat holds M . (FSets . n) < +infty ) holds
M . ((Partial_Union FSets) . k) < +infty
let F be Field_Subset of X; ::_thesis: for M being Measure of F
for k being Nat
for FSets being Set_Sequence of F st ( for n being Nat holds M . (FSets . n) < +infty ) holds
M . ((Partial_Union FSets) . k) < +infty
let M be Measure of F; ::_thesis: for k being Nat
for FSets being Set_Sequence of F st ( for n being Nat holds M . (FSets . n) < +infty ) holds
M . ((Partial_Union FSets) . k) < +infty
let k be Nat; ::_thesis: for FSets being Set_Sequence of F st ( for n being Nat holds M . (FSets . n) < +infty ) holds
M . ((Partial_Union FSets) . k) < +infty
let FSets be Set_Sequence of F; ::_thesis: ( ( for n being Nat holds M . (FSets . n) < +infty ) implies M . ((Partial_Union FSets) . k) < +infty )
defpred S1[ Nat] means M . ((Partial_Union FSets) . $1) < +infty ;
assume A1: for n being Nat holds M . (FSets . n) < +infty ; ::_thesis: M . ((Partial_Union FSets) . k) < +infty
A2: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_
S1[k_+_1]
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
A3: 0 <= M . ((Partial_Union FSets) . k) by SUPINF_2:51;
( M . (FSets . (k + 1)) < +infty & 0 <= M . (FSets . (k + 1)) ) by A1, SUPINF_2:51;
then A4: M . (FSets . (k + 1)) in REAL by XXREAL_0:10;
assume S1[k] ; ::_thesis: S1[k + 1]
then M . ((Partial_Union FSets) . k) in REAL by A3, XXREAL_0:10;
then A5: (M . ((Partial_Union FSets) . k)) + (M . (FSets . (k + 1))) in REAL by A4, XREAL_0:def_1;
Partial_Union FSets is Set_Sequence of F by Th15;
then A6: (Partial_Union FSets) . k in F by Def2;
(Partial_Union FSets) . (k + 1) = ((Partial_Union FSets) . k) \/ (FSets . (k + 1)) by PROB_3:def_2;
then M . ((Partial_Union FSets) . (k + 1)) <= (M . ((Partial_Union FSets) . k)) + (M . (FSets . (k + 1))) by A6, MEASURE1:10;
hence S1[k + 1] by A5, XXREAL_0:9, XXREAL_0:13; ::_thesis: verum
end;
(Partial_Union FSets) . 0 = FSets . 0 by PROB_3:def_2;
then A7: S1[ 0 ] by A1;
for k being Nat holds S1[k] from NAT_1:sch_2(A7, A2);
hence M . ((Partial_Union FSets) . k) < +infty ; ::_thesis: verum
end;
theorem :: MEASURE8:35
for X being non empty set
for F being Field_Subset of X
for m being Measure of F st m is completely-additive & ex Aseq being Set_Sequence of F st
( ( for n being Nat holds m . (Aseq . n) < +infty ) & X = union (rng Aseq) ) holds
for M being sigma_Measure of (sigma F) st M is_extension_of m holds
M = (sigma_Meas (C_Meas m)) | (sigma F)
proof
let X be non empty set ; ::_thesis: for F being Field_Subset of X
for m being Measure of F st m is completely-additive & ex Aseq being Set_Sequence of F st
( ( for n being Nat holds m . (Aseq . n) < +infty ) & X = union (rng Aseq) ) holds
for M being sigma_Measure of (sigma F) st M is_extension_of m holds
M = (sigma_Meas (C_Meas m)) | (sigma F)
let F be Field_Subset of X; ::_thesis: for m being Measure of F st m is completely-additive & ex Aseq being Set_Sequence of F st
( ( for n being Nat holds m . (Aseq . n) < +infty ) & X = union (rng Aseq) ) holds
for M being sigma_Measure of (sigma F) st M is_extension_of m holds
M = (sigma_Meas (C_Meas m)) | (sigma F)
let m be Measure of F; ::_thesis: ( m is completely-additive & ex Aseq being Set_Sequence of F st
( ( for n being Nat holds m . (Aseq . n) < +infty ) & X = union (rng Aseq) ) implies for M being sigma_Measure of (sigma F) st M is_extension_of m holds
M = (sigma_Meas (C_Meas m)) | (sigma F) )
A1: F c= sigma F by PROB_1:def_9;
assume m is completely-additive ; ::_thesis: ( for Aseq being Set_Sequence of F holds
( ex n being Nat st not m . (Aseq . n) < +infty or not X = union (rng Aseq) ) or for M being sigma_Measure of (sigma F) st M is_extension_of m holds
M = (sigma_Meas (C_Meas m)) | (sigma F) )
then consider M1 being sigma_Measure of (sigma F) such that
A2: M1 is_extension_of m and
A3: M1 = (sigma_Meas (C_Meas m)) | (sigma F) by Th33;
assume ex Aseq being Set_Sequence of F st
( ( for n being Nat holds m . (Aseq . n) < +infty ) & X = union (rng Aseq) ) ; ::_thesis: for M being sigma_Measure of (sigma F) st M is_extension_of m holds
M = (sigma_Meas (C_Meas m)) | (sigma F)
then consider Aseq being Set_Sequence of F such that
A4: for n being Nat holds m . (Aseq . n) < +infty and
A5: X = union (rng Aseq) ;
let M be sigma_Measure of (sigma F); ::_thesis: ( M is_extension_of m implies M = (sigma_Meas (C_Meas m)) | (sigma F) )
reconsider Bseq = Partial_Union Aseq as Set_Sequence of F by Th15;
assume A6: M is_extension_of m ; ::_thesis: M = (sigma_Meas (C_Meas m)) | (sigma F)
F c= sigma_Field (C_Meas m) by Th20;
then A7: sigma F c= sigma_Field (C_Meas m) by PROB_1:def_9;
A8: for B being Subset of X st B in sigma F holds
M . B <= M1 . B
proof
let B be Subset of X; ::_thesis: ( B in sigma F implies M . B <= M1 . B )
assume A9: B in sigma F ; ::_thesis: M . B <= M1 . B
A10: for seq being Covering of B,F holds M . B <= SUM (vol (m,seq))
proof
let seq be Covering of B,F; ::_thesis: M . B <= SUM (vol (m,seq))
A11: now__::_thesis:_for_n_being_Element_of_NAT_holds_seq_._n_in_sigma_F
let n be Element of NAT ; ::_thesis: seq . n in sigma F
seq . n in F ;
hence seq . n in sigma F by A1; ::_thesis: verum
end;
now__::_thesis:_for_y_being_set_st_y_in_rng_seq_holds_
y_in_sigma_F
let y be set ; ::_thesis: ( y in rng seq implies y in sigma F )
assume y in rng seq ; ::_thesis: y in sigma F
then consider x being set such that
A12: x in NAT and
A13: seq . x = y by FUNCT_2:11;
thus y in sigma F by A11, A12, A13; ::_thesis: verum
end;
then rng seq c= sigma F by TARSKI:def_3;
then reconsider seq1 = seq as SetSequence of sigma F by RELAT_1:def_19;
A16: rng seq1 c= sigma F ;
then reconsider Fseq = seq1 as Function of NAT,(sigma F) by FUNCT_2:6;
B c= union (rng seq1) by Def3;
then ( Union seq1 in sigma F & B c= Union seq1 ) by CARD_3:def_4, PROB_1:17;
then A17: M . B <= M . (Union seq1) by A9, MEASURE1:31;
for n being set st n in NAT holds
(M * Fseq) . n = (vol (m,seq)) . n
proof
let n be set ; ::_thesis: ( n in NAT implies (M * Fseq) . n = (vol (m,seq)) . n )
assume A18: n in NAT ; ::_thesis: (M * Fseq) . n = (vol (m,seq)) . n
then reconsider n1 = n as Element of NAT ;
n1 in dom Fseq by A18, FUNCT_2:def_1;
then (M * Fseq) . n = M . (Fseq . n1) by FUNCT_1:13
.= m . (seq . n1) by A6, Def12 ;
hence (M * Fseq) . n = (vol (m,seq)) . n by Def5; ::_thesis: verum
end;
then A19: SUM (M * Fseq) = SUM (vol (m,seq)) by FUNCT_2:12;
rng Fseq is N_Sub_set_fam of X by MEASURE1:23;
then rng Fseq is N_Measure_fam of sigma F by A16, MEASURE2:def_1;
then M . (union (rng Fseq)) <= SUM (M * Fseq) by MEASURE2:11;
then M . (Union seq1) <= SUM (vol (m,seq)) by A19, CARD_3:def_4;
hence M . B <= SUM (vol (m,seq)) by A17, XXREAL_0:2; ::_thesis: verum
end;
for r being ext-real number st r in Svc (m,B) holds
M . B <= r
proof
let r be ext-real number ; ::_thesis: ( r in Svc (m,B) implies M . B <= r )
assume r in Svc (m,B) ; ::_thesis: M . B <= r
then ex seq being Covering of B,F st r = SUM (vol (m,seq)) by Def7;
hence M . B <= r by A10; ::_thesis: verum
end;
then M . B is LowerBound of Svc (m,B) by XXREAL_2:def_2;
then M . B <= inf (Svc (m,B)) by XXREAL_2:def_4;
then M . B <= (C_Meas m) . B by Def8;
then M . B <= (sigma_Meas (C_Meas m)) . B by A7, A9, MEASURE4:def_3;
hence M . B <= M1 . B by A3, A9, FUNCT_1:49; ::_thesis: verum
end;
A20: for B being set st ex k being Element of NAT st B c= Bseq . k & B in sigma F holds
M . B = M1 . B
proof
let B be set ; ::_thesis: ( ex k being Element of NAT st B c= Bseq . k & B in sigma F implies M . B = M1 . B )
assume ex k being Element of NAT st B c= Bseq . k ; ::_thesis: ( not B in sigma F or M . B = M1 . B )
then consider k being Element of NAT such that
A21: B c= Bseq . k ;
A22: M . (Bseq . k) = m . (Bseq . k) by A6, Def12;
assume A23: B in sigma F ; ::_thesis: M . B = M1 . B
then reconsider B9 = B as Subset of X ;
A24: ( F c= sigma F & Bseq . k in F ) by PROB_1:def_9;
then A25: (Bseq . k) \ B is Element of sigma F by A23, PROB_1:6;
then M . ((Bseq . k) \ B) <= M . (Bseq . k) by A24, MEASURE1:31, XBOOLE_1:36;
then A26: M . ((Bseq . k) \ B) < +infty by A4, A22, Th34, XXREAL_0:2;
(M . B) + (M . ((Bseq . k) \ B)) = M . (B \/ ((Bseq . k) \ B)) by A23, A25, MEASURE1:30, XBOOLE_1:79;
then (M . B) + (M . ((Bseq . k) \ B)) = M . ((Bseq . k) \/ B) by XBOOLE_1:39;
then A27: (M . B) + (M . ((Bseq . k) \ B)) = M . (Bseq . k) by A21, XBOOLE_1:12;
0 <= M . ((Bseq . k) \ B) by SUPINF_2:51;
then A28: M . B = (M . (Bseq . k)) - (M . ((Bseq . k) \ B)) by A27, A26, XXREAL_3:28;
A29: M1 . (Bseq . k) = m . (Bseq . k) by A2, Def12;
(M1 . B) + (M1 . ((Bseq . k) \ B)) = M1 . (B \/ ((Bseq . k) \ B)) by A23, A25, MEASURE1:30, XBOOLE_1:79;
then (M1 . B) + (M1 . ((Bseq . k) \ B)) = M1 . ((Bseq . k) \/ B) by XBOOLE_1:39;
then A30: (M1 . B) + (M1 . ((Bseq . k) \ B)) = M1 . (Bseq . k) by A21, XBOOLE_1:12;
M1 . ((Bseq . k) \ B) <= M1 . (Bseq . k) by A24, A25, MEASURE1:31, XBOOLE_1:36;
then A31: M1 . ((Bseq . k) \ B) < +infty by A4, A29, Th34, XXREAL_0:2;
0 <= M1 . ((Bseq . k) \ B) by SUPINF_2:51;
then A32: M1 . B = (M1 . (Bseq . k)) - (M1 . ((Bseq . k) \ B)) by A30, A31, XXREAL_3:28;
M . ((Bseq . k) \ B) <= M1 . ((Bseq . k) \ B) by A8, A23, A24, PROB_1:6;
then A33: (M1 . (Bseq . k)) - (M1 . ((Bseq . k) \ B)) <= (M . (Bseq . k)) - (M . ((Bseq . k) \ B)) by A29, A22, XXREAL_3:37;
M . B9 <= M1 . B9 by A8, A23;
hence M . B = M1 . B by A28, A32, A33, XXREAL_0:1; ::_thesis: verum
end;
for B being set st B in sigma F holds
M . B = M1 . B
proof
let B be set ; ::_thesis: ( B in sigma F implies M . B = M1 . B )
deffunc H1( set ) -> set = B /\ (Bseq . $1);
assume A34: B in sigma F ; ::_thesis: M . B = M1 . B
then reconsider B9 = B as Subset of X ;
A35: for n being set st n in NAT holds
H1(n) in bool X
proof
let n be set ; ::_thesis: ( n in NAT implies H1(n) in bool X )
assume n in NAT ; ::_thesis: H1(n) in bool X
then Bseq . n in F by Def2;
then (Bseq . n) /\ B c= X /\ X by A34, XBOOLE_1:27;
hence H1(n) in bool X ; ::_thesis: verum
end;
consider Cseq being Function of NAT,(bool X) such that
A36: for n being set st n in NAT holds
Cseq . n = H1(n) from FUNCT_2:sch_2(A35);
reconsider Cseq = Cseq as SetSequence of X ;
for n, m being Element of NAT st n <= m holds
Cseq . n c= Cseq . m
proof
let n, m be Element of NAT ; ::_thesis: ( n <= m implies Cseq . n c= Cseq . m )
A37: Bseq is non-descending by PROB_3:11;
assume n <= m ; ::_thesis: Cseq . n c= Cseq . m
then Bseq . n c= Bseq . m by A37, PROB_1:def_5;
then B /\ (Bseq . n) c= B /\ (Bseq . m) by XBOOLE_1:26;
then Cseq . n c= B /\ (Bseq . m) by A36;
hence Cseq . n c= Cseq . m by A36; ::_thesis: verum
end;
then A38: Cseq is non-descending by PROB_1:def_5;
now__::_thesis:_for_y_being_set_st_y_in_rng_Cseq_holds_
y_in_sigma_F
let y be set ; ::_thesis: ( y in rng Cseq implies y in sigma F )
assume y in rng Cseq ; ::_thesis: y in sigma F
then consider x being set such that
A39: x in NAT and
A40: Cseq . x = y by FUNCT_2:11;
reconsider x = x as Element of NAT by A39;
Bseq . x in F ;
then (Bseq . x) /\ B in sigma F by A1, A34, MEASURE1:34;
hence y in sigma F by A36, A40; ::_thesis: verum
end;
then rng Cseq c= sigma F by TARSKI:def_3;
then reconsider Cseq = Cseq as SetSequence of sigma F by RELAT_1:def_19;
for n being set st n in NAT holds
(M1 * (Partial_Union Cseq)) . n = (M * (Partial_Union Cseq)) . n
proof
let n be set ; ::_thesis: ( n in NAT implies (M1 * (Partial_Union Cseq)) . n = (M * (Partial_Union Cseq)) . n )
assume n in NAT ; ::_thesis: (M1 * (Partial_Union Cseq)) . n = (M * (Partial_Union Cseq)) . n
then reconsider n1 = n as Element of NAT ;
A41: now__::_thesis:_for_x_being_set_st_x_in_(Partial_Union_Cseq)_._n1_holds_
ex_k_being_Element_of_NAT_st_
(_k_<=_n1_&_x_in_Bseq_._k_)
let x be set ; ::_thesis: ( x in (Partial_Union Cseq) . n1 implies ex k being Element of NAT st
( k <= n1 & x in Bseq . k ) )
assume x in (Partial_Union Cseq) . n1 ; ::_thesis: ex k being Element of NAT st
( k <= n1 & x in Bseq . k )
then consider k being Nat such that
A42: k <= n1 and
A43: x in Cseq . k by PROB_3:13;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
take k = k; ::_thesis: ( k <= n1 & x in Bseq . k )
x in B /\ (Bseq . k) by A36, A43;
hence ( k <= n1 & x in Bseq . k ) by A42, XBOOLE_0:def_4; ::_thesis: verum
end;
A44: (Partial_Union Cseq) . n1 c= Bseq . n1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Partial_Union Cseq) . n1 or x in Bseq . n1 )
assume x in (Partial_Union Cseq) . n1 ; ::_thesis: x in Bseq . n1
then consider k being Element of NAT such that
A45: k <= n1 and
A46: x in Bseq . k by A41;
Bseq is non-descending by PROB_3:11;
then Bseq . k c= Bseq . n1 by A45, PROB_1:def_5;
hence x in Bseq . n1 by A46; ::_thesis: verum
end;
A47: (M1 * (Partial_Union Cseq)) . n = M1 . ((Partial_Union Cseq) . n1) by FUNCT_2:15;
A48: rng (Partial_Union Cseq) c= sigma F by RELAT_1:def_19;
dom (Partial_Union Cseq) = NAT by PARTFUN1:def_2;
then (Partial_Union Cseq) . n1 in rng (Partial_Union Cseq) by FUNCT_1:3;
then (M1 * (Partial_Union Cseq)) . n = M . ((Partial_Union Cseq) . n1) by A47, A20, A44, A48;
hence (M1 * (Partial_Union Cseq)) . n = (M * (Partial_Union Cseq)) . n by FUNCT_2:15; ::_thesis: verum
end;
then A49: M1 * (Partial_Union Cseq) = M * (Partial_Union Cseq) by FUNCT_2:12;
for n being Element of NAT holds Cseq . n = B9 /\ (Bseq . n) by A36;
then Cseq = B9 (/\) Bseq by SETLIM_2:def_5;
then Union Cseq = B9 /\ (Union Bseq) by SETLIM_2:38;
then Union Cseq = B9 /\ (Union Aseq) by PROB_3:15;
then Union Cseq = B9 /\ X by A5, CARD_3:def_4;
then A50: B9 = Union Cseq by XBOOLE_1:28;
then B9 = lim Cseq by A38, SETLIM_1:63;
then M1 . B = lim (M1 * Cseq) by A38, Th26;
then M1 . B = lim (M * (Partial_Union Cseq)) by A38, A49, PROB_4:19;
then M1 . B = lim (M * Cseq) by A38, PROB_4:19;
then M1 . B = M . (lim Cseq) by A38, Th26;
hence M1 . B = M . B by A38, A50, SETLIM_1:63; ::_thesis: verum
end;
hence M = (sigma_Meas (C_Meas m)) | (sigma F) by A3, FUNCT_2:12; ::_thesis: verum
end;