:: Lebesgue Integral of Simple Valued Function
:: by Yasunari Shidama and Noboru Endou
::
:: Received September 25, 2004
:: Copyright (c) 2004-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, NAT_1, FUNCT_1, ZFMISC_1, FINSEQ_1, RELAT_1, CARD_3,
ARYTM_3, SUBSET_1, XXREAL_0, TARSKI, XBOOLE_0, FINSEQ_2, ARYTM_1,
PARTFUN1, BINOP_2, ORDINAL4, CARD_1, FUNCOP_1, PROB_1, MESFUNC2, FUNCT_3,
SUPINF_2, PROB_2, MEASURE1, XXREAL_2, ORDINAL2, SUPINF_1, XREAL_0,
MESFUNC1, VALUED_0, COMPLEX1, SETFAM_1, FINSET_1, FINSOP_1, INTEGRA1,
REAL_1, MESFUNC3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS,
RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, XREAL_0, FINSEQ_1,
SETFAM_1, FUNCOP_1, FINSOP_1, FUNCT_3, FINSET_1, PROB_1, PROB_2,
XXREAL_0, XXREAL_2, XXREAL_3, NAT_1, REAL_1, XCMPLX_0, SUPINF_1,
SUPINF_2, MEASURE1, FINSEQOP, FINSEQ_2, BINOP_1, BINOP_2, RVSUM_1,
EXTREAL1, MESFUNC1, MESFUNC2;
constructors PARTFUN1, BINOP_1, SETWISEO, REAL_1, NAT_1, FINSEQOP, PROB_2,
FINSOP_1, RVSUM_1, MEASURE3, MEASURE6, EXTREAL1, MESFUNC1, BINARITH,
MESFUNC2, BINOP_2, SUPINF_1, RELSET_1, NUMBERS;
registrations SUBSET_1, RELAT_1, ORDINAL1, FUNCT_2, NUMBERS, XXREAL_0,
XREAL_0, NAT_1, MEMBERED, FINSEQ_1, MEASURE1, FINSET_1, VALUED_0, CARD_1,
CARD_3, XXREAL_3, RELSET_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0, BINOP_1, SUPINF_2;
expansions TARSKI, XBOOLE_0;
theorems MEASURE1, TARSKI, FUNCT_1, FUNCT_2, NAT_1, SUPINF_2, EXTREAL1,
ZFMISC_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FUNCOP_1, FINSEQ_4, PROB_2,
FUNCT_3, XBOOLE_0, XBOOLE_1, RELAT_1, RVSUM_1, MESFUNC2, MEASURE2,
CARD_2, XREAL_1, XXREAL_0, ORDINAL1, NUMBERS, VALUED_1, XXREAL_2,
VALUED_0, XXREAL_3, XREAL_0;
schemes FINSEQ_1, FINSEQ_2, NAT_1, PARTFUN1, BINOP_1;
begin :: Integral of Simple Valued Function
theorem Th1:
for n,m be Nat, a be Function of [:Seg n,Seg m:],REAL for p,q
be FinSequence of REAL st ( dom p=Seg n & for i be Nat st i in dom p holds ex r
be FinSequence of REAL st (dom r = Seg m & p.i = Sum r & for j be Nat st j in
dom r holds r.j=a.[i,j])) & ( dom q=Seg m & for j be Nat st j in dom q holds ex
s be FinSequence of REAL st (dom s = Seg n & q.j = Sum s & for i be Nat st i in
dom s holds s.i=a.[i,j])) holds Sum p = Sum q
proof
defpred P[Nat] means for m be Nat, a be Function of [: Seg $1, Seg m :],REAL
for p,q be FinSequence of REAL st (dom p=Seg $1 & for i be Nat st i in dom p
holds ex r be FinSequence of REAL st (dom(r) = Seg m & p.i=Sum(r) & for j be
Nat st j in dom(r) holds r.j=a.[i,j] )) & ( dom q=Seg m & for j be Nat st j in
dom q holds ex s be FinSequence of REAL st (dom(s) = Seg $1 & q.j=Sum(s) & for
i be Nat st i in dom(s) holds s.i=a.[i,j])) holds Sum(p)=Sum(q);
A1: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat such that
A2: P[n];
reconsider n as Element of NAT by ORDINAL1:def 12;
now
let m be Nat, a be Function of [:Seg (n+1),Seg m :],REAL;
let p,q be FinSequence of REAL such that
A3: dom p=Seg (n+1) and
A4: for i be Nat st i in dom p holds ex r be FinSequence of REAL st
( dom(r) = Seg m & p.i=Sum(r) & for j be Nat st j in dom(r) holds r.j=a.[i,j])
and
A5: dom q=Seg m and
A6: for j be Nat st j in dom q holds ex s be FinSequence of REAL st
( dom s = Seg (n+1) & q.j=Sum s & for i be Nat st i in dom s holds s.i=a.[i,j]
);
set a0=a| [:Seg n, Seg m :];
n <= n+1 by NAT_1:11;
then Seg n c= Seg (n+1) by FINSEQ_1:5;
then [:Seg n,Seg m:] c= [:Seg (n+1),Seg m:] by ZFMISC_1:95;
then reconsider a0 as Function of [:Seg n,Seg m :],REAL by FUNCT_2:32;
deffunc F(Nat)=a.[n+1,$1];
reconsider p0= p | (Seg n) as FinSequence of REAL by FINSEQ_1:18;
n+1 in NAT by ORDINAL1:def 12;
then len p=n+1 by A3,FINSEQ_1:def 3;
then
A7: n <= len p by NAT_1:11;
then
A8: dom p0=Seg n by FINSEQ_1:17;
A9: dom p0=Seg n by A7,FINSEQ_1:17;
A10: now
let i be Nat such that
A11: i in dom p0;
consider r be FinSequence of REAL such that
A12: dom(r) = Seg m and
A13: p.i=Sum(r) and
A14: for j be Nat st j in dom(r) holds r.j=a.[i,j] by A3,A4,A9,A11,
FINSEQ_2:8;
take r;
thus dom(r) = Seg m by A12;
thus p0.i = Sum(r) by A11,A13,FUNCT_1:47;
thus for j be Nat st j in dom(r) holds r.j=a0.[i,j]
proof
n <= n+1 by NAT_1:11;
then
A15: Seg n c= Seg (n+1) by FINSEQ_1:5;
dom a= [:Seg (n+1),Seg m:] by FUNCT_2:def 1;
then
A16: dom a0 = [:Seg (n+1),Seg m:] /\ [:Seg n,Seg m:] by RELAT_1:61
.= [:Seg n,Seg m:] by A15,ZFMISC_1:101;
let j be Nat such that
A17: j in dom(r);
A18: [i,j] in [:Seg n,Seg m:] by A9,A11,A12,A17,ZFMISC_1:87;
thus r.j=a.[i,j] by A14,A17
.=a0.[i,j] by A18,A16,FUNCT_1:47;
end;
end;
reconsider m as Element of NAT by ORDINAL1:def 12;
consider an be FinSequence such that
A19: len an=m & for j be Nat st j in dom an holds an.j=F(j) from
FINSEQ_1:sch 2;
A20: now
let i be Nat;
assume i in dom an;
then an.i = a.[n+1,i] by A19;
hence an.i in REAL by XREAL_0:def 1;
end;
A21: dom an = Seg m by A19,FINSEQ_1:def 3;
reconsider an as FinSequence of REAL by A20,FINSEQ_2:12;
A22: an is Element of m-tuples_on REAL by A19,FINSEQ_2:92;
A23: dom an=Seg m by A19,FINSEQ_1:def 3;
A24: Sum(an) = p.(n+1)
proof
consider r be FinSequence of REAL such that
A25: dom(r) = Seg m and
A26: p.(n+1)=Sum(r) and
A27: for j be Nat st j in dom(r) holds r.j=a.[n+1,j] by A3,A4,FINSEQ_1:4;
now
let j be Nat;
assume
A28: j in dom r;
hence r.j=a.[n+1,j] by A27
.=an.j by A19,A21,A25,A28;
end;
hence thesis by A23,A25,A26,FINSEQ_1:13;
end;
reconsider q0=q-an as FinSequence of REAL;
A29: rng <:q,an:> c= [:rng q, rng an:] by FUNCT_3:51;
dom diffreal = [:REAL,REAL:] by FUNCT_2:def 1;
then
A30: [:rng q, rng an:] c= dom diffreal by ZFMISC_1:96;
dom (diffreal.:(q,an)) = dom(diffreal*<:q,an:>) by FUNCOP_1:def 3
.= dom <:q,an:> by A30,A29,RELAT_1:27,XBOOLE_1:1
.= dom q /\ dom an by FUNCT_3:def 7;
then
A31: dom q0= dom q /\ dom an by RVSUM_1:def 6
.= Seg m /\ Seg m by A5,A19,FINSEQ_1:def 3
.= Seg m;
then len q0=m by FINSEQ_1:def 3;
then
A32: q0 is Element of m-tuples_on REAL by FINSEQ_2:92;
A33: now
let j be Nat such that
A34: j in dom q0;
consider s be FinSequence of REAL such that
A35: dom(s) = Seg (n+1) and
A36: q.j=Sum(s) and
A37: for i be Nat st i in dom(s) holds s.i=a.[i,j] by A5,A6,A31,A34;
s.(n+1)=a.[n+1,j] by A35,A37,FINSEQ_1:4;
then
A38: s.(n+1)=an.j by A19,A21,A31,A34;
reconsider sn=s|Seg (n) as FinSequence of REAL by FINSEQ_1:18;
take sn;
n+1 in NAT by ORDINAL1:def 12;
then
A39: len s = n+1 by A35,FINSEQ_1:def 3;
then n <= len s by NAT_1:11;
hence
A40: dom sn =Seg n by FINSEQ_1:17;
sn^<*(s.(n+1))*> = s by A39,FINSEQ_3:55;
then q.j-an.j=Sum(sn) +an.j-an.j by A36,A38,RVSUM_1:74
.=Sum(sn);
hence q0.j = Sum(sn) by A34,VALUED_1:13;
thus for i be Nat st i in dom(sn) holds sn.i=a0.[i,j]
proof
n <= n+1 by NAT_1:11;
then
A41: Seg n c= Seg (n+1) by FINSEQ_1:5;
dom a= [:Seg (n+1),Seg m:] by FUNCT_2:def 1;
then
A42: dom a0 = [:Seg (n+1),Seg m:] /\ [:Seg n,Seg m:] by RELAT_1:61
.= [:Seg n,Seg m:] by A41,ZFMISC_1:101;
let i be Nat such that
A43: i in dom(sn);
A44: [i,j] in [:Seg n,Seg m:] by A31,A34,A40,A43,ZFMISC_1:87;
thus sn.i=s.i by A43,FUNCT_1:47
.=a.[i,j] by A35,A37,A40,A43,A41
.=a0.[i,j] by A44,A42,FUNCT_1:47;
end;
end;
len q=m by A5,FINSEQ_1:def 3;
then q is Element of m-tuples_on REAL by FINSEQ_2:92;
then
A45: q0+an=q by A22,RVSUM_1:43;
n+1 in NAT by ORDINAL1:def 12;
then
len p=n+1 by A3,FINSEQ_1:def 3;
then p0^<*Sum(an)*> = p by A24,FINSEQ_3:55;
hence Sum(p) = Sum(p0)+Sum(an) by RVSUM_1:74
.=Sum(q0)+Sum(an) by A2,A10,A8,A31,A33
.=Sum(q) by A32,A22,A45,RVSUM_1:89;
end;
hence thesis;
end;
now
let m be Nat, a be Function of [: Seg 0, Seg m :],REAL;
let p,q be FinSequence of REAL such that
A46: dom p=Seg 0 and
for i be Nat st i in dom p holds ex r be FinSequence of REAL st (dom(r
) = Seg m & p.i=Sum(r) & for j be Nat st j in dom(r) holds r.j=a.[i,j]) and
A47: dom q=Seg m and
A48: for j be Nat st j in dom q holds ex s be FinSequence of REAL st (
dom(s) = Seg 0 & q.j=Sum(s) & for i be Nat st i in dom(s) holds s.i=a.[i,j] );
reconsider m as Element of NAT by ORDINAL1:def 12;
now
let z be object;
assume
A49: z in dom q;
then z in { k where k is Nat : 1 <= k & k <= m } by A47,FINSEQ_1:def 1;
then ex k be Nat st z=k & 1 <= k & k <= m;
then reconsider j=z as Nat;
consider s be FinSequence of REAL such that
A50: dom(s) = Seg 0 and
A51: q.j=Sum(s) and
for i be Nat st i in dom(s) holds s.i=a.[i,j] by A48,A49;
s = <*>REAL by A50;
hence q.z=0 by A51,RVSUM_1:72;
end;
then q = dom q --> 0 by FUNCOP_1:11;
then
A52: q= m |-> 0 by A47,FINSEQ_2:def 2;
p = <*>REAL by A46;
hence Sum(p)=Sum(q) by A52,RVSUM_1:72,81;
end;
then
A53: P[0];
thus for n be Nat holds P[n] from NAT_1:sch 2(A53,A1);
end;
theorem Th2:
for F be FinSequence of ExtREAL, f be FinSequence of REAL st F=f
holds Sum(F)=Sum(f)
proof
let F be FinSequence of ExtREAL;
let f be FinSequence of REAL;
defpred P[Nat] means for G be FinSequence of ExtREAL, g be FinSequence of
REAL st G=F|(Seg $1) & g = f|(Seg $1) & $1 <= len F holds Sum(G) = Sum(g);
F|(Seg len F) = F|(len F) by FINSEQ_1:def 16;
then
A1: F|(Seg len F) = F by FINSEQ_1:58;
assume
A2: F = f;
A3: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A4: P[k];
for G be FinSequence of ExtREAL, g be FinSequence of REAL st G = F|(
Seg (k+1)) & g = f|(Seg (k+1)) & k+1 <= len F holds Sum(G) = Sum(g)
proof
let G be FinSequence of ExtREAL, g be FinSequence of REAL;
assume that
A5: G = F|(Seg (k+1)) and
A6: g = f|(Seg (k+1)) and
A7: k+1 <= len F;
reconsider gk= g.(k+1) as Element of REAL by XREAL_0:def 1;
reconsider g2=<*gk*> as FinSequence of REAL;
reconsider G1 = G|(Seg k) as FinSequence of ExtREAL by FINSEQ_1:18;
A8: not -infty in rng G1 & not -infty in rng <*G.(k+1)*> by A2,A5;
reconsider g1 = g|(Seg k) as FinSequence of REAL by FINSEQ_1:18;
len g = k+1 by A2,A6,A7,FINSEQ_1:17;
then g = g1^<*g.(k+1)*> by FINSEQ_3:55;
then
A10: Sum g = Sum g1 + g.(k+1) by RVSUM_1:74;
A11: k <= k+1 by NAT_1:11;
len G = k+1 by A5,A7,FINSEQ_1:17;
then G = G1^<*G.(k+1)*> by FINSEQ_3:55;
then
A12: Sum G = Sum G1 + Sum (<*G.(k+1)*>) by A8,EXTREAL1:10
.= Sum G1 + G.(k+1) by EXTREAL1:8;
k <= k+1 by NAT_1:11;
then Seg k c= Seg (k+1) by FINSEQ_1:5;
then G1 = F|(Seg k) & g1 = f|(Seg k) by A5,A6,FUNCT_1:51;
then Sum G1 = Sum g1 by A4,A7,A11,XXREAL_0:2;
hence thesis by A2,A5,A6,A12,A10,SUPINF_2:1;
end;
hence thesis;
end;
A13: P[0] by EXTREAL1:7,RVSUM_1:72;
for k be Nat holds P[k] from NAT_1:sch 2(A13,A3);
hence thesis by A2,A1;
end;
theorem Th3:
for X be non empty set, S be SigmaField of X, f be PartFunc of X,
ExtREAL st f is_simple_func_in S holds ex F be Finite_Sep_Sequence of S, a be
FinSequence of ExtREAL st dom f = union rng F & dom F= dom a & (for n be Nat st
n in dom F for x be object st x in F.n holds f.x = a.n) &
for x be object st x in dom f
ex ax be FinSequence of ExtREAL st dom ax = dom a & for n be Nat st n
in dom ax holds ax.n=a.n*(chi(F.n,X)).x
proof
let X be non empty set;
let S be SigmaField of X;
let f be PartFunc of X,ExtREAL;
assume f is_simple_func_in S;
then consider F be Finite_Sep_Sequence of S such that
A1: dom f = union rng F and
A2: for n being Nat,x,y being Element of X st n in dom F & x in F.n & y
in F.n holds f.x = f.y by MESFUNC2:def 4;
defpred P[Nat,Element of ExtREAL] means for x be set st x in F.$1 holds $2 =
f.x;
A3: for k be Nat st k in Seg len F ex y be Element of ExtREAL st P[k,y]
proof
let k be Nat;
assume k in Seg len F;
then
A4: k in dom F by FINSEQ_1:def 3;
then
A5: F.k in rng F by FUNCT_1:3;
per cases;
suppose
A6: F.k = {};
take y = 0.;
for x be set st x in F.k holds y = f.x by A6;
hence thesis;
end;
suppose
F.k <> {};
then consider x1 be object such that
A7: x1 in F.k by XBOOLE_0:def 1;
reconsider x1 as set by TARSKI:1;
take y = f.x1;
for x be set st x in F.k holds y = f.x
proof
let x be set;
A8: rng F c= bool X by XBOOLE_1:1;
then reconsider x1 as Element of X by A5,A7;
assume
A9: x in F.k;
then reconsider x as Element of X by A5,A8;
f.x = f.x1 by A2,A4,A7,A9;
hence thesis;
end;
hence thesis;
end;
end;
consider a be FinSequence of ExtREAL such that
A10: dom a = Seg len F & for k be Nat st k in Seg len F holds P[k,a.k]
from FINSEQ_1:sch 5(A3);
take F,a;
A11: for x be set st x in dom f holds ex ax be FinSequence of ExtREAL st dom
ax = dom a & for n be Nat st n in dom ax holds ax.n = a.n*(chi(F.n,X)).x
proof
let x be set;
assume x in dom f;
deffunc Q(Nat) = a.$1 * (chi(F.$1,X)).x;
consider ax be FinSequence of ExtREAL such that
A12: len ax = len F & for k be Nat st k in dom ax holds ax.k=Q(k) from
FINSEQ_2:sch 1;
take ax;
thus thesis by A10,A12,FINSEQ_1:def 3;
end;
for n be Nat st n in dom F for x be set st x in F.n holds a.n = f.x
proof
let n be Nat;
assume n in dom F;
then n in Seg len F by FINSEQ_1:def 3;
hence thesis by A10;
end;
hence thesis by A1,A10,A11,FINSEQ_1:def 3;
end;
theorem Th4:
for X be set, F be FinSequence of X holds F is disjoint_valued
iff for i,j be Nat st i in dom F & j in dom F & i <> j holds F.i misses F.j
proof
let X be set;
let F be FinSequence of X;
now
assume
A1: for i,j be Nat st i in dom F & j in dom F & i <> j holds F.i misses F.j;
for x,y be object st x <> y holds F.x misses F.y
proof
let x,y be object;
assume
A2: x <> y;
per cases;
suppose
x in dom F & y in dom F;
hence thesis by A1,A2;
end;
suppose
not x in dom F;
then F.x = {} by FUNCT_1:def 2;
hence thesis;
end;
suppose
not y in dom F;
then F.y = {} by FUNCT_1:def 2;
hence thesis;
end;
end;
hence F is disjoint_valued by PROB_2:def 2;
end;
hence thesis by PROB_2:def 2;
end;
theorem Th5:
for X be non empty set, A be set, S be SigmaField of X, F be
Finite_Sep_Sequence of S, G be FinSequence of S st dom G = dom F & for i be Nat
st i in dom G holds G.i = A /\ F.i holds G is Finite_Sep_Sequence of S
proof
let X be non empty set, A be set, S be SigmaField of X, F be
Finite_Sep_Sequence of S, G be FinSequence of S such that
A1: dom G = dom F and
A2: for i be Nat st i in dom G holds G.i= A /\ F.i;
now
let i,j be Nat;
assume that
A3: i in dom G and
A4: j in dom G and
A5: i <> j;
A6: F.i misses F.j by A1,A3,A4,A5,Th4;
(A /\ F.i) /\ (A /\ F.j) =A /\ (F.i /\ (A /\ F.j)) by XBOOLE_1:16
.=A /\ ((F.i /\ F.j) /\ A) by XBOOLE_1:16
.=A /\ ({} /\ A) by A6
.={};
then A /\ F.i misses A /\ F.j;
then G.i misses A /\ F.j by A2,A3;
hence G.i misses G.j by A2,A4;
end;
hence thesis by Th4;
end;
theorem Th6:
for X be non empty set, A be set, F,G be FinSequence of X st dom
G = dom F & (for i be Nat st i in dom G holds G.i = A /\ F.i) holds union rng G
= A /\ union rng F
proof
let X be non empty set;
let A be set;
let F,G be FinSequence of X;
assume that
A1: dom G = dom F and
A2: for i be Nat st i in dom G holds G.i = A /\ F.i;
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
A3: r in E and
A4: E in rng G by TARSKI:def 4;
consider s being object such that
A5: s in dom G and
A6: E = G.s by A4,FUNCT_1:def 3;
reconsider s as Element of NAT by A5;
A7: r in A /\ F.s by A2,A3,A5,A6;
then
A8: r in F.s by XBOOLE_0:def 4;
F.s in rng F by A1,A5,FUNCT_1:3;
then
A9: r in union rng F by A8,TARSKI:def 4;
r in A by A7,XBOOLE_0:def 4;
hence thesis by A9,XBOOLE_0:def 4;
end;
let r be object;
assume
A10: r in A /\ union rng F;
then
A11: r in A by XBOOLE_0:def 4;
r in union rng F by A10,XBOOLE_0:def 4;
then consider E being set such that
A12: r in E and
A13: E in rng F by TARSKI:def 4;
consider s being object such that
A14: s in dom F and
A15: E = F.s by A13,FUNCT_1:def 3;
reconsider s as Element of NAT by A14;
A /\ E = G.s by A1,A2,A14,A15;
then
A16: r in G.s by A11,A12,XBOOLE_0:def 4;
G.s in rng G by A1,A14,FUNCT_1:3;
hence thesis by A16,TARSKI:def 4;
end;
theorem Th7:
for X be set, F be FinSequence of X, i be Nat st i in dom F holds
F.i c= union rng F & F.i /\ union rng F = F.i
proof
let X be set, F be FinSequence of X, i be Nat;
assume
A1: i in dom F;
hence F.i c= union rng F by FUNCT_1:3,ZFMISC_1:74;
F.i in rng F by A1,FUNCT_1:3;
hence thesis by XBOOLE_1:28,ZFMISC_1:74;
end;
theorem Th8:
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, F be Finite_Sep_Sequence of S holds dom F = dom (M*F)
proof
let X be non empty set;
let S be SigmaField of X;
let M be sigma_Measure of S;
let F be Finite_Sep_Sequence of S;
dom M = S by FUNCT_2:def 1;
then rng F c= dom M;
hence thesis by RELAT_1:27;
end;
theorem Th9:
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, F be Finite_Sep_Sequence of S holds M.(union rng F) = Sum(M*F)
proof
let X be non empty set;
let S be SigmaField of X;
let M be sigma_Measure of S;
let F be Finite_Sep_Sequence of S;
reconsider F1 = M*F as FinSequence of ExtREAL;
consider f be sequence of ExtREAL such that
A1: Sum(F1) = f.(len F1) and
A2: f.0 = 0. and
A3: for i be Nat st i < len F1 holds f.(i+1) = f.i + F1.(i+1)
by EXTREAL1:def 2;
consider G being Sep_Sequence of S such that
A4: union rng F = union rng G and
A5: for n being Nat st n in dom F holds F.n = G.n and
A6: for m being Nat st not m in dom F holds G.m = {} by MESFUNC2:30;
defpred Q[Nat] means $1 <= len F1 implies Ser(M*G).$1 = f.$1;
set G1 = M*G;
A7: dom G = NAT by FUNCT_2:def 1;
A9: for i be Nat st i < len F1 holds Ser(M*G).(i+1) = Ser(M*G).i + F1.(i+1)
proof
let i be Nat;
assume i < len F1;
then 1 <= i+1 & i+1 <= len F1 by NAT_1:11,13;
then i+1 in dom F1 by FINSEQ_3:25;
then
A10: i+1 in dom F by Th8;
reconsider i as Element of NAT by ORDINAL1:def 12;
A11: i+1 in NAT by ORDINAL1:def 12;
Ser(M*G).(i+1) = Ser(M*G).i + (M*G).(i+1) by SUPINF_2:def 11
.= Ser(M*G).i + M.(G.(i+1)) by A7,FUNCT_1:13,A11
.= Ser(M*G).i + M.(F.(i+1)) by A5,A10;
hence thesis by A10,FUNCT_1:13;
end;
A12: for k be Nat st Q[k] holds Q[k+1]
proof
A13: for i be Nat st i < len F1 holds f.(i+1) = f.i + F1.(i+1)
by A3;
let k be Nat;
assume
A14: Q[k];
assume k+1 <= len F1;
then
A15: k < len F1 by NAT_1:13;
then Ser(M*G).(k+1) = f.k + F1.(k+1) by A9,A14;
hence thesis by A13,A15;
end;
defpred P[Nat] means $1 >= len F1 implies Ser(M*G).$1 = Ser(M*G).(len F1);
A16: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A17: P[k];
assume
A18: k+1 >= len F1;
reconsider k as Element of NAT by ORDINAL1:def 12;
now
per cases;
case
A19: k >= len F1;
then k+1 > len F1 by NAT_1:13;
then not k+1 in Seg len F1 by FINSEQ_1:1;
then not k+1 in dom F1 by FINSEQ_1:def 3;
then
A20: not k+1 in dom F by Th8;
k+1 in NAT by ORDINAL1:def 12;
then
A21: G1.(k+1) = M.(G.(k+1)) by A7,FUNCT_1:13
.= M.{} by A6,A20
.= 0. by VALUED_0:def 19;
Ser(M*G).(k+1) = Ser(M*G).(len F1) + G1.(k+1) by A17,A19,
SUPINF_2:def 11;
hence thesis by A21,XXREAL_3:4;
end;
case
k < len F1;
then k+1 <= len F1 by NAT_1:13;
hence thesis by A18,XXREAL_0:1;
end;
end;
hence thesis;
end;
defpred P1[Nat] means $1 < len F1 implies Ser(M*G).(len F1 - $1) <= Ser(M*G)
.(len F1);
A22: M*G is nonnegative by MEASURE2:1;
A23: for k be Nat st P1[k] holds P1[k+1]
proof
let k be Nat;
assume
A24: P1[k];
assume
A25: k+1 < len F1;
then consider k9 being Nat such that
A26: len F1 = (k+1 qua Nat) + k9 by NAT_1:10;
reconsider k9 as Element of NAT by ORDINAL1:def 12;
k <= k+1 & Ser(M*G).(k9) <= Ser(M*G).(k9 + 1) by A22,NAT_1:11,SUPINF_2:40;
hence thesis by A24,A25,A26,XXREAL_0:2;
end;
not 0 in Seg len F by FINSEQ_1:1;
then not 0 in dom F by FINSEQ_1:def 3;
then
A27: G.0 = {} by A6;
Ser(M*G).0 = G1.0 by SUPINF_2:def 11;
then
A28: Ser(M*G).0 = M.(G.0) by A7,FUNCT_1:13
.= 0. by A27,VALUED_0:def 19;
then
A29: Q[0] by A2;
A30: for k be Nat holds Q[k] from NAT_1:sch 2(A29,A12);
A31: P1[0];
A32: for i be Nat holds P1[i] from NAT_1:sch 2(A31,A23);
A33: for i be Nat st i < len F1 holds Ser(M*G).i <= Ser(M*G).(len F1)
proof
let i be Nat;
A34: len F1 <= len F1 + i by NAT_1:11;
assume i < len F1;
then consider k be Nat such that
A35: len F1 = i + k by NAT_1:10;
reconsider k as Element of NAT by ORDINAL1:def 12;
k = len F1 - i by A35;
then
A36: k <= len F1 by A34,XREAL_1:20;
Ser(M*G).(len F1 - k) <= Ser(M*G).(len F1)
proof
now
per cases by A36,XXREAL_0:1;
case
k = len F1;
hence thesis by A28,A22,SUPINF_2:40;
end;
case
k < len F1;
hence thesis by A32;
end;
end;
hence thesis;
end;
hence thesis by A35;
end;
A37: P[0];
A38: for k be Nat holds P[k] from NAT_1:sch 2(A37,A16);
for z be ExtReal st z in rng Ser(M*G) holds z <= Ser(M*G).(len F1)
proof
let z be ExtReal;
assume z in rng Ser(M*G);
then consider n be object such that
A39: n in dom Ser(M*G) and
A40: z = Ser(M*G).n by FUNCT_1:def 3;
reconsider n as Element of NAT by A39;
now
per cases;
case
n < len F1;
hence thesis by A33,A40;
end;
case
n >= len F1;
hence thesis by A38,A40;
end;
end;
hence thesis;
end;
then
A41: Ser(M*G).(len F1) is UpperBound of rng Ser(M*G) by XXREAL_2:def 1;
dom (Ser(M*G)) = NAT by FUNCT_2:def 1;
then
A42: Ser(M*G).(len F1) = sup(rng Ser(M*G)) by A41,FUNCT_1:3,XXREAL_2:55;
M.(union rng F) = SUM(M*G) by A4,MEASURE1:def 6
.= sup(rng Ser(M*G));
hence thesis by A1,A30,A42;
end;
theorem Th10:
for F,G be FinSequence of ExtREAL, a be R_eal st (a is real or (
for i be Nat st i in dom F holds F.i < 0.) or
for i be Nat st i in dom F holds 0. < F.i )
& dom F = dom G & for i be Nat st i in dom G holds G.i=a*F.i holds
Sum(G)=a*Sum(F)
proof
let F,G be FinSequence of ExtREAL;
let a be R_eal;
assume that
A1: a is real or (for i be Nat st i in dom F holds F.i < 0.) or for i be
Nat st i in dom F holds 0. < F.i and
A2: dom F = dom G and
A3: for i be Nat st i in dom G holds G.i=a*F.i;
consider g be sequence of ExtREAL such that
A4: Sum(G) = g.(len G) and
A5: g.0 = 0. and
A6: for i being Nat st i < len G holds g.(i+1)=g.i+G.(i+1) by
EXTREAL1:def 2;
consider f be sequence of ExtREAL such that
A7: Sum(F) = f.(len F) and
A8: f.0 = 0. and
A9: for i being Nat st i < len F holds f.(i+1)=f.i+F.(i+1) by
EXTREAL1:def 2;
defpred P[Nat] means $1 <= len G implies g.$1 = a*f.$1;
A10: for i be Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume
A11: P[i];
assume
A12: i+1 <= len G;
reconsider i as Element of NAT by ORDINAL1:def 12;
1 <= i+1 by NAT_1:11;
then
A13: i+1 in dom G by A12,FINSEQ_3:25;
then i+1 in Seg len F by A2,FINSEQ_1:def 3;
then i+1 <= len F by FINSEQ_1:1;
then
A14: i < len F by NAT_1:13;
i < len G by A12,NAT_1:13;
then
A15: g.(i+1) = g.i + G.(i+1) by A6
.= a*f.i + a*F.(i+1) by A3,A11,A12,A13,NAT_1:13;
now
per cases by A1;
case
a is real;
then g.(i+1) = a*(f.i + F.(i+1)) by A15,XXREAL_3:95;
hence thesis by A9,A14;
end;
case
A16: for i be Nat st i in dom F holds F.i < 0.;
defpred P1[Nat] means $1 < len F implies f.$1 <= 0.;
A17: for i be Nat st P1[i] holds P1[i+1]
proof
let i be Nat;
assume
A18: P1[i];
assume
A19: i+1 < len F;
reconsider i as Element of NAT by ORDINAL1:def 12;
1 <= i+1 by NAT_1:12;
then i+1 in dom F by A19,FINSEQ_3:25;
then
A20: F.(i+1) < 0. by A16;
i < len F by A19,NAT_1:13;
then f.(i+1) = f.i + F.(i+1) by A9;
hence thesis by A18,A19,A20,NAT_1:13;
end;
A21: P1[0] by A8;
for i be Nat holds P1[i] from NAT_1:sch 2(A21,A17);
then
A22: f.i < 0. or f.i = 0. by A14;
F.(i+1) < 0. by A2,A13,A16;
then g.(i+1) = a*(f.i + F.(i+1)) by A15,A22,XXREAL_3:97;
hence thesis by A9,A14;
end;
case
A23: for i be Nat st i in dom F holds 0. < F.i;
defpred P2[Nat] means $1 < len F implies 0. <= f.$1;
A24: for i be Nat st P2[i] holds P2[i+1]
proof
let i be Nat;
assume
A25: P2[i];
assume
A26: i+1 < len F;
reconsider i as Element of NAT by ORDINAL1:def 12;
1 <= i+1 by NAT_1:12;
then i+1 in dom F by A26,FINSEQ_3:25;
then
A27: 0. < F.(i+1) by A23;
i < len F by A26,NAT_1:13;
then f.(i+1) = f.i + F.(i+1) by A9;
hence thesis by A25,A26,A27,NAT_1:13;
end;
A28: P2[0] by A8;
for i be Nat holds P2[i] from NAT_1:sch 2(A28,A24);
then
A29: 0. < f.i or f.i = 0. by A14;
0. < F.(i+1) by A2,A13,A23;
then g.(i+1) = a*(f.i + F.(i+1)) by A15,A29,XXREAL_3:96;
hence thesis by A9,A14;
end;
end;
hence thesis;
end;
A30: P[0] by A8,A5;
A31: for i be Nat holds P[i] from NAT_1:sch 2(A30,A10);
Seg len F = dom G by A2,FINSEQ_1:def 3
.= Seg len G by FINSEQ_1:def 3;
then a*Sum(F) = a*f.(len G) by A7,FINSEQ_1:6
.= g.(len G) by A31;
hence thesis by A4;
end;
theorem Th11:
for F be FinSequence of REAL holds F is FinSequence of ExtREAL
proof
let F be FinSequence of REAL;
rng F c= ExtREAL by NUMBERS:31;
hence thesis by FINSEQ_1:def 4;
end;
definition
let X be non empty set;
let S be SigmaField of X;
let f be PartFunc of X,ExtREAL;
let F be Finite_Sep_Sequence of S;
let a be FinSequence of ExtREAL;
pred F,a are_Re-presentation_of f means
dom f = union rng F & dom F=
dom a & for n be Nat st n in dom F
for x be object st x in F.n holds f.x=a.n;
end;
theorem
for X be non empty set, S be SigmaField of X, f be PartFunc of X,
ExtREAL st f is_simple_func_in S
ex F be Finite_Sep_Sequence of S, a be
FinSequence of ExtREAL st F,a are_Re-presentation_of f
proof
let X be non empty set;
let S be SigmaField of X;
let f be PartFunc of X,ExtREAL;
assume f is_simple_func_in S;
then consider
F being Finite_Sep_Sequence of S, a be FinSequence of ExtREAL such
that
A1: dom f = union rng F & dom F= dom a & for n be Nat st n in dom F for
x be object st x in F.n holds f.x=a.n and
for x be object st x in dom f
ex ax be FinSequence of ExtREAL st dom ax= dom a &
for n be Nat st n in dom ax
holds ax.n=a.n*(chi(F.n,X)).x by Th3;
take F,a;
thus thesis by A1;
end;
theorem Th13:
for X be non empty set, S be SigmaField of X, F be
Finite_Sep_Sequence of S holds ex G be Finite_Sep_Sequence of S st union rng F
= union rng G & for n be Nat st n in dom G holds (G.n <> {} & ex m be Nat st m
in dom F & F.m = G.n)
proof
let X be non empty set;
let S be SigmaField of X;
let F be Finite_Sep_Sequence of S;
defpred P[Nat] means for F be Finite_Sep_Sequence of S st len F = $1 holds
ex G be Finite_Sep_Sequence of S st (union rng F = union rng G & (for n be Nat
st n in dom G holds (G.n <> {} & ex m be Nat st m in dom F & F.m = G.n)));
A1: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A2: P[n];
let F be Finite_Sep_Sequence of S;
assume
A3: len F = n+1;
reconsider n as Element of NAT by ORDINAL1:def 12;
reconsider F1 = F|(Seg n) as Finite_Sep_Sequence of S by MESFUNC2:33;
A4: n <= len F by A3,NAT_1:11;
then
A5: len F1 = n by FINSEQ_1:17;
then consider G1 be Finite_Sep_Sequence of S such that
A6: union rng F1 = union rng G1 and
A7: for n be Nat st n in dom G1 holds (G1.n <> {} & ex m be Nat st m
in dom F1 & F1.m = G1.n) by A2;
A8: dom F = dom (F1^<*F.(n+1)*>) & for k be Nat st k in dom F holds F.k =
(F1^<*F.(n+1)*>).k
proof
thus dom (F1^<*F.(n+1)*>) = Seg (len F1 + len <*F.(n+1)*>) by
FINSEQ_1:def 7
.= Seg (n + 1) by A5,FINSEQ_1:39
.= dom F by A3,FINSEQ_1:def 3;
let k be Nat;
assume
A9: k in dom F;
now
per cases;
case
A10: k in dom F1;
then k in Seg n by A4,FINSEQ_1:17;
then k <= n by FINSEQ_1:1;
then
A11: (F|n).k = F.k by FINSEQ_3:112;
(F1^<*F.(n+1)*>).k = F1.k by A10,FINSEQ_1:def 7;
hence thesis by A11,FINSEQ_1:def 16;
end;
case
A12: not k in dom F1;
A13: k in Seg (n+1) by A3,A9,FINSEQ_1:def 3;
not k in Seg n by A4,A12,FINSEQ_1:17;
then not (1 <= k & k <= n) by FINSEQ_1:1;
then
A14: not k < n + 1 by A13,FINSEQ_1:1,NAT_1:13;
dom <*F.(n+1)*> = Seg 1 by FINSEQ_1:def 8;
then
A15: 1 in dom <*F.(n+1)*> by FINSEQ_1:2,TARSKI:def 1;
A16: k <= n+1 by A13,FINSEQ_1:1;
then (F1^<*F.(n+1)*>).k = (F1^<*F.(n+1)*>).(len F1 + 1) by A5,A14,
XXREAL_0:1
.= <*F.(n+1)*>.1 by A15,FINSEQ_1:def 7
.= F.(n+1);
hence thesis by A14,A16,XXREAL_0:1;
end;
end;
hence thesis;
end;
then
A17: F = F1^<*F.(n+1)*> by FINSEQ_1:13;
ex G be Finite_Sep_Sequence of S st union rng F = union rng G & for k
be Nat st k in dom G holds (G.k <> {} & ex m be Nat st m in dom F & F.m = G.k)
proof
now
per cases;
case
F.(n+1) = {};
then
A18: rng <*F.(n+1)*> = {{}} by FINSEQ_1:38;
take G = G1;
A19: for k be Nat st k in dom G holds (G.k <> {} & ex m be Nat st m
in dom F & F.m = G.k)
proof
let k be Nat;
A20: dom F1 c= dom F by A8,FINSEQ_1:26;
assume
A21: k in dom G;
then consider m be Nat such that
A22: m in dom F1 and
A23: F1.m = G.k by A7;
F1.m = F.m by A17,A22,FINSEQ_1:def 7;
hence thesis by A7,A21,A22,A23,A20;
end;
rng F = rng F1 \/ rng <*F.(n+1)*> by A17,FINSEQ_1:31;
then union rng F = union rng F1 \/ union rng <*F.(n+1)*> by
ZFMISC_1:78
.= union rng F1 \/ {} by A18,ZFMISC_1:25
.= union rng G by A6;
hence thesis by A19;
end;
case
A24: F.(n+1) <> {};
A25: for k,m be object st k <> m holds (G1^<*F.(n+1)*>).k misses (G1^<*
F.(n+1)*>).m
proof
let k,m be object;
assume
A26: k <> m;
now
per cases;
case
A27: k in dom (G1^<*F.(n+1)*>) & m in dom (G1^<*F.(n+1)*>);
then reconsider k,m as Element of NAT;
now
per cases;
case
k = len (G1^<*F.(n+1)*>);
then k = len G1 + len <*F.(n+1)*> by FINSEQ_1:22;
then
A28: k = len G1 + 1 by FINSEQ_1:39;
1 <= len <*F.(n+1)*> by FINSEQ_1:39;
then
A29: (G1^<*F.(n+1)*>).k = <*F.(n+1)*>.1 by A28,FINSEQ_1:65
.= F.(n+1);
A30: m in Seg (len (G1^<*F.(n+1)*>)) by A27,FINSEQ_1:def 3;
then m in Seg (len G1 + len <*F.(n+1)*>) by FINSEQ_1:22;
then m in Seg (len G1 + 1) by FINSEQ_1:39;
then m <= len G1 + 1 by FINSEQ_1:1;
then m < len G1 + 1 by A26,A28,XXREAL_0:1;
then
A31: m <= len G1 by NAT_1:13;
1 <= m by A30,FINSEQ_1:1;
then
A32: m in dom G1 by A31,FINSEQ_3:25;
then consider m1 be Nat such that
A33: m1 in dom F1 and
A34: F1.m1 = G1.m by A7;
m1 in Seg len F1 by A33,FINSEQ_1:def 3;
then m1 <= n by A5,FINSEQ_1:1;
then
A35: m1 <> n+1 by NAT_1:13;
(G1^<*F.(n+1)*>).m = G1.m by A32,FINSEQ_1:def 7;
then (G1^<*F.(n+1)*>).m = F.m1 by A17,A33,A34,
FINSEQ_1:def 7;
hence thesis by A29,A35,PROB_2:def 2;
end;
case
k <> len (G1^<*F.(n+1)*>);
then k <> len G1 + len <*F.(n+1)*> by FINSEQ_1:22;
then
A36: k <> len G1 + 1 by FINSEQ_1:39;
A37: k in Seg (len (G1^<*F.(n+1)*>)) by A27,FINSEQ_1:def 3;
then k in Seg (len G1 + len <*F.(n+1)*>) by FINSEQ_1:22;
then k in Seg (len G1 + 1) by FINSEQ_1:39;
then k <= len G1 + 1 by FINSEQ_1:1;
then k < len G1 + 1 by A36,XXREAL_0:1;
then
A38: k <= len G1 by NAT_1:13;
1 <= k by A37,FINSEQ_1:1;
then
A39: k in dom G1 by A38,FINSEQ_3:25;
then
A40: (G1^<*F.(n+1)*>).k = G1.k by FINSEQ_1:def 7;
now
per cases;
case
m = len (G1^<*F.(n+1)*>);
then m = len G1 + len <*F.(n+1)*> by FINSEQ_1:22;
then
A41: m = len G1 + 1 by FINSEQ_1:39;
1 <= len <*F.(n+1)*> by FINSEQ_1:39;
then
A42: (G1^<*F.(n+1)*>).m = <*F.( n+1)*>.1 by A41,FINSEQ_1:65
.= F.(n+1);
consider k1 be Nat such that
A43: k1 in dom F1 and
A44: F1.k1 = G1.k by A7,A39;
k1 in Seg len F1 by A43,FINSEQ_1:def 3;
then k1 <= n by A5,FINSEQ_1:1;
then
A45: k1 <> n+1 by NAT_1:13;
(G1^<*F.(n+1)*>).k = F.k1 by A17,A40,A43,A44,
FINSEQ_1:def 7;
hence thesis by A42,A45,PROB_2:def 2;
end;
case
m <> len (G1^<*F.(n+1)*>);
then m <> len G1 + len <*F.(n+1)*> by FINSEQ_1:22;
then
A46: m <> len G1 + 1 by FINSEQ_1:39;
A47: m in Seg (len (G1^<*F.(n+1)*>)) by A27,FINSEQ_1:def 3;
then m in Seg (len G1 + len <*F.(n+1)*>) by FINSEQ_1:22
;
then m in Seg (len G1 + 1) by FINSEQ_1:39;
then m <= len G1 + 1 by FINSEQ_1:1;
then m < len G1 + 1 by A46,XXREAL_0:1;
then
A48: m <= len G1 by NAT_1:13;
1 <= m by A47,FINSEQ_1:1;
then m in dom G1 by A48,FINSEQ_3:25;
then (G1^<*F.(n+1)*>).m = G1.m by FINSEQ_1:def 7;
hence thesis by A26,A40,PROB_2:def 2;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
case
not(k in dom (G1^<*F.(n+1)*>) & m in dom (G1^<*F.(n+ 1)*>));
then (G1^<*F.(n+1)*>).k = {} or (G1^<*F.(n+1)*>).m = {} by
FUNCT_1:def 2;
hence thesis;
end;
end;
hence thesis;
end;
1 <= n+1 by NAT_1:11;
then n+1 in Seg (n+1) by FINSEQ_1:1;
then n+1 in dom F by A3,FINSEQ_1:def 3;
then F.(n+1) in rng F by FUNCT_1:3;
then <*F.(n+1)*> is FinSequence of S by FINSEQ_1:74;
then reconsider G = G1^<*F.(n+1)*> as Finite_Sep_Sequence of S by A25
,FINSEQ_1:75,PROB_2:def 2;
A49: len G = len G1 + len <*F.(n+1)*> by FINSEQ_1:22
.= len G1 + 1 by FINSEQ_1:39;
A50: for k be Nat st k in dom G holds (G.k <> {} & ex m be Nat st m
in dom F & F.m = G.k)
proof
let k be Nat;
assume
A51: k in dom G;
reconsider k as Element of NAT by ORDINAL1:def 12;
now
per cases;
case
A52: k = len G;
1 <= n+1 by NAT_1:11;
then n+1 in Seg (n+1) by FINSEQ_1:1;
then
A53: n+1 in dom F by A3,FINSEQ_1:def 3;
dom <*F.(n+1)*> = Seg 1 by FINSEQ_1:38;
then 1 in dom <*F.(n+1)*> by FINSEQ_1:2,TARSKI:def 1;
then G.k = <*F.(n+1)*>.1 by A49,A52,FINSEQ_1:def 7
.= F.(n+1);
hence thesis by A24,A53;
end;
case
A54: k <> len G;
k <= len G by A51,FINSEQ_3:25;
then k < len G by A54,XXREAL_0:1;
then
A55: k <= len G1 by A49,NAT_1:13;
1 <= k by A51,FINSEQ_3:25;
then
A56: k in dom G1 by A55,FINSEQ_3:25;
then
A57: G.k = G1.k by FINSEQ_1:def 7;
ex m be Nat st m in dom F & F.m = G.k
proof
consider m be Nat such that
A58: m in dom F1 & F1.m = G1.k by A7,A56;
take m;
dom F1 c= dom F by A8,FINSEQ_1:26;
hence thesis by A17,A57,A58,FINSEQ_1:def 7;
end;
hence thesis by A7,A56,A57;
end;
end;
hence thesis;
end;
take G;
rng F = rng F1 \/ rng <*F.(n+1)*> by A17,FINSEQ_1:31;
then union rng F = union rng F1 \/ union rng <*F.(n+1)*> by
ZFMISC_1:78
.= union (rng G1 \/ rng <*F.(n+1)*>) by A6,ZFMISC_1:78
.= union rng G by FINSEQ_1:31;
hence thesis by A50;
end;
end;
hence thesis;
end;
hence thesis;
end;
A59: len F = len F;
A60: P[0]
proof
let F be Finite_Sep_Sequence of S;
assume
A61: len F = 0;
take G = F;
G = {} by A61;
hence thesis;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A60,A1);
hence thesis by A59;
end;
Lm1: for a be FinSequence of ExtREAL, p,N be Element of ExtREAL st N = len a &
(for n be Nat st n in dom a holds a.n = p) holds Sum(a) = N * p
proof
defpred P[Nat] means for F be FinSequence of ExtREAL, p be Element of
ExtREAL st $1 = len F & (for n be Nat st n in dom F holds F.n = p) holds ex N
be Element of ExtREAL st N = $1 & Sum(F) = N * p;
let a be FinSequence of ExtREAL;
let p,N be Element of ExtREAL;
assume that
A1: N = len a and
A2: for n be Nat st n in dom a holds a.n = p;
A3: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A4: P[k];
reconsider k as Element of NAT by ORDINAL1:def 12;
for F be FinSequence of ExtREAL, p be Element of ExtREAL st k+1 = len
F & (for n be Nat st n in dom F holds F.n = p)
ex N be Element of ExtREAL st N = k+1 & Sum(F) = N * p
proof
let F be FinSequence of ExtREAL;
let p be Element of ExtREAL;
assume that
A5: k+1 = len F and
A6: for n be Nat st n in dom F holds F.n = p;
F <> {} by A5;
then consider G be FinSequence, v be object such that
A7: F = G^<*v*> by FINSEQ_1:46;
reconsider G as FinSequence of ExtREAL by A7,FINSEQ_1:36;
A8: k + 1 = len G + len <*v*> by A5,A7,FINSEQ_1:22
.= len G + 1 by FINSEQ_1:39;
dom <*v*> = Seg 1 by FINSEQ_1:38;
then
A9: 1 in dom <*v*> by FINSEQ_1:2,TARSKI:def 1;
1 <= k + 1 by NAT_1:11;
then
A10: k + 1 in dom F by A5,FINSEQ_3:25;
v = <*v*>.1
.= F.(k + 1) by A7,A8,A9,FINSEQ_1:def 7
.= p by A6,A10;
then reconsider v as Element of ExtREAL;
consider g be sequence of ExtREAL such that
A11: Sum(G) = g.(len G) and
A12: g.0 = 0. and
A13: for i being Nat st i < len G holds g.(i+1) = g.i + G
.(i+ 1) by EXTREAL1:def 2;
for n be Nat st n in dom G holds G.n = p
proof
let n be Nat;
A14: len G <= len G + 1 by NAT_1:11;
assume
A15: n in dom G;
then n <= len G by FINSEQ_3:25;
then
A16: n <= len G + 1 by A14,XXREAL_0:2;
A17: len F = len G + len <*v*> by A7,FINSEQ_1:22
.= len G + 1 by FINSEQ_1:39;
1 <= n by A15,FINSEQ_3:25;
then n in dom F by A16,A17,FINSEQ_3:25;
then F.n = p by A6;
hence thesis by A7,A15,FINSEQ_1:def 7;
end;
then consider N1 be Element of ExtREAL such that
A18: N1 = k and
A19: Sum(G) = N1 * p by A4,A8;
consider f be sequence of ExtREAL such that
A20: Sum(F) = f.(len F) and
A21: f.0 = 0. and
A22: for i being Nat st i < len F holds f.(i+1) = f.i + F
.(i+ 1) by EXTREAL1:def 2;
A23: for k1 be Nat st k1 <= len G holds f.k1 = g.k1
proof
defpred P2[Nat] means $1 <= len G implies f.$1 = g.$1;
A24: for k1 be Nat st P2[k1] holds P2[k1+1]
proof
let k1 be Nat;
assume
A25: P2[k1];
reconsider k1 as Element of NAT by ORDINAL1:def 12;
now
assume
A26: k1+1 <= len G;
then
A27: k1 < len G by NAT_1:13;
len F = len G + len <*v*> by A7,FINSEQ_1:22
.= len G + 1 by FINSEQ_1:39;
then k1 < len F by A27,NAT_1:13;
then
A28: f.(k1+1) = f.k1 + F.(k1+1) by A22;
1 <= k1 + 1 by NAT_1:11;
then
A29: k1 + 1 in dom G by A26,FINSEQ_3:25;
k1 <= k1+1 & g.(k1+1) = g.k1 + G.(k1+1) by A13,A27,NAT_1:11;
hence thesis by A7,A25,A28,A29,FINSEQ_1:def 7,XXREAL_0:2;
end;
hence thesis;
end;
A30: P2[0] by A21,A12;
for k1 be Nat holds P2[k1] from NAT_1:sch 2(A30,A24);
hence thesis;
end;
take N1+1.;
reconsider jj=1 as Real;
thus N1+1. = k+jj by A18,SUPINF_2:1
.= k+1;
k < len F by A5,NAT_1:13;
then Sum(F) = f.k + F.(k+1) by A5,A20,A22
.= g.k + F.(k+1) by A8,A23;
then Sum(F) = Sum(G) + p by A6,A8,A10,A11
.= N1 * p + 1. * p by A19,XXREAL_3:81;
hence Sum(F) = (N1+1.) * p by A18,XXREAL_3:96;
end;
hence thesis;
end;
for F be FinSequence of ExtREAL, p be Element of ExtREAL st 0 = len F &
(for n be Nat st n in dom F holds F.n = p) holds ex N be Element of ExtREAL st
N = 0 & Sum(F) = N * p
proof
let F be FinSequence of ExtREAL;
let p be Element of ExtREAL;
assume that
A31: 0 = len F and
for n be Nat st n in dom F holds F.n = p;
take 0.;
ex f be sequence of ExtREAL st Sum(F) = f.(len F) & f.0 = 0. & for
i be Nat st i < len F holds f.(i+1)=f.i+F.(i+1) by EXTREAL1:def 2;
hence thesis by A31;
end;
then
A32: P[0];
for k be Nat holds P[k] from NAT_1:sch 2(A32,A3);
then ex N9 be Element of ExtREAL st N9 = len a & Sum(a) = N9 * p by A2;
hence thesis by A1;
end;
Lm2: for X be non empty set, S be SigmaField of X, f be PartFunc of X,ExtREAL
st f is_simple_func_in S & f is nonnegative &
(for x be object st x in dom f holds 0. <> f.x)
ex F be Finite_Sep_Sequence of S,
a be FinSequence of ExtREAL st F,a are_Re-presentation_of f & a.1=0. & for n be
Nat st 2 <= n & n in dom a holds 0. < a.n & a.n < +infty
proof
let X be non empty set;
let S be SigmaField of X;
let f be PartFunc of X,ExtREAL;
assume that
A1: f is_simple_func_in S and
A2: f is nonnegative and
A3: for x be object st x in dom f holds 0. <> f.x;
a2: for x be object st x in dom f holds 0. <= f.x by A2,SUPINF_2:39;
consider F1 be Finite_Sep_Sequence of S such that
A4: dom f = union rng F1 and
A5: for n be Nat, x,y be Element of X st n in dom F1 & x in F1.n & y in
F1.n holds f.x = f.y by A1,MESFUNC2:def 4;
consider G be Finite_Sep_Sequence of S such that
A6: union rng F1 = union rng G and
A7: for n be Nat st n in dom G holds (G.n <> {} & ex m be Nat st m in
dom F1 & F1.m = G.n) by Th13;
set F = <*{}*>^G;
rng <*{}*> = {{}} & {} in S by FINSEQ_1:38,MEASURE1:7;
then rng <*{}*> c= S by ZFMISC_1:31;
then rng <*{}*> \/ rng G c= S by XBOOLE_1:8;
then rng F c= S by FINSEQ_1:31;
then reconsider F as FinSequence of S by FINSEQ_1:def 4;
for x,y be object st x <> y holds F.x misses F.y
proof
let x,y be object;
assume
A8: x<>y;
now
per cases;
case
A9: x in dom F & y in dom F;
then reconsider x,y as Element of NAT;
A10: x in Seg (len (<*{}*>^G)) by A9,FINSEQ_1:def 3;
then
A11: x <= len (<*{}*>^G) by FINSEQ_1:1;
A12: y in Seg (len (<*{}*>^G)) by A9,FINSEQ_1:def 3;
then
A13: 1 <= y by FINSEQ_1:1;
A14: y <= len (<*{}*>^G) by A12,FINSEQ_1:1;
A15: 1 <= x by A10,FINSEQ_1:1;
now
per cases;
case
A16: x = 1 or y = 1;
A17: dom <*{}*> = Seg 1 by FINSEQ_1:38;
now
per cases by A16;
case
A18: x = 1;
then x in dom <*{}*> by A17,FINSEQ_1:2,TARSKI:def 1;
then F.x = <*{}*>.x by FINSEQ_1:def 7;
then F.x = {} by A18;
hence thesis;
end;
case
A19: y = 1;
then y in dom <*{}*> by A17,FINSEQ_1:2,TARSKI:def 1;
then F.y = <*{}*>.y by FINSEQ_1:def 7;
then F.y = {} by A19;
hence thesis;
end;
end;
hence thesis;
end;
case
A20: x <> 1 & y <> 1;
then 1 < y by A13,XXREAL_0:1;
then len <*{}*> < y by FINSEQ_1:40;
then
A21: F.y = G.(y - len <*{}*> ) by A14,FINSEQ_1:24;
1 < x by A15,A20,XXREAL_0:1;
then len <*{}*> < x by FINSEQ_1:40;
then
A22: F.x = G.(x - len <*{}*>) by A11,FINSEQ_1:24;
x - (len <*{}*>) <> y - (len <*{}*>) by A8;
hence thesis by A22,A21,PROB_2:def 2;
end;
end;
hence thesis;
end;
case
not x in dom F or not y in dom F;
then F.x = {} or F.y = {} by FUNCT_1:def 2;
hence thesis;
end;
end;
hence thesis;
end;
then reconsider F as Finite_Sep_Sequence of S by PROB_2:def 2;
A23: union rng F = union (rng <*{}*> \/ rng G) by FINSEQ_1:31
.= union ({{}} \/ rng G) by FINSEQ_1:38
.= union {{}} \/ union rng G by ZFMISC_1:78
.= {} \/ union rng G by ZFMISC_1:25
.= dom f by A4,A6;
defpred P[Nat,Element of ExtREAL] means (for x be Element of X st $1 in dom
F & $1 = 1 holds $2 = 0.) & (for x be Element of X st $1 in dom F & $1 >= 2 & x
in F.$1 holds $2 = f.x);
A24: for k be Nat st k in Seg len F ex y be Element of ExtREAL st P[k,y]
proof
let k be Nat;
assume
A25: k in Seg len F;
ex y be Element of ExtREAL st P[k,y]
proof
per cases;
suppose
A26: k = 1;
take y = 0.;
( for x be Element of X st k in dom F & k = 1 holds y = 0.)&
for x be Element of X st k in dom F & k >= 2 & x in F.k holds y = f.x by A26;
hence thesis;
end;
suppose
A27: k <> 1;
A28: k <= len F by A25,FINSEQ_1:1;
then k <= len <*{}*> + len G by FINSEQ_1:22;
then
A29: k - len <*{}*> <= len G by XREAL_1:20;
1 <= k by A25,FINSEQ_1:1;
then 1 < k by A27,XXREAL_0:1;
then 1+1 <= k by NAT_1:13;
then
A30: len <*{}*> + 1 <= k by FINSEQ_1:39;
then consider k2 being Nat such that
A31: len <*{}*> + 1 + k2 = k by NAT_1:10;
reconsider k2 as Element of NAT by ORDINAL1:def 12;
1 + k2 = k - len <*{}*> by A31;
then 1 <= 1 + k2 by A30,XREAL_1:19;
then 1 + k2 in Seg len G by A31,A29,FINSEQ_1:1;
then
A32: 1 + k2 in dom G by FINSEQ_1:def 3;
then consider m1 be Nat such that
A33: m1 in dom F1 and
A34: F1.m1 = G.(1+k2) by A7;
k <= len <*{}*> + len G by A28,FINSEQ_1:22;
then
A35: F.k = G.(k - len <*{}*>) by A30,FINSEQ_1:23
.= G.(1+k2) by A31;
then F.k <> {} by A7,A32;
then consider z be object such that
A36: z in F.k by XBOOLE_0:def 1;
reconsider z as set by TARSKI:1;
take y = f.z;
F.k in rng F1 by A35,A33,A34,FUNCT_1:3;
then F.k in S;
then reconsider z as Element of X by A36;
A37: for x be Element of X st k in dom F & k >= 2 & x in F.k holds y = f.x
proof
let x be Element of X;
assume that
k in dom F and
k >= 2 and
A38: x in F.k;
z in F1.m1 by A35,A36,A34;
hence thesis by A5,A35,A33,A34,A38;
end;
for x be Element of X st k in dom F & k = 1 holds y = 0. by A27;
hence thesis by A37;
end;
end;
hence thesis;
end;
consider a be FinSequence of ExtREAL such that
A39: dom a = Seg len F & for n be Nat st n in Seg len F holds P[n,a.n]
from FINSEQ_1:sch 5(A24);
A40: dom F = dom a by A39,FINSEQ_1:def 3;
A41: for n be Nat, x be Element of X st n in dom F & n >= 2 & x in F.n holds
a.n = f.x
proof
let n be Nat;
let x be Element of X;
assume that
A42: n in dom F and
A43: n >= 2 & x in F.n;
n in Seg len F by A42,FINSEQ_1:def 3;
hence thesis by A39,A42,A43;
end;
A44: for n be Nat st 2 <= n & n in dom a holds 0. < a.n & a.n < +infty
proof
let n be Nat;
assume that
A45: 2 <= n and
A46: n in dom a;
1+1 <= n by A45;
then
A47: len <*{}*> + 1 <= n by FINSEQ_1:39;
n <= len F by A39,A46,FINSEQ_1:1;
then n <= len <*{}*> + len G by FINSEQ_1:22;
then
A48: F.n = G.(n - len <*{}*>) by A47,FINSEQ_1:23
.= G.(n-1) by FINSEQ_1:39;
dom <*{}*> = {1} & 1 <> n by A45,FINSEQ_1:2,38;
then not n in dom <*{}*> by TARSKI:def 1;
then consider k be Nat such that
A49: k in dom G and
A50: n = len <*{}*> + k by A40,A46,FINSEQ_1:25;
n = 1 + k by A50,FINSEQ_1:39;
then F.n <> {} by A7,A48,A49;
then consider x1 be object such that
A51: x1 in F.n by XBOOLE_0:def 1;
A52: F.n c= union rng F by A40,A46,FUNCT_1:3,ZFMISC_1:74;
then x1 in dom f by A23,A51;
then reconsider x1 as Element of X;
A53: 0. <> f.x1 by A3,A23,A51,A52;
f is real-valued by A1,MESFUNC2:def 4;
then
A54: |.f.x1.| < +infty by A23,A51,A52,MESFUNC2:def 1;
a.n = f.x1 by A41,A40,A45,A46,A51;
hence thesis by A23,A51,A52,A54,A53,EXTREAL1:21,a2;
end;
take F,a;
A55: for n9 be Nat st n9 in dom F for x be object st x in F.n9 holds f.x=a.n9
proof
let n9 be Nat;
assume
A56: n9 in dom F;
now
per cases;
case
A57: n9 = 1;
thus for x be set st x in F.n9 holds f.x = a.n9
proof
let x be set;
dom <*{}*> = {1} by FINSEQ_1:2,38;
then 1 in dom <*{}*> by TARSKI:def 1;
then
A58: F.1 = <*{}*>.1 by FINSEQ_1:def 7
.= {};
assume x in F.n9;
hence thesis by A57,A58;
end;
end;
case
A59: n9 <> 1;
n9 in Seg len F by A56,FINSEQ_1:def 3;
then 1 <= n9 by FINSEQ_1:1;
then 1 < n9 by A59,XXREAL_0:1;
then
A60: 1+1 <= n9 by NAT_1:13;
thus for x be set st x in F.n9 holds f.x = a.n9
proof
let x be set;
assume
A61: x in F.n9;
F.n9 in rng F by A56,FUNCT_1:3;
then F.n9 in S;
then reconsider x as Element of X by A61;
a.n9 = f.x by A41,A56,A60,A61;
hence thesis;
end;
end;
end;
hence thesis;
end;
len F = len <*{}*> + len G by FINSEQ_1:22
.= 1 + len G by FINSEQ_1:39;
then 1 <= len F by NAT_1:11;
then 1 in Seg len F by FINSEQ_1:1;
hence thesis by A23,A39,A40,A55,A44;
end;
Lm3: for X be non empty set, S be SigmaField of X, f be PartFunc of X,ExtREAL
st f is_simple_func_in S & f is nonnegative
& (ex x
be set st x in dom f & 0. = f.x) holds ex F be Finite_Sep_Sequence of S, a be
FinSequence of ExtREAL st F,a are_Re-presentation_of f & a.1=0. & for n be Nat
st 2 <= n & n in dom a holds 0. < a.n & a.n < +infty
proof
let X be non empty set;
let S be SigmaField of X;
let f be PartFunc of X,ExtREAL;
assume that
A1: f is_simple_func_in S and
A2: f is nonnegative and
A3: ex x be set st x in dom f & 0. = f.x;
a2: for x be object st x in dom f holds 0. <= f.x by A2,SUPINF_2:39;
consider x0 be set such that
A4: x0 in dom f and
A5: 0.= f.x0 by A3;
reconsider x0 as Element of X by A4;
consider F1 be Finite_Sep_Sequence of S such that
A6: dom f = union rng F1 and
A7: for n be Nat, x,y be Element of X st n in dom F1 & x in F1.n & y in
F1.n holds f.x = f.y by A1,MESFUNC2:def 4;
consider V be set such that
A8: x0 in V and
A9: V in rng F1 by A4,A6,TARSKI:def 4;
consider n0 be object such that
A10: n0 in dom F1 and
A11: V = F1.n0 by A9,FUNCT_1:def 3;
set F0 = {Fn where Fn is Element of S : Fn in rng F1 & for x be Element of X
st x in Fn holds f.x = 0.};
set G1 = union F0;
for F9 be object st F9 in F0 holds F9 in bool X
proof
let F9 be object;
assume F9 in F0;
then ex Fn be Element of S st F9=Fn & Fn in rng F1 & for x be Element of X
st x in Fn holds f.x = 0.;
hence thesis;
end;
then reconsider F0 as Subset-Family of X by TARSKI:def 3;
set N={n where n is Element of NAT: n in dom F1 & for x be Element of X st x
in F1.n holds f.x = 0.};
A12: len F1 <= len F1 + 1 by NAT_1:11;
reconsider n0 as Element of NAT by A10;
F1.n0 is Element of S & F1.n0 in rng F1 & for x be Element of X st x in
F1.n0 holds f.x = 0.
proof
F1.n0 in rng F1 by A10,FUNCT_1:3;
hence F1.n0 is Element of S;
thus F1.n0 in rng F1 by A10,FUNCT_1:3;
let x be Element of X;
assume x in F1.n0;
hence thesis by A5,A7,A8,A10,A11;
end;
then
A13: F1.n0 in F0;
for z be object st z in F0 holds z in rng F1
proof
let z be object;
assume z in F0;
then ex Fn9 be Element of S st z = Fn9 & Fn9 in rng F1 & for x be Element
of X st x in Fn9 holds f.x = 0.;
hence thesis;
end;
then
A14: F0 c= rng F1;
for z be object st z in N holds z in dom F1
proof
let z be object;
assume z in N;
then
ex n9 be Element of NAT st z = n9 & n9 in dom F1 & for x be Element of
X st x in F1.n9 holds f.x = 0.;
hence thesis;
end;
then
A15: N c= dom F1;
then reconsider N as finite set;
consider P1 be FinSequence such that
A16: rng P1 = N & P1 is one-to-one by FINSEQ_4:58;
reconsider F0 as N_Sub_set_fam of X by A14,A13;
for F9 be object st F9 in F0 holds F9 in S
proof
let F9 be object;
assume F9 in F0;
then ex Fn be Element of S st F9=Fn & Fn in rng F1 & for x be Element of X
st x in Fn holds f.x = 0.;
hence thesis;
end;
then F0 c= S;
then reconsider G1 as Element of S by MEASURE1:def 5;
A17: len P1 = card N by A16,FINSEQ_4:62;
reconsider L = Seg len F1 as finite set;
set M = findom F1 \ N;
consider P2 be FinSequence such that
A18: rng P2 = M and
A19: P2 is one-to-one by FINSEQ_4:58;
A20: N c= Seg len F1 by A15,FINSEQ_1:def 3;
then card N <= card L by NAT_1:43;
then len P1 <= len F1 by A17,FINSEQ_1:57;
then consider lenF being Nat such that
A21: len F1 + 1 = len P1 + lenF by A12,NAT_1:10,XXREAL_0:2;
reconsider lenF as Element of NAT by ORDINAL1:def 12;
M = (Seg len F1) \ N by FINSEQ_1:def 3;
then
A22: card M = card (Seg len F1) - card N by A20,CARD_2:44;
defpred P[Nat,set] means ($1 = 1 implies $2 = G1) & ($1 >=2 implies ex k9 be
Nat st k9=$1-1 & $2 = F1.(P2.k9));
len P2 = card M by A18,A19,FINSEQ_4:62;
then
A23: len P2 = len F1 - len P1 + 1 - 1 by A17,A22,FINSEQ_1:57;
A24: for k be Nat st k in Seg lenF ex U be Element of S st P[k,U]
proof
let k be Nat;
assume
A25: k in Seg lenF;
per cases;
suppose
A26: k = 1;
take G1;
thus thesis by A26;
end;
suppose
A27: k <> 1;
A28: k >= 1 by A25,FINSEQ_1:1;
then consider k9 being Nat such that
A29: k = 1 + k9 by NAT_1:10;
k > 1 by A27,A28,XXREAL_0:1;
then k >= 1+1 by NAT_1:13;
then
A30: k-1>=1 by XREAL_1:19;
k <= lenF by A25,FINSEQ_1:1;
then k-1<=lenF -1 by XREAL_1:9;
then k9 in Seg len P2 by A21,A23,A29,A30,FINSEQ_1:1;
then k9 in dom P2 by FINSEQ_1:def 3;
then P2.k9 in M by A18,FUNCT_1:3;
then F1.(P2.k9) in rng F1 by FUNCT_1:3;
then reconsider U = F1.(P2.k9) as Element of S;
take U;
thus thesis by A27,A29;
end;
end;
consider F be FinSequence of S such that
A31: dom F = Seg lenF & for k be Nat st k in Seg lenF holds P[k,F.k]
from FINSEQ_1:sch 5(A24);
defpred A[Nat,Element of ExtREAL] means for y be Element of X holds (y in F.
$1 implies $2 = f.y) & (F.$1 = {} implies $2 = 1.);
A32: for k be Nat st k in Seg len F ex x be Element of ExtREAL st A[k,x]
proof
let k be Nat;
assume
A33: k in Seg len F;
then
A34: k in dom F by FINSEQ_1:def 3;
now
per cases;
case
A35: k = 1;
take x = 0.;
A36: F.k = G1 by A31,A34,A35;
for y be Element of X holds (y in F.k implies 0. = f.y) & (F.k =
{} implies 0.=1.)
proof
let y be Element of X;
y in F.k implies 0. = f.y
proof
assume y in F.k;
then consider Y be set such that
A37: y in Y and
A38: Y in F0 by A36,TARSKI:def 4;
ex Fn be Element of S st Y = Fn & Fn in rng F1 & for x be
Element of X st x in Fn holds f.x = 0. by A38;
hence thesis by A37;
end;
hence thesis by A8,A11,A13,A36,TARSKI:def 4;
end;
hence thesis;
end;
case
A39: k <> 1;
1 <= k by A33,FINSEQ_1:1;
then 1 < k by A39,XXREAL_0:1;
then
A40: 1+1 <= k by NAT_1:13;
then consider k1 be Nat such that
A41: k1 = k-1 and
A42: F.k = F1.(P2.k1) by A31,A34;
A43: 1 <= k1 by A40,A41,XREAL_1:19;
k <= lenF by A31,A34,FINSEQ_1:1;
then k1 <= len P2 by A21,A23,A41,XREAL_1:9;
then k1 in Seg len P2 by A43,FINSEQ_1:1;
then k1 in dom P2 by FINSEQ_1:def 3;
then P2.k1 in M by A18,FUNCT_1:3;
then consider k9 be set such that
A44: k9 in dom F1 and
A45: F.k = F1.k9 by A42;
now
per cases;
case
A46: F.k = {};
take x = 1.;
for y be Element of X holds (y in F.k implies 1. = f.y) & (F.
k = {} implies 1.=1.) by A46;
hence thesis;
end;
case
F.k <> {};
then consider y1 be object such that
A47: y1 in F.k by XBOOLE_0:def 1;
F.k in rng F by A34,FUNCT_1:3;
then F.k in S;
then reconsider y1 as Element of X by A47;
take x = f.y1;
for y be Element of X holds (y in F.k implies x = f.y) & (F.k
= {} implies x=1.) by A7,A44,A45,A47;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
consider a be FinSequence of ExtREAL such that
A48: dom a = Seg len F & for n be Nat st n in Seg (len F) holds A[n,a.n]
from FINSEQ_1:sch 5(A32);
A49: for n be Nat, x be Element of X st n in dom F & x in F.n holds a.n = f. x
proof
let n be Nat;
let x be Element of X;
assume that
A50: n in dom F and
A51: x in F.n;
n in Seg len F by A50,FINSEQ_1:def 3;
hence thesis by A48,A51;
end;
A52: for n be Nat st n in dom F for x be object st x in F.n holds f.x=a.n
proof
let n be Nat;
assume
A53: n in dom F;
let x be object;
assume
A54: x in F.n;
F.n in rng F by A53,FUNCT_1:3;
then F.n in S;
then reconsider x as Element of X by A54;
a.n = f.x by A49,A53,A54;
hence thesis;
end;
A55: for x be Element of X st x in F1.n0 holds f.x = 0. by A5,A7,A8,A10,A11;
A56: a.1 = 0. & dom F = dom a & for n be Nat,x be Element of X st n in dom
F & x in F.n holds a.n = f.x
proof
reconsider F1n0 = F1.n0 as Element of S by A9,A11;
0+1 <= lenF by A21,A23,XREAL_1:19;
then
A57: 1 in Seg lenF by FINSEQ_1:1;
then
A58: 1 in Seg len F by A31,FINSEQ_1:def 3;
A59: F.1 = G1 by A31,A57;
F1n0 in F0 by A9,A11,A55;
then x0 in F.1 by A8,A11,A59,TARSKI:def 4;
hence a.1 = 0. by A5,A48,A58;
thus dom F = dom a by A48,FINSEQ_1:def 3;
thus thesis by A49;
end;
A60: for n,m be Nat st n in dom F & m in dom F & n = 1 & m <> 1 holds F.n
misses F.m
proof
let n,m be Nat;
assume that
A61: n in dom F and
A62: m in dom F and
A63: n = 1 and
A64: m <> 1;
A65: F.n = G1 by A31,A61,A63;
m <= lenF by A31,A62,FINSEQ_1:1;
then
A66: m-1<=lenF -1 by XREAL_1:9;
1 <= m by A62,FINSEQ_3:25;
then 1 < m by A64,XXREAL_0:1;
then
A67: 1+1 <= m by NAT_1:13;
then consider k9 be Nat such that
A68: k9 = m-1 and
A69: F.m = F1.(P2.k9) by A31,A62;
m-1>=1 by A67,XREAL_1:19;
then k9 in Seg len P2 by A21,A23,A68,A66,FINSEQ_1:1;
then k9 in dom P2 by FINSEQ_1:def 3;
then
A70: P2.k9 in M by A18,FUNCT_1:3;
then
A71: not P2.k9 in N by XBOOLE_0:def 5;
F.n /\ F.m = {}
proof
assume F.n /\ F.m <> {};
then consider v be object such that
A72: v in F.n /\ F.m by XBOOLE_0:def 1;
A73: v in F.m by A72,XBOOLE_0:def 4;
v in F.n by A72,XBOOLE_0:def 4;
then consider Y be set such that
A74: v in Y and
A75: Y in F0 by A65,TARSKI:def 4;
consider Fv be Element of S such that
A76: Y = Fv and
A77: Fv in rng F1 and
A78: for x be Element of X st x in Fv holds f.x = 0. by A75;
consider n9 be object such that
A79: n9 in dom F1 and
A80: Fv = F1.n9 by A77,FUNCT_1:def 3;
reconsider n9 as Element of NAT by A79;
n9 <> P2.k9 by A70,A71,A78,A80;
then F1.(n9) misses F1.(P2.k9) by PROB_2:def 2;
then F1.(n9) /\ F1.(P2.k9) = {};
hence contradiction by A69,A73,A74,A76,A80,XBOOLE_0:def 4;
end;
hence thesis;
end;
A81: for n,m be Nat st n in dom F & m in dom F & n <> 1 & m <> 1 & n <> m
holds F.n misses F.m
proof
let n,m be Nat;
assume that
A82: n in dom F and
A83: m in dom F and
A84: n <> 1 and
A85: m <> 1 and
A86: n <> m;
n <= lenF by A31,A82,FINSEQ_1:1;
then
A87: n-1 <= lenF -1 by XREAL_1:9;
m <= lenF by A31,A83,FINSEQ_1:1;
then
A88: m-1<=lenF -1 by XREAL_1:9;
1 <= m by A31,A83,FINSEQ_1:1;
then 1 < m by A85,XXREAL_0:1;
then
A89: 1+1 <= m by NAT_1:13;
then consider k2 be Nat such that
A90: k2 = m-1 and
A91: F.m = F1.(P2.k2) by A31,A83;
1<=m-1 by A89,XREAL_1:19;
then k2 in Seg len P2 by A21,A23,A90,A88,FINSEQ_1:1;
then
A92: k2 in dom P2 by FINSEQ_1:def 3;
1 <= n by A31,A82,FINSEQ_1:1;
then 1 < n by A84,XXREAL_0:1;
then
A93: 1+1 <= n by NAT_1:13;
then consider k1 be Nat such that
A94: k1 = n-1 and
A95: F.n = F1.(P2.k1) by A31,A82;
1 <= n-1 by A93,XREAL_1:19;
then k1 in Seg len P2 by A21,A23,A94,A87,FINSEQ_1:1;
then
A96: k1 in dom P2 by FINSEQ_1:def 3;
k1 <> k2 by A86,A94,A90;
then P2.k1 <> P2.k2 by A19,A96,A92,FUNCT_1:def 4;
hence thesis by A95,A91,PROB_2:def 2;
end;
A97: for x,y be object st x <> y holds F.x misses F.y
proof
let x,y be object;
assume
A98: x<>y;
now
per cases;
case
A99: x in dom F & y in dom F;
then reconsider x,y as Element of NAT;
now
per cases;
case
x = 1 or y = 1;
hence thesis by A60,A98,A99;
end;
case
x <> 1 & y <> 1;
hence thesis by A81,A98,A99;
end;
end;
hence thesis;
end;
case
A100: not x in dom F or not y in dom F;
now
per cases by A100;
case
not x in dom F;
then F.x = {} by FUNCT_1:def 2;
hence thesis;
end;
case
not y in dom F;
then F.y = {} by FUNCT_1:def 2;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
for z be object st z in union rng F holds z in union rng F1
proof
let z be object;
assume z in union rng F;
then consider Y be set such that
A101: z in Y and
A102: Y in rng F by TARSKI:def 4;
consider k be object such that
A103: k in dom F and
A104: Y = F.k by A102,FUNCT_1:def 3;
reconsider k as Element of NAT by A103;
now
per cases;
case
k = 1;
then z in G1 by A31,A101,A103,A104;
then consider Y9 be set such that
A105: z in Y9 and
A106: Y9 in F0 by TARSKI:def 4;
ex Fn9 be Element of S st Y9 = Fn9 & Fn9 in rng F1 & for x be
Element of X st x in Fn9 holds f.x = 0. by A106;
hence thesis by A105,TARSKI:def 4;
end;
case
A107: k <> 1;
1 <= k by A31,A103,FINSEQ_1:1;
then 1 < k by A107,XXREAL_0:1;
then
A108: 1 + 1 <= k by NAT_1:13;
then consider k9 be Nat such that
A109: k9 = k-1 and
A110: F.k = F1.(P2.k9) by A31,A103;
A111: 1 <= k9 by A108,A109,XREAL_1:19;
k <= lenF by A31,A103,FINSEQ_1:1;
then k9 <= len P2 by A21,A23,A109,XREAL_1:9;
then k9 in dom P2 by A111,FINSEQ_3:25;
then P2.k9 in M by A18,FUNCT_1:3;
then F1.(P2.k9) in rng F1 by FUNCT_1:3;
hence thesis by A101,A104,A110,TARSKI:def 4;
end;
end;
hence thesis;
end;
then
A112: union rng F c= union rng F1;
for z be object st z in union rng F1 holds z in union rng F
proof
let z be object;
assume z in union rng F1;
then consider Y be set such that
A113: z in Y and
A114: Y in rng F1 by TARSKI:def 4;
consider m1 be object such that
A115: m1 in dom F1 and
A116: Y = F1.m1 by A114,FUNCT_1:def 3;
reconsider m1 as Element of NAT by A115;
now
per cases;
case
m1 in N;
then ex m19 be Element of NAT st m1 = m19 & m19 in dom F1 & for x be
Element of X st x in F1.m19 holds f.x = 0.;
then Y in F0 by A114,A116;
then
A117: z in union F0 by A113,TARSKI:def 4;
lenF >= 1+0 by A21,A23,XREAL_1:19;
then
A118: 1 in Seg lenF by FINSEQ_1:1;
then F.1 in rng F by A31,FUNCT_1:3;
then union F0 in rng F by A31,A118;
hence thesis by A117,TARSKI:def 4;
end;
case
not m1 in N;
then m1 in M by A115,XBOOLE_0:def 5;
then consider m19 be object such that
A119: m19 in dom P2 and
A120: m1 = P2.m19 by A18,FUNCT_1:def 3;
reconsider m19 as Element of NAT by A119;
A121: m19 in Seg len P2 by A119,FINSEQ_1:def 3;
then m19 <= len P2 by FINSEQ_1:1;
then
A122: m19+1 <= lenF by A21,A23,XREAL_1:6;
reconsider m2 = m19+1 as Nat;
1 <= m19 by A121,FINSEQ_1:1;
then
A123: 1+1 <= m19 + 1 by XREAL_1:6;
then 1 <= m2 by XXREAL_0:2;
then
A124: m2 in Seg lenF by A122,FINSEQ_1:1;
then
A125: F.m2 in rng F by A31,FUNCT_1:3;
ex k9 be Nat st k9 = m2 -1 & F.m2 = F1.(P2.k9) by A31,A123,A124;
hence thesis by A113,A116,A120,A125,TARSKI:def 4;
end;
end;
hence thesis;
end;
then union rng F1 c= union rng F;
then
A126: union rng F = dom f by A6,A112;
reconsider F as Finite_Sep_Sequence of S by A97,PROB_2:def 2;
take F,a;
for n be Nat st 2 <= n & n in dom a holds 0. < a.n & a.n < +infty
proof
A127: f is real-valued by A1,MESFUNC2:def 4;
0+1 <= lenF by A21,A23,XREAL_1:19;
then
A128: 1 in dom F by A31,FINSEQ_1:1;
let n be Nat;
assume that
A129: 2 <= n and
A130: n in dom a;
1 + 1 <= n by A129;
then
A131: 1 <= n-1 by XREAL_1:19;
consider k1 be Nat such that
A132: k1 = n-1 and
A133: F.n = F1.(P2.k1) by A31,A56,A129,A130;
n <= lenF by A31,A56,A130,FINSEQ_1:1;
then n-1 <= lenF -1 by XREAL_1:9;
then k1 in Seg len P2 by A21,A23,A132,A131,FINSEQ_1:1;
then k1 in dom P2 by FINSEQ_1:def 3;
then P2.k1 in M by A18,FUNCT_1:3;
then
A134: F.n in rng F1 by A133,FUNCT_1:3;
n <> 1 by A129;
then F.1 misses F.n by A56,A60,A130,A128;
then
A135: G1 misses F.n by A31,A128;
a.n <> 0. & 0. <= a.n & a.n < +infty
proof
per cases;
suppose
A136: F.n <> {};
A137: F.n in rng F by A56,A130,FUNCT_1:3;
then reconsider Fn = F.n as Element of S;
consider y be object such that
A138: y in F.n by A136,XBOOLE_0:def 1;
F.n in S by A137;
then reconsider y as Element of X by A138;
A139: a.n = f.y by A48,A130,A138;
G1 /\ F.n = {} by A135;
then
A140: not y in G1 by A138,XBOOLE_0:def 4;
thus a.n <> 0.
proof
assume a.n = 0.;
then for x be Element of X st x in F.n holds f.x = 0. by A56,A130;
then Fn in F0 by A134;
hence contradiction by A138,A140,TARSKI:def 4;
end;
A141: y in union rng F by A138,A137,TARSKI:def 4;
then |. f.y .| < +infty by A6,A112,A127,MESFUNC2:def 1;
hence thesis by A6,A112,A139,A141,EXTREAL1:21,a2;
end;
suppose
A142: F.n = {};
hence a.n <> 0. by A48,A130;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
thus 0. <= a.n by A48,A130,A142;
A[n,a.n] by A48,A130;
then a.n = jj by A142;
hence a.n < +infty by XXREAL_0:9;
end;
end;
hence thesis;
end;
hence thesis by A126,A56,A52;
end;
theorem Th14:
for X be non empty set, S be SigmaField of X, f be PartFunc of X
,ExtREAL st f is_simple_func_in S & f is nonnegative
holds ex F be Finite_Sep_Sequence of S, a be FinSequence of ExtREAL st F,a
are_Re-presentation_of f & a.1=0. & for n be Nat st 2 <= n & n in dom a holds
0. < a.n & a.n < +infty
proof
let X be non empty set;
let S be SigmaField of X;
let f be PartFunc of X,ExtREAL;
assume
A1: f is_simple_func_in S & f is nonnegative;
per cases;
suppose
ex x be object st x in dom f & 0. = f.x;
hence thesis by A1,Lm3;
end;
suppose
for x be object st x in dom f holds 0. <> f.x;
hence thesis by A1,Lm2;
end;
end;
theorem
for X be non empty set, S be SigmaField of X, f be PartFunc of X,
ExtREAL, F be Finite_Sep_Sequence of S, a be FinSequence of ExtREAL, x be
Element of X st F,a are_Re-presentation_of f & x in dom f holds ex ax be
FinSequence of ExtREAL st dom ax= dom a & (for n be Nat st n in dom ax holds ax
.n=a.n*(chi(F.n,X)).x) & f.x=Sum(ax)
proof
let X be non empty set;
let S be SigmaField of X;
let f be PartFunc of X,ExtREAL;
let F be Finite_Sep_Sequence of S;
let a be FinSequence of ExtREAL;
let x be Element of X such that
A1: F,a are_Re-presentation_of f and
A2: x in dom f;
A3: dom F = dom a by A1;
deffunc F(Nat) = a.$1*(chi(F.$1,X)).x;
consider ax be FinSequence of ExtREAL such that
A4: len ax = len a & for j be Nat st j in dom ax holds ax.j = F(j) from
FINSEQ_2:sch 1;
A5: dom ax = Seg len a by A4,FINSEQ_1:def 3;
A6: dom f = union rng F by A1;
A7: f.x = Sum(ax)
proof
consider Y be set such that
A8: x in Y and
A9: Y in rng F by A2,A6,TARSKI:def 4;
consider k be object such that
A10: k in dom F and
A11: Y = F.k by A9,FUNCT_1:def 3;
reconsider k as Element of NAT by A10;
A12: k in Seg len a by A3,A10,FINSEQ_1:def 3;
then
A13: len ax >= k by A4,FINSEQ_1:1;
A14: for i be Nat st i in Seg len ax & i <> k holds ax.i = 0.
proof
let i be Nat;
assume that
A15: i in Seg len ax and
A16: i <> k;
F.i misses F.k by A16,PROB_2:def 2;
then F.i /\ F.k = {};
then not x in F.i by A8,A11,XBOOLE_0:def 4;
then
A17: chi(F.i,X).x = 0. by FUNCT_3:def 3;
ax.i = a.i * (chi(F.i,X)).x by A4,A5,A15;
hence thesis by A17;
end;
consider SA be sequence of ExtREAL such that
A18: Sum(ax) = SA.(len ax) and
A19: SA.0 = 0. and
A20: for i be Nat st i < len ax holds SA.(i+1)=SA.i + ax.(i
+1 ) by EXTREAL1:def 2;
defpred P[Nat] means $1 <= len ax implies ($1 < k implies SA.$1 = 0.) & (
$1 >= k implies SA.$1 = f.x);
A21: for i be Nat st i in Seg len ax & i = k holds ax.i = f.x
proof
let i be Nat;
assume that
A22: i in Seg len ax and
A23: i = k;
chi(F.i,X).x = 1. by A8,A11,A23,FUNCT_3:def 3;
then ax.i = a.i * 1. by A4,A5,A22
.= a.i by XXREAL_3:81;
hence thesis by A1,A8,A10,A11,A23;
end;
A24: for i be Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume
A25: P[i];
assume
A26: i+1 <= len ax;
reconsider i as Element of NAT by ORDINAL1:def 12;
now
per cases;
case
A27: i+1 < k;
A28: k <= len a by A12,FINSEQ_1:1;
A29: i <= i+1 by NAT_1:11;
then i < k by A27,XXREAL_0:2;
then
A30: i < len ax by A4,A28,XXREAL_0:2;
then 1 <= i+1 & i+1 <= len ax by NAT_1:11,13;
then
A31: i+1 in Seg len ax by FINSEQ_1:1;
SA.(i+1) = 0. + ax.(i+1) by A20,A25,A27,A29,A30,XXREAL_0:2
.= ax.(i+1) by XXREAL_3:4
.= 0. by A14,A27,A31;
hence thesis by A27;
end;
case
A32: i+1 >= k;
now
per cases;
case
A33: k = i+1;
A34: k <= len a by A12,FINSEQ_1:1;
then i < len ax by A4,A33,NAT_1:13;
hence SA.(i+1) = SA.i + ax.(i+1) by A20
.= ax.k by A4,A25,A33,A34,NAT_1:13,XXREAL_3:4
.= f.x by A4,A12,A21;
end;
case
k <> i+1;
then
A35: k < i+1 by A32,XXREAL_0:1;
1 <= i+1 by NAT_1:11;
then
A36: i+1 in Seg len ax by A26,FINSEQ_1:1;
i < len ax by A26,NAT_1:13;
hence SA.(i+1) = SA.i + ax.(i+1) by A20
.= f.x + 0. by A14,A25,A26,A35,A36,NAT_1:13
.= f.x by XXREAL_3:4;
end;
end;
hence thesis by A32;
end;
end;
hence thesis;
end;
A37: P[0] by A12,A19,FINSEQ_1:1;
for i be Nat holds P[i] from NAT_1:sch 2(A37,A24);
hence thesis by A18,A13;
end;
take ax;
dom ax = Seg len a by A4,FINSEQ_1:def 3;
hence thesis by A4,A7,FINSEQ_1:def 3;
end;
theorem
for p be FinSequence of ExtREAL, q be FinSequence of REAL st p=q holds
Sum(p) = Sum(q) by Th2;
theorem Th17:
for p be FinSequence of ExtREAL st not -infty in rng p & +infty in rng p
holds Sum(p) = +infty
proof
let p be FinSequence of ExtREAL;
assume
A1: not -infty in rng p;
assume +infty in rng p;
then ex n be object st n in dom p & p.n=+infty by FUNCT_1:def 3;
then consider m be Nat such that
A2: m in dom p and
A3: p.m = +infty;
m in Seg len p by A2,FINSEQ_1:def 3;
then
A4: len p >= m by FINSEQ_1:1;
consider f be sequence of ExtREAL such that
A5: Sum(p) = f.(len p) and
A6: f.0 = 0. and
A7: for i be Nat st i < len p holds f.(i+1)=f.i + p.(i+1)
by EXTREAL1:def 2;
A8: for n be Nat st n in dom p holds -infty < p.n
proof
let n be Nat;
assume n in dom p;
then p.n in rng p by FUNCT_1:def 3;
hence thesis by A1,XXREAL_0:6;
end;
defpred P[Nat] means $1 <= len p implies
($1 < m implies -infty < f.$1) & ($1 >= m implies f.$1 = +infty);
A9: for i be Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume
A10: P[i];
assume
A11: i+1 <= len p;
reconsider i as Element of NAT by ORDINAL1:def 12;
A12: i < len p by A11,NAT_1:13;
now
per cases;
case i+1 < m;
1 <= i+1 by NAT_1:11;
then i+1 in Seg len p by A11,FINSEQ_1:1;
then i+1 in dom p by FINSEQ_1:def 3;
then
A13: -infty < p.(i+1) by A8;
A14: -infty + -infty = -infty by XXREAL_3:def 2;
-infty + -infty < f.i + p.(i+1) by A10,A11,A13,NAT_1:13,XXREAL_3:64;
hence -infty < f.(i+1) by A7,A12,A14;
end;
case
A15: i+1 >= m;
now
per cases;
case
A16: i+1 = m;
f.(i+1) = f.i + p.(i+1) by A7,A12;
hence f.(i+1) = +infty by A3,A10,A11,A16,NAT_1:13,XXREAL_3:def 2;
end;
case
A17: i+1 <> m;
i < len p by A11,NAT_1:13;
then
A18: f.(i+1) = f.i + p.(i+1) by A7;
1 <= i+1 by NAT_1:11;
then i+1 in Seg len p by A11,FINSEQ_1:1;
then i+1 in dom p by FINSEQ_1:def 3;
then
A19: p.(i+1) <> -infty by A8;
i+1 > m by A15,A17,XXREAL_0:1;
hence f.(i+1) = +infty by A10,A11,A19,A18,NAT_1:13,XXREAL_3:def 2;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
A20: P[0] by A2,A6,FINSEQ_3:25;
for i be Nat holds P[i] from NAT_1:sch 2(A20,A9);
hence thesis by A5,A4;
end;
definition
let X be non empty set;
let S be SigmaField of X;
let M be sigma_Measure of S;
let f be PartFunc of X,ExtREAL;
assume
A1: f is_simple_func_in S & f is nonnegative;
func integral(M,f) -> Element of ExtREAL means
ex F be Finite_Sep_Sequence of S, a, x be FinSequence of ExtREAL st F,a
are_Re-presentation_of f & a.1 =0. & (for n be Nat st 2 <= n & n in dom a holds
0. < a.n & a.n < +infty ) & dom x = dom F & (for n be Nat st n in dom x holds x
.n=a.n*(M*F).n) & it=Sum(x);
existence
proof
consider F be Finite_Sep_Sequence of S, a be FinSequence of ExtREAL such
that
A2: F,a are_Re-presentation_of f & a.1 =0. & for n be Nat st 2 <= n &
n in dom a holds 0. < a.n & a.n < +infty by A1,Th14;
defpred P[object] means $1 in dom F;
deffunc G(object) = (a.$1)*((M*F).$1);
A3: for x be object st P[x] holds G(x) in ExtREAL by XXREAL_0:def 1;
consider p be PartFunc of NAT,ExtREAL such that
A4: (for x be object holds x in dom p iff x in NAT & P[x]) &
for x be object
st x in dom p holds p.x = G(x) from PARTFUN1:sch 3(A3);
for x be object st x in dom F holds x in dom p by A4;
then
A5: dom F c= dom p;
for x be object st x in dom p holds x in dom F by A4;
then dom p c= dom F;
then
A6: dom p = dom F by A5;
then dom p = Seg len F by FINSEQ_1:def 3;
then
A7: p is FinSequence by FINSEQ_1:def 2;
rng p c= ExtREAL;
then reconsider p as FinSequence of ExtREAL by A7,FINSEQ_1:def 4;
take Sum(p);
for n be Nat st n in dom p holds p.n=a.n*(M*F).n by A4;
hence thesis by A2,A6;
end;
uniqueness
proof
let s1,s2 be Element of ExtREAL such that
A8: ex F1 be Finite_Sep_Sequence of S, a1, x1 be FinSequence of
ExtREAL st F1,a1 are_Re-presentation_of f & a1.1 =0. & (for n be Nat st 2 <= n
& n in dom a1 holds 0. < a1.n & a1.n < +infty) & dom x1 = dom F1 & (for n be
Nat st n in dom x1 holds x1.n=a1.n*(M*F1).n) & s1=Sum(x1) and
A9: ex F2 be Finite_Sep_Sequence of S, a2 be FinSequence of ExtREAL,
x2 be FinSequence of ExtREAL st F2,a2 are_Re-presentation_of f & a2.1 =0. & (
for n be Nat st 2 <= n & n in dom a2 holds 0. < a2.n & a2.n < +infty) & dom x2
= dom F2 & (for n be Nat st n in dom x2 holds x2.n=a2.n*(M*F2).n) & s2=Sum(x2);
thus s1=s2
proof
consider F2 be Finite_Sep_Sequence of S, a2 be FinSequence of ExtREAL,
x2 be FinSequence of ExtREAL such that
A10: F2,a2 are_Re-presentation_of f and
A11: a2.1 =0. and
A12: for n be Nat st 2 <= n & n in dom a2 holds 0. < a2.n & a2.n < +infty and
A13: dom x2 = dom F2 and
A14: for n be Nat st n in dom x2 holds x2.n=a2.n*(M*F2).n and
A15: s2=Sum(x2) by A9;
A16: dom F2 = dom a2 by A10;
A17: for n be Nat st n in dom a2 holds 0. <= a2.n
proof
let n be Nat;
assume
A18: n in dom a2;
now
per cases;
case
n=1;
thus a2.1=0. by A11;
end;
case
A19: n<>1;
n in Seg len a2 by A18,FINSEQ_1:def 3;
then 1 <=n by FINSEQ_1:1;
then 1 < n by A19,XXREAL_0:1;
then 1+1 < n+1 by XREAL_1:8;
then 2<=n by NAT_1:13;
hence thesis by A12,A18;
end;
end;
hence thesis;
end;
A20: for n be Nat st n in dom F2 holds 0. <= (M*F2).n
proof
let n be Nat;
assume n in dom F2;
then (M*F2).n=M.(F2.n) & F2.n in rng F2 by FUNCT_1:3,13;
hence thesis by SUPINF_2:39;
end;
A21: not -infty in rng x2
proof
assume not thesis;
then consider n being object such that
A22: n in dom x2 and
A23: x2.n = -infty by FUNCT_1:def 3;
reconsider n as set by TARSKI:1;
0. <= a2.n & 0. <= (M*F2).n by A13,A16,A20,A17,A22;
then 0. <= (a2.n)*( (M*F2).n);
hence thesis by A14,A22,A23;
end;
consider F1 be Finite_Sep_Sequence of S, a1 be FinSequence of ExtREAL,
x1 be FinSequence of ExtREAL such that
A24: F1,a1 are_Re-presentation_of f and
A25: a1.1 =0. and
A26: for n be Nat st 2 <= n & n in dom a1 holds 0. < a1.n & a1.n < +infty and
A27: dom x1 = dom F1 and
A28: for n be Nat st n in dom x1 holds x1.n=a1.n*(M*F1).n and
A29: s1=Sum(x1) by A8;
A30: dom F1 = dom a1 by A24;
A31: for n be Nat st n in dom a1 holds 0. <= a1.n
proof
let n be Nat;
assume
A32: n in dom a1;
now
per cases;
case
n=1;
thus a1.1=0. by A25;
end;
case
A33: n<>1;
n in Seg len a1 by A32,FINSEQ_1:def 3;
then 1 <= n by FINSEQ_1:1;
then 1 < n by A33,XXREAL_0:1;
then 1+1 < n+1 by XREAL_1:8;
then 2<=n by NAT_1:13;
hence thesis by A26,A32;
end;
end;
hence thesis;
end;
A34: for n be Nat st n in dom F1 holds 0. <= (M*F1).n
proof
let n be Nat;
assume n in dom F1;
then (M*F1).n=M.(F1.n) & F1.n in rng F1 by FUNCT_1:3,13;
hence thesis by SUPINF_2:39;
end;
A35: not -infty in rng x1
proof
assume not thesis;
then consider n being object such that
A36: n in dom x1 and
A37: x1.n = -infty by FUNCT_1:def 3;
reconsider n as set by TARSKI:1;
0. <= a1.n & 0. <= (M*F1).n by A27,A30,A34,A31,A36;
then 0. <= (a1.n)*( (M*F1).n);
hence thesis by A28,A36,A37;
end;
now
per cases;
case
ex i,j be Nat st i in dom F1 & j in dom F2 &2<= i & 2<=j &
M.(F1.i /\ F2.j)=+infty;
then consider i,j be Nat such that
A38: i in dom F1 and
A39: j in dom F2 and
A40: 2<= i and
A41: 2<=j and
A42: M.(F1.i /\ F2.j)=+infty;
A43: F2.j in rng F2 by A39,FUNCT_1:3;
A44: F1.i in rng F1 by A38,FUNCT_1:3;
then
A45: F1.i /\ F2.j in S by A43,MEASURE1:34;
F1.i /\ F2.j c= F1.i by XBOOLE_1:17;
then M.(F1.i)= +infty by A42,A44,A45,MEASURE1:31,XXREAL_0:4;
then
A46: (M*F1).i = +infty by A38,FUNCT_1:13;
0. < a1.i by A26,A30,A38,A40;
then +infty = ( a1.i)*((M*F1).i) by A46,XXREAL_3:def 5;
then x1.i=+infty by A27,A28,A38;
then +infty in rng x1 by A27,A38,FUNCT_1:def 3;
then
A47: Sum(x1)=+infty by A35,Th17;
F1.i /\ F2.j c= F2.j by XBOOLE_1:17;
then M.(F2.j)= +infty by A42,A43,A45,MEASURE1:31,XXREAL_0:4;
then
A48: (M*F2).j = +infty by A39,FUNCT_1:13;
0. < a2.j by A12,A16,A39,A41;
then +infty = (a2.j)*((M*F2).j) by A48,XXREAL_3:def 5;
then x2.j=+infty by A13,A14,A39;
then +infty in rng x2 by A13,A39,FUNCT_1:def 3;
hence thesis by A29,A15,A21,A47,Th17;
end;
case
A49: for i,j be Nat st i in dom F1 & j in dom F2 & 2<= i & 2<=j
holds M.(F1.i /\ F2.j) <> +infty;
set m= len x2;
set n= len x1;
ex a be Function of [:(Seg n),(Seg m) :],REAL st for i,j be Nat
st i in Seg n & j in Seg m holds a.(i,j) = a1.i * (M.(F1.i /\ F2.j))
proof
deffunc F(object,object) = a1.$1 * (M.(F1.$1 /\ F2.$2));
A50: for x,y be object st x in Seg n & y in Seg m holds F(x,y) in REAL
proof
let x,y be object such that
A51: x in Seg n and
A52: y in Seg m;
x in { k where k is Nat : 1 <= k & k <= n } by A51,FINSEQ_1:def 1
;
then consider kx be Nat such that
A53: x=kx and
A54: 1 <= kx and
kx <= n;
y in { k where k is Nat : 1 <= k & k <= m } by A52,FINSEQ_1:def 1
;
then consider ky be Nat such that
A55: y=ky and
A56: 1 <= ky and
ky <= m;
A57: ky in dom F2 by A13,A52,A55,FINSEQ_1:def 3;
then
A58: F2.ky in rng F2 by FUNCT_1:3;
A59: kx in dom F1 by A27,A51,A53,FINSEQ_1:def 3;
then F1.kx in rng F1 by FUNCT_1:3;
then
A60: F1.kx /\ F2.ky in S by A58,MEASURE1:34;
now
per cases;
case
A61: not (2 <= kx & 2 <= ky);
now
per cases by A61;
case
A62: kx < 2;
then kx <=1+1;
then kx <= 1 by A62,NAT_1:8;
then F(kx,ky) = 0. * (M.(F1.kx /\ F2.ky)) by A25,A54,
XXREAL_0:1
.=0;
hence F(kx,ky) in REAL by XREAL_0:def 1;
end;
case
A63: ky < 2;
then ky <=1+1;
then
A64: ky <= 1 by A63,NAT_1:8;
now
per cases;
case
F1.kx /\ F2.ky = {};
hence F(kx,ky) = a1.kx * 0. by VALUED_0:def 19
.=0;
end;
case
F1.kx /\ F2.ky <> {};
then consider x be object such that
A65: x in F1.kx /\ F2.ky by XBOOLE_0:def 1;
A66: x in F2.ky by A65,XBOOLE_0:def 4;
x in F1.kx by A65,XBOOLE_0:def 4;
then a1.kx=f.x by A24,A59
.=a2.ky by A10,A57,A66
.=0. by A11,A56,A64,XXREAL_0:1;
hence F(kx,ky) = 0;
end;
end;
hence F(kx,ky) in REAL by XREAL_0:def 1;
end;
end;
hence F(kx,ky) in REAL;
end;
case
A67: 2 <= kx & 2 <= ky;
A68: 0. <= a1.kx by A30,A31,A59;
a1.kx <> +infty by A26,A30,A59,A67;
then reconsider r2=a1.kx as Element of REAL
by A68,XXREAL_0:14;
0. <= M.(F1.kx /\ F2.ky) by A60,SUPINF_2:39;
then reconsider
r3=M.(F1.kx /\ F2.ky) as Element of REAL
by A49,A59,A57,A67,XXREAL_0:14;
a1.kx*M.(F1.kx /\ F2.ky) = r2*r3 by EXTREAL1:1;
hence F(kx,ky) in REAL by XREAL_0:def 1;
end;
end;
hence thesis by A53,A55;
end;
consider f being Function of [:(Seg n),(Seg m) :],REAL such that
A69: for x,y be object st x in Seg n & y in Seg m holds f.(x,y)=
F(x,y) from BINOP_1:sch 2(A50);
take f;
thus thesis by A69;
end;
then consider a be Function of [:(Seg n),(Seg m) :],REAL such that
A70: for i,j be Nat st i in Seg n & j in Seg m holds a.(i,j) =
a1.i * (M.(F1.i /\ F2.j));
ex p be FinSequence of REAL st dom p=Seg n & for i be Nat st i
in dom p holds ex r be FinSequence of REAL st (dom r = Seg m & p.i=Sum(r) & for
j be Nat st j in dom(r) holds r.j=a.[i,j] )
proof
defpred P[Nat,object] means
ex r be FinSequence of REAL st dom(r) =
Seg m & $2=Sum(r) & for j be Nat st j in dom(r) holds r.j=a.[$1,j];
A71: for k be Nat st k in Seg n ex x be object st P[k,x]
proof
let k be Nat;
assume k in Seg n;
deffunc G(set)= a.[k,$1];
consider r being FinSequence such that
A72: len r = m and
A73: for i be Nat st i in dom r holds r.i=G(i) from
FINSEQ_1:sch 2;
A74: dom(r) = Seg m by A72,FINSEQ_1:def 3;
for i be Nat st i in dom r holds r.i in REAL
proof
let i be Nat;
A75: a.[k,i] in REAL by XREAL_0:def 1;
assume i in dom r;
hence thesis by A73,A75;
end;
then reconsider r as FinSequence of REAL by FINSEQ_2:12;
take x=Sum(r);
thus thesis by A73,A74;
end;
consider p be FinSequence such that
A76: dom p = Seg n & for k be Nat st k in Seg n holds P[k,p.k
] from FINSEQ_1:sch 1(A71);
for i be Nat st i in dom p holds p.i in REAL
proof
let i be Nat;
assume i in dom p;
then ex r be FinSequence of REAL st dom(r) = Seg m & p.i=Sum( r)
& for j be Nat st j in dom(r) holds r.j=a.[i,j] by A76;
hence thesis by XREAL_0:def 1;
end;
then reconsider p as FinSequence of REAL by FINSEQ_2:12;
take p;
thus thesis by A76;
end;
then consider p be FinSequence of REAL such that
A77: dom p=Seg n and
A78: for i be Nat st i in dom p holds ex r be FinSequence of
REAL st ( dom r = Seg m & p.i=Sum r & for j be Nat st j in dom r holds r.j=a.[i
,j]);
A79: dom p = dom x1 by A77,FINSEQ_1:def 3;
for k be Nat st k in dom p holds p.k = x1.k
proof
let k be Nat;
assume
A80: k in dom p;
then consider r be FinSequence of REAL such that
A81: dom r = Seg m and
A82: p.k=Sum r and
A83: for j be Nat st j in dom r holds r.j=a.[k,j] by A78;
ex F11 be Finite_Sep_Sequence of S st union rng F11 = F1.k &
dom F11=dom r & for j be Nat st j in dom r holds F11.j=F1.k /\ F2.j
proof
deffunc G(set)=F1.k /\ F2.$1;
consider F being FinSequence such that
A84: len F = m and
A85: for i be Nat st i in dom F holds F.i=G(i) from
FINSEQ_1:sch 2;
A86: dom F = Seg m by A84,FINSEQ_1:def 3;
A87: for i be Nat st i in dom F holds F.i in S
proof
let i be Nat;
assume
A88: i in dom F;
then i in Seg m by A84,FINSEQ_1:def 3;
then i in dom F2 by A13,FINSEQ_1:def 3;
then
A89: F2.i in rng F2 by FUNCT_1:3;
F1.k in rng F1 by A27,A79,A80,FUNCT_1:3;
then F1.k /\ F2.i in S by A89,MEASURE1:34;
hence thesis by A85,A88;
end;
A90: dom F = Seg m by A84,FINSEQ_1:def 3;
reconsider F as FinSequence of S by A87,FINSEQ_2:12;
A91: dom F = dom F2 by A13,A90,FINSEQ_1:def 3;
then reconsider F as Finite_Sep_Sequence of S by A85,Th5;
take F;
union rng F = F1.k /\ union rng F2 by A85,A91,Th6
.= F1.k /\ dom f by A10
.= F1.k /\ union rng F1 by A24
.= F1.k by A27,A79,A80,Th7;
hence thesis by A81,A85,A86;
end;
then consider F11 be Finite_Sep_Sequence of S such that
A92: union rng F11 = F1.k and
A93: dom F11=dom r and
A94: for j be Nat st j in dom r holds F11.j=F1.k /\ F2.j;
A95: Sum(M*F11) = M.((F1.k)) by A92,Th9;
k in Seg len a1 by A27,A30,A79,A80,FINSEQ_1:def 3;
then
A96: 1 <= k by FINSEQ_1:1;
a1.k <> -infty & a1.k <> +infty
proof
per cases;
suppose
k = 1;
hence thesis by A25;
end;
suppose
k <> 1;
then 1 < k by A96,XXREAL_0:1;
then 1+1 <= k by NAT_1:13;
hence thesis by A26,A27,A30,A79,A80;
end;
end;
then
A97: a1.k is Element of REAL by XXREAL_0:14;
reconsider rr=r as FinSequence of ExtREAL by Th11;
A98: for j be Nat st j in dom r holds r.j=a1.k * (M.(F1.k /\ F2.j ))
proof
let j be Nat;
assume
A99: j in dom r;
hence r.j=a.(k,j) by A83
.=a1.k * (M.(F1.k /\ F2.j)) by A70,A77,A80,A81,A99;
end;
A100: for j be Nat st j in dom rr holds rr.j=a1.k * (M*F11).j
proof
let j be Nat;
assume
A101: j in dom rr;
hence rr.j = a1.k * (M.(F1.k /\ F2.j)) by A98
.=a1.k *(M.(F11.j)) by A94,A101
.=a1.k *(M*F11).j by A93,A101,FUNCT_1:13;
end;
dom rr = dom (M*F11) by A93,Th8;
then Sum rr=(a1.k)*Sum(M*F11) by A100,A97,Th10;
then Sum r=(a1.k)*M.((F1.k)) by A95,Th2
.=a1.k*((M*F1).k) by A27,A79,A80,FUNCT_1:13;
hence thesis by A28,A79,A80,A82;
end;
then
A102: Sum p = Sum x1 by A79,Th2,FINSEQ_1:13;
ex q be FinSequence of REAL st dom q=Seg m & for j be Nat st j
in dom q holds ex s be FinSequence of REAL st (dom s = Seg n & q.j=Sum s & for
i be Nat st i in dom s holds s.i=a.[i,j] )
proof
defpred P[Nat,object] means
ex s be FinSequence of REAL st dom(s) =
Seg n & $2=Sum(s) & for i be Nat st i in dom(s) holds s.i=a.[i,$1];
A103: for k be Nat st k in Seg m ex x be object st P[k,x]
proof
let k be Nat;
assume k in Seg m;
deffunc G(set)= a.[$1,k];
consider s being FinSequence such that
A104: len s = n and
A105: for i be Nat st i in dom s holds s.i=G(i) from
FINSEQ_1:sch 2;
A106: dom(s) = Seg n by A104,FINSEQ_1:def 3;
for i be Nat st i in dom s holds s.i in REAL
proof
let i be Nat;
A107: a.[i,k] in REAL by XREAL_0:def 1;
assume i in dom s;
hence thesis by A105,A107;
end;
then reconsider s as FinSequence of REAL by FINSEQ_2:12;
take x=Sum(s);
thus thesis by A105,A106;
end;
consider p be FinSequence such that
A108: dom p = Seg m & for k be Nat st k in Seg m holds P[k,p.k
] from FINSEQ_1:sch 1(A103);
for i be Nat st i in dom p holds p.i in REAL
proof
let i be Nat;
assume i in dom p;
then ex s be FinSequence of REAL st dom(s) = Seg n & p.i=Sum( s)
& for j be Nat st j in dom(s) holds s.j=a.[j,i] by A108;
hence thesis by XREAL_0:def 1;
end;
then reconsider p as FinSequence of REAL by FINSEQ_2:12;
take p;
thus thesis by A108;
end;
then consider q be FinSequence of REAL such that
A109: dom q=Seg m and
A110: for j be Nat st j in dom q holds ex s be FinSequence of
REAL st ( dom(s) = Seg n & q.j=Sum(s) & for i be Nat st i in dom(s) holds s.i=a
.[i,j]);
A111: dom q = dom x2 by A109,FINSEQ_1:def 3;
A112: for k be Nat st k in dom q holds q.k = x2.k
proof
let k be Nat;
assume
A113: k in dom q;
then consider s be FinSequence of REAL such that
A114: dom s = Seg n and
A115: q.k=Sum s and
A116: for i be Nat st i in dom s holds s.i=a.[i,k] by A110;
reconsider ss=s as FinSequence of ExtREAL by Th11;
ex F21 be Finite_Sep_Sequence of S st union rng F21 = F2.k &
dom F21=dom(s) & for j be Nat st j in dom(s) holds F21.j=F1.j /\ F2.k
proof
deffunc G(set)= F2.k /\ F1.$1;
consider F being FinSequence such that
A117: len F = n and
A118: for i be Nat st i in dom F holds F.i=G(i) from
FINSEQ_1:sch 2;
A119: dom F = Seg n by A117,FINSEQ_1:def 3;
A120: for i be Nat st i in dom F holds F.i in S
proof
let i be Nat;
assume
A121: i in dom F;
then i in Seg n by A117,FINSEQ_1:def 3;
then i in dom F1 by A27,FINSEQ_1:def 3;
then
A122: F1.i in rng F1 by FUNCT_1:3;
F2.k in rng F2 by A13,A111,A113,FUNCT_1:3;
then F1.i /\ F2.k in S by A122,MEASURE1:34;
hence thesis by A118,A121;
end;
A123: dom F = Seg n by A117,FINSEQ_1:def 3;
reconsider F as FinSequence of S by A120,FINSEQ_2:12;
A124: dom F = dom F1 by A27,A123,FINSEQ_1:def 3;
then reconsider F as Finite_Sep_Sequence of S by A118,Th5;
take F;
union rng F = F2.k /\ union rng F1 by A118,A124,Th6
.= F2.k /\ dom f by A24
.= F2.k /\ union rng F2 by A10
.= F2.k by A13,A111,A113,Th7;
hence thesis by A114,A118,A119;
end;
then consider F21 be Finite_Sep_Sequence of S such that
A125: union rng F21 = F2.k and
A126: dom F21 = dom s and
A127: for i be Nat st i in dom s holds F21.i=F1.i /\ F2.k;
A128: Sum(M*F21) = M.((F2.k)) by A125,Th9;
A129: for i be Nat st i in dom s holds s.i=a1.i * (M.(F1.i /\ F2.k ))
proof
let i be Nat;
assume
A130: i in dom s;
hence s.i=a.(i,k) by A116
.=a1.i * (M.(F1.i /\ F2.k)) by A70,A109,A113,A114,A130;
end;
A131: for i be Nat st i in dom s holds s.i=a2.k * (M.(F1.i /\ F2.k ))
proof
let i be Nat;
assume
A132: i in dom s;
now
per cases;
case
A133: F1.i /\ F2.k = {};
then M.(F1.i /\ F2.k)=0. by VALUED_0:def 19;
hence s.i = a1.i * 0. by A129,A132
.=0.
.=a2.k *0.
.=a2.k *M.(F1.i /\ F2.k) by A133,VALUED_0:def 19;
end;
case
F1.i /\ F2.k <> {};
then consider x be object such that
A134: x in F1.i /\ F2.k by XBOOLE_0:def 1;
A135: x in F2.k by A134,XBOOLE_0:def 4;
A136: dom p = dom x1 by A77,FINSEQ_1:def 3;
x in F1.i by A134,XBOOLE_0:def 4;
then a1.i=f.x by A24,A27,A77,A114,A132,A136
.=a2.k by A10,A13,A111,A113,A135;
hence thesis by A129,A132;
end;
end;
hence thesis;
end;
A137: for j be Nat st j in dom ss holds ss.j=a2.k * (M*F21).j
proof
let j be Nat;
assume
A138: j in dom ss;
hence ss.j = a2.k * (M.(F1.j /\ F2.k)) by A131
.=a2.k *(M.(F21.j)) by A127,A138
.=a2.k *(M*F21).j by A126,A138,FUNCT_1:13;
end;
k in Seg len a2 by A13,A16,A111,A113,FINSEQ_1:def 3;
then
A139: 1 <= k by FINSEQ_1:1;
a2.k <> -infty & a2.k <> +infty
proof
per cases;
suppose
k = 1;
hence thesis by A11;
end;
suppose
k <> 1;
then 1 < k by A139,XXREAL_0:1;
then 1+1 <= k by NAT_1:13;
hence thesis by A12,A13,A16,A111,A113;
end;
end;
then
A140: a2.k is Element of REAL by XXREAL_0:14;
dom ss=dom (M*F21) by A126,Th8;
then Sum(ss)=(a2.k)*Sum(M*F21) by A137,A140,Th10;
then Sum(s)=(a2.k)*M.((F2.k)) by A128,Th2
.=a2.k*((M*F2).k) by A13,A111,A113,FUNCT_1:13;
hence thesis by A14,A111,A113,A115;
end;
Sum(p)=Sum(q) by A77,A78,A109,A110,Th1;
hence thesis by A29,A15,A102,A111,A112,Th2,FINSEQ_1:13;
end;
end;
hence thesis;
end;
end;
end;
begin :: Additional Lemma
theorem
for a be FinSequence of ExtREAL, p,N be Element of ExtREAL st N = len a &
(for n be Nat st n in dom a holds a.n = p) holds Sum(a) = N * p by Lm1;