:: The Hopf Extension Theorem of Measure
:: by Noboru Endou , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received April 7, 2009
:: Copyright (c) 2009-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, PROB_1, MEASURE1, SUBSET_1, MESFUNC5, ORDINAL1,
SUPINF_2, SERIES_1, FUNCT_1, NAT_1, ARYTM_3, CARD_1, CARD_3, VALUED_0,
SEQ_2, ORDINAL2, XXREAL_0, RELAT_1, PROB_2, XBOOLE_0, TARSKI, FINSEQ_1,
ZFMISC_1, FUNCOP_1, FUNCT_2, MEASURE7, SUPINF_1, NAGATA_2, MCART_1,
FUNCT_7, XXREAL_2, REAL_1, MEASURE4, PROB_3, SETLIM_2, ARYTM_1, SETLIM_1,
EQREL_1, LATTICE5, MEASURE2, MEASURE8;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, XXREAL_0, XXREAL_2,
XREAL_0, VALUED_0, RELAT_1, FUNCOP_1, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, NUMBERS, FINSEQ_1, SETFAM_1, RINFSUP2, MEASURE1, MEASURE2,
MEASURE4, MESFUNC5, SUPINF_2, XXREAL_3, NAT_1, MESFUNC9, SUPINF_1,
RECDEF_1, PROB_1, PROB_2, PROB_3, SETLIM_1, SETLIM_2, NAGATA_2, FUNCT_7;
constructors KURATO_0, MESFUNC5, RINFSUP2, MESFUNC9, SUPINF_1, PROB_3,
MEASURE7, RECDEF_1, SETLIM_2, SETLIM_1, NAGATA_2, FUNCT_7;
registrations MEMBERED, ORDINAL1, MEASURE1, XBOOLE_0, NUMBERS, XXREAL_0,
VALUED_0, FUNCT_1, FUNCT_2, SUBSET_1, RELSET_1, MEASURE4, NAT_1,
XXREAL_3, XREAL_0, PROB_3;
requirements NUMERALS, REAL, BOOLE, SUBSET;
definitions TARSKI, PROB_2;
equalities SUPINF_2, RINFSUP2, MESFUNC9;
expansions SUPINF_2, TARSKI, MESFUNC9;
theorems ZFMISC_1, TARSKI, XBOOLE_0, PROB_1, MEASURE1, FUNCT_2, FUNCT_1,
XBOOLE_1, PROB_3, FINSEQ_1, RELAT_1, MEASURE4, ORDINAL1, NAT_1, FUNCOP_1,
SUPINF_2, XXREAL_2, PROB_4, MEASURE7, XXREAL_0, MEASURE6, FINSUB_1,
CARD_3, RINFSUP2, MESFUNC9, VALUED_0, MESFUNC5, MONOID_1, MEASURE2,
SETLIM_1, SETLIM_2, ABCMIZ_1, PROB_2, NAGATA_2, FUNCTOR1, FUNCT_7,
XXREAL_3, XREAL_0, PARTFUN1, XTUPLE_0;
schemes FUNCT_2, NAT_1, BINOP_2, XBOOLE_0, SUBSET_1;
begin :: The outer measure induced by the finite additive measure
reserve X for set,
F for Field_Subset of X,
M for Measure of F,
A,B for Subset of X,
Sets for SetSequence of X,
seq,seq1,seq2 for ExtREAL_sequence,
n,k for Nat;
theorem Th1:
Ser seq = Partial_Sums seq
proof
for x be object st x in NAT holds Ser(seq).x = (Partial_Sums seq).x
proof
defpred P[Nat] means Ser(seq).$1 = (Partial_Sums seq).$1;
let x be object;
A1: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k];
then (Ser seq).(k+1) = (Partial_Sums seq).k + seq.(k+1) by SUPINF_2:
def 11;
hence P[k+1] by MESFUNC9:def 1;
end;
assume x in NAT;
then reconsider n = x as Element of NAT;
(Ser seq).0 = seq.0 by SUPINF_2:def 11
.= (Partial_Sums seq).0 by MESFUNC9:def 1;
then
A2: P[0];
for k be Nat holds P[k] from NAT_1:sch 2(A2,A1);
then (Ser seq).x = (Partial_Sums seq).n;
hence (Ser seq).x = (Partial_Sums seq).x;
end;
hence Ser seq = Partial_Sums seq by FUNCT_2:12;
end;
:: In the theorem below, the notion "summable" means in MESFUNC9, not in SUPINF_2
theorem Th2:
seq is nonnegative implies seq is summable & SUM seq = Sum seq
proof
assume seq is nonnegative;
then
A1: Partial_Sums seq is non-decreasing by MESFUNC9:16;
then Partial_Sums seq is convergent by RINFSUP2:37;
hence seq is summable;
lim Partial_Sums seq = sup Partial_Sums seq by A1,RINFSUP2:37;
hence Sum seq = SUM seq by Th1;
end;
theorem Th3: :: extension of MEASURE7:4
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
proof
assume that
A1: seq1 is nonnegative and
A2: seq2 is nonnegative;
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;
then
A4: for n be Element of NAT holds seq.n = seq1.n + seq2.n;
A5: for k be Nat holds Fseq.k = Gseq.k + Hseq.k
by A1,A2,A4,MEASURE7:3;
for m,n being ExtReal st m in dom Fseq & n in dom Fseq & m <= n
holds Fseq.m <= Fseq.n
proof
let m,n be ExtReal;
assume that
A6: m in dom Fseq and
A7: n in dom Fseq and
A8: m <= 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 thesis by A1,A2,A4,A7,MEASURE7:3;
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
let n be object;
assume n in dom seq;
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;
end;
hence
A13: seq is nonnegative by SUPINF_2:52;
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;
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;
end;
registration
let X,F;
cluster disjoint_valued for sequence of F;
existence
proof
consider f being sequence of {{}} 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 as sequence of F by FUNCT_2:7;
take f;
A2: for x being object holds f.x = {}
proof
let x be object;
x in dom f implies f.x = {} by A1;
hence thesis by FUNCT_1:def 2;
end;
thus for x,y being object st x <> y holds f.x misses f.y
proof
let x,y be object;
f.x = {} by A2;
hence thesis by XBOOLE_1:65;
end;
end;
end;
definition
let X,F;
mode FinSequence of F -> FinSequence of bool X means
:Def1:
for k being Nat st k in dom it holds it.k in F;
existence
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;
hereby
let k be Nat;
assume k in dom f;
then f.k = X by A1;
hence f.k in F by PROB_1:5;
end;
end;
end;
registration
let X,F;
cluster disjoint_valued for FinSequence of F;
existence
proof
{} c= X;
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;
assume k in dom 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;
end;
then reconsider f = <* {} *> as FinSequence of F by Def1;
take f;
A1: for n being object holds f.n = {}
proof
let n be object;
now
assume n in dom f;
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;
end;
hence thesis by FUNCT_1:def 2;
end;
thus for x,y being object st x <> y holds f.x misses f.y
proof
let x,y be object;
f.x = {} by A1;
hence thesis by XBOOLE_1:65;
end;
end;
end;
definition
let X,F;
mode Sep_FinSequence of F is disjoint_valued FinSequence of F;
end;
definition
let X,F;
mode Sep_Sequence of F is disjoint_valued sequence of F;
end;
definition
let X,F;
mode Set_Sequence of F -> SetSequence of X means
:Def2:
for n be Nat holds it.n in F;
existence
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;
let n be Nat;
n is Element of NAT by ORDINAL1:def 12;
then A.n = X by FUNCOP_1:7;
hence thesis by PROB_1:5;
end;
end;
definition
let X,A,F;
mode Covering of A,F -> Set_Sequence of F means
:Def3:
A c= union rng it;
existence
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 be Nat holds IT.n in F
proof
let n be Nat;
n in NAT by ORDINAL1:def 12;
then IT.n = X by FUNCOP_1:7;
hence IT.n in F by PROB_1:5;
end;
then reconsider IT as Set_Sequence of F by Def2;
take IT;
rng IT = {X} by FUNCOP_1:8;
then X c= union rng IT by ZFMISC_1:25;
hence thesis;
end;
end;
reserve FSets for Set_Sequence of F,
CA for Covering of A,F;
definition
let X,F,FSets,n;
redefine func FSets.n -> Element of F; :: redefines . (FUNCT_1, definition)
correctness by Def2;
end;
Lm1: NAT --> X is Set_Sequence of F
proof
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 be Nat holds G0.n in F
proof
let n be Nat;
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;
end;
hence NAT --> X is Set_Sequence of F by Def2;
end;
definition
let X,F,Sets;
mode Covering of Sets,F -> sequence of Funcs(NAT,bool X) means
:Def4:
for n being Nat holds it.n is Covering of Sets.n,F;
existence
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 sequence of Funcs(NAT,bool X);
take H;
hereby
let n be Nat;
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);
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;
end;
end;
end;
reserve Cvr for Covering of Sets,F;
definition
let X,F,M,FSets;
func vol(M,FSets) -> ExtREAL_sequence means
:Def5:
for n holds it.n = M.( FSets.n);
existence
proof
deffunc H(Element of NAT) = M.(FSets.$1);
consider IT be sequence of ExtREAL such that
A1: for n being Element of NAT holds IT.n = H(n) from FUNCT_2:sch 4;
take IT;
hereby
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence IT.n = M.(FSets.n) by A1;
end;
end;
uniqueness
proof
let V1,V2 be sequence of ExtREAL;
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);
now
let x be object;
assume x in NAT;
then reconsider n = x as Nat;
thus V1.x = M.(FSets.n) by A2
.= V2.x by A3;
end;
hence thesis by FUNCT_2:12;
end;
end;
theorem Th4:
vol(M,FSets) is nonnegative
proof
for n being Element of NAT holds 0 <= (vol(M,FSets)).n
proof
let n be Element of NAT;
(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;
end;
hence thesis by SUPINF_2:39;
end;
definition
let X,F,Sets,Cvr,n;
redefine func Cvr.n -> Covering of Sets.n,F; :: redefines . (FUNCT_1, definition)
correctness by Def4;
end;
definition
let X,F,Sets,M,Cvr;
func Volume(M,Cvr) -> ExtREAL_sequence means
:Def6:
for n being Nat holds it .n = SUM(vol(M,Cvr.n));
existence
proof
defpred P[Element of NAT,Element of ExtREAL] means $2 = SUM(vol(M,Cvr.$1));
A1: for n being Element of NAT holds ex y being Element of ExtREAL st P[n,y ];
consider G0 being sequence of ExtREAL such that
A2: for n being Element of NAT holds P[n,G0.n] from FUNCT_2:sch 3(A1);
take G0;
hereby
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence G0.n = SUM(vol(M,Cvr.n)) by A2;
end;
end;
uniqueness
proof
let G1,G2 be sequence of ExtREAL;
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));
now
let x be object;
assume x in NAT;
then reconsider n = x as Nat;
thus G1.x = SUM(vol(M,Cvr.n)) by A3
.= G2.x by A4;
end;
hence thesis by FUNCT_2:12;
end;
end;
theorem Th5:
0 <= (Volume(M,Cvr)).n
proof
for k being Element of NAT holds 0 <= (vol(M,Cvr.n)).k
proof
let k be Element of NAT;
0 <= M.((Cvr.n).k) by SUPINF_2:51;
hence thesis by Def5;
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 thesis by A1,MEASURE6:2;
end;
definition
let X,F,M,A;
func Svc(M,A) -> Subset of ExtREAL means
:Def7:
for x being R_eal holds x in
it iff ex CA being Covering of A,F st x = SUM vol(M,CA);
existence
proof
defpred P[object] means ex CA being Covering of A,F st $1 = SUM vol(M,CA);
consider D being set such that
A1: for x being object holds x in D iff x in ExtREAL & P[x] from XBOOLE_0
:sch 1;
for z being object holds z in D implies z in ExtREAL by A1;
then reconsider D as Subset of ExtREAL by TARSKI:def 3;
take D;
thus thesis by A1;
end;
uniqueness
proof
defpred P[set] means ex CA being Covering of A,F st $1 = SUM(vol(M,CA));
let D1,D2 be Subset of ExtREAL such that
A2: for x being R_eal holds x in D1 iff P[x] and
A3: for x being R_eal holds x in D2 iff P[x];
thus D1 = D2 from SUBSET_1:sch 2(A2,A3);
end;
end;
registration
let X,A,F,M;
cluster Svc(M,A) -> non empty;
coherence
proof
X c= X & {} c= X;
then consider CA being sequence of bool X such that
A1: rng CA = {X,{}} and
CA.0 = X and
for n being Nat st 0 < n holds CA.n = {} by MEASURE1:19;
for n be Nat holds CA.n in F
proof
let n be Nat;
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,5;
then rng CA c= F by A1,ZFMISC_1:32;
hence CA.n in F by A2;
end;
then union{X,{}} = X \/ {} & CA is Set_Sequence of F by Def2,ZFMISC_1:75;
then reconsider CA as Covering of A,F by A1,Def3;
defpred P[object] means ex G being Covering of A,F st $1 = SUM(vol(M,G));
consider D being set such that
A3: for x being object holds x in D iff x in ExtREAL & P[x] from XBOOLE_0
:sch 1;
SUM(vol(M,CA)) in D by A3;
hence thesis by Def7;
end;
end;
definition
let X,F,M;
func C_Meas M -> Function of bool X,ExtREAL means
:Def8:
for A being Subset of X holds it.A = inf(Svc(M,A));
existence
proof
deffunc F(Element of bool X qua set) = inf(Svc(M,$1));
thus ex G being Function of bool X,ExtREAL st for A being Subset of X
holds G.A = F(A) from FUNCT_2:sch 4;
end;
uniqueness
proof
deffunc F(Subset of X) = inf(Svc(M,$1));
thus for F1,F2 being Function of bool X,ExtREAL st (for A being Subset of
X holds F1.A = F(A)) & (for A being Subset of X holds F2.A = F(A)) holds F1 =
F2 from BINOP_2:sch 1;
end;
end;
definition
func InvPairFunc -> sequence of [:NAT,NAT:] equals
PairFunc";
correctness by FUNCTOR1:2,NAGATA_2:2;
end;
definition
let X,F,Sets,Cvr;
func On Cvr -> Covering of union rng Sets,F means
:Def10:
for n being Nat holds it.n = (Cvr.(pr1 InvPairFunc.n)).(pr2 InvPairFunc.n);
existence
proof
defpred P[Element of NAT,Subset of X] means $2 = (Cvr.(pr1 InvPairFunc.$1)
).(pr2 InvPairFunc.$1);
A1: for n being Element of NAT holds ex y being Subset of X st P[n,y];
consider Seq0 being sequence of bool X such that
A2: for n being Element of NAT holds P[n,Seq0.n] from FUNCT_2:sch 3(A1
);
reconsider Seq0 as SetSequence of X;
for n be Nat holds Seq0.n in F
proof
let n be Nat;
n in NAT by ORDINAL1:def 12;
then Seq0.n = (Cvr.(pr1 InvPairFunc.n)).(pr2 InvPairFunc.n) by A2;
hence Seq0.n in F;
end;
then reconsider Seq0 as Set_Sequence of F by Def2;
union rng Sets c= union rng Seq0
proof
let x be object;
assume x in union rng Sets;
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 thesis by A10,TARSKI:def 4;
end;
then reconsider Seq0 as Covering of union rng Sets,F by Def3;
take Seq0;
hereby
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence Seq0.n = (Cvr.(pr1 InvPairFunc.n)).(pr2 InvPairFunc.n) by A2;
end;
end;
uniqueness
proof
let Seq1,Seq2 be Covering of union rng Sets,F such 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);
for n being object st n in NAT holds Seq1.n = Seq2.n
proof
let n be object;
assume n in NAT;
then reconsider n as Element of NAT;
Seq1.n = (Cvr.(pr1 InvPairFunc.n)).(pr2 InvPairFunc.n) by A11;
hence thesis by A12;
end;
hence thesis by FUNCT_2:12;
end;
end;
theorem Th6:
for k being Nat ex m be Nat st for Sets being
SetSequence of X holds for Cvr being Covering of Sets,F holds (Partial_Sums(vol
(M,On Cvr))).k <= (Partial_Sums Volume(M,Cvr)).m
proof
defpred P[Nat] means
ex m being Nat st for Sets being SetSequence
of X holds for Cvr being Covering of Sets,F holds (Partial_Sums(vol(M,On Cvr)))
.$1 <= (Partial_Sums Volume(M,Cvr)).m;
{} c= X;
then reconsider D = NAT --> {} as sequence of bool X by FUNCOP_1:45;
reconsider y = D as Element of Funcs(NAT,bool X) by FUNCT_2:8;
A1: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
set a = (pr1 InvPairFunc).(k+1);
set b = (pr2 InvPairFunc).(k+1);
set N0 = {s where s is Element of NAT : a = pr1 InvPairFunc.s};
A2: N0 c= NAT
proof
let s1 be object;
assume s1 in N0;
then ex s being Element of NAT st s = s1 & a = pr1 InvPairFunc.s;
hence thesis;
end;
k+1 in N0;
then reconsider N0 as non empty Subset of NAT by A2;
given m0 being Nat such that
A3: for Sets being SetSequence of X holds for Cvr being Covering of
Sets,F holds Partial_Sums(vol(M,On Cvr)).k <= (Partial_Sums Volume(M,Cvr)).m0;
take m = m0 + pr1 InvPairFunc.(k+1);
let Sets be SetSequence of X;
let Cvr be Covering of Sets,F;
defpred QQ0[Element of NAT,Function] means (($1 = a implies for m being
Element of NAT holds $2.m = (Cvr.$1).m) & ($1 <> a implies for m being Element
of NAT holds $2.m = {}));
defpred QQ1[Element of NAT,Function] means ($1 <> a implies for m being
Element of NAT holds $2.m = (Cvr.$1).m) & ($1 = a implies for m being Element
of NAT holds $2.m = {});
A4: for n being Element of NAT holds ex y being Element of Funcs(NAT,bool
X) st QQ0[n,y]
proof
let n be Element of NAT;
A5: now
reconsider y = Cvr.n as Element of Funcs(NAT,bool X) by FUNCT_2:8;
assume
A6: n = a;
take y;
thus QQ0[n,y] by A6;
end;
n <> a implies QQ0[n,y] by FUNCOP_1:7;
hence thesis by A5;
end;
consider Cvr0 being sequence of Funcs(NAT,bool X) such that
A7: for n being Element of NAT holds QQ0[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;
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 as SetSequence of X by A10,FUNCT_2:2;
for s being Nat holds FSets0.s in F
proof
let s be Nat;
A11: s in NAT by ORDINAL1:def 12;
A12: now
assume n = a;
then FSets0.s = (Cvr.n).s by A7,A9,A11;
hence FSets0.s in F;
end;
n in NAT by ORDINAL1:def 12;
then n <> a implies FSets0.s = {} by A7,A9,A11;
hence thesis by A12,PROB_1:4;
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;
hence Cvr0.n is Covering of D.n,F by A9,A13,Def3;
end;
A14: for n being Element of NAT holds ex y being Element of Funcs(NAT,bool
X) st QQ1[n,y]
proof
let n be Element of NAT;
A15: now
reconsider y = Cvr.n as Element of Funcs(NAT,bool X) by FUNCT_2:8;
assume
A16: n <> a;
take y;
thus QQ1[n,y] by A16;
end;
n = a implies QQ1[n,y] by FUNCOP_1:7;
hence thesis by A15;
end;
consider Cvr1 being sequence of Funcs(NAT,bool X) such that
A17: for n being Element of NAT holds QQ1[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;
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 as sequence of bool X by A19,FUNCT_2:2;
for s being Nat holds FSets1.s in F
proof
let s be Nat;
A20: s in NAT by ORDINAL1:def 12;
A21: n in NAT by ORDINAL1:def 12;
A22: now
assume n <> a;
then FSets1.s = (Cvr.n).s by A17,A18,A21,A20;
hence FSets1.s in F;
end;
n = a implies FSets1.s = {} by A17,A18,A20;
hence thesis by A22,PROB_1:4;
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;
hence Cvr1.n is Covering of D.n,F by A18,A23,Def3;
end;
then reconsider Cvr1 as Covering of D,F by Def4;
reconsider Cvr0 as Covering of D,F by A8,Def4;
set PSv1 = Partial_Sums vol(M,On Cvr1);
(On Cvr1).(k+1) = (Cvr1.a).b 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 SSS[Element of N0,Element of NAT] means $2 = pr2 InvPairFunc.$1;
A25: for s being Element of N0 holds ex y being Element of NAT st SSS[s,y];
consider SOS being Function of N0,NAT such that
A26: for s being Element of N0 holds SSS[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.a))*SOS).s) & (not s in N0 implies (vol(M,On Cvr0)).s = 0)
proof
let s be Element of NAT;
thus s in N0 implies (vol(M,On Cvr0)).s = ((vol(M,Cvr0.a))*SOS).s
proof
A28: (vol(M,On Cvr0)).s = M.((On Cvr0).s) by Def5;
assume
A29: s in N0;
then
( ex s1 being Element of NAT st s1 = s & a = pr1 InvPairFunc.s1)&
pr2 InvPairFunc.s =SOS.s by A26;
then (vol(M,On Cvr0)).s = M.((Cvr0.a).(SOS.s)) by A28,Def10;
then (vol(M,On Cvr0)).s = (vol(M,Cvr0.a)).(SOS.s) by Def5;
hence thesis by A29,FUNCT_2:15;
end;
assume not s in N0;
then
A30: not a = 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 thesis by VALUED_0:def 19;
end;
now
let s1,s2 be object;
assume that
A31: s1 in N0 & s2 in N0 and
A32: SOS.s1 = SOS.s2;
A33: ( ex s11 being Element of NAT st s11 = s1 & a = pr1 InvPairFunc.s11
)& ex s22 being Element of NAT st s22 = s2 & a = 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;
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:def 11
.= (Ser vol(M,On Cvr1)).k by A24,XXREAL_3:4;
then PSv1.(k+1) = (Ser vol(M,On Cvr1)).k by Th1;
then
A36: PSv1.(k+1) = PSv1.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)).a <= (Ser Volume(M,Cvr0)).a by MEASURE7:2;
then
A38: SUM vol(M,Cvr0.a) <= (Ser Volume(M,Cvr0)).a by Def6;
(Ser Volume(M,Cvr0)).a <= (Ser Volume(M,Cvr0)).m by A37,SUPINF_2:41;
then
A39: SUM vol(M,Cvr0.a) <= (Ser Volume(M,Cvr0)).m by A38,XXREAL_0:2;
vol(M,Cvr0.a) is nonnegative by Th4;
then SUM vol(M,On Cvr0) <= SUM vol(M,Cvr0.a) by A35,A27,MEASURE7:11;
then
A40: SUM vol(M,On Cvr0) <= (Ser Volume(M,Cvr0)).m by A39,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 A40,XXREAL_0:2
;
then PSv0.(k+1) <= (Ser Volume(M,Cvr0)).m by Th1;
then
A41: PSv0.(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
A42: 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
A43: (Partial_Sums Volume(M,Cvr1)).m0 <= (Partial_Sums Volume(M,Cvr1)).m
by RINFSUP2:7;
A44: 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;
set n1 = pr1 InvPairFunc.n;
set n2 = pr2 InvPairFunc.n;
A45: (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
A46: (vol(M,On Cvr)).n = M.((Cvr.n1).n2) by Def10;
per cases;
suppose
A47: n1 = a;
(On Cvr1).n = (Cvr1.n1).n2 by Def10
.= {} by A17,A47;
then
A48: M.((On Cvr1).n) = 0 by VALUED_0:def 19;
(On Cvr0).n = (Cvr0.n1).n2 by Def10
.= (Cvr.n1).n2 by A7,A47;
hence thesis by A45,A46,A48,XXREAL_3:4;
end;
suppose
A49: n1 <> a;
(On Cvr0).n = (Cvr0.n1).n2 by Def10
.= {} by A7,A49;
then
A50: M.((On Cvr0).n) = 0 by VALUED_0:def 19;
(On Cvr1).n = (Cvr1.n1).n2 by Def10
.= (Cvr.n1).n2 by A17,A49;
hence thesis by A45,A46,A50,XXREAL_3:4;
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 A44,MEASURE7:3;
then PSv.(k+1) = (Ser vol(M,On Cvr0)).(k+1) + (Ser vol(M,On Cvr1)).(k+1)
by Th1;
then PSv.(k+1) = PSv0.(k+1) + (Ser vol(M,On Cvr1)).(k+1) by Th1;
then
A51: PSv.(k+1) = PSv0.(k+1) + PSv1.(k+1) by Th1;
PSv1.k <= (Partial_Sums Volume(M,Cvr1)).m0 by A3;
then
A52: PSv1.(k+1) <= (Partial_Sums Volume(M,Cvr1)).m by A36,A43,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;
A53: now
assume
A54: n <> a;
for s being Element of NAT holds (vol(M,Cvr0.n)).s = 0.
proof
let s be Element of NAT;
(Cvr0.n).s = {} by A7,A54;
then M.((Cvr0.n).s) = 0 by VALUED_0:def 19;
hence thesis by Def5;
end;
then
A55: 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;
(vol(M,Cvr1.n)).s = M.((Cvr1.n).s) & (vol(M,Cvr.n)).s = M.((Cvr
.n).s) by Def5;
hence thesis by A17,A54;
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 A55,
XXREAL_3:4;
end;
A56: now
assume
A57: n = a;
for s being Element of NAT holds (vol(M,Cvr1.n)).s = 0
proof
let s be Element of NAT;
(Cvr1.n).s = {} by A17,A57;
then M.((Cvr1.n).s) = 0 by VALUED_0:def 19;
hence (vol(M,Cvr1.n)).s = 0 by Def5;
end;
then
A58: 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;
(vol(M,Cvr0.n)).s = M.((Cvr0.n).s) by Def5
.= M.((Cvr.n).s) by A7,A57;
hence thesis by Def5;
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 A58,
XXREAL_3:4;
end;
(Volume(M,Cvr)).n = SUM vol(M,Cvr.n) & (Volume(M,Cvr0)).n = SUM vol
(M,Cvr0.n ) by Def6;
hence thesis by A56,A53,Def6;
end;
then (Ser Volume(M,Cvr)).m = (Ser Volume(M,Cvr0)).m + (Ser Volume(M,Cvr1)
).m by A37,A42,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 thesis by A41,A52,A51,XXREAL_3:36;
end;
A59: P[0]
proof
take m = pr1 InvPairFunc.0;
let Sets be SetSequence of X;
let Cvr be Covering of Sets,F;
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
A60: (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 thesis by A60,XXREAL_0:2;
end;
thus for k being Nat holds P[k] from NAT_1:sch 2(A59,A1 );
end;
theorem Th7:
inf Svc(M,union rng Sets) <= SUM Volume(M,Cvr)
proof
set Q = SUM(vol(M,On Cvr));
for x being ExtReal st x in rng Ser vol(M,On Cvr) ex y being
ExtReal st y in rng Ser Volume(M,Cvr) & x <= y
proof
let x be ExtReal;
assume x in rng Ser vol(M,On Cvr);
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 holds for G be 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;
A3: for Sets being SetSequence of X, G be Covering of Sets,F holds Ser(vol
(M,On G)).n <= Ser (Volume(M,G)).m
proof
let Sets be SetSequence of X;
let G be Covering of Sets,F;
(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;
end;
m in NAT by ORDINAL1:def 12;
hence thesis by A1,A3,FUNCT_2:4;
end;
then
A4: SUM vol(M,On Cvr) <= SUM Volume(M,Cvr) by XXREAL_2:63;
Q in Svc(M,union rng Sets) by Def7;
then inf Svc(M,union rng Sets) <= Q by XXREAL_2:3;
hence thesis by A4,XXREAL_0:2;
end;
theorem Th8:
A in F implies (A,{}X) followed_by {}X is Covering of A,F
proof
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;
for n be Nat holds Sets.n in F
proof
let n be Nat;
per cases by NAT_1:25;
suppose
n = 0;
hence Sets.n in F by A3,FUNCT_7:122;
end;
suppose
n = 1;
hence Sets.n in F by A2,PROB_1:4;
end;
suppose
n > 1;
then Sets.n = {} by FUNCT_7:124;
hence Sets.n in F by PROB_1:4;
end;
end;
then reconsider Sets as Set_Sequence of F by Def2;
A c= union rng Sets
proof
let x be object;
dom Sets = NAT by FUNCT_2:def 1;
then
A4: Sets.0 in rng Sets by FUNCT_1:3;
assume x in A;
hence x in union rng Sets by A1,A4,TARSKI:def 4;
end;
hence (A,{}X) followed_by {}X is Covering of A,F by Def3;
end;
theorem Th9:
for X being set, F being Field_Subset of X, M being Measure of F,
A be set st A in F holds (C_Meas M).A <= M.A
proof
let X be set;
let F be Field_Subset of X;
let M be Measure of F;
let A9 be set;
assume
A1: A9 in F;
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 object;
dom Aseq = NAT by FUNCT_2:def 1;
then
A4: Aseq.0 in rng Aseq by FUNCT_1:3;
assume x in A;
hence x in union rng Aseq by A3,A4,TARSKI:def 4;
end;
then reconsider 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 being Element of NAT;
assume 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;
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;
end;
theorem Th10:
C_Meas M is nonnegative
proof
for r being ExtReal st r in rng (C_Meas M) holds 0 <= r
proof
let r be ExtReal;
assume r in rng (C_Meas M);
then consider A being object such that
A1: A in bool X and
A2: (C_Meas M).A = r by FUNCT_2:11;
reconsider A as Subset of X by A1;
now
let p be ExtReal;
assume p in Svc(M,A);
then ex G be Covering of A,F st p = SUM vol(M,G) by Def7;
hence 0 <= p by Th4,MEASURE6:2;
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;
end;
then for r being ExtReal holds r in rng C_Meas M implies 0 <= r;
then rng C_Meas M is nonnegative;
hence C_Meas M is nonnegative;
end;
theorem Th11:
(C_Meas M).{} = 0
proof
(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;
hence (C_Meas M).{} = 0. by A1,A2;
end;
theorem Th12:
A c= B implies (C_Meas M).A <= (C_Meas M).B
proof
assume
A1: A c= B;
now
let r be object;
assume r in Svc(M,B);
then consider G be 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;
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;
end;
then
A3: Svc(M,B) c= Svc(M,A);
(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;
end;
Lm2: (ex n be Nat st (C_Meas M).(Sets.n) = +infty) implies (C_Meas M).(union
rng Sets) <= SUM((C_Meas M)*Sets)
proof
assume ex n be Nat st (C_Meas M).(Sets.n) = +infty;
then consider N being Nat such that
A1: (C_Meas M).(Sets.N) = +infty;
reconsider 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;
end;
theorem Th13:
(C_Meas M).(union rng Sets) <= SUM((C_Meas M)*Sets)
proof
A1: now
assume
A2: for n being Element of NAT holds Svc(M,Sets.n) <> {+infty};
inf Svc(M,union rng Sets) <= sup rng Ser((C_Meas M)*Sets)
proof
set y = inf Svc(M,union rng Sets), x = sup rng Ser((C_Meas M)*Sets);
A3: Ser((C_Meas M)*Sets).0 <= x 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:def 11;
assume not inf Svc(M,union rng Sets) <= sup rng Ser((C_Meas M)*Sets);
then consider eps being Real such that
A6: 0 < eps and
A7: x + eps < y by A5,A3,XXREAL_3:49;
consider E being sequence of ExtREAL such that
A8: for n being 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 P[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 holds ex F0 being Element of Funcs(NAT,
bool X) st P[n,F0]
proof
let n be Element of NAT;
C_Meas M is nonnegative & (C_Meas M).(Sets.n) = inf Svc(M,Sets.n)
by Def8,Th10;
then
A12: 0 in REAL & 0. <= inf Svc(M,Sets.n) by SUPINF_2:51,XREAL_0:def 1;
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 object such that
A13: x in Svc(M,Sets.n) \ {+infty} by XBOOLE_0:def 1;
reconsider 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,4;
then inf Svc(M,Sets.n) is Element of REAL by A12,XXREAL_0:46;
then consider S1 being ExtReal 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 as Element of Funcs(NAT,bool X) by FUNCT_2:8;
take FS;
thus thesis by A16,A17;
end;
consider FF being sequence of Funcs(NAT,bool X) such that
A18: for n being Element of NAT holds P[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;
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 thesis;
end;
deffunc F(Element of NAT) = ((C_Meas M)*Sets).$1 + E.$1;
A20: for x being Element of NAT holds F(x) is Element of ExtREAL;
consider G0 being sequence of ExtREAL such that
A21: for n being Element of NAT holds G0.n = F(n) from FUNCT_2:sch 9
(A20);
reconsider 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;
(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 thesis by A21;
end;
then
A22: SUM Volume(M,FF) <= SUM G0 by SUPINF_2:43;
A23: now
let n be Nat;
n is Element of NAT by ORDINAL1:def 12;
hence G0.n = ((C_Meas M)*Sets).n + E.n by A21;
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;
y <= SUM Volume(M,FF) by Th7;
hence thesis by A7,A24,XXREAL_0:2;
end;
hence thesis by Def8;
end;
now
assume ex n being Element of NAT st Svc(M,Sets.n) = {+infty};
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 thesis by Lm2;
end;
hence thesis by A1;
end;
theorem Th14:
C_Meas M is C_Measure of X
proof
(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 sequence of bool X holds (C_Meas
M).( union rng F) <= SUM((C_Meas M)*F) by Th10,Th12,Th13;
hence thesis by A1,MEASURE4:def 1;
end;
definition
let X be set;
let F be Field_Subset of X;
let M be Measure of F;
redefine func C_Meas M -> C_Measure of X; :: redefines C_Meas (MEASURE8, definition)
correctness by Th14;
end;
begin :: E. Hopf's extension theorem
definition
let X be set;
let F be Field_Subset of X;
let M be Measure of F;
attr M is completely-additive means
for FSets being Sep_Sequence of
F st union rng FSets in F holds SUM(M*FSets) = M.(union rng FSets);
end;
theorem Th15:
Partial_Union FSets is Set_Sequence of F
proof
defpred P[Nat] means (Partial_Union FSets).$1 in F;
A1: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
A2: (Partial_Union FSets).(k+1) = (Partial_Union FSets).k \/ FSets.(k+1)
by PROB_3:def 2;
assume P[k];
hence P[k+1] by A2,PROB_1:3;
end;
(Partial_Union FSets).0 = FSets.0 by PROB_3:def 2;
then
A3: P[0];
for n be Nat holds P[n] from NAT_1:sch 2(A3,A1);
hence thesis by Def2;
end;
theorem Th16:
Partial_Diff_Union FSets is Set_Sequence of F
proof
defpred P[Nat] means (Partial_Diff_Union FSets).$1 in F;
A1: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k];
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 P[k+1] by A2,PROB_1:6;
end;
(Partial_Diff_Union FSets).0 = FSets.0 by PROB_3:def 3;
then
A3: P[0];
for n be Nat holds P[n] from NAT_1:sch 2(A3,A1);
hence thesis by Def2;
end;
theorem Th17:
A in F implies ex FSets being Sep_Sequence of F st A = union rng
FSets & for n be Nat holds FSets.n c= CA.n
proof
deffunc F(Element of NAT) = (Partial_Diff_Union CA).$1 /\ A;
consider FSets be sequence of bool X such that
A1: for n being Element of NAT holds FSets.n = F(n) from FUNCT_2:sch 4;
reconsider FSets as SetSequence of X;
assume
A2: A in F;
now
let y be object;
assume y in rng FSets;
then consider x be object 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;
end;
then rng FSets c= F;
then reconsider FSets as sequence of F by FUNCT_2:6;
for m,n be Nat st m <> n holds FSets.m misses FSets.n
proof
let m,n be Nat;
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;
then (Partial_Diff_Union CA).m misses (Partial_Diff_Union CA).n by
PROB_3:def 4;
hence thesis by A7,A6,XBOOLE_1:64;
end;
then reconsider FSets as Sep_Sequence of F by PROB_3:def 4;
now
let x be object;
assume
A8: x in A;
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 be set such that
A9: x in E and
A10: E in rng Partial_Diff_Union CA by TARSKI:def 4;
consider n be object such that
A11: n in NAT and
A12: (Partial_Diff_Union CA).n = E by A10,FUNCT_2:11;
reconsider 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;
end;
then
A14: A c= union rng FSets;
take FSets;
now
let x be object;
assume x in union rng FSets;
then consider E be set such that
A15: x in E and
A16: E in rng FSets by TARSKI:def 4;
consider n be object such that
A17: n in NAT and
A18: FSets.n = E by A16,FUNCT_2:11;
reconsider 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;
end;
then union rng FSets c= A;
hence A = union rng FSets by A14,XBOOLE_0:def 10;
hereby
let n be Nat;
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;
end;
end;
theorem Th18:
M is completely-additive implies for A be set st A in F holds M.
A = (C_Meas M).A
proof
assume
A1: M is completely-additive;
let A be set;
assume
A2: A in F;
then reconsider A9 = A as Subset of X;
for x be ExtReal st x in Svc(M,A9) holds M.A <= x
proof
let x be ExtReal;
assume x in Svc(M,A9);
then consider Aseq be 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 be 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;
M.(Bseq.n) <= M.(Aseq.n) by A5,MEASURE1:8;
then (M*Bseq).n <= M.(Aseq.n) by FUNCT_2:15;
hence thesis by Def5;
end;
then SUM(M*Bseq) <= SUM vol(M,Aseq) by SUPINF_2:43;
hence M.A <= x by A1,A2,A3,A4;
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;
end;
reserve C for C_Measure of X;
theorem Th19:
(for B being Subset of X holds C.(B /\ A) + C.(B /\ (X \ A)) <=
C.B) implies A in sigma_Field C
proof
assume
A1: for B being Subset of X holds C.(B /\ A) + C.(B /\ (X \ A)) <= C.B;
for W,Z being Subset of X holds (W c= A & Z c= X \ A implies C.W + C.Z
<= C.(W \/ Z))
proof
let W,Z be Subset of X;
assume that
A2: W c= A and
A3: Z c= X \ A;
set Y = W \/ Z;
A4: Z misses A by A3,XBOOLE_1:106;
A5: Y /\ (X \ A) = (Y /\ 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;
Y /\ 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 thesis by A1,A5;
end;
hence A in sigma_Field C by MEASURE4:def 2;
end;
theorem Th20:
F c= sigma_Field C_Meas M
proof
set C = C_Meas M;
let E be object;
assume
A1: E in F;
then reconsider E9 = E as Subset of X;
for A being Subset of X holds C.(A /\ E9) + C.(A /\ (X \ E9)) <= C.A
proof
let A be Subset of X;
set CA = (C_Meas M).(A /\ E9) + (C_Meas M).(A /\ (X \ E9));
A2: for seq be 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;
deffunc F1(Element of NAT) = seq.$1 /\ E9;
consider Bseq be sequence of bool X such that
A3: for n be Element of NAT holds Bseq.n = F1(n) from FUNCT_2:sch
4;
reconsider Bseq as SetSequence of X;
for n be Nat holds Bseq.n in F
proof
let n be Nat;
n in NAT by ORDINAL1:def 12;
then Bseq.n = seq.n /\ E9 by A3;
hence Bseq.n in F by A1,FINSUB_1:def 2;
end;
then reconsider Bseq as Set_Sequence of F by Def2;
A4: for x being set st x in A ex n being Element of NAT st x in seq.n
proof
let x be set;
assume
A5: x in A;
A c= union rng seq by Def3;
then consider B be set such that
A6: x in B and
A7: B in rng seq by A5,TARSKI:def 4;
ex n be Element of NAT st B = seq.n by A7,FUNCT_2:113;
hence thesis by A6;
end;
now
let x be object;
assume
A8: x in A /\ E9;
then x in A by XBOOLE_0:def 4;
then consider n be 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 /\ E9 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;
end;
then A /\ E9 c= union rng Bseq;
then reconsider Bseq as Covering of A/\E9,F by Def3;
deffunc F2(Element of NAT) = seq.$1 /\ (X \ E9);
consider Cseq be sequence of bool X such that
A11: for n be Element of NAT holds Cseq.n = F2(n) from FUNCT_2:sch
4;
reconsider Cseq as SetSequence of X;
for n be Nat holds Cseq.n in F
proof
let n be Nat;
X in F by PROB_1:5;
then
A12: X \ E9 in F by A1,PROB_1:6;
n in NAT by ORDINAL1:def 12;
then Cseq.n = seq.n /\ (X \ E9) by A11;
hence Cseq.n in F by A12,FINSUB_1:def 2;
end;
then reconsider Cseq as Set_Sequence of F by Def2;
now
let x be object;
assume
A13: x in A /\ (X \ E9);
then x in A by XBOOLE_0:def 4;
then consider n be 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 \ E9) 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;
end;
then A /\ (X \ E9) c= union rng Cseq;
then reconsider Cseq as Covering of A/\(X\E9),F by Def3;
A16: for n be Nat holds (vol(M,seq)).n = (vol(M,Bseq)).n + (vol(M,Cseq )).n
proof
let n be Nat;
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 /\ E9 & Cseq.n = seq.n /\ (X \ E9) by A3,A11;
then Bseq.n \/ Cseq.n = seq.n /\ (E9 \/ (X \ E9)) by XBOOLE_1:23;
then Bseq.n \/ Cseq.n = seq.n /\ (E9 \/ 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,79;
hence (vol(M,seq)).n = (vol(M,Bseq)).n + (vol(M,Cseq)).n by A20,A17
,A18,MEASURE1:def 3;
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;
end;
for r be ExtReal holds r in Svc(M,A) implies CA <= r
proof
let r be ExtReal;
assume r in Svc(M,A);
then ex G be Covering of A,F st r = SUM vol(M,G) by Def7;
hence thesis by A2;
end;
then CA is LowerBound of Svc(M,A) by XXREAL_2:def 2;
then CA <= inf Svc(M,A) by XXREAL_2:def 4;
hence CA <= (C_Meas M).A by Def8;
end;
hence E in sigma_Field(C_Meas M) by Th19;
end;
theorem Th21:
for X be set, F be Field_Subset of X, FSets be Set_Sequence of F
, M be Function of F,ExtREAL holds M * FSets is ExtREAL_sequence
proof
let X be set;
let F be Field_Subset of X;
let FSets be Set_Sequence of F;
let M be Function of F,ExtREAL;
now
let y be object;
assume y in rng FSets;
then ex x be object st x in NAT & FSets.x = y by FUNCT_2:11;
hence y in F by Def2;
end;
then rng FSets c= F;
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 thesis by FUNCT_2:def 1;
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;
redefine func g*FSets -> ExtREAL_sequence; :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
correctness by Th21;
end;
theorem Th22:
for X be set, S be SigmaField of X, SSets be SetSequence of S, M
be Function of S,ExtREAL holds M * SSets is ExtREAL_sequence
proof
let X be set;
let S be SigmaField of X;
let SSets be SetSequence of S;
let M be Function of S,ExtREAL;
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 thesis by FUNCT_2:def 1;
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;
redefine func g*SSets -> ExtREAL_sequence; :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
correctness by Th22;
end;
theorem Th23:
for F,G being sequence of ExtREAL, 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 sequence of ExtREAL;
let n be Nat;
assume
A1: for m being Nat st m <= n holds F.m <= G.m;
defpred P[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 P[k] holds P[k+1]
proof
let k be Nat;
assume
A3: P[k];
now
assume
A4: for m being Nat st m <= k+1 holds F.m <= G.m;
A5: now
let m be Nat;
assume m <= k;
then m < k+1 by NAT_1:13;
hence F.m <= G.m by A4;
end;
F.(k+1) <= G.(k+1) by A4;
then (Ser F).k + F.(k+1) <= (Ser G).k + G.(k+1) by A3,A5,XXREAL_3:36;
then (Ser F).(k+1) <= (Ser G).k + G.(k+1) by SUPINF_2:def 11;
hence (Ser F).(k+1) <= (Ser G).(k+1) by SUPINF_2:def 11;
end;
hence P[k+1];
end;
now
A6: (Ser F).0 = F.0 & (Ser G).0 = G.0 by SUPINF_2:def 11;
assume for m being Nat st m <= 0 holds F.m <= G.m;
hence (Ser F).0 <= (Ser G).0 by A6;
end;
then
A7: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A7,A2);
hence thesis by A1;
end;
theorem Th24:
for X,C 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,C;
let seq be Sep_Sequence of sigma_Field C;
A1: rng seq c= sigma_Field C by RELAT_1:def 19;
then reconsider seq1 = seq as sequence of bool X by FUNCT_2:6;
A2: for A being Subset of X, n being Element of NAT holds (Ser(C*(A (/\) seq1
))).n + C.(A /\ (X \ union rng seq)) <= C.A
proof
defpred P[Nat] means for A be Subset of X holds C.A >= (Ser(C*(A (/\) seq1
))).$1 + C.(A /\ (X \ union rng seq));
let A be Subset of X, n be Element of NAT;
A3: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A4: P[k];
A5: now
let A be Subset of X;
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;
reconsider m1 = m as Element of NAT by ORDINAL1:def 12;
assume m <= k;
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,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 thesis by FUNCT_2:15;
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,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;
end;
let A be Subset of X;
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,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,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:def 11;
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;
end;
A17: seq.0 in sigma_Field C;
now
let A be Subset of X;
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:def 11
.= 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;
end;
then
A20: P[0];
for k be Nat holds P[k] from NAT_1:sch 2(A20,A3);
hence thesis;
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;
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 & 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 & C.(A /\ (X \ union rng seq)) = +infty);
for x be ExtReal holds x in rng Ser(C*(A(/\)seq1)) implies
x <= C.A - C.(A /\ (X \ union rng seq))
proof
let x be ExtReal;
assume x in rng Ser(C*(A(/\)seq1));
then consider i be object such that
A26: i in NAT and
A27: Ser(C*(A(/\)seq1)).i = x by FUNCT_2:11;
reconsider 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;
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;
end;
hence SUM(C*(A(/\)seq1)) + C.(A /\ (X \ union rng seq)) <= C.A by
XXREAL_0:3;
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;
end;
then
A30: C.(union rng seq /\ Union seq1) <= SUM(C*(union rng seq (/\) seq1));
for W,Z be Subset of X holds (W c= Union seq1 & Z c= X \ Union seq1
implies C.W + C.Z <= C.(W \/ Z))
proof
let W,Z be Subset of X;
assume that
A31: W c= Union seq1 and
A32: Z c= X \ Union seq1;
set A = W \/ Z;
A33: A /\ (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.(A /\ (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;
A /\ Union seq1 = W \/ Z /\ Union seq1 by A31,XBOOLE_1:30;
then C.W <= SUM(C*(A(/\)seq1)) by A21,A36;
then
A37: C.W + C.Z <= SUM(C*(A(/\)seq1)) + C.(A /\ (X \ union rng seq)) by A35,
XXREAL_3:36;
SUM(C*(A(/\)seq1)) + C.(A /\ (X \ union rng seq)) <= C.A by A21;
hence C.W + C.Z <= C.(W \/ Z) by A37,XXREAL_0:2;
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;
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 be object st n in NAT holds (union rng seq(/\)seq1).n = seq.n
proof
let n be object;
assume n in NAT;
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 thesis by SETLIM_2:def 5;
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 ExtReal st m in dom Sseq & n in dom Sseq & m <= n
holds Sseq.m <= Sseq.n by MEASURE7:8;
then Sseq 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;
end;
theorem
for X,C for seq being SetSequence of sigma_Field C holds Union seq in
sigma_Field C
proof
let X,C;
let seq be SetSequence of sigma_Field(C);
set Aseq = Partial_Diff_Union seq;
rng Aseq c= sigma_Field(C) by RELAT_1:def 19;
then reconsider Aseq9 = Aseq as sequence of sigma_Field(C) by FUNCT_2:6;
reconsider Aseq9 as Sep_Sequence of sigma_Field(C);
union rng Aseq9 in sigma_Field(C) by Th24;
then Union Aseq in sigma_Field(C) by CARD_3:def 4;
hence Union seq in sigma_Field(C) by PROB_3:36;
end;
theorem Th26:
for X being non empty set, S be SigmaField of X, M be
sigma_Measure of S, SSets being SetSequence of S st SSets is non-descending
holds lim(M*SSets) = M.(lim SSets)
proof
let X be non empty set;
let S be SigmaField of X;
let M be sigma_Measure of S;
let SSets be SetSequence of S;
assume
A1: SSets is non-descending;
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 be object st n in NAT holds Ser(M*Bseq).n = (M*Partial_Union SSets) .n
proof
defpred P[Nat] means Ser(M*Bseq).$1 = (M*Partial_Union SSets).$1;
let n be object;
A3: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A4: P[k];
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,def 3;
A6: k in NAT by ORDINAL1:def 12;
Ser(M*Bseq).(k+1) = Ser(M*Bseq).k + (M*Bseq).(k+1) by SUPINF_2:def 11
.= (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,A6
.= 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;
end;
assume n in NAT;
then reconsider n1 = n as Element of NAT;
Ser(M*Bseq).0 = (M*Bseq).0 by SUPINF_2:def 11
.= 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
A7: P[0] by FUNCT_2:15;
for k being Nat holds P[k] from NAT_1:sch 2(A7,A3);
then Ser(M*Bseq).n1 = (M*Partial_Union SSets).n1;
hence thesis;
end;
then
A8: 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 ExtReal 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
A9: 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 A9,CARD_3:def 4;
hence thesis by A1,A8,SETLIM_1:63;
end;
theorem
FSets is non-descending implies M*FSets is non-decreasing
proof
A1: dom(M*FSets) = NAT by FUNCT_2:def 1;
assume
A2: FSets is non-descending;
now
let n,m be Nat;
A3: n in NAT & m in NAT by ORDINAL1:def 12;
assume n <= m;
then
A4: 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,A3;
hence (M*FSets).n <= (M*FSets).m by A4,MEASURE1:8;
end;
then for n,m be Nat st m<=n holds (M*FSets).m<=(M*FSets).n;
hence M*FSets is non-decreasing by RINFSUP2:7;
end;
theorem
FSets is non-ascending implies M*FSets is non-increasing
proof
A1: dom(M*FSets) = NAT by FUNCT_2:def 1;
assume
A2: FSets is non-ascending;
now
let n,m be Nat;
A3: n in NAT & m in NAT by ORDINAL1:def 12;
assume m <= n;
then
A4: 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,A3;
hence (M*FSets).n <= (M*FSets).m by A4,MEASURE1:8;
end;
hence M*FSets is non-increasing by RINFSUP2:7;
end;
theorem Th29:
for X being set, S be SigmaField of X, M be sigma_Measure of S,
SSets being SetSequence of S st SSets is non-descending holds M*SSets is
non-decreasing
proof
let X be set;
let S be SigmaField of X;
let M be sigma_Measure of S;
let SSets be SetSequence of S;
A1: dom(M*SSets) = NAT by FUNCT_2:def 1;
assume
A2: SSets is non-descending;
now
let n,m be Nat;
A3: n in NAT & m in NAT by ORDINAL1:def 12;
A4: (M*SSets).m = M.(SSets.m) by A1,FUNCT_1:12,A3;
assume n <= m;
then
A5: 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,A3;
hence (M*SSets).n <= (M*SSets).m by A5,A4,MEASURE1:31;
end;
then for n,m be Nat st m<=n holds (M*SSets).m<=(M*SSets).n;
hence M*SSets is non-decreasing by RINFSUP2:7;
end;
theorem Th30:
for X being set, S being SigmaField of X, M be sigma_Measure of
S, SSets being SetSequence of S st SSets is non-ascending holds M*SSets is
non-increasing
proof
let X be set;
let S be SigmaField of X;
let M be sigma_Measure of S;
let SSets be SetSequence of S;
A1: dom(M*SSets) = NAT by FUNCT_2:def 1;
assume
A2: SSets is non-ascending;
now
let n,m be Nat;
A3: n in NAT & m in NAT by ORDINAL1:def 12;
A4: (M*SSets).m = M.(SSets.m) by A1,FUNCT_1:12,A3;
assume m <= n;
then
A5: 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,A3;
hence (M*SSets).n <= (M*SSets).m by A5,A4,MEASURE1:31;
end;
hence M*SSets is non-increasing by RINFSUP2:7;
end;
theorem
for X being non empty set, S be SigmaField of X, M be sigma_Measure of
S, 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;
let S be SigmaField of X;
let M be sigma_Measure of S;
let SSets be SetSequence of S;
assume that
A1: SSets is non-ascending and
A2: M.(SSets.0) < +infty;
A3: M.(SSets.0 \ lim SSets) >= 0 by SUPINF_2:51;
now
let y be object;
assume y in rng (SSets.0 (\) SSets);
then consider x be object such that
A4: x in NAT and
A5: (SSets.0 (\) SSets).x = y by FUNCT_2:11;
reconsider x as Element of NAT by A4;
SSets.0 \ SSets.x in S;
hence y in S by A5,SETLIM_2:def 7;
end;
then rng (SSets.0 (\) SSets) c= S;
then reconsider Bseq = SSets.0 (\) SSets as SetSequence of S by
RELAT_1:def 19;
deffunc F1(Element of NAT) = (M*SSets).0;
consider seq1 be sequence of ExtREAL such that
A6: for n being Element of NAT holds seq1.n = F1(n) from FUNCT_2:sch 4;
A7: now
let k be Nat;
reconsider k1=k as Element of NAT by ORDINAL1:def 12;
A8: k is Element of NAT by ORDINAL1:def 12;
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
A9: SSets.k \/ Bseq.k = SSets.0 by SETLIM_2:def 7;
SSets.k misses SSets.0 \ SSets.k by XBOOLE_1:79;
then SSets.k misses Bseq.k by SETLIM_2:def 7;
then M.(SSets.0) = M.(SSets.k) + M.(Bseq.k) by A9,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,A8;
then seq1.k = (M*SSets).k + M.(Bseq.k) by A8,FUNCT_2:15;
hence seq1.k = (M*SSets).k + (M*Bseq).k by A8,FUNCT_2:15;
end;
M*SSets is non-increasing by A1,Th30;
then
A10: M*SSets is convergent by RINFSUP2:36;
rng Bseq c= S;
then Bseq is sequence of S by FUNCT_2:6;
then
A11: M*Bseq is nonnegative by MEASURE2:1;
A12: for n be Nat holds seq1.n = (M*SSets).0
proof
let n be Nat;
n is Element of NAT by ORDINAL1:def 12;
hence seq1.n = (M*SSets).0 by A6;
end;
A13: rng SSets c= S;
then SSets is sequence of S by FUNCT_2:6;
then
A14: M*SSets is nonnegative by MEASURE2:1;
then
A15: -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
A16: SSets.0 \/ lim SSets = SSets.0 by XBOOLE_1:12;
Intersection SSets in S by A13,PROB_1:def 6;
then
A17: lim SSets in S by A1,SETLIM_1:61;
then
A18: 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 A17,MEASURE1:30,XBOOLE_1:79;
then
A19: 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
A20: (M*SSets).0 in REAL by A15,XXREAL_0:14;
for n,m being Nat st n <= m holds Bseq.n c= Bseq.m
proof
let n,m be Nat;
assume n <= 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;
end;
then
A21: 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 A10,A11,A14,A7,MESFUNC9:11;
then
A22: (M*SSets).0 = lim(M*Bseq) + lim(M*SSets) by A20,A12,MESFUNC5:52;
lim(M*Bseq) = M.(lim Bseq) by A21,Th26
.= M.(SSets.0 \ lim SSets) by A1,SETLIM_1:64,SETLIM_2:86;
then
A23: M.(SSets.0 \ lim SSets) + M.(lim SSets) = lim(M*SSets) + M.(SSets.0 \
lim SSets) by A19,A16,A22,FUNCT_2:15;
A24: M.(SSets.0 \ lim SSets) <= M.(SSets.0) by A18,MEASURE1:31,XBOOLE_1:36;
then M.(SSets.0 \ lim SSets) < +infty by A2,XXREAL_0:2;
then
A25: M.(lim SSets) = lim(M*SSets) + M.(SSets.0 \ lim SSets) - M.(SSets.0 \
lim SSets) by A3,A23,XXREAL_3:28;
M.(SSets.0 \ lim SSets) in REAL by A2,A24,A3,XXREAL_0:14;
hence M.(lim SSets) = lim(M*SSets) by A25,XXREAL_3:22;
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;
pred M is_extension_of m means
for A be set st A in F holds M.A = m. A;
end;
theorem
for X being non empty set, F being Field_Subset of X, m being Measure
of F st (ex M be sigma_Measure of sigma F st M is_extension_of m) holds m is
completely-additive
proof
let X be non empty set, F be Field_Subset of X, m be Measure of F;
given M be sigma_Measure of sigma F such that
A1: M is_extension_of m;
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;
reconsider Bseq = Aseq as sequence of sigma F by A2,FUNCT_2:7;
reconsider Bseq as Sep_Sequence of sigma F;
A3: now
let n be object;
assume n in NAT;
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;
hence (M*Bseq).n = (m*Aseq).n by FUNCT_2:15;
end;
assume union rng Aseq in F;
then m.(union rng Aseq) = M.(union rng Aseq) by A1;
then m.(union rng Aseq) = SUM(M*Bseq) by MEASURE1:def 6;
hence thesis by A3,FUNCT_2:12;
end;
hence m is completely-additive;
end;
theorem Th33:
for X being non empty set, F being Field_Subset of X, m being
Measure of F st m is completely-additive ex M be 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, F be Field_Subset of X, m be Measure of F;
assume
A1: m is completely-additive;
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 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;
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;
end;
M.{} = (sigma_Meas(C_Meas m)).{} by FUNCT_1:49,PROB_1:4
.= 0 by VALUED_0:def 19;
then reconsider M as sigma_Measure of sigma F by A4,MEASURE1:def 6
,MESFUNC5:15,VALUED_0:def 19;
take M;
A7: F c= sigma F by PROB_1:def 9;
for A be set st A in F holds M.A = m.A
proof
let A be set;
assume
A8: A in F;
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;
end;
hence M is_extension_of m & M = (sigma_Meas(C_Meas m))|(sigma F);
end;
theorem Th34:
(for n holds M.(FSets.n) < +infty) implies M.((Partial_Union
FSets).k) < +infty
proof
defpred P[Nat] means M.((Partial_Union FSets).$1) < +infty;
assume
A1: for n holds M.(FSets.n) < +infty;
A2: now
let k be Nat;
A3: In(0,REAL) <= M.((Partial_Union FSets).k) by SUPINF_2:51;
M.(FSets.(k+1)) < +infty & In(0,REAL) <= M.(FSets.(k+1))
by A1,SUPINF_2:51;
then
A4: M.(FSets.(k+1)) in REAL by XXREAL_0:10;
assume P[k];
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 P[k+1] by A5,XXREAL_0:9,13;
end;
(Partial_Union FSets).0 = FSets.0 by PROB_3:def 2;
then
A7: P[0] by A1;
for k being Nat holds P[k] from NAT_1:sch 2(A7,A2);
hence thesis;
end;
theorem
for X being non empty set, F being Field_Subset of X, m being Measure
of F st m is completely-additive & (ex Aseq be Set_Sequence of F st (for n be
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, F be Field_Subset of X, m be Measure of F;
A1: F c= sigma F by PROB_1:def 9;
assume m is completely-additive;
then consider M1 be 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 be Set_Sequence of F st (for n be Nat holds m.(Aseq.n) <
+infty) & X = union rng Aseq;
then consider Aseq be Set_Sequence of F such that
A4: for n be Nat holds m.(Aseq.n) < +infty and
A5: X = union rng Aseq;
let M be sigma_Measure of sigma F;
reconsider Bseq = Partial_Union Aseq as Set_Sequence of F by Th15;
assume
A6: M is_extension_of m;
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;
assume
A9: B in sigma F;
A10: for seq being Covering of B,F holds M.B <= SUM vol(m,seq)
proof
let seq be Covering of B,F;
A11: for n being Element of NAT holds seq.n in sigma F by A1;
now
let y be object;
assume y in rng seq;
then consider x be object such that
A12: x in NAT and
A13: seq.x = y by FUNCT_2:11;
thus y in sigma F by A11,A12,A13;
end;
then rng seq c= sigma F;
then reconsider seq1=seq as SetSequence of sigma F by RELAT_1:def 19;
A14: rng seq1 c= sigma F;
then reconsider Fseq = seq1 as sequence of 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
A15: M.B <= M.(Union seq1) by A9,MEASURE1:31;
for n be object st n in NAT holds (M*Fseq).n = (vol(m,seq)).n
proof
let n be object;
assume
A16: n in NAT;
then reconsider n1=n as Element of NAT;
n1 in dom Fseq by A16,FUNCT_2:def 1;
then (M*Fseq).n = M.(Fseq.n1) by FUNCT_1:13
.= m.(seq.n1) by A6;
hence (M*Fseq).n = (vol(m,seq)).n by Def5;
end;
then
A17: 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 A14,MEASURE2:def 1;
then M.(union rng Fseq) <= SUM(M*Fseq) by MEASURE2:11;
then M.(Union seq1) <= SUM vol(m,seq) by A17,CARD_3:def 4;
hence M.B <= SUM vol(m,seq) by A15,XXREAL_0:2;
end;
for r be ExtReal st r in Svc(m,B) holds M.B <= r
proof
let r be ExtReal;
assume r in Svc(m,B);
then ex seq be Covering of B,F st r = SUM vol(m,seq) by Def7;
hence M.B <= r by A10;
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;
end;
A18: for B be set st (ex k be Element of NAT st B c= Bseq.k) & B in sigma F
holds M.B = M1.B
proof
let B be set;
assume ex k be Element of NAT st B c= Bseq.k;
then consider k be Element of NAT such that
A19: B c= Bseq.k;
A20: M.(Bseq.k) = m.(Bseq.k) by A6;
assume
A21: B in sigma F;
then reconsider B9 = B as Subset of X;
A22: F c= sigma F & Bseq.k in F by PROB_1:def 9;
then
A23: Bseq.k \ B is Element of sigma F by A21,PROB_1:6;
then M.(Bseq.k \ B) <= M.(Bseq.k) by A22,MEASURE1:31,XBOOLE_1:36;
then
A24: M.(Bseq.k \ B) < +infty by A4,A20,Th34,XXREAL_0:2;
M.B + M.(Bseq.k \ B) = M.(B \/ (Bseq.k \ B)) by A21,A23,MEASURE1:30
,XBOOLE_1:79;
then M.B + M.(Bseq.k \ B) = M.(Bseq.k \/ B) by XBOOLE_1:39;
then
A25: M.B + M.(Bseq.k \ B) = M.(Bseq.k) by A19,XBOOLE_1:12;
0 <= M.(Bseq.k \ B) by SUPINF_2:51;
then
A26: M.B = M.(Bseq.k) - M.(Bseq.k \ B) by A25,A24,XXREAL_3:28;
A27: M1.(Bseq.k) = m.(Bseq.k) by A2;
M1.B + M1.(Bseq.k \ B) = M1.(B \/ (Bseq.k \ B)) by A21,A23,MEASURE1:30
,XBOOLE_1:79;
then M1.B + M1.(Bseq.k \ B) = M1.(Bseq.k \/ B) by XBOOLE_1:39;
then
A28: M1.B + M1.(Bseq.k \ B) = M1.(Bseq.k) by A19,XBOOLE_1:12;
M1.(Bseq.k \ B) <= M1.(Bseq.k) by A22,A23,MEASURE1:31,XBOOLE_1:36;
then
A29: M1.(Bseq.k \ B) < +infty by A4,A27,Th34,XXREAL_0:2;
0 <= M1.(Bseq.k \ B) by SUPINF_2:51;
then
A30: M1.B = M1.(Bseq.k) - M1.(Bseq.k \ B) by A28,A29,XXREAL_3:28;
M.(Bseq.k \ B) <= M1.(Bseq.k \ B) by A8,A21,A22,PROB_1:6;
then
A31: M1.(Bseq.k) - M1.(Bseq.k \ B) <= M.(Bseq.k) - M.(Bseq.k \ B) by A27,A20,
XXREAL_3:37;
M.B9 <= M1.B9 by A8,A21;
hence M.B = M1.B by A26,A30,A31,XXREAL_0:1;
end;
for B be object st B in sigma F holds M.B = M1.B
proof
let B be object;
assume
A32: B in sigma F;
then reconsider B9 = B as Subset of X;
deffunc F1(object) = B9 /\ Bseq.$1;
A33: for n be object st n in NAT holds F1(n) in bool X;
consider Cseq be sequence of bool X such that
A34: for n be object st n in NAT holds Cseq.n = F1(n) from FUNCT_2:sch 2(
A33 );
reconsider Cseq as SetSequence of X;
for n,m be Nat st n <= m holds Cseq.n c= Cseq.m
proof
let n,m be Nat;
A35: n in NAT & m in NAT by ORDINAL1:def 12;
A36: Bseq is non-descending by PROB_3:11;
assume n <= m;
then Bseq.n c= Bseq.m by A36,PROB_1:def 5;
then B9 /\ Bseq.n c= B9 /\ Bseq.m by XBOOLE_1:26;
then Cseq.n c= B9 /\ Bseq.m by A34,A35;
hence Cseq.n c= Cseq.m by A34,A35;
end;
then
A37: Cseq is non-descending by PROB_1:def 5;
now
let y be object;
assume y in rng Cseq;
then consider x be object such that
A38: x in NAT and
A39: Cseq.x = y by FUNCT_2:11;
reconsider x as Element of NAT by A38;
Bseq.x in F;
then Bseq.x /\ B9 in sigma F by A1,A32,MEASURE1:34;
hence y in sigma F by A34,A39;
end;
then rng Cseq c= sigma F;
then reconsider Cseq as SetSequence of sigma F by RELAT_1:def 19;
for n be object st n in NAT holds (M1 * Partial_Union Cseq).n = (M *
Partial_Union Cseq).n
proof
let n be object;
assume
A40: n in NAT;
then reconsider n1 = n as Nat;
A41: now
let x be set;
assume x in (Partial_Union Cseq).n1;
then consider k be Nat such that
A42: k <= n1 and
A43: x in (Cseq qua SetSequence of X).k by PROB_3:13;
reconsider k as Element of NAT by ORDINAL1:def 12;
take k;
x in B9 /\ Bseq.k by A34,A43;
hence k <= n1 & x in Bseq.k by A42,XBOOLE_0:def 4;
end;
A44: (Partial_Union Cseq).n1 c= Bseq.n1
proof
let x be object;
assume x in (Partial_Union Cseq).n1;
then consider k be 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;
end;
A47: (M1 * Partial_Union Cseq).n = M1.((Partial_Union Cseq).n1)
by FUNCT_2:15,A40;
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,A40;
then (M1 * Partial_Union Cseq).n = M.((Partial_Union Cseq).n1)
by A47,A18,A44,A48,A40;
hence (M1 * Partial_Union Cseq).n = (M * Partial_Union Cseq).n by
FUNCT_2:15,A40;
end;
then
A49: M1 * Partial_Union Cseq = M * Partial_Union Cseq by FUNCT_2:12;
for n be Nat holds Cseq.n = B9 /\ Bseq.n
by ORDINAL1:def 12,A34;
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 A37,SETLIM_1:63;
then M1.B = lim(M1 * Cseq) by A37,Th26;
then M1.B = lim(M * Partial_Union Cseq) by A37,A49,PROB_4:19;
then M1.B = lim(M * Cseq) by A37,PROB_4:19;
then M1.B = M.(lim Cseq) by A37,Th26;
hence M1.B = M.B by A37,A50,SETLIM_1:63;
end;
hence thesis by A3,FUNCT_2:12;
end;