:: Completeness of the $\sigma$-Additive Measure. Measure Theory
:: by J\'ozef Bia{\l}as
::
:: Received February 22, 1992
:: Copyright (c) 1992-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 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;
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
::
notation
let X be set;
let S be SigmaField of X;
synonym N_Sub_fam of S for N_Measure_fam of S;
end;
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 S be SigmaField of X;
let M be sigma_Measure of S;
pred M is_complete S means
:: MEASURE3:def 1
for A being Subset of X, B being set st B
in S & A c= B & M.B = 0. holds A in S;
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 COM(S,M);