:: The Hopf Extension Theorem of Measure
:: by Noboru Endou , Hiroyuki Okazaki and Yasunari Shidama
::
:: Received April 7, 2009
:: Copyright (c) 2009-2016 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;
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 :: MEASURE8:1
Ser seq = Partial_Sums seq;
:: In the theorem below, the notion "summable" means in MESFUNC9, not in SUPINF_2
theorem :: MEASURE8:2
seq is nonnegative implies seq is summable & SUM seq = Sum seq;
theorem :: MEASURE8:3 :: 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;
registration
let X,F;
cluster disjoint_valued for sequence of F;
end;
definition
let X,F;
mode FinSequence of F -> FinSequence of bool X means
:: MEASURE8:def 1
for k being Nat st k in dom it holds it.k in F;
end;
registration
let X,F;
cluster disjoint_valued for FinSequence of F;
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
:: MEASURE8:def 2
for n be Nat holds it.n in F;
end;
definition
let X,A,F;
mode Covering of A,F -> Set_Sequence of F means
:: MEASURE8:def 3
A c= union rng it;
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;
end;
definition
let X,F,Sets;
mode Covering of Sets,F -> sequence of Funcs(NAT,bool X) means
:: MEASURE8:def 4
for n being Nat holds it.n is Covering of Sets.n,F;
end;
reserve Cvr for Covering of Sets,F;
definition
let X,F,M,FSets;
func vol(M,FSets) -> ExtREAL_sequence means
:: MEASURE8:def 5
for n holds it.n = M.( FSets.n);
end;
theorem :: MEASURE8:4
vol(M,FSets) is nonnegative;
definition
let X,F,Sets,Cvr,n;
redefine func Cvr.n -> Covering of Sets.n,F;
end;
definition
let X,F,Sets,M,Cvr;
func Volume(M,Cvr) -> ExtREAL_sequence means
:: MEASURE8:def 6
for n being Nat holds it .n = SUM(vol(M,Cvr.n));
end;
theorem :: MEASURE8:5
0 <= (Volume(M,Cvr)).n;
definition
let X,F,M,A;
func Svc(M,A) -> Subset of ExtREAL means
:: 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);
end;
registration
let X,A,F,M;
cluster Svc(M,A) -> non empty;
end;
definition
let X,F,M;
func C_Meas M -> Function of bool X,ExtREAL means
:: MEASURE8:def 8
for A being Subset of X holds it.A = inf(Svc(M,A));
end;
definition
func InvPairFunc -> sequence of [:NAT,NAT:] equals
:: MEASURE8:def 9
PairFunc";
end;
definition
let X,F,Sets,Cvr;
func On Cvr -> Covering of union rng Sets,F means
:: MEASURE8:def 10
for n being Nat holds it.n = (Cvr.(pr1 InvPairFunc.n)).(pr2 InvPairFunc.n);
end;
theorem :: MEASURE8:6
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;
theorem :: MEASURE8:7
inf Svc(M,union rng Sets) <= SUM Volume(M,Cvr);
theorem :: MEASURE8:8
A in F implies (A,{}X) followed_by {}X is Covering of A,F;
theorem :: MEASURE8:9
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;
theorem :: MEASURE8:10
C_Meas M is nonnegative;
theorem :: MEASURE8:11
(C_Meas M).{} = 0;
theorem :: MEASURE8:12
A c= B implies (C_Meas M).A <= (C_Meas M).B;
theorem :: MEASURE8:13
(C_Meas M).(union rng Sets) <= SUM((C_Meas M)*Sets);
theorem :: MEASURE8:14
C_Meas M is C_Measure of X;
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;
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
:: 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;
theorem :: MEASURE8:15
Partial_Union FSets is Set_Sequence of F;
theorem :: MEASURE8:16
Partial_Diff_Union FSets is Set_Sequence of F;
theorem :: MEASURE8:17
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;
theorem :: MEASURE8:18
M is completely-additive implies for A be set st A in F holds M.
A = (C_Meas M).A;
reserve C for C_Measure of X;
theorem :: MEASURE8:19
(for B being Subset of X holds C.(B /\ A) + C.(B /\ (X \ A)) <=
C.B) implies A in sigma_Field C;
theorem :: MEASURE8:20
F c= sigma_Field C_Meas M;
theorem :: MEASURE8:21
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;
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;
end;
theorem :: MEASURE8:22
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;
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;
end;
theorem :: MEASURE8:23
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;
theorem :: MEASURE8:24
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);
theorem :: MEASURE8:25
for X,C for seq being SetSequence of sigma_Field C holds Union seq in
sigma_Field C;
theorem :: MEASURE8:26
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);
theorem :: MEASURE8:27
FSets is non-descending implies M*FSets is non-decreasing;
theorem :: MEASURE8:28
FSets is non-ascending implies M*FSets is non-increasing;
theorem :: MEASURE8:29
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;
theorem :: MEASURE8:30
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;
theorem :: MEASURE8:31
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);
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
:: MEASURE8:def 12
for A be set st A in F holds M.A = m. A;
end;
theorem :: MEASURE8:32
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;
theorem :: MEASURE8:33
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);
theorem :: MEASURE8:34
(for n holds M.(FSets.n) < +infty) implies M.((Partial_Union
FSets).k) < +infty;
theorem :: MEASURE8:35
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);