:: Properties of Caratheodory's Measure
:: by J\'ozef Bia{\l}as
::
:: Received June 25, 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 NUMBERS, SUPINF_1, PROB_1, XBOOLE_0, SETFAM_1, FUNCT_1, SUBSET_1,
TARSKI, RELAT_1, CARD_1, ARYTM_3, NAT_1, XXREAL_0, ZFMISC_1, MEASURE1,
SUPINF_2, VALUED_0, FUNCOP_1, XREAL_0, ARYTM_1, MEASURE3, MEASURE4,
REWRITE1, MEASURE2;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS,
FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, XXREAL_0, XREAL_0, VALUED_0,
XXREAL_3,
XCMPLX_0, FUNCOP_1, REAL_1, NAT_1, SETFAM_1, PROB_1, SUPINF_1, SUPINF_2,
MEASURE1, MEASURE2, MEASURE3;
constructors ENUMSET1, PARTFUN1, REAL_1, NAT_1, PROB_2, MEASURE3, SUPINF_1,
FUNCOP_1, RELSET_1, XREAL_0, MEASURE2;
registrations SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0,
XREAL_0, NAT_1, MEASURE1, VALUED_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, MEASURE3, XBOOLE_0;
equalities XBOOLE_0;
expansions TARSKI, XBOOLE_0;
theorems TARSKI, ENUMSET1, FUNCT_1, FUNCT_2, ZFMISC_1, NAT_1, SUPINF_2,
MEASURE1, MEASURE2, MEASURE3, XBOOLE_0, XBOOLE_1, XXREAL_0, PROB_1,
ORDINAL1, VALUED_0, XXREAL_3, FUNCOP_1;
schemes NAT_1, FUNCT_2, XFAMILY;
begin :: Some theorems about R_eal numbers
reserve
A,B,X for set,
S for SigmaField of X;
theorem Th1:
for S being non empty Subset-Family of X, F, G being sequence of S,
A being Element of S st for n being Element of NAT holds G.n = A /\ F.n
holds union rng G = A /\ union rng F
proof
let S be non empty Subset-Family of X;
let F, G be sequence of S, A be Element of S;
assume
A1: for n being Element of NAT holds G.n = A /\ F.n;
thus union rng G c= A /\ union rng F
proof
let r be object;
assume r in union rng G;
then consider E being set such that
A2: r in E and
A3: E in rng G by TARSKI:def 4;
consider s being object such that
A4: s in dom G and
A5: E = G.s by A3,FUNCT_1:def 3;
reconsider s as Element of NAT by A4;
A6: r in A /\ F.s by A1,A2,A5;
then
A7: r in A by XBOOLE_0:def 4;
A8: F.s in rng F by FUNCT_2:4;
r in F.s by A6,XBOOLE_0:def 4;
then r in union rng F by A8,TARSKI:def 4;
hence thesis by A7,XBOOLE_0:def 4;
end;
let r be object;
assume
A9: r in A /\ union rng F;
then
A10: r in A by XBOOLE_0:def 4;
r in union rng F by A9,XBOOLE_0:def 4;
then consider E being set such that
A11: r in E and
A12: E in rng F by TARSKI:def 4;
consider s being object such that
A13: s in dom F and
A14: E = F.s by A12,FUNCT_1:def 3;
reconsider s as Element of NAT by A13;
A15: G.s in rng G by FUNCT_2:4;
A /\ E = G.s by A1,A14;
then r in G.s by A10,A11,XBOOLE_0:def 4;
hence thesis by A15,TARSKI:def 4;
end;
theorem Th2:
for S being non empty Subset-Family of X for F, G being sequence of S
st (G.0 = F.0 & for n being Nat holds G.(n+1) = F.(n+1) \/
G.n) holds for H being sequence of S st (H.0 = F.0 & for n being Nat
holds H.(n+1) = F.(n+1) \ G.n) holds union rng F = union rng H
proof
let S be non empty Subset-Family of X;
let F, G be sequence of S;
assume that
A1: G.0 = F.0 and
A2: for n being Nat holds G.(n+1) = F.(n+1) \/ G.n;
let H be sequence of S;
assume that
A3: H.0 = F.0 and
A4: for n being Nat holds H.(n+1) = F.(n+1) \ G.n;
thus union rng F c= union rng H
proof
let r be object;
assume r in union rng F;
then consider E being set such that
A5: r in E and
A6: E in rng F by TARSKI:def 4;
A7: ex s being object st s in dom F & E = F.s by A6,FUNCT_1:def 3;
ex s1 being Element of NAT st r in H.s1
proof
defpred P[Nat] means r in F.$1;
A8: ex k being Nat st P[k] by A5,A7;
ex k being Nat st P[k] & for n being Nat st P[n] holds k <= n from
NAT_1:sch 5(A8);
then consider k being Nat such that
A9: r in F.k and
A10: for n being Nat st r in F.n holds k <= n;
A11: (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
A12: k = l + 1;
take k;
reconsider l as Element of NAT by ORDINAL1:def 12;
A13: not r in G.l
proof
assume r in G.l;
then consider i being Nat such that
A14: i <= l and
A15: r in F.i by A1,A2,MEASURE2:5;
k <= i by A10,A15;
hence thesis by A12,A14,NAT_1:13;
end;
H.(l+1) = F.(l+1) \ G.l by A4;
hence thesis by A9,A12,A13,XBOOLE_0:def 5;
end;
k=0 implies ex s1 being Element of NAT st r in H.s1 by A3,A9;
hence thesis by A11,NAT_1:6;
end;
then consider s1 being Element of NAT such that
A16: r in H.s1;
H.s1 in rng H by FUNCT_2:4;
hence thesis by A16,TARSKI:def 4;
end;
A17: for n being Element of NAT holds H.n c= F.n
proof
let n be Element of NAT;
A18: (ex k being Nat st n = k + 1) implies H.n c= F.n
proof
given k being Nat such that
A19: n = k + 1;
reconsider k as Element of NAT by ORDINAL1:def 12;
H.n = F.n \ G.k by A4,A19;
hence thesis;
end;
n=0 implies H.n c= F.n by A3;
hence thesis by A18,NAT_1:6;
end;
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
A20: r in E and
A21: E in rng H by TARSKI:def 4;
consider s being object such that
A22: s in dom H and
A23: E = H.s by A21,FUNCT_1:def 3;
reconsider s as Element of NAT by A22;
A24: F.s in rng F by FUNCT_2:4;
E c= F.s by A17,A23;
hence thesis by A20,A24,TARSKI:def 4;
end;
hence thesis;
end;
theorem Th3:
bool X is SigmaField of X
proof
A1: for M being N_Sub_set_fam of X st M c= bool X holds union M in bool X;
reconsider Y = bool X as Subset-Family of X;
for A being set holds A in bool X implies X\A in bool X;
then reconsider
Y as non empty compl-closed sigma-additive Subset-Family of X by A1,
MEASURE1:def 1,def 5;
Y is SigmaField of X;
hence thesis;
end;
definition
let X be set;
mode C_Measure of X -> Function of bool X,ExtREAL means
:Def1:
it is
nonnegative zeroed & for A,B being Subset of X st A c= B holds it.A <= it.B &
for F being sequence of bool X holds it.(union rng F) <= SUM(it*F);
existence
proof
set M = bool X --> 0.;
take M;
A1: for A being Subset of X holds 0.<= M.A;
then
A2: M is nonnegative by MEASURE1:def 2;
A3: for F being sequence of bool X holds M.(union rng F) <= SUM(M*F)
proof
let F be sequence of bool X;
A4: M.(union rng F) = 0.by FUNCOP_1:7;
A5: for r being Element of NAT st 0 <= r holds (M*F).r = 0.
proof
let r be Element of NAT;
dom (M*F) = NAT by FUNCT_2:def 1;
then (M*F).r = M.(F.r) by FUNCT_1:12;
hence thesis by FUNCOP_1:7;
end;
A6: Ser(M*F).0 = (M*F).0 by SUPINF_2:def 11;
M*F is nonnegative by A2,MEASURE1:25;
hence thesis by A4,A5,A6,SUPINF_2:48;
end;
{} c= X;
then M.{} = 0. by FUNCOP_1:7;
hence thesis by A1,A3,FUNCOP_1:7,MEASURE1:def 2,VALUED_0:def 19;
end;
end;
reserve C for C_Measure of X;
definition
let X be set;
let C be C_Measure of X;
func sigma_Field(C) -> non empty Subset-Family of X means
:Def2:
for A being
Subset of X holds (A in it iff for W,Z being Subset of X holds (W c= A & Z c= X
\ A implies C.W + C.Z <= C.(W \/ Z)));
existence
proof
reconsider A = {} as Subset of X by XBOOLE_1:2;
defpred P[set] means for A being set holds (A = $1 implies for W,Z being
Subset of X holds (W c= A & Z c= X \ A implies C.W + C.Z <= C.(W \/ Z)));
consider D being set such that
A1: for y being set holds (y in D iff y in bool X & P[y] ) from
XFAMILY:sch 1;
A2: for A being set holds (A in D iff A in bool X & for W,Z being Subset
of X holds (W c= A & Z c= X \ A implies C.W + C.Z <= C.(W \/ Z)))
proof
let A be set;
P[A] iff for W,Z being Subset of X holds (W c= A & Z c= X \ A
implies C.W + C.Z <= C.(W \/ Z));
hence thesis by A1;
end;
then
A3: for A being object holds A in D implies A in bool X;
now
let W,Z be Subset of X;
assume that
A4: W c= A and
Z c= X \ A;
A5: W = {} by A4;
C is zeroed by Def1;
then C.W = 0 by A5,VALUED_0:def 19;
hence C.W + C.Z <= C.(W \/ Z) by A5,XXREAL_3:4;
end;
then reconsider D as non empty Subset-Family of X by A2,A3,TARSKI:def 3;
take D;
thus thesis by A2;
end;
uniqueness
proof
let D1,D2 be non empty Subset-Family of X such that
A6: for A being Subset of X holds (A in D1 iff for W,Z being Subset
of X holds (W c= A & Z c= X \ A implies C.W + C.Z <= C.(W \/ Z))) and
A7: for A being Subset of X holds (A in D2 iff for W,Z being Subset
of X holds (W c= A & Z c= X \ A implies C.W + C.Z <= C.(W \/ Z)));
for A being object holds A in D1 iff A in D2
proof
let A be object;
reconsider AA = A as set by TARSKI:1;
hereby
assume
A8: A in D1;
then reconsider A9 = A as Subset of X;
for W,Z being Subset of X
holds (W c= AA & Z c= X \ A9 implies C.W
+ C.Z <= C.(W \/ Z)) by A6,A8;
hence A in D2 by A7;
end;
assume
A9: A in D2;
then reconsider A as Subset of X;
for W,Z being Subset of X holds (W c= A & Z c= X \ A implies C.W +
C.Z <= C.(W \/ Z)) by A7,A9;
hence thesis by A6;
end;
hence thesis by TARSKI:2;
end;
end;
theorem Th4:
for W,Z being Subset of X holds C.(W \/ Z) <= C.W + C.Z
proof
let W,Z be Subset of X;
reconsider P = {} as Subset of X by XBOOLE_1:2;
consider F being sequence of bool X such that
A1: rng F = {W,Z,P} and
A2: F.0 = W and
A3: F.1 = Z and
A4: for n being Element of NAT st 1 < n holds F.n = P by MEASURE1:17;
A5: (C*F).1 = C.Z by A3,FUNCT_2:15;
set G = C*F;
A6: union {W,Z,P} = W \/ Z
proof
thus union {W,Z,P} c= W \/ Z
proof
let x be object;
assume x in union {W,Z,P};
then ex Y being set st x in Y & Y in {W,Z,P} by TARSKI:def 4;
then x in W or x in Z or x in P by ENUMSET1:def 1;
hence thesis by XBOOLE_0:def 3;
end;
let x be object;
assume
A7: x in W \/ Z;
now
per cases by A7,XBOOLE_0:def 3;
suppose
A8: x in W;
take Y = W;
thus x in Y & Y in {W,Z,P} by A8,ENUMSET1:def 1;
end;
suppose
A9: x in Z;
take Y = Z;
thus x in Y & Y in {W,Z,P} by A9,ENUMSET1:def 1;
end;
end;
hence thesis by TARSKI:def 4;
end;
A10: C is zeroed by Def1;
A11: for r being Element of NAT st 2 <= r holds (C*F).r = 0.
proof
let r be Element of NAT;
assume 2 <= r;
then 1 + 1 <= r;
then 1 < r by NAT_1:13;
then
A12: F.r = {} by A4;
C is zeroed by Def1;
then C.(F.r) = 0. by A12,VALUED_0:def 19;
hence thesis by FUNCT_2:15;
end;
C is nonnegative by Def1;
then
A13: C*F is nonnegative by MEASURE1:25;
F.2 = P by A4;
then
A14: (C*F).2 = C.P by FUNCT_2:15;
A15: (C*F).0 = C.W by A2,FUNCT_2:15;
consider y1,y2 being R_eal such that
A16: y1 = Ser(G).1 and
A17: y2 = Ser(G).0;
Ser(G).2 = y1 + G.(1 + 1) by A16,SUPINF_2:def 11
.= Ser(G).1 + 0. by A14,A16,A10,VALUED_0:def 19
.= Ser(G).1 by XXREAL_3:4
.= y2 + G.(0 + 1) by A17,SUPINF_2:def 11
.= C.W + C.Z by A5,A15,A17,SUPINF_2:def 11;
then SUM(C*F) = C.W + C.Z by A13,A11,SUPINF_2:48;
hence thesis by A1,A6,Def1;
end;
theorem Th5:
for A being Subset of X holds (A in sigma_Field(C) iff for W,Z
being Subset of X holds (W c= A & Z c= X \ A implies C.W + C.Z = C.(W \/ Z)))
proof
let A be Subset of X;
hereby
assume
A1: A in sigma_Field(C);
let W,Z be Subset of X;
assume that
A2: W c= A and
A3: Z c= X \ A;
A4: C.(W \/ Z) <= C.W + C.Z by Th4;
C.W + C.Z <= C.(W \/ Z) by A1,A2,A3,Def2;
hence C.W + C.Z = C.(W \/ Z) by A4,XXREAL_0:1;
end;
assume for W,Z being Subset of X holds (W c= A & Z c= X \ A implies C.W + C
.Z = C.(W \/ Z));
then for W,Z being Subset of X holds (W c= A & Z c= X \ A implies C.W + C.Z
<= C.(W \/ Z));
hence thesis by Def2;
end;
theorem Th6:
for W,Z being Subset of X holds W in sigma_Field(C) & Z misses W
implies C.(W \/ Z) = C.W + C.Z
proof
let W,Z be Subset of X;
assume that
A1: W in sigma_Field(C) and
A2: Z misses W;
Z \ W c= X \ W by XBOOLE_1:33;
then Z c= X \ W by A2,XBOOLE_1:83;
hence thesis by A1,Th5;
end;
theorem Th7:
A in sigma_Field(C) implies X \ A in sigma_Field(C)
proof
assume
A1: A in sigma_Field(C);
for W,Z being Subset of X holds W c= X \ A & Z c= X \ (X \ A) implies C.
W + C.Z <= C.(W \/ Z)
proof
let W,Z be Subset of X;
assume that
A2: W c= X \ A and
A3: Z c= X \ (X \ A);
X \ (X \ A) = X /\ A by XBOOLE_1:48;
then Z c= A by A1,A3,XBOOLE_1:28;
hence thesis by A1,A2,Def2;
end;
hence thesis by Def2;
end;
theorem Th8:
A in sigma_Field(C) & B in sigma_Field(C) implies A \/ B in sigma_Field(C)
proof
assume that
A1: A in sigma_Field(C) and
A2: B in sigma_Field(C);
reconsider A,B as Subset of X by A1,A2;
set D = A \/ B;
for W,Z being Subset of X holds W c= D & Z c= X \ D implies C.W + C.Z =
C.(W \/ Z)
proof
let W,Z be Subset of X;
assume that
A3: W c= D and
A4: Z c= X \ D;
set W2 = W \ A;
set Z1 = W2 \/ Z;
A5: (X \ A) /\ (X \ B) c= X \ B by XBOOLE_1:17;
set W1 = W /\ A;
A6: W1 c= A by XBOOLE_1:17;
(X \ A) /\ (X \ B) c= X \ A by XBOOLE_1:17;
then
A7: X \ (A \/ B) c= X \ A by XBOOLE_1:53;
Z c= (X \ A) /\ (X \ B) by A4,XBOOLE_1:53;
then
A8: Z c= X \ B by A5;
W = W1 \/ W2 by XBOOLE_1:51;
then C.W <= C.W1 + C.W2 by Th4;
then
A9: C.W + C.Z <= (C.W1 + C.W2) + C.Z by XXREAL_3:36;
W \ A c= B \/ A \ A by A3,XBOOLE_1:33;
then
A10: W \ A c= B \ A by XBOOLE_1:40;
B \ A c= B by XBOOLE_1:36;
then W2 c= B by A10;
then
A11: C.W2 + C.Z <= C.Z1 by A2,A8,Def2;
C is nonnegative by Def1;
then
A12: 0. <= C.W1 by MEASURE1:def 2;
W \ A c= X \ A by XBOOLE_1:33;
then W2 \/ Z c= X \ A \/ Z by XBOOLE_1:9;
then
A13: Z1 c= X \ A by A4,A7,XBOOLE_1:1,12;
C.(W \/ Z) = C.((W1 \/ W2) \/ Z) by XBOOLE_1:51
.= C.(W1 \/ Z1) by XBOOLE_1:4
.= C.W1 + C.Z1 by A1,A6,A13,Th5;
then
A14: C.W1 + (C.W2 + C.Z) <= C.(W \/ Z) by A11,XXREAL_3:36;
A15: C is nonnegative by Def1;
then
A16: 0.<= C.Z by MEASURE1:def 2;
0.<= C.W2 by A15,MEASURE1:def 2;
then (C.W1 + C.W2) + C.Z <= C.(W \/ Z) by A16,A12,A14,XXREAL_3:44;
then
A17: C.W + C.Z <= C.(W \/ Z) by A9,XXREAL_0:2;
C.(W \/ Z) <= C.W + C.Z by Th4;
hence thesis by A17,XXREAL_0:1;
end;
hence thesis by Th5;
end;
theorem Th9:
A in sigma_Field(C) & B in sigma_Field(C) implies A /\ B in sigma_Field(C)
proof
assume that
A1: A in sigma_Field(C) and
A2: B in sigma_Field(C);
A3: X \ B in sigma_Field(C) by A2,Th7;
A /\ B c= X /\ X by A1,A2,XBOOLE_1:27;
then
A4: A /\ B = X /\ (A /\ B) by XBOOLE_1:28
.= X \ (X \(A /\ B)) by XBOOLE_1:48
.= X \ ((X \ A) \/ (X \ B)) by XBOOLE_1:54;
X \ A in sigma_Field(C) by A1,Th7;
then (X \ A) \/ (X \ B) in sigma_Field(C) by A3,Th8;
hence thesis by A4,Th7;
end;
theorem Th10:
A in sigma_Field(C) & B in sigma_Field(C) implies A \ B in sigma_Field(C)
proof
assume that
A1: A in sigma_Field(C) and
A2: B in sigma_Field(C);
for x being object holds x in A \ B iff x in A /\ (X \ B)
proof
let x be object;
hereby
assume
A3: x in A \ B;
then
A4: not x in B by XBOOLE_0:def 5;
x in A by A3;
then x in (X \ B) by A1,A4,XBOOLE_0:def 5;
hence x in A /\ (X \ B) by A3,XBOOLE_0:def 4;
end;
assume
A5: x in A /\ (X \ B);
then x in (X \ B) by XBOOLE_0:def 4;
then
A6: not x in B by XBOOLE_0:def 5;
x in A by A5,XBOOLE_0:def 4;
hence thesis by A6,XBOOLE_0:def 5;
end;
then
A7: A \ B = A /\ (X \ B) by TARSKI:2;
X \ B in sigma_Field(C) by A2,Th7;
hence thesis by A1,A7,Th9;
end;
theorem Th11:
for N being sequence of S holds for A being Element of S
holds ex F being sequence of S st for n being Element of NAT holds F.n = A
/\ N.n
proof
let N be sequence of S;
let A be Element of S;
defpred P[object,object] means ($1 in NAT implies $2 = A /\ N.$1);
A1: for x being object st x in NAT ex y being object st y in S & P[x,y]
proof
let x be object;
assume x in NAT;
then reconsider x as Element of NAT;
consider y being set such that
A2: y = A /\ N.x;
take y;
thus thesis by A2;
end;
ex F being sequence of S st for x being object st x in NAT holds P[x,F.
x] from FUNCT_2:sch 1(A1);
then consider F being sequence of S such that
A3: for x being object st x in NAT holds P[x,F.x];
take F;
thus thesis by A3;
end;
theorem Th12:
sigma_Field(C) is SigmaField of X
proof
A1: C is nonnegative by Def1;
A2: for M being N_Sub_set_fam of X holds M c= sigma_Field(C) implies union M
in sigma_Field(C)
proof
let M be N_Sub_set_fam of X;
assume
A3: M c= sigma_Field(C);
for W,Z being Subset of X holds (W c= union M & Z c= X \ union M
implies C.W + C.Z <= C.(W \/ Z))
proof
reconsider S = bool X as SigmaField of X by Th3;
let W,Z be Subset of X;
assume that
A4: W c= union M and
A5: Z c= X \ union M;
consider F being sequence of bool X such that
A6: rng F = M by SUPINF_2:def 8;
consider G being sequence of S such that
A7: G.0 = F.0 and
A8: for n being Nat holds G.(n+1) = F.(n+1) \/ G.n by MEASURE2:4;
consider B being sequence of S such that
A9: B.0 = F.0 and
A10: for n being Nat holds B.(n+1) = F.(n+1) \ G.n by MEASURE2:8;
A11: union rng F = union rng B by A7,A8,A9,A10,Th2;
defpred P[Nat] means G.$1 in sigma_Field(C);
A12: for n being Element of NAT holds F.n in sigma_Field(C)
proof
let n be Element of NAT;
F.n in M by A6,FUNCT_2:4;
hence thesis by A3;
end;
A13: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A14: G.k in sigma_Field(C);
A15: F.(k+1) in sigma_Field(C) by A12;
G.(k+1) = F.(k+1) \/ G.k by A8;
hence thesis by A14,A15,Th8;
end;
A16: P[0] by A12,A7;
A17: for n being Nat holds P[n] from NAT_1:sch 2(A16,A13);
consider Q being sequence of S such that
A18: for n being Element of NAT holds Q.n = W /\ B.n by Th11;
A19: union rng Q = W /\ union rng B by A18,Th1;
consider QQ being sequence of S such that
A20: QQ.0 = Q.0 and
A21: for n being Nat holds QQ.(n+1) = Q.(n+1) \/ QQ.n by MEASURE2:4;
reconsider Q,QQ,F,G as sequence of bool X;
A22: F.0 in sigma_Field(C) by A12;
defpred P[Nat] means C.(Z \/ QQ.$1) = C.Z + Ser(C*Q).$1;
A23: C*Q is nonnegative by A1,MEASURE1:25;
A24: for k being Nat st P[k] holds P[k+1]
proof
defpred P[Nat] means QQ.$1 c= G.$1;
let k be Nat;
A25: F.(k+1) \ G.k c= F.(k+1) by XBOOLE_1:36;
A26: QQ.(k+1) = QQ.k \/ Q.(k+1) by A21;
A27: G.k in sigma_Field(C) by A17;
F.(k+1) in sigma_Field(C) by A12;
then
A28: F.(k+1) \ G.k in sigma_Field(C) by A27,Th10;
A29: 0. <= (C*Q).(k+1) by A23,SUPINF_2:39;
A30: 0. <= Ser(C*Q).k by A23,SUPINF_2:40;
QQ.0 = W /\ F.0 by A9,A18,A20;
then
A31: P[0] by A7,XBOOLE_1:17;
for n being Nat holds QQ.n misses (F.(n+1) \ G.n)
proof
let n be Nat;
A32: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A33: QQ.n c= G.n;
A34: W /\ F.(n+1) c= F.(n+1) by XBOOLE_1:17;
W /\ (F.(n+1) \ G.n) c= W /\ F.(n+1) by XBOOLE_1:26,36;
then
A35: W /\ (F.(n+1) \ G.n) c= F.(n+1) by A34;
QQ.(n+1) = Q.(n+1) \/ QQ.n by A21
.= (W /\ B.(n+1)) \/ QQ.n by A18
.= (W /\ (F.(n+1) \ G.n)) \/ QQ.n by A10;
then QQ.(n+1) c= F.(n+1) \/ G.n by A33,A35,XBOOLE_1:13;
hence thesis by A8;
end;
A36: for n being Nat holds P[n] from NAT_1:sch 2(A31,A32);
G.n misses (F.(n+1) \ G.n) by XBOOLE_1:79;
hence thesis by A36,XBOOLE_1:63;
end;
then QQ.k misses (F.(k+1) \ G.k);
then
A37: QQ.k /\ (F.(k+1) \ G.k) = {};
A38: QQ.k c= X \ (F.(k+1) \ G.k)
proof
let z be object;
assume
A39: z in QQ.k;
then not z in F.(k+1) \ G.k by A37,XBOOLE_0:def 4;
hence thesis by A39,XBOOLE_0:def 5;
end;
Q.(k+1) = W /\ B.(k+1) by A18
.= W /\ (F.(k+1) \ G.k) by A10;
then
A40: Q.(k+1) c= F.(k+1) \ G.k by XBOOLE_1:17;
F.(k+1) c= union rng F by FUNCT_2:4,ZFMISC_1:74;
then F.(k+1) \ G.k c= union rng F by A25;
then X \ union rng F c= X \ (F.(k+1) \ G.k) by XBOOLE_1:34;
then Z c= X \ (F.(k+1) \ G.k) by A5,A6;
then Z \/ QQ.k c= X \ (F.(k+1) \ G.k) by A38,XBOOLE_1:8;
then
A41: C.(Q.(k+1)) + C.(Z \/ QQ.k) = C.((Z \/ QQ.k) \/ Q.(k+1)) by A40,A28,Th5
.= C.(Z \/ QQ.(k+1)) by A26,XBOOLE_1:4;
A42: 0. <= C.Z by A1,SUPINF_2:39;
assume C.(Z \/ QQ.k) = C.Z + Ser(C*Q).k;
then C.(Z \/ QQ.(k+1)) = (C.Z + Ser(C*Q).k) + (C*Q).(k+1) by A41,
FUNCT_2:15
.= C.Z + (Ser(C*Q).k + (C*Q).(k+1)) by A42,A30,A29,XXREAL_3:44
.= C.Z + Ser(C*Q).(k+1) by SUPINF_2:def 11;
hence thesis;
end;
QQ.0 = W /\ F.0 by A9,A18,A20;
then
A43: QQ.0 c= F.0 by XBOOLE_1:17;
A44: Ser(C*Q).0 = (C*Q).0 by SUPINF_2:def 11
.= C.(QQ.0) by A20,FUNCT_2:15;
F.0 in rng F by FUNCT_2:4;
then X \ union rng F c= X \ F.0 by XBOOLE_1:34,ZFMISC_1:74;
then Z c= X \ F.0 by A5,A6;
then
A45: P[0] by A22,A43,A44,Th5;
A46: for n being Nat holds P[n] from NAT_1:sch 2(A45,A24);
defpred Q[Nat] means QQ.$1 c= W;
A47: for n being Nat st Q[n] holds Q[n+1]
proof
let n be Nat;
assume
A48: QQ.n c= W;
A49: W /\ B.(n+1) c= W by XBOOLE_1:17;
QQ.(n+1) = Q.(n+1) \/ QQ.n by A21
.= (W /\ B.(n+1)) \/ QQ.n by A18;
then QQ.(n+1) c= W \/ W by A48,A49,XBOOLE_1:13;
hence thesis;
end;
QQ.0 = W /\ B.0 by A18,A20;
then
A50: Q[0] by XBOOLE_1:17;
A51: for n being Nat holds Q[n] from NAT_1:sch 2(A50,A47);
A52: union rng Q = W by A4,A6,A11,A19,XBOOLE_1:28;
A53: C.Z is real implies C.W + C.Z <= C.(W \/ Z )
proof
defpred P[object,object] means
($1 = 0 implies $2 = C.(Z \/ W) - C.Z ) & ($1
<> 0 implies $2 = 0.);
A54: for x being object st x in NAT
ex y being object st y in ExtREAL & P[x, y]
proof
let x be object;
assume x in NAT;
then reconsider x as Element of NAT;
x <> 0 implies ex y being set st y in ExtREAL & P[x,y];
hence thesis;
end;
consider R being sequence of ExtREAL such that
A55: for x being object st x in NAT holds P[x,R.x] from FUNCT_2:sch 1
(A54);
assume
A56: C.Z is real;
for n being Element of NAT holds 0. <= R.n
proof
let n be Element of NAT;
C.Z in REAL or C.Z in {-infty,+infty} by XBOOLE_0:def 3
,XXREAL_0:def 4;
then consider y being Element of REAL such that
A57: y = C.Z by A56,TARSKI:def 2;
Z c= Z \/ W by XBOOLE_1:7;
then C.Z <= C.(Z \/ W) by Def1;
then
A58: C.Z - C.Z <= C.(Z \/ W) - C.Z by XXREAL_3:37;
C.Z - C.Z = y - y by A57,SUPINF_2:3;
hence thesis by A55,A58;
end;
then
A59: R is nonnegative by SUPINF_2:39;
A60: for n being Element of NAT holds Ser(C*Q).n <= C.(Z \/ W) - C.Z
proof
let n be Element of NAT;
A61: Z \/ QQ.n c= Z \/ W by A51,XBOOLE_1:9;
Ser(C*Q).n + C.Z = C.(Z \/ QQ.n) by A46;
then Ser(C*Q).n + C.Z <= C.(Z \/ W) by A61,Def1;
hence thesis by A56,XXREAL_3:45;
end;
A62: for n being Element of NAT holds Ser(C*Q).n <= Ser(R).n
proof
let n be Element of NAT;
defpred P[Nat] means Ser(R).$1 = C.(Z \/ W) - C.Z;
A63: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A64: Ser(R).k = C.(Z \/ W) - C.Z;
set y = Ser(R).k;
thus Ser(R).(k+1) = y + R.(k+1) by SUPINF_2:def 11
.= y + 0. by A55
.= C.(Z \/ W) - C.Z by A64,XXREAL_3:4;
end;
Ser(R).0 = R.0 by SUPINF_2:def 11;
then
A65: P[0] by A55;
for k being Nat holds P[k] from NAT_1:sch 2(A65,A63);
then Ser(R).n = C.(Z \/ W) - C.Z;
hence thesis by A60;
end;
set y = Ser(R).0;
y = R.0 by SUPINF_2:def 11;
then
A66: y = C.(Z \/ W) - C.Z by A55;
A67: C.W <= SUM(C*Q) by A52,Def1;
for k being Element of NAT st 1 <= k holds R.k = 0. by A55;
then
A68: SUM(R) = Ser(R).1 by A59,SUPINF_2:48;
Ser(R).1 = y + R.(0+1) by SUPINF_2:def 11
.= y + 0. by A55
.= C.(Z \/ W) - C.Z by A66,XXREAL_3:4;
then SUM(C*Q) <= C.(Z \/ W) - C.Z by A62,A68,MEASURE3:1;
then C.W <= C.(Z \/ W) - C.Z by A67,XXREAL_0:2;
hence thesis by A56,XXREAL_3:45;
end;
A69: C.Z = +infty implies C.W + C.Z <= C.(W \/ Z)
proof
A70: Z c= W \/ Z by XBOOLE_1:7;
assume
A71: C.Z = +infty;
0. <= C.W by A1,MEASURE1:def 2;
then C.W + C.Z = +infty by A71,XXREAL_3:def 2;
hence thesis by A71,A70,Def1;
end;
0 <= C.Z by A1,MEASURE1:def 2;
then C.Z is Element of REAL or C.Z = +infty by XXREAL_0:14;
hence thesis by A69,A53;
end;
hence thesis by Def2;
end;
for A being set holds A in sigma_Field(C) implies X\A in sigma_Field(C)
by Th7;
then reconsider Y = sigma_Field C as non empty compl-closed sigma-additive
Subset-Family of X by A2,MEASURE1:def 1,def 5;
Y is SigmaField of X;
hence thesis;
end;
registration
let X be set;
let C be C_Measure of X;
cluster sigma_Field(C) -> sigma-additive compl-closed non empty;
coherence by Th12;
end;
definition
let X be set;
let S be SigmaField of X;
let A be N_Measure_fam of S;
redefine func union A -> Element of S; :: redefines union (TARSKI, definition)
coherence by MEASURE2:def 1,MEASURE1:def 5;
end;
definition
let X be set;
let C be C_Measure of X;
func sigma_Meas(C) -> Function of sigma_Field(C),ExtREAL means
:Def3:
for A being Subset of X st A in sigma_Field(C) holds it.A = C.A;
existence
proof
ex D being Function of sigma_Field(C),ExtREAL st for A being Subset of
X holds A in sigma_Field(C) implies D.A = C.A
proof
deffunc F(object) = C.$1;
A1: for S being object st S in sigma_Field(C) holds F(S) in ExtREAL
proof let S be object;
assume
S in sigma_Field(C);
reconsider S as set by TARSKI:1;
C.S in ExtREAL;
hence thesis;
end;
consider D being Function of sigma_Field(C),ExtREAL such that
A2: for S being object st S in sigma_Field(C) holds D.S = F(S) from
FUNCT_2:sch 2(A1);
take D;
thus thesis by A2;
end;
then consider D being Function of sigma_Field(C),ExtREAL such that
A3: for A being Subset of X st A in sigma_Field(C) holds D.A = C.A;
take D;
thus thesis by A3;
end;
uniqueness
proof
let D1,D2 be Function of sigma_Field(C),ExtREAL such that
A4: for A being Subset of X holds A in sigma_Field(C) implies D1.A = C .A and
A5: for A being Subset of X holds A in sigma_Field(C) implies D2.A = C .A;
A6: for A being object st A in sigma_Field(C) holds D1.A = D2.A
proof
let A be object;
assume
A7: A in sigma_Field(C);
then reconsider A as Subset of X;
D1.A = C.A by A4,A7
.= D2.A by A5,A7;
hence thesis;
end;
A8: sigma_Field(C) = dom D2 by FUNCT_2:def 1;
sigma_Field(C) = dom D1 by FUNCT_2:def 1;
hence thesis by A8,A6,FUNCT_1:2;
end;
end;
theorem Th13:
sigma_Meas(C) is Measure of sigma_Field(C)
proof
A1: now
let A be Element of sigma_Field(C);
reconsider A9 = A as Subset of X;
A2: C is nonnegative by Def1;
(sigma_Meas(C)).A9 = C.A9 by Def3;
hence 0.<= (sigma_Meas(C)).A by A2,MEASURE1:def 2;
end;
{} in sigma_Field(C) by PROB_1:4;
then
A3: (sigma_Meas(C)).{} = C.{} by Def3;
A4: now
let A,B be Element of sigma_Field(C);
reconsider A9 = A,B9 = B as Subset of X;
A5: (sigma_Meas(C)).B9 = C.B9 by Def3;
assume A misses B;
then
A6: C.(A9 \/ B9) = C.A9 + C.B9 by Th6;
(sigma_Meas(C)).A9 = C.A9 by Def3;
hence (sigma_Meas(C)).(A \/ B) = (sigma_Meas(C)).A + (sigma_Meas(C)).B by
A5,A6,Def3;
end;
C is zeroed by Def1;
then (sigma_Meas(C)).{} = 0. by A3,VALUED_0:def 19;
hence thesis by A1,A4,MEASURE1:def 2,def 8,VALUED_0:def 19;
end;
::$N Caratheodory's Theorem
theorem Th14:
sigma_Meas(C) is sigma_Measure of sigma_Field(C)
proof
reconsider M = sigma_Meas(C) as Measure of sigma_Field(C) by Th13;
for F being Sep_Sequence of sigma_Field(C) holds M.(union rng F) <= SUM( M*F)
proof
let F be Sep_Sequence of sigma_Field(C);
consider A being Subset of X such that
A1: A = union rng F;
A2: for k being object st k in NAT holds (M*F).k = (C*F).k
proof
let k be object;
assume
A3: k in NAT;
then
A4: (M*F).k = M.(F.k) by FUNCT_2:15;
A5: F.k in sigma_Field(C) by A3,FUNCT_2:5;
reconsider F as sequence of bool X by FUNCT_2:7;
(C*F).k = C.(F.k) by A3,FUNCT_2:15;
hence thesis by A4,A5,Def3;
end;
reconsider F9 = F as sequence of bool X by FUNCT_2:7;
consider a,b being R_eal such that
a = M.A and
A6: b = C.A;
C*F9 is sequence of ExtREAL;
then
A7: M*F = C*F by A2,FUNCT_2:12;
reconsider F as sequence of bool X by FUNCT_2:7;
b <= SUM(C*F) by A1,A6,Def1;
hence thesis by A1,A6,A7,Def3;
end;
hence thesis by MEASURE3:14;
end;
registration
let X be set;
let C be C_Measure of X;
cluster sigma_Meas(C) -> nonnegative sigma-additive zeroed;
coherence by Th14;
end;
theorem Th15:
for A being Subset of X holds C.A = 0. implies A in sigma_Field(C)
proof
let A be Subset of X;
assume
A1: C.A = 0.;
now
let W,Z be Subset of X;
assume that
A2: W c= A and
Z c= X \ A;
Z c= W \/ Z by XBOOLE_1:7;
then
A3: C.Z <= C.(W \/ Z) by Def1;
C is nonnegative by Def1;
then 0.<= C.W by MEASURE1:def 2;
then C.W = 0. by A1,A2,Def1;
hence C.W + C.Z <= C.(W \/ Z) by A3,XXREAL_3:4;
end;
hence thesis by Def2;
end;
theorem
sigma_Meas(C) is complete
proof
let A be Subset of X;
let B;
assume that
A1: B in sigma_Field(C) and
A2: A c= B and
A3: (sigma_Meas(C)).B = 0.;
reconsider B as Subset of X by A1;
C is nonnegative by Def1;
then
A4: 0.<= C.A by MEASURE1:def 2;
C.B = 0. by A1,A3,Def3;
then C.A = 0. by A2,A4,Def1;
hence thesis by Th15;
end;