:: Several Properties of the $\sigma$-additive Measure
:: by J\'ozef Bia{\l}as
::
:: Received July 3, 1991
:: Copyright (c) 1991-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 PROB_1, MEASURE1, FUNCT_1, NUMBERS, RELAT_1, SUPINF_2, TARSKI,
XBOOLE_0, SUBSET_1, SETFAM_1, CARD_1, ARYTM_3, XXREAL_0, NAT_1, ZFMISC_1,
VALUED_0, ORDINAL2, MEASURE2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0,
XXREAL_3,
XCMPLX_0, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, NAT_1, SETFAM_1, PROB_1,
SUPINF_2, MEASURE1;
constructors PARTFUN1, NAT_1, PROB_2, MEASURE1, SUPINF_1, XREAL_0, RELSET_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, FUNCT_2, NUMBERS, XXREAL_0,
MEASURE1, MEMBERED, RELSET_1;
requirements NUMERALS, SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0;
equalities SUPINF_2;
expansions TARSKI, XBOOLE_0;
theorems TARSKI, FUNCT_1, FUNCT_2, ZFMISC_1, NAT_1, SETFAM_1, SUPINF_2,
MEASURE1, ENUMSET1, PROB_2, XBOOLE_0, XBOOLE_1, PROB_1, ORDINAL1,
XXREAL_0, RELAT_1;
schemes NAT_1, RECDEF_1;
begin
::
:: Some useful theorems about measures and functions
::
reserve X for set;
theorem
for S being SigmaField of X, M being sigma_Measure of S, F being
sequence of S holds M*F is nonnegative by MEASURE1:25;
definition
let X be set;
let S be SigmaField of X;
mode N_Measure_fam of S -> N_Sub_set_fam of X means
:Def1:
it c= S;
existence
proof
{} is Subset of X & {{},{}} = {{}} by ENUMSET1:29,XBOOLE_1:2;
then reconsider C = {{}} as N_Sub_set_fam of X by MEASURE1:20;
take C;
{} in S by PROB_1:4;
hence thesis by ZFMISC_1:31;
end;
end;
theorem Th2:
for S being SigmaField of X, T being N_Measure_fam of S holds
meet T in S & union T in S
proof
let S be SigmaField of X, T be N_Measure_fam of S;
T c= S by Def1;
hence thesis by MEASURE1:22,def 5;
end;
definition
let X be set, S be SigmaField of X, T be N_Measure_fam of S;
redefine func meet T -> Element of S; :: redefines meet (SETFAM_1, definition)
coherence by Th2;
redefine func union T -> Element of S; :: redefines union (TARSKI, definition)
coherence by Th2;
end;
theorem Th3:
for S being SigmaField of X, N being sequence of S holds ex F
being sequence of S st F.0 = N.0 & for n being Nat holds F.(n+1)
= N.(n+1) \ N.n
proof
let S be SigmaField of X, N be sequence of 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);
reconsider A = N.0 as Element of S;
A1: for c being Nat, A being Element of S ex B being Element of S
st P[c,A,B]
proof
let c be Nat, A be Element of S;
reconsider B = N.(c+1) \ N.c as Element of S;
take B;
thus thesis;
end;
consider F being sequence of S such that
A2: F.0 = A & for n being Nat holds P[n,F.n,F.(n+1)] from
RECDEF_1:sch 2(A1);
for n being Nat holds F.(n + 1) = N.(n+1) \ N.n
proof
let n be 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 Th4:
for S being SigmaField of X, N being sequence of S holds ex F
being sequence of S st F.0 = N.0 & for n being Nat holds F.(n+1)
= N.(n+1) \/ F.n
proof
let S be SigmaField of X, N be sequence of 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, A be Element of S;
reconsider B = N.(c+1) \/ A as Element of S;
take B;
thus thesis;
end;
consider F being sequence of S such that
A2: F.0 = N.0 & for n being Nat holds P[n,F.n,F.(n+1)] from
RECDEF_1:sch 2(A1);
for n being Nat holds F.(n + 1) = N.(n+1) \/ F.n by A2;
hence thesis by A2;
end;
theorem Th5:
for S being non empty Subset-Family of X, N,F being sequence of S
holds F.0 = N.0 & (for n being 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 sequence of S;
assume that
A1: F.0 = N.0 and
A2: for n being Nat holds F.(n+1) = N.(n+1) \/ F.n;
let r be set, n be Nat;
defpred P[Nat] means
(ex k being Nat st k <= $1 & r in N.k) implies r in F.$1;
A3: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A4: (ex k being Nat st k <= n & r in N.k) implies r in F.n;
A5: F.(n+1) = N.(n+1) \/ F.n by A2;
given k being Nat such that
A6: k <= n+1 and
A7: r in N.k;
k <= n or k = n + 1 by A6,NAT_1:8;
hence thesis by A4,A7,A5,XBOOLE_0:def 3;
end;
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
A8: r in F.n;
then
A9: 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
NAT_1:sch 5(A9);
then consider s being Nat such that
A10: r in F.s and
A11: for k being Nat st r in F.k holds s <= k;
A12: (ex k being Nat st s = k + 1) implies ex k being Element of NAT st k
<= n & r in N.k
proof
given k being Nat such that
A13: s = k + 1;
reconsider k as Element of NAT by ORDINAL1:def 12;
A14: not r in F.k
proof
assume r in F.k;
then s <= k by A11;
hence thesis by A13,NAT_1:13;
end;
take s;
A15: s in NAT by ORDINAL1:def 12;
F.s = N.s \/ F.k by A2,A13;
hence thesis by A8,A10,A11,A14,A15,XBOOLE_0:def 3;
end;
s=0 implies ex k being Element of NAT st k <= n & r in N.k
by A1,A10,NAT_1:2;
hence thesis by A12,NAT_1:6;
end;
A16: P[0] by A1,NAT_1:3;
for n being Nat holds P[n] from NAT_1:sch 2(A16,A3);
hence thesis;
end;
theorem Th6:
for S being non empty Subset-Family of X, N,F being sequence of S holds
(F.0 = N.0 & (for n being 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 sequence of S;
assume that
A1: F.0 = N.0 and
A2: for n being 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;
A3: X[0]
proof
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);
A5: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
A6: 0 <= k by NAT_1:2;
F.(k+1+1) = N.(k+1+1) \/ F.(k+1) by A2;
then
A7: F.(k+1) c= F.(k+1+1) by XBOOLE_1:7;
assume 0 < k + 1 implies F.0 c= F.(k+1);
hence thesis by A7,A6,NAT_1:13,XBOOLE_1:1;
end;
F.(0+1) = N.(0+1) \/ F.0 by A2;
then
A8: P[0] by XBOOLE_1:7;
thus for k being Nat holds P[k] from NAT_1:sch 2(A8,A5 );
end;
let m be Nat;
assume
A9: 0 < m;
then consider k being Nat such that
A10: m = k + 1 by NAT_1:6;
reconsider k as Element of NAT by ORDINAL1:def 12;
m=k+1 by A10;
hence thesis by A9,A4;
end;
A11: for n being Nat st X[n] holds X[n+1]
proof
let n be Nat;
assume
A12: for m being Nat st n < m holds F.n c= F.m;
let m be Nat;
assume
A13: n+1 < m;
let r be object;
A14: 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 A12;
hence thesis by A15;
end;
hence thesis by A13,NAT_1:13;
end;
assume
A16: r in F.(n+1);
A17: F.(n+1) = N.(n+1) \/ F.n by A2;
r in N.(n+1) implies r in F.m by A1,A2,A13,Th5;
hence thesis by A16,A17,A14,XBOOLE_0:def 3;
end;
thus for n being Nat holds X[n] from NAT_1:sch 2(A3,A11);
end;
theorem Th7:
for S being non empty Subset-Family of X, N, G, F being sequence of S holds
G.0 = N.0 & (for n being Nat holds G.(n+1) = N.(n+1)
\/ G.n) & F.0 = N.0 & (for n being 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 sequence of S;
assume that
A1: G.0 = N.0 and
A2: for n being Nat holds G.(n+1) = N.(n+1) \/ G.n and
A3: F.0 = N.0 and
A4: for n being Nat holds F.(n+1) = N.(n+1) \ G.n;
let n,m be Nat;
A5: for n being Nat holds F.n c= G.n
proof
defpred P[Nat] means F.$1 c= G.$1;
A6: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume F.n c= G.n;
G.(n+1) = N.(n+1) \/ G.n by A2;
then
A7: N.(n+1) c= G.(n+1) by XBOOLE_1:7;
F.(n+1) = N.(n+1) \ G.n by A4;
hence thesis by A7,XBOOLE_1:1;
end;
A8: P[0] by A1,A3;
thus for n being Nat holds P[n] from NAT_1:sch 2(A8,A6);
end;
A9: n < m implies F.n c= G.m
proof
assume n < m;
then
A10: G.n c= G.m by A1,A2,Th6;
F.n c= G.n by A5;
hence thesis by A10;
end;
assume n <= m;
then n = m or n < m by XXREAL_0:1;
hence thesis by A5,A9;
end;
theorem Th8:
for S being SigmaField of X holds for N, G being sequence of
S holds ex F being sequence of S st F.0 = N.0 & for n being Nat
holds F.(n+1) = N.(n+1) \ G.n
proof
let S be SigmaField of X;
let N, G be sequence of 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 sequence of S such that
A3: F.0 = N.0 & for n being Nat holds P[n,F.n,F.(n+1)] from
RECDEF_1:sch 2(A1);
for n being Nat holds F.(n + 1) = N.(n+1) \ G.n
proof
let n be 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 SigmaField of X holds for N being sequence of S holds
ex F being sequence of S st F.0 = {} & for n being Nat holds F.(
n+1) = N.0 \ N.n
proof
let S be SigmaField of X;
let N be sequence of 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));
reconsider A = {} as Element of S by PROB_1:4;
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;
consider F being sequence of S such that
A2: F.0 = A & for n being Nat holds P[n,F.n,F.(n+1)] from
RECDEF_1:sch 2(A1);
for n being Nat holds F.(n + 1) = N.0 \ N.n
proof
let n be 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 Th10:
for S being SigmaField of X holds for N, G, F being sequence of S holds
G.0 = N.0 & (for n being Nat holds G.(n+1) = N.(n+1) \/
G.n) & F.0 = N.0 & (for n being 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 SigmaField of X;
let N, G, F be sequence of S;
assume that
A1: ( G.0 = N.0 & for n being Nat holds G.(n+1) = N.(n+1) \/
G.n )& F.0 = N.0 and
A2: for n being Nat holds F.(n+1) = N.(n+1) \ G.n;
let n,m be Nat;
assume
A3: n < m;
then 0 <> m by NAT_1:2;
then consider k being Nat such that
A4: m = k + 1 by NAT_1:6;
reconsider k as Element of NAT by ORDINAL1:def 12;
F.(k+1) = N.(k+1) \ G.k by A2;
then
A5: G.k misses F.(k+1) by XBOOLE_1:79;
n <= k by A3,A4,NAT_1:13;
hence F.n /\ F.m = (F.n /\ G.k) /\ F.(k+1) by A1,A2,A4,Th7,XBOOLE_1:28
.= F.n /\ (G.k /\ F.(k+1)) by XBOOLE_1:16
.= F.n /\ {} by A5
.= {};
end;
theorem Th11:
for S being SigmaField of X, M being sigma_Measure of S, T being
N_Measure_fam of S, F being sequence of S st T = rng F holds M.(union T) <=
SUM(M*F)
proof
let S be SigmaField of X, M be sigma_Measure of S, T be N_Measure_fam of S,
F be sequence of S;
consider G being sequence of S such that
A1: G.0 = F.0 & for n being Nat holds G.(n+1) = F.(n+1) \/ G.
n by Th4;
consider H being sequence of S such that
A2: H.0 = F.0 and
A3: for n being Nat holds H.(n+1) = F.(n+1) \ G.n by Th8;
for n,m being object st n <> m holds H.n misses H.m
proof
let n,m be object;
assume
A4: n <> m;
per cases;
suppose
n in dom H & m in dom H;
then reconsider n9=n,m9=m as Element of NAT;
A5: m9 < n9 implies H.m misses H.n by A1,A2,A3,Th10;
n9 < m9 implies H.n misses H.m by A1,A2,A3,Th10;
hence thesis by A4,A5,XXREAL_0:1;
end;
suppose
not (n in dom H & m in dom H);
then H.n = {} or H.m = {} by FUNCT_1:def 2;
hence thesis;
end;
end;
then H is Sep_Sequence of S by PROB_2:def 2;
then
A6: SUM(M*H) = M.(union rng H) by MEASURE1:def 6;
A7: for n being Element of NAT holds H.n c= F.n
proof
let n be Element of NAT;
A8: (ex k being Nat st n = k + 1) implies H.n c= F.n
proof
given k being Nat such that
A9: n = k + 1;
reconsider k as Element of NAT by ORDINAL1:def 12;
H.n = F.n \ G.k by A3,A9;
hence thesis by XBOOLE_1:36;
end;
n=0 or ex k being Nat st n = k + 1 by NAT_1:6;
hence thesis by A2,A8;
end;
A10: for n being Element of NAT holds (M*H).n <= (M*F).n
proof
let n be Element of NAT;
NAT = dom(M*F) by FUNCT_2:def 1;
then
A11: (M*F).n = M.(F.n) by FUNCT_1:12;
NAT = dom(M*H) by FUNCT_2:def 1;
then (M*H).n = M.(H.n) by FUNCT_1:12;
hence thesis by A7,A11,MEASURE1:31;
end;
A12: union rng H = union rng F
proof
thus union rng H c= union rng F
proof
let r be object;
assume r in union rng H;
then consider E being set such that
A13: r in E and
A14: E in rng H by TARSKI:def 4;
consider s being object such that
A15: s in dom H and
A16: E = H.s by A14,FUNCT_1:def 3;
reconsider s as Element of NAT by A15;
A17: F.s in rng F by FUNCT_2:4;
E c= F.s by A7,A16;
hence thesis by A13,A17,TARSKI:def 4;
end;
let r be object;
assume r in union rng F;
then consider E being set such that
A18: r in E and
A19: E in rng F by TARSKI:def 4;
A20: ex s being object st s in dom F & E = F.s by A19,FUNCT_1:def 3;
ex s1 being Element of NAT st r in H.s1
proof
defpred P[Nat] means r in F.$1;
A21: ex k being Nat st P[k] by A18,A20;
ex k being Nat st P[k] & for n being Nat st P[n] holds k <= n from
NAT_1:sch 5(A21);
then consider k being Nat such that
A22: r in F.k and
A23: for n being Nat st r in F.n holds k <= n;
A24: (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
A25: k = l + 1;
take k;
reconsider l as Element of NAT by ORDINAL1:def 12;
A26: not r in G.l
proof
assume r in G.l;
then consider i being Nat such that
A27: i <= l and
A28: r in F.i by A1,Th5;
k <= i by A23,A28;
hence thesis by A25,A27,NAT_1:13;
end;
H.(l+1) = F.(l+1) \ G.l by A3;
hence thesis by A22,A25,A26,XBOOLE_0:def 5;
end;
k=0 implies ex s1 being Element of NAT st r in H.s1 by A2,A22;
hence thesis by A24,NAT_1:6;
end;
then consider s1 being Element of NAT such that
A29: r in H.s1;
H.s1 in rng H by FUNCT_2:4;
hence thesis by A29,TARSKI:def 4;
end;
assume T = rng F;
hence thesis by A10,A6,A12,SUPINF_2:43;
end;
theorem Th12:
for S being SigmaField of X, T being N_Measure_fam of S holds ex
F being sequence of S st T = rng F
proof
let S be SigmaField of X, T be N_Measure_fam of S;
consider F being sequence of bool X such that
A1: T = rng F by SUPINF_2:def 8;
rng F c= S by A1,Def1;
then F is sequence of S by FUNCT_2:6;
then consider F being sequence of S such that
A2: T = rng F by A1;
take F;
thus thesis by A2;
end;
theorem Th13:
for N, F being Function st (F.0 = {} & for n being Nat
holds F.(n+1) = N.0 \ N.n & N.(n+1) c= N.n )
for n being Nat holds F.n c= F.(n+1)
proof
let N,F be Function;
assume that
A1: F.0 = {} and
A2: for n being Nat holds F.(n+1) = N.0 \ N.n & N.(n+1) c= N. n;
defpred P[Nat] means F.$1 c= F.($1+1);
A3: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume F.n c= F.(n+1);
F.((n+1)+1) = N.0 \ N.(n+1) by A2;
then N.0 \ N.n c= F.((n+1)+1) by A2,XBOOLE_1:34;
hence thesis by A2;
end;
let n be Nat;
F.(0+1) = N.0 \ N.0 by A2;
then
A4: P[0] by A1,XBOOLE_1:37;
for n being Nat holds P[n] from NAT_1:sch 2(A4,A3);
hence thesis;
end;
theorem
for S being SigmaField of X, M being sigma_Measure of S, T being
N_Measure_fam of S st (for A being set st A in T holds A is measure_zero of M)
holds union T is measure_zero of M
proof
let S be SigmaField of X, M be sigma_Measure of S, T be N_Measure_fam of S;
consider F being sequence of S such that
A1: T = rng F by Th12;
set G = M*F;
assume
A2: for A being set st A in T holds A is measure_zero of M;
A3: for r being Element of NAT st 0 <= r holds G.r = 0.
proof
let r be Element of NAT;
F.r is measure_zero of M by A2,A1,FUNCT_2:4;
then M.(F.r) = 0. by MEASURE1:def 7;
hence thesis by FUNCT_2:15;
end;
G is nonnegative by MEASURE1:25;
then SUM(G) = Ser(G).0 by A3,SUPINF_2:48;
then SUM(G) = G.0 by SUPINF_2:def 11;
then SUM(M*F) = 0. by A3;
then
A4: M.(union T) <= 0. by A1,Th11;
0. <= M.(union T) by MEASURE1:def 2;
then M.(union T) = 0. by A4,XXREAL_0:1;
hence thesis by MEASURE1:def 7;
end;
theorem
for S being SigmaField 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 by MEASURE1:36,SETFAM_1:3;
theorem
for S being SigmaField of X, M being sigma_Measure of S, T being
N_Measure_fam of S st (for A being set st A in T holds A is measure_zero of M)
holds meet T is measure_zero of M
proof
let S be SigmaField 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 sequence of bool X such that
A2: T = rng F by SUPINF_2:def 8;
take F.0;
thus thesis by A1,A2,FUNCT_2:4;
end;
hence thesis by MEASURE1:36,SETFAM_1:3;
end;
definition
let X be set;
let S be SigmaField of X;
let IT be N_Measure_fam of S;
attr IT is non-decreasing means
:Def2:
ex F being sequence of S st IT =
rng F & for n being Nat holds F.n c= F.(n+1);
end;
registration
let X be set;
let S be SigmaField of X;
cluster non-decreasing for N_Measure_fam of S;
existence
proof
consider A being set such that
A1: A in S by PROB_1:4;
reconsider A as Subset of X by A1;
consider B,C being Subset of X such that
A2: B = A & C = A;
A3: {A} c= S by A1,ZFMISC_1:31;
consider F being sequence of bool X such that
A4: rng F = {B,C} and
A5: F.0 = B & for n being Nat st 0 < n holds F.n = C by MEASURE1:19;
A6: rng F = {A} by A2,A4,ENUMSET1:29;
then
A7: rng F c= S by A1,ZFMISC_1:31;
{A} is N_Sub_set_fam of X by A6,SUPINF_2:def 8;
then reconsider T = {A} as N_Measure_fam of S by A3,Def1;
reconsider F as sequence of S by A7,FUNCT_2:6;
take T,F;
for n being Nat holds F.n c= F.(n+1)
proof
let n be Nat;
F.n = A by A2,A5,NAT_1:3;
hence thesis by A2,A5,NAT_1:3;
end;
hence thesis by A2,A4,ENUMSET1:29;
end;
end;
definition
let X be set;
let S be SigmaField of X;
let IT be N_Measure_fam of S;
attr IT is non-increasing means
ex F being sequence of S st IT = rng F &
for n being Element of NAT holds F.(n+1) c= F.n;
end;
registration
let X be set;
let S be SigmaField of X;
cluster non-increasing for N_Measure_fam of S;
existence
proof
consider A being set such that
A1: A in S by PROB_1:4;
reconsider A as Subset of X by A1;
A2: {A} c= S by A1,ZFMISC_1:31;
set B = A, C = A;
consider F being sequence of bool X such that
A3: rng F = {B,C} and
A4: F.0 = B & for n being Nat st 0 < n holds F.n = C by MEASURE1:19;
A5: rng F = {A} by A3,ENUMSET1:29;
then
A6: rng F c= S by A1,ZFMISC_1:31;
{A} is N_Sub_set_fam of X by A5,SUPINF_2:def 8;
then reconsider T = {A} as N_Measure_fam of S by A2,Def1;
reconsider F as sequence of S by A6,FUNCT_2:6;
take T,F;
for n being Element of NAT holds F.(n+1) c= F.n
proof
let n be Element of NAT;
F.n = A by A4,NAT_1:3;
hence thesis by A4,NAT_1:3;
end;
hence thesis by A3,ENUMSET1:29;
end;
end;
theorem
for S being SigmaField of X, N,F being sequence of S holds (F.0 =
{} & for n being 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 SigmaField of X, N,F be sequence of S;
assume F.0 = {} & for n being Nat holds F.(n+1) = N.0 \ N.n & N.
(n+1) c= N. n;
then
A1: for n being Nat holds F.n c= F.(n+1) by Th13;
rng F c= S & rng F is N_Sub_set_fam of X by MEASURE1:23,RELAT_1:def 19;
hence thesis by A1,Def1,Def2;
end;
theorem Th18:
for N being Function st (for n being Nat holds N.n c=
N.(n+1)) holds for m,n being Nat st n <= m holds N.n c= N.m
proof
let N be Function;
defpred P[Nat] means for n being Nat st n <= $1 holds N.n c= N.$1;
assume
A1: for n being Nat holds N.n c= N.(n+1);
A2: for m being Nat st P[m] holds P[m+1]
proof
let m be Nat;
assume
A3: for n being Nat st n <= m holds N.n c= N.m;
let n be Nat;
A4: n <= m implies N.n c= N.(m+1)
proof
assume n <= m;
then
A5: N.n c= N.m by A3;
N.m c= N.(m+1) by A1;
hence thesis by A5;
end;
assume n <= m+1;
hence thesis by A4,NAT_1:8;
end;
A6: P[0] by NAT_1:3;
thus for m being Nat holds P[m] from NAT_1:sch 2(A6,A2);
end;
theorem Th19:
for N,F being Function st (F.0 = N.0 & for n being Nat
holds F.(n+1) = N.(n+1) \ N.n & N.n c= N.(n+1))
for n,m being Nat st n < m holds F.n misses F.m
proof
let N,F be Function;
assume that
A1: F.0 = N.0 and
A2: for n being Nat holds F.(n+1) = N.(n+1) \ N.n & N.n c= N. (n+1);
let n,m be Nat;
assume
A3: n < m;
then 0 <> m by NAT_1:2;
then consider k being Nat such that
A4: m = k + 1 by NAT_1:6;
A5: for n being Nat holds F.n c= N.n
proof
defpred P[Nat] means F.$1 c= N.$1;
A6: 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 A2;
hence thesis;
end;
A7: P[0] by A1;
thus for n being Nat holds P[n] from NAT_1:sch 2(A7, A6);
end;
A8: for n,m being Nat st n <= m holds F.n c= N.m
proof
let n,m be Nat;
A9: n < m implies F.n c= N.m
proof
assume n < m;
then
A10: N.n c= N.m by A2,Th18;
F.n c= N.n by A5;
hence thesis by A10;
end;
assume n <= m;
then n = m or n < m by XXREAL_0:1;
hence thesis by A5,A9;
end;
reconsider k as Element of NAT by ORDINAL1:def 12;
F.(k+1) = N.(k+1) \ N.k by A2;
then
A11: N.k misses F.(k+1) by XBOOLE_1:79;
n <= k by A3,A4,NAT_1:13;
then F.n /\ F.(k+1) = (F.n /\ N.k) /\ F.(k+1) by A8,XBOOLE_1:28
.= F.n /\ (N.k /\ F.(k+1)) by XBOOLE_1:16
.= F.n /\ {} by A11
.= {};
hence thesis by A4;
end;
theorem Th20:
for S being SigmaField of X, N,F being sequence of S holds (
F.0 = N.0 & for n being 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 SigmaField of X, N,F be sequence of S;
assume that
A1: F.0 = N.0 and
A2: for n being 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 object;
assume x in union rng F;
then consider Y being set such that
A3: x in Y and
A4: Y in rng F by TARSKI:def 4;
consider n being object such that
A5: n in dom F and
A6: Y = F.n by A4,FUNCT_1:def 3;
reconsider n as Element of NAT by A5;
A7: (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
A8: n = k + 1;
reconsider k as Element of NAT by ORDINAL1:def 12;
Y=N.(k+1) \ N.k by A2,A6,A8;
then x in N.(k+1) by A3,XBOOLE_0:def 5;
hence thesis by FUNCT_2:4;
end;
n=0 implies ex Z being set st x in Z & Z in rng N by A1,A3,A6,FUNCT_2:4;
hence thesis by A7,NAT_1:6,TARSKI:def 4;
end;
let x be object;
assume x in union rng N;
then consider Y being set such that
A9: x in Y and
A10: Y in rng N by TARSKI:def 4;
A11: ex n being object st n in dom N & Y = N.n by A10,FUNCT_1:def 3;
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;
A12: ex k being Nat st P[k] by A9,A11;
ex k being Nat st P[k] & for r being Nat st P[r] holds k <= r from
NAT_1:sch 5(A12);
then consider k being Nat such that
A13: x in N.k and
A14: for r being Nat st x in N.r holds k <= r;
A15: (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
A16: k = l + 1;
take k;
reconsider l as Element of NAT by ORDINAL1:def 12;
A17: not x in N.l
proof
assume x in N.l;
then l + 1 <= l by A14,A16;
hence thesis by NAT_1:13;
end;
F.(l+1) = N.(l+1) \ N.l by A2;
hence thesis by A13,A16,A17,XBOOLE_0:def 5;
end;
k=0 implies ex s being Element of NAT st x in F.s by A1,A13;
hence thesis by A15,NAT_1:6;
end;
hence thesis by FUNCT_2:4;
end;
hence thesis by TARSKI:def 4;
end;
theorem Th21:
for S being SigmaField of X, N,F being sequence of S holds (
F.0 = N.0 & for n being 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 SigmaField of X, N,F be sequence of S;
assume
A1: F.0 = N.0 & for n being Nat holds F.(n+1) = N.(n+1) \ N.n
& N.n c= N. (n+1);
for n,m being object st n <> m holds F.n misses F.m
proof
let n,m be object;
assume
A2: n <> m;
per cases;
suppose
n in dom F & m in dom F;
then reconsider n9=n,m9=m as Element of NAT;
A3: m9 < n9 implies F.m misses F.n by A1,Th19;
n9 < m9 implies F.n misses F.m by A1,Th19;
hence thesis by A2,A3,XXREAL_0:1;
end;
suppose
not (n in dom F & m in dom F);
then F.n = {} or F.m = {} by FUNCT_1:def 2;
hence thesis;
end;
end;
hence thesis by PROB_2:def 2;
end;
theorem
for S being SigmaField of X, N,F being sequence of 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 SigmaField of X, N,F be sequence of S;
assume that
A1: F.0 = N.0 and
A2: 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 by A2;
hence thesis by A2,XBOOLE_1:45;
end;
hence thesis by A1;
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 c= F.(n+1)) holds M.
(union rng F) = sup(rng (M*F))
proof
let S be SigmaField of X;
let M be sigma_Measure of S;
let F be sequence of S;
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) \ F.n by Th3;
assume
A3: for n being Nat holds F.n c= F.(n+1);
then
A4: G is Sep_Sequence of S by A1,A2,Th21;
A5: for m being object st m in NAT holds Ser(M*G).m = (M*F).m
proof
defpred P[Nat] means Ser(M*G).$1 = (M*F).$1;
let m be object;
assume
A6: m in NAT;
A7: for m being Nat holds P[m] implies P[m+1]
proof
let m be Nat;
A8: (M*G).(m+1) = M.(G.(m+1)) by FUNCT_2:15;
A9: (M*F).(m+1) = M.(F.(m+1)) by FUNCT_2:15;
A10: G.(m+1) = F.(m+1) \ F.m by A2;
A11: m in NAT by ORDINAL1:def 12;
assume Ser(M*G).m = (M*F).m;
then Ser(M*G).(m + 1) = (M*F).m + (M*G).(m+1) by SUPINF_2:def 11
.= M.(F.m) + M.(G.(m+1)) by A8,FUNCT_2:15,A11
.= M.(F.m \/ G.(m+1)) by A10,MEASURE1:30,XBOOLE_1:79
.= (M*F).(m+1) by A3,A9,A10,XBOOLE_1:45;
hence thesis;
end;
Ser(M*G).0 = (M*G).0 by SUPINF_2:def 11
.= M.(F.0) by A1,FUNCT_2:15
.= (M*F).0 by FUNCT_2:15;
then
A12: P[0];
for m being Nat holds P[m] from NAT_1:sch 2(A12,A7);
hence thesis by A6;
end;
A13: dom Ser(M*G) = NAT & dom (M*F) = NAT by FUNCT_2:def 1;
M.(union rng F) = M.(union rng G) by A3,A1,A2,Th20
.= SUM(M*G) by A4,MEASURE1:def 6
.= sup(rng (M*F)) by A13,A5,FUNCT_1:2;
hence thesis;
end;