:: The Hopf Extension Theorem of Measure :: by Noboru Endou , Hiroyuki Okazaki and Yasunari Shidama :: :: Received April 7, 2009 :: Copyright (c) 2009-2021 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);