:: Completeness of the $\sigma$-Additive Measure. Measure Theory :: by J\'ozef Bia{\l}as :: :: Received February 22, 1992 :: Copyright (c) 1992-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 FUNCT_1, NUMBERS, SUBSET_1, SUPINF_2, XXREAL_0, RELAT_1, SUPINF_1, ORDINAL2, PROB_1, MEASURE2, MEASURE1, TARSKI, SETFAM_1, CARD_1, XBOOLE_0, ARYTM_3, NAT_1, ARYTM_1, REAL_1, XXREAL_2, ZFMISC_1, MEASURE3, FUNCT_7, REWRITE1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, NAT_1, SETFAM_1, PROB_1, XXREAL_2, SUPINF_1, SUPINF_2, MEASURE1, MEASURE2; constructors PARTFUN1, REAL_1, NAT_1, PROB_2, MEASURE1, MEASURE2, SUPINF_1, RELSET_1, XREAL_0; registrations SUBSET_1, ORDINAL1, FUNCT_2, NUMBERS, XREAL_0, MEMBERED, MEASURE1, VALUED_0, XXREAL_3, RELSET_1; requirements NUMERALS, SUBSET, BOOLE, ARITHM; begin :: :: Some additional properties about R_eal numbers :: reserve X for set; theorem :: MEASURE3:1 for F1,F2 being sequence of ExtREAL st (for n being Element of NAT holds Ser(F1).n <= Ser(F2).n) holds SUM(F1) <= SUM(F2); theorem :: MEASURE3:2 for F1,F2 being sequence of ExtREAL st (for n being Element of NAT holds Ser(F1).n = Ser(F2).n) holds SUM(F1) = SUM(F2); :: :: Some additional theorems about measures and functions :: definition let X be set; let S be SigmaField of X; let F be sequence of S; redefine func rng F -> N_Measure_fam of S; end; theorem :: MEASURE3:3 for S being SigmaField of X, M being sigma_Measure of S, F being sequence of S, A being Element of S st meet rng F c= A & (for n being Element of NAT holds A c= F.n) holds M.A = M.(meet rng F); theorem :: MEASURE3:4 for S being SigmaField of X, G,F being sequence of S st (G.0 = {} & for n being Nat holds G.(n+1) = F.0 \ F.n & F.(n+1) c= F.n ) holds union rng G = F.0 \ meet rng F; theorem :: MEASURE3:5 for S being SigmaField of X, G,F being sequence of S st (G.0 = {} & for n being Nat holds G.(n+1) = F.0 \ F.n & F.(n+1) c= F.n ) holds meet rng F = F.0 \ union rng G; theorem :: MEASURE3:6 for S being SigmaField of X, M being sigma_Measure of S, G,F being sequence of S st (M.(F.0) <+infty & G.0 = {} & for n being Nat holds G.(n+1) = F.0 \ F.n & F.(n+1) c= F.n ) holds M.(meet rng F) = M.(F.0) - M.(union rng G); theorem :: MEASURE3:7 for S being SigmaField of X, M being sigma_Measure of S, G,F being sequence of S st (M.(F.0) <+infty & G.0 = {} & for n being Nat holds G.(n+1) = F.0 \ F.n & F.(n+1) c= F.n ) holds M.(union rng G) = M.(F.0 ) - M.(meet rng F); theorem :: MEASURE3:8 for S being SigmaField of X, M being sigma_Measure of S, G,F being sequence of S st (M.(F.0) <+infty & G.0 = {} & for n being Nat holds G.(n+1) = F.0 \ F.n & F.(n+1) c= F.n ) holds M.(meet rng F) = M.(F.0) - sup(rng (M*G)); theorem :: MEASURE3:9 for S being SigmaField of X, M being sigma_Measure of S, G,F being sequence of S st (M.(F.0) <+infty & G.0 = {} & for n being Nat holds G.(n+1) = F.0 \ F.n & F.(n+1) c= F.n ) holds M.(F.0) in REAL & inf(rng (M*F)) in REAL & sup(rng (M*G)) in REAL; theorem :: MEASURE3:10 for S being SigmaField of X, M being sigma_Measure of S, G,F being sequence of S st (M.(F.0) <+infty & G.0 = {} & for n being Nat holds G.(n+1) = F.0 \ F.n & F.(n+1) c= F.n ) holds sup rng (M*G) = M.(F.0) - inf rng (M*F); theorem :: MEASURE3:11 for S being SigmaField of X, M being sigma_Measure of S, G,F being sequence of S st (M.(F.0) <+infty & G.0 = {} & for n being Nat holds G.(n+1) = F.0 \ F.n & F.(n+1) c= F.n ) holds inf(rng (M*F)) = M.(F.0) - sup(rng (M*G)); theorem :: MEASURE3:12 for S being SigmaField of X, M being sigma_Measure of S, F being sequence of S st (for n being Nat holds F.(n+1) c= F.n) & M.(F.0 ) <+infty holds M.(meet rng F) = inf(rng (M*F)); theorem :: MEASURE3:13 for S being SigmaField of X, M being Measure of S, F being Sep_Sequence of S holds SUM(M*F) <= M.(union rng F); theorem :: MEASURE3:14 for S being SigmaField of X, M being Measure of S st (for F being Sep_Sequence of S holds M.(union rng F) <= SUM(M*F)) holds M is sigma_Measure of S; :: :: Completeness of sigma_additive Measure :: definition let X be set; let Sigma be SigmaField of X; let M be sigma_Measure of Sigma; attr M is complete means :: MEASURE3:def 1 for A being Subset of X, B being set st B in Sigma & A c= B & M.B = 0. holds A in Sigma; end; definition let X be set; let S be SigmaField of X; let M be sigma_Measure of S; mode thin of M -> Subset of X means :: MEASURE3:def 2 ex B being set st B in S & it c= B & M.B = 0.; end; definition let X be set; let S be SigmaField of X; let M be sigma_Measure of S; func COM(S,M) -> non empty Subset-Family of X means :: MEASURE3:def 3 for A being set holds (A in it iff ex B being set st B in S & ex C being thin of M st A = B \/ C ); end; definition let X be set; let S be SigmaField of X; let M be sigma_Measure of S; let A be Element of COM(S,M); func MeasPart(A) -> non empty Subset-Family of X means :: MEASURE3:def 4 for B being set holds (B in it iff B in S & B c= A & A \ B is thin of M ); end; theorem :: MEASURE3:15 for S being SigmaField of X, M being sigma_Measure of S, F being sequence of COM(S,M) holds ex G being sequence of S st for n being Element of NAT holds G.n in MeasPart(F.n); theorem :: MEASURE3:16 for S being SigmaField of X, M being sigma_Measure of S, F being sequence of COM(S,M), G being sequence of S ex H being sequence of bool X st for n being Element of NAT holds H.n = F.n \ G.n; theorem :: MEASURE3:17 for S being SigmaField of X, M being sigma_Measure of S, F being sequence of bool X st (for n being Element of NAT holds F.n is thin of M) holds ex G being sequence of S st for n being Element of NAT holds F.n c= G .n & M.(G.n) = 0.; theorem :: MEASURE3:18 for S being SigmaField of X, M being sigma_Measure of S, D being non empty Subset-Family of X st (for A being set holds (A in D iff ex B being set st B in S & ex C being thin of M st A = B \/ C)) holds D is SigmaField of X ; registration let X be set; let S be SigmaField of X; let M be sigma_Measure of S; cluster COM(S,M) -> sigma-additive compl-closed non empty; end; theorem :: MEASURE3:19 for S being SigmaField of X, M being sigma_Measure of S, B1,B2 being set st B1 in S & B2 in S holds for C1,C2 being thin of M holds B1 \/ C1 = B2 \/ C2 implies M.B1 = M.B2; definition let X be set; let S be SigmaField of X; let M be sigma_Measure of S; func COM(M) -> sigma_Measure of COM(S,M) means :: MEASURE3:def 5 for B being set st B in S for C being thin of M holds it.(B \/ C) = M.B; end; theorem :: MEASURE3:20 for S being SigmaField of X, M being sigma_Measure of S holds COM(M) is complete;