:: The $\sigma$-additive Measure Theory
:: by J\'ozef Bia{\l}as
::
:: Received October 15, 1990
:: Copyright (c) 1990-2026 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,
XXREAL_3, 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;
definitions SUPINF_2, TARSKI, FINSUB_1, PROB_2, PROB_1, XBOOLE_0;
equalities PROB_1, SUBSET_1, XXREAL_3;
expansions TARSKI, FINSUB_1, PROB_1, XBOOLE_0;
theorems TARSKI, FUNCT_1, FUNCT_2, ENUMSET1, ZFMISC_1, NAT_1, SETFAM_1,
SUPINF_2, RELAT_1, FUNCOP_1, FINSUB_1, PROB_2, PROB_1, SUBSET_1,
XBOOLE_0, XBOOLE_1, XXREAL_0, CARD_3, ORDINAL1, VALUED_0, XXREAL_3,
FUNCT_7;
schemes FUNCT_2, XFAMILY;
begin :: Some useful theorems about sets and R_eal numbers
reserve X for set;
theorem Th1:
for X,Y being set holds union {X,Y,{}} = union {X,Y}
proof
let X,Y be set;
thus union {X,Y,{}} = union ({X,Y} \/ {{}}) by ENUMSET1:3
.= union {X,Y} \/ union {{}} by ZFMISC_1:78
.= union {X,Y} \/ {} by ZFMISC_1:25
.= union {X,Y};
end;
theorem
for A,B being Subset of X holds {A,B} is Subset-Family of X
proof
let A,B be Subset of X;
set C = {A,B};
C c= bool X
proof
let x be object;
assume x in C;
then x = A or x = B by TARSKI:def 2;
hence thesis;
end;
hence thesis;
end;
theorem
for A,B,C being Subset of X holds {A,B,C} is Subset-Family of X
proof
let A,B,C be Subset of X;
set D = {A,B,C};
D c= bool X
proof
let x be object;
assume x in D;
then x = A or x = B or x = C by ENUMSET1:def 1;
hence thesis;
end;
hence thesis;
end;
scheme
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
A1: ex B being set st B c= A() & P[B]
proof
defpred X[set] means ex Z being set st $1 = Z & P[Z];
consider X being set such that
A2: for x being set holds x in X iff x in bool A() & X[x] from XFAMILY:
sch 1;
X c= bool A()
by A2;
then reconsider X as non empty Subset-Family of A() by A1,A2;
take X;
for B being set holds B in X iff B c= A() & P[B]
proof
let B be set;
thus B in X implies B c= A() & P[B]
proof
assume
A3: B in X;
then ex Z being set st B = Z & P[Z] by A2;
hence thesis by A3;
end;
assume B c= A() & P[B];
hence thesis by A2;
end;
hence thesis;
end;
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;
coherence
proof
consider x being Subset of X such that
A1: x in S by SUBSET_1:4;
x`` in S by A1;
hence thesis by SETFAM_1:def 7;
end;
end;
theorem Th4:
for S being non empty Subset-Family of X holds
meet S = X \ union (X \ S) & union S = X \ meet (X \ S)
proof
let S be non empty Subset-Family of X;
A1: X \ union (X \ S) c= meet S
proof
let x be object;
assume
A2: x in X \ union (X \ S);
then
A3: not x in union (X \ S) by XBOOLE_0:def 5;
for Y being set st Y in S holds x in Y
proof
let Y be set;
assume that
A4: Y in S and
A5: not x in Y;
reconsider Y as Subset of X by A4;
Y`` in S by A4;
then
A6: Y` in X \ S by SETFAM_1:def 7;
x in Y` by A2,A5,SUBSET_1:29;
hence contradiction by A3,A6,TARSKI:def 4;
end;
hence thesis by SETFAM_1:def 1;
end;
meet S c= X \ union (X \ S)
proof
let x be object;
assume
A7: x in meet S;
not x in union (X \ S)
proof
assume x in union (X \ S);
then consider Z being set such that
A8: x in Z and
A9: Z in X \ S by TARSKI:def 4;
reconsider Z as Subset of X by A9;
Z` in S & not x in Z` by A8,A9,SETFAM_1:def 7,XBOOLE_0:def 5;
hence thesis by A7,SETFAM_1:def 1;
end;
hence thesis by A7,XBOOLE_0:def 5;
end;
hence meet S = X \ union (X \ S) by A1;
thus union S c= X \ meet (X \ S)
proof
let x be object;
assume x in union S;
then consider Y being set such that
A10: x in Y and
A11: Y in S by TARSKI:def 4;
reconsider Y as Subset of X by A11;
not x in meet (X \ S)
proof
Y`` in S by A11;
then
A12: Y` in X \ S by SETFAM_1:def 7;
assume
A13: x in meet (X \ S);
not x in Y` by A10,XBOOLE_0:def 5;
hence thesis by A13,A12,SETFAM_1:def 1;
end;
hence thesis by A10,A11,XBOOLE_0:def 5;
end;
let x be object;
assume
A14: x in X \ meet (X \ S);
then not x in meet (X \ S) by XBOOLE_0:def 5;
then consider Z being set such that
A15: Z in X \ S and
A16: not x in Z by SETFAM_1:def 1;
reconsider Z as Subset of X by A15;
A17: Z` in S by A15,SETFAM_1:def 7;
x in Z` by A14,A16,SUBSET_1:29;
hence thesis by A17,TARSKI:def 4;
end;
::
:: 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 :Def1: :: redefines compl-closed (PROB_1, definition)
for A being set holds A in IT implies X\A in IT;
compatibility
proof
hereby
assume
A1: IT is compl-closed;
let A be set;
assume
A2: A in IT;
then reconsider A9 = A as Subset of X;
A9` in IT by A1,A2;
hence X\A in IT;
end;
assume
A3: for A being set holds A in IT implies X\A in IT;
let A be Subset of X;
assume A in IT;
hence thesis by A3;
end;
end;
registration
let X be set;
cluster cup-closed compl-closed -> cap-closed for Subset-Family of X;
coherence
proof
let S be Subset-Family of X;
assume
A1: S is cup-closed compl-closed;
let A,B be set;
assume that
A2: A in S and
A3: B in S;
X \ A in S & X \ B in S by A1,A2,A3;
then
A4: (X \ A) \/ (X \ B) in S by A1;
A /\ B c= A by XBOOLE_1:17;
then A /\ B = X /\ (A /\ B) by A2,XBOOLE_1:1,28
.= X \ (X \ (A /\ B)) by XBOOLE_1:48
.= X \ ((X \ A) \/ (X \ B)) by XBOOLE_1:54;
hence thesis by A1,A4;
end;
cluster cap-closed compl-closed -> cup-closed for Subset-Family of X;
coherence
proof
let S be Subset-Family of X;
assume
A5: S is cap-closed compl-closed;
let A,B be set;
assume
A6: A in S & B in S;
then X \ A in S & X \ B in S by A5;
then
A7: (X \ A) /\ (X \ B) in S by A5;
A \/ B = X /\ (A \/ B) by A6,XBOOLE_1:8,28
.= X \ (X \ (A \/ B)) by XBOOLE_1:48
.= X \ ((X \ A) /\ (X \ B)) by XBOOLE_1:53;
hence thesis by A5,A7;
end;
end;
theorem
for S being Field_Subset of X holds S = X \ S
proof
let S be Field_Subset of X;
for A being object holds A in S iff A in X \ S
proof
let A be object;
hereby
assume
A1: A in S;
then reconsider B = A as Subset of X;
B` in S by A1,PROB_1:def 1;
hence A in X \ S by SETFAM_1:def 7;
end;
assume
A2: A in X \ S;
then reconsider B = A as Subset of X;
B` in S by A2,SETFAM_1:def 7;
then B`` in S by PROB_1:def 1;
hence thesis;
end;
hence thesis by TARSKI:2;
end;
registration let X;
cluster compl-closed cap-closed -> diff-closed for Subset-Family of X;
coherence
proof
let S be Subset-Family of X such that
A1: S is compl-closed and
A2: S is cap-closed;
let A,B be set;
assume that
A3: A in S and
A4: B in S;
A5: A /\ (X \ B) = (A /\ X) \ B by XBOOLE_1:49
.= A \ B by A3,XBOOLE_1:28;
X \ B in S by A4,A1;
hence thesis by A3,A5,A2;
end;
end;
theorem
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 by FINSUB_1:def 3;
theorem
for S being Field_Subset of X holds {} in S & X in S by PROB_1:4,5;
definition
let X be non empty set, F be Function of X,ExtREAL;
redefine attr F is nonnegative means :Def2: :: redefines nonnegative (SUPINF_2, definition)
for A being Element of X holds 0. <= F.A;
compatibility by SUPINF_2:39;
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 :Def3:
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;
existence
proof
reconsider M = S --> 0. as Function of S,ExtREAL;
A1: for A,B being Element of S st A misses B holds M.(A \/ B) = M.A + M.B
proof
let A,B be Element of S;
assume A misses B;
A2: M.A = 0. & M.B = 0. by FUNCOP_1:7;
reconsider A,B as set;
reconsider A,B as Element of S;
0.= M.A + M.B by A2,XXREAL_3:4;
hence thesis by FUNCOP_1:7;
end;
take M;
( for x being Element of S holds 0.<= M.x)& M.{} = 0. by FUNCOP_1:7
,PROB_1:4;
hence thesis by A1,VALUED_0:def 19;
end;
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 Th8:
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
proof
let S be Field_Subset of X, M be Measure of S, A,B be Element of S;
reconsider C = B \ A as Element of S;
A1: 0.<= M.C by Def2;
A misses C by XBOOLE_1:79;
then
A2: M.(A \/ C) = M.A + M.C by Def3;
assume A c= B;
then M.B = M.A + M.C by A2,XBOOLE_1:45;
hence thesis by A1,XXREAL_3:39;
end;
theorem Th9:
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
proof
let S be Field_Subset of X, M be Measure of S, A,B be Element of S;
set C = B \ A;
assume that
A1: A c= B and
A2: M.A < +infty;
A3: 0.<= M.A by Def2;
A misses C by XBOOLE_1:79;
then M.(A \/ C) = M.A + M.C by Def3;
then M.B = M.A + M.C by A1,XBOOLE_1:45;
hence thesis by A2,A3,XXREAL_3:28;
end;
registration
let X be set;
cluster non empty compl-closed cap-closed for Subset-Family of X;
existence
proof
take the non empty compl-closed cap-closed Subset-Family of X;
thus thesis;
end;
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; :: redefines \/ (XBOOLE_0, definition)
coherence by FINSUB_1:def 1;
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; :: redefines /\ (XBOOLE_0, definition)
coherence by FINSUB_1:def 2;
redefine func A \ B -> Element of S; :: redefines \ (XBOOLE_0, definition)
coherence by FINSUB_1:def 3;
end;
theorem Th10:
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
proof
let S be Field_Subset of X, M be Measure of S, A,B be Element of S;
set C = B \ A;
A1: A misses C by XBOOLE_1:79;
A2: M.C <= M.B by Th8,XBOOLE_1:36;
M.(A \/ B) = M.(A \/ C) by XBOOLE_1:39
.= M.A + M.C by A1,Def3;
hence thesis by A2,XXREAL_3:36;
end;
theorem
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 by Def1,FINSUB_1:def 1,def 2,PROB_1:4,5;
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
:Def4:
M.it = 0.;
existence
proof
reconsider A = {} as Element of S by PROB_1:4;
take A;
thus thesis by VALUED_0:def 19;
end;
end;
theorem
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
proof
let S be Field_Subset of X, M be Measure of S, A be Element of S, B be
measure_zero of M;
assume A c= B;
then M.A <= M.B by Th8;
then
A1: M.A <= 0. by Def4;
0.<= M.A by Def2;
then M.A = 0.by A1;
hence thesis by Def4;
end;
theorem
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
proof
let S be Field_Subset of X, M be Measure of S, A,B be measure_zero of M;
A1: 0.<= M.(A /\ B) by Def2;
A2: 0.<= M.(A \ B) by Def2;
A3: M.A = 0. by Def4;
then M.(A \ B) <= 0.by Th8,XBOOLE_1:36;
then
A4: M.(A \ B) = 0.by A2;
M.B = 0. by Def4;
then M.(A \/ B) <= 0.+ 0.by A3,Th10;
then
A5: M.(A \/ B) <= 0.by XXREAL_3:4;
0.<= M.(A \/ B) by Def2;
then
A6: M.(A \/ B) = 0.by A5;
M.(A /\ B) <= 0.by A3,Th8,XBOOLE_1:17;
then M.(A /\ B) = 0.by A1;
hence thesis by A6,A4,Def4;
end;
theorem
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
proof
let S be Field_Subset of X, M be Measure of S, A be Element of S, B be
measure_zero of M;
A1: M.A = M.((A /\ B) \/ (A \ B)) by XBOOLE_1:51;
A2: M.B = 0.by Def4;
then
A3: M.(A /\ B) <= 0.by Th8,XBOOLE_1:17;
A4: 0.<= M.(A /\ B) by Def2;
then M.(A /\ B) = 0.by A3;
then M.A <= 0.+ M.(A \ B) by A1,Th10;
then
A5: M.A <= M.(A \ B) by XXREAL_3:4;
M.(A \/ B) <= M.A + 0.by A2,Th10;
then
A6: M.(A \/ B) <= M.A by XXREAL_3:4;
M.A <= M.(A \/ B) & M.(A \ B) <= M.A by Th8,XBOOLE_1:7,36;
hence thesis by A4,A6,A3,A5,XXREAL_0:1;
end;
::
:: sigma_Field Subset of X and sigma_additive nonnegative measure
::
theorem Th15:
for A being Subset of X ex F being sequence of bool X st rng F = {A}
proof
let A be Subset of X;
take NAT --> A;
thus thesis by FUNCOP_1:8;
end;
theorem Th16:
for A being set ex F being sequence of {A} st
for n being Element of NAT holds F.n = A
proof
let A be set;
take NAT --> A;
thus thesis by TARSKI:def 1;
end;
registration
let X be set;
cluster non empty countable for Subset-Family of X;
existence
proof
reconsider S = {{}} as Subset-Family of X by SETFAM_1:46;
take S;
thus S is non empty;
{}X is Subset of X;
hence S is empty or ex F being sequence of bool X st S = rng F by Th15;
end;
end;
definition
let X be set;
mode N_Sub_set_fam of X is non empty countable Subset-Family of X;
end;
theorem Th17:
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
proof
let A,B,C be Subset of X;
take (A,B) followed_by C;
thus thesis by FUNCT_7:122,123,124,127;
end;
theorem
for A,B being Subset of X holds {A,B,{}} is N_Sub_set_fam of X
proof
let A,B be Subset of X;
ex F being sequence of bool X st rng F = {A,B,{}X} & F.0 = A & F.1 = B
& for n being Element of NAT st 1 < n holds F.n = {}X by Th17;
hence thesis by SUPINF_2:def 8;
end;
theorem Th19:
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
proof
let A,B be Subset of X;
take A followed_by B;
thus thesis by FUNCT_7:119,120,126;
end;
theorem
for A,B being Subset of X holds {A,B} is N_Sub_set_fam of X
proof
let A,B be 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) by Th19;
hence thesis by SUPINF_2:def 8;
end;
theorem Th21:
for S being N_Sub_set_fam of X holds X \ S is N_Sub_set_fam of X
proof
let S be N_Sub_set_fam of X;
consider F being sequence of bool X such that
A1: S = rng F by SUPINF_2:def 8;
defpred P[object,object] means
ex V being Subset of X st V = F.$1 & $2 = V`;
A2: for n being object st n in NAT ex y being object st y in X\S & P[n,y]
proof
let n be object;
assume n in NAT;
then consider V being set such that
A3: V in S and
A4: V=F.n by A1,FUNCT_2:4;
reconsider V as Subset of X by A3;
take V`;
V`` in S by A3;
hence thesis by A4,SETFAM_1:def 7;
end;
A5: ex G being sequence of X \ S st for n being object st n in NAT holds P[
n,G.n] from FUNCT_2:sch 1(A2);
A6: NAT = dom F by FUNCT_2:def 1;
ex G being sequence of bool X st X \ S = rng G
proof
consider G being sequence of X \ S such that
A7: for n being object st n in NAT holds ex V being Subset of X st V = F
.n & G.n = V` by A5;
A8: dom G = NAT by FUNCT_2:def 1;
A9: X \ S c= rng G
proof
let x be object;
assume
A10: x in X \ S;
then reconsider B = x as Subset of X;
B` in S by A10,SETFAM_1:def 7;
then consider n being object such that
A11: n in NAT and
A12: F.n = B` by A1,A6,FUNCT_1:def 3;
ex V being Subset of X st V = F.n & G.n = V` by A7,A11;
hence thesis by A8,A11,A12,FUNCT_1:def 3;
end;
reconsider G as sequence of bool X by FUNCT_2:7;
take G;
thus thesis by A9;
end;
hence thesis by SUPINF_2:def 8;
end;
definition
let X be set;
let IT be Subset-Family of X;
attr IT is sigma-additive means
:Def5:
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;
existence
proof
reconsider S = {{},X} as non empty Subset-Family of X by PROB_1:8;
take S;
thus S is non empty;
thus for A being set holds A in S implies X\A in S
proof
let A be set;
A1: A = {} implies X\A in S by TARSKI:def 2;
A2: A = X implies X\A in S
proof
assume A = X;
then X\A = {} by XBOOLE_1:37;
hence thesis by TARSKI:def 2;
end;
assume A in S;
hence thesis by A1,A2,TARSKI:def 2;
end;
let M be N_Sub_set_fam of X;
assume
A3: M c= S;
A4: not X in M implies union M in S
proof
assume not X in M;
then for A being set st A in M holds A c= {} by A3,TARSKI:def 2;
then union M c= {} by ZFMISC_1:76;
then union M = {};
hence thesis by TARSKI:def 2;
end;
X in M implies union M in S
proof
assume X in M;
then X c= union M by ZFMISC_1:74;
then X = union M;
hence thesis by TARSKI:def 2;
end;
hence thesis by A4;
end;
end;
registration
let X;
cluster compl-closed sigma-multiplicative -> sigma-additive for
Subset-Family of X;
coherence
proof
let F be Subset-Family of X such that
A1: F is compl-closed and
A2: F is sigma-multiplicative;
let M be non empty countable Subset-Family of X such that
A3: M c= F;
consider f being SetSequence of X such that
A4: M = rng f by SUPINF_2:def 8;
for n being Nat holds (Complement f).n in F
proof
let n be Nat;
reconsider n as Element of NAT by ORDINAL1:def 12;
f.n in M & (Complement f).n = (f.n)` by A4,FUNCT_2:4,PROB_1:def 2;
hence thesis by A1,A3;
end;
then rng Complement f c= F by NAT_1:52;
then
A5: Intersection Complement f in F by A2;
(Intersection Complement f)` = union M by A4,CARD_3:def 4;
hence thesis by A1,A5;
end;
cluster compl-closed sigma-additive -> sigma-multiplicative for
Subset-Family of X;
coherence
proof
let F be Subset-Family of X such that
A6: F is compl-closed and
A7: F is sigma-additive;
let f be SetSequence of X such that
A8: rng f c= F;
dom Complement f = NAT by FUNCT_2:def 1;
then reconsider
M = rng Complement f as non empty countable Subset-Family of X
by CARD_3:93;
M c= F
proof
let e be object;
assume e in M;
then consider n being object such that
A9: n in NAT and
A10: e = (Complement f).n by FUNCT_2:11;
reconsider n as Element of NAT by A9;
A11: f.n in rng f by NAT_1:51;
e = (f.n)` by A10,PROB_1:def 2;
hence thesis by A6,A8,A11;
end;
then Intersection f = (union M)` & union M in F by A7,CARD_3:def 4;
hence thesis by A6;
end;
end;
registration
let X be set;
cluster -> non empty for SigmaField of X;
coherence;
end;
theorem Th22:
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
proof
let S be non empty Subset-Family of X;
hereby
assume that
A1: for A being set holds A in S implies X\A in S and
A2: for M being N_Sub_set_fam of X st M c= S holds meet M in S;
for M being N_Sub_set_fam of X st M c= S holds union M in S
proof
let M be N_Sub_set_fam of X;
assume
A3: M c= S;
A4: X \ M c= S
proof
let y be object;
assume
A5: y in X \ M;
then reconsider B = y as Subset of X;
B` in M by A5,SETFAM_1:def 7;
then B`` in S by A1,A3;
hence thesis;
end;
X \ M is N_Sub_set_fam of X by Th21;
then X \ meet (X \ M) in S by A1,A2,A4;
hence thesis by Th4;
end;
then reconsider
S9 = S as non empty compl-closed sigma-additive Subset-Family
of X by A1,Def1,Def5;
S9 is SigmaField of X;
hence S is SigmaField of X;
end;
assume
A6: S is SigmaField of X;
for M being N_Sub_set_fam of X st M c= S holds meet M in S
proof
let M be N_Sub_set_fam of X;
assume
A7: M c= S;
A8: X \ M c= S
proof
let y be object;
assume
A9: y in X \ M;
then reconsider B = y as Subset of X;
B` in M by A9,SETFAM_1:def 7;
then B`` in S by A6,A7,PROB_1:def 1;
hence thesis;
end;
X \ M is N_Sub_set_fam of X by Th21;
then union (X \ M) in S by A6,A8,Def5;
then X \ union (X \ M) in S by A6,Def1;
hence thesis by Th4;
end;
hence thesis by A6,Def1;
end;
registration
let X be set;
let S be SigmaField of X;
cluster disjoint_valued for sequence of S;
existence
proof
consider F being sequence of {{}} such that
A1: for n being Element of NAT holds F.n = {} by Th16;
{} in S by PROB_1:4;
then {{}} c= S by ZFMISC_1:31;
then reconsider F as sequence of S by FUNCT_2:7;
take F;
A2: for n being object holds F.n = {}
proof
let n be object;
per cases;
suppose
n in dom F;
hence thesis by A1;
end;
suppose
not n in dom F;
hence thesis by FUNCT_1:def 2;
end;
end;
thus for x,y being object st x <> y holds F.x misses F.y
proof
let x,y be object;
F.x = {} by A2;
hence thesis;
end;
end;
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; :: redefines rng (FUNCT_1, redefinition) → rng (RELAT_1, synonym) → proj2 (XTUPLE_0, definition)
coherence
proof
rng F <> {};
hence thesis by XBOOLE_1:1;
end;
end;
theorem Th23:
for S being SigmaField of X, F being sequence of S holds rng
F is N_Sub_set_fam of X
proof
let S be SigmaField of X;
let F be sequence of S;
ex H being sequence of bool X st rng F = rng H
proof
rng F c= bool X;
then reconsider F as sequence of bool X by FUNCT_2:6;
take F;
thus thesis;
end;
hence thesis by SUPINF_2:def 8;
end;
theorem Th24:
for S being SigmaField of X, F being sequence of S holds
union rng F is Element of S
proof
let S be SigmaField of X, F be sequence of S;
rng F is N_Sub_set_fam of X & rng F c= S by Th23,RELAT_1:def 19;
hence thesis by Def5;
end;
theorem Th25:
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
proof
let Y,S be non empty set;
let F be Function of Y,S;
let M be Function of S,ExtREAL;
assume
A1: M is nonnegative;
for n being Element of Y holds 0.<= (M*F).n
proof
let n be Element of Y;
dom (M*F) = Y by FUNCT_2:def 1;
then (M*F).n = M.(F.n) by FUNCT_1:12;
hence thesis by A1;
end;
hence thesis;
end;
theorem Th26:
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)
proof
let S be SigmaField of X, a,b be R_eal;
defpred P[object,object] means
($1 = {} implies $2 = a) & ($1 <> {} implies $2 = b);
A1: for x being object st x in S ex y being object st y in ExtREAL & P[x,y]
proof
let x be object;
x <> {} implies ex y being set st y in ExtREAL & P[x,y];
hence thesis;
end;
ex F being Function of S,ExtREAL st for x being object st x in S holds P[x,
F.x] from FUNCT_2:sch 1(A1);
then consider M being Function of S,ExtREAL such that
A2: for x being object st x in S holds P[x,M.x];
take M;
thus thesis by A2;
end;
theorem
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) by Th26;
theorem Th28:
for S being SigmaField of X ex M being Function of S,ExtREAL st
for A being Element of S holds M.A = 0.
proof
let S be SigmaField of X;
consider M being Function of S,ExtREAL such that
A1: for A being Element of S holds (A = {} implies M.A = 0.) & (A <> {}
implies M.A = 0.) by Th26;
take M;
thus thesis by A1;
end;
definition
let X be set;
let S be SigmaField of X;
let F be Function of S,ExtREAL;
attr F is sigma-additive means
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;
existence
proof
consider M being Function of S,ExtREAL such that
A1: for A being Element of S holds M.A = 0. by Th28;
take M;
for A being Element of S holds 0.<= M.A by A1;
hence
A2: M is nonnegative;
thus M is sigma-additive
proof
let F be Sep_Sequence of S;
A3: for r being Element of NAT st 0 <= r holds (M*F).r = 0.
proof
let r be Element of NAT;
dom (M*F) = NAT by FUNCT_2:def 1;
then (M*F).r = M.(F.r) by FUNCT_1:12;
hence thesis by A1;
end;
M*F is nonnegative by A2,Th25;
then
A4: SUM(M*F) = Ser(M*F).0 by A3,SUPINF_2:48;
union rng F is Element of S by Th24;
then
A5: M.(union rng F) = 0.by A1;
Ser(M*F).0 = (M*F).0 by SUPINF_2:def 11;
hence thesis by A5,A3,A4;
end;
{} is Element of S by PROB_1:4;
then M.{} = 0. by A1;
hence thesis by VALUED_0:def 19;
end;
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;
coherence;
end;
registration let X be set, S be SigmaField of X;
cluster sigma-additive -> additive
for nonnegative zeroed Function of S, ExtREAL;
coherence
proof
let M be nonnegative zeroed Function of S, ExtREAL;
assume A1: M is sigma-additive;
for A,B being Element of S holds (A misses B implies M.(A \/ B) = M.A + M.B)
proof
set n2 = 1 + 1;
let A,B be Element of S;
assume
A2: A misses B;
A3: A in S & B in S;
reconsider A,B as Subset of X;
{} is Subset of X by XBOOLE_1:2;
then consider F being sequence of bool X such that
A4: rng F = {A,B,{}} and
A5: F.0 = A & F.1 = B and
A6: for n being Element of NAT st 1 < n holds F.n = {} by Th17;
{} in S by PROB_1:4;
then for x being object holds x in {A,B,{}} implies x in S by A3,
ENUMSET1:def 1;
then {A,B,{}} c= S;
then reconsider F as sequence of S by A4,FUNCT_2:6;
A7: for n,m being Element of NAT st n <> m holds F.n misses F.m
proof
let n,m be Element of NAT;
A8: n = 0 or n = 1 or 1 < n by NAT_1:25;
A9: m = 0 or m = 1 or 1 < m by NAT_1:25;
A10: 1 < n & m = 1 implies F.n misses F.m
proof
assume that
A11: 1 < n and
m = 1;
F.n = {} by A6,A11;
then F.n /\ F.m = {};
hence thesis;
end;
A12: 1 < n & m = 0 implies F.n misses F.m
proof
assume that
A13: 1 < n and
m = 0;
F.n = {} by A6,A13;
then F.n /\ F.m = {};
hence thesis;
end;
A14: 1 < n & 1 < m implies F.n misses F.m
proof
assume that
A15: 1 < n and
1 < m;
F.n = {} by A6,A15;
then F.n /\ F.m = {};
hence thesis;
end;
A16: n = 1 & 1 < m implies F.n misses F.m
proof
assume that
n = 1 and
A17: 1 < m;
F.m = {} by A6,A17;
then F.n /\ F.m = {};
hence thesis;
end;
A18: n = 0 & 1 < m implies F.n misses F.m
proof
assume that
n = 0 and
A19: 1 < m;
F.m = {} by A6,A19;
then F.n /\ F.m = {};
hence thesis;
end;
assume n <> m;
hence thesis by A2,A5,A8,A9,A18,A16,A12,A10,A14;
end;
for m,n being object st m <> n holds F.m misses F.n
proof
let m,n be object;
assume
A20: m <> n;
per cases;
suppose
m in NAT & n in NAT;
hence thesis by A7,A20;
end;
suppose
not m in NAT or not n in NAT;
then not m in dom F or not n in dom F;
then F.m = {} or F.n = {} by FUNCT_1:def 2;
hence thesis;
end;
end;
then reconsider F as disjoint_valued sequence of S by PROB_2:def 2;
union {A,B,{}} = union {A,B} by Th1;
then
A21: union rng F = A \/ B by A4,ZFMISC_1:75;
A22: for r being Element of NAT holds (M*F).0 = M.A & (M*F).1 = M.B & (1+1
<= r implies (M*F).r = 0.)
proof
let r be Element of NAT;
A23: for r being Element of NAT holds (M*F).r = M.(F.r)
proof
let r be Element of NAT;
dom (M*F) = NAT by FUNCT_2:def 1;
hence thesis by FUNCT_1:12;
end;
1 + 1 <= r implies (M*F).r = 0.
proof
assume 1 + 1 <= r;
then 1 < r by NAT_1:13;
then F.r = {} by A6;
then (M*F).r = M.{} by A23;
hence thesis by VALUED_0:def 19;
end;
hence thesis by A5,A23;
end;
set H = M*F;
A24: 0 + 1 = 0 + 1;
set y1 = Ser H.1;
A25: H is nonnegative by Th25;
reconsider A,B as Element of S;
Ser H.n2 = y1 + H.n2 by SUPINF_2:def 11;
then Ser H.n2 = y1 + 0.by A22
.= Ser H.1 by XXREAL_3:4
.= Ser H.0 + H.1 by A24,SUPINF_2:def 11
.= M.A + M.B by A22,SUPINF_2:def 11;
then SUM(M*F) = M.A + M.B by A22,A25,SUPINF_2:48;
hence thesis by A21,A1;
end;
then M is additive;
hence thesis;
end;
end;
theorem
for S being SigmaField of X, M being sigma_Measure of S holds
M is Measure of S;
theorem
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 by Def3;
theorem
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 by Th8;
theorem
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 by Th9;
theorem
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 by Th10;
theorem
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 by Def1,FINSUB_1:def 1,def 2,PROB_1:4,5;
theorem
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
proof
let S be SigmaField of X, M be sigma_Measure of S, T be N_Sub_set_fam of X;
assume
A1: for A being set st A in T holds A in S;
T c= S
by A1;
hence thesis by Def5,Th22;
end;
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 :Def7:
M.it = 0.;
existence
proof
{} is Element of S by PROB_1:4;
then consider A being Element of S such that
A1: A = {};
take A;
thus thesis by A1,VALUED_0:def 19;
end;
end;
theorem
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
proof
let S be SigmaField of X, M be sigma_Measure of S, A be Element of S, B be
measure_zero of M;
assume A c= B;
then M.A <= M.B by Th8;
then
A1: M.A <= 0. by Def7;
0.<= M.A by Def2;
then M.A = 0.by A1;
hence thesis by Def7;
end;
theorem
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
proof
let S be SigmaField of X, M be sigma_Measure of S, A,B be measure_zero of M;
A1: 0.<= M.(A /\ B) by Def2;
A2: 0.<= M.(A \ B) by Def2;
A3: M.A = 0. by Def7;
then M.(A \ B) <= 0.by Th8,XBOOLE_1:36;
then
A4: M.(A \ B) = 0.by A2;
M.B = 0. by Def7;
then M.(A \/ B) <= 0.+ 0.by A3,Th10;
then
A5: M.(A \/ B) <= 0.by XXREAL_3:4;
0.<= M.(A \/ B) by Def2;
then
A6: M.(A \/ B) = 0.by A5;
M.(A /\ B) <= 0.by A3,Th8,XBOOLE_1:17;
then M.(A /\ B) = 0.by A1;
hence thesis by A6,A4,Def7;
end;
theorem
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
proof
let S be SigmaField of X, M be sigma_Measure of S, A be Element of S, B be
measure_zero of M;
A1: M.A = M.((A /\ B) \/ (A \ B)) by XBOOLE_1:51;
A2: M.B = 0.by Def7;
then
A3: M.(A /\ B) <= 0.by Th8,XBOOLE_1:17;
A4: 0.<= M.(A /\ B) by Def2;
then M.(A /\ B) = 0.by A3;
then M.A <= 0.+ M.(A \ B) by A1,Th10;
then
A5: M.A <= M.(A \ B) by XXREAL_3:4;
M.(A \/ B) <= M.A + 0.by A2,Th10;
then
A6: M.(A \/ B) <= M.A by XXREAL_3:4;
M.A <= M.(A \/ B) & M.(A \ B) <= M.A by Th8,XBOOLE_1:7,36;
hence thesis by A4,A6,A3,A5,XXREAL_0:1;
end;
definition
let X be set, S be Field_Subset of X;
let F be Function of S,ExtREAL;
redefine attr F is additive means :: redefines additive (MEASURE1, definition)
for A,B being Element of S st A misses B holds
F.(A \/ B) = F.A + F.B;
compatibility;
end;