:: Completeness of the $\sigma$-Additive Measure. Measure Theory
:: by J\'ozef Bia{\l}as
::
:: Received February 22, 1992
:: Copyright (c) 1992-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 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,
XXREAL_3, 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;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0, XXREAL_3;
expansions TARSKI, XBOOLE_0;
theorems TARSKI, FUNCT_1, FUNCT_2, ZFMISC_1, NAT_1, SETFAM_1, SUPINF_2,
MEASURE1, MEASURE2, PROB_2, XBOOLE_0, XBOOLE_1, XXREAL_0, PROB_1,
FINSUB_1, ORDINAL1, XXREAL_2, VALUED_0, XXREAL_3, RELAT_1, XREAL_0;
schemes NAT_1, FUNCT_2, XFAMILY;
begin
::
:: Some additional properties about R_eal numbers
::
reserve X for set;
theorem Th1:
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)
proof
let F1,F2 be sequence of ExtREAL;
assume
A1: for n being Element of NAT holds Ser(F1).n <= Ser(F2).n;
A2: for x being ExtReal st x in rng Ser(F1) holds ex y being
ExtReal st y in rng Ser(F2) & x <= y
proof
let x be ExtReal;
A3: dom Ser(F1) = NAT by FUNCT_2:def 1;
assume x in rng Ser(F1);
then consider n being object such that
A4: n in NAT and
A5: x = Ser(F1).n by A3,FUNCT_1:def 3;
reconsider n as Element of NAT by A4;
reconsider y = Ser(F2).n as R_eal;
take y;
dom Ser(F2) = NAT by FUNCT_2:def 1;
hence thesis by A1,A5,FUNCT_1:def 3;
end;
SUM(F1) = sup(rng Ser F1) & SUM(F2) = sup(rng Ser F2)
by SUPINF_2:def 13;
hence thesis by A2,XXREAL_2:63;
end;
theorem
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)
proof
let F1,F2 be sequence of ExtREAL;
assume
A1: for n being Element of NAT holds Ser(F1).n = Ser(F2).n;
then for n being Element of NAT holds Ser(F2).n <= Ser(F1).n;
then
A2: SUM(F2) <= SUM(F1) by Th1;
for n being Element of NAT holds Ser(F1).n <= Ser(F2).n by A1;
then SUM(F1) <= SUM(F2) by Th1;
hence thesis by A2,XXREAL_0:1;
end;
::
:: 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; :: redefines rng (FUNCT_1, redefinition) → rng (RELAT_1, synonym) → proj2 (XTUPLE_0, definition)
coherence
proof
rng F is N_Sub_set_fam of X & rng F c= S by MEASURE1:23,RELAT_1:def 19;
hence thesis by MEASURE2:def 1;
end;
end;
theorem
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)
proof
let S be SigmaField of X;
let M be sigma_Measure of S;
let F be sequence of S;
let A be Element of S;
assume that
A1: meet rng F c= A and
A2: for n being Element of NAT holds A c= F.n;
A c= meet rng F
proof
let x be object;
assume
A3: x in A;
for Y being set st Y in rng F holds x in Y
proof
let Y be set;
A4: dom F = NAT by FUNCT_2:def 1;
assume Y in rng F;
then ex n being object st n in NAT & Y = F.n by A4,FUNCT_1:def 3;
then A c= Y by A2;
hence thesis by A3;
end;
hence thesis by SETFAM_1:def 1;
end;
then
A5: M.(A) <= M.(meet rng F) by MEASURE1:31;
M.(meet rng F) <= M.(A) by A1,MEASURE1:31;
hence thesis by A5,XXREAL_0:1;
end;
theorem Th4:
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
proof
let S be SigmaField of X;
let G,F be sequence of S;
assume that
A1: G.0 = {} and
A2: for n being Nat holds G.(n+1) = F.0 \ F.n & F.(n+1) c= F. n;
A3: dom G = NAT by FUNCT_2:def 1;
thus union rng G c= F.0 \ meet rng F
proof
let A be object;
assume A in union rng G;
then consider Z being set such that
A4: A in Z and
A5: Z in rng G by TARSKI:def 4;
consider n being object such that
A6: n in NAT and
A7: Z = G.n by A3,A5,FUNCT_1:def 3;
reconsider n as Element of NAT by A6;
consider k being Nat such that
A8: n = k + 1 by A1,A4,A7,NAT_1:6;
reconsider k as Element of NAT by ORDINAL1:def 12;
set Y = F.k;
A9: A in F.0 \ F.k by A2,A4,A7,A8;
then Y in rng F & not A in Y by FUNCT_2:4,XBOOLE_0:def 5;
then
A10: not A in meet rng F by SETFAM_1:def 1;
A in F.0 by A9,XBOOLE_0:def 5;
hence thesis by A10,XBOOLE_0:def 5;
end;
let A be object;
assume
A11: A in F.0 \ meet rng F;
then not A in meet rng F by XBOOLE_0:def 5;
then
A12: ex Y being set st Y in rng F & not A in Y by SETFAM_1:def 1;
A in F.0 by A11,XBOOLE_0:def 5;
then consider Y being set such that
A13: A in F.0 and
A14: Y in rng F and
A15: not A in Y by A12;
dom F = NAT by FUNCT_2:def 1;
then consider n being object such that
A16: n in NAT and
A17: Y = F.n by A14,FUNCT_1:def 3;
reconsider n as Element of NAT by A16;
A in F.0 \ F.n by A13,A15,A17,XBOOLE_0:def 5;
then
A18: A in G.(n+1) by A2;
G.(n + 1) in rng G by FUNCT_2:4;
hence thesis by A18,TARSKI:def 4;
end;
theorem Th5:
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
proof
let S be SigmaField of X;
let G,F be sequence of S;
assume that
A1: G.0 = {} and
A2: for n being Nat holds G.(n+1) = F.0 \ F.n & F.(n+1) c= F .n;
A3: for n being Nat holds F.n c= F.0
proof
defpred P[Nat] means F.$1 c= F.0;
A4: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A5: F.k c= F.0;
F.(k+1) c= F.k by A2;
hence thesis by A5,XBOOLE_1:1;
end;
A6: P[0];
thus for n being Nat holds P[n] from NAT_1:sch 2(A6,A4);
end;
A7: meet rng F c= F.0
proof
set X = the Element of rng F;
let A be object;
dom F = NAT by FUNCT_2:def 1;
then ex n being object st n in NAT & F.n = X by FUNCT_1:def 3;
then
A8: X c= F.0 by A3;
assume A in meet rng F;
then A in X by SETFAM_1:def 1;
hence thesis by A8;
end;
A9: F.0 /\ meet rng F = F.0 \ (F.0 \ meet rng F) by XBOOLE_1:48;
union rng G = F.0 \ meet rng F by A1,A2,Th4;
hence thesis by A7,A9,XBOOLE_1:28;
end;
theorem Th6:
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)
proof
let S be SigmaField of X, M be sigma_Measure of S, G,F be sequence of S;
assume that
A1: M.(F.0) <+infty and
A2: G.0 = {} & for n being Nat holds G.(n+1) = F.0 \ F.n & F.
(n+1) c= F .n;
A3: union rng G = F.0 \ meet rng F by A2,Th4;
A4: M.(F.0 \ union rng G) = M.(meet rng F) by A2,Th5;
M.(F.0 \ meet rng F) <> +infty by A1,MEASURE1:31,XBOOLE_1:36;
then M.(union rng G) <+infty by A3,XXREAL_0:4;
hence thesis by A3,A4,MEASURE1:32,XBOOLE_1:36;
end;
theorem Th7:
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)
proof
let S be SigmaField of X, M be sigma_Measure of S, G,F be sequence of S;
assume that
A1: M.(F.0) <+infty and
A2: G.0 = {} & for n being Nat holds G.(n+1) = F.0 \ F.n & F.
(n+1) c= F .n;
A3: meet rng F = F.0 \ union rng G by A2,Th5;
A4: M.(F.0 \ meet rng F) = M.(union rng G) by A2,Th4;
M.(F.0 \ union rng G) <> +infty by A1,MEASURE1:31,XBOOLE_1:36;
then M.(meet rng F) <+infty by A3,XXREAL_0:4;
hence thesis by A3,A4,MEASURE1:32,XBOOLE_1:36;
end;
theorem
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))
proof
let S be SigmaField of X, M be sigma_Measure of S, G,F be sequence of S;
assume that
A1: M.(F.0) <+infty and
A2: G.0 = {} & for n being Nat holds G.(n+1) = F.0 \ F.n & F.
(n+1) c= F .n;
for n being Nat holds G.n c= G.(n+1) by A2,MEASURE2:13;
then M.(union rng G) = sup(rng (M*G)) by MEASURE2:23;
hence thesis by A1,A2,Th6;
end;
theorem Th9:
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
proof
let S be SigmaField of X, M be sigma_Measure of S, G,F be sequence of S;
assume that
A1: M.(F.0) <+infty and
A2: G.0 = {} and
A3: for n being Nat holds G.(n+1) = F.0 \ F.n & F.(n+1) c= F .n;
reconsider P = {} as Element of S by PROB_1:4;
A4: 0 in REAL by XREAL_0:def 1;
M.P <= M.(F.0) by MEASURE1:31,XBOOLE_1:2;
then 0. <= M.(F.0) by VALUED_0:def 19;
hence
A5: M.(F.0) in REAL by A1,XXREAL_0:46,A4;
for x being ExtReal st x in rng(M*G) holds x <= M.(F.0)
proof
let x be ExtReal;
A6: dom (M*G) = NAT by FUNCT_2:def 1;
assume x in rng(M*G);
then consider n being object such that
A7: n in NAT and
A8: (M*G).n = x by A6,FUNCT_1:def 3;
reconsider n as Element of NAT by A7;
A9: x = M.(G.n) by A6,A8,FUNCT_1:12;
A10: (ex k being Nat st n = k + 1) implies x <= M.(F.0)
proof
given k being Nat such that
A11: n = k + 1;
reconsider k as Element of NAT by ORDINAL1:def 12;
G.n = F.0 \ F.k by A3,A11;
hence thesis by A9,MEASURE1:31,XBOOLE_1:36;
end;
n = 0 implies x <= M.(F.0) by A2,A9,MEASURE1:31,XBOOLE_1:2;
hence thesis by A10,NAT_1:6;
end;
then M.(F.0) is UpperBound of rng(M*G) by XXREAL_2:def 1;
then
A12: sup(rng(M*G)) <= M.(F.0) by XXREAL_2:def 3;
for x being ExtReal st x in rng(M*F) holds 0.<= x
proof
let x be ExtReal;
A13: dom (M*F) = NAT by FUNCT_2:def 1;
A14: (M*F) is nonnegative by MEASURE2:1;
assume x in rng(M*F);
then ex n being object st n in NAT & (M*F).n = x by A13,FUNCT_1:def 3;
hence thesis by A14,SUPINF_2:39;
end;
then 0. is LowerBound of rng(M*F) by XXREAL_2:def 2;
then
A15: inf(rng(M*F)) >= In(0,REAL) by XXREAL_2:def 4;
ex x being R_eal st x in rng(M*F) & x = M.(F.0)
proof
take (M*F).0;
dom (M*F) = NAT by FUNCT_2:def 1;
hence thesis by FUNCT_1:12,FUNCT_2:4;
end;
then inf(rng(M*F)) <= M.(F.0) by XXREAL_2:3;
hence inf(rng(M*F)) in REAL by A5,A15,XXREAL_0:45;
In(0,REAL) <= sup(rng(M*G))
proof
set x = (M*G).0;
for x being R_eal st x in rng(M*G) holds 0.<= x
proof
let x be R_eal;
A16: dom (M*G) = NAT by FUNCT_2:def 1;
A17: (M*G) is nonnegative by MEASURE2:1;
assume x in rng(M*G);
then ex n being object st n in NAT & (M*G).n = x by A16,FUNCT_1:def 3;
hence thesis by A17,SUPINF_2:39;
end;
then
A18: 0. <= x by FUNCT_2:4;
x <= sup rng(M*G) by FUNCT_2:4,XXREAL_2:4;
hence thesis by A18,XXREAL_0:2;
end;
hence thesis by A5,A12,XXREAL_0:45;
end;
theorem Th10:
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)
proof
let S be SigmaField of X, M be sigma_Measure of S, G,F be sequence of S;
assume that
A1: M.(F.0) <+infty and
A2: G.0 = {} and
A3: for n being Nat holds G.(n+1) = F.0 \ F.n & F.(n+1) c= F .n;
set l = M.(F.0) - inf rng (M*F);
for x being ExtReal st x in rng (M*G) holds x <= l
proof
let x be ExtReal;
A4: dom (M*G) = NAT by FUNCT_2:def 1;
assume x in rng (M*G);
then consider n being object such that
A5: n in NAT and
A6: (M*G).n = x by A4,FUNCT_1:def 3;
M*G is nonnegative by MEASURE2:1;
then x >= In(0,REAL) by A5,A6,SUPINF_2:39;
then
A7: x > -infty by XXREAL_0:2,12;
reconsider n as Element of NAT by A5;
A8: n = 0 implies G.n c= F.0 by A2;
A9: dom (M*F) = NAT by FUNCT_2:def 1;
A10: n = 0 implies M.(F.0 \ G.n) in rng (M*F)
proof
assume
A11: n = 0;
M.(F.0) = (M*F).0 by A9,FUNCT_1:12;
hence thesis by A2,A11,FUNCT_2:4;
end;
A12: (ex k being Nat st n = k + 1) implies M.(F.0 \ G.n) in rng (M*F)
proof
defpred P[Nat] means F.$1 c= F.0;
A13: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A14: F.k c= F.0;
F.(k+1) c= F.k by A3;
hence thesis by A14,XBOOLE_1:1;
end;
A15: P[0];
A16: for n being Nat holds P[n] from NAT_1:sch 2(A15,A13);
given k being Nat such that
A17: n = k + 1;
reconsider k as Element of NAT by ORDINAL1:def 12;
A18: M.(F.k) = (M*F).k by A9,FUNCT_1:12;
F.0 \ G.n = F.0 \ ( F.0 \ F.k) by A3,A17
.= F.0 /\ F.k by XBOOLE_1:48
.= F.k by A16,XBOOLE_1:28;
hence thesis by A18,FUNCT_2:4;
end;
A19: (ex k being Nat st n = k + 1) implies G.n c= F.0
proof
given k being Nat such that
A20: n = k + 1;
reconsider k as Element of NAT by ORDINAL1:def 12;
G.n = F.0 \ F.k by A3,A20;
hence thesis by XBOOLE_1:36;
end;
A21: x = M.(G.n) by A4,A6,FUNCT_1:12;
then x <> +infty by A1,A8,A19,MEASURE1:31,NAT_1:6;
then
A22: x in REAL by A7,XXREAL_0:14;
reconsider x as R_eal by XXREAL_0:def 1;
M.(F.0) in REAL & inf(rng(M*F)) in REAL by A1,A2,A3,Th9;
then consider a,b,c being Real such that
A23: a = M.(F.0) and
A24: b = x and
A25: c = inf(rng (M*F)) by A22;
M.(F.0) - x = a - b by A23,A24;
then
A26: (M.(F.0) - x) + x = (a - b) + b by A24
.= M.(F.0) by A23;
inf(rng (M*F)) + x = c + b by A24,A25;
then
A27: inf(rng (M*F)) + x - inf(rng (M*F)) = b + c - c by A25
.= x by A24;
M.(F.0) - x = M.(F.0 \ G.n) by A21,A8,A19,A22,MEASURE1:32,NAT_1:6
,XXREAL_0:9;
then inf(rng (M*F)) <= M.(F.0) - x by A10,A12,NAT_1:6,XXREAL_2:3;
then inf(rng (M*F)) + x <= M.(F.0) by A26,XXREAL_3:36;
hence thesis by A27,XXREAL_3:37;
end;
then
A28: l is UpperBound of rng (M*G) by XXREAL_2:def 1;
A29: for n being Nat holds G.n c= G.(n+1) by A2,A3,MEASURE2:13;
for y being UpperBound of rng (M*G) holds l <= y
proof
let y be UpperBound of rng (M*G);
l <= y
proof
for x being ExtReal st x in rng (M*F) holds M.(meet rng F) <= x
proof
let x be ExtReal;
A30: dom (M*F) = NAT by FUNCT_2:def 1;
assume x in rng (M*F);
then consider n being object such that
A31: n in NAT and
A32: (M*F).n = x by A30,FUNCT_1:def 3;
reconsider n as Element of NAT by A31;
A33: meet rng F c= F.n by FUNCT_2:4,SETFAM_1:3;
x = M.(F.n) by A30,A32,FUNCT_1:12;
hence thesis by A33,MEASURE1:31;
end;
then M.(meet rng F) is LowerBound of rng (M*F) by XXREAL_2:def 2;
then
A34: M.(meet rng F) <= inf(rng (M*F)) by XXREAL_2:def 4;
set Q = union rng G;
sup rng(M*G) = M.Q by A29,MEASURE2:23;
then
A35: M.Q <= y by XXREAL_2:def 3;
M.(F.0) - M.(meet rng F) = M.(union rng G) by A1,A2,A3,Th7;
then l <= M.Q by A34,XXREAL_3:37;
hence thesis by A35,XXREAL_0:2;
end;
hence thesis;
end;
hence thesis by A28,XXREAL_2:def 3;
end;
theorem Th11:
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))
proof
let S be SigmaField of X, M be sigma_Measure of S, G,F be sequence of S;
assume that
A1: M.(F.0) <+infty and
A2: G.0 = {} and
A3: for n being Nat holds G.(n+1) = F.0 \ F.n & F.(n+1) c= F .n;
set l = M.(F.0) - sup(rng (M*G));
for x being ExtReal st x in rng (M*F) holds l <= x
proof
let x be ExtReal;
assume
A4: x in rng (M*F);
x <> +infty implies l <=x
proof
A5: dom (M*F) = NAT by FUNCT_2:def 1;
then consider n being object such that
A6: n in NAT and
A7: (M*F).n = x by A4,FUNCT_1:def 3;
M*F is nonnegative by MEASURE2:1;
then
A8: 0. <= x by A6,A7,SUPINF_2:39;
assume
A9: x <> +infty;
reconsider x as R_eal by XXREAL_0:def 1;
x <= +infty by XXREAL_0:3;
then x < +infty by A9,XXREAL_0:1;
then
A10: x in REAL by A8,XXREAL_0:14,46;
M.(F.0) in REAL & sup(rng(M*G)) in REAL by A1,A2,A3,Th9;
then consider a,b,c being Real such that
A11: a = M.(F.0) and
A12: b = x and
A13: c = sup(rng (M*G)) by A10;
sup(rng (M*G)) + x = c + b by A12,A13;
then
A14: sup(rng (M*G)) + x - sup(rng (M*G)) = b + c - c by A13
.= x by A12;
reconsider n as Element of NAT by A6;
A15: dom (M*G) = NAT by FUNCT_2:def 1;
A16: M.(F.0) - x <= sup(rng (M*G))
proof
set k = n + 1;
A17: for n being Nat holds F.n c= F.0
proof
defpred P[Nat] means F.$1 c= F.0;
A18: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A19: F.k c= F.0;
F.(k+1) c= F.k by A3;
hence thesis by A19,XBOOLE_1:1;
end;
A20: P[0];
thus for k being Nat holds P[k] from NAT_1:sch 2(A20,A18);
end;
then M.(F.n) <= M.(F.0) by MEASURE1:31;
then
A21: M.(F.n) <+infty by A1,XXREAL_0:2;
M.(F.0) - x = M.(F.0) - M.(F.n) by A5,A7,FUNCT_1:12
.= M.(F.0 \ F.n) by A17,A21,MEASURE1:32
.= M.(G.(n+1)) by A3;
then M.(F.0) - x = (M*G).k by A15,FUNCT_1:12;
hence thesis by FUNCT_2:4,XXREAL_2:4;
end;
M.(F.0) - x = a - b by A11,A12;
then (M.(F.0) - x) + x = (a - b) + b by A12
.= M.(F.0) by A11;
then M.(F.0) <= sup(rng (M*G)) + x by A16,XXREAL_3:36;
hence thesis by A14,XXREAL_3:37;
end;
hence thesis by XXREAL_0:4;
end;
then
A22: l is LowerBound of rng (M*F) by XXREAL_2:def 2;
for y being LowerBound of rng (M*F) holds y <= l
proof
A23: inf(rng (M*F)) in REAL by A1,A2,A3,Th9;
sup(rng (M*G)) in REAL & M.(F.0) in REAL by A1,A2,A3,Th9;
then consider a,b,c being Real such that
A24: a = sup(rng (M*G)) and
A25: b = M.(F.0) and
A26: c = inf(rng (M*F)) by A23;
sup(rng (M*G)) + inf(rng (M*F)) = a + c by A24,A26;
then
A27: sup(rng (M*G)) + inf(rng (M*F)) - sup(rng (M*G)) = c + a - a by A24
.= inf(rng (M*F)) by A26;
let y be LowerBound of rng (M*F);
consider s,t,r being R_eal such that
s = sup(rng (M*G)) and
t = M.(F.0) - inf(rng (M*F)) and
A28: r = inf(rng (M*F));
A29: sup(rng (M*G)) = M.(F.0) - inf(rng (M*F)) by A1,A2,A3,Th10;
M.(F.0) - inf(rng (M*F)) = b - c by A25,A26;
then M.(F.0) - inf(rng (M*F)) + r = b - c + c by A26,A28
.= M.(F.0) by A25;
hence thesis by A29,A28,A27,XXREAL_2:def 4;
end;
hence thesis by A22,XXREAL_2:def 4;
end;
theorem
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))
proof
let S be SigmaField of X, M be sigma_Measure of S, F be sequence of S;
assume that
A1: for n being Nat holds F.(n+1) c= F.n and
A2: M.(F.0) <+infty;
consider G being sequence of S such that
A3: G.0 = {} & for n being Nat holds G.(n+1) = F.0 \ F.n by
MEASURE2:9;
A4: union rng G = F.0 \ meet rng F by A1,A3,Th4;
A5: M.(F.0 \ union rng G) = M.(meet rng F) by A1,A3,Th5;
A6: for A being Element of S st A = union rng G holds M.(meet rng F) = M.(F.
0) - M.A
proof
let A be Element of S;
assume
A7: A = union rng G;
M.(F.0 \ meet rng F) <> +infty by A2,MEASURE1:31,XBOOLE_1:36;
then M.A <+infty by A4,A7,XXREAL_0:4;
hence thesis by A4,A5,A7,MEASURE1:32,XBOOLE_1:36;
end;
for n being Nat holds G.n c= G.(n+1) by A1,A3,MEASURE2:13;
then M.(union rng G) = sup(rng (M*G)) by MEASURE2:23;
then M.(meet rng F) = M.(F.0) - sup(rng (M*G)) by A6;
hence thesis by A1,A2,A3,Th11;
end;
theorem Th13:
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)
proof
let S be SigmaField of X, M be Measure of S, F be Sep_Sequence of S;
set T = rng F;
consider G being sequence of S such that
A1: G.0 = F.0 and
A2: for n being Nat holds G.(n+1) = F.(n+1) \/ G.n by MEASURE2:4;
{} is Subset of X by XBOOLE_1:2;
then consider H being sequence of bool X such that
A3: rng H = {union T,{}} and
A4: H.0 = union T and
A5: for n being Nat st 0 < n holds H.n = {} by MEASURE1:19;
rng H c= S
proof
let a be object;
assume a in rng H;
then a = union T or a = {} by A3,TARSKI:def 2;
hence thesis by PROB_1:4;
end;
then reconsider H as sequence of S by FUNCT_2:6;
defpred P[Nat] means Ser(M*F).$1 = M.(G.$1);
A6: dom (M*F) = NAT by FUNCT_2:def 1;
A7: for n being Nat holds G.n /\ F.(n+1) = {}
proof
let n be Nat;
A8: for n being Nat holds for k being Element of NAT st n < k
holds G.n /\ F.k = {}
proof
defpred P[Nat] means
for k being Element of NAT st $1 < k
holds G.$1 /\ F.k = {};
A9: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A10: for k being Element of NAT st n < k holds G.n /\ F.k = {};
let k be Element of NAT;
assume
A11: n+1 < k;
then
A12: n < k by NAT_1:13;
F.(n+1) misses F.k by A11,PROB_2:def 2;
then
A13: F.(n+1) /\ F.k = {};
G.(n+1) /\ F.k = (F.(n+1) \/ G.n) /\ F.k by A2
.= (F.(n+1) /\ F.k) \/ (G.n /\ F.k) by XBOOLE_1:23;
hence thesis by A10,A12,A13;
end;
A14: P[0]
by PROB_2:def 2,A1,XBOOLE_0:def 7;
thus for n being Nat holds P[n] from NAT_1:sch 2(A14, A9);
end;
n < n + 1 by NAT_1:13;
hence thesis by A8;
end;
A15: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
G.k /\ F.(k+1) = {} by A7;
then
A16: G.k misses F.(k+1);
assume Ser(M*F).k = M.(G.k);
then Ser(M*F).(k+1) = M.(G.k) + (M*F).(k+1) by SUPINF_2:def 11;
then Ser(M*F).(k+1) = M.(G.k) + M.(F.(k+1)) by A6,FUNCT_1:12
.= M.(F.(k+1) \/ G.k) by A16,MEASURE1:def 3
.= M.(G.(k+1)) by A2;
hence thesis;
end;
Ser(M*F).0 = (M*F).0 by SUPINF_2:def 11;
then
A17: P[0] by A1,A6,FUNCT_1:12;
A18: for n being Nat holds P[n] from NAT_1:sch 2(A17,A15 );
defpred P[Nat] means Ser(M*H).$1 = M.(union T);
A19: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
0 <= n by NAT_1:2;
then 0 < n + 1 by NAT_1:13;
then
A20: H.(n+1) = {} by A5;
dom (M*H) = NAT by FUNCT_2:def 1;
then (M*H).(n+1) = M.({}) by A20,FUNCT_1:12;
then
A21: (M*H).(n+1) = 0. by VALUED_0:def 19;
assume Ser(M*H).n = M.(union T);
then Ser(M*H).(n+1) = M.(union T) + (M*H).(n+1) by SUPINF_2:def 11;
hence thesis by A21,XXREAL_3:4;
end;
Ser(M*H).0 = (M*H).0 & dom (M*H) = NAT by FUNCT_2:def 1,SUPINF_2:def 11;
then
A22: P[0] by A4,FUNCT_1:12;
A23: for n being Nat holds P[n] from NAT_1:sch 2(A22,A19 );
A24: for r being Element of NAT st 1 <= r holds (M*H).r = 0.
proof
let r be Element of NAT;
assume 1 <= r;
then 0 + 1 <= r;
then 0 < r by NAT_1:13;
then
A25: H.r = {} by A5;
dom (M*H) = NAT by FUNCT_2:def 1;
then (M*H).r = M.({}) by A25,FUNCT_1:12;
hence thesis by VALUED_0:def 19;
end;
A26: for n being Nat holds G.n c= union T
proof
defpred P[Nat] means G.$1 c= union T;
A27: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A28: G.n c= union T;
G.(n+1) = F.(n+1) \/ G.n & F.(n+1) c= union T by A2,FUNCT_2:4,ZFMISC_1:74
;
hence thesis by A28,XBOOLE_1:8;
end;
A29: P[0] by A1,FUNCT_2:4,ZFMISC_1:74;
thus for n being Nat holds P[n] from NAT_1:sch 2(A29,A27 );
end;
A30: for n being Element of NAT holds Ser(M*F).n <= Ser(M*H).n
proof
let n be Element of NAT;
Ser(M*F).n = M.(G.n) by A18;
then Ser(M*F).n <= M.(union T) by A26,MEASURE1:8;
hence thesis by A23;
end;
M*H is nonnegative by MEASURE1:25;
then SUM(M*H) = Ser(M*H).1 by A24,SUPINF_2:48;
then SUM(M*H) = M.(union T) by A23;
hence thesis by A30,Th1;
end;
theorem
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
proof
let S be SigmaField of X, M be Measure of S;
assume
A1: for F being Sep_Sequence of S holds M.(union rng F) <= SUM(M*F);
for F being Sep_Sequence of S holds SUM(M*F) = M.(union rng F)
proof
let F be Sep_Sequence of S;
M.(union rng F) <= SUM(M*F) & SUM(M*F) <= M.(union rng F) by A1,Th13;
hence thesis by XXREAL_0:1;
end;
hence thesis by MEASURE1:def 6;
end;
::
:: 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
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
:Def2:
ex B being set st B in S & it c= B & M.B = 0.;
existence
proof
reconsider A = {} as Subset of X by XBOOLE_1:2;
take A;
take B={};
thus B in S by PROB_1:4;
thus A c= B;
thus thesis by VALUED_0:def 19;
end;
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
:Def3:
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 );
existence
proof
A1: ex B being set st B in S & {} c= B & M.B = 0.
proof
consider B being set such that
A2: B = {} & B in S by PROB_1:4;
take B;
thus thesis by A2,VALUED_0:def 19;
end;
A3: {} is Subset of X by XBOOLE_1:2;
A4: for A being set st A = {} holds ex B being set st B in S & ex C being
thin of M st A = B \/ C
proof
reconsider C = {} as thin of M by A3,A1,Def2;
let A be set;
consider B being set such that
A5: B = {} and
A6: B in S by PROB_1:4;
assume A = {};
then A = B \/ C by A5;
hence thesis by A6;
end;
defpred P[set] means for A being set st A = $1 holds ex B being set st B
in S & ex C being thin of M st A = B \/ C;
consider D being set such that
A7: for y being set holds y in D iff y in bool X & P[y] from XFAMILY:
sch 1;
A8: 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) )
proof
let A be set;
A9: A in D iff (A in bool X & for y being set st y = A holds ex B being
set st (B in S & ex C being thin of M st y = B \/ C) ) by A7;
(ex B being set st (B in S & ex C being thin of M st A = B \/ C))
implies A in D
proof
assume
A10: ex B being set st (B in S & ex C being thin of M st A = B \/ C );
then A c= X by XBOOLE_1:8;
hence thesis by A9,A10;
end;
hence thesis by A7;
end;
A11: D c= bool X
by A7;
{} c= X;
then reconsider D as non empty Subset-Family of X by A7,A11,A4;
take D;
thus thesis by A8;
end;
uniqueness
proof
let D1,D2 be non empty Subset-Family of X such that
A12: for A being set holds (A in D1 iff ex B being set st (B in S & ex
C being thin of M st A = B \/ C) ) and
A13: for A being set holds (A in D2 iff ex B being set st (B in S & ex
C being thin of M st A = B \/ C) );
for A being object holds A in D1 iff A in D2
proof
let A be object;
thus A in D1 implies A in D2
proof
assume A in D1;
then ex B being set st (B in S & ex C being thin of M st A = B \/ C)
by A12;
hence thesis by A13;
end;
assume A in D2;
then ex B being set st (B in S & ex C being thin of M st A = B \/ C) by
A13;
hence thesis by A12;
end;
hence thesis by TARSKI:2;
end;
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
:Def4:
for B being set holds (B in it iff B in S & B c= A & A \ B is thin of M );
existence
proof
defpred P[set] means for t being set st t = $1 holds t in S & t c= A & A \
t is thin of M;
consider D being set such that
A1: for t being set holds t in D iff t in bool X & P[t] from XFAMILY:sch 1;
A2: for B being set holds B in D iff B in S & B c= A & A \ B is thin of M
proof
let B be set;
B in S & B c= A & A \ B is thin of M implies B in D
proof
assume that
A3: B in S and
A4: B c= A & A \ B is thin of M;
for t being set st t = B holds t in S & t c= A & A \ t is thin of
M by A3,A4;
hence thesis by A1,A3;
end;
hence thesis by A1;
end;
A5: D c= bool X
proof
let B be object;
assume B in D;
then B in S by A2;
hence thesis;
end;
D <> {}
proof
consider B being set such that
A6: B in S and
A7: ex C being thin of M st A = B \/ C by Def3;
consider C being thin of M such that
A8: A = B \/ C by A7;
consider E being set such that
A9: E in S and
A10: C c= E and
A11: M.E = 0. by Def2;
A \ B = C \ B by A8,XBOOLE_1:40;
then A \ B c= C by XBOOLE_1:36;
then A \ B c= E by A10;
then
A12: A \ B is thin of M by A9,A11,Def2;
B c= A by A8,XBOOLE_1:7;
hence thesis by A2,A6,A12;
end;
then reconsider D as non empty Subset-Family of X by A5;
take D;
thus thesis by A2;
end;
uniqueness
proof
let D1,D2 be non empty Subset-Family of X such that
A13: for B being set holds B in D1 iff B in S & B c= A & A \ B is thin of M and
A14: for B being set holds B in D2 iff B in S & B c= A & A \ B is thin of M;
for B being object holds B in D1 iff B in D2
proof
let B be object;
reconsider BB = B as set by TARSKI:1;
thus B in D1 implies B in D2
proof
assume
A15: B in D1;
then
A16: A \ BB is thin of M by A13;
B in S & BB c= A by A13,A15;
hence thesis by A14,A16;
end;
assume
A17: B in D2;
then
A18: A \ BB is thin of M by A14;
B in S & BB c= A by A14,A17;
hence thesis by A13,A18;
end;
hence thesis by TARSKI:2;
end;
end;
theorem Th15:
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)
proof
let S be SigmaField of X, M be sigma_Measure of S, F be sequence of COM(
S,M);
defpred P[Element of NAT, set] means for n being Element of NAT, y being set
st n = $1 & y = $2 holds y in MeasPart(F.n);
A1: for t being Element of NAT ex A being Element of S st P[t,A]
proof
let t be Element of NAT;
set A = the Element of MeasPart(F.t);
reconsider A as Element of S by Def4;
take A;
thus thesis;
end;
ex G being sequence of S st for t being Element of NAT holds P[t,G.t
] from FUNCT_2:sch 3(A1);
then consider G being sequence of S such that
A2: for t being Element of NAT, n being Element of NAT, y being set st n
= t & y = G.t holds y in MeasPart(F.n);
take G;
thus thesis by A2;
end;
theorem Th16:
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
proof
let S be SigmaField of X, M be sigma_Measure of S, F be sequence of COM(
S,M), G be sequence of S;
defpred P[Element of NAT, set] means for n being Element of NAT, y being set
st n = $1 & y = $2 holds y = F.n \ G.n;
A1: for t being Element of NAT ex A being Subset of X st P[t,A]
proof
let t be Element of NAT;
F.t is Element of COM(S,M);
then reconsider A = F.t \ G.t as Subset of X by XBOOLE_1:1;
take A;
thus thesis;
end;
ex H being sequence of bool X st for t being Element of NAT holds P[
t,H.t] from FUNCT_2:sch 3(A1);
then consider H being sequence of bool X such that
A2: for t being Element of NAT holds for n being Element of NAT for y
being set holds (n = t & y = H.t implies y = F.n \ G.n);
take H;
thus thesis by A2;
end;
theorem Th17:
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.
proof
let S be SigmaField of X, M be sigma_Measure of S, F be sequence of bool
X;
defpred P[Element of NAT, set] means for n being Element of NAT, y being set
st n = $1 & y = $2 holds y in S & F.n c= y & M.y = 0.;
assume
A1: for n being Element of NAT holds F.n is thin of M;
A2: for t being Element of NAT ex A being Element of S st P[t,A]
proof
let t be Element of NAT;
F.t is thin of M by A1;
then consider A being set such that
A3: A in S and
A4: F.t c= A & M.A = 0. by Def2;
reconsider A as Element of S by A3;
take A;
thus thesis by A4;
end;
ex G being sequence of S st for t being Element of NAT holds P[t,G.t
] from FUNCT_2:sch 3(A2);
then consider G being sequence of S such that
A5: for t being Element of NAT, n being Element of NAT, y being set st n
= t & y = G.t holds y in S & F.n c= y & M.y = 0.;
take G;
thus thesis by A5;
end;
theorem Th18:
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
proof
let S be SigmaField of X, M be sigma_Measure of S, D be non empty
Subset-Family of X;
assume
A1: 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;
A2: for K being N_Sub_set_fam of X st K c= D holds union K in D
proof
let K be N_Sub_set_fam of X;
consider F being sequence of bool X such that
A3: K = rng F by SUPINF_2:def 8;
assume
A4: K c= D;
A5: for n being Element of NAT holds F.n in D
proof
let n be Element of NAT;
F.n in K by A3,FUNCT_2:4;
hence thesis by A4;
end;
A6: for n being Element of NAT holds ex B being set st B in S & ex C
being thin of M st F.n = B \/ C
by A5,A1;
for n being Element of NAT holds F.n in COM(S,M)
proof
let n be Element of NAT;
ex B being set st B in S & ex C being thin of M st F.n = B \/ C by A6;
hence thesis by Def3;
end;
then
A7: for n being object st n in NAT holds F.n in COM(S,M);
A8: dom F = NAT by FUNCT_2:def 1;
then reconsider F as sequence of COM(S,M) by A7,FUNCT_2:3;
consider G being sequence of S such that
A9: for n being Element of NAT holds G.n in MeasPart(F.n) by Th15;
consider H be sequence of bool X such that
A10: for n being Element of NAT holds H.n = F.n \ G.n by Th16;
A11: for n being Element of NAT holds G.n in S & G.n c= F.n & F.n \ G.n is
thin of M
proof
let n be Element of NAT;
G.n in MeasPart(F.n) by A9;
hence thesis by Def4;
end;
for n being Element of NAT holds H.n is thin of M
proof
let n be Element of NAT;
F.n \ G.n is thin of M by A11;
hence thesis by A10;
end;
then consider L being sequence of S such that
A12: for n being Element of NAT holds H.n c= L.n & M.(L.n) = 0. by Th17;
ex B being set st B in S & ex C being thin of M st union K = B \/ C
proof
set B = union rng G;
take B;
A13: union rng G c= union rng F
proof
let x be object;
assume x in union rng G;
then consider Z being set such that
A14: x in Z and
A15: Z in rng G by TARSKI:def 4;
dom G = NAT by FUNCT_2:def 1;
then consider n being object such that
A16: n in NAT and
A17: Z = G.n by A15,FUNCT_1:def 3;
reconsider n as Element of NAT by A16;
set P = F.n;
A18: G.n c= P by A11;
ex P being set st P in rng F & x in P
proof
take P;
thus thesis by A8,A14,A17,A18,FUNCT_1:def 3;
end;
hence thesis by TARSKI:def 4;
end;
ex C being thin of M st union K = B \/ C
proof
for A being set st A in rng L holds A is measure_zero of M
proof
let A be set;
assume
A19: A in rng L;
dom L = NAT by FUNCT_2:def 1;
then
A20: ex n being object st n in NAT & A = L.n by A19,FUNCT_1:def 3;
rng L c= S by MEASURE2:def 1;
then reconsider A as Element of S by A19;
M.A = 0. by A12,A20;
hence thesis by MEASURE1:def 7;
end;
then union rng L is measure_zero of M by MEASURE2:14;
then
A21: M.(union rng L) = 0. by MEASURE1:def 7;
set C = union K \ B;
A22: union K = C \/ union rng F /\ union rng G by A3,XBOOLE_1:51
.= B \/ C by A13,XBOOLE_1:28;
reconsider C as Subset of X;
A23: C c= union rng H
proof
let x be object;
assume
A24: x in C;
then x in union rng F by A3,XBOOLE_0:def 5;
then consider Z being set such that
A25: x in Z and
A26: Z in rng F by TARSKI:def 4;
consider n being object such that
A27: n in NAT and
A28: Z = F.n by A8,A26,FUNCT_1:def 3;
reconsider n as Element of NAT by A27;
A29: not x in union rng G by A24,XBOOLE_0:def 5;
not x in G.n
proof
dom G = NAT by FUNCT_2:def 1;
then
A30: G.n in rng G by FUNCT_1:def 3;
assume x in G.n;
hence thesis by A29,A30,TARSKI:def 4;
end;
then
A31: x in F.n \ G.n by A25,A28,XBOOLE_0:def 5;
ex Z being set st x in Z & Z in rng H
proof
take H.n;
dom H = NAT by FUNCT_2:def 1;
hence thesis by A10,A31,FUNCT_1:def 3;
end;
hence thesis by TARSKI:def 4;
end;
union rng H c= union rng L
proof
let x be object;
assume x in union rng H;
then consider Z being set such that
A32: x in Z and
A33: Z in rng H by TARSKI:def 4;
dom H = NAT by FUNCT_2:def 1;
then consider n being object such that
A34: n in NAT and
A35: Z = H.n by A33,FUNCT_1:def 3;
reconsider n as Element of NAT by A34;
n in dom L by A34,FUNCT_2:def 1;
then
A36: L.n in rng L by FUNCT_1:def 3;
H.n c= L.n by A12;
hence thesis by A32,A35,A36,TARSKI:def 4;
end;
then C c= union rng L by A23;
then C is thin of M by A21,Def2;
then consider C being thin of M such that
A37: union K = B \/ C by A22;
take C;
thus thesis by A37;
end;
hence thesis;
end;
hence thesis by A1;
end;
for A being set holds A in D implies X\A in D
proof
let A be set;
assume
A38: A in D;
ex Q being set st Q in S & ex W being thin of M st X \ A = Q \/ W
proof
consider B being set such that
A39: B in S and
A40: ex C being thin of M st A = B \/ C by A1,A38;
set P = X \ B;
consider C being thin of M such that
A41: A = B \/ C by A40;
consider G being set such that
A42: G in S and
A43: C c= G and
A44: M.G = 0. by Def2;
set Q = P \ G;
A45: X \ A = P \ C by A41,XBOOLE_1:41;
A46: ex W being thin of M st X \ A = Q \/ W
proof
set W = P /\ (G \ C);
W c= P by XBOOLE_1:17;
then reconsider W as Subset of X by XBOOLE_1:1;
reconsider W as thin of M by A42,A44,Def2;
take W;
thus thesis by A43,A45,XBOOLE_1:117;
end;
take Q;
X \ B in S by A39,MEASURE1:def 1;
hence thesis by A42,A46,MEASURE1:6;
end;
hence thesis by A1;
end;
then reconsider
D9 = D as compl-closed sigma-additive non empty Subset-Family of
X by A2,MEASURE1:def 1,def 5;
D9 is SigmaField of X;
hence thesis;
end;
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;
coherence
proof
for A being set holds A in COM(S,M) iff ex B being set st B in S & ex
C being thin of M st A = B \/ C by Def3;
hence thesis by Th18;
end;
end;
theorem Th19:
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
proof
let S be SigmaField of X, M be sigma_Measure of S, B1,B2 be set;
assume
A1: B1 in S & B2 in S;
let C1,C2 be thin of M;
assume
A2: B1 \/ C1 = B2 \/ C2;
then
A3: B1 c= B2 \/ C2 by XBOOLE_1:7;
A4: B2 c= B1 \/ C1 by A2,XBOOLE_1:7;
consider D1 being set such that
A5: D1 in S and
A6: C1 c= D1 and
A7: M.D1 = 0. by Def2;
A8: B1 \/ C1 c= B1 \/ D1 by A6,XBOOLE_1:9;
consider D2 being set such that
A9: D2 in S and
A10: C2 c= D2 and
A11: M.D2 = 0. by Def2;
A12: B2 \/ C2 c= B2 \/ D2 by A10,XBOOLE_1:9;
reconsider B1,B2,D1,D2 as Element of S by A1,A5,A9;
A13: M.(B1 \/ D1) <= M.B1 + M.D1 & M.B1 + M.D1 = M.B1 by A7,MEASURE1:33
,XXREAL_3:4;
M.B2 <= M.(B1 \/ D1) by A4,A8,MEASURE1:31,XBOOLE_1:1;
then
A14: M.B2 <= M.B1 by A13,XXREAL_0:2;
A15: M.(B2 \/ D2) <= M.B2 + M.D2 & M.B2 + M.D2 = M.B2 by A11,MEASURE1:33
,XXREAL_3:4;
M.B1 <= M.(B2 \/ D2) by A3,A12,MEASURE1:31,XBOOLE_1:1;
then M.B1 <= M.B2 by A15,XXREAL_0:2;
hence thesis by A14,XXREAL_0:1;
end;
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
:Def5:
for B being set st B in S for C being thin of M holds it.(B \/ C) = M.B;
existence
proof
set B = {};
defpred P[object,object] means
for x,y being set st x in COM(S,M) holds (x = $1
& y = $2 implies (for B being set st B in S for C being thin of M st x = B \/ C
holds y = M.B));
A1: ex B1 being set st B1 in S & {} c= B1 & M.B1 = 0.
proof
take {};
thus thesis by PROB_1:4,VALUED_0:def 19;
end;
{} is Subset of X by XBOOLE_1:2;
then reconsider C = {} as thin of M by A1,Def2;
A2: for x being object st x in COM(S,M)
ex y being object st y in ExtREAL & P[x, y]
proof
let x be object;
assume x in COM(S,M);
then consider B being set such that
A3: B in S & ex C being thin of M st x = B \/ C by Def3;
take M.B;
thus thesis by A3,Th19;
end;
consider comM being Function of COM(S,M),ExtREAL such that
A4: for x being object st x in COM(S,M) holds P[x,comM.x] from FUNCT_2:
sch 1( A2);
A5: for B being set st B in S for C being thin of M holds comM.(B \/ C) = M.B
proof
let B be set;
assume
A6: B in S;
let C be thin of M;
B \/ C in COM(S,M) by A6,Def3;
hence thesis by A4,A6;
end;
A7: for F being Sep_Sequence of COM(S,M) holds SUM(comM*F) = comM.(union rng F)
proof
let F be Sep_Sequence of COM(S,M);
consider G being sequence of S such that
A8: for n being Element of NAT holds G.n in MeasPart(F.n) by Th15;
consider H be sequence of bool X such that
A9: for n being Element of NAT holds H.n = F.n \ G.n by Th16;
A10: for n being Element of NAT holds G.n in S & G.n c= F.n & F.n \ G.n
is thin of M
proof
let n be Element of NAT;
G.n in MeasPart(F.n) by A8;
hence thesis by Def4;
end;
for n being Element of NAT holds H.n is thin of M
proof
let n be Element of NAT;
F.n \ G.n is thin of M by A10;
hence thesis by A9;
end;
then consider L being sequence of S such that
A11: for n being Element of NAT holds H.n c= L.n & M.(L.n) = 0. by Th17;
A12: for n,m being object st n <> m holds G.n misses G.m
proof
let n,m be object;
A13: dom F = NAT by FUNCT_2:def 1
.= dom G by FUNCT_2:def 1;
for n being object holds G.n c= F.n
proof
let n be object;
per cases;
suppose
n in dom F;
hence thesis by A10;
end;
suppose
A14: not n in dom F;
then F.n = {} by FUNCT_1:def 2
.= G.n by A13,A14,FUNCT_1:def 2;
hence thesis;
end;
end;
then
A15: G.n c= F.n & G.m c= F.m;
assume n <> m;
then F.n misses F.m by PROB_2:def 2;
then F.n /\ F.m = {};
then G.n /\ G.m = {} by A15,XBOOLE_1:3,27;
hence thesis;
end;
consider B being set such that
A16: B = union rng G;
A17: dom F = NAT by FUNCT_2:def 1;
A18: B c= union rng F
proof
let x be object;
assume x in B;
then consider Z being set such that
A19: x in Z and
A20: Z in rng G by A16,TARSKI:def 4;
dom G = NAT by FUNCT_2:def 1;
then consider n being object such that
A21: n in NAT and
A22: Z = G.n by A20,FUNCT_1:def 3;
reconsider n as Element of NAT by A21;
set P = F.n;
A23: G.n c= P by A10;
ex P being set st P in rng F & x in P
proof
take P;
thus thesis by A17,A19,A22,A23,FUNCT_1:def 3;
end;
hence thesis by TARSKI:def 4;
end;
A24: ex C being thin of M st union rng F = B \/ C
proof
for A being set st A in rng L holds A is measure_zero of M
proof
let A be set;
assume
A25: A in rng L;
dom L = NAT by FUNCT_2:def 1;
then
A26: ex n being object st n in NAT & A = L.n by A25,FUNCT_1:def 3;
rng L c= S by MEASURE2:def 1;
then reconsider A as Element of S by A25;
M.A = 0. by A11,A26;
hence thesis by MEASURE1:def 7;
end;
then union rng L is measure_zero of M by MEASURE2:14;
then
A27: M.(union rng L) = 0. by MEASURE1:def 7;
set C = union rng F \ B;
A28: union rng F = C \/ union rng F /\ B by XBOOLE_1:51
.= B \/ C by A18,XBOOLE_1:28;
reconsider C as Subset of X;
A29: C c= union rng H
proof
let x be object;
assume
A30: x in C;
then x in union rng F by XBOOLE_0:def 5;
then consider Z being set such that
A31: x in Z and
A32: Z in rng F by TARSKI:def 4;
consider n being object such that
A33: n in NAT and
A34: Z = F.n by A17,A32,FUNCT_1:def 3;
reconsider n as Element of NAT by A33;
A35: not x in union rng G by A16,A30,XBOOLE_0:def 5;
not x in G.n
proof
dom G = NAT by FUNCT_2:def 1;
then
A36: G.n in rng G by FUNCT_1:def 3;
assume x in G.n;
hence thesis by A35,A36,TARSKI:def 4;
end;
then
A37: x in F.n \ G.n by A31,A34,XBOOLE_0:def 5;
ex Z being set st x in Z & Z in rng H
proof
take H.n;
dom H = NAT by FUNCT_2:def 1;
hence thesis by A9,A37,FUNCT_1:def 3;
end;
hence thesis by TARSKI:def 4;
end;
union rng H c= union rng L
proof
let x be object;
assume x in union rng H;
then consider Z being set such that
A38: x in Z and
A39: Z in rng H by TARSKI:def 4;
dom H = NAT by FUNCT_2:def 1;
then consider n being object such that
A40: n in NAT and
A41: Z = H.n by A39,FUNCT_1:def 3;
reconsider n as Element of NAT by A40;
n in dom L by A40,FUNCT_2:def 1;
then
A42: L.n in rng L by FUNCT_1:def 3;
H.n c= L.n by A11;
hence thesis by A38,A41,A42,TARSKI:def 4;
end;
then C c= union rng L by A29;
then C is thin of M by A27,Def2;
then consider C being thin of M such that
A43: union rng F = B \/ C by A28;
take C;
thus thesis by A43;
end;
reconsider G as Sep_Sequence of S by A12,PROB_2:def 2;
A44: for n being Element of NAT holds comM.(F.n) = M.(G.n)
proof
let n be Element of NAT;
F.n \ G.n is thin of M by A10;
then consider C being thin of M such that
A45: C = F.n \ G.n;
F.n = (F.n /\ G.n) \/ (F.n \ G.n) by XBOOLE_1:51
.= G.n \/ C by A10,A45,XBOOLE_1:28;
hence thesis by A5;
end;
A46: for n being Element of NAT holds (comM*F).n = (M*G).n
proof
let n be Element of NAT;
(comM*F).n = comM.(F.n) by FUNCT_2:15
.= M.(G.n) by A44
.= (M*G).n by FUNCT_2:15;
hence thesis;
end;
then for n being Element of NAT holds (M*G).n <= (comM*F).n;
then
A47: SUM(M*G) <= SUM(comM*F) by SUPINF_2:43;
for n being Element of NAT holds (comM*F).n <= (M*G).n by A46;
then SUM(comM*F) <= SUM(M*G) by SUPINF_2:43;
then SUM(M*G) = M.(union rng G) & SUM(comM*F) = SUM(M*G) by A47,
MEASURE1:def 6,XXREAL_0:1;
hence thesis by A5,A16,A24;
end;
A48: for x being Element of COM(S,M) holds 0. <= comM.x
proof
let x be Element of COM(S,M);
consider B being set such that
A49: B in S and
A50: ex C being thin of M st x = B \/ C by Def3;
reconsider B as Element of S by A49;
comM.x = M.B by A4,A50;
hence thesis by MEASURE1:def 2;
end;
{} = B \/ C;
then comM.{} = M.{} by A5,PROB_1:4
.= 0. by VALUED_0:def 19;
then reconsider comM as sigma_Measure of COM(S,M) by A48,A7,MEASURE1:def 2
,def 6,VALUED_0:def 19;
take comM;
thus thesis by A5;
end;
uniqueness
proof
let M1,M2 be sigma_Measure of COM(S,M) such that
A51: for B being set st B in S for C being thin of M holds M1.(B \/ C)
= M.B and
A52: for B being set st B in S for C being thin of M holds M2.(B \/ C) = M.B;
for x being object st x in COM(S,M) holds M1.x = M2.x
proof
let x be object;
assume x in COM(S,M);
then consider B being set such that
A53: B in S & ex C being thin of M st x = B \/ C by Def3;
M1.x = M.B by A51,A53
.= M2.x by A52,A53;
hence thesis;
end;
hence thesis by FUNCT_2:12;
end;
end;
theorem
for S being SigmaField of X, M being sigma_Measure of S holds COM(M)
is complete
proof
let S be SigmaField of X, M be sigma_Measure of S;
for A being Subset of X, B being set st B in COM(S,M) holds (A c= B & (
COM(M)).B = 0. implies A in COM(S,M))
proof
let A be Subset of X;
let B be set;
assume
A1: B in COM(S,M);
assume that
A2: A c= B and
A3: (COM(M)).B = 0.;
ex B1 being set st (B1 in S & ex C1 being thin of M st A = B1 \/ C1)
proof
take {};
consider B2 being set such that
A4: B2 in S and
A5: ex C2 being thin of M st B = B2 \/ C2 by A1,Def3;
A6: M.B2 = 0. by A3,A4,A5,Def5;
consider C2 being thin of M such that
A7: B = B2 \/ C2 by A5;
set C1 = (A /\ B2) \/ (A /\ C2);
consider D2 being set such that
A8: D2 in S and
A9: C2 c= D2 and
A10: M.D2 = 0. by Def2;
set O = B2 \/ D2;
A /\ C2 c= C2 by XBOOLE_1:17;
then
A11: A /\ B2 c= B2 & A /\ C2 c= D2 by A9,XBOOLE_1:17;
ex O being set st O in S & C1 c= O & M.O = 0.
proof
reconsider B2,D2 as Element of S by A4,A8;
reconsider O1 = O as Element of S by A4,A8,FINSUB_1:def 1;
take O;
M.(B2 \/ D2) <= 0. + 0. & 0. <= M.O1 by A6,A10,MEASURE1:33,def 2;
hence thesis by A11,XBOOLE_1:13,XXREAL_0:1;
end;
then
A12: C1 is thin of M by Def2;
A = A /\ (B2 \/ C2) by A2,A7,XBOOLE_1:28
.= {} \/ C1 by XBOOLE_1:23;
hence thesis by A12,PROB_1:4;
end;
hence thesis by Def3;
end;
hence thesis;
end;