:: 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;