Several Properties of the $\sigma$-additive Measure

by
Jozef Bialas

Copyright (c) 1991 Association of Mizar Users

MML identifier: MEASURE2
[ MML identifier index ]

environ

vocabulary MEASURE1, FUNCT_1, SUPINF_2, BOOLE, SETFAM_1, TARSKI, RELAT_1,
ARYTM_3, RLVECT_1, PROB_1, ORDINAL2, MEASURE2;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, RELAT_1,
FUNCT_1, FUNCT_2, NAT_1, SETFAM_1, SUPINF_1, SUPINF_2, MEASURE1;
constructors NAT_1, SUPINF_2, MEASURE1, PROB_2, MEMBERED, XBOOLE_0;
clusters SUBSET_1, SUPINF_1, MEASURE1, RELSET_1, ARYTM_3, MEMBERED, ZFMISC_1,
XBOOLE_0, NUMBERS, ORDINAL2;
requirements NUMERALS, SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0;
theorems TARSKI, FUNCT_1, FUNCT_2, ZFMISC_1, NAT_1, SETFAM_1, SUPINF_1,
SUPINF_2, MEASURE1, ENUMSET1, REAL_1, RELSET_1, PROB_2, XBOOLE_0,
XBOOLE_1;
schemes NAT_1, RECDEF_1;

begin
::
::         Some useful theorems about measures and functions
::

reserve X for set;

theorem Th1:
for S being sigma_Field_Subset of X,
M being sigma_Measure of S,
F being Function of NAT,S holds
M*F is nonnegative
proof
let S be sigma_Field_Subset of X,
M be sigma_Measure of S,
F be Function of NAT,S;
M is nonnegative by MEASURE1:def 11;
hence thesis by MEASURE1:54;
end;

definition
let X be set;
let S be sigma_Field_Subset of X;
mode N_Measure_fam of S -> N_Sub_set_fam of X means
:Def1: it c= S;
existence
proof
A1:{} is Subset of X by XBOOLE_1:2;
{{},{}} = {{}} by ENUMSET1:69;
then A2:{{}} is N_Sub_set_fam of X by A1,MEASURE1:41;
A3:{} in S by MEASURE1:45;
consider C being N_Sub_set_fam of X such that
A4:C = {{}} by A2;
take C;
thus thesis by A3,A4,ZFMISC_1:37;
end;
end;

canceled;

theorem Th3:
for S being sigma_Field_Subset of X,
T being N_Measure_fam of S holds
meet T in S & union T in S
proof
let S be sigma_Field_Subset of X,
T be N_Measure_fam of S;
T c= S by Def1;
hence thesis by MEASURE1:49,def 9;
end;

definition
let X be set;
let S be sigma_Field_Subset of X;
let T be N_Measure_fam of S;
redefine func meet T -> Element of S;
coherence by Th3;

redefine func union T -> Element of S;
coherence by Th3;
end;

theorem Th4:
for S being sigma_Field_Subset of X,
N being Function of NAT,S holds
ex F being Function of NAT,S st
F.0 = N.0 & for n being Element of NAT holds F.(n+1) = N.(n+1) \ N.n
proof
let S be sigma_Field_Subset of X,
N be Function of NAT,S;
reconsider S as non empty set;
defpred P[set,set,set] means
for A,B being Element of S,c being Nat holds
c = $1 & A =$2 & B = $3 implies B = N.(c+1) \ N.(c); A1:for c being Nat for A being Element of S ex B being Element of S st P[c,A,B] proof let c be Nat; let A be Element of S; reconsider B = N.(c+1) \ N.c as Element of S; take B; thus thesis; end; reconsider A = N.0 as Element of S; consider F being Function of NAT,S such that A2:(F.0 = A & for n being Element of NAT holds P[n,F.n,F.(n+1)]) from RecExD(A1); for n being Element of NAT holds F.(n + 1) = N.(n+1) \ N.n proof let n be Element of NAT; for a,b being Element of S,s being Nat st s = n & a = F.n & b = F.(n+1) holds b = N.(s+1) \ N.s by A2; hence thesis; end; hence thesis by A2; end; theorem Th5: for S being sigma_Field_Subset of X, N being Function of NAT,S holds ex F being Function of NAT,S st F.0 = N.0 & for n being Element of NAT holds F.(n+1) = N.(n+1) \/ F.n proof let S be sigma_Field_Subset of X, N be Function of NAT,S; defpred P[set,set,set] means for A,B being Element of S,c being Nat holds (c =$1 & A = $2 & B =$3 implies B = (N.(c+1)) \/ A);
A1:for c being Nat for A being Element of S
ex B being Element of S st P[c,A,B]
proof
let c be Nat;
let A be Element of S;
reconsider B = N.(c+1) \/ A as Element of S;
take B;
thus thesis;
end;
consider F being Function of NAT,S such that
A2:F.0 = (N.0) & for n being Element of NAT holds P[n,F.n,F.(n+1)]
from RecExD(A1);
for n being Element of NAT holds F.(n + 1) = N.(n+1) \/ F.n by A2;
hence thesis by A2;
end;

theorem Th6:
for S being non empty Subset-Family of X,
N,F being Function of NAT,S holds
F.0 = N.0 & (for n being Element of NAT holds F.(n+1) = N.(n+1) \/ F.n)
implies (for r being set for n being Nat holds (r in F.n iff
ex k being Nat st (k <= n & r in N.k)))
proof
let S be non empty Subset-Family of X,
N,F be Function of NAT,S;
assume
A1:F.0 = N.0 & (for n being Element of NAT holds F.(n+1) = N.(n+1) \/ F.n);
let r be set;
let n be Nat;
thus r in F.n implies ex k being Nat st k <= n & r in N.k
proof
defpred P[Nat] means r in F.$1; assume A2:r in F.n; then A3:ex n being Nat st P[n]; ex s being Nat st P[s] & for k being Nat st P[k] holds s <= k from Min(A3); then consider s being Nat such that A4:r in F.s & for k being Nat st r in F.k holds s <= k; A5:s=0 implies ex k being Nat st k <= n & r in N.k proof assume A6: s = 0; take 0; thus thesis by A1,A4,A6,NAT_1:18; end; (ex k being Nat st s = k + 1) implies (ex k being Nat st k <= n & r in N.k) proof given k being Nat such that A7:s = k + 1; A8: F.s = N.s \/ F.k by A1,A7; A9: not r in F.k proof assume r in F.k; then s <= k by A4; hence thesis by A7,NAT_1:38; end; take s; thus thesis by A2,A4,A8,A9,XBOOLE_0:def 2; end; hence thesis by A5,NAT_1:22; end; defpred P[Nat] means (ex k being Nat st k <=$1 & r in N.k) implies r in F.$1; A10: P[0] by A1,NAT_1:19; A11:for n being Nat st P[n] holds P[n+1] proof let n be Nat; assume A12:(ex k being Nat st k <= n & r in N.k) implies r in F.n; given k being Nat such that A13:k <= n+1 & r in N.k; A14:F.(n+1) = N.(n+1) \/ F.n by A1; k <= n or k = n + 1 by A13,NAT_1:26; hence thesis by A12,A13,A14,XBOOLE_0:def 2; end; for n being Nat holds P[n] from Ind(A10,A11); hence thesis; end; theorem Th7: for S being non empty Subset-Family of X, N,F being Function of NAT,S holds (F.0 = N.0 & (for n being Element of NAT holds F.(n+1) = N.(n+1) \/ F.n) implies for n,m being Nat st n < m holds F.n c= F.m) proof let S be non empty Subset-Family of X, N,F be Function of NAT,S; assume A1:F.0 = N.0 & for n being Element of NAT holds F.(n+1) = N.(n+1) \/ F.n; defpred X[Nat] means for m being Nat st$1 < m holds F.$1 c= F.m; A2: X[0] proof let m be Nat; assume A3:0 < m; A4:for k being Nat st 0 < k + 1 holds F.0 c= F.(k+1) proof defpred P[Nat] means 0 <$1 + 1 implies F.0 c= F.($1+1); F.(0+1) = N.(0+1) \/ F.0 by A1; then A5: P[0] by XBOOLE_1:7; A6:for k being Nat st P[k] holds P[k+1] proof let k be Nat; assume A7:0 < k + 1 implies F.0 c= F.(k+1); F.(k+1+1) = N.(k+1+1) \/ F.(k+1) by A1; then A8:F.(k+1) c= F.(k+1+1) by XBOOLE_1:7; 0 <= k by NAT_1:18; hence thesis by A7,A8,NAT_1:38,XBOOLE_1:1; end; thus for k being Nat holds P[k] from Ind(A5,A6); end; ex k being Nat st m = k + 1 by A3,NAT_1:22; hence thesis by A3,A4; end; A9:for n being Nat st X[n] holds X[n+1] proof let n be Nat; assume A10:for m being Nat st n < m holds F.n c= F.m; let m be Nat; assume A11:n+1 < m; let r be set; assume A12:r in F.(n+1); A13: F.(n+1) = N.(n+1) \/ F.n by A1; A14:r in N.(n+1) implies r in F.m by A1,A11,Th6; r in F.n implies r in F.m proof assume A15:r in F.n; n < m implies r in F.m proof assume n < m; then F.n c= F.m by A10; hence thesis by A15; end; hence thesis by A11,NAT_1:38; end; hence thesis by A12,A13,A14,XBOOLE_0:def 2; end; thus for n being Nat holds X[n] from Ind(A2,A9); end; theorem Th8: for S being non empty Subset-Family of X, N, G, F being Function of NAT,S holds (G.0 = N.0 & (for n being Element of NAT holds G.(n+1) = N.(n+1) \/ G.n) & F.0 = N.0 & (for n being Element of NAT holds F.(n+1) = N.(n+1) \ G.n)) implies (for n,m being Nat st n <= m holds F.n c= G.m) proof let S be non empty Subset-Family of X, N, G, F be Function of NAT,S; assume A1:(G.0 = N.0) & (for n being Element of NAT holds G.(n+1) = N.(n+1) \/ G.n) & (F.0 = N.0) & (for n being Element of NAT holds F.(n+1) = N.(n+1) \ G.n); A2:for n being Nat holds F.n c= G.n proof defpred P[Nat] means F.$1 c= G.$1; A3: P[0] by A1; A4:for n being Nat st P[n] holds P[n+1] proof let n be Nat; assume F.n c= G.n; F.(n+1) = N.(n+1) \ G.n by A1; then A5:F.(n+1) c= N.(n+1) by XBOOLE_1:36; G.(n+1) = N.(n+1) \/ G.n by A1; then N.(n+1) c= G.(n+1) by XBOOLE_1:7; hence thesis by A5,XBOOLE_1:1; end; thus for n being Nat holds P[n] from Ind(A3,A4); end; let n,m be Nat; assume n <= m; then A6:n = m or n < m by REAL_1:def 5; n < m implies F.n c= G.m proof assume A7:n < m; A8:F.n c= G.n by A2; G.n c= G.m by A1,A7,Th7; hence thesis by A8,XBOOLE_1:1; end; hence thesis by A2,A6; end; theorem Th9: for S being sigma_Field_Subset of X holds for N, G being Function of NAT,S holds ex F being Function of NAT,S st F.0 = N.0 & for n being Element of NAT holds F.(n+1) = N.(n+1) \ G.n proof let S be sigma_Field_Subset of X; let N, G be Function of NAT,S; defpred P[set,set,set] means for A,B being Element of S,c being Nat holds (c =$1 & A = $2 & B =$3 implies B = (N.(c+1)) \ G.c);
A1:for c being Nat for A being Element of S
ex B being Element of S st P[c,A,B]
proof
let c be Nat;
let A be Element of S;
consider B being set such that
A2:B = N.(c+1) \ G.c;
reconsider B as Element of S by A2;
take B;
thus thesis by A2;
end;
consider F being Function of NAT,S such that
A3:F.0 = N.0 & for n being Element of NAT holds P[n,F.n,F.(n+1)]
from RecExD(A1);
for n being Element of NAT holds F.(n + 1) = N.(n+1) \ G.n
proof
let n be Element of NAT;
for a,b being Element of S,s being Nat st
s = n & a = F.n & b = F.(n+1) holds b = N.(s+1) \ G.s by A3;
hence thesis;
end;
hence thesis by A3;
end;

theorem
for S being sigma_Field_Subset of X holds
for N being Function of NAT,S holds
ex F being Function of NAT,S st
F.0 = {} & for n being Element of NAT holds F.(n+1) = N.0 \ N.n
proof
let S be sigma_Field_Subset of X;
let N be Function of NAT,S;
defpred P[set,set,set] means
for A,B being Element of S,c being Nat holds
(c = $1 & A =$2 & B = $3 implies B = N.0 \ N.(c)); A1:for c being Nat for A being Element of S ex B being Element of S st P[c,A,B] proof let c be Nat; let A be Element of S; reconsider B = N.0 \ N.c as Element of S; take B; thus thesis; end; reconsider A = {} as Element of S by MEASURE1:45; consider F being Function of NAT,S such that A2:(F.0 = A & for n being Element of NAT holds P[n,F.n,F.(n+1)]) from RecExD(A1); for n being Element of NAT holds F.(n + 1) = N.0 \ N.n proof let n be Element of NAT; for a,b being Element of S,s being Nat st s = n & a = F.n & b = F.(n+1) holds b = N.0 \ N.s by A2; hence thesis; end; hence thesis by A2; end; theorem Th11: for S being sigma_Field_Subset of X holds for N, G, F being Function of NAT,S holds (G.0 = N.0 & (for n being Element of NAT holds G.(n+1) = N.(n+1) \/ G.n) & F.0 = N.0 & (for n being Element of NAT holds F.(n+1) = N.(n+1) \ G.n)) implies (for n,m being Nat st n < m holds F.n misses F.m) proof let S be sigma_Field_Subset of X; let N, G, F be Function of NAT,S; assume A1:G.0 = N.0 & (for n being Element of NAT holds G.(n+1) = N.(n+1) \/ G.n) & F.0 = N.0 & (for n being Element of NAT holds F.(n+1) = N.(n+1) \ G.n); let n,m be Nat; assume A2:n < m; then 0 <= m & 0 <> m by NAT_1:18; then consider k being Nat such that A3:m = k + 1 by NAT_1:22; F.(k+1) = N.(k+1) \ G.k by A1; then A4:G.k misses F.(k+1) by XBOOLE_1:79; n <= k by A2,A3,NAT_1:38; then F.n c= G.k by A1,Th8; hence F.n /\ F.m = (F.n /\ G.k) /\ F.(k+1) by A3,XBOOLE_1:28 .= F.n /\ (G.k /\ F.(k+1)) by XBOOLE_1:16 .= F.n /\ {} by A4,XBOOLE_0:def 7 .= {}; end; canceled; theorem Th13: for S being sigma_Field_Subset of X, M being sigma_Measure of S, T being N_Measure_fam of S, F being Function of NAT,S st T = rng F holds M.(union T) <=' SUM(M*F) proof let S be sigma_Field_Subset of X, M be sigma_Measure of S, T be N_Measure_fam of S, F be Function of NAT,S; assume A1:T = rng F; consider G being Function of NAT,S such that A2:G.0 = F.0 & for n being Element of NAT holds G.(n+1) = F.(n+1) \/ G.n by Th5; consider H being Function of NAT,S such that A3:H.0 = F.0 & for n being Element of NAT holds H.(n+1) = F.(n+1) \ G.n by Th9; A4:for n being Element of NAT holds H.n c= F.n proof let n be Element of NAT; A5:n=0 or ex k being Nat st n = k + 1 by NAT_1:22; (ex k being Nat st n = k + 1) implies H.n c= F.n proof given k being Nat such that A6:n = k + 1; H.n = F.n \ G.k by A3,A6; hence thesis by XBOOLE_1:36; end; hence thesis by A3,A5; end; A7:for n being Element of NAT holds (M*H).n <=' (M*F).n proof let n be Element of NAT; NAT = dom(M*H) & NAT = dom(M*F) by FUNCT_2:def 1; then A8:(M*H).n = M.(H.n) & (M*F).n = M.(F.n) by FUNCT_1:22; consider A,B being Element of S such that A9:A = H.n & B = F.n; A c= B by A4,A9; hence thesis by A8,A9,MEASURE1:62; end; A10: M*H is nonnegative by Th1; for n,m being set st n <> m holds H.n misses H.m proof let n,m be set; assume A11: n <> m; per cases; suppose n in dom H & m in dom H; then reconsider n'=n,m'=m as Nat by FUNCT_2:def 1; A12:n' < m' implies H.n misses H.m by A2,A3,Th11; m' < n' implies H.m misses H.n by A2,A3,Th11; hence H.n misses H.m by A11,A12,REAL_1:def 5; suppose not (n in dom H & m in dom H); then H.n = {} or H.m = {} by FUNCT_1:def 4; hence thesis by XBOOLE_1:65; end; then H is Sep_Sequence of S by PROB_2:def 3; then A13:SUM(M*H) = M.(union rng H) by MEASURE1:def 11; union rng H = union rng F proof thus union rng H c= union rng F proof let r be set; assume r in union rng H; then consider E being set such that A14:r in E & E in rng H by TARSKI:def 4; consider s being set such that A15:s in dom H & E = H.s by A14,FUNCT_1:def 5; reconsider s as Element of NAT by A15,FUNCT_2:def 1; A16: E c= F.s by A4,A15; F.s in rng F by FUNCT_2:6; hence thesis by A14,A16,TARSKI:def 4; end; let r be set; assume r in union rng F; then consider E being set such that A17:r in E & E in rng F by TARSKI:def 4; consider s being set such that A18:s in dom F & E = F.s by A17,FUNCT_1:def 5; reconsider s as Element of NAT by A18,FUNCT_2:def 1; ex s1 being Element of NAT st r in H.s1 proof defpred P[Nat] means r in F.$1;
r in F.s by A17,A18;
then A19:ex k being Nat st P[k];
ex k being Nat st P[k] &
for n being Nat st P[n] holds k <= n from Min(A19);
then consider k being Nat such that
A20:r in F.k & for n being Nat st r in F.n holds k <= n;
A21:k=0 implies ex s1 being Element of NAT st r in H.s1 by A3,A20;
(ex l being Nat st k = l + 1) implies
(ex s1 being Element of NAT st r in H.s1)
proof
given l being Nat such that
A22:k = l + 1;
A23:not r in G.l
proof
assume r in G.l;
then consider i being Nat such that
A24:i <= l & r in F.i by A2,Th6;
k <= i by A20,A24;
hence thesis by A22,A24,NAT_1:38;
end;
A25:           H.(l+1) = F.(l+1) \ G.l by A3;
take k;
thus thesis by A20,A22,A23,A25,XBOOLE_0:def 4;
end;
hence thesis by A21,NAT_1:22;
end;
then consider s1 being Element of NAT such that
A26:r in H.s1;
H.s1 in rng H by FUNCT_2:6;
hence thesis by A26,TARSKI:def 4;
end;
hence thesis by A1,A7,A10,A13,SUPINF_2:62;
end;

theorem Th14:
for S being sigma_Field_Subset of X,
T being N_Measure_fam of S holds
ex F being Function of NAT,S st T = rng F
proof
let S be sigma_Field_Subset of X,
T be N_Measure_fam of S;
consider F being Function of NAT,bool X such that
A1:T = rng F by SUPINF_2:def 14;
rng F c= S by A1,Def1;
then F is Function of NAT,S by FUNCT_2:8;
then consider F being Function of NAT,S such that
A2:T = rng F by A1;
take F;
thus thesis by A2;
end;

theorem Th15:
for S being sigma_Field_Subset of X,
N, F being Function of NAT,S st
(F.0 = {} &
for n being Element of NAT holds (F.(n+1) = N.0 \ N.n & N.(n+1) c= N.n))
holds
for n being Element of NAT holds F.n c= F.(n+1)
proof
let S be sigma_Field_Subset of X;
let N,F be Function of NAT,S;
assume
A1:F.0 = {} & for n being Element of NAT holds
F.(n+1) = N.0 \ N.n & N.(n+1) c= N.n;
let n be Element of NAT;
defpred P[Nat] means F.$1 c= F.($1+1);
F.(0+1) = N.0 \ N.0 by A1;
then A2: P[0] by A1,XBOOLE_1:37;
A3:for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume F.n c= F.(n+1);
A4:F.((n+1)+1) = N.0 \ N.(n+1) by A1;
N.(n+1) c= N.n by A1;
then N.0 \ N.n c= F.((n+1)+1) by A4,XBOOLE_1:34;
hence thesis by A1;
end;
for n being Element of NAT holds P[n] from Ind(A2,A3);
hence thesis;
end;

theorem
for S being sigma_Field_Subset of X,
M being sigma_Measure of S,
T being N_Measure_fam of S holds
(for A being set holds A in T implies A is measure_zero of M) implies
union T is measure_zero of M
proof
let S be sigma_Field_Subset of X,
M be sigma_Measure of S,
T be N_Measure_fam of S;
assume
A1:for A being set holds A in T implies A is measure_zero of M;
consider F being Function of NAT,S such that
A2:T = rng F by Th14;
set G = M*F;
A3:G is nonnegative by Th1;
A4:for r being Nat holds 0 <= r implies G.r = 0.
proof
let r be Nat;
F.r in T & F.r is Element of S by A2,FUNCT_2:6;
then F.r is measure_zero of M by A1;
then M.(F.r) = 0. by MEASURE1:def 13;
hence thesis by FUNCT_2:21;
end;
then SUM(G) = Ser(G).0 by A3,SUPINF_2:67;
then SUM(G) = G.0 by SUPINF_2:63;
then SUM(M*F) = 0. by A4;
then A5:M.(union T) <=' 0. by A2,Th13;
M is nonnegative by MEASURE1:def 11;
then 0. <=' M.(union T) by MEASURE1:def 4;
then M.(union T) = 0. by A5,SUPINF_1:22;
hence thesis by MEASURE1:def 13;
end;

theorem Th17:
for S being sigma_Field_Subset of X,
M being sigma_Measure of S,
T being N_Measure_fam of S st
(ex A being set st A in T & A is measure_zero of M) holds
meet T is measure_zero of M
proof
let S be sigma_Field_Subset of X,
M be sigma_Measure of S,
T be N_Measure_fam of S;
given A being set such that A1: A in T & A is measure_zero of M;
meet T c= A by A1,SETFAM_1:4;
hence thesis by A1,MEASURE1:69;
end;

theorem
for S being sigma_Field_Subset of X,
M being sigma_Measure of S,
T being N_Measure_fam of S st
(for A being set holds A in T implies A is measure_zero of M) holds
meet T is measure_zero of M
proof
let S be sigma_Field_Subset of X,
M be sigma_Measure of S,
T be N_Measure_fam of S;
assume
A1:for A being set holds A in T implies A is measure_zero of M;
ex A being set st A in T & A is measure_zero of M
proof
consider F being Function of NAT,bool X such that
A2:   T = rng F by SUPINF_2:def 14;
A3:   F.0 in T by A2,FUNCT_2:6;
take F.0;
thus thesis by A1,A3;
end;
hence thesis by Th17;
end;

definition
let X be set;
let S be sigma_Field_Subset of X;
let IT be N_Measure_fam of S;
attr IT is non-decreasing means
:Def2:ex F being Function of NAT,S st
IT = rng F & for n being Element of NAT holds F.n c= F.(n+1);
end;

definition
let X be set;
let S be sigma_Field_Subset of X;
cluster non-decreasing N_Measure_fam of S;
existence
proof
{} in S by MEASURE1:45;
then consider A being set such that
A1:A in S;
reconsider A as Subset of X by A1;
consider B,C being Subset of X such that
A2:B = A & C = A;
consider F being Function of NAT,bool X such that
A3:rng F = {B,C} &
F.0 = B & for n being Nat st 0 < n holds F.n = C by MEASURE1:40;
A4:rng F = {A} &
F.0 = A & for n being Nat st 0 < n holds F.n = A by A2,A3,ENUMSET1:69;
then rng F c= S by A1,ZFMISC_1:37;
then reconsider F as Function of NAT,S by FUNCT_2:8;
A5:{A} is N_Sub_set_fam of X by A4,MEASURE1:6,SUPINF_2:def 14;
{A} c= S by A1,ZFMISC_1:37;
then reconsider T = {A} as N_Measure_fam of S by A5,Def1;
take T,F;
for n being Element of NAT holds F.n c= F.(n+1)
proof
let n be Element of NAT;
for n being Nat holds F.n = A
proof
let n be Nat;
n = 0 or 0 < n by NAT_1:19;
hence thesis by A2,A3;
end;
then F.n = A & F.(n + 1) = A;
hence thesis;
end;
hence thesis by A2,A3,ENUMSET1:69;
end;
end;

definition
let X be set;
let S be sigma_Field_Subset of X;
let IT be N_Measure_fam of S;
attr IT is non-increasing means
ex F being Function of NAT,S st
(IT = rng F &
for n being Element of NAT holds F.(n+1) c= F.n);
end;

definition
let X be set;
let S be sigma_Field_Subset of X;
cluster non-increasing N_Measure_fam of S;
existence
proof
{} in S by MEASURE1:45;
then consider A being set such that
A1:A in S;
reconsider A as Subset of X by A1;
set B = A, C = A;
consider F being Function of NAT,bool X such that
A2:rng F = {B,C} &
F.0 = B & for n being Nat st 0 < n holds F.n = C by MEASURE1:40;
A3:rng F = {A} &
F.0 = A & for n being Nat st 0 < n holds F.n = A by A2,ENUMSET1:69;
then rng F c= S by A1,ZFMISC_1:37;
then reconsider F as Function of NAT,S by FUNCT_2:8;
A4:{A} is N_Sub_set_fam of X by A3,MEASURE1:6,SUPINF_2:def 14;
{A} c= S by A1,ZFMISC_1:37;
then reconsider T = {A} as N_Measure_fam of S by A4,Def1;
take T,F;
for n being Element of NAT holds F.(n+1) c= F.n
proof
let n be Element of NAT;
for n being Nat holds F.n = A
proof
let n be Nat;
n = 0 or 0 < n by NAT_1:19;
hence thesis by A2;
end;
then F.n = A & F.(n + 1) = A;
hence thesis;
end;
hence thesis by A2,ENUMSET1:69;
end;
end;

canceled 2;

theorem
for S being sigma_Field_Subset of X,
N,F being Function of NAT,S holds
(F.0 = {} & for n being Element of NAT holds
(F.(n+1) = N.0 \ N.n & N.(n+1) c= N.n)) implies
rng F is non-decreasing N_Measure_fam of S
proof
let S be sigma_Field_Subset of X,
N,F be Function of NAT,S;
assume F.0 = {} & for n being Element of NAT holds
F.(n+1) = N.0 \ N.n & N.(n+1) c= N.n;
then A1:for n being Element of NAT holds F.n c= F.(n+1) by Th15;
A2:rng F c= S by RELSET_1:12;
rng F is N_Sub_set_fam of X by MEASURE1:52;
hence thesis by A1,A2,Def1,Def2;
end;

theorem Th22:
for S being non empty Subset-Family of X,
N being Function of NAT,S holds
(for n being Element of NAT holds N.n c= N.(n+1))
implies (for m,n being Nat st n < m holds N.n c= N.m)
proof
let S be non empty Subset-Family of X,
N be Function of NAT,S;
assume
A1:for n being Element of NAT holds N.n c= N.(n+1);
defpred P[Nat] means for n being Nat st n < $1 holds N.n c= N.$1;
A2: P[0] by NAT_1:18;
A3:for m being Nat st P[m] holds P[m+1]
proof
let m be Nat;
assume
A4:for n being Nat st n < m holds N.n c= N.m;
let n be Nat;
assume
A5:n < m+1;
A6:n = m or n < m
proof
assume
A7:n <> m & not n < m;
n <= m by A5,NAT_1:38;
hence thesis by A7,REAL_1:def 5;
end;
n < m implies N.n c= N.(m+1)
proof
assume n < m;
then A8:N.n c= N.m by A4;
N.m c= N.(m+1) by A1;
hence thesis by A8,XBOOLE_1:1;
end;
hence thesis by A1,A6;
end;
thus for m being Nat holds P[m] from Ind(A2,A3);
end;

theorem Th23:
for S being sigma_Field_Subset of X,
N,F being Function of NAT,S holds
(F.0 = N.0 & for n being Element of NAT holds
(F.(n+1) = N.(n+1) \ N.n & N.n c= N.(n+1)))
implies (for n,m being Nat st n < m holds F.n misses F.m)
proof
let S be sigma_Field_Subset of X,
N,F be Function of NAT,S;
assume
A1:F.0 = N.0 & for n being Element of NAT holds
(F.(n+1) = N.(n+1) \ N.n & N.n c= N.(n+1));
let n,m be Nat;
assume
A2:n < m;
then 0 <= m & 0 <> m by NAT_1:18;
then consider k being Nat such that
A3:m = k + 1 by NAT_1:22;
F.(k+1) = N.(k+1) \ N.k by A1;
then A4:N.k misses F.(k+1) by XBOOLE_1:79;
A5:n <= k by A2,A3,NAT_1:38;
F.n c= N.k
proof
A6:for n being Nat holds F.n c= N.n
proof
defpred P[Nat] means F.$1 c= N.$1;
A7: P[0] by A1;
A8:for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume F.n c= N.n;
F.(n+1) = N.(n+1) \ N.n by A1;
hence thesis by XBOOLE_1:36;
end;
thus for n being Nat holds P[n] from Ind(A7,A8);
end;
for n,m being Nat st n <= m holds F.n c= N.m
proof
let n,m be Nat;
assume n <= m;
then A9:n = m or n < m by REAL_1:def 5;
n < m implies F.n c= N.m
proof
assume
A10:n < m;
A11:F.n c= N.n by A6;
N.n c= N.m by A1,A10,Th22;
hence thesis by A11,XBOOLE_1:1;
end;
hence thesis by A6,A9;
end;
hence thesis by A5;
end;
then F.n /\ F.(k+1) = (F.n /\ N.k) /\ F.(k+1) by XBOOLE_1:28
.= F.n /\ (N.k /\ F.(k+1)) by XBOOLE_1:16
.= F.n /\ {} by A4,XBOOLE_0:def 7
.= {};
hence thesis by A3,XBOOLE_0:def 7;
end;

theorem Th24:
for S being sigma_Field_Subset of X,
N,F being Function of NAT,S holds
(F.0 = N.0 & for n being Element of NAT holds
(F.(n+1) = N.(n+1) \ N.n & N.n c= N.(n+1)))
implies union rng F = union rng N
proof
let S be sigma_Field_Subset of X,
N,F be Function of NAT,S;
assume
A1:F.0 = N.0 & for n being Element of NAT holds
F.(n+1) = N.(n+1) \ N.n & N.n c= N.(n+1);
thus union rng F c= union rng N
proof
let x be set;
assume x in union rng F;
then consider Y being set such that
A2:x in Y & Y in rng F by TARSKI:def 4;
consider n being set such that
A3:n in dom F & Y = F.n by A2,FUNCT_1:def 5;
reconsider n as Nat by A3,FUNCT_2:def 1;
A4:n=0 implies ex Z being set st x in Z & Z in rng N
proof
assume
A5:      n=0;
take N.0;
thus thesis by A1,A2,A3,A5,FUNCT_2:6;
end;
ex Z being set st x in Z & Z in rng N
proof
(ex k being Nat st n = k + 1) implies
(ex Z being set st x in Z & Z in rng N)
proof
given k being Nat such that
A6:n = k + 1;
Y=N.(k+1) \ N.k by A1,A3,A6;
then A7:x in N.(k+1) by A2,XBOOLE_0:def 4;
consider Z being set such that
A8:Z = N.(k+1);
Z in rng N by A8,FUNCT_2:6;
hence thesis by A7,A8;
end;
hence thesis by A4,NAT_1:22;
end;
hence thesis by TARSKI:def 4;
end;
let x be set;
assume x in union rng N;
then consider Y being set such that
A9:x in Y & Y in rng N by TARSKI:def 4;
consider n being set such that
A10:n in dom N & Y = N.n by A9,FUNCT_1:def 5;
reconsider n as Nat by A10,FUNCT_2:def 1;
ex Z being set st x in Z & Z in rng F
proof
ex s being Element of NAT st x in F.s
proof
defpred P[Nat] means x in N.$1; x in N.n by A9,A10; then A11:ex k being Nat st P[k]; ex k being Nat st P[k] & for r being Nat st P[r] holds k <= r from Min(A11); then consider k being Nat such that A12:x in N.k & for r being Nat st x in N.r holds k <= r; A13:k=0 implies (ex s being Element of NAT st x in F.s) by A1,A12; (ex l being Nat st k = l + 1) implies (ex s being Element of NAT st x in F.s) proof given l being Nat such that A14:k = l + 1; A15:not x in N.l proof assume x in N.l; then l + 1 <= l by A12,A14; hence thesis by NAT_1:38; end; A16: F.(l+1) = N.(l+1) \ N.l by A1; take k; thus thesis by A12,A14,A15,A16,XBOOLE_0:def 4; end; hence thesis by A13,NAT_1:22; end; then consider s being Element of NAT such that A17:x in F.s; F.s in rng F by FUNCT_2:6; hence thesis by A17; end; hence thesis by TARSKI:def 4; end; theorem Th25: for S being sigma_Field_Subset of X, N,F being Function of NAT,S holds (F.0 = N.0 & for n being Element of NAT holds (F.(n+1) = N.(n+1) \ N.n & N.n c= N.(n+1))) implies F is Sep_Sequence of S proof let S be sigma_Field_Subset of X, N,F be Function of NAT,S; assume A1:F.0 = N.0 & for n being Element of NAT holds F.(n+1) = N.(n+1) \ N.n & N.n c= N.(n+1); for n,m being set st n <> m holds F.n misses F.m proof let n,m be set; assume A2: n <> m; per cases; suppose n in dom F & m in dom F; then reconsider n'=n,m'=m as Nat by FUNCT_2:def 1; A3:n' < m' implies F.n misses F.m by A1,Th23; m' < n' implies F.m misses F.n by A1,Th23; hence F.n misses F.m by A2,A3,REAL_1:def 5; suppose not (n in dom F & m in dom F); then F.n = {} or F.m = {} by FUNCT_1:def 4; hence thesis by XBOOLE_1:65; end; hence thesis by PROB_2:def 3; end; theorem for S being sigma_Field_Subset of X, N,F being Function of NAT,S holds (F.0 = N.0 & for n being Element of NAT holds (F.(n+1) = N.(n+1) \ N.n & N.n c= N.(n+1))) implies (N.0 = F.0 & for n being Element of NAT holds N.(n+1) = F.(n+1) \/ N.n) proof let S be sigma_Field_Subset of X, N,F be Function of NAT,S; assume A1:F.0 = N.0 & for n being Element of NAT holds F.(n+1) = N.(n+1) \ N.n & N.n c= N.(n+1); for n being Element of NAT holds N.(n+1) = F.(n+1) \/ N.n proof let n be Element of NAT; F.(n+1) = N.(n+1) \ N.n & N.n c= N.(n+1) by A1; hence thesis by XBOOLE_1:45; end; hence thesis by A1; end; theorem for S being sigma_Field_Subset of X, M being sigma_Measure of S, F being Function of NAT,S st (for n being Element of NAT holds F.n c= F.(n+1)) holds M.(union rng F) = sup(rng (M*F)) proof let S be sigma_Field_Subset of X; let M be sigma_Measure of S; let F be Function of NAT,S; assume A1:for n being Element of NAT holds F.n c= F.(n+1); consider G being Function of NAT,S such that A2:G.0 = F.0 & for n being Element of NAT holds G.(n+1) = F.(n+1) \ F.n by Th4; A3:G is Sep_Sequence of S by A1,A2,Th25; A4:rng Ser(M*G) = rng (M*F) proof A5:dom Ser(M*G) = NAT & dom (M*F) = NAT by FUNCT_2:def 1; for m being set st m in NAT holds Ser(M*G).m = (M*F).m proof let m be set; assume A6:m in NAT; defpred P[Nat] means Ser(M*G).$1 = (M*F).\$1;
A7:   P[0]
proof
thus Ser(M*G).0 = (M*G).0 by SUPINF_2:63
.= M.(F.0) by A2,FUNCT_2:21
.= (M*F).0 by FUNCT_2:21;
end;
A8:for m being Nat holds P[m] implies P[m+1]
proof
let m be Nat;
assume
A9:Ser(M*G).m = (M*F).m;
A10:(M*G).(m+1) = M.(G.(m+1)) & (M*F).(m+1) = M.(F.(m+1))
by FUNCT_2:21;
A11:G.(m+1) = F.(m+1) \ F.m & F.m c= F.(m+1) by A1,A2;
then A12:F.m misses G.(m+1) by XBOOLE_1:79;
Ser(M*G).(m + 1) = (M*F).m + (M*G).(m+1) by A9,SUPINF_2:63
.= M.(F.m) + M.(G.(m+1)) by A10,FUNCT_2:21
.= M.(F.m \/ G.(m+1)) by A12,MEASURE1:61
.= (M*F).(m+1) by A10,A11,XBOOLE_1:45;
hence thesis;
end;
for m being Nat holds P[m] from Ind(A7,A8);
hence thesis by A6;
end;
hence thesis by A5,FUNCT_1:9;
end;
M.(union rng F) = M.(union rng G) by A1,A2,Th24
.= SUM(M*G) by A3,MEASURE1:def 11
.= sup(rng (M*F)) by A4,SUPINF_2:def 23;
hence thesis;
end;