:: The $\sigma$-additive Measure Theory :: by J\'ozef Bia{\l}as :: :: Received October 15, 1990 :: Copyright (c) 1990-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, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ZFMISC_1, PROB_1, FINSUB_1, FUNCT_1, SUPINF_2, XXREAL_0, MSSUBFAM, ARYTM_3, VALUED_0, FUNCOP_1, ARYTM_1, RELAT_1, CARD_3, CARD_1, NAT_1, EQREL_1, PROB_2, SUPINF_1, MEASURE1, FUNCT_7; notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, RELAT_1, FINSUB_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, NAT_1, SETFAM_1, FUNCOP_1, PROB_1, PROB_2, VALUED_0, FUNCT_7, SUPINF_1, SUPINF_2; constructors ENUMSET1, PARTFUN1, FUNCOP_1, FINSUB_1, REAL_1, NAT_1, PROB_2, SUPINF_2, SUPINF_1, RELSET_1, FUNCT_7; registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, PROB_1, VALUED_0, FINSUB_1, RELAT_1, XXREAL_0; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; begin :: Some useful theorems about sets and R_eal numbers reserve X for set; theorem :: MEASURE1:1 for X,Y being set holds union {X,Y,{}} = union {X,Y}; theorem :: MEASURE1:2 for A,B being Subset of X holds {A,B} is Subset-Family of X; theorem :: MEASURE1:3 for A,B,C being Subset of X holds {A,B,C} is Subset-Family of X; scheme :: MEASURE1:sch 1 DomsetFamEx {A() -> set,P[set]}: ex F being non empty Subset-Family of A() st for B being set holds B in F iff B c= A() & P[B] provided ex B being set st B c= A() & P[B]; notation let X be set; let S be non empty Subset-Family of X; synonym X\S for COMPLEMENT S; end; registration let X be set; let S be non empty Subset-Family of X; cluster X\S -> non empty; end; theorem :: MEASURE1:4 for S being non empty Subset-Family of X holds meet S = X \ union (X \ S) & union S = X \ meet (X \ S); :: :: Field Subset of X and nonnegative measure :: definition let X be set; let IT be Subset-Family of X; redefine attr IT is compl-closed means :: MEASURE1:def 1 for A being set holds A in IT implies X\A in IT; end; registration let X be set; cluster cup-closed compl-closed -> cap-closed for Subset-Family of X; cluster cap-closed compl-closed -> cup-closed for Subset-Family of X; end; theorem :: MEASURE1:5 for S being Field_Subset of X holds S = X \ S; registration let X; cluster compl-closed cap-closed -> diff-closed for Subset-Family of X; end; theorem :: MEASURE1:6 for S being Field_Subset of X holds for A,B being set st A in S & B in S holds A \ B in S; theorem :: MEASURE1:7 for S being Field_Subset of X holds {} in S & X in S; definition let X be non empty set, F be Function of X,ExtREAL; redefine attr F is nonnegative means :: MEASURE1:def 2 for A being Element of X holds 0. <= F.A; end; definition let X be set, S be non empty Subset-Family of X; let F be Function of S,ExtREAL; attr F is additive means :: MEASURE1:def 3 for A,B being Element of S st A misses B & A \/ B in S holds F.(A \/ B) = F.A + F.B; end; registration let X be set, S be Field_Subset of X; cluster nonnegative additive zeroed for Function of S,ExtREAL; end; definition let X be set, S be Field_Subset of X; mode Measure of S is nonnegative additive zeroed Function of S,ExtREAL; end; theorem :: MEASURE1:8 for S being Field_Subset of X, M being Measure of S, A,B being Element of S st A c= B holds M.A <= M.B; theorem :: MEASURE1:9 for S being Field_Subset of X, M being Measure of S, A,B being Element of S st A c= B & M.A < +infty holds M.(B \ A) = M.B - M.A; registration let X be set; cluster non empty compl-closed cap-closed for Subset-Family of X; end; definition let X be set, S be non empty cup-closed Subset-Family of X, A,B be Element of S; redefine func A \/ B -> Element of S; end; definition let X be set, S be Field_Subset of X, A,B be Element of S; redefine func A /\ B -> Element of S; redefine func A \ B -> Element of S; end; theorem :: MEASURE1:10 for S being Field_Subset of X, M being Measure of S, A,B being Element of S holds M.(A \/ B) <= M.A + M.B; theorem :: MEASURE1:11 for S being Field_Subset of X, M being Measure of S holds {} in S & X in S & for A,B being set st A in S & B in S holds X \ A in S & A \/ B in S & A /\ B in S; definition let X be set, S be Field_Subset of X, M be Measure of S; mode measure_zero of M -> Element of S means :: MEASURE1:def 4 M.it = 0.; end; theorem :: MEASURE1:12 for S being Field_Subset of X, M being Measure of S, A being Element of S, B being measure_zero of M st A c= B holds A is measure_zero of M; theorem :: MEASURE1:13 for S being Field_Subset of X, M being Measure of S, A,B being measure_zero of M holds A \/ B is measure_zero of M & A /\ B is measure_zero of M & A \ B is measure_zero of M; theorem :: MEASURE1:14 for S being Field_Subset of X, M being Measure of S, A being Element of S, B being measure_zero of M holds M.(A \/ B) = M.A & M.(A /\ B) = 0.& M.(A \ B) = M.A; :: :: sigma_Field Subset of X and sigma_additive nonnegative measure :: theorem :: MEASURE1:15 for A being Subset of X ex F being sequence of bool X st rng F = {A}; theorem :: MEASURE1:16 for A being set ex F being sequence of {A} st for n being Element of NAT holds F.n = A; registration let X be set; cluster non empty countable for Subset-Family of X; end; definition let X be set; mode N_Sub_set_fam of X is non empty countable Subset-Family of X; end; theorem :: MEASURE1:17 for A,B,C being Subset of X ex F being sequence of bool X st rng F = {A,B,C} & F.0 = A & F.1 = B & for n being Element of NAT st 1 < n holds F.n = C; theorem :: MEASURE1:18 for A,B being Subset of X holds {A,B,{}} is N_Sub_set_fam of X; theorem :: MEASURE1:19 for A,B being Subset of X ex F being sequence of bool X st rng F = {A,B} & F.0 = A & for n being Nat st 0 < n holds F.n = B; theorem :: MEASURE1:20 for A,B being Subset of X holds {A,B} is N_Sub_set_fam of X; theorem :: MEASURE1:21 for S being N_Sub_set_fam of X holds X \ S is N_Sub_set_fam of X; definition let X be set; let IT be Subset-Family of X; attr IT is sigma-additive means :: MEASURE1:def 5 for M being N_Sub_set_fam of X st M c= IT holds union M in IT; end; registration let X be set; cluster non empty compl-closed sigma-additive for Subset-Family of X; end; registration let X; cluster compl-closed sigma-multiplicative -> sigma-additive for Subset-Family of X; cluster compl-closed sigma-additive -> sigma-multiplicative for Subset-Family of X; end; registration let X be set; cluster -> non empty for SigmaField of X; end; theorem :: MEASURE1:22 for S being non empty Subset-Family of X holds (for A being set holds A in S implies X\A in S) & (for M being N_Sub_set_fam of X st M c= S holds meet M in S) iff S is SigmaField of X; registration let X be set; let S be SigmaField of X; cluster disjoint_valued for sequence of S; end; definition let X be set; let S be SigmaField of X; mode Sep_Sequence of S is disjoint_valued sequence of S; end; definition let X be set; let S be SigmaField of X; let F be sequence of S; redefine func rng F -> non empty Subset-Family of X; end; theorem :: MEASURE1:23 for S being SigmaField of X, F being sequence of S holds rng F is N_Sub_set_fam of X; theorem :: MEASURE1:24 for S being SigmaField of X, F being sequence of S holds union rng F is Element of S; theorem :: MEASURE1:25 for Y,S being non empty set, F being Function of Y,S, M being Function of S,ExtREAL st M is nonnegative holds M*F is nonnegative; theorem :: MEASURE1:26 for S being SigmaField of X, a,b being R_eal holds ex M being Function of S,ExtREAL st for A being Element of S holds (A = {} implies M.A = a ) & (A <> {} implies M.A = b); theorem :: MEASURE1:27 for S being SigmaField of X ex M being Function of S,ExtREAL st for A being Element of S holds (A = {} implies M.A = 0.) & (A <> {} implies M.A = +infty); theorem :: MEASURE1:28 for S being SigmaField of X ex M being Function of S,ExtREAL st for A being Element of S holds M.A = 0.; definition let X be set; let S be SigmaField of X; let F be Function of S,ExtREAL; attr F is sigma-additive means :: MEASURE1:def 6 for s being Sep_Sequence of S holds SUM(F*s) = F.(union rng s); end; registration let X be set; let S be SigmaField of X; cluster nonnegative sigma-additive zeroed for Function of S,ExtREAL; end; definition let X be set; let S be SigmaField of X; mode sigma_Measure of S is nonnegative sigma-additive zeroed Function of S, ExtREAL; end; registration let X be set; cluster sigma-additive compl-closed -> cup-closed for non empty Subset-Family of X; end; registration let X be set, S be SigmaField of X; cluster sigma-additive -> additive for nonnegative zeroed Function of S, ExtREAL; end; theorem :: MEASURE1:29 for S being SigmaField of X, M being sigma_Measure of S holds M is Measure of S; theorem :: MEASURE1:30 for S being SigmaField of X, M being sigma_Measure of S, A,B being Element of S st A misses B holds M.(A \/ B) = M.A + M.B; theorem :: MEASURE1:31 for S being SigmaField of X, M being sigma_Measure of S, A,B being Element of S st A c= B holds M.A <= M.B; theorem :: MEASURE1:32 for S being SigmaField of X, M being sigma_Measure of S, A,B being Element of S st A c= B & M.A < +infty holds M.(B \ A) = M.B - M.A; theorem :: MEASURE1:33 for S being SigmaField of X, M being sigma_Measure of S, A,B being Element of S holds M.(A \/ B) <= M.A + M.B; theorem :: MEASURE1:34 for S being SigmaField of X, M being sigma_Measure of S holds {} in S & X in S & for A,B being set st A in S & B in S holds X \ A in S & A \/ B in S & A /\ B in S; theorem :: MEASURE1:35 for S being SigmaField of X, M being sigma_Measure of S, T being N_Sub_set_fam of X st (for A being set st A in T holds A in S) holds union T in S & meet T in S; definition let X be set, S be SigmaField of X, M be sigma_Measure of S; mode measure_zero of M -> Element of S means :: MEASURE1:def 7 M.it = 0.; end; theorem :: MEASURE1:36 for S being SigmaField of X, M being sigma_Measure of S, A being Element of S, B being measure_zero of M st A c= B holds A is measure_zero of M; theorem :: MEASURE1:37 for S being SigmaField of X, M being sigma_Measure of S, A,B being measure_zero of M holds A \/ B is measure_zero of M & A /\ B is measure_zero of M & A \ B is measure_zero of M; theorem :: MEASURE1:38 for S being SigmaField of X, M being sigma_Measure of S, A being Element of S, B being measure_zero of M holds M.(A \/ B) = M.A & M.(A /\ B) = 0.& M.(A \ B) = M.A; definition let X be set, S be Field_Subset of X; let F be Function of S,ExtREAL; redefine attr F is additive means :: MEASURE1:def 8 for A,B being Element of S st A misses B holds F.(A \/ B) = F.A + F.B; end;