Copyright (c) 1991 Association of Mizar Users
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;