:: The One-Dimensional Lebesgue Measure As an Example of a
:: Formalization in the Mizar Language of the Classical Definition
:: of a Mathematical Object
:: by J\'ozef Bia{\l}as
::
:: Received February 4, 1995
:: Copyright (c) 1995-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FUNCT_1, NUMBERS, SUBSET_1, SUPINF_2, ARYTM_3, CARD_1, RELAT_1,
TARSKI, ORDINAL2, XXREAL_0, NAT_1, XXREAL_2, ORDINAL1, XBOOLE_0,
ZFMISC_1, FUNCOP_1, MEASURE5, FUNCT_2, SUPINF_1, MCART_1, MEASURE4,
REAL_1, PROB_1, MEASURE1, MEASURE7, FUNCT_7, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, DOMAIN_1, ORDINAL1,
NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, XXREAL_3, RELAT_1, FUNCT_1,
RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, NAT_1, PROB_1, XXREAL_2, SUPINF_1,
SUPINF_2, MEASURE1, MEASURE4, MEASURE5, RECDEF_1;
constructors PARTFUN1, DOMAIN_1, FUNCOP_1, NAT_1, MEASURE4, MEASURE5,
RECDEF_1, SUPINF_1, XREAL_0, RELSET_1, XXREAL_2, MEASURE1, PROB_2;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, FUNCT_2, NUMBERS, XREAL_0,
MEMBERED, MEASURE1, MEASURE4, VALUED_0, XXREAL_2, XXREAL_3, FUNCT_1,
RELSET_1, XXREAL_0;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, MEASURE4, XBOOLE_0, XXREAL_2, VALUED_0;
equalities SUPINF_2;
expansions TARSKI;
theorems TARSKI, SUPINF_2, MEASURE1, FUNCT_1, MEASURE5, MEASURE6, ZFMISC_1,
FUNCT_2, NAT_1, XBOOLE_0, XBOOLE_1, FUNCOP_1, XXREAL_0, ORDINAL1,
XXREAL_2, XXREAL_3, XTUPLE_0;
schemes FUNCT_2, NAT_1, BINOP_2, SUBSET_1, XBOOLE_0, XFAMILY;
begin :: Some theorems about series of R_eal numbers
theorem Th1:
for F being sequence of ExtREAL st for n being Element of NAT
holds F.n = 0. holds SUM(F) = 0.
proof
let F be sequence of ExtREAL;
defpred P[Nat] means Ser(F).$1 = 0.;
assume
A1: for n being Element of NAT holds F.n = 0.;
A2: for t being Nat st P[t] holds P[t+1]
proof
let t be Nat;
assume Ser(F).t = 0.;
hence Ser(F).(t+1) = 0. + F.(t+1) by SUPINF_2:def 11
.= F.(t+1) by XXREAL_3:4
.= 0. by A1;
end;
A3: Ser(F).0 = F.0 by SUPINF_2:def 11
.= 0. by A1;
then
A4: P[0];
A5: for s being Nat holds P[s] from NAT_1:sch 2(A4,A2);
A6: rng Ser(F) = {0.}
proof
thus rng Ser(F) c= {0.}
proof
let x be object;
assume x in rng Ser(F);
then consider s being object such that
A7: s in dom Ser(F) and
A8: x = Ser(F).s by FUNCT_1:def 3;
reconsider s as Element of NAT by A7;
Ser(F).s = 0. by A5;
hence thesis by A8,TARSKI:def 1;
end;
let x be object;
assume x in {0.};
then dom Ser(F) = NAT & x = 0. by FUNCT_2:def 1,TARSKI:def 1;
hence thesis by A3,FUNCT_1:def 3;
end;
sup {0.} = 0. by XXREAL_2:11;
hence thesis by A6;
end;
theorem Th2:
for F being sequence of ExtREAL st F is nonnegative holds for
n being Nat holds F.n <= Ser(F).n
proof
let F be sequence of ExtREAL;
assume
A1: F is nonnegative;
let n be Nat;
per cases;
suppose
n = 0;
hence thesis by SUPINF_2:def 11;
end;
suppose
n <> 0;
then consider k being Nat such that
A2: n = k + 1 by NAT_1:6;
reconsider k as Element of NAT by ORDINAL1:def 12;
A3: 0. <= Ser(F).k by A1,SUPINF_2:40;
Ser(F).n = Ser(F).k + F.n by A2,SUPINF_2:def 11;
then 0. + F.n <= Ser(F).n by A3,XXREAL_3:36;
hence thesis by XXREAL_3:4;
end;
end;
theorem Th3:
for F,G,H being sequence of ExtREAL st G is nonnegative & H
is nonnegative holds (for n being Element of NAT holds F.n = G.n + H.n )
implies for n being Nat holds (Ser F).n = (Ser G).n + (Ser H).n
proof
let F,G,H be sequence of ExtREAL;
assume that
A1: G is nonnegative and
A2: H is nonnegative;
defpred P[Nat] means (Ser F).$1 = (Ser G).$1 + (Ser H).$1;
assume
A3: for n being Element of NAT holds F.n = G.n + H.n;
A4: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A5: (Ser F).k = (Ser G).k + (Ser H).k;
set n = k+1;
A6: Ser(G).(k + 1) = Ser(G).k + G.(k + 1) & Ser(H).(k + 1) = Ser(H).k + H
.(k + 1 ) by SUPINF_2:def 11;
A7: 0. <= H.(k+1) by A2,SUPINF_2:39;
A8: F.(k+1) = G.(k+1) + H.(k+1) & 0. <= G.(k+1) by A1,A3,SUPINF_2:39;
A9: 0. <= (Ser G).k by A1,SUPINF_2:40;
A10: 0. <= (Ser G).(k+1) by A1,SUPINF_2:40;
A11: 0. <= (Ser H).k by A2,SUPINF_2:40;
0. <= G.n & 0. <= H.n by A1,A2,SUPINF_2:39;
then 0. + 0. <= G.n + H.n by XXREAL_3:36;
then 0. <= F.(k+1) by A3;
then
(Ser G).k + (Ser H).k + F.(k + 1) = ((Ser G).k + F.(k+1)) + (Ser H).k
by A9,A11,XXREAL_3:44
.= (((Ser G).k + G.(k+1)) + H.(k+1)) + (Ser H).k by A9,A7,A8,XXREAL_3:44
.= (Ser G).(k+1) + (Ser H).(k+1) by A6,A11,A10,A7,XXREAL_3:44;
hence thesis by A5,SUPINF_2:def 11;
end;
A12: (Ser H).0 = H.0 by SUPINF_2:def 11;
(Ser F).0 = F.0 & (Ser G).0 = G.0 by SUPINF_2:def 11;
then
A13: P[0] by A3,A12;
thus for k being Nat holds P[k] from NAT_1:sch 2(A13,A4);
end;
theorem Th4:
for F,G,H being sequence of ExtREAL st for n being Element of
NAT holds F.n = G.n + H.n holds G is nonnegative & H is nonnegative implies SUM
(F) <= SUM(G) + SUM(H)
proof
let F,G,H be sequence of ExtREAL;
assume
A1: for n being Element of NAT holds F.n = G.n + H.n;
defpred P[Nat] means Ser(F).$1 = Ser(G).$1 + Ser(H).$1;
assume that
A2: G is nonnegative and
A3: H is nonnegative;
A4: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
A5: Ser(G).(k+1) = Ser(G).k + G.(k+1) & Ser(H).(k+1) = Ser(H).k + H.(k+1)
by SUPINF_2:def 11;
A6: 0. <= Ser(G).k by A2,SUPINF_2:40;
A7: 0. <= Ser(H).(k+1) by A3,SUPINF_2:40;
A8: 0. <= H.(k+1) by A3,SUPINF_2:39;
A9: 0. <= Ser(H).k by A3,SUPINF_2:40;
0. <= G.(k+1) & 0. <= H.(k+1) by A2,A3,SUPINF_2:39;
then 0. + 0. <= G.(k+1) + H.(k+1) by XXREAL_3:36;
then
A10: Ser(F).(k+1) = Ser(F).k + F.(k+1) & 0. <= F.(k+1) by A1,SUPINF_2:def 11;
A11: 0. <= G.(k+1) by A2,SUPINF_2:39;
assume Ser(F).k = Ser(G).k + Ser(H).k;
hence Ser(F).(k+1) = Ser(G).k + (Ser(H).k + F.(k+1)) by A10,A6,A9,
XXREAL_3:44
.= Ser(G).k + (Ser(H).k + (G.(k+1) + H.(k+1))) by A1
.= Ser(G).k + ((Ser(H).k + H.(k+1)) + G.(k+1)) by A11,A9,A8,XXREAL_3:44
.= Ser(G).(k+1) + Ser(H).(k+1) by A5,A6,A11,A7,XXREAL_3:44;
end;
A12: Ser(H).0 = H.0 by SUPINF_2:def 11;
Ser(F).0 = F.0 & Ser(G).0 = G.0 by SUPINF_2:def 11;
then
A13: P[0] by A1,A12;
A14: for n being Nat holds P[n] from NAT_1:sch 2(A13,A4);
SUM(G) + SUM(H) is UpperBound of rng Ser(F)
proof
let x be ExtReal;
A15: dom Ser(F) = NAT by FUNCT_2:def 1;
assume x in rng Ser(F);
then consider n being object such that
A16: n in NAT and
A17: x = Ser(F).n by A15,FUNCT_1:def 3;
reconsider n as Element of NAT by A16;
Ser(H).n <= sup(rng Ser(H)) by FUNCT_2:4,XXREAL_2:4;
then
A18: Ser(H).n <= SUM(H);
Ser(G).n <= sup(rng Ser(G)) by FUNCT_2:4,XXREAL_2:4;
then Ser(G).n <= SUM(G);
then Ser(G).n + Ser(H).n <= SUM(G) + SUM(H) by A18,XXREAL_3:36;
hence thesis by A14,A17;
end;
then sup(rng Ser(F)) <= SUM(G) + SUM(H) by XXREAL_2:def 3;
hence thesis;
end;
theorem Th5:
for F,G being sequence of ExtREAL holds ( for n being Element
of NAT holds F.n <= G.n) implies for n being Element of NAT holds (Ser(F)).n <=
SUM(G)
proof
let F,G be sequence of ExtREAL;
assume
A1: for n being Element of NAT holds F.n <= G.n;
let n be Element of NAT;
set y = Ser(G).n;
dom Ser(G) = NAT by FUNCT_2:def 1;
then SUM(G) = sup(rng Ser(G)) & y in rng Ser(G) by FUNCT_1:def 3;
hence thesis by A1,SUPINF_2:42,XXREAL_2:61;
end;
theorem Th6:
for F being sequence of ExtREAL holds F is nonnegative
implies for n being Element of NAT holds (Ser(F)).n <= SUM(F)
proof
let F be sequence of ExtREAL;
for n being Element of NAT holds F.n <= F.n;
hence thesis by Th5;
end;
definition
let S be non empty set;
let H be Function of S,ExtREAL;
func On H -> sequence of ExtREAL means
:Def1:
for n being Element of NAT
holds (n in S implies it.n = H.n) & (not n in S implies it.n = 0.);
existence
proof
defpred P[Element of NAT,Element of ExtREAL] means ($1 in S implies $2 = H
.$1) & (not $1 in S implies $2 = 0.);
A1: for n being Element of NAT holds ex y being Element of ExtREAL st P[n, y]
proof
let n be Element of NAT;
per cases;
suppose
n in S;
then reconsider n as Element of S;
take H.n;
thus thesis;
end;
suppose
A2: not n in S;
take 0.;
thus thesis by A2;
end;
end;
consider GG being sequence of ExtREAL such that
A3: for n being Element of NAT holds P[n,GG.n] from FUNCT_2:sch 3(A1);
take GG;
thus thesis by A3;
end;
uniqueness
proof
let G1,G2 be sequence of ExtREAL such that
A4: for n being Element of NAT holds (n in S implies G1.n = H.n) & ((
not n in S) implies G1.n = 0.) and
A5: for n being Element of NAT holds (n in S implies G2.n = H.n) & ((
not n in S) implies G2.n = 0.);
for n being object st n in NAT holds G1.n = G2.n
proof
let n be object;
assume n in NAT;
then reconsider n as Element of NAT;
per cases;
suppose
A6: n in S;
then G1.n = H.n by A4;
hence thesis by A5,A6;
end;
suppose
A7: not n in S;
then G1.n = 0. by A4;
hence thesis by A5,A7;
end;
end;
hence thesis by FUNCT_2:12;
end;
end;
theorem Th7:
for X being non empty set for G being Function of X,ExtREAL st G
is nonnegative holds On G is nonnegative
proof
let X be non empty set;
let G be Function of X,ExtREAL;
assume
A1: G is nonnegative;
for n being Element of NAT holds 0. <= (On G).n
proof
let n be Element of NAT;
per cases;
suppose
A2: n in X;
then (On G).n = G.n by Def1;
hence thesis by A1,A2,SUPINF_2:39;
end;
suppose
not n in X;
hence thesis by Def1;
end;
end;
hence thesis by SUPINF_2:39;
end;
theorem Th8:
for F being sequence of ExtREAL st F is nonnegative holds for
n,k being Nat st n <= k holds Ser(F).n <= Ser(F).k
proof
let F be sequence of ExtREAL;
assume
A1: F is nonnegative;
let n,k be Nat;
defpred P[Nat] means Ser(F).n <= Ser(F).(n+$1);
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A3: Ser(F).n <= Ser(F).(n+k);
Ser(F).(n+k) <= Ser(F).((n+k)+1) by A1,SUPINF_2:40;
hence thesis by A3,XXREAL_0:2;
end;
assume n <= k;
then consider s being Nat such that
A4: k = (n qua Complex) + s by NAT_1:10;
A5: k = n + s by A4;
A6: P[0];
for s being Nat holds P[s] from NAT_1:sch 2(A6,A2);
hence thesis by A5;
end;
theorem Th9:
for k being Nat holds for F being sequence of
ExtREAL holds ((for n being Element of NAT st n <> k holds F.n = 0.) implies (
for n being Element of NAT st n < k holds Ser(F).n = 0.) & for n being Element
of NAT st k <= n holds Ser(F).n = F.k )
proof
let k be Nat;
let F be sequence of ExtREAL;
defpred P[Nat] means $1 < k implies Ser(F).$1 = 0.;
assume
A1: for n being Element of NAT st n <> k holds F.n = 0.;
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A3: n < k implies Ser(F).n = 0.;
assume
A4: n+1 < k;
then
A5: n <= n+1 & F.(n+1) = 0. by A1,NAT_1:11;
Ser(F).(n+1) = Ser(F).n + F.(n+1) by SUPINF_2:def 11
.= 0. by A3,A4,A5,XXREAL_0:2;
hence thesis;
end;
A6: P[0]
proof
assume 0 < k;
then F.0 = 0. by A1;
hence thesis by SUPINF_2:def 11;
end;
A7: for n being Nat holds P[n] from NAT_1:sch 2(A6,A2);
defpred P[Nat] means k <= $1 implies Ser(F).$1 = F.k;
A8: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A9: k <= n implies Ser(F).n = F.k;
assume
A10: k <= n+1;
per cases by A10,NAT_1:8;
suppose
A11: k <= n;
then k <> n+1 by NAT_1:13;
then
A12: F.(n+1) = 0. by A1;
Ser(F).(n+1) = Ser(F).n + F.(n+1) by SUPINF_2:def 11
.= F.k by A9,A11,A12,XXREAL_3:4;
hence thesis;
end;
suppose
A13: k = n + 1;
then n < k by NAT_1:13;
then
A14: Ser(F).n = 0. by A7;
Ser(F).(n+1) = Ser(F).n + F.(n+1) by SUPINF_2:def 11
.= F.k by A13,A14,XXREAL_3:4;
hence thesis;
end;
end;
A15: P[0]
proof
A16: 0 <= k by NAT_1:2;
assume k <= 0;
then F.0 = F.k by A16,XXREAL_0:1;
hence thesis by SUPINF_2:def 11;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A15,A8);
hence thesis by A7;
end;
theorem Th10:
for G being sequence of ExtREAL st G is nonnegative holds
for S being non empty Subset of NAT holds for H being Function of S,NAT st H is
one-to-one holds SUM(On(G*H)) <= SUM(G)
proof
let G be sequence of ExtREAL;
assume
A1: G is nonnegative;
let S be non empty Subset of NAT;
let H be Function of S,NAT;
defpred P[Nat] means
ex m being Element of NAT st for F being
sequence of ExtREAL st F is nonnegative holds Ser(On(F*H)).$1 <= Ser(F).m;
assume
A2: H is one-to-one;
A3: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
given m0 being Element of NAT such that
A4: for F being sequence of ExtREAL st F is nonnegative holds Ser
(On(F*H)).k <= Ser(F).m0;
per cases;
suppose
A5: k+1 in S;
reconsider m1 = H.(k+1) as Element of NAT;
set m = m0 + m1;
take m;
let F be sequence of ExtREAL;
defpred QQ0[Element of NAT,Element of ExtREAL] means (($1 = H.(k+1)
implies $2 = F.$1) & ($1 <> H.(k+1) implies $2 = 0.));
A6: for n being Element of NAT holds ex y being Element of ExtREAL st
QQ0[n,y]
proof
let n be Element of NAT;
per cases;
suppose
A7: n = H.(k+1);
take F.n;
thus thesis by A7;
end;
suppose
A8: n <> H.(k+1);
take 0.;
thus thesis by A8;
end;
end;
consider G0 being sequence of ExtREAL such that
A9: for n being Element of NAT holds QQ0[n,G0.n] from FUNCT_2:sch 3
(A6);
reconsider GG0 = On(G0*H) as sequence of ExtREAL;
A10: for n being Element of NAT holds n <> k+1 implies GG0.n = 0.
proof
let n be Element of NAT;
assume
A11: n <> k+1;
per cases;
suppose
A12: n in S;
then
A13: GG0.n = (G0*H).n by Def1
.= G0.(H.n) by A12,FUNCT_2:15;
reconsider n as Element of S by A12;
not H.n = H.(k+1) by A2,A5,A11,FUNCT_2:19;
hence thesis by A9,A13;
end;
suppose
not n in S;
hence thesis by Def1;
end;
end;
assume
A14: F is nonnegative;
for n being Element of NAT holds 0. <= G0.n
proof
let n be Element of NAT;
per cases;
suppose
n = H.(k+1);
then G0.n = F.n by A9;
hence thesis by A14,SUPINF_2:39;
end;
suppose
not n = H.(k+1);
hence thesis by A9;
end;
end;
then
A15: G0 is nonnegative by SUPINF_2:39;
reconsider n = k+1 as Element of S by A5;
defpred QQ1[Element of NAT,Element of ExtREAL] means (($1 <> H.(k+1)
implies $2 = F.$1) & ($1 = H.(k+1) implies $2 = 0.));
A16: for n being Element of NAT holds ex y being Element of ExtREAL st
QQ1[n,y]
proof
let n be Element of NAT;
per cases;
suppose
A17: n <> H.(k+1);
take F.n;
thus thesis by A17;
end;
suppose
A18: n = H.(k+1);
take 0.;
thus thesis by A18;
end;
end;
consider G1 being sequence of ExtREAL such that
A19: for n being Element of NAT holds QQ1[n,G1.n] from FUNCT_2:sch 3
(A16);
set GG1 = On(G1*H);
A20: GG1.(k+1) = (G1*H).n by Def1
.= G1.(H.n) by FUNCT_2:15
.= 0. by A19;
A21: GG0.n = (G0*H).n by Def1
.= G0.(H.n) by FUNCT_2:15
.= F.(H.n) by A9;
then
A22: (Ser GG0).(k+1) = F.(H.(k+1)) by A10,Th9;
A23: for n being Element of NAT holds n <> k+1 & n in S implies GG1.n =
F.(H.n)
proof
let n be Element of NAT;
assume that
A24: n <> k+1 and
A25: n in S;
A26: GG1.n = (G1*H).n by A25,Def1
.= G1.(H.n) by A25,FUNCT_2:15;
reconsider n as Element of S by A25;
not H.n = H.(k+1) by A2,A5,A24,FUNCT_2:19;
hence thesis by A19,A26;
end;
A27: for n being Element of NAT holds On(F*H).n = GG0.n + GG1.n
proof
let n be Element of NAT;
per cases;
suppose
A28: n = k+1;
then On(F*H).n = (F*H).n by A5,Def1
.= F.(H.n) by A5,A28,FUNCT_2:15
.= GG0.n + GG1.n by A21,A20,A28,XXREAL_3:4;
hence thesis;
end;
suppose
A29: n <> k+1;
now
per cases;
suppose
A30: n in S;
then
A31: GG1.n = F.(H.n) by A23,A29;
A32: GG0.n = 0. by A10,A29;
On(F*H).n = (F*H).n by A30,Def1
.= F.(H.n) by A30,FUNCT_2:15
.= GG0.n + GG1.n by A32,A31,XXREAL_3:4;
hence thesis;
end;
suppose
A33: not n in S;
then
A34: GG1.n = 0. by Def1;
A35: GG0.n = 0. by A10,A29;
On(F*H).n = 0. by A33,Def1
.= GG0.n + GG1.n by A35,A34;
hence thesis;
end;
end;
hence thesis;
end;
end;
m1 <= m by NAT_1:11;
then
A36: (Ser G0).m = G0.(H.(k+1)) by A9,Th9;
set v = H.n;
A37: (Ser GG1).(k+1) = (Ser GG1).k + GG1.(k+1) by SUPINF_2:def 11
.= (Ser On(G1*H)).k by A20,XXREAL_3:4;
A38: G0.v = F.v by A9;
for n being Element of NAT holds 0. <= G1.n
proof
let n be Element of NAT;
per cases;
suppose
n <> H.(k+1);
then G1.n = F.n by A19;
hence thesis by A14,SUPINF_2:39;
end;
suppose
n = H.(k+1);
hence thesis by A19;
end;
end;
then
A39: G1 is nonnegative by SUPINF_2:39;
then G1*H is nonnegative by MEASURE1:25;
then
A40: GG1 is nonnegative by Th7;
G0*H is nonnegative by A15,MEASURE1:25;
then GG0 is nonnegative by Th7;
then
A41: (Ser On(F*H)).(k+1) = (Ser GG0).(k+1) + (Ser GG1).(k+1) by A40,A27,Th3;
(Ser On(G1*H)).k <= Ser(G1).m0 & Ser(G1).m0 <= Ser(G1).m by A4,A39,Th8,
NAT_1:11;
then
A42: (Ser GG1).(k+1) <= (Ser G1).m by A37,XXREAL_0:2;
for m being Element of NAT holds F.m = G0.m + G1.m
proof
let m be Element of NAT;
per cases;
suppose
m = H.(k+1);
then G0.m = F.m & G1.m = 0. by A9,A19;
hence thesis by XXREAL_3:4;
end;
suppose
m <> H.(k+1);
then G0.m = 0. & G1.m = F.m by A9,A19;
hence thesis by XXREAL_3:4;
end;
end;
then (Ser F).m = (Ser G0).m + (Ser G1).m by A15,A39,Th3;
hence thesis by A22,A36,A38,A42,A41,XXREAL_3:36;
end;
suppose
A43: not k+1 in S;
take m0;
let F be sequence of ExtREAL;
A44: On(F*H).(k+1) = 0. by A43,Def1;
assume
A45: F is nonnegative;
Ser(On(F*H)).(k+1) = Ser(On(F*H)).k + (On(F*H)).(k+1) by SUPINF_2:def 11
.= Ser(On(F*H)).k by A44,XXREAL_3:4;
hence thesis by A4,A45;
end;
end;
A46: P[0]
proof
per cases;
suppose
A47: 0 in S;
reconsider m = H.0 as Element of NAT;
take m;
let F be sequence of ExtREAL;
Ser(On(F*H)).0 = (On(F*H)).0 by SUPINF_2:def 11;
then
A48: Ser(On(F*H)).0 = (F*H).0 by A47,Def1
.= F.(H.0) by A47,FUNCT_2:15;
assume F is nonnegative;
hence thesis by A48,Th2;
end;
suppose
A49: not 0 in S;
take m = 0;
let F be sequence of ExtREAL;
assume F is nonnegative;
then
A50: 0. <= F.0 & F.0 <= Ser(F).m by Th2,SUPINF_2:39;
Ser(On(F*H)).0 = (On(F*H)).0 by SUPINF_2:def 11;
then Ser(On(F*H)).0 = 0. by A49,Def1;
hence thesis by A50,XXREAL_0:2;
end;
end;
A51: for k being Nat holds P[k] from NAT_1:sch 2(A46,A3);
for x being ExtReal st x in rng Ser(On(G*H)) holds ex y being
ExtReal st y in rng Ser(G) & x <= y
proof
let x be ExtReal;
assume
A52: x in rng Ser(On(G*H));
ex y being ExtReal st y in rng Ser(G) & x <= y
proof
consider n being object such that
A53: n in dom Ser(On(G*H)) and
A54: x = Ser(On(G*H)).n by A52,FUNCT_1:def 3;
reconsider n as Element of NAT by A53;
consider m being Element of NAT such that
A55: for F being sequence of ExtREAL st F is nonnegative holds
Ser(On(F*H)).n <= Ser(F).m by A51;
take Ser(G).m;
dom Ser(G) = NAT by FUNCT_2:def 1;
hence thesis by A1,A54,A55,FUNCT_1:def 3;
end;
hence thesis;
end;
then
sup(rng Ser(On(G*H))) <= sup(rng Ser(G)) by XXREAL_2:63;
hence thesis;
end;
theorem Th11:
for F,G being sequence of ExtREAL st G is nonnegative holds
for S being non empty Subset of NAT holds for H being Function of S,NAT st H is
one-to-one holds (for k being Element of NAT holds ((k in S implies F.k = (G*H)
.k) & ((not k in S) implies F.k = 0.))) implies SUM(F) <= SUM(G)
proof
let F,G be sequence of ExtREAL;
assume
A1: G is nonnegative;
let S be non empty Subset of NAT;
let H be Function of S,NAT;
assume
A2: H is one-to-one;
assume for k being Element of NAT holds (k in S implies F.k = (G*H).k) & ((
not k in S) implies F.k = 0.);
then F = On(G*H) by Def1;
hence thesis by A1,A2,Th10;
end;
::
:: Outside Lebesque measure
::
REAL in bool REAL by ZFMISC_1:def 1;
then reconsider G0 = NAT --> REAL as sequence of bool REAL by FUNCOP_1:45;
Lm1: rng G0 = {REAL} by FUNCOP_1:8;
then
Lm2: REAL c= union rng G0 by ZFMISC_1:25;
Lm3: for n being Element of NAT holds G0.n is Interval
proof
let n be Element of NAT;
G0.n in {REAL} by Lm1,FUNCT_2:4;
hence thesis by TARSKI:def 1;
end;
definition
let A be Subset of REAL;
mode Interval_Covering of A -> sequence of bool REAL means
:Def2:
A c= union(rng it) & for n being Element of NAT holds it.n is Interval;
existence by Lm2,Lm3,XBOOLE_1:1;
end;
definition
let A be Subset of REAL;
let F be Interval_Covering of A;
let n be Element of NAT;
redefine func F.n ->Interval; :: redefines . (FUNCT_1, definition)
correctness by Def2;
end;
definition
let F be sequence of bool REAL;
mode Interval_Covering of F -> sequence of Funcs(NAT,bool REAL) means
:
Def3: for n being Element of NAT holds it.n is Interval_Covering of F.n;
existence
proof
reconsider G = G0 as Element of Funcs(NAT,bool REAL) by FUNCT_2:8;
reconsider H = NAT --> G as sequence of Funcs(NAT,bool REAL);
take H;
A1: for n being Element of NAT holds G0 is Interval_Covering of F.n
by Lm2,XBOOLE_1:1,Def2,Lm3;
for n being Element of NAT holds H.n is Interval_Covering of F.n
proof
let n be Element of NAT;
H.n = G by FUNCOP_1:7;
hence thesis by A1;
end;
hence thesis;
end;
end;
definition
let A be Subset of REAL;
let F be Interval_Covering of A;
deffunc F(Element of NAT) = diameter(F.$1);
func F vol -> sequence of ExtREAL means
:Def4:
for n being Element of NAT holds it.n = diameter(F.n);
existence
proof
thus ex G being sequence of ExtREAL st for n being Element of NAT
holds G.n = F(n) from FUNCT_2:sch 4;
end;
uniqueness
proof
thus for G1,G2 being sequence of ExtREAL st (for n being Element of
NAT holds G1.n = F(n)) & (for n being Element of NAT holds G2.n = F(n)) holds
G1=G2 from BINOP_2:sch 1;
end;
end;
theorem Th12:
for A being Subset of REAL holds for F being Interval_Covering
of A holds (F vol) is nonnegative
proof
let A be Subset of REAL;
let F be Interval_Covering of A;
for n being Element of NAT holds 0. <= (F vol).n
proof
let n be Element of NAT;
(F vol).n = diameter(F.n) by Def4;
hence thesis by MEASURE5:13;
end;
hence thesis by SUPINF_2:39;
end;
definition
let F be sequence of bool REAL;
let H be Interval_Covering of F;
let n be Element of NAT;
redefine func H.n -> Interval_Covering of F.n; :: redefines . (FUNCT_1, definition)
correctness by Def3;
end;
definition
let F be sequence of bool REAL;
let G be Interval_Covering of F;
func G vol -> sequence of Funcs(NAT,ExtREAL) means
for n being Element of NAT holds it.n = (G.n) vol;
existence
proof
defpred P[Element of NAT,set] means $2 = (G.$1) vol;
A1: for n being Element of NAT holds ex y being Element of Funcs(NAT,
ExtREAL) st P[n,y]
proof
let n be Element of NAT;
(G.n) vol is Element of Funcs(NAT,ExtREAL) by FUNCT_2:8;
hence thesis;
end;
ex G0 being sequence of Funcs(NAT,ExtREAL) st for n being Element
of NAT holds P[n,G0.n] from FUNCT_2:sch 3(A1);
hence thesis;
end;
uniqueness
proof
deffunc F(Element of NAT) = (G.$1) vol;
thus for F1,F2 be sequence of Funcs(NAT,ExtREAL) st (for n being
Element of NAT holds F1.n = F(n)) & (for n being Element of NAT holds F2.n = F(
n)) holds F1 = F2 from BINOP_2:sch 1;
end;
end;
definition
let A be Subset of REAL;
let F be Interval_Covering of A;
func vol F -> R_eal equals
SUM(F vol);
correctness;
end;
definition
let F be sequence of (bool REAL);
let G be Interval_Covering of F;
func vol(G) -> sequence of ExtREAL means
:Def7:
for n being Element of NAT holds it.n = vol(G.n);
existence
proof
defpred P[Element of NAT,Element of ExtREAL] means $2 = vol(G.$1);
A1: for n being Element of NAT holds ex y being Element of ExtREAL st P[n, y];
consider G0 being sequence of ExtREAL such that
A2: for n being Element of NAT holds P[n,G0.n] from FUNCT_2:sch 3(A1);
take G0;
thus thesis by A2;
end;
uniqueness
proof
deffunc F(Element of NAT) = vol(G.$1);
thus for F1,F2 being sequence of ExtREAL st (for n being Element of
NAT holds F1.n = F(n)) & (for n being Element of NAT holds F2.n = F(n)) holds
F1 = F2 from BINOP_2:sch 1;
end;
end;
theorem Th13:
for F being sequence of (bool REAL) holds for G being
Interval_Covering of F holds for n being Element of NAT holds 0. <= (vol(G)).n
proof
let F be sequence of bool REAL;
let G be Interval_Covering of F;
let n be Element of NAT;
for k being Element of NAT holds 0. <= ((G.n) vol).k
proof
let k be Element of NAT;
0. <= diameter((G.n).k) by MEASURE5:13;
hence thesis by Def4;
end;
then
A1: ((G.n) vol) is nonnegative by SUPINF_2:39;
(vol(G)).n = vol(G.n) by Def7;
hence thesis by A1,MEASURE6:2;
end;
definition
let A be Subset of REAL;
defpred P[object] means ex F being Interval_Covering of A st $1 = vol(F);
func Svc(A) -> Subset of ExtREAL means
:Def8:
for x being R_eal holds x in
it iff ex F being Interval_Covering of A st x = vol(F);
existence
proof
consider D being set such that
A1: for x being object holds x in D iff x in ExtREAL & P[x] from XBOOLE_0
:sch 1;
for z being object holds z in D implies z in ExtREAL by A1;
then reconsider D as Subset of ExtREAL by TARSKI:def 3;
take D;
thus thesis by A1;
end;
uniqueness
proof
let D1,D2 be Subset of ExtREAL such that
A2: for x being R_eal holds x in D1 iff P[x] and
A3: for x being R_eal holds x in D2 iff P[x];
thus D1 = D2 from SUBSET_1:sch 2(A2,A3);
end;
end;
registration
let A be Subset of REAL;
cluster Svc(A) -> non empty;
coherence
proof
REAL c= REAL;
then consider F0 being sequence of bool REAL such that
A1: rng F0 = {REAL,{}REAL} and
A2: F0.0 = REAL & for n being Nat st 0 < n holds F0.n = {}
REAL by MEASURE1:19;
union{REAL,{}} = REAL \/ {} & for n being Element of NAT holds F0.n is
Interval by A2,NAT_1:3,ZFMISC_1:75;
then reconsider F0 as Interval_Covering of A by A1,Def2;
defpred P[set] means ex F being Interval_Covering of A st $1 = vol(F);
consider D being set such that
A3: for x being set holds x in D iff x in ExtREAL & P[x] from XFAMILY
:sch 1;
vol F0 in D by A3;
hence thesis by Def8;
end;
end;
definition
let A be Subset of REAL;
func COMPLEX(A) -> Element of ExtREAL equals
inf(Svc(A));
correctness;
end;
definition
func OS_Meas -> Function of bool REAL,ExtREAL means
:Def10:
for A being Subset of REAL holds it.A = inf(Svc(A));
existence
proof
consider G being Function of bool REAL,ExtREAL such that
A1: for A being Subset of REAL holds G.A = COMPLEX(A) from FUNCT_2:sch
4;
take G;
for A being Subset of REAL holds G.A = inf(Svc(A))
proof
let A be Subset of REAL;
G.A = COMPLEX(A) by A1;
hence thesis;
end;
hence thesis;
end;
uniqueness
proof
deffunc F(Subset of REAL) = inf(Svc($1));
thus for F1,F2 being Function of bool REAL,ExtREAL st (for A being Subset
of REAL holds F1.A = F(A)) & (for A being Subset of REAL holds F2.A = F(A))
holds F1 = F2 from BINOP_2:sch 1;
end;
end;
definition
let F be sequence of bool REAL;
let G be Interval_Covering of F;
let H be sequence of [:NAT,NAT:] such that
A1: rng H = [:NAT,NAT:];
func On(G,H) -> Interval_Covering of union rng F means
:Def11:
for n being Element of NAT holds it.n = (G.(pr1(H).n)).(pr2(H).n);
existence
proof
defpred P[Element of NAT,Subset of REAL] means $2 = (G.(pr1(H).$1)).(pr2(H
).$1);
A2: for n being Element of NAT holds ex y being Subset of REAL st P[n,y];
consider GG being sequence of bool REAL such that
A3: for n being Element of NAT holds P[n,GG.n] from FUNCT_2:sch 3(A2);
A4: union rng F c= union(rng GG)
proof
let x be object;
assume x in union rng F;
then consider A being set such that
A5: x in A and
A6: A in rng F by TARSKI:def 4;
consider n1 being object such that
A7: n1 in dom F and
A8: A = F.n1 by A6,FUNCT_1:def 3;
reconsider n1 as Element of NAT by A7;
F.n1 c= union rng(G.n1) by Def2;
then consider AA being set such that
A9: x in AA and
A10: AA in rng(G.n1) by A5,A8,TARSKI:def 4;
consider n2 being object such that
A11: n2 in dom(G.n1) and
A12: AA = (G.n1).n2 by A10,FUNCT_1:def 3;
reconsider n2 as Element of NAT by A11;
consider n being object such that
A13: n in dom(H) and
A14: [n1,n2] = H.n by A1,FUNCT_1:def 3;
reconsider n as Element of NAT by A13;
[pr1(H).n,pr2(H).n] = [n1,n2] by A14,FUNCT_2:119;
then pr1(H).n = n1 & pr2(H).n = n2 by XTUPLE_0:1;
then
A15: x in GG.n by A3,A9,A12;
GG.n in rng GG by FUNCT_2:4;
hence thesis by A15,TARSKI:def 4;
end;
for n being Element of NAT holds GG.n is Interval
proof
let n be Element of NAT;
GG.n = (G.(pr1(H).n)).(pr2(H).n) by A3;
hence thesis;
end;
then reconsider GG as Interval_Covering of union rng F by A4,Def2;
take GG;
thus thesis by A3;
end;
uniqueness
proof
let G1,G2 be Interval_Covering of union rng F such that
A16: for n being Element of NAT holds G1.n = (G.(pr1(H).n)).(pr2(H).n) and
A17: for n being Element of NAT holds G2.n = (G.(pr1(H).n)).(pr2(H).n);
for n being object st n in NAT holds G1.n = G2.n
proof
let n be object;
assume n in NAT;
then reconsider n as Element of NAT;
G1.n = (G.(pr1(H).n)).(pr2(H).n) by A16;
hence thesis by A17;
end;
hence thesis by FUNCT_2:12;
end;
end;
reconsider D = NAT --> {}REAL as sequence of bool REAL;
theorem Th14:
for H being sequence of [:NAT,NAT:] st H is one-to-one & rng
H = [:NAT,NAT:] holds for k being Nat holds ex m being Element of
NAT st for F being sequence of bool REAL holds for G being
Interval_Covering of F holds Ser((On(G,H)) vol).k <= Ser(vol(G)).m
proof
reconsider y = D as Element of Funcs(NAT,bool REAL) by FUNCT_2:8;
let H be sequence of [:NAT,NAT:];
assume that
A1: H is one-to-one and
A2: rng H = [:NAT,NAT:];
defpred P[Nat] means
ex m being Element of NAT st for F being
sequence of bool REAL holds for G being Interval_Covering of F holds Ser((
On(G,H)) vol).($1) <= Ser(vol(G)).m;
A3: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
set N0 = {s where s is Element of NAT : pr1(H).(k+1) = pr1(H).s};
A4: N0 c= NAT
proof
let s1 be object;
assume s1 in N0;
then ex s being Element of NAT st s = s1 & pr1(H).(k+1) = pr1(H).s;
hence thesis;
end;
k+1 in N0;
then reconsider N0 as non empty Subset of NAT by A4;
given m0 being Element of NAT such that
A5: for F being sequence of bool REAL holds for G being
Interval_Covering of F holds Ser((On(G,H)) vol).k <= Ser(vol(G)).m0;
take m = m0 + pr1(H).(k+1);
let F be sequence of bool REAL;
let G be Interval_Covering of F;
defpred QQ1[Element of NAT,Function] means (($1 <> pr1(H).(k+1) implies
for m being Element of NAT holds $2.m = (G.$1).m) & ($1 = pr1(H).(k+1) implies
for m being Element of NAT holds $2.m = {}));
A6: for n being Element of NAT holds ex y being Element of Funcs(NAT,bool
REAL) st QQ1[n,y]
proof
let n be Element of NAT;
per cases;
suppose
A7: n <> pr1(H).(k+1);
reconsider y = G.n as Element of Funcs(NAT,bool REAL) by FUNCT_2:8;
take y;
thus thesis by A7;
end;
suppose
A8: n = pr1(H).(k+1);
take y;
thus thesis by A8,FUNCOP_1:7;
end;
end;
consider G1 being sequence of Funcs(NAT,bool REAL) such that
A9: for n being Element of NAT holds QQ1[n,G1.n] from FUNCT_2:sch 3(
A6);
A10: for n being Element of NAT holds G1.n is Interval_Covering of D.n
proof
let n be Element of NAT;
consider f0 being Function such that
A11: G1.n = f0 and
A12: dom f0 = NAT & rng f0 c= bool REAL by FUNCT_2:def 2;
reconsider f0 as sequence of bool REAL by A12,FUNCT_2:2;
A13: for s being Element of NAT holds f0.s is Interval
proof
let s be Element of NAT;
per cases;
suppose
n <> pr1(H).(k+1);
then f0.s = (G.n).s by A9,A11;
hence thesis;
end;
suppose
n = pr1(H).(k+1);
hence thesis by A9,A11;
end;
end;
D.n = {} by FUNCOP_1:7;
then D.n c= union(rng f0);
then reconsider f0 as Interval_Covering of D.n by A13,Def2;
G1.n = f0 by A11;
hence thesis;
end;
defpred SSS[Element of N0,Element of NAT] means $2 = pr2(H).$1;
defpred QQ0[Element of NAT,Function] means (($1 = pr1(H).(k+1) implies for
m being Element of NAT holds $2.m = (G.$1).m) & ($1 <> pr1(H).(k+1) implies for
m being Element of NAT holds $2.m = {}));
A14: for n being Element of NAT holds ex y being Element of Funcs(NAT,bool
REAL) st QQ0[n,y]
proof
let n be Element of NAT;
per cases;
suppose
A15: n = pr1(H).(k+1);
reconsider y = G.n as Element of Funcs(NAT,bool REAL) by FUNCT_2:8;
take y;
thus thesis by A15;
end;
suppose
A16: n <> pr1(H).(k+1);
take y;
thus thesis by A16,FUNCOP_1:7;
end;
end;
consider G0 being sequence of Funcs(NAT,bool REAL) such that
A17: for n being Element of NAT holds QQ0[n,G0.n] from FUNCT_2:sch 3(
A14);
for n being Element of NAT holds G0.n is Interval_Covering of D.n
proof
let n be Element of NAT;
consider f0 being Function such that
A18: G0.n = f0 and
A19: dom f0 = NAT & rng f0 c= bool REAL by FUNCT_2:def 2;
reconsider f0 as sequence of bool REAL by A19,FUNCT_2:2;
A20: for s being Element of NAT holds f0.s is Interval
proof
let s be Element of NAT;
per cases;
suppose
n = pr1(H).(k+1);
then f0.s = (G.n).s by A17,A18;
hence thesis;
end;
suppose
n <> pr1(H).(k+1);
hence thesis by A17,A18;
end;
end;
D.n = {} by FUNCOP_1:7;
then D.n c= union(rng f0);
then reconsider f0 as Interval_Covering of D.n by A20,Def2;
G0.n = f0 by A18;
hence thesis;
end;
then reconsider G0 as Interval_Covering of D by Def3;
set GG0 = On(G0,H);
reconsider G1 as Interval_Covering of D by A10,Def3;
set GG1 = On(G1,H);
A21: (Ser(GG0 vol)).(k+1) <= SUM(GG0 vol) by Th6,Th12;
GG1.(k+1) = (G1.(pr1(H).(k+1))).(pr2(H).(k+1)) by A2,Def11
.= {} by A9;
then
A22: (GG1 vol).(k+1) = 0. by Def4,MEASURE5:10;
(Ser (GG1 vol)).(k+1) = (Ser (GG1 vol)).k + (GG1 vol).(k+1) by SUPINF_2:
def 11;
then
A23: (Ser (GG1 vol)).(k+1) = (Ser (GG1 vol)).k by A22,XXREAL_3:4;
for s being Element of NAT holds 0. <= (vol(G1)).s by Th13;
then vol(G1) is nonnegative by SUPINF_2:39;
then
A24: (Ser vol(G1)).m0 <= (Ser vol(G1)).m by SUPINF_2:41;
A25: for n being Element of NAT holds ((On(G,H)) vol).n = (GG0 vol).n + (
GG1 vol). n
proof
let n be Element of NAT;
A26: (GG0 vol).n = diameter(GG0.n) & (GG1 vol).n = diameter(GG1.n) by Def4;
((On(G,H)) vol).n = diameter((On(G,H)).n) by Def4;
then
A27: ((On(G,H)) vol).n = diameter((G.(pr1(H).n)).(pr2(H).n)) by A2,Def11;
per cases;
suppose
A28: pr1(H).n = pr1(H).(k+1);
A29: GG1.n = (G1.(pr1(H).n)).(pr2(H).n) by A2,Def11
.= {} by A9,A28;
GG0.n = (G0.(pr1(H).n)).(pr2(H).n) by A2,Def11
.= (G.(pr1(H).n)).(pr2(H).n) by A17,A28;
hence thesis by A26,A27,A29,MEASURE5:10,XXREAL_3:4;
end;
suppose
A30: pr1(H).n <> pr1(H).(k+1);
A31: GG0.n = (G0.(pr1(H).n)).(pr2(H).n) by A2,Def11
.= {} by A17,A30;
GG1.n = (G1.(pr1(H).n)).(pr2(H).n) by A2,Def11
.= (G.(pr1(H).n)).(pr2(H).n) by A9,A30;
hence thesis by A26,A27,A31,MEASURE5:10,XXREAL_3:4;
end;
end;
GG0 vol is nonnegative & GG1 vol is nonnegative by Th12;
then
A32: (Ser (On(G,H) vol)).(k+1) = (Ser (GG0 vol)).(k+1) + (Ser (GG1 vol)).
(k+1) by A25,Th3;
for s being Element of NAT holds 0. <= (vol(G1)).s by Th13;
then
A33: vol(G1) is nonnegative by SUPINF_2:39;
(Ser(GG1 vol)).k <= (Ser vol(G1)).m0 by A5;
then
A34: (Ser (GG1 vol)).(k+1) <= (Ser vol(G1)).m by A23,A24,XXREAL_0:2;
A35: for s being Element of N0 holds ex y being Element of NAT st SSS[s,y];
consider SOS being Function of N0,NAT such that
A36: for s being Element of N0 holds SSS[s,SOS.s] from FUNCT_2:sch 3(
A35);
A37: for n being Element of NAT holds (vol(G)).n = (vol(G0)).n + (vol(G1)) .n
proof
let n be Element of NAT;
A38: vol(G.n) = vol(G0.n) + vol(G1.n)
proof
per cases;
suppose
A39: n = pr1(H).(k+1);
for s being Element of NAT holds ((G.n) vol).s <= ((G0.n) vol). s
proof
let s be Element of NAT;
((G0.n) vol).s = diameter((G0.n).s) by Def4
.= diameter((G.n).s) by A17,A39
.= ((G.n) vol).s by Def4;
hence thesis;
end;
then
A40: SUM((G.n) vol) <= SUM((G0.n) vol) by SUPINF_2:43;
for s being Element of NAT holds ((G1.n) vol).s = 0.
proof
let s be Element of NAT;
diameter((G1.n).s) = 0. by A9,A39,MEASURE5:10;
hence thesis by Def4;
end;
then
A41: SUM((G1.n) vol) = 0. by Th1;
for s being Element of NAT holds ((G0.n) vol).s <= ((G.n) vol). s
proof
let s be Element of NAT;
((G0.n) vol).s = diameter((G0.n).s) by Def4
.= diameter((G.n).s) by A17,A39
.= ((G.n) vol).s by Def4;
hence thesis;
end;
then SUM((G0.n) vol) <= SUM((G.n) vol) by SUPINF_2:43;
then SUM((G.n) vol) = SUM((G0.n) vol) by A40,XXREAL_0:1;
hence thesis by A41,XXREAL_3:4;
end;
suppose
A42: n <> pr1(H).(k+1);
A43: for s being Element of NAT holds ((G1.n) vol).s = ((G.n) vol).s
proof
let s be Element of NAT;
((G1.n) vol).s = diameter((G1.n).s) & ((G.n) vol).s =
diameter((G.n).s) by Def4;
hence thesis by A9,A42;
end;
then
for s being Element of NAT holds ((G.n) vol).s <= ((G1.n) vol). s;
then
A44: SUM((G.n) vol) <= SUM((G1.n) vol) by SUPINF_2:43;
for s being Element of NAT holds ((G0.n) vol).s = 0.
proof
let s be Element of NAT;
diameter((G0.n).s) = 0. by A17,A42,MEASURE5:10;
hence thesis by Def4;
end;
then
A45: SUM((G0.n) vol) = 0. by Th1;
for s being Element of NAT holds ((G1.n) vol).s <= ((G.n) vol).
s by A43;
then SUM((G1.n) vol) <= SUM((G.n) vol) by SUPINF_2:43;
then SUM((G.n) vol) = SUM((G1.n) vol) by A44,XXREAL_0:1;
hence thesis by A45,XXREAL_3:4;
end;
end;
(vol(G)).n = vol(G.n) & (vol(G0)).n = vol(G0.n) by Def7;
hence thesis by A38,Def7;
end;
for s being Element of NAT holds 0. <= (vol(G0)).s by Th13;
then vol(G0) is nonnegative by SUPINF_2:39;
then
A46: (vol(G0)).(pr1(H).(k+1)) <= (Ser(vol(G0))).(pr1(H).(k+1 )) & (Ser
vol(G0)).( pr1(H).(k+1)) <= (Ser vol(G0)).m by Th2,SUPINF_2:41;
A47: for s being Element of NAT holds (s in N0 implies (GG0 vol).s = ((G0.
(pr1(H).(k+1)) vol)*SOS).s) & (not s in N0 implies (GG0 vol).s = 0.)
proof
let s be Element of NAT;
thus s in N0 implies (GG0 vol).s = ((G0.(pr1(H).(k+1)) vol)*SOS).s
proof
assume
A48: s in N0;
then
A49: ex s1 being Element of NAT st s1 = s & pr1(H).(k+1) = pr1(H).s1;
A50: pr2(H).s =SOS.s by A36,A48;
(GG0 vol).s = diameter(GG0.s) by Def4
.= diameter((G0.(pr1(H).(k+1))).(pr2(H).s)) by A2,A49,Def11
.= (G0.(pr1(H).(k+1)) vol).(SOS.s) by A50,Def4
.= ((G0.(pr1(H).(k+1)) vol)*SOS).s by A48,FUNCT_2:15;
hence thesis;
end;
assume not s in N0;
then
A51: not pr1(H).(k+1) = pr1(H).s;
(GG0 vol).s = diameter(GG0.s) by Def4
.= diameter((G0.(pr1(H).s)).(pr2(H).s)) by A2,Def11
.= 0. by A17,A51,MEASURE5:10;
hence thesis;
end;
for s1,s2 being object st s1 in N0 & s2 in N0 & SOS.s1 = SOS.s2
holds s1 = s2
proof
let s1,s2 be object;
assume that
A52: s1 in N0 & s2 in N0 and
A53: SOS.s1 = SOS.s2;
reconsider s1,s2 as Element of NAT by A52;
A54: (ex s11 being Element of NAT st s11 = s1 & pr1(H).(k+1) = pr1(H).
s11 )& ex s22 being Element of NAT st s22 = s2 & pr1(H).(k+1) = pr1(H).s22 by
A52;
A55: H.s1 = [pr1(H).s1,pr2(H).s1] & H.s2 = [pr1(H).s2,pr2(H).s2] by
FUNCT_2:119;
SOS.s1 = pr2(H).s1 & SOS.s2 = pr2(H).s2 by A36,A52;
hence thesis by A1,A53,A54,A55,FUNCT_2:19;
end;
then
A56: SOS is one-to-one by FUNCT_2:19;
G0.(pr1(H).(k+1)) vol is nonnegative by Th12;
then SUM(GG0 vol) <= SUM(G0.(pr1(H).(k+1)) vol) by A56,A47,Th11;
then
A57: (Ser(GG0 vol)).(k+1) <= SUM(G0.(pr1(H).(k+1)) vol) by A21,XXREAL_0:2;
SUM(G0.(pr1(H).(k+1)) vol) = vol(G0.(pr1(H).(k+1)))
.= (vol(G0)).(pr1(H).(k+1)) by Def7;
then SUM(G0.(pr1(H).(k+1)) vol) <= (Ser vol(G0)).m by A46,XXREAL_0:2;
then
A58: (Ser (GG0 vol)).(k+1) <= (Ser vol(G0)).m by A57,XXREAL_0:2;
for s being Element of NAT holds 0. <= (vol(G0)).s by Th13;
then vol(G0) is nonnegative by SUPINF_2:39;
then (Ser vol(G)).m = (Ser vol(G0)).m + (Ser vol(G1)).m by A37,A33,Th3;
hence thesis by A58,A34,A32,XXREAL_3:36;
end;
A59: P[0]
proof
take m = pr1(H).0;
let F be sequence of bool REAL;
let G be Interval_Covering of F;
reconsider GG = On(G,H) as Interval_Covering of union rng F;
(GG vol).0 = diameter(GG.0) & ((G.(pr1(H).0)) vol).(pr2(H).0) =
diameter((G. (pr1(H).0)).(pr2(H).0)) by Def4;
then (GG vol).0 <= ((G.(pr1(H).0)) vol).(pr2(H).0) by A2,Def11;
then (GG vol).0 <= vol(G.(pr1(H).0)) by Th12,MEASURE6:3;
then
A60: Ser(GG vol).0 = (GG vol).0 & (GG vol).0 <= (vol(G)).(pr1(H).0) by Def7,
SUPINF_2:def 11;
for n being Element of NAT holds 0. <= (vol(G)).n by Th13;
then vol(G) is nonnegative by SUPINF_2:39;
then (vol(G)).m <= Ser(vol(G)).m by Th2;
hence thesis by A60,XXREAL_0:2;
end;
thus for k being Nat holds P[k] from NAT_1:sch 2(A59,A3);
end;
theorem Th15:
for F being sequence of bool REAL holds for G being
Interval_Covering of F holds inf Svc(union rng F) <= SUM(vol(G))
proof
let F be sequence of bool REAL;
let G be Interval_Covering of F;
consider H being sequence of [:NAT,NAT:] such that
A1: H is one-to-one and
dom H = NAT and
A2: rng H = [:NAT,NAT:] by MEASURE6:1;
set GG = On(G,H);
A3: for x being ExtReal st x in rng Ser(GG vol) ex y being ExtReal
st y in rng Ser(vol(G)) & x <= y
proof
let x be ExtReal;
assume x in rng Ser(GG vol);
then consider n being object such that
A4: n in dom Ser(GG vol) and
A5: x = Ser(GG vol).n by FUNCT_1:def 3;
reconsider n as Element of NAT by A4;
consider m being Element of NAT such that
A6: for F being sequence of bool REAL holds for G be
Interval_Covering of F holds Ser((On(G,H)) vol).n <= Ser(vol(G)).m by A1,A2
,Th14;
take Ser(vol(G)).m;
dom Ser(vol(G)) = NAT by FUNCT_2:def 1;
hence thesis by A5,A6,FUNCT_1:def 3;
end;
set Q = vol(GG);
Q in Svc(union rng F) by Def8;
then
A7: inf Svc(union rng F) <= Q by XXREAL_2:3;
vol(GG) <= SUM(vol(G)) by A3,XXREAL_2:63;
hence thesis by A7,XXREAL_0:2;
end;
theorem Th16:
OS_Meas is C_Measure of REAL
proof
set G = D;
{} c= union(rng G) & for n being Element of NAT holds G.n is Interval
by FUNCOP_1:7;
then reconsider G as Interval_Covering of {}REAL by Def2;
A1: for A being Subset of REAL holds for F being Interval_Covering of A
holds F vol is nonnegative
proof
let A be Subset of REAL;
let F be Interval_Covering of A;
for n being Element of NAT holds 0. <= (F vol).n
proof
let n be Element of NAT;
(F vol).n = diameter(F.n) by Def4;
hence thesis by MEASURE5:13;
end;
hence thesis by SUPINF_2:39;
end;
A2: for A being Subset of REAL holds 0.<= OS_Meas.A
proof
let A be Subset of REAL;
A3: 0. is LowerBound of Svc(A)
proof
let x be ExtReal;
assume x in Svc(A);
then consider F being Interval_Covering of A such that
A4: x = vol(F) by Def8;
set y = Ser(F vol).0;
F vol is nonnegative by A1;
then
A5: 0. <= y by SUPINF_2:40;
SUM(F vol) = sup(rng Ser(F vol)) & y <= sup(rng Ser(F vol)) by FUNCT_2:4
,XXREAL_2:4;
hence thesis by A4,A5,XXREAL_0:2;
end;
OS_Meas.A = inf(Svc(A)) by Def10;
hence thesis by A3,XXREAL_2:def 4;
end;
hence OS_Meas is nonnegative by MEASURE1:def 2;
A6: for r being Element of NAT holds 0 <= r implies (G vol).r = 0.
proof
let n be Element of NAT;
diameter(G.n) = diameter({}) by FUNCOP_1:7;
hence thesis by Def4,MEASURE5:10;
end;
then vol(G) = Ser(G vol).0 by A1,SUPINF_2:48
.= (G vol).0 by SUPINF_2:def 11
.= 0. by A6;
then
A7: 0. in Svc({}REAL) by Def8;
0. is LowerBound of Svc {}REAL
proof
let x be ExtReal;
assume x in Svc({}REAL);
then
A8: inf Svc({}REAL) <= x by XXREAL_2:3;
0. <= OS_Meas.{}REAL by A2;
then 0. <= inf Svc({}REAL) by Def10;
hence thesis by A8,XXREAL_0:2;
end;
then inf Svc {}REAL = 0. by A7,XXREAL_2:56;
hence OS_Meas.{} = 0 by Def10;
let A,B be Subset of REAL;
assume
A9: A c= B;
A10: Svc(B) c= Svc(A)
proof
let x be object;
assume
A11: x in Svc(B);
then reconsider x as R_eal;
consider F being Interval_Covering of B such that
A12: x = vol(F) by A11,Def8;
B c= union(rng F) by Def2;
then
( for n being Element of NAT holds F.n is Interval)& A c= union(rng F
) by A9;
then reconsider G = F as Interval_Covering of A by Def2;
for n being Element of NAT holds (F vol).n <= (G vol).n
proof
let n be Element of NAT;
(G vol).n = diameter(G.n) by Def4
.= (F vol).n by Def4;
hence thesis;
end;
then
A13: SUM(F vol) <= SUM(G vol) by SUPINF_2:43;
for n being Element of NAT holds (G vol).n <= (F vol).n
proof
let n be Element of NAT;
(G vol).n = diameter(G.n) by Def4
.= (F vol).n by Def4;
hence thesis;
end;
then SUM(G vol) <= SUM(F vol) by SUPINF_2:43;
then x = vol(G) by A12,A13,XXREAL_0:1;
hence thesis by Def8;
end;
OS_Meas.A = inf Svc(A) & OS_Meas.B = inf Svc(B) by Def10;
hence OS_Meas.A <= OS_Meas.B by A10,XXREAL_2:60;
let F be sequence of bool REAL;
per cases;
suppose
A14: for n being Element of NAT holds Svc(F.n) <> {+infty};
A16: for n being Element of NAT holds 0. <= (OS_Meas*F).n
proof
let n be Element of NAT;
(OS_Meas*F).n = OS_Meas.(F.n) by FUNCT_2:15;
hence thesis by A2;
end;
then
A17: OS_Meas*F is nonnegative by SUPINF_2:39;
inf Svc(union rng F) <= sup(rng Ser(OS_Meas*F))
proof
set y = inf Svc(union rng F), x = sup(rng Ser(OS_Meas*F));
assume
A18: not inf Svc(union rng F) <= sup(rng Ser(OS_Meas*F));
0. <= (OS_Meas*F).0 by A16;
then
A19: 0. <= Ser(OS_Meas*F).0 by SUPINF_2:def 11;
Ser(OS_Meas*F).0 <= x by FUNCT_2:4,XXREAL_2:4;
then 0. <= x by A19,XXREAL_0:2;
then consider eps being Real such that
A20: 0. < eps and
A21: x + eps < y by A18,XXREAL_3:49;
reconsider eps as Element of ExtREAL by XXREAL_0:def 1;
consider E being sequence of ExtREAL such that
A22: for n being Nat holds 0. < E.n and
A23: SUM(E) < eps by A20,MEASURE6:4;
A24: SUM(OS_Meas*F) + SUM(E) <= SUM(OS_Meas*F) + eps by A23,XXREAL_3:36;
defpred P[Element of NAT,set] means ex F0 being Interval_Covering of F.
$1 st ($2 = F0 & (vol(F0) < inf Svc(F.$1) + E.$1));
A25: for n being Element of NAT holds ex F0 being Element of Funcs(NAT,
bool REAL) st P[n,F0]
proof
let n be Element of NAT;
A26: OS_Meas.(F.n) = inf Svc(F.n) & In(0,REAL) is Real by Def10;
Svc(F.n) <> {+infty} by A14;
then not Svc(F.n) c= {+infty} by ZFMISC_1:33;
then Svc(F.n) \ {+infty} <> {} by XBOOLE_1:37;
then consider x being object such that
A27: x in Svc(F.n) \ {+infty} by XBOOLE_0:def 1;
reconsider x as R_eal by A27;
not x in {+infty} by A27,XBOOLE_0:def 5;
then
A28: x <> +infty by TARSKI:def 1;
x in Svc(F.n) by A27,XBOOLE_0:def 5;
then inf Svc(F.n) <= x by XXREAL_2:3;
then inf Svc(F.n) < +infty by A28,XXREAL_0:2,4;
then inf Svc(F.n) is Element of REAL by A2,A26,XXREAL_0:46;
then consider S being ExtReal such that
A29: S in Svc(F.n) and
A30: S < inf Svc(F.n) + E.n by A22,MEASURE6:5;
consider FS being Interval_Covering of F.n such that
A31: S = vol(FS) by A29,Def8;
reconsider FS as Element of Funcs(NAT,bool REAL) by FUNCT_2:8;
take FS;
thus thesis by A30,A31;
end;
consider FF being sequence of Funcs(NAT,bool REAL) such that
A32: for n being Element of NAT holds P[n,FF.n] from FUNCT_2:sch 3(
A25);
for n being Element of NAT holds FF.n is Interval_Covering of F.n
proof
let n be Element of NAT;
ex F0 being Interval_Covering of F.n st F0 = FF.n & vol( F0) < inf
Svc(F.n) + E.n by A32;
hence thesis;
end;
then reconsider FF as Interval_Covering of F by Def3;
A33: y <= SUM vol(FF) by Th15;
defpred P1[Element of NAT,Element of ExtREAL] means $2 = (OS_Meas*F).$1
+ E.$1;
A34: for n being Element of NAT holds ex y being Element of ExtREAL st
P1[n,y];
consider G0 being sequence of ExtREAL such that
A35: for n being Element of NAT holds P1[n,G0.n] from FUNCT_2:sch 3(
A34);
for n being Element of NAT holds (vol(FF)).n <= G0.n
proof
let n be Element of NAT;
(ex F0 being Interval_Covering of F.n st F0 = FF.n & vol( F0) <
inf Svc(F.n) + E.n )& (OS_Meas*F).n = OS_Meas.(F.n) by A32,FUNCT_2:15;
then vol(FF.n) < (OS_Meas*F).n + E.n by Def10;
then (vol(FF)).n < (OS_Meas*F).n + E.n by Def7;
hence thesis by A35;
end;
then
A36: SUM(vol(FF)) <= SUM(G0) by SUPINF_2:43;
for n being Element of NAT holds 0. <= E.n by A22;
then E is nonnegative by SUPINF_2:39;
then SUM(G0) <= SUM(OS_Meas*F) + SUM(E) by A17,A35,Th4;
then SUM(G0) <= SUM(OS_Meas*F) + eps by A24,XXREAL_0:2;
then SUM (vol(FF)) <= SUM (OS_Meas*F) + eps by A36,XXREAL_0:2;
hence thesis by A21,A33,XXREAL_0:2;
end;
hence thesis by Def10;
end;
suppose
ex n being Element of NAT st Svc(F.n) = {+infty};
then consider n being Element of NAT such that
A37: Svc(F.n) = {+infty};
for n being Element of NAT holds 0. <= (OS_Meas*F).n
proof
let n be Element of NAT;
(OS_Meas*F).n = OS_Meas.(F.n) by FUNCT_2:15;
hence thesis by A2;
end;
then
A38: OS_Meas*F is nonnegative by SUPINF_2:39;
inf {+infty} = +infty by XXREAL_2:13;
then OS_Meas.(F.n) = +infty by A37,Def10;
then (OS_Meas*F).n = +infty by FUNCT_2:15;
then SUM(OS_Meas*F) = +infty by A38,SUPINF_2:45;
hence thesis by XXREAL_0:4;
end;
end;
definition
redefine func OS_Meas -> C_Measure of REAL; :: redefines OS_Meas (MEASURE7, definition)
correctness by Th16;
end;
definition
func Lmi_sigmaFIELD -> SigmaField of REAL equals
sigma_Field(OS_Meas);
coherence;
end;
definition
func L_mi -> sigma_Measure of Lmi_sigmaFIELD equals
sigma_Meas(OS_Meas);
correctness;
end;