:: Construction of Measure from Semialgebra of Sets
:: by Noboru Endou
::
:: Received August 14, 2015
:: Copyright (c) 2015-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, SUBSET_1, CARD_3, FUNCT_1, RELAT_1, FINSEQ_1, XBOOLE_0,
ARYTM_3, ARYTM_1, XXREAL_0, CARD_1, TARSKI, NAT_1, ZFMISC_1, ORDINAL4,
PROB_1, FINSUB_1, SETFAM_1, PROB_2, MEASURE9, MSSUBFAM, FUNCOP_1,
SUPINF_2, VALUED_0, PARTFUN1, MEASURE1, ORDINAL2, SERIES_1, MESFUNC5,
SUPINF_1, MEASURE4, SEQ_2, MATRIX_1, QC_LANG1, MATRIXC1, ORDINAL1,
PRE_POLY, TREES_1, FINSEQ_3, INCSP_1, FINSEQ_2, XREAL_0, MEASURE8,
REAL_1, XCMPLX_0, COMPLEX1, DBLSEQ_1, DBLSEQ_2, MESFUNC9, RFINSEQ,
SIMPLEX0, ASYMPT_1, SRINGS_3, DBLSEQ_3, LATTICE5;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSUB_1, CARD_3,
NUMBERS, XXREAL_3, BINOP_1, XTUPLE_0, PROB_1, XCMPLX_0, XREAL_0,
XXREAL_0, SIMPLEX0, NAT_1, VALUED_0, SUPINF_1, SEQ_1, MEASURE8, FINSEQ_1,
FINSEQ_2, FINSEQOP, SUPINF_2, PROB_2, MEASURE1, MEASURE4, MESFUNC1,
MESFUNC5, MESFUNC9, MATRIX_0, SEQ_2, SERIES_1, RVSUM_1, RFINSEQ,
WSIERP_1, MATRLIN, EXTREAL1, SRINGS_3, DBLSEQ_3;
constructors PROB_2, EXTREAL1, SUPINF_1, MESFUNC9, RINFSUP2, FINSEQOP,
MATRPROB, MATRLIN, MEASURE6, SEQ_1, MEASURE8, SERIES_1, WSIERP_1,
COMSEQ_2, RFINSEQ, SRINGS_3, DBLSEQ_3;
registrations XREAL_0, MEMBERED, FUNCT_1, XBOOLE_0, FINSEQ_1, RELAT_1,
SUBSET_1, XXREAL_0, ROUGHS_1, NUMBERS, VALUED_0, FUNCT_2, ORDINAL1,
RELSET_1, FINSUB_1, MEASURE1, MESFUNC5, MATRLIN, NAT_1, XXREAL_3, CARD_1,
PBOOLE, SIMPLEX0, SEQ_2, SEQ_1, SETFAM_1, NUMPOLY1, SRINGS_3, DBLSEQ_3;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities FINSEQ_1, XXREAL_3, BINOP_1, SRINGS_3;
expansions FINSEQ_1, SETFAM_1, PARTFUN1;
theorems TARSKI, XBOOLE_0, XREAL_0, FINSEQ_1, NAT_1, FUNCT_1, CARD_3,
XXREAL_0, ZFMISC_1, FINSEQ_3, XBOOLE_1, PROB_2, XREAL_1, PROB_1,
FINSUB_1, SETFAM_1, FUNCOP_1, XXREAL_3, MEASURE1, VALUED_0, FUNCT_2,
MEASURE7, RELAT_1, MESFUNC5, EXTREAL1, MESFUNC9, FINSEQ_2, PARTFUN1,
ORDINAL1, RINFSUP2, MEASURE8, MESFUNC3, RFINSEQ, PRE_POLY, MATRLIN,
RVSUM_1, MESFUNC1, MATRPROB, ORDERS_1, SERIES_1, SUPINF_2, VALUED_1,
MATRIX_0, ROUGHS_1, FINSEQOP, SEQM_3, XTUPLE_0, SRINGS_3, FINSEQ_5,
SEQ_1, DBLSEQ_3;
schemes FINSEQ_1, NAT_1, FUNCT_2, MATRIX_0, FINSEQ_2, BINOP_1;
begin :: Join of many finite sequence
theorem Th52:
for K be Relation st rng K is empty-membered holds
union rng K = {}
proof
let K be Relation;
assume A2: rng K is empty-membered;
now let x be object;
assume x in union rng K; then
ex A be set st x in A & A in rng K by TARSKI:def 4;
hence x in {} by A2;
end; then
union rng K c= {} by TARSKI:def 3;
hence union rng K = {};
end;
theorem
for K be Function holds
rng K is empty-membered iff (for x be object holds K.x = {})
proof
let K be Function;
hereby assume A1: rng K is empty-membered;
let x be object;
per cases;
suppose x in dom K;
hence K.x = {} by A1,FUNCT_1:3;
end;
suppose not x in dom K;
hence K.x = {} by FUNCT_1:def 2;
end;
end;
assume A2: for x be object holds K.x = {};
now assume ex y be non empty set st y in rng K; then
consider y be non empty set such that
A3: y in rng K;
ex a be object st a in dom K & y = K.a by A3,FUNCT_1:def 3;
hence contradiction by A2;
end;
hence rng K is empty-membered;
end;
definition
let D be set, F be FinSequenceSet of D,
f be FinSequence of F, n be Nat;
redefine func f.n -> FinSequence of D; :: redefines . (FUNCT_1, definition)
correctness
proof
per cases;
suppose n in dom f; then
f.n in rng f by FUNCT_1:3;
hence f.n is FinSequence of D by FINSEQ_2:def 3;
end;
suppose not n in dom f; then
f.n = <*>D by FUNCT_1:def 2;
hence f.n is FinSequence of D;
end;
end;
end;
definition
let D be set, Y be FinSequenceSet of D, F be FinSequence of Y;
func Length F -> FinSequence of NAT means :Def1:
dom it = dom F & for n be Nat st n in dom it holds it.n = len(F.n);
existence
proof
defpred P[Nat,object] means $2 = len(F.$1);
A1:for k be Nat st k in Seg len F
ex x be Element of NAT st P[k,x];
consider IT be FinSequence of NAT such that
A2: dom IT = Seg len F
& for k be Nat st k in Seg len F holds P[k,IT.k] from FINSEQ_1:sch 5(A1);
take IT;
thus dom IT = dom F by A2,FINSEQ_1:def 3;
thus for n be Nat st n in dom IT holds IT.n = len(F.n) by A2;
end;
uniqueness
proof
let IT1,IT2 be FinSequence of NAT;
assume that
A1: dom IT1 = dom F &
for n be Nat st n in dom IT1 holds IT1.n = len(F.n) and
A2: dom IT2 = dom F &
for n be Nat st n in dom IT2 holds IT2.n = len(F.n);
A3:len IT1 = len IT2 by A1,A2,FINSEQ_3:29;
now let k be Nat;
assume k in dom IT1; then
IT1.k = len(F.k) & IT2.k = len(F.k) by A1,A2;
hence IT1.k = IT2.k;
end;
hence IT1 = IT2 by A3,FINSEQ_2:9;
end;
end;
theorem
for D be set, Y be FinSequenceSet of D, F be FinSequence of Y
st (for n be Nat st n in dom F holds F.n = <*>D) holds Sum Length F = 0
proof
let D be set, Y be FinSequenceSet of D, F be FinSequence of Y;
assume A1: for n be Nat st n in dom F holds F.n = <*>D;
A2:dom (Length F) = dom F by Def1 .= Seg len F by FINSEQ_1:def 3;
A6:len F |-> (0 qua Real) = Seg len F --> (0 qua Real) by FINSEQ_2:def 2; then
A3:dom(len F |-> (0 qua Real)) = Seg len F by FUNCT_2:def 1;
now let k be Nat;
assume A4: k in dom (Length F); then
k in dom F by Def1; then
F.k = <*>D by A1; then
(Length F).k = 0 by A4,Def1;
hence (Length F).k = (len F |-> (0 qua Real)).k by A2,A4,A6,FUNCOP_1:7;
end; then
Length F = (len F |-> (0 qua Real)) by A2,A3,FINSEQ_1:13;
hence Sum Length F = 0 by RVSUM_1:81;
end;
theorem Th2:
for D be set, Y be FinSequenceSet of D, F be FinSequence of Y,
k be Nat st k < len F holds
Length(F|(k+1)) = Length(F|k) ^ <*len(F.(k+1))*>
proof
let D be set, Y be FinSequenceSet of D, F be FinSequence of Y, k be Nat;
assume A1: k < len F; then
k+1 <= len F by NAT_1:13; then
A3:len(F|(k+1)) = k+1 by FINSEQ_1:59;
A6:len(F|k) = k by A1,FINSEQ_1:59;
A5:dom (Length(F|(k+1))) = dom (F|(k+1)) & dom (Length(F|k)) = dom(F|k)
by Def1; then
A7:len(Length(F|(k+1))) = k+1 & len(Length(F|k)) = k by A3,A6,FINSEQ_3:29; then
A8:len( Length(F|k) ^ <*len(F.(k+1))*> )
= k + len <*len(F.(k+1))*> by FINSEQ_1:22
.= k+1 by FINSEQ_1:40;
now let n be Nat;
assume A9: 1 <= n & n <= len(Length(F|(k+1))); then
n in dom(Length(F|(k+1))) by FINSEQ_3:25; then
A10: (Length(F|(k+1))).n = len((F|(k+1)).n) by Def1
.= len(F.n) by A7,A9,FINSEQ_3:112;
per cases;
suppose n = len(Length(F|(k+1)));
hence (Length(F|(k+1))).n = (Length(F|k)^<*len(F.(k+1))*>).n
by A7,A10,FINSEQ_1:42;
end;
suppose n <> len(Length(F|(k+1))); then
n < k+1 by A7,A9,XXREAL_0:1; then
A11: n <= k by NAT_1:13; then
(Length(F|k) ^ <*len(F.(k+1))*>).n = (Length(F|k)).n by A9,A7,FINSEQ_1:64
.= len((F|k).n) by A11,Def1,A9,A5,A6,FINSEQ_3:25
.= len(F.n) by A11,FINSEQ_3:112;
hence (Length(F|(k+1))).n = (Length(F|k) ^ <*len(F.(k+1))*>).n by A10;
end;
end;
hence thesis by A5,A8,A3,FINSEQ_3:29;
end;
theorem Th3:
for D be set, Y be FinSequenceSet of D, F be FinSequence of Y,
n be Nat st 1 <= n & n <= Sum Length F holds
ex k,m be Nat
st 1 <= m & m <= len(F.(k+1)) & k < len F & m + Sum Length(F|k) = n
& n <= Sum Length(F|(k+1))
proof
let D be set, Y be FinSequenceSet of D, F be FinSequence of Y, n be Nat;
assume A1: 1<= n & n <= Sum Length F;
now assume
A2: for k be Nat holds n <= Sum Length(F|k) or n > Sum Length(F|(k+1));
defpred P[Nat] means n > Sum Length(F|($1+1));
dom Length(F|0) = dom {} by Def1; then
Length(F|0) = {}; then
A3: P[0] by A2,A1,RVSUM_1:72;
A4: for k be Nat st P[k] holds P[k+1] by A2;
for k be Nat holds P[k] from NAT_1:sch 2(A3,A4); then
n > Sum Length(F|(len F + 1));
hence contradiction by A1,FINSEQ_1:58,NAT_1:11;
end; then
consider k be Nat such that
A6: Sum Length(F|k) < n & n <= Sum Length(F|(k+1));
consider m be Nat such that
A7: n = Sum Length(F|k) + m by A6,NAT_1:10;
take k,m;
A8:now assume A9: len F <= k;
k <= k+1 by NAT_1:11; then
(F|(k+1)) = F & F|k = F by A9,XXREAL_0:2,FINSEQ_1:58;
hence contradiction by A6;
end; then
Length(F|(k+1)) = Length(F|k) ^ <*len(F.(k+1))*> by Th2; then
m + Sum Length(F|k) <= Sum Length(F|k) + len(F.(k+1)) by A6,A7,RVSUM_1:74;
hence thesis by A6,A7,NAT_1:19,A8,XREAL_1:6;
end;
RFINSEQlm3:
for n be Nat, D be set, f be FinSequence of D st len f<=n holds (f|n) = f
proof
let n be Nat, D be set,f be FinSequence of D;
A1:dom f = Seg len f by FINSEQ_1:def 3;
assume len f<=n;
hence thesis by A1,FINSEQ_1:5,RELAT_1:68;
end;
RFINSEQ6:
for D be set, f be FinSequence of D, n,m be Nat holds
n in dom f & m in Seg n implies (f|n).m = f.m & m in dom f
proof
let D be set,f be FinSequence of D, n,m be Nat;
assume that
A1: n in dom f and
A2: m in Seg n;
A3:dom f = Seg len f & n<=len f by A1,FINSEQ_1:def 3,FINSEQ_3:25; then
A4:Seg n c= dom f by FINSEQ_1:5;
Seg n = dom f /\ Seg n by A3,FINSEQ_1:5,XBOOLE_1:28
.= dom(f|n) by RELAT_1:61;
hence thesis by A2,A4,FUNCT_1:47;
end;
RFINSEQ8:
for D be set, f be FinSequence of D, n be Nat holds (f|n)^(f/^n) = f
proof
let D be set, f be FinSequence of D,n be Nat;
set fn = f/^n;
per cases;
suppose len f<n; then
f/^n = <*>D & f|n = f by RFINSEQ:def 1,RFINSEQlm3;
hence thesis by FINSEQ_1:34;
end;
suppose
A1: n<=len f; then
A3: len (f|n) = n by FINSEQ_1:59;
A4: len fn = len f - n by A1,RFINSEQ:def 1; then
A5: len ((f|n)^(f/^n)) = n+(len f - n) by A3,FINSEQ_1:22;
A6: dom(f|n) = Seg n by A3,FINSEQ_1:def 3;
now let m be Nat;
assume m in dom f; then
A8: 1<=m & m<=len f by FINSEQ_3:25;
per cases;
suppose
A10: m<=n; then
1<=n by A8,XXREAL_0:2; then
A11: n in dom f by A1,FINSEQ_3:25;
A12: m in Seg n by A8,A10;
hence ((f|n)^(f/^n)).m = (f|n).m by A6,FINSEQ_1:def 7
.= f.m by A12,A11,RFINSEQ6;
end;
suppose
A13: n<m; then
max(0,m-n) = m-n by FINSEQ_2:4; then
reconsider k = m-n as Element of NAT by FINSEQ_2:5;
n+1<=m by A13,NAT_1:13; then
1<=k by XREAL_1:19; then
A15: k in dom fn by A4,A8,XREAL_1:9,FINSEQ_3:25;
((f|n) ^ (f/^n)).m = fn.k by A3,A5,A8,A13,FINSEQ_1:24; then
((f|n) ^ (f/^n)).m = f.(k+n) by A1,A15,RFINSEQ:def 1;
hence ((f|n) ^ (f/^n)).m = f.m;
end;
end;
hence thesis by A5,FINSEQ_2:9;
end;
end;
theorem Th4:
for D be set, Y be FinSequenceSet of D, F1,F2 be FinSequence of Y
holds Length(F1^F2) = (Length F1) ^ (Length F2)
proof
let D be set, Y be FinSequenceSet of D, F1,F2 be FinSequence of Y;
B1:dom (Length(F1^F2)) = dom(F1^F2)
& dom (Length F1) = dom F1 & dom (Length F2) = dom F2 by Def1; then
A1:len (Length(F1^F2)) = len(F1^F2)
& len (Length F1) = len F1 & len (Length F2) = len F2 by FINSEQ_3:29;
B2:len((Length F1)^(Length F2))
= len(Length F1) + len(Length F2) by FINSEQ_1:22; then
A2:len(Length(F1^F2)) = len((Length F1)^(Length F2)) by A1,FINSEQ_1:22;
now let k be Nat;
assume A3: 1 <= k & k <= len(Length(F1^F2)); then
k in dom(Length(F1^F2)) by FINSEQ_3:25; then
A4: (Length(F1^F2)).k = len((F1^F2).k) by Def1;
per cases;
suppose B5: k <= len(Length F1); then
A5: k in dom F1 & k in dom(Length F1) by B1,A3,FINSEQ_3:25; then
((Length F1)^(Length F2)).k = (Length F1).k by FINSEQ_1:def 7
.= len(F1.k) by B5,Def1,B1,A3,FINSEQ_3:25;
hence (Length(F1^F2)).k = ((Length F1) ^ (Length F2)).k
by A5,A4,FINSEQ_1:def 7;
end;
suppose A7: len(Length F1) < k; then
len(Length F1) + 1 <= k by NAT_1:13; then
k - (len(Length F1) + 1) is Nat by NAT_1:21; then
reconsider k1 = k - len(Length F1) - 1 as Nat;
k <= len(Length F1) + len(Length F2) by A3,A1,FINSEQ_1:22; then
k - len(Length F1) <= len(Length F2) by XREAL_1:20; then
A10: k1+1 in dom (Length F2) by FINSEQ_3:25,NAT_1:11;
((Length F1)^(Length F2)).k
= (Length F2).(k1+1) by A2,A3,A7,FINSEQ_1:24
.= len(F2.(k1+1)) by A10,Def1;
hence (Length(F1^F2)).k = ((Length F1) ^ (Length F2)).k
by A4,A3,A1,A7,FINSEQ_1:24;
end;
end;
hence thesis by B2,A1,FINSEQ_1:22;
end;
theorem Th5:
for D be set, Y be FinSequenceSet of D, F be FinSequence of Y,
k1,k2 be Nat st k1 <= k2
holds Sum Length(F|k1) <= Sum Length(F|k2)
proof
let D be set, Y be FinSequenceSet of D, F be FinSequence of Y, k1,k2 be Nat;
assume k1 <= k2; then
F|k2|k1 = F|k1 by FINSEQ_1:82; then
F|k2 = (F|k1)^((F|k2)/^k1) by RFINSEQ8; then
Length(F|k2) = Length(F|k1) ^ Length((F|k2)/^k1) by Th4; then
Sum Length(F|k2) = Sum Length(F|k1) + Sum Length((F|k2)/^k1) by RVSUM_1:75;
hence thesis by NAT_1:11;
end;
theorem Th6:
for D be set, Y be FinSequenceSet of D,
F be FinSequence of Y, m1,m2,k1,k2 be Nat
st 1 <= m1 & 1 <= m2
& m1 + Sum Length(F|k1) = m2 + Sum Length(F|k2)
& m1 + Sum Length(F|k1) <= Sum Length(F|(k1+1))
& m2 + Sum Length(F|k2) <= Sum Length(F|(k2+1))
holds m1=m2 & k1=k2
proof
let D be set, Y be FinSequenceSet of D, F be FinSequence of Y,
m1,m2,k1,k2 be Nat;
assume that
A1: 1 <= m1 & 1 <= m2 and
A2: m1 + Sum Length(F|k1) = m2 + Sum Length(F|k2) and
A3: m1 + Sum Length(F|k1) <= Sum Length(F|(k1+1)) and
A4: m2 + Sum Length(F|k2) <= Sum Length(F|(k2+1));
set n = m1 + Sum Length(F|k1);
A5:now assume A6: k1 <> k2;
per cases by A6,XXREAL_0:1;
suppose k1 < k2; then
k1+1 <= k2 by NAT_1:13; then
Sum Length(F|(k1+1)) <= Sum Length(F|k2) by Th5; then
n <= Sum Length(F|k2) by A3,XXREAL_0:2;
hence contradiction by A2,A1,NAT_1:19;
end;
suppose k1 > k2; then
k2+1 <= k1 by NAT_1:13; then
Sum Length(F|(k2+1)) <= Sum Length(F|k1) by Th5; then
n <= Sum Length(F|k1) by A2,A4,XXREAL_0:2;
hence contradiction by A1,NAT_1:19;
end;
end;
now assume m1 <> m2; then
Sum Length(F|k1) - Sum Length(F|k2) <> 0 by A2;
hence k1 <> k2;
end;
hence thesis by A5;
end;
definition
let D be non empty set, Y be FinSequenceSet of D, F be FinSequence of Y;
func joined_FinSeq F -> FinSequence of D means :Def2:
len it = Sum Length F &
for n be Nat st n in dom it
ex k,m be Nat st
1 <= m & m <= len(F.(k+1)) & k < len F
& m + Sum Length(F|k) = n & n <= Sum Length(F|(k+1)) & it.n = (F.(k+1)).m;
existence
proof
defpred P[Nat,object] means
ex k,m be Nat st
1<= m & m <= len(F.(k+1)) & k < len F & m + Sum Length(F|k) = $1
& $1 <= Sum Length(F|(k+1)) & $2 = (F.(k+1)).m;
A1:for n be Nat st n in Seg (Sum Length F)
ex x be Element of D st P[n,x]
proof
let n be Nat;
assume n in Seg (Sum Length F); then
1 <= n & n <= Sum Length F by FINSEQ_1:1; then
consider k,m be Nat such that
A2: 1 <= m & m <= len(F.(k+1)) & k < len F & m + Sum Length(F|k) = n
& n <= Sum Length(F|(k+1)) by Th3;
m in dom (F.(k+1)) by A2,FINSEQ_3:25; then
(F.(k+1)).m in rng(F.(k+1)) by FUNCT_1:3; then
reconsider x = (F.(k+1)).m as Element of D;
take x;
thus thesis by A2;
end;
consider IT be FinSequence of D such that
A3: dom IT = Seg (Sum Length F)
& for n be Nat st n in Seg (Sum Length F) holds P[n,IT.n]
from FINSEQ_1:sch 5(A1);
take IT;
thus len IT = Sum Length F by A3,FINSEQ_1:def 3;
thus for n be Nat st n in dom IT holds
ex k,m be Nat st
1 <= m & m <= len(F.(k+1)) & k < len F & m + Sum Length(F|k) = n
& n <= Sum Length(F|(k+1)) & IT.n = (F.(k+1)).m by A3;
end;
uniqueness
proof
let IT1,IT2 be FinSequence of D;
assume that
A1: len IT1 = Sum Length F &
(for n be Nat st n in dom IT1
ex k,m be Nat st
1 <= m & m <= len(F.(k+1)) & k < len F
& m + Sum Length(F|k) = n & n <= Sum Length(F|(k+1))
& IT1.n = (F.(k+1)).m)
and
A2: len IT2 = Sum Length F &
(for n be Nat st n in dom IT2
ex k,m be Nat st
1 <= m & m <= len(F.(k+1)) & k < len F
& m + Sum Length(F|k) = n & n <= Sum Length(F|(k+1))
& IT2.n = (F.(k+1)).m);
A3:dom IT1 = dom IT2 by A1,A2,FINSEQ_3:29;
now let n be Nat;
assume A4: n in dom IT1; then
consider k1,m1 be Nat such that
A5: 1 <= m1 & m1 <= len(F.(k1+1)) & k1 < len F & m1 + Sum Length(F|k1) = n
& n <= Sum Length(F|(k1+1)) & IT1.n = (F.(k1+1)).m1 by A1;
consider k2,m2 be Nat such that
A6: 1 <= m2 & m2 <= len(F.(k2+1)) & k2 < len F & m2 + Sum Length(F|k2) = n
& n <= Sum Length(F|(k2+1)) & IT2.n = (F.(k2+1)).m2 by A2,A3,A4;
k1 = k2 & m1 = m2 by A5,A6,Th6;
hence IT1.n = IT2.n by A5,A6;
end;
hence IT1=IT2 by A1,A2,FINSEQ_3:29,FINSEQ_1:13;
end;
end;
definition
let D be set, Y be FinSequenceSet of D, s be sequence of Y;
func Length s -> sequence of NAT means :Def3:
for n be Nat holds it.n = len(s.n);
existence
proof
defpred P[Nat,object] means $2 = len(s.$1);
A1:for k be Element of NAT ex x be Element of NAT st P[k,x];
consider IT be Function of NAT,NAT such that
A2: for k be Element of NAT holds P[k,IT.k] from FUNCT_2:sch 3(A1);
take IT;
hereby let n be Nat;
n is Element of NAT by ORDINAL1:def 12;
hence IT.n = len(s.n) by A2;
end;
end;
uniqueness
proof
let IT1,IT2 be sequence of NAT;
assume that
A1: for n be Nat holds IT1.n = len(s.n) and
A2: for n be Nat holds IT2.n = len(s.n);
now let n be Element of NAT;
IT1.n = len(s.n) by A1;
hence IT1.n = IT2.n by A2;
end;
hence IT1 = IT2 by FUNCT_2:63;
end;
end;
definition
let s be sequence of NAT;
redefine func Partial_Sums s -> sequence of NAT; :: redefines Partial_Sums (SERIES_1, definition)
correctness
proof
A2:Partial_Sums s is total;
now let y be object;
assume y in rng(Partial_Sums s); then
consider n be object such that
A3: n in dom(Partial_Sums s) & y = (Partial_Sums s).n by FUNCT_1:def 3;
reconsider n as Nat by A3;
defpred P[Nat] means (Partial_Sums s).$1 is Nat;
(Partial_Sums s).0 = s.0 by SERIES_1:def 1; then
A4: P[0];
A5: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k]; then
reconsider Pk = (Partial_Sums s).k as Nat;
(Partial_Sums s).(k+1) = Pk + s.(k+1) by SERIES_1:def 1;
hence P[k+1];
end;
for k be Nat holds P[k] from NAT_1:sch 2(A4,A5); then
(Partial_Sums s).n is Nat;
hence y in NAT by A3,ORDINAL1:def 12;
end;
hence Partial_Sums s is sequence of NAT by A2,TARSKI:def 3,FUNCT_2:2;
end;
end;
registration
let D be non empty set;
cluster non empty with_non-empty_element for FinSequenceSet of D;
existence
proof
consider x be object such that
A1:x in D by XBOOLE_0:def 1;
reconsider x as Element of D by A1;
set S = {<*x*>};
for a be object st a in S holds a is FinSequence of D by TARSKI:def 1; then
reconsider S as FinSequenceSet of D by FINSEQ_2:def 3;
take S;
thus S is non empty with_non-empty_element;
end;
end;
theorem Th7:
for D be non empty set,
Y be non empty with_non-empty_element FinSequenceSet of D,
s be non-empty sequence of Y, n be Nat holds
len(s.n) >= 1 & n < (Partial_Sums(Length s)).n
& (Partial_Sums(Length s)).n < (Partial_Sums(Length s)).(n+1)
proof
let D be non empty set,
Y be non empty with_non-empty_element FinSequenceSet of D,
s be non-empty sequence of Y,
n be Nat;
defpred P[Nat] means $1 < (Partial_Sums(Length s)).$1;
A1:for k be Nat holds len(s.k) >= 1
proof
let k be Nat;
dom s = NAT by FUNCT_2:def 1; then
k in dom s by ORDINAL1:def 12;
hence len(s.k) >= 1 by FINSEQ_1:20;
end;
(Partial_Sums(Length s)).0 = (Length s).0 by SERIES_1:def 1
.= len(s.0) by Def3; then
A3:P[0];
A4:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A5: P[k];
A6: (Partial_Sums(Length s)).(k+1)
= (Partial_Sums(Length s)).k + (Length s).(k+1) by SERIES_1:def 1;
(Length s).(k+1) = len(s.(k+1)) by Def3;
hence P[k+1] by A1,A6,A5,XREAL_1:8;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A3,A4);
hence len(s.n) >= 1 & n < (Partial_Sums(Length s)).n by A1;
(Partial_Sums(Length s)).(n+1)
= (Partial_Sums(Length s)).n + (Length s).(n+1) by SERIES_1:def 1
.= (Partial_Sums(Length s)).n + len(s.(n+1)) by Def3;
hence thesis by XREAL_1:29;
end;
theorem Th8:
for D be non empty set,
Y be non empty with_non-empty_element FinSequenceSet of D,
s be non-empty sequence of Y, n be Nat holds
ex k,m be Nat st
m in dom(s.k) & (Partial_Sums(Length s)).k - len(s.k) + m - 1 = n
proof
let D be non empty set,
Y be non empty with_non-empty_element FinSequenceSet of D,
s be non-empty sequence of Y, n be Nat;
per cases;
suppose A1: n < len(s.0);
set k = 0;
set m = n+1;
take k,m;
A4: m <= len(s.k) by A1,NAT_1:13;
(Partial_Sums(Length s)).k = (Length s).0 by SERIES_1:def 1
.= len(s.k) by Def3;
hence m in dom(s.k) & (Partial_Sums(Length s)).k - len(s.k) + m-1= n
by NAT_1:11,A4,FINSEQ_3:25;
end;
suppose A5: len(s.0) <= n; then
(Length s).0 <= n by Def3; then
A6: (Partial_Sums(Length s)).0 <= n by SERIES_1:def 1;
now assume
A8: for k be Nat st k < n holds
n < (Partial_Sums(Length s)).k or (Partial_Sums(Length s)).(k+1) <= n;
defpred P[Nat] means $1 < n implies (Partial_Sums(Length s)).($1+1) <= n;
A9: P[0] by A6,A8;
A12: for k be Nat st P[k] holds P[k+1] by A8,NAT_1:13;
A13: for k be Nat holds P[k] from NAT_1:sch 2(A9,A12);
reconsider n1 = n-1 as Nat by A5,NAT_1:20;
(Partial_Sums(Length s)).(n1+1) <= n by A13,NAT_1:19;
hence contradiction by Th7;
end; then
consider k1 be Nat such that
A14: k1 < n
& (Partial_Sums(Length s)).k1 <= n & n < (Partial_Sums(Length s)).(k1+1);
take k = k1+1;
reconsider m1 = (Partial_Sums(Length s)).k - n as Nat by A14,NAT_1:21;
(Partial_Sums(Length s)).k = (Partial_Sums(Length s)).k1 + (Length s).k
by SERIES_1:def 1; then
A15:m1 = (Partial_Sums(Length s)).k1 + len(s.k) - n by Def3;
(Partial_Sums(Length s)).k1 - n <= 0 by A14,XREAL_1:47; then
A17:(Partial_Sums(Length s)).k1 - n + len(s.k) <= len(s.k) by XREAL_1:32; then
m1 <= len(s.k) & len(s.k) <= len(s.k)+1 by A15,NAT_1:11; then
reconsider m = len(s.k) +1 - m1 as Nat by NAT_1:21,XXREAL_0:2;
take m;
m1 > 0 by A14,XREAL_1:50; then
len(s.k) - m1 >= 0 & 1-m1 <= 0 by A15,A17,NAT_1:14,XREAL_1:47,48; then
len(s.k) - m1 + 1 >= 0+1 & len(s.k) + (1 - m1) <= len(s.k) + 0
by XREAL_1:6;
hence m in dom(s.k) & (Partial_Sums(Length s)).k - len(s.k) + m -1 = n
by FINSEQ_3:25;
end;
end;
theorem Th9:
for D be non empty set,
Y be non empty with_non-empty_element FinSequenceSet of D,
s be non-empty sequence of Y
holds Partial_Sums(Length s) is increasing
proof
let D be non empty set,
Y be non empty with_non-empty_element FinSequenceSet of D,
s be non-empty sequence of Y;
now let n,m be Nat;
assume
A1: n in dom(Partial_Sums(Length s)) & m in dom(Partial_Sums(Length s))
& n < m;
defpred P[Nat] means
(Partial_Sums(Length s)).n < (Partial_Sums(Length s)).(n+1+$1);
(Partial_Sums(Length s)).(n+1+0)
= (Partial_Sums(Length s)).n + (Length s).(n+1) by SERIES_1:def 1
.= (Partial_Sums(Length s)).n + len(s.(n+1)) by Def3; then
A3: P[0] by XREAL_1:29;
A4: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A5: P[k];
(Partial_Sums(Length s)).(n+1+(k+1))
= (Partial_Sums(Length s)).(n+1+k) + (Length s).(n+1+k+1)
by SERIES_1:def 1
.= (Partial_Sums(Length s)).(n+1+k) + len(s.(n+1+k+1)) by Def3; then
(Partial_Sums(Length s)).(n+1+(k+1)) > (Partial_Sums(Length s)).(n+1+k)
by XREAL_1:29;
hence P[k+1] by A5,XXREAL_0:2;
end;
A7: for k be Nat holds P[k] from NAT_1:sch 2(A3,A4);
n+1 <= m by A1,NAT_1:13; then
reconsider k = m - (n+1) as Nat by NAT_1:21;
m = n+1+k;
hence (Partial_Sums(Length s)).n < (Partial_Sums(Length s)).m by A7;
end;
hence Partial_Sums(Length s) is increasing by SEQM_3:def 1;
end;
theorem Th10:
for D be non empty set,
Y be non empty with_non-empty_element FinSequenceSet of D,
s be non-empty sequence of Y, m1,m2,k1,k2 be Nat
st m1 in dom(s.k1) & m2 in dom(s.k2) &
(Partial_Sums(Length s)).k1 - len(s.k1) + m1
= (Partial_Sums(Length s)).k2 - len(s.k2) + m2
holds m1=m2 & k1=k2
proof
let D be non empty set,
Y be non empty with_non-empty_element FinSequenceSet of D,
s be non-empty sequence of Y, m1,m2,k1,k2 be Nat;
assume that
A1: m1 in dom(s.k1) & m2 in dom(s.k2) and
A2: (Partial_Sums(Length s)).k1 - len(s.k1) + m1
= (Partial_Sums(Length s)).k2 - len(s.k2) + m2;
set n = (Partial_Sums(Length s)).k1 - len(s.k1) + m1;
A3:1 <= m1 & m1 <= len(s.k1) & 1 <= m2 & m2 <= len(s.k2)
by A1,FINSEQ_3:25; then
len(s.k1) - m1 >= 0 & len(s.k2) - m2 >= 0 by XREAL_1:48; then
A4:(Partial_Sums(Length s)).k1 - (len(s.k1) - m1)
<= (Partial_Sums(Length s)).k1
& (Partial_Sums(Length s)).k2 - (len(s.k2) - m2)
<= (Partial_Sums(Length s)).k2 by XREAL_1:43;
A5:dom(Partial_Sums(Length s)) = NAT by FUNCT_2:def 1; then
A6:k1 in dom(Partial_Sums(Length s)) & k2 in dom(Partial_Sums(Length s))
by ORDINAL1:def 12;
A7:Partial_Sums(Length s) is increasing by Th9;
A14:now assume A8: k1 <> k2;
per cases by A8,XXREAL_0:1;
suppose k1 < k2; then
A10: k1+1 <= k2 by NAT_1:13;
1 <= k1+1 by NAT_1:11; then
reconsider j = k2-1 as Element of NAT by NAT_1:21,A10,XXREAL_0:2;
A11: k1 <= j by A10,XREAL_1:19;
A12: (Partial_Sums(Length s)).k1 <= (Partial_Sums(Length s)).j
proof
k1 = j or k1 < j by A11,XXREAL_0:1;
hence thesis by A5,A6,A7,SEQM_3:def 1;
end;
(Partial_Sums(Length s)).(j+1)
= (Partial_Sums(Length s)).j + (Length s).(j+1) by SERIES_1:def 1
.= (Partial_Sums(Length s)).j + len(s.k2) by Def3; then
n > (Partial_Sums(Length s)).j by A3,A2,XREAL_1:29;
hence contradiction by A4,A12,XXREAL_0:2;
end;
suppose k2 < k1; then
A10: k2+1 <= k1 by NAT_1:13;
1 <= k2+1 by NAT_1:11; then
reconsider j = k1-1 as Element of NAT by NAT_1:21,A10,XXREAL_0:2;
A11: k2 <= j by A10,XREAL_1:19;
A12: (Partial_Sums(Length s)).k2 <= (Partial_Sums(Length s)).j
proof
k2 = j or k2 < j by A11,XXREAL_0:1;
hence thesis by A5,A6,A7,SEQM_3:def 1;
end;
(Partial_Sums(Length s)).(j+1)
= (Partial_Sums(Length s)).j + (Length s).(j+1) by SERIES_1:def 1
.= (Partial_Sums(Length s)).j + len(s.k1) by Def3; then
n > (Partial_Sums(Length s)).j by A3,XREAL_1:29;
hence contradiction by A2,A4,A12,XXREAL_0:2;
end;
end; then
(Partial_Sums(Length s)).k1 - len(s.k1)
= (Partial_Sums(Length s)).k2 - len(s.k2);
hence m1=m2 & k1=k2 by A2,A14;
end;
theorem Th11:
for D be non empty set, Y be with_non-empty_element FinSequenceSet of D,
s be non-empty sequence of Y
ex N be increasing sequence of NAT st
for k be Nat holds N.k = (Partial_Sums(Length s)).k - 1
proof
let D be non empty set, Y be with_non-empty_element FinSequenceSet of D,
s be non-empty sequence of Y;
defpred P[Nat,Nat] means $2 = (Partial_Sums(Length s)).$1 - 1;
A1:for k be Element of NAT ex n be Element of NAT st P[k,n]
proof
let k be Element of NAT;
reconsider n = (Partial_Sums(Length s)).k - 1 as Element of NAT
by Th7,NAT_1:20;
take n;
thus thesis;
end;
consider N be Function of NAT,NAT such that
A2: for k be Element of NAT holds P[k,N.k] from FUNCT_2:sch 3(A1);
A3:for k be Nat holds N.k = (Partial_Sums(Length s)).k - 1
proof
let k be Nat;
k is Element of NAT by ORDINAL1:def 12;
hence thesis by A2;
end;
for n be Nat holds N.n < N.(n+1)
proof
let n be Nat;
(Partial_Sums(Length s)).n - 1 < (Partial_Sums(Length s)).(n+1) - 1
by Th7,XREAL_1:9; then
N.n < (Partial_Sums(Length s)).(n+1) - 1 by A3;
hence N.n < N.(n+1) by A3;
end; then
reconsider N as increasing sequence of NAT by VALUED_1:def 13;
take N;
thus thesis by A3;
end;
definition
let D be non empty set,
Y be with_non-empty_element FinSequenceSet of D,
s be non-empty sequence of Y;
func joined_seq s -> sequence of D means :Def4:
for n be Nat
ex k,m be Nat st
m in dom(s.k) & (Partial_Sums(Length s)).k - len(s.k) + m - 1 = n
& it.n = (s.k).m;
existence
proof
defpred P[Nat,object] means
ex k,m be Nat st
m in dom(s.k) & (Partial_Sums(Length s)).k - len(s.k) + m -1 = $1
& $2 = (s.k).m;
A1:for n be Element of NAT ex y be Element of D st P[n,y]
proof
let n be Element of NAT;
consider k,m be Nat such that
A2: m in dom(s.k) & (Partial_Sums(Length s)).k - len(s.k) + m - 1 = n
by Th8;
(s.k).m in rng(s.k) by A2,FUNCT_1:3; then
reconsider y = (s.k).m as Element of D;
take y;
thus thesis by A2;
end;
consider IT be Function of NAT,D such that
A4: for n be Element of NAT holds P[n,IT.n] from FUNCT_2:sch 3(A1);
reconsider IT as sequence of D;
take IT;
hereby let n be Nat;
n is Element of NAT by ORDINAL1:def 12;
hence ex k,m be Nat st
m in dom(s.k) & (Partial_Sums(Length s)).k - len(s.k) + m-1 = n
& IT.n = (s.k).m by A4;
end;
end;
uniqueness
proof
let f1,f2 be sequence of D such that
A1: (for n be Nat ex k,m be Nat st
m in dom(s.k) & (Partial_Sums(Length s)).k - len(s.k) + m - 1 = n
& f1.n = (s.k).m) and
A2: (for n be Nat ex k,m be Nat st
m in dom(s.k) & (Partial_Sums(Length s)).k - len(s.k) + m - 1 = n
& f2.n = (s.k).m);
for n be Element of NAT holds f1.n = f2.n
proof
let n be Element of NAT;
consider k1,m1 be Nat such that
A3: m1 in dom(s.k1) & (Partial_Sums(Length s)).k1 - len(s.k1) + m1 - 1 = n
& f1.n = (s.k1).m1 by A1;
consider k2,m2 be Nat such that
A4: m2 in dom(s.k2) & (Partial_Sums(Length s)).k2 - len(s.k2) + m2 - 1 = n
& f2.n = (s.k2).m2 by A2;
m1 = m2 & k1 = k2 by A3,A4,Th10;
hence f1.n = f2.n by A3,A4;
end;
hence f1 = f2 by FUNCT_2:def 8;
end;
end;
theorem
for D be non empty set, Y be with_non-empty_element FinSequenceSet of D,
s be non-empty sequence of Y, s1 be sequence of D st
( for n be Nat holds s1.n = (joined_seq s).(Partial_Sums(Length s).n - 1) )
holds s1 is subsequence of joined_seq s
proof
let D be non empty set, Y be with_non-empty_element FinSequenceSet of D;
let s be non-empty sequence of Y, s1 be sequence of D;
assume
A1:for n be Nat holds s1.n = (joined_seq s).(Partial_Sums(Length s).n - 1);
consider N be increasing sequence of NAT such that
A2: for n be Nat holds N.n = (Partial_Sums(Length s)).n - 1 by Th11;
for n be Element of NAT holds s1.n = ((joined_seq s)*N).n
proof
let n be Element of NAT;
s1.n = (joined_seq s).(Partial_Sums(Length s).n - 1) by A1; then
s1.n = (joined_seq s).(N.n) by A2;
hence s1.n = ((joined_seq s)*N).n by FUNCT_2:15;
end;
hence s1 is subsequence of joined_seq s by FUNCT_2:def 8;
end;
theorem Th13:
for D be non empty set, Y be with_non-empty_element FinSequenceSet of D,
s be non-empty sequence of Y, k,m be Nat st m in dom(s.k)
ex n be Nat st n = (Partial_Sums(Length s)).k - len(s.k) + m - 1
& (joined_seq s).n = (s.k).m
proof
let D be non empty set, Y be with_non-empty_element FinSequenceSet of D,
s be non-empty sequence of Y, k,m be Nat;
assume A0: m in dom(s.k); then
A1:1 <= m & m <= len(s.k) by FINSEQ_3:25;
now per cases;
suppose A2: k = 0; then
(Partial_Sums(Length s)).k = (Length s).0 by SERIES_1:def 1
.= len(s.0) by Def3;
hence (Partial_Sums(Length s)).k - len(s.k) + m - 1 is Nat
by A1,A2,NAT_1:21;
end;
suppose k <> 0; then
reconsider k1 = k-1 as Element of NAT by NAT_1:14,21;
k = k1+1; then
(Partial_Sums(Length s)).k = (Partial_Sums(Length s)).k1 + (Length s).k
by SERIES_1:def 1
.= (Partial_Sums(Length s)).k1 + len(s.k) by Def3; then
reconsider n1= (Partial_Sums(Length s)).k - len(s.k) as Nat;
n1+m >= m by NAT_1:11;
hence (Partial_Sums(Length s)).k - len(s.k) + m - 1 is Nat
by A1,XXREAL_0:2,NAT_1:21;
end;
end; then
reconsider n = (Partial_Sums(Length s)).k - len(s.k) + m - 1 as Nat;
take n;
thus n = (Partial_Sums(Length s)).k - len(s.k) + m - 1;
consider k2,m2 be Nat such that
A4: m2 in dom(s.k2) & (Partial_Sums(Length s)).k2 - len(s.k2) + m2 - 1 = n
& (joined_seq s).n = (s.k2).m2 by Def4;
m = m2 & k = k2 by A0,A4,Th10;
hence (joined_seq s).n = (s.k).m by A4;
end;
theorem Th14:
for D be non empty set, Y be FinSequenceSet of D,
F be FinSequence of Y
st ( for n,m be Nat st n <> m holds union rng(F.n) misses union rng(F.m) )
& ( for n be Nat holds F.n is disjoint_valued)
holds (joined_FinSeq F) is disjoint_valued
proof
let D be non empty set, Y be FinSequenceSet of D, F be FinSequence of Y;
assume that
A1: for n,m be Nat st n <> m holds union rng(F.n) misses union rng(F.m) and
A2: for n be Nat holds F.n is disjoint_valued;
now let x,y be object;
assume A3: x <> y;
per cases;
suppose A4: x in dom(joined_FinSeq F) & y in dom(joined_FinSeq F); then
reconsider n1=x, n2=y as Nat;
consider k1,m1 be Nat such that
A5: 1<=m1 & m1<=len(F.(k1+1)) & k1<len F
& m1+Sum Length(F|k1) = n1 & n1 <= Sum Length(F|(k1+1))
& (joined_FinSeq F).x = (F.(k1+1)).m1 by A4,Def2;
consider k2,m2 be Nat such that
A6: 1<=m2 & m2<=len(F.(k2+1)) & k2<len F
& m2+Sum Length(F|k2) = n2 & n2 <= Sum Length(F|(k2+1))
& (joined_FinSeq F).y = (F.(k2+1)).m2 by A4,Def2;
m1 in dom (F.(k1+1)) & m2 in dom (F.(k2+1)) by A5,A6,FINSEQ_3:25; then
A8: (joined_FinSeq F).x in rng(F.(k1+1))
& (joined_FinSeq F).y in rng(F.(k2+1)) by A5,A6,FUNCT_1:3;
now assume A9: not (joined_FinSeq F).x misses (joined_FinSeq F).y; then
(joined_FinSeq F).x /\ (joined_FinSeq F).y <> {} by XBOOLE_0:def 7; then
consider z be object such that
A10: z in (joined_FinSeq F).x /\ (joined_FinSeq F).y by XBOOLE_0:def 1;
z in (joined_FinSeq F).x & z in (joined_FinSeq F).y
by A10,XBOOLE_0:def 4; then
z in union rng(F.(k1+1)) & z in union rng(F.(k2+1))
by A8,TARSKI:def 4; then
A11: k1+1 = k2+1 by A1,XBOOLE_0:3;
(F.(k1+1)) is disjoint_valued by A2;
hence contradiction by A5,A6,A3,A9,A11,PROB_2:def 2;
end;
hence (joined_FinSeq F).x misses (joined_FinSeq F).y;
end;
suppose not x in dom(joined_FinSeq F)
or not y in dom(joined_FinSeq F); then
(joined_FinSeq F).x = {} or (joined_FinSeq F).y = {} by FUNCT_1:def 2;
hence (joined_FinSeq F).x misses (joined_FinSeq F).y by XBOOLE_1:65;
end;
end;
hence joined_FinSeq F is disjoint_valued by PROB_2:def 2;
end;
theorem Th15:
for D be non empty set, Y be FinSequenceSet of D,
F be FinSequence of Y holds
rng(joined_FinSeq F) = union {rng(F.n) where n is Nat : n in dom F}
proof
let D be non empty set, Y be FinSequenceSet of D, F be FinSequence of Y;
now let x be object;
assume x in rng(joined_FinSeq F); then
consider n be object such that
A1: n in dom(joined_FinSeq F) & x = (joined_FinSeq F).n by FUNCT_1:def 3;
reconsider n as Nat by A1;
consider k,m be Nat such that
A2: 1 <= m & m <= len(F.(k+1)) & k < len F
& m + Sum Length(F|k) = n & n <= Sum Length(F|(k+1))
& (joined_FinSeq F).n = (F.(k+1)).m by A1,Def2;
1 <= k+1 & k+1 <= len F by A2,NAT_1:11,13; then
A3: k+1 in dom F by FINSEQ_3:25;
m in dom(F.(k+1)) by A2,FINSEQ_3:25; then
A4: x in rng(F.(k+1)) by A1,A2,FUNCT_1:3;
rng(F.(k+1)) in {rng(F.n) where n is Nat: n in dom F} by A3;
hence x in union{rng(F.n) where n is Nat: n in dom F} by A4,TARSKI:def 4;
end; then
A5:rng(joined_FinSeq F) c= union {rng(F.n) where n is Nat : n in dom F}
by TARSKI:def 3;
now let x be object;
assume x in union{rng(F.n) where n is Nat: n in dom F}; then
consider A be set such that
A6: x in A & A in {rng(F.n) where n is Nat: n in dom F} by TARSKI:def 4;
consider k be Nat such that
A7: A = rng(F.k) & k in dom F by A6;
consider m be object such that
A8: m in dom(F.k) & x = (F.k).m by A6,A7,FUNCT_1:def 3;
reconsider m as Nat by A8;
A9: 1 <= k & k <= len F by A7,FINSEQ_3:25;
reconsider k1 = k-1 as Nat by A7,FINSEQ_3:25,NAT_1:21;
set n = m + Sum Length(F|k1);
Length(F|(k1+1)) = Length(F|k1) ^ <*len(F.(k1+1))*>
by Th2,A9,NAT_1:13; then
A11:Sum Length(F|(k1+1)) = Sum Length(F|k1) + len(F.(k1+1)) by RVSUM_1:74;
A14:1 <= m & m <= len(F.(k1+1)) by A8,FINSEQ_3:25; then
A12:n <= Sum Length(F|(k1+1)) by A11,XREAL_1:6;
Sum Length(F|(k1+1)) <= Sum Length(F|(len F)) by A9,Th5; then
n <= Sum Length(F|(len F)) by A12,XXREAL_0:2; then
n <= Sum Length F by FINSEQ_1:58; then
A13:n <= len (joined_FinSeq F) by Def2;
m <= n by NAT_1:11; then
1 <= n by A14,XXREAL_0:2; then
A17:n in dom (joined_FinSeq F) by A13,FINSEQ_3:25; then
consider k2,m2 be Nat such that
A15: 1 <= m2 & m2 <= len(F.(k2+1)) & k2 < len F
& m2 + Sum Length(F|k2) = n & n <= Sum Length(F|(k2+1))
& (joined_FinSeq F).n = (F.(k2+1)).m2 by Def2;
m = m2 & k1 = k2 by A14,A15,A12,Th6;
hence x in rng(joined_FinSeq F) by A8,A15,A17,FUNCT_1:3;
end; then
union {rng(F.n) where n is Nat:n in dom F} c= rng(joined_FinSeq F)
by TARSKI:def 3;
hence thesis by A5,XBOOLE_0:def 10;
end;
begin :: Extended real valued matrix
definition
let x be ext-real number;
redefine func <*x*> -> FinSequence of ExtREAL; :: redefines <* (FINSEQ_1, definition)
coherence
proof
for y be object st y in rng <*x*> holds y in ExtREAL;
hence thesis by FINSEQ_1:def 4;
end;
end;
definition
let e be FinSequence of ExtREAL*;
func Sum e -> FinSequence of ExtREAL means :Def5:
len it = len e & for k be Nat st k in dom it holds it.k = Sum(e.k);
existence
proof
deffunc f(Nat) = Sum(e.$1);
consider e1 be FinSequence of ExtREAL such that
A1: len e1 = len e & for k be Nat st k in dom e1 holds e1.k = f(k)
from FINSEQ_2:sch 1;
take e1;
thus thesis by A1;
end;
uniqueness
proof
let e1,e2 be FinSequence of ExtREAL such that
A2: len e1 = len e and
A3: for k be Nat st k in dom e1 holds e1.k = Sum(e.k) and
A4: len e2 = len e and
A5: for k be Nat st k in dom e2 holds e2.k = Sum(e.k);
dom e1 = dom e2 & for k be Nat st k in dom e1 holds e1.k = e2.k
proof
thus
A6: dom e1 = Seg len e by A2,FINSEQ_1:def 3
.= dom e2 by A4,FINSEQ_1:def 3;
let k be Nat such that
A7: k in dom e1;
thus e1.k = Sum(e.k) by A3,A7
.= e2.k by A5,A6,A7;
end;
hence thesis by FINSEQ_1:13;
end;
end;
definition
let M be Matrix of ExtREAL;
func SumAll M -> Element of ExtREAL equals
Sum Sum M;
coherence;
end;
theorem Th16:
for M be Matrix of ExtREAL holds
len Sum M = len M
& for i be Nat st i in Seg len M holds (Sum M).i=Sum Line(M,i)
proof
let M be Matrix of ExtREAL;
thus len Sum M = len M by Def5;
thus for k be Nat st k in Seg len M holds (Sum M).k=Sum Line(M,k)
proof
let k be Nat such that
A1: k in Seg len M;
A2: k in dom M by A1,FINSEQ_1:def 3;
k in Seg len Sum M by A1,Def5;
then k in dom Sum M by FINSEQ_1:def 3;
hence (Sum M).k = Sum(M.k) by Def5
.= Sum(Line(M,k)) by A2,MATRIX_0:60;
end;
end;
theorem Th17:
for F be FinSequence of ExtREAL st
for i be Nat st i in dom F holds F.i <> -infty
holds Sum F <> -infty
proof
let F be FinSequence of ExtREAL;
assume A1: for i be Nat st i in dom F holds F.i <> -infty;
consider f be Function of NAT,ExtREAL such that
A2: 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;
defpred P[Nat] means $1 <= len F implies f.$1 <> -infty;
A4:P[0] by A2;
A5:for j be Nat st P[j] holds P[j+1]
proof
let j be Nat;
assume A6: P[j];
now assume B2: j+1 <= len F; then
A8: f.(j+1) = f.j + F.(j+1) by A2,NAT_1:13;
1 <= j+1 by NAT_1:11; then
F.(j+1) <> -infty by A1,B2,FINSEQ_3:25;
hence f.(j+1) <> -infty by A8,A6,B2,NAT_1:13,XXREAL_3:17;
end;
hence P[j+1];
end;
for i be Nat holds P[i] from NAT_1:sch 2(A4,A5);
hence Sum F <> -infty by A2;
end;
theorem Th18:
for F,G,H be FinSequence of ExtREAL st
not -infty in rng F & not -infty in rng G &
dom F = dom G & H = F + G
holds Sum H = Sum F + Sum G
proof
let F,G,H be FinSequence of ExtREAL;
assume that
A1: not -infty in rng F & not -infty in rng G and
A3: dom F = dom G and
A4: H = F + G;
B1:for y be object st y in rng F holds not y in {-infty}
by A1,TARSKI:def 1; then
A7:F"{-infty} = {} by XBOOLE_0:3,RELAT_1:138;
B2:for y be object st y in rng G holds not y in {-infty}
by A1,TARSKI:def 1; then
A10: G"{-infty} = {} by XBOOLE_0:3,RELAT_1:138;
A11: dom H = (dom F /\ dom G)\((F"{-infty}/\G"{+infty})\/(F"{+infty}/\G"{
-infty})) by A4,MESFUNC1:def 3
.= dom F by A3,A7,A10; then
A12:len H = len F by FINSEQ_3:29;
consider h be Function of NAT,ExtREAL such that
A13: Sum H = h.(len H) & h.0 = 0.
& for i be Nat st i < len H holds h.(i+1) = h.i + H.(i+1)
by EXTREAL1:def 2;
consider f be Function of NAT,ExtREAL such that
A16: 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;
consider g be Function of NAT,ExtREAL such that
A19: Sum G = g.(len G) & g.0 = 0.
& for i be Nat st i < len G holds g.(i+1) = g.i + G.(i+1)
by EXTREAL1:def 2;
defpred P[Nat] means $1 <= len H implies h.$1 = f.$1 + g.$1;
A22:len H = len G by A3,A11,FINSEQ_3:29;
A23:for k be Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume A24: P[k];
assume A25: k+1 <= len H;
A26:k < len H by A25,NAT_1:13;
A27:f.(k+1) = f.k + F.(k+1) & g.(k+1) = g.k + G.(k+1)
by A16,A19,A12,A22,A25,NAT_1:13;
A28:k+1 in dom H by A25,NAT_1:11,FINSEQ_3:25;
A29:f.k <> -infty & g.k <> -infty & F.(k+1) <> -infty & G.(k+1) <> -infty
proof
defpred Pg[Nat] means $1 <= len H implies g.$1 <> -infty;
defpred Pf[Nat] means $1 <= len H implies f.$1 <> -infty;
A30: for m be Nat st Pf[m] holds Pf[m+1]
proof
let m be Nat;
assume A31: Pf[m];
assume A32: m+1 <= len H; then
m+1 in dom H by NAT_1:11,FINSEQ_3:25; then
not F.(m+1) in {-infty} by B1,A11,FUNCT_1:3; then
A33: F.(m+1) <> -infty by TARSKI:def 1;
f.(m+1) = f.m + F.(m+1) by A12,A16,A32,NAT_1:13;
hence thesis by A33,A32,NAT_1:13,A31,XXREAL_3:17;
end;
A34: Pf[0] by A16;
for i be Nat holds Pf[i] from NAT_1:sch 2(A34,A30);
hence f.k <> -infty by A26;
A35: for m be Nat st Pg[m] holds Pg[m+1]
proof
let m be Nat;
assume A36: Pg[m];
assume A37: m+1 <= len H; then
m+1 in dom H by NAT_1:11,FINSEQ_3:25; then
not G.(m+1) in {-infty} by B2,A11,A3,FUNCT_1:3; then
A38: G.(m+1) <> -infty by TARSKI:def 1;
g.(m+1) = g.m + G.(m+1) by A19,A22,A37,NAT_1:13;
hence thesis by A38,A37,NAT_1:13,A36,XXREAL_3:17;
end;
A39: Pg[0] by A19;
for i be Nat holds Pg[i] from NAT_1:sch 2(A39,A35);
hence g.k <> -infty by A26;
thus F.(k+1) <> -infty by A1,A11,A28,FUNCT_1:3;
thus thesis by A1,A3,A11,A28,FUNCT_1:3;
end; then
A40:f.k + F.(k+1) <> -infty by XXREAL_3:17;
A41:h.(k+1) = (f.k + g.k) + H.(k+1) by A13,A24,A25,NAT_1:13
.= (f.k + g.k) + (F.(k+1) + G.(k+1)) by A4,A28,MESFUNC1:def 3;
f.k + g.k <> -infty by A29,XXREAL_3:17;
then h.(k+1) = ((f.k + g.k) + F.(k+1)) + G.(k+1) by A41,A29,XXREAL_3:29
.= (f.k + F.(k+1) + g.k) + G.(k+1) by A29,XXREAL_3:29
.= f.(k+1) + g.(k+1) by A27,A29,A40,XXREAL_3:29;
hence thesis;
end;
A42: P[0] by A16,A19,A13;
for i be Nat holds P[i] from NAT_1:sch 2(A42,A23);
hence thesis by A16,A19,A13,A12,A22;
end;
theorem Th19:
for r be R_eal, F be FinSequence of ExtREAL holds
Sum(F^<*r*>) = Sum F + r
proof
let r be R_eal, F be FinSequence of ExtREAL;
consider f be Function of NAT,ExtREAL such that
A1: Sum(F^<*r*>) = f.(len (F^<*r*>)) &
f.0 = 0 &
for i be Nat st i < len (F^<*r*>) holds
f.(i+1) = f.i + (F^<*r*>).(i+1) by EXTREAL1:def 2;
consider g be Function of NAT,ExtREAL such that
A2: Sum F = g.(len F) &
g.0 = 0 &
for i be Nat st i < len F holds
g.(i+1) = g.i + F.(i+1) by EXTREAL1:def 2;
len (F^<*r*>) = len F + len <*r*> by FINSEQ_1:22; then
B1:len (F^<*r*>) = len F + 1 by FINSEQ_1:39; then
B2:len F < len (F^<*r*>) by NAT_1:13;
defpred P[Nat] means $1 <= len F implies f.$1 = g.$1;
A3:P[0] by A1,A2;
A4:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A5: P[k];
assume A6: k+1 <= len F; then
A7: k < len F by NAT_1:13;
A9: (F^<*r*>).(k+1) = F.(k+1) by A6,FINSEQ_1:64,NAT_1:11;
k < len (F^<*r*>) by A7,B1,NAT_1:13; then
f.(k+1) = f.k + (F^<*r*>).(k+1) by A1;
hence f.(k+1) = g.(k+1) by A2,A6,A5,A9,NAT_1:13;
end;
for i be Nat holds P[i] from NAT_1:sch 2(A3,A4); then
f.(len F) = g.(len F); then
f.(len F + 1) = g.(len F) + (F^<*r*>).(len F+1) by A1,B2;
hence Sum(F^<*r*>) = Sum F + r by A1,A2,B1,FINSEQ_1:42;
end;
theorem Th20:
for r be R_eal, i be Nat st r is real holds Sum(i |-> r) = i*r
proof
let r be R_eal, i be Nat;
assume A0: r is real;
defpred P[Nat] means Sum($1 |->r) = $1*r;
A1:for i be Nat st P[i] holds P[i+1]
proof
let i be Nat such that
A2: Sum(i |-> r) = i*r;
reconsider i1 = i, One = 1 as ext-real number;
thus Sum((i+1) |-> r) = Sum((i |-> r)^<*r*>) by FINSEQ_2:60
.= i*r + r by A2,Th19
.= i*r + 1*r by XXREAL_3:81
.= (i1+One)*r by A0,XXREAL_3:95
.= (i+1)*r by XXREAL_3:def 2;
end;
A3:P[0] by EXTREAL1:7,FINSEQ_2:58;
for i be Nat holds P[i] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem Th21:
for M be Matrix of ExtREAL st len M = 0 holds SumAll M = 0
proof
let M be Matrix of ExtREAL;
assume len M = 0; then
len Sum M = 0 by Def5; then
Sum M is empty;
hence thesis by EXTREAL1:7;
end;
theorem Th22:
for m be Nat, M be Matrix of m,0,ExtREAL holds SumAll M = 0
proof
let m be Nat, M be Matrix of m,0,ExtREAL;
per cases;
suppose m = 0; then
len M = 0 by MATRIX_0:def 2;
hence thesis by Th21;
end;
suppose m > 0; then
len M > 0 by MATRIX_0:def 2; then
reconsider k = len Sum M as non zero Nat by Def5;
reconsider Z = 0. as R_eal;
for k be Nat st k in dom Sum M holds (Sum M).k = 0
proof
len M = len Sum M by Def5; then
A2: dom M = dom Sum M by FINSEQ_3:29;
hereby let k be Nat;
assume A3: k in dom Sum M; then
M.k in rng M by A2,FUNCT_1:def 3; then
M.k = <*>ExtREAL by MATRIX_0:def 2;
hence (Sum M).k = 0 by A3,Def5,EXTREAL1:7;
end;
end; then
Sum M = k |-> 0. by MATRPROB:1; then
SumAll M = (len Sum M) * Z by Th20;
hence SumAll M = 0;
end;
end;
theorem Th23:
for n,m,k be Nat, M1 be Matrix of n,k,ExtREAL, M2 be Matrix of m,k,ExtREAL
holds Sum (M1^M2) = (Sum M1)^(Sum M2)
proof
let n,m,k be Nat;
let M1 be Matrix of n,k,ExtREAL;
let M2 be Matrix of m,k,ExtREAL;
A1:dom Sum(M1^M2) = Seg len Sum(M1^M2) by FINSEQ_1:def 3;
A2:now let i be Nat;
assume
A3: i in dom Sum(M1^M2); then
i in Seg len (M1^M2) by A1,Def5; then
A4: i in dom (M1^M2) by FINSEQ_1:def 3;
A8: len M1 = len Sum M1 & len M2 = len Sum M2 by Def5; then
A6: dom M1 = dom Sum M1 & dom M2 = dom Sum M2 by FINSEQ_3:29;
per cases by A4,FINSEQ_1:25;
suppose A5: i in dom M1;
thus Sum(M1^M2).i = Sum ((M1^M2).i) by A3,Def5
.= Sum (M1.i) by A5,FINSEQ_1:def 7
.= (Sum M1).i by A5,A6,Def5
.= ((Sum M1)^(Sum M2)).i by A5,A6,FINSEQ_1:def 7;
end;
suppose ex n be Nat st n in dom M2 & i = len M1 + n; then
consider n be Nat such that
A10: n in dom M2 & i = len M1 + n;
thus Sum(M1^M2).i = Sum ((M1^M2).i) by A3,Def5
.= Sum (M2.n) by A10,FINSEQ_1:def 7
.= (Sum M2).n by A10,A6,Def5
.= ((Sum M1)^(Sum M2)).i by A10,A8,A6,FINSEQ_1:def 7;
end;
end;
len Sum(M1^M2) = len (M1^M2) by Def5
.= len M1 + len M2 by FINSEQ_1:22
.= len Sum M1 + len M2 by Def5
.= len Sum M1 + len Sum M2 by Def5
.= len ((Sum M1)^(Sum M2)) by FINSEQ_1:22;
hence thesis by A2,FINSEQ_2:9;
end;
theorem Th24:
for M1,M2 be Matrix of ExtREAL st
(for i be Nat st i in dom M1 holds not -infty in rng (M1.i) ) &
(for i be Nat st i in dom M2 holds not -infty in rng (M2.i) )
holds Sum M1 + Sum M2 = Sum (M1 ^^ M2)
proof
let M1,M2 be Matrix of ExtREAL;
reconsider M = min(len M1,len M2) as Element of NAT;
assume B0:
(for i be Nat st i in dom M1 holds not -infty in rng (M1.i) ) &
(for i be Nat st i in dom M2 holds not -infty in rng (M2.i) );
now assume -infty in rng (Sum M1); then
consider i be Nat such that
C1: i in dom Sum M1 & (Sum M1).i = -infty by FINSEQ_2:10;
i in Seg len Sum M1 by C1,FINSEQ_1:def 3; then
i in Seg len M1 by Def5; then
i in dom M1 by FINSEQ_1:def 3; then
C2: not -infty in rng (M1.i) by B0;
(Sum M1).i = Sum(M1.i) by C1,Def5; then
ex j be Nat st j in dom (M1.i) & (M1.i).j = -infty by C1,Th17;
hence contradiction by C2,FUNCT_1:3;
end; then
D1:(Sum M1)"{-infty} = {} by FUNCT_1:72;
now assume -infty in rng (Sum M2); then
consider i be Nat such that
C1: i in dom Sum M2 & (Sum M2).i = -infty by FINSEQ_2:10;
i in Seg len Sum M2 by C1,FINSEQ_1:def 3; then
i in Seg len M2 by Def5; then
i in dom M2 by FINSEQ_1:def 3; then
C2: not -infty in rng (M2.i) by B0;
(Sum M2).i = Sum(M2.i) by C1,Def5; then
ex j be Nat st j in dom (M2.i) & (M2.i).j = -infty by C1,Th17;
hence contradiction by C2,FUNCT_1:3;
end; then
(Sum M2)"{-infty} = {} by FUNCT_1:72; then
D2:dom Sum M1 /\ dom Sum M2
=(dom Sum M1 /\ dom Sum M2) \
(((Sum M1)"{-infty} /\ (Sum M2)"{+infty})
\/ ((Sum M2)"{-infty} /\ (Sum M1)"{+infty})) by D1;
A1:Seg M = Seg len M1 /\ Seg len M2 by FINSEQ_2:2
.= Seg len M1 /\ dom M2 by FINSEQ_1:def 3
.= dom M1 /\ dom M2 by FINSEQ_1:def 3
.= dom (M1 ^^ M2) by PRE_POLY:def 4
.= Seg len (M1 ^^ M2) by FINSEQ_1:def 3;
A0:dom Sum M1 = Seg(len Sum M1) & dom Sum M2 = Seg(len Sum M2)
by FINSEQ_1:def 3;
dom(Sum M1 + Sum M2) = dom Sum M1 /\ dom Sum M2 by D2,MESFUNC1:def 3; then
K1:dom(Sum M1 + Sum M2) = Seg min(len Sum M1,len Sum M2) by A0,FINSEQ_2:2; then
reconsider SM12 = Sum M1 + Sum M2 as FinSequence by FINSEQ_1:def 2;
len SM12 = min(len Sum M1,len Sum M2) by K1,FINSEQ_1:def 3; then
A2:len SM12 = min(len M1,len Sum M2) by Def5
.= min(len M1,len M2) by Def5
.= len (M1 ^^ M2) by A1,FINSEQ_1:6
.= len Sum(M1 ^^ M2) by Def5;
A3:dom (Sum M1 + Sum M2) = Seg len SM12 by FINSEQ_1:def 3;
now
let i be Nat;
assume
A4: i in dom (Sum M1 + Sum M2); then
i in Seg len SM12 by FINSEQ_1:def 3; then
i in Seg len(M1 ^^ M2) by A2,Def5; then
A6: i in dom (M1 ^^ M2) by FINSEQ_1:def 3; then
i in dom M1 /\ dom M2 by PRE_POLY:def 4; then
B1: i in dom M1 & i in dom M2 by XBOOLE_0:def 4; then
i in Seg len M1 & i in Seg len M2 by FINSEQ_1:def 3; then
i in Seg len Sum M1 & i in Seg len Sum M2 by Def5; then
A8: i in dom Sum M1 & i in dom Sum M2 by FINSEQ_1:def 3;
A10:i in dom Sum(M1 ^^ M2) by A2,A3,A4,FINSEQ_1:def 3;
A11:((M1.i) ^ (M2.i)) = (M1 ^^ M2).i by A6,PRE_POLY:def 4;
B3: not -infty in rng (M1.i) & not -infty in rng (M2.i) by B0,B1;
thus (Sum M1 + Sum M2).i = (Sum M1).i + (Sum M2).i by A4,MESFUNC1:def 3
.= Sum (M1.i) + (Sum M2.i) by A8,Def5
.= Sum (M1.i) + Sum (M2.i) by A8,Def5
.= Sum ((M1 ^^ M2).i) by A11,B3,EXTREAL1:10
.= (Sum(M1 ^^ M2)).i by A10,Def5;
end;
hence thesis by A2,FINSEQ_2:9;
end;
theorem Th25:
for M1,M2 be Matrix of ExtREAL
st len M1 = len M2 &
(for i be Nat st i in dom M1 holds not -infty in rng (M1.i) ) &
(for i be Nat st i in dom M2 holds not -infty in rng (M2.i) )
holds SumAll M1 + SumAll M2 = SumAll(M1 ^^ M2)
proof
let M1,M2 be Matrix of ExtREAL such that
A1: len M1 = len M2 &
(for i be Nat st i in dom M1 holds not -infty in rng (M1.i) ) &
(for i be Nat st i in dom M2 holds not -infty in rng (M2.i) );
A2:len Sum M1 = len M1 by Def5
.= len Sum M2 by A1,Def5; then
reconsider p1=Sum M1, p2 = Sum M2 as
Element of (len Sum M1)-tuples_on ExtREAL by FINSEQ_2:92;
C0:now assume -infty in rng (Sum M1); then
consider i be Nat such that
C1: i in dom Sum M1 & (Sum M1).i = -infty by FINSEQ_2:10;
i in Seg len Sum M1 by C1,FINSEQ_1:def 3; then
i in Seg len M1 by Def5; then
i in dom M1 by FINSEQ_1:def 3; then
C2: not -infty in rng (M1.i) by A1;
(Sum M1).i = Sum(M1.i) by C1,Def5; then
ex j be Nat st j in dom (M1.i) & (M1.i).j = -infty by C1,Th17;
hence contradiction by C2,FUNCT_1:3;
end;
A3:now assume -infty in rng (Sum M2); then
consider i be Nat such that
C1: i in dom Sum M2 & (Sum M2).i = -infty by FINSEQ_2:10;
i in Seg len Sum M2 by C1,FINSEQ_1:def 3; then
i in Seg len M2 by Def5; then
i in dom M2 by FINSEQ_1:def 3; then
C2: not -infty in rng (M2.i) by A1;
(Sum M2).i = Sum(M2.i) by C1,Def5; then
ex j be Nat st j in dom (M2.i) & (M2.i).j = -infty by C1,Th17;
hence contradiction by C2,FUNCT_1:3;
end;
A4:dom Sum M1 = dom Sum M2 by A2,FINSEQ_3:29;
Sum (M1 ^^ M2) = Sum M1 + Sum M2 by A1,Th24;
hence SumAll M1 + SumAll M2 = SumAll(M1 ^^ M2) by A3,C0,A4,Th18;
end;
theorem Th26:
for p be FinSequence of ExtREAL st not -infty in rng p
holds SumAll <*p*> = SumAll(<*p*>@)
proof
defpred x[FinSequence of ExtREAL] means
not -infty in rng $1 implies SumAll <*$1*> = SumAll(<*$1*>@);
let p be FinSequence of ExtREAL;
assume
B0: not -infty in rng p;
A2:for p be FinSequence of ExtREAL,
x be Element of ExtREAL st x[p] holds x[p^<*x*>]
proof
let p be FinSequence of ExtREAL, x be Element of ExtREAL such that
A3: not -infty in rng p implies SumAll <*p*> = SumAll (<*p*>@);
assume not -infty in rng (p^<*x*>); then
not -infty in rng p \/ rng <*x*> by FINSEQ_1:31; then
B3: not -infty in rng p & not -infty in rng <*x*> by XBOOLE_0:def 3;
Seg len (<*p*> ^^ <*<*x*>*>) = dom (<*p*> ^^ <*<*x*>*>) by FINSEQ_1:def 3
.= dom <*p*> /\ dom <*<*x*>*> by PRE_POLY:def 4
.= Seg 1 /\ dom <*<*x*>*> by FINSEQ_1:38
.= Seg 1 /\ Seg 1 by FINSEQ_1:38
.= Seg 1; then
A4: len (<*p*> ^^ <*<*x*>*>) = 1 by FINSEQ_1:6
.= len <*p^<*x*>*> by FINSEQ_1:39;
A5: dom <*p^<*x*>*> = Seg len <*p^<*x*>*> by FINSEQ_1:def 3;
A6: now let i be Nat;
reconsider M1 = <*p*>.i,M2 = <*<*x*>*>.i as FinSequence;
assume
A7: i in dom <*p^<*x*>*>; then
A8: i = 1 by FINSEQ_1:90;
i in dom (<*p*> ^^ <*<*x*>*>) by A4,A5,A7,FINSEQ_1:def 3;
hence (<*p*> ^^ <*<*x*>*>).i = M1 ^ M2 by PRE_POLY:def 4
.= p ^ M2 by A8
.= p ^ <*x*> by A8
.= <*p^<*x*>*>.i by A8;
end;
per cases;
suppose len p = 0; then
A9: p = {};
hence SumAll <*p^<*x*>*> = SumAll <*<*x*>*> by FINSEQ_1:34
.= SumAll (<*<*x*>*>@) by MATRLIN:15
.= SumAll (<*p^<*x*>*>@) by A9,FINSEQ_1:34;
end;
suppose
A10: len p <> 0;
A11: len <*<*x*>*> = 1 & len <*p*> = 1 & len <*x*> = 1 by FINSEQ_1:40; then
A12: width <*<*x*>*> = 1 & width <*p*> = len p by MATRIX_0:20; then
A16: len (<*p*>@) = len p by MATRIX_0:def 6;
P5: width (<*p*>@) = 1 by A10,A11,A12,MATRIX_0:29; then
reconsider d1 = <*p*>@ as Matrix of len p,1,ExtREAL
by A10,A16,MATRIX_0:20;
A13: len (<*<*x*>*>@) = 1 by A12,MATRIX_0:54;
PP5: width (<*<*x*>*>@) = 1 by A11,A12,MATRIX_0:29; then
reconsider d2 = <*<*x*>*>@ as Matrix of 1,1,ExtREAL by A13,MATRIX_0:20;
len <*p^<*x*>*> = 1 by FINSEQ_1:40; then
A18: width <*p^<*x*>*> = len (p^<*x*>) by MATRIX_0:20
.= len p + 1 by A11,FINSEQ_1:22;
A19: (<*<*x*>*>@)@ = <*<*x*>*> by A11,A12,MATRIX_0:57;
width (<*p*>@) = width(<*<*x*>*>@) by P5,A11,A12,MATRIX_0:29; then
A21: (d1 ^ d2)@ = ((<*p*>@)@) ^^ ((<*<*x*>*>@)@) by MATRLIN:28
.= <*p*> ^^ <*<*x*>*> by A10,A11,A12,A19,MATRIX_0:57
.= <*p^<*x*>*> by A4,A6,FINSEQ_2:9
.= (<*p^<*x*>*>@)@ by A18,MATRIX_0:57;
A22: len ((<*p*>@) ^ (<*<*x*>*>@)) = len (<*p*>@) + len (<*<*x*>*>@)
by FINSEQ_1:22
.= width <*p*> + len (<*<*x*>*>@) by MATRIX_0:def 6
.= width <*p*> + width <*<*x*>*> by MATRIX_0:def 6
.= len (<*p^<*x*>*>@) by A12,A18,MATRIX_0:def 6;
B4: now let i be Nat;
assume i in dom <*p*>; then
i = 1 by FINSEQ_1:90;
hence not -infty in rng (<*p*>.i) by B3;
end;
B5: now let i be Nat;
assume i in dom <*<*x*>*>; then
i = 1 by FINSEQ_1:90;
hence not -infty in rng (<*<*x*>*>.i) by B3;
end;
dom <*p*> = Seg 1 by FINSEQ_1:38; then
1 in dom <*p*>; then
B6: not -infty in rng (<*p*>.1) by B4; then
T6: not -infty in rng p;
for x be object st x in dom (Sum d1) holds (Sum d1).x <> -infty
proof
let x be object;
assume P1: x in dom(Sum d1); then
reconsider i = x as Nat;
P2: (Sum d1).x = Sum(d1.i) by P1,Def5;
1 <= i & i <= len (Sum d1) by P1,FINSEQ_3:25; then
P3: 1 <= i & i <= len d1 by Def5; then
i in dom p by A16,FINSEQ_3:25; then
R10: p.i <> -infty by T6,FUNCT_1:3;
i in dom d1 by P3,FINSEQ_3:25; then
P4: d1.i = Line(d1,i) by MATRIX_0:60;
dom d1 = Seg len p by A16,FINSEQ_1:def 3; then
R2: Indices d1 = [: Seg len p, {1} :] by P5,FINSEQ_1:2,MATRIX_0:def 4;
R3: i in Seg len p by P3,A16;
for j be Nat st j in dom Line(d1,i) holds Line(d1,i).j <> -infty
proof
let j be Nat;
assume j in dom Line(d1,i); then
1 <= j & j <= len Line(d1,i) by FINSEQ_3:25; then
1 <= j & j <= width d1 by MATRIX_0:def 7; then
P6: j in Seg width d1; then
R4: [i,j] in [: Seg len p, {1}:] by P5,R3,FINSEQ_1:2,ZFMISC_1:def 2; then
[j,i] in Indices (d1@) by R2,MATRIX_0:def 6; then
consider F be FinSequence of ExtREAL such that
R7: F = (d1@).j & (d1@)*(j,i) = F.i by MATRIX_0:def 5;
F = <*p*>.j by A10,A12,R7,A11,MATRIX_0:57; then
F = <*p*>.1 by P5,P6,FINSEQ_1:2,TARSKI:def 1; then
R9: F = p;
Line(d1,i).j = (<*p*>@)*(i,j) by P6,MATRIX_0:def 7;
hence Line(d1,i).j <> -infty by R7,R9,R10,R2,R4,MATRIX_0:def 6;
end;
hence (Sum d1).x <> -infty by P2,P4,Th17;
end; then
B7: not -infty in rng Sum d1 by FUNCT_1:def 3;
for z be object st z in dom (Sum d2) holds (Sum d2).z <> -infty
proof
let z be object;
assume P1: z in dom(Sum d2); then
reconsider i = z as Nat;
P2: (Sum d2).z = Sum(d2.i) by P1,Def5;
1 <= i & i <= len (Sum d2) by P1,FINSEQ_3:25; then
P3: 1 <= i & i <= len d2 by Def5; then
R1: 1 <= i & i <= len <*x*> by A13,FINSEQ_1:40; then
i in dom <*x*> by FINSEQ_3:25; then
R10: <*x*>.i <> -infty by B3,FUNCT_1:3;
i in dom d2 by P3,FINSEQ_3:25; then
P4: d2.i = Line(d2,i) by MATRIX_0:60;
dom d2 = Seg len <*x*> by A13,FINSEQ_1:def 3,40; then
R2: Indices d2 = [: Seg len <*x*>, {1} :] by PP5,FINSEQ_1:2,MATRIX_0:def 4;
R3: i in Seg len <*x*> by R1;
for j be Nat st j in dom Line(d2,i) holds Line(d2,i).j <> -infty
proof
let j be Nat;
assume j in dom Line(d2,i); then
1 <= j & j <= len Line(d2,i) by FINSEQ_3:25; then
1 <= j & j <= width d2 by MATRIX_0:def 7; then
P6: j in Seg width d2; then
R4: [i,j] in [: Seg len <*x*>, {1} :]
by PP5,R3,FINSEQ_1:2,ZFMISC_1:def 2; then
[j,i] in Indices(d2@) by R2,MATRIX_0:def 6; then
consider F be FinSequence of ExtREAL such that
R7: F = (d2@).j & (d2@)*(j,i) = F.i by MATRIX_0:def 5;
F = <*<*x*>*>.j by A12,R7,A11,MATRIX_0:57; then
F = <*<*x*>*>.1 by PP5,P6,FINSEQ_1:2,TARSKI:def 1; then
R9: F = <*x*>;
Line(d2,i).j = ( <*<*x*>*>@ )*(i,j) by P6,MATRIX_0:def 7;
hence Line(d2,i).j <> -infty by R7,R9,R10,R2,R4,MATRIX_0:def 6;
end;
hence (Sum d2).z <> -infty by P2,P4,Th17;
end; then
B8: not -infty in rng Sum d2 by FUNCT_1:def 3;
thus SumAll <*p^<*x*>*>
= SumAll (<*p*> ^^ <*<*x*>*>) by A4,A6,FINSEQ_2:9
.= SumAll (<*p*>) + SumAll <*<*x*>*> by A11,B4,B5,Th25
.= SumAll (<*p*>@) + SumAll (<*<*x*>*>@)
by A3,B6,MATRLIN:15
.= Sum (Sum d1 ^ Sum d2) by B7,B8,EXTREAL1:10
.= SumAll (d1 ^ d2) by Th23
.= SumAll (<*p^<*x*>*>@) by A22,A21,MATRIX_0:53;
end;
end;
A23:x[<*>(ExtREAL)]
proof
reconsider M1 = <* <*>(ExtREAL) *> as Matrix of 1,0,ExtREAL
by MATRIX_0:14;
len M1 = 1 by MATRIX_0:def 2; then
width M1 = 0 by MATRIX_0:20; then
A24:len (M1@) = 0 by MATRIX_0:def 6;
SumAll M1 = 0 by Th22;
hence thesis by A24,Th21;
end;
for p be FinSequence of ExtREAL holds x[p] from FINSEQ_2:sch 2(A23,A2);
hence thesis by B0;
end;
theorem Th27:
for p be ext-real number, M be Matrix of ExtREAL st
(for i be Nat st i in dom M holds not p in rng (M.i)) holds
(for j be Nat st j in dom (M@) holds not p in rng((M@).j))
proof
let p be ext-real number;
let M be Matrix of ExtREAL;
assume
A1: for i be Nat st i in dom M holds not p in rng (M.i);
hereby let j be Nat;
assume A2: j in dom(M@); then
A3: M@.j = Line(M@,j) by MATRIX_0:60;
j in Seg len (M@) by A2,FINSEQ_1:def 3; then
j in Seg width M by MATRIX_0:def 6; then
A5: Line(M@,j) = Col(M,j) by MATRIX_0:59;
for v be object st v in dom Line(M@,j) holds Line(M@,j).v <> p
proof
let v be object;
assume A6: v in dom Line(M@,j); then
reconsider i = v as Element of NAT;
1 <= i & i <= len Line(M@,j) by A6,FINSEQ_3:25; then
1 <= i & i <= width (M@) by MATRIX_0:def 7; then
i in Seg width (M@); then
[j,i] in [:dom(M@),Seg width(M@):] by A2,ZFMISC_1:def 2; then
[j,i] in Indices (M@) by MATRIX_0:def 4; then
A7: [i,j] in Indices M by MATRIX_0:def 6; then
A8: i in dom M & j in dom (M.i) by MATRPROB:13; then
Line(M@,j).v = M*(i,j) by A5,MATRIX_0:def 8; then
Line(M@,j).v = (M.i).j by A7,MATRPROB:14; then
Line(M@,j).v in rng (M.i) by A8,FUNCT_1:3;
hence Line(M@,j).v <> p by A1,A7,MATRPROB:13;
end;
hence not p in rng (M@.j) by A3,FUNCT_1:def 3;
end;
end;
theorem Th28:
for M be Matrix of ExtREAL st
(for i be Nat st i in dom M holds not -infty in rng (M.i))
holds SumAll M = SumAll(M@)
proof
let M be Matrix of ExtREAL;
assume
A0: for i be Nat st i in dom M holds not -infty in rng (M.i);
defpred x[Nat] means for M be Matrix of ExtREAL st
len M = $1 & (for i be Nat st i in dom M holds not -infty in rng (M.i))
holds SumAll M = SumAll (M@);
A1:for n be Nat st x[n] holds x[n+1]
proof
let n be Nat;
assume
A2: for M be Matrix of ExtREAL st
len M = n &
(for i be Nat st i in dom M holds not -infty in rng (M.i))
holds SumAll M = SumAll (M@);
thus for M be Matrix of ExtREAL st
len M = n+1 &
(for i be Nat st i in dom M holds not -infty in rng (M.i))
holds SumAll M = SumAll (M@)
proof
let M be Matrix of ExtREAL;
assume
A3: len M = n+1 &
(for i be Nat st i in dom M holds not -infty in rng (M.i)); then
a3: M <> {};
per cases;
suppose
A4: n = 0;
1 <= len M by A3,NAT_1:11; then
A5: not -infty in rng (M.1) by A3,FINSEQ_3:25;
M = <*M.1*> by A3,A4,FINSEQ_1:40;
hence thesis by A5,Th26;
end;
suppose
A30: n > 0;
reconsider M9 = M as Matrix of n+1,width M,ExtREAL by A3,MATRIX_0:20;
reconsider M1 = M.(n+1) as FinSequence of ExtREAL;
reconsider w = Del(M9,n+1) as Matrix of n,width M,ExtREAL by MATRLIN:3;
V1: 1 <= n+1 by NAT_1:11; then
M.(n+1) = Line(M,n+1) by A3,FINSEQ_3:25,MATRIX_0:60; then
Y11: len M1 = width M by MATRIX_0:def 7; then
reconsider r = <*M1*> as Matrix of 1,width M,ExtREAL;
A31: width w = width M9 by A30,MATRLIN:2
.= width r by MATRLIN:2;
A32: len (w@) = width w by MATRIX_0:def 6
.= len (r@) by A31,MATRIX_0:def 6;
A33: len (Del(M,n+1)) = n by A3,PRE_POLY:12;
T5: not -infty in rng M1 by V1,A3,FINSEQ_3:25;
for v be object st v in dom (Sum w) holds (Sum w).v <> -infty
proof
let v be object;
assume P1: v in dom (Sum w); then
reconsider i = v as Nat;
P2: (Sum w).v = Sum(w.i) by P1,Def5;
1 <= i & i <= len (Sum w) by P1,FINSEQ_3:25; then
P3: 1 <= i & i <= len w by Def5; then
S0: 1 <= i & i <= n+1 by A33,NAT_1:12;
R1: i in dom w by P3,FINSEQ_3:25; then
P4: w.i = Line(w,i) by MATRIX_0:60;
for j be Nat st j in dom Line(w,i) holds Line(w,i).j <> -infty
proof
let j be Nat;
assume j in dom Line(w,i); then
1 <= j & j <= len Line(w,i) by FINSEQ_3:25; then
1 <= j & j <= width w by MATRIX_0:def 7; then
P6: j in Seg width w; then
[i,j] in [:dom w,Seg width w:] by R1,ZFMISC_1:def 2; then
[i,j] in Indices w by MATRIX_0:def 4; then
consider F be FinSequence of ExtREAL such that
R7: F = w.i & w*(i,j) = F.j by MATRIX_0:def 5;
M <> {} by A3; then
M = Del(M,len M) ^ <*M.(len M)*> by PRE_POLY:13; then
M.i = w.i by A3,R1,FINSEQ_1:def 7; then
S2: not -infty in rng F by R7,A3,S0,FINSEQ_3:25;
len F = width w by P4,R7,MATRIX_0:def 7; then
j in dom F by P6,FINSEQ_1:def 3; then
F.j in rng F by FUNCT_1:3;
hence Line(w,i).j <> -infty by R7,S2,P6,MATRIX_0:def 7;
end;
hence (Sum w).v <> -infty by P2,P4,Th17;
end; then
L1: not -infty in rng Sum w by FUNCT_1:def 3;
for v be object st v in dom (Sum r) holds (Sum r).v <> -infty
proof
let v be object;
assume P1: v in dom (Sum r); then
reconsider i = v as Nat;
P2: (Sum r).v = Sum(r.i) by P1,Def5;
1 <= i & i <= len (Sum r) by P1,FINSEQ_3:25; then
P3: 1 <= i & i <= len r by Def5; then
1 <= i & i <= 1 by FINSEQ_1:40; then
i = 1 by XXREAL_0:1; then
n+i in Seg (n+1) by FINSEQ_1:4; then
S0: n+i in dom M by A3,FINSEQ_1:def 3;
R1: i in dom r by P3,FINSEQ_3:25; then
P4: r.i = Line(r,i) by MATRIX_0:60;
for j be Nat st j in dom Line(r,i) holds Line(r,i).j <> -infty
proof
let j be Nat;
assume j in dom Line(r,i); then
1 <= j & j <= len Line(r,i) by FINSEQ_3:25; then
1 <= j & j <= width r by MATRIX_0:def 7; then
P6: j in Seg width r; then
[i,j] in [:dom r, Seg width r:] by R1,ZFMISC_1:def 2; then
[i,j] in Indices r by MATRIX_0:def 4; then
consider F be FinSequence of ExtREAL such that
R7: F = r.i & r*(i,j) = F.j by MATRIX_0:def 5;
M <> {} by A3; then
M = w ^ <*M.(n+1)*> by A3,PRE_POLY:13; then
M.(n + i) = r.i by A33,R1,FINSEQ_1:def 7; then
S2: not -infty in rng F by R7,A3,S0;
len F = width r by P4,R7,MATRIX_0:def 7; then
j in dom F by P6,FINSEQ_1:def 3; then
F.j in rng F by FUNCT_1:3;
hence Line(r,i).j <> -infty by R7,S2,P6,MATRIX_0:def 7;
end;
hence (Sum r).v <> -infty by P2,P4,Th17;
end; then
T3: not -infty in rng Sum r by FUNCT_1:def 3;
T4: for i be Nat st i in dom (Del(M,n+1)) holds
not -infty in rng((Del(M,n+1)).i)
proof
let i be Nat;
assume R1: i in dom(Del(M,n+1)); then
P4: w.i = Line(w,i) by MATRIX_0:60;
1 <= i & i <= len w by R1,FINSEQ_3:25; then
S0: 1 <= i & i <= n+1 by A33,NAT_1:12;
for v be object st v in dom Line(w,i) holds Line(w,i).v <> -infty
proof
let v be object;
assume TT0:v in dom Line(w,i); then
reconsider j=v as Nat;
1 <= j & j <= len Line(w,i) by TT0,FINSEQ_3:25; then
1 <= j & j <= width w by MATRIX_0:def 7; then
P6: j in Seg width w; then
[i,j] in [:dom w, Seg width w:] by R1,ZFMISC_1:def 2; then
[i,j] in Indices w by MATRIX_0:def 4; then
consider F be FinSequence of ExtREAL such that
R7: F = w.i & w*(i,j) = F.j by MATRIX_0:def 5;
M <> {} by A3; then
M = Del(M,len M) ^ <*M.(len M)*> by PRE_POLY:13; then
M.i = w.i by A3,R1,FINSEQ_1:def 7; then
S2: not -infty in rng F by R7,A3,S0,FINSEQ_3:25;
len F = width w by P4,R7,MATRIX_0:def 7; then
j in dom F by P6,FINSEQ_1:def 3; then
F.j in rng F by FUNCT_1:3;
hence Line(w,i).v <> -infty by R7,S2,P6,MATRIX_0:def 7;
end;
hence not -infty in rng((Del(M,n+1)).i) by P4,FUNCT_1:def 3;
end;
M <> {} by A3; then
M = Del(M,len M) ^ <*M.(len M)*> by PRE_POLY:13; then
H1: M@ = (w@) ^^ (<*M.(n+1)*>)@ by A3,A31,MATRLIN:28; then
Q4: dom (M@) = dom (w@) /\ dom((<*M.(n+1)*>)@) by PRE_POLY:def 4;
dom (w@) = Seg len (w@) by FINSEQ_1:def 3; then
dom (w@) = Seg width w by MATRIX_0:def 6; then
dom (w@) = Seg len (<*M.(n+1)*>@) by A31,MATRIX_0:def 6; then
Z0: dom (w@) = dom (<*M.(n+1)*>@) by FINSEQ_1:def 3;
Y2: len <*M.(n+1)*> = 1 by FINSEQ_1:40; then
Z2: width <*M.(n+1)*> = width M by Y11,MATRIX_0:20;
T6: for i be Nat st i in dom (w@) holds not -infty in rng (w@.i)
proof
let i be Nat;
assume R1: i in dom (w@); then
P4: w@.i = Line(w@,i) by MATRIX_0:60;
1 <= i & i <= len (w@) by R1,FINSEQ_3:25; then
1 <= i & i <= width w by MATRIX_0:def 6; then
1 <= width w by XXREAL_0:2; then
V5: 1 <= width M by A30,MATRLIN:2;
for v be object st v in dom Line(w@,i) holds Line(w@,i).v <> -infty
proof
let v be object;
assume TT0:v in dom Line(w@,i); then
reconsider j = v as Nat;
1 <= j & j <= len Line(w@,i) by TT0,FINSEQ_3:25; then
1 <= j & j <= width (w@) by MATRIX_0:def 7; then
P6: j in Seg width (w@); then
[i,j] in [:dom (w@), Seg width(w@):] by R1,ZFMISC_1:def 2; then
[i,j] in Indices (w@) by MATRIX_0:def 4; then
consider F be FinSequence of ExtREAL such that
R7: F = (w@).i & (w@)*(i,j) = F.j by MATRIX_0:def 5;
width (<*M.(n+1)*>@) = len <*M.(n+1)*> by V5,Z2,MATRIX_0:29; then
1 in Seg width (<*M.(n+1)*>@) by Y2; then
[i,1] in [:dom(<*M.(n+1)*>@), Seg width(<*M.(n+1)*>@):]
by Z0,R1,ZFMISC_1:87; then
[i,1] in Indices (<*M.(n+1)*>@) by MATRIX_0:def 4; then
consider G be FinSequence of ExtREAL such that
Q7: G = (<*M.(n+1)*>@).i & (<*M.(n+1)*>@)*(i,1) = G.1 by MATRIX_0:def 5;
(M@).i = F^G by R7,H1,Z0,Q4,R1,Q7,PRE_POLY:def 4; then
not -infty in rng (F^G) by Z0,Q4,R1,A3,Th27; then
not -infty in (rng F \/ rng G) by FINSEQ_1:31; then
S2: not -infty in rng F & not -infty in rng G by XBOOLE_0:def 3;
len F = width (w@) by P4,R7,MATRIX_0:def 7; then
j in dom F by P6,FINSEQ_1:def 3; then
F.j in rng F by FUNCT_1:3;
hence Line(w@,i).v <> -infty by R7,S2,P6,MATRIX_0:def 7;
end;
hence not -infty in rng (w@.i) by P4,FUNCT_1:def 3;
end;
T7: for i be Nat st i in dom (r@) holds not -infty in rng (r@.i)
proof
let i be Nat;
assume R1: i in dom (r@); then
P4: r@.i = Line(r@,i) by MATRIX_0:60;
1 <= i & i <= len (r@) by R1,FINSEQ_3:25; then
1 <= i & i <= width r by MATRIX_0:def 6; then
1 <= width r by XXREAL_0:2; then
M1: 1 <= width M9 by MATRLIN:2;
for v be object st v in dom Line(r@,i) holds Line(r@,i).v <> -infty
proof
let v be object;
assume TT0: v in dom Line(r@,i); then
reconsider j = v as Nat;
1 <= j & j <= len Line(r@,i) by TT0,FINSEQ_3:25; then
1 <= j & j <= width (r@) by MATRIX_0:def 7; then
P6: j in Seg width (r@); then
[i,j] in [:dom(r@),Seg width(r@):] by R1,ZFMISC_1:def 2; then
[i,j] in Indices (r@) by MATRIX_0:def 4; then
consider G be FinSequence of ExtREAL such that
R7: G = (r@).i & (r@)*(i,j) = G.j by MATRIX_0:def 5;
1 <= width w by A30,M1,MATRLIN:2; then
width (w@) = len w by MATRIX_0:29; then
n in Seg width (w@) by A30,A33,FINSEQ_1:3; then
[i,n] in [:dom(w@),Seg width(w@):] by Z0,R1,ZFMISC_1:87; then
[i,n] in Indices (w@) by MATRIX_0:def 4; then
consider F be FinSequence of ExtREAL such that
Q7: F = (w@).i & (w@)*(i,n) = F.n by MATRIX_0:def 5;
(M@).i = F^G by R7,H1,Z0,Q4,R1,Q7,PRE_POLY:def 4; then
not -infty in rng (F^G) by Z0,Q4,R1,A3,Th27; then
not -infty in (rng F \/ rng G) by FINSEQ_1:31; then
S2: not -infty in rng F & not -infty in rng G by XBOOLE_0:def 3;
len G = width (r@) by P4,R7,MATRIX_0:def 7; then
j in dom G by P6,FINSEQ_1:def 3; then
G.j in rng G by FUNCT_1:3;
hence Line(r@,i).v <> -infty by S2,R7,P6,MATRIX_0:def 7;
end;
hence not -infty in rng (r@.i) by P4,FUNCT_1:def 3;
end;
thus SumAll M = SumAll (w ^ r) by A3,PRE_POLY:13,a3
.= Sum (Sum w ^ Sum r) by Th23
.= SumAll (Del(M,n+1)) + SumAll r by T3,L1,EXTREAL1:10
.= SumAll (Del(M,n+1)@) + SumAll r by A2,A33,T4
.= SumAll (Del(M,n+1)@) + SumAll (r@) by T5,Th26
.= SumAll ((w@) ^^ (r@)) by A32,Th25,T6,T7
.= SumAll ((w ^ r)@) by A31,MATRLIN:28
.= SumAll (M@) by A3,PRE_POLY:13,a3;
end;
end;
end;
A34:
x[0]
proof
let M be Matrix of ExtREAL;
assume
A35: len M = 0 & (for i be Nat st i in dom M holds not -infty in rng (M.i));
then width M = 0 by MATRIX_0:def 3;
then
A36:len (M@) = 0 by MATRIX_0:def 6;
thus SumAll M = 0 by A35,Th21
.= SumAll (M@) by A36,Th21;
end;
for n be Nat holds x[n] from NAT_1:sch 2(A34,A1);
then x[len M];
hence thesis by A0;
end;
begin :: Definition of pre-measure
registration
let x be object;
cluster <*x*> -> disjoint_valued;
correctness
proof
now let i,j be object;
assume A3: i<>j;
per cases;
suppose i in dom <*x*>; then
i in {1} by FINSEQ_1:2,38; then
i = 1 by TARSKI:def 1; then
not j in {1} by A3,TARSKI:def 1; then
not j in dom <*x*> by FINSEQ_1:2,38; then
<*x*>.j = {} by FUNCT_1:def 2;
hence <*x*>.i misses <*x*>.j by XBOOLE_1:65;
end;
suppose not i in dom <*x*>; then
<*x*>.i = {} by FUNCT_1:def 2;
hence <*x*>.i misses <*x*>.j by XBOOLE_1:65;
end;
end;
hence <*x*> is disjoint_valued by PROB_2:def 2;
end;
end;
theorem
for X be set, S be with_empty_element semi-diff-closed cap-closed
Subset-Family of X, F be FinSequence of S,
G be Element of S
ex H be disjoint_valued FinSequence of S st G \ Union F = Union H
proof
let X be set, S be with_empty_element semi-diff-closed cap-closed
Subset-Family of X, F be FinSequence of S,
G be Element of S;
defpred P[Nat] means
for f be FinSequence of S st len f = $1 holds
ex H be disjoint_valued FinSequence of S st G \ Union f = Union H;
for f be FinSequence of S st len f = 0 holds
ex H be disjoint_valued FinSequence of S st G \ Union f = Union H
proof
let f be FinSequence of S;
assume len f = 0; then
f = {}; then
rng f = {}; then
A4: Union f = {} by CARD_3:def 4,ZFMISC_1:2;
A5: rng <*G*> = {G} by FINSEQ_1:38;
reconsider H = <*G*> as disjoint_valued FinSequence of S;
take H;
union rng H = G by A5,ZFMISC_1:25;
hence G \ Union f = Union H by A4,CARD_3:def 4;
end; then
A6:P[0];
A7:for i be Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume A8: P[i];
now let f be FinSequence of S;
assume A9: len f = i+1; then
len (f|i) = i by NAT_1:11,FINSEQ_1:59; then
consider h be disjoint_valued FinSequence of S such that
A12: G \ Union(f|i) = Union h by A8;
A10: f = (f|i)^<*f.(i+1)*> by A9,FINSEQ_3:55; then
reconsider f1 = <*f.(i+1)*> as FinSequence of S by FINSEQ_1:36;
A11: Union f1 = union rng f1 by CARD_3:def 4
.= union {f.(i+1)} by FINSEQ_1:38 .= f.(i+1) by ZFMISC_1:25;
Union f = (Union(f|i)) \/ Union f1 by A10,ROUGHS_1:5; then
A13: G \ Union f = (G \ Union(f|i)) \ f.(i+1) by A11,XBOOLE_1:41
.= Union h \ f.(i+1) by A12;
deffunc F(Nat) = h.$1 \ f.(i+1);
consider V be FinSequence such that
A14: len V = len h
& for k be Nat st k in dom V holds V.k = F(k) from FINSEQ_1:sch 2;
A19: for k be Nat st k in dom V
ex D be disjoint_valued FinSequence of S st V.k = Union D
proof
let k be Nat;
assume A15: k in dom V;
k in dom h by A14,A15,FINSEQ_3:29; then
A16: h.k in rng h by FUNCT_1:3;
i+1 in Seg len f by A9,FINSEQ_1:4; then
i+1 in dom f by FINSEQ_1:def 3; then
f.(i+1) in rng f by FUNCT_1:3; then
consider D be disjoint_valued FinSequence of S such that
A18: h.k \ f.(i+1) = Union D by A16,SRINGS_3:def 1;
take D;
thus V.k = Union D by A15,A14,A18;
end;
defpred P[Nat,object] means
ex D be disjoint_valued FinSequence of S
st $2 = D & V.$1 = Union D;
P1: for k be Nat st k in Seg len V
ex x be object st P[k,x]
proof
let k be Nat;
assume k in Seg len V; then
k in dom V by FINSEQ_1:def 3; then
consider D be disjoint_valued FinSequence of S such that
P2: V.k = Union D by A19;
take D;
thus thesis by P2;
end;
consider FinS be FinSequence such that
P3: dom FinS = Seg len V
& for k be Nat st k in Seg len V holds P[k,FinS.k]
from FINSEQ_1:sch 1(P1);
now let a be object;
assume a in rng FinS; then
consider x be object such that
P4: x in dom FinS & a = FinS.x by FUNCT_1:def 3;
consider D be disjoint_valued FinSequence of S such that
P5: FinS.x = D & V.x = Union D by P3,P4;
thus a is FinSequence of S by P4,P5;
end; then
reconsider Y = rng FinS as FinSequenceSet of S by FINSEQ_2:def 3;
reconsider FinS as FinSequence of Y by FINSEQ_1:def 4;
H1: for n,m be Nat st n<>m holds union rng(FinS.n) misses union rng(FinS.m)
proof
let n,m be Nat;
assume H2: n<>m;
per cases;
suppose H3: n in dom FinS & m in dom FinS; then
consider D1 be disjoint_valued FinSequence of S such that
H4: FinS.n = D1 & V.n = Union D1 by P3;
consider D2 be disjoint_valued FinSequence of S such that
H5: FinS.m = D2 & V.m = Union D2 by H3,P3;
H6: V.n = union rng(FinS.n) & V.m = union rng(FinS.m)
by H4,H5,CARD_3:def 4;
n in dom V & m in dom V by H3,P3,FINSEQ_1:def 3; then
P15: V.n = h.n \ f.(i+1) & V.m = h.m \ f.(i+1) by A14; then
V.n misses h.m by XBOOLE_1:80,H2,PROB_2:def 2;
hence union rng(FinS.n) misses union rng(FinS.m) by H6,P15,XBOOLE_1:80;
end;
suppose not n in dom FinS or not m in dom FinS; then
FinS.n = {} or FinS.m = {} by FUNCT_1:def 2; then
rng(FinS.n) = {} or rng(FinS.m) = {};
hence union rng(FinS.n) misses union rng(FinS.m)
by ZFMISC_1:2,XBOOLE_1:65;
end;
end;
for n be Nat holds FinS.n is disjoint_valued
proof
let n be Nat;
per cases;
suppose not n in dom FinS;
hence FinS.n is disjoint_valued by FUNCT_1:def 2;
end;
suppose n in dom FinS; then
ex D be disjoint_valued FinSequence of S st
FinS.n = D & V.n = Union D by P3;
hence FinS.n is disjoint_valued;
end;
end; then
reconsider H= joined_FinSeq FinS as disjoint_valued FinSequence of S
by H1,Th14;
take H;
Union H = union rng H by CARD_3:def 4; then
X1: Union H = union union{rng(FinS.n) where n is Nat : n in dom FinS}
by Th15;
X2: G \ Union f = union rng h \ f.(i+1) by CARD_3:def 4,A13;
now let x be object;
assume B0: x in union rng h \ f.(i+1); then
consider A be set such that
B2: x in A & A in rng h by TARSKI:def 4;
consider k be object such that
B3: k in dom h & A = h.k by B2,FUNCT_1:def 3;
reconsider k as Nat by B3;
B4: k in dom V by A14,B3,FINSEQ_3:29;
B5: k in dom FinS by P3,FINSEQ_1:def 3,A14,B3; then
consider D be disjoint_valued FinSequence of S such that
B6: FinS.k = D & V.k = Union D by P3;
B7: V.k = union rng(FinS.k) by B6,CARD_3:def 4;
x in union rng h & not x in f.(i+1) by B0,XBOOLE_0:def 5; then
x in h.k \ f.(i+1) by B2,B3,XBOOLE_0:def 5; then
x in V.k by A14,B4; then
consider V be set such that
B8: x in V & V in rng(FinS.k) by B7,TARSKI:def 4;
rng(FinS.k) in {rng(FinS.n) where n is Nat : n in dom FinS} by B5; then
V in union {rng(FinS.n) where n is Nat : n in dom FinS}
by B8,TARSKI:def 4;
hence x in union union {rng(FinS.n) where n is Nat : n in dom FinS}
by B8,TARSKI:def 4;
end; then
B9: G \ Union f c= Union H by X1,X2,TARSKI:def 3;
now let x be object;
assume x in union union{rng(FinS.n) where n is Nat:n in dom FinS}; then
consider A be set such that
C1: x in A & A in union{rng(FinS.n) where n is Nat: n in dom FinS}
by TARSKI:def 4;
consider D1 be set such that
C2: A in D1 & D1 in {rng(FinS.n) where n is Nat: n in dom FinS}
by C1,TARSKI:def 4;
consider k be Nat such that
C3: D1 = rng(FinS.k) & k in dom FinS by C2;
consider D2 be disjoint_valued FinSequence of S such that
C4: FinS.k = D2 & V.k = Union D2 by C3,P3;
C5: k in dom V by C3,P3,FINSEQ_1:def 3; then
V.k = h.k \ f.(i+1) by A14; then
h.k \ f.(i+1) = union D1 by C3,C4,CARD_3:def 4; then
C6: x in (h.k \ f.(i+1)) by C1,C2,TARSKI:def 4; then
C7: x in h.k & not x in f.(i+1) by XBOOLE_0:def 5;
dom V = dom h by A14,FINSEQ_3:29; then
h.k in rng h by C5,FUNCT_1:3; then
x in union rng h by C6,TARSKI:def 4;
hence x in (union rng h) \ f.(i+1) by C7,XBOOLE_0:def 5;
end; then
Union H c= G \ Union f by X1,X2,TARSKI:def 3;
hence G \ Union f = Union H by B9,XBOOLE_0:def 10;
end;
hence P[i+1];
end;
for i be Nat holds P[i] from NAT_1:sch 2(A6,A7); then
for f be FinSequence of S st len f = len F holds
ex H be disjoint_valued FinSequence of S st G \ Union f = Union H;
hence thesis;
end;
registration
let X be set, P be with_empty_element semi-diff-closed cap-closed
Subset-Family of X;
cluster disjoint_valued for sequence of P;
existence
proof
consider F be sequence of {{}} such that
A1: for n be Element of NAT holds F.n = {} by MEASURE1:16;
{{}} c= P by ZFMISC_1:31,SETFAM_1:def 8;
then reconsider F as sequence of P by FUNCT_2:7;
take F;
for x,y be object st x <> y holds F.x misses F.y
proof
let x,y be object;
assume x <> y;
per cases;
suppose x in dom F; then
F.x = {} by A1;
hence F.x misses F.y by XBOOLE_1:65;
end;
suppose not x in dom F; then
F.x = {} by FUNCT_1:def 2;
hence F.x misses F.y by XBOOLE_1:65;
end;
end;
hence F is disjoint_valued by PROB_2:def 2;
end;
end;
LM:
for X be set, P be non empty Subset-Family of X holds
P --> 0. is nonnegative & P --> 0. is additive & P --> 0. is zeroed
proof
let X be set, P be non empty Subset-Family of X;
set M = P --> 0.;
for A be Element of P holds 0. <= M.A;
hence P --> 0. is nonnegative by MEASURE1:def 2;
now let A,B be Element of P;
assume A misses B & A \/ B in P; then
reconsider D = A \/ B as Element of P;
M.A = 0. & M.B = 0. & M.D = 0. by FUNCOP_1:7;
hence M.(A \/ B) = (M.A) qua ExtReal + M.B;
end;
hence P --> 0. is additive by MEASURE1:def 3;
per cases;
suppose {} in P; then
(P --> 0.).{} = 0. by FUNCOP_1:7;
hence P --> 0. is zeroed by VALUED_0:def 19;
end;
suppose not {} in P; then
not {} in dom (P--> 0.); then
(P--> 0.).{} = 0 by FUNCT_1:def 2;
hence P --> 0. is zeroed by VALUED_0:def 19;
end;
end;
registration
let X be set, P be non empty Subset-Family of X;
cluster nonnegative additive zeroed for Function of P,ExtREAL;
existence
proof
reconsider M = P --> 0. as Function of P,ExtREAL;
take M;
thus thesis by LM;
end;
end;
registration
let X be set, P be with_empty_element Subset-Family of X;
cluster disjoint_valued for Function of NAT,P;
existence
proof
{} in P by SETFAM_1:def 8; then
reconsider F = NAT --> {} as Function of NAT,P by FUNCOP_1:46;
take F;
now let i,j be object;
assume i <> j;
per cases;
suppose i in dom F;
thus F.i misses F.j by XBOOLE_1:65;
end;
suppose not i in dom F;
thus F.i misses F.j by XBOOLE_1:65;
end;
end;
hence F is disjoint_valued by PROB_2:def 2;
end;
end;
definition
let X be set, P be with_empty_element Subset-Family of X;
mode pre-Measure of P ->
nonnegative zeroed Function of P,ExtREAL means :Def8:
( for F be disjoint_valued FinSequence of P st Union F in P
holds it.(Union F) = Sum(it*F) )
& ( for K be disjoint_valued Function of NAT,P st Union K in P
holds it.(Union K) <= SUM(it*K) );
existence
proof
reconsider M = P --> 0. as Function of P,ExtREAL;
( for x be Element of P holds 0.<= M.x) & M.{} = 0
by FUNCOP_1:7,SETFAM_1:def 8; then
reconsider M as nonnegative zeroed Function of P,ExtREAL
by MEASURE1:def 2,VALUED_0:def 19;
take M;
0 is Element of REAL by XREAL_0:def 1; then
reconsider m = P --> 0 as Function of P,REAL by FUNCOP_1:46;
A2:for F be disjoint_valued FinSequence of P st Union F in P
holds M.(Union F) = Sum(M*F)
proof
let F be disjoint_valued FinSequence of P;
assume Union F in P; then
A3: M.(Union F) = 0. by FUNCOP_1:7;
rng F c= P & dom M = P & dom m = P by FUNCT_2:def 1; then
A4: dom(M*F) = dom F & dom(m*F) = dom F by RELAT_1:27;
A7: Sum(M*F) = Sum(m*F) by MESFUNC3:2;
A8: m*F = F"P --> 0 by FUNCOP_1:19; then
dom F = F"P by A4,FUNCOP_1:13; then
Seg len F = F"P by FINSEQ_1:def 3; then
m*F = (len F) |-> 0 by A8,FINSEQ_2:def 2;
hence M.(Union F) = Sum(M*F) by A3,A7,RVSUM_1:81;
end;
for K be disjoint_valued Function of NAT,P st Union K in P
holds M.(Union K) <= SUM(M*K)
proof
let K be disjoint_valued Function of NAT,P;
assume Union K in P; then
A10:M.(Union K) = 0. by FUNCOP_1:7;
now let n be Element of NAT;
(M*K).n = M.(K.n) by FUNCT_2:15;
hence (M*K).n = 0. by FUNCOP_1:7;
end;
hence M.(Union K) <= SUM(M*K) by A10,MEASURE7:1;
end;
hence thesis by A2;
end;
end;
theorem
for X be with_empty_element set, F be FinSequence of X holds
ex G be Function of NAT,X st
(for i be Nat holds F.i = G.i) & Union F = Union G
proof
let X be with_empty_element set;
let F be FinSequence of X;
defpred P[Element of NAT,set] means
($1 in dom F implies F.$1 = $2) & (not $1 in dom F implies $2 = {});
A1:for i be Element of NAT ex y be Element of X st P[i,y]
proof
let i be Element of NAT;
per cases;
suppose A2: i in dom F; then
F.i in rng F & rng F c= X by FUNCT_1:3; then
reconsider y = F.i as Element of X;
take y;
thus P[i,y] by A2;
end;
suppose A3: not i in dom F;
reconsider y = {} as Element of X by SETFAM_1:def 8;
take y;
thus P[i,y] by A3;
end;
end;
consider G be Function of NAT,X such that
A4: for i be Element of NAT holds P[i,G.i] from FUNCT_2:sch 3(A1);
take G;
A5:now let i be Nat;
per cases;
suppose i in dom F;
hence F.i = G.i by A4;
end;
suppose not i in dom F;
reconsider j = i as Element of NAT by ORDINAL1:def 12;
P[j,G.j] by A4;
hence F.i = G.i by FUNCT_1:def 2;
end;
end;
B1:Union F = union rng F & Union G = union rng G by CARD_3:def 4;
now let x be object;
assume x in Union F; then
consider A be set such that
A7: x in A & A in rng F by B1,TARSKI:def 4;
consider k be object such that
A8: k in dom F & A = F.k by A7,FUNCT_1:def 3;
reconsider k as Nat by A8;
dom G = NAT by FUNCT_2:def 1; then
A = G.k & G.k in rng G by A5,A8,FUNCT_1:3;
hence x in Union G by A7,B1,TARSKI:def 4;
end; then
A9:Union F c= Union G by TARSKI:def 3;
now let x be object;
assume x in Union G; then
consider A be set such that
A10: x in A & A in rng G by B1,TARSKI:def 4;
consider k be object such that
A11: k in dom G & A = G.k by A10,FUNCT_1:def 3;
reconsider k as Nat by A11;
A12:now assume not k in dom F; then
F.k = {} by FUNCT_1:def 2;
hence contradiction by A5,A10,A11;
end;
A13:F.k = G.k by A5;
F.k in rng F by A12,FUNCT_1:3;
hence x in Union F by B1,A10,A11,A13,TARSKI:def 4;
end; then
Union G c= Union F by TARSKI:def 3;
hence thesis by A5,A9,XBOOLE_0:def 10;
end;
theorem
for X be non empty set, F be FinSequence of X, G be Function of NAT,X
st (for i be Nat holds F.i = G.i)
holds F is disjoint_valued iff G is disjoint_valued
proof
let X be non empty set, F be FinSequence of X, G be Function of NAT,X;
assume A1: for i be Nat holds F.i = G.i;
hereby assume
A2: F is disjoint_valued;
now let x,y be object;
assume A3: x <> y;
per cases;
suppose x in dom F & y in dom F; then
G.x = F.x & G.y = F.y by A1;
hence G.x misses G.y by A2,A3,PROB_2:def 2;
end;
suppose not x in dom F & x in dom G; then
F.x = {} & G.x = F.x by A1,FUNCT_1:def 2;
hence G.x misses G.y by XBOOLE_1:65;
end;
suppose not x in dom F & not x in dom G; then
G.x = {} by FUNCT_1:def 2;
hence G.x misses G.y by XBOOLE_1:65;
end;
suppose not y in dom F & y in dom G; then
F.y = {} & G.y = F.y by A1,FUNCT_1:def 2;
hence G.x misses G.y by XBOOLE_1:65;
end;
suppose not y in dom F & not y in dom G; then
G.y = {} by FUNCT_1:def 2;
hence G.x misses G.y by XBOOLE_1:65;
end;
end;
hence G is disjoint_valued by PROB_2:def 2;
end;
assume A8: G is disjoint_valued;
now let x,y be object;
assume A9: x <> y;
per cases;
suppose x in dom G & y in dom G; then
F.x = G.x & F.y = G.y by A1;
hence F.x misses F.y by A8,A9,PROB_2:def 2;
end;
suppose A10: not x in dom G or not y in dom G;
dom F c= NAT; then
dom F c= dom G by FUNCT_2:def 1; then
not x in dom F or not y in dom F by A10; then
F.x = {} or F.y = {} by FUNCT_1:def 2;
hence F.x misses F.y by XBOOLE_1:65;
end;
end;
hence F is disjoint_valued by PROB_2:def 2;
end;
theorem
for F be FinSequence of ExtREAL, G be ExtREAL_sequence
st (for i be Nat holds F.i = G.i)
holds F is nonnegative iff G is nonnegative
proof
let F be FinSequence of ExtREAL, G be ExtREAL_sequence;
assume
A1: for i be Nat holds F.i = G.i;
hereby assume A3: F is nonnegative;
now let i be object;
assume A4: i in dom G;
per cases;
suppose i in dom F; then
G.i = F.i by A1;
hence G.i >= 0 by A3,SUPINF_2:51;
end;
suppose not i in dom F; then
F.i = 0 by FUNCT_1:def 2;
hence G.i >= 0 by A1,A4;
end;
end;
hence G is nonnegative by SUPINF_2:52;
end;
assume A5: G is nonnegative;
now let i be object;
per cases;
suppose i in dom F; then
F.i = G.i by A1;
hence F.i >= 0 by A5,SUPINF_2:51;
end;
suppose not i in dom F;
hence F.i >= 0 by FUNCT_1:def 2;
end;
end;
hence F is nonnegative by SUPINF_2:51;
end;
LL1:
<*+infty*> is nonnegative & <*+infty*> is without-infty
proof
set F = <*+infty*>;
now let i be object;
per cases;
suppose i in dom F; then
i in Seg 1 by FINSEQ_1:38; then
i = 1 by TARSKI:def 1,FINSEQ_1:2;
hence F.i >= 0;
end;
suppose not i in dom F;
hence F.i >= 0 by FUNCT_1:def 2;
end;
end;
hence F is nonnegative by SUPINF_2:51;
hence F is without-infty;
end;
LL2:
<*-infty*> is nonpositive & <*-infty*> is without+infty
proof
set F = <*-infty*>;
now let i be object;
per cases;
suppose i in dom F; then
i in Seg 1 by FINSEQ_1:38; then
i = 1 by TARSKI:def 1,FINSEQ_1:2;
hence F.i <= 0;
end;
suppose not i in dom F;
hence F.i <= 0 by FUNCT_1:def 2;
end;
end;
hence F is nonpositive by MESFUNC5:8;
hence F is without+infty;
end;
registration
cluster nonnegative for FinSequence of ExtREAL;
existence by LL1;
cluster without-infty for FinSequence of ExtREAL;
existence by LL1;
cluster nonpositive for FinSequence of ExtREAL;
existence by LL2;
cluster without+infty for FinSequence of ExtREAL;
existence by LL2;
cluster nonnegative -> without-infty for FinSequence of ExtREAL;
correctness;
cluster nonpositive -> without+infty for FinSequence of ExtREAL;
correctness;
end;
registration
let X,Y be non empty set, F be without-infty Function of Y,ExtREAL,
G be Function of X,Y;
cluster F*G -> without-infty for Function of X,ExtREAL;
correctness
proof
for x be object holds -infty < (F*G).x
proof
let x be object;
per cases;
suppose x in dom (F*G); then
(F*G).x = F.(G.x) by FUNCT_1:12;
hence -infty < (F*G).x by MESFUNC5:def 5;
end;
suppose not x in dom (F*G);
hence -infty < (F*G).x by FUNCT_1:def 2;
end;
end;
hence thesis by MESFUNC5:def 5;
end;
end;
registration
let X,Y be non empty set, F be nonnegative Function of Y,ExtREAL,
G be Function of X,Y;
cluster F*G -> nonnegative for Function of X,ExtREAL;
correctness by MEASURE1:25;
end;
theorem Th33:
for a be R_eal holds Sum <*a*> = a
proof
let a be R_eal;
consider f be sequence of ExtREAL such that
A1: Sum <*a*> = f.(len <*a*>) & f.0 = 0. &
for i be Nat st i < len <*a*> holds f.(i+1) = f.i+ <*a*>.(i+1)
by EXTREAL1:def 2;
A2:len <*a*> = 1 by FINSEQ_1:39;
f.(0+1) = f.0 + <*a*>.(0+1) by A1
.= 0 + a by A1;
hence Sum <*a*> = a by A1,A2,XXREAL_3:4;
end;
theorem Th34:
for F be FinSequence of ExtREAL, k be Nat
holds (F is without-infty implies F|k is without-infty)
& (F is without+infty implies F|k is without+infty)
proof
let F be FinSequence of ExtREAL, k be Nat;
hereby assume A1: F is without-infty;
now assume -infty in rng(F|k); then
consider i be Element of NAT such that
A2: i in dom(F|k) & -infty = (F|k).i by PARTFUN1:3;
dom(F|k) c= dom F by RELAT_1:60; then
i in dom F & (F|k).i = F.i by A2,FUNCT_1:47; then
-infty in rng F by A2,FUNCT_1:3;
hence contradiction by A1,MESFUNC5:def 3;
end;
hence F|k is without-infty by MESFUNC5:def 3;
end;
assume A3: F is without+infty;
now assume +infty in rng(F|k); then
consider i be Element of NAT such that
A4: i in dom(F|k) & +infty = (F|k).i by PARTFUN1:3;
dom(F|k) c= dom F by RELAT_1:60; then
i in dom F & (F|k).i = F.i by A4,FUNCT_1:47; then
+infty in rng F by A4,FUNCT_1:3;
hence contradiction by A3,MESFUNC5:def 4;
end;
hence F|k is without+infty by MESFUNC5:def 4;
end;
theorem Th35:
for F be without-infty FinSequence of ExtREAL, G be ExtREAL_sequence
st (for i be Nat holds F.i = G.i)
holds for i be Nat holds Sum(F|i) = (Partial_Sums G).i
proof
let F be without-infty FinSequence of ExtREAL, G be ExtREAL_sequence;
assume A1: for i be Nat holds F.i = G.i;
hereby let i be Nat;
defpred P[Nat] means Sum(F|$1) = (Partial_Sums G).$1;
A3: ex f0 be sequence of ExtREAL st
Sum(F|0) = f0.(len (F|0)) & f0.0 = 0.
& for i be Nat st i < len (F|0) holds f0.(i+1)= f0.i+(F|0).(i+1)
by EXTREAL1:def 2;
not 0 in Seg len F by FINSEQ_1:1; then
not 0 in dom F by FINSEQ_1:def 3; then
F.0 = 0 by FUNCT_1:def 2; then
G.0 = 0 by A1; then
A4: P[0] by A3,MESFUNC9:def 1;
A5: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A6: P[k];
F|k is without-infty by Th34; then
A7: not -infty in rng(F|k) by MESFUNC5:def 3;
A8: now assume -infty in rng <*F.(k+1)*>; then
-infty in { F.(k+1) } by FINSEQ_1:39; then
A9: F.(k+1) = -infty by TARSKI:def 1;
per cases;
suppose k+1 in dom F; then
F.(k+1) in rng F by FUNCT_1:3;
hence contradiction by A9,MESFUNC5:def 3;
end;
suppose not k+1 in dom F;
hence contradiction by A9,FUNCT_1:def 2;
end;
end;
per cases;
suppose k+1 <= len F; then
F|(k+1) = F|k ^ <*F.(k+1)*> by NAT_1:13,FINSEQ_5:83; then
Sum(F|(k+1)) = Sum(F|k) + Sum(<*F.(k+1)*>) by A7,A8,EXTREAL1:10
.= (Partial_Sums G).k + F.(k+1) by A6,Th33
.= (Partial_Sums G).k + G.(k+1) by A1;
hence P[k+1] by MESFUNC9:def 1;
end;
suppose A10: k+1 > len F; then
A11: F|k = F & F|(k+1) = F by NAT_1:13,FINSEQ_1:58;
not k+1 in dom F by A10,FINSEQ_3:25; then
F.(k+1) = 0 by FUNCT_1:def 2; then
G.(k+1) = 0 by A1; then
(Partial_Sums G).(k+1) = (Partial_Sums G).k + 0 by MESFUNC9:def 1;
hence P[k+1] by A6,A11,XXREAL_3:4;
end;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A4,A5);
hence Sum(F|i) = (Partial_Sums G).i;
end;
end;
theorem
for F be without-infty FinSequence of ExtREAL, G be ExtREAL_sequence
st (for i be Nat holds F.i = G.i)
holds G is summable & Sum F = Sum G
proof
let F be without-infty FinSequence of ExtREAL, G be ExtREAL_sequence;
assume A1: for i be Nat holds F.i = G.i; then
A2:Sum(F|len F) = (Partial_Sums G).(len F) by Th35;
defpred P[Nat] means Sum F = (Partial_Sums G).(len F + $1);
B1:P[0] by A2,FINSEQ_1:58;
B2:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A3: P[k];
len F < len F + (k+1) by NAT_1:11,19; then
not len F + k+1 in dom F by FINSEQ_3:25; then
F.(len F + k+1) = 0 by FUNCT_1:def 2; then
A4: G.(len F + k+1) = 0 by A1;
(Partial_Sums G).(len F + (k+1))
= (Partial_Sums G).(len F + k) + G.(len F + k + 1) by MESFUNC9:def 1
.= (Partial_Sums G).(len F + k) by A4,XXREAL_3:4;
hence P[k+1] by A3;
end;
A5:for k be Nat holds P[k] from NAT_1:sch 2(B1,B2);
hereby
per cases by XXREAL_0:14;
suppose Sum F in REAL; then
reconsider r = Sum F as Real;
B1: for p be Real st 0<p ex n be Nat st for m be Nat st n<=m
holds |.(Partial_Sums G).m - r qua ExtReal .| < p
proof
let p be Real;
assume A6: 0 < p;
take n = len F;
now let m be Nat;
assume len F <= m; then
reconsider k = m - n as Nat by NAT_1:21;
m = n + k; then
(Partial_Sums G).m = Sum F by A5;
hence |. (Partial_Sums G).m - r qua ExtReal .| < p
by A6,XXREAL_3:7,EXTREAL1:16;
end;
hence thesis;
end; then
B2: Partial_Sums G is convergent_to_finite_number by MESFUNC5:def 8;
hence G is summable by MESFUNC9:def 2;
lim Partial_Sums G = Sum F by B1,B2,MESFUNC5:def 12;
hence Sum F = Sum G by MESFUNC9:def 3;
end;
suppose A7: Sum F = +infty;
now let g be Real;
assume 0 < g;
thus ex n be Nat st
for m be Nat st n <= m holds g <= (Partial_Sums G).m
proof
take n = len F;
hereby let m be Nat;
assume n <= m; then
reconsider k = m - n as Nat by NAT_1:21;
m = n + k; then
(Partial_Sums G).m = +infty by A5,A7;
hence g <= (Partial_Sums G).m by XXREAL_0:3;
end;
end;
end; then
B5: Partial_Sums G is convergent_to_+infty by MESFUNC5:def 9;
hence G is summable by MESFUNC9:def 2;
lim Partial_Sums G = Sum F by A7,B5,MESFUNC5:def 12;
hence Sum F = Sum G by MESFUNC9:def 3;
end;
suppose A8: Sum F = -infty;
now let g be Real;
assume g < 0;
thus ex n be Nat st
for m be Nat st n <= m holds (Partial_Sums G).m <= g
proof
take n = len F;
hereby let m be Nat;
assume n <= m; then
reconsider k = m - n as Nat by NAT_1:21;
m = n + k; then
(Partial_Sums G).m = -infty by A5,A8;
hence (Partial_Sums G).m <= g by XXREAL_0:5;
end;
end;
end; then
B8: Partial_Sums G is convergent_to_-infty by MESFUNC5:def 10;
hence G is summable by MESFUNC9:def 2;
lim Partial_Sums G = Sum F by A8,B8,MESFUNC5:def 12;
hence Sum F = Sum G by MESFUNC9:def 3;
end;
end;
end;
theorem
for X be set, S be with_empty_element semi-diff-closed cap-closed
Subset-Family of X,
F be disjoint_valued FinSequence of S,
R be non empty preBoolean Subset-Family of X
st S c= R & Union F in R
holds for i be Nat holds Union (F|i) in R
proof
let X be set,
S be with_empty_element semi-diff-closed cap-closed Subset-Family of X,
F be disjoint_valued FinSequence of S,
R be non empty preBoolean Subset-Family of X;
assume A1: S c= R & Union F in R;
defpred P[Nat] means Union (F|$1) in R;
union rng (F|0) = {} by ZFMISC_1:2; then
Union (F|0) = {} by CARD_3:def 4; then
A3:P[0] by FINSUB_1:7;
A4:for i be Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume A5: P[i];
per cases;
suppose i >= len F; then
F|i = F & F|(i+1) = F by NAT_1:12,FINSEQ_1:58;
hence P[i+1] by A5;
end;
suppose i < len F; then
A8: i+1 <= len F by NAT_1:13;
set F1 = F|(i+1);
A9: F1|i = F|i by NAT_1:12,FINSEQ_1:82;
F1 = F1|i ^ <*F1.(i+1)*> by A8,FINSEQ_1:17,FINSEQ_3:55; then
rng F1 = rng(F1|i) \/ rng <*F1.(i+1)*> by FINSEQ_1:31; then
rng F1 = rng(F|i) \/ {F1.(i+1)} by A9,FINSEQ_1:38; then
rng F1 = rng(F|i) \/ {F.(i+1)} by FINSEQ_3:112; then
union rng F1 = union rng(F|i) \/ union {F.(i+1)} by ZFMISC_1:78; then
Union F1 = union rng(F|i) \/ union {F.(i+1)} by CARD_3:def 4; then
Union F1 = Union (F|i) \/ union {F.(i+1)} by CARD_3:def 4; then
A11: Union F1 = Union (F|i) \/ F.(i+1) by ZFMISC_1:25;
i+1 in dom F by A8,NAT_1:12,FINSEQ_3:25; then
F.(i+1) in rng F by FUNCT_1:3; then
F.(i+1) in S;
hence P[i+1] by A1,A5,A11,FINSUB_1:def 1;
end;
end;
for i be Nat holds P[i] from NAT_1:sch 2(A3,A4);
hence thesis;
end;
theorem
for X be set, S be with_empty_element semi-diff-closed
cap-closed Subset-Family of X,
P be pre-Measure of S,
F1,F2 be disjoint_valued FinSequence of S
st Union F1 in S & Union F1 = Union F2 holds P.(Union F1) = P.(Union F2);
theorem FStoMAT1:
for S be non empty cap-closed set, F1,F2 be FinSequence of S holds
ex Mx be Matrix of len F1,len F2,S st
for i,j be Nat st [i,j] in Indices Mx holds Mx*(i,j) = F1.i /\ F2.j
proof
let S be non empty cap-closed set;
let F1,F2 be FinSequence of S;
defpred P[Nat,Nat,set] means $3 = F1.$1 /\ F2.$2;
A2:for i,j be Nat st [i,j] in [:Seg len F1, Seg len F2:]
ex K be Element of S st P[i,j,K]
proof
let i,j be Nat;
assume [i,j] in [:Seg len F1,Seg len F2:]; then
i in Seg len F1 & j in Seg len F2 by ZFMISC_1:87; then
i in dom F1 & j in dom F2 by FINSEQ_1:def 3; then
F1.i in rng F1 & F2.j in rng F2 by FUNCT_1:3; then
F1.i /\ F2.j in S by FINSUB_1:def 2;
hence thesis;
end;
consider Mx be Matrix of len F1,len F2,S such that
A3: for i,j be Nat st
[i,j] in Indices Mx holds P[i,j,Mx*(i,j)] from MATRIX_0:sch 2(A2);
take Mx;
thus thesis by A3;
end;
theorem Th40:
for X be set, S be with_empty_element cap-closed Subset-Family of X,
F1,F2 be non empty disjoint_valued FinSequence of S,
P be nonnegative zeroed Function of S,ExtREAL,
Mx be Matrix of len F1,len F2,ExtREAL
st
Union F1 = Union F2 &
( for i,j be Nat st [i,j] in Indices Mx holds Mx*(i,j) = P.(F1.i /\ F2.j) ) &
( for F be disjoint_valued FinSequence of S st Union F in S
holds P.(Union F) = Sum(P*F) )
holds
( for i be Nat st i <= len(P*F1) holds (P*F1).i = (Sum Mx).i )
& Sum(P*F1) = SumAll(Mx)
proof
let X be set, S be with_empty_element cap-closed Subset-Family of X,
F1,F2 be non empty disjoint_valued FinSequence of S,
P be nonnegative zeroed Function of S,ExtREAL,
Mx be Matrix of len F1,len F2,ExtREAL;
assume that
A1: Union F1 = Union F2 and
A2: for i,j be Nat st [i,j] in Indices Mx holds Mx*(i,j) = P.(F1.i /\ F2.j) and
A3: for F be disjoint_valued FinSequence of S st Union F in S
holds P.(Union F) = Sum(P*F);
consider Kx be Matrix of len F1,len F2,S such that
KX1:for i,j be Nat st [i,j] in Indices Kx holds Kx*(i,j) = F1.i /\ F2.j
by FStoMAT1;
C0:len Kx = len F1 & len Mx = len F1 by MATRIX_0:def 2; then
C1:len (P*F1) = len Mx & len (P*F1) = len Kx by FINSEQ_2:33;
C4:width Kx = len F2 & width Mx = len F2 by C0,MATRIX_0:20;
C2:len (P*F1) = len (Sum Mx) by C1,Def5;
thus
C6:for i be Nat st i <= len(P*F1) holds (P*F1).i = (Sum Mx).i
proof
let i be Nat;
assume E0: i <= len (P*F1);
per cases;
suppose i = 0; then
not i in dom(P*F1) & not i in dom(Sum Mx) by FINSEQ_3:24; then
(P*F1).i = 0 & (Sum Mx).i = 0 by FUNCT_1:def 2;
hence (P*F1).i = (Sum Mx).i;
end;
suppose i <> 0; then
E1: 1 <= i by NAT_1:14; then
i in dom (P*F1) by E0,FINSEQ_3:25; then
E2: i in dom F1 by FUNCT_1:11; then
F1.i c= union rng F1 by FUNCT_1:3,ZFMISC_1:74; then
F1.i c= Union F2 by A1,CARD_3:def 4; then
E3: F1.i /\ Union F2 = F1.i by XBOOLE_1:28;
E4: F1.i in rng F1 by E2,FUNCT_1:3;
E5: i in dom Kx & i in dom Mx by C1,E0,E1,FINSEQ_3:25;
for p,q be object st p <> q holds (Kx.i).p misses (Kx.i).q
proof
let p,q be object;
assume SA0: p <> q;
per cases;
suppose SA1: p in dom (Kx.i) & q in dom (Kx.i); then
reconsider p1 = p, q1 = q as Nat;
E6: [i,p1] in Indices Kx & [i,q1] in Indices Kx by SA1,E5,MATRIX_0:37;
Kx*(i,p1) = (Kx.i).p & Kx*(i,q1) = (Kx.i).q by E6,MATRPROB:14; then
(Kx.i).p = F1.i /\ F2.p1 & (Kx.i).q = F1.i /\ F2.q1 by E6,KX1;
hence (Kx.i).p misses (Kx.i).q by SA0,PROB_2:def 2,XBOOLE_1:76;
end;
suppose not p in dom(Kx.i); then
(Kx.i).p = {} by FUNCT_1:def 2;
hence (Kx.i).p misses (Kx.i).q by XBOOLE_1:65;
end;
suppose not q in dom(Kx.i); then
(Kx.i).q = {} by FUNCT_1:def 2;
hence (Kx.i).p misses (Kx.i).q by XBOOLE_1:65;
end;
end; then
E8: Kx.i is disjoint_valued FinSequence of S by PROB_2:def 2;
now let x be object;
assume x in Union(Kx.i); then
x in union rng (Kx.i) by CARD_3:def 4; then
consider A be set such that
E9: x in A & A in rng(Kx.i) by TARSKI:def 4;
consider m be object such that
E10: m in dom(Kx.i) & A = (Kx.i).m by E9,FUNCT_1:def 3;
reconsider m as Nat by E10;
E11: [i,m] in Indices Kx by E10,E5,MATRIX_0:37; then
(Kx.i).m = Kx*(i,m) by MATRPROB:14; then
(Kx.i).m = F1.i /\ F2.m by E11,KX1; then
E12: x in F1.i & x in F2.m by E9,E10,XBOOLE_0:def 4;
1 <= m & m <= len F2 by E11,MATRIX_0:33; then
m in dom F2 by FINSEQ_3:25; then
F2.m in rng F2 by FUNCT_1:3; then
x in union rng F2 by E12,TARSKI:def 4; then
x in Union F2 by CARD_3:def 4;
hence x in (F1.i /\ Union F2) by E12,XBOOLE_0:def 4;
end; then
E13: Union(Kx.i) c= (F1.i /\ Union F2) by TARSKI:def 3;
now let x be object;
assume x in F1.i /\ Union F2; then
E14: x in F1.i & x in Union F2 by XBOOLE_0:def 4; then
x in union rng F2 by CARD_3:def 4; then
consider A be set such that
E15: x in A & A in rng F2 by TARSKI:def 4;
consider m be object such that
E16: m in dom F2 & A = F2.m by E15,FUNCT_1:def 3;
reconsider m as Nat by E16;
1 <= i & i <= len F1 & 1 <= m & m <= len F2
by E2,E16,FINSEQ_3:25; then
E17: [i,m] in Indices Kx by MATRIX_0:31; then
(Kx.i).m = Kx*(i,m) by MATRPROB:14; then
(Kx.i).m = F1.i /\ F2.m by E17,KX1; then
E18: x in (Kx.i).m by E14,E15,E16,XBOOLE_0:def 4;
m in dom(Kx.i) by E17,MATRIX_0:38; then
(Kx.i).m in rng(Kx.i) by FUNCT_1:3; then
x in union rng(Kx.i) by E18,TARSKI:def 4;
hence x in Union(Kx.i) by CARD_3:def 4;
end; then
F1.i /\ Union F2 c= Union(Kx.i) by TARSKI:def 3; then
F1.i /\ Union F2 = Union(Kx.i) by E13,XBOOLE_0:def 10; then
E19: P.(F1.i /\ Union F2) = Sum(P*(Kx.i)) by E3,E4,E8,A3;
E20: i in Seg len Mx by C1,E0,E1;
E21: Mx.i = Line(Mx,i) & Kx.i = Line(Kx,i) by E5,MATRIX_0:60;
rng(Kx.i) c= S; then
rng(Kx.i) c= dom P by FUNCT_2:def 1; then
E22: dom(P*(Kx.i)) = dom (Kx.i) by RELAT_1:27; then
len(P*(Kx.i)) = len (Kx.i) by FINSEQ_3:29; then
E23a:len(P*(Kx.i)) = width Kx by E21,MATRIX_0:def 7; then
E23: len(P*(Kx.i)) = len (Mx.i) by C4,E21,MATRIX_0:def 7;
for k be Nat st 1 <= k & k <= len (P*(Kx.i)) holds
(P*(Kx.i)).k = (Mx.i).k
proof
let k be Nat;
assume E24: 1 <= k & k <= len (P*(Kx.i)); then
k in dom (Kx.i) & k in dom(Mx.i) by E23,E22,FINSEQ_3:25; then
E25: [i,k] in Indices Kx & [i,k] in Indices Mx by E5,MATRPROB:13;
k in dom(P*(Kx.i)) by E24,FINSEQ_3:25; then
(P*(Kx.i)).k = P.((Kx.i).k) by FUNCT_1:12; then
(P*(Kx.i)).k = P.(Kx*(i,k)) by E25,MATRPROB:14; then
(P*(Kx.i)).k = P.(F1.i /\ F2.k) by E25,KX1; then
(P*(Kx.i)).k = Mx*(i,k) by E25,A2;
hence (P*(Kx.i)).k = (Mx.i).k by E25,MATRPROB:14;
end; then
E27: P*(Kx.i) = Mx.i by E23a,C4,E21,MATRIX_0:def 7;
F1.i c= union rng F1 by E2,FUNCT_1:3,ZFMISC_1:74; then
F1.i c= Union F1 by CARD_3:def 4; then
F1.i /\ Union F2 = F1.i by A1,XBOOLE_1:28; then
(P*F1).i = Sum(P*(Kx.i)) by E2,E19,FUNCT_1:13;
hence (P*F1).i = (Sum Mx).i by E20,E27,E21,Th16;
end;
end;
consider SMF1 be Function of NAT,ExtREAL such that
A2: Sum(P*F1) = SMF1.(len(P*F1)) &
SMF1.0 = 0 &
for i be Nat st i < len (P*F1) holds
SMF1.(i+1) = SMF1.i + (P*F1).(i+1) by EXTREAL1:def 2;
consider LL be Function of NAT,ExtREAL such that
C7: SumAll(Mx) = LL.(len (Sum Mx)) &
LL.0 = 0. &
for i be Nat st i < len (Sum Mx) holds
LL.(i+1) = LL.i + (Sum Mx).(i+1) by EXTREAL1:def 2;
defpred PK1[Nat] means $1 <= len(P*F1) implies SMF1.$1 = LL.$1;
C8: PK1[0] by A2,C7;
C9: for i be Nat st PK1[i] holds PK1[i+1]
proof
let i be Nat;
assume V1: PK1[i];
assume V3: i+1 <= len (P*F1); then
SMF1.(i+1) = SMF1.i + (P*F1).(i+1) by A2,NAT_1:13; then
SMF1.(i+1) = LL.i + (Sum Mx).(i+1) by C6,V1,V3,NAT_1:13;
hence SMF1.(i+1) = LL.(i+1) by C7,V3,C2,NAT_1:13;
end;
for i be Nat holds PK1[i] from NAT_1:sch 2(C8,C9);
hence Sum(P*F1) = SumAll(Mx) by A2,C2,C7;
end;
theorem Th41:
for X be set, S be with_empty_element cap-closed Subset-Family of X,
F1,F2 be non empty disjoint_valued FinSequence of S,
P be nonnegative zeroed Function of S,ExtREAL,
Mx be Matrix of len F1,len F2,ExtREAL
st
Union F1 = Union F2 &
( for i,j be Nat st [i,j] in Indices Mx holds Mx*(i,j) = P.(F1.i /\ F2.j) ) &
( for F be disjoint_valued FinSequence of S st Union F in S
holds P.(Union F) = Sum(P*F) )
holds
( for i be Nat st i <= len (P*F2) holds (P*F2).i = (Sum(Mx@)).i )
& Sum(P*F2) = SumAll(Mx@)
proof
let X be set, S be with_empty_element cap-closed Subset-Family of X,
F1,F2 be non empty disjoint_valued FinSequence of S,
P be nonnegative zeroed Function of S,ExtREAL,
Mx be Matrix of len F1,len F2,ExtREAL;
assume that
A1: Union F1 = Union F2 and
A2: for i,j be Nat st [i,j] in Indices Mx holds Mx*(i,j) = P.(F1.i /\ F2.j) and
A3: for F be disjoint_valued FinSequence of S st Union F in S
holds P.(Union F) = Sum(P*F);
consider Kx be Matrix of len F1,len F2,S such that
KX1:for i,j be Nat st [i,j] in Indices Kx holds Kx*(i,j) = F1.i /\ F2.j
by FStoMAT1;
A5:len (P*F2) = len F2 by FINSEQ_2:33;
C3:len Kx = len F1 & len Mx = len F1 by MATRIX_0:def 2; then
width Kx = len F2 & width Mx = len F2 by MATRIX_0:20; then
C5:len (Kx@) = len F2 & len (Mx@) = len F2 &
width (Kx@) = len F1 & width(Mx@) = len F1 by C3,MATRIX_0:29; then
D2: len (P*F2) = len (Sum(Mx@)) by A5,Def5;
thus
D6:for i be Nat st i <= len (P*F2) holds (P*F2).i = (Sum(Mx@)).i
proof
let i be Nat;
assume E0: i <= len (P*F2);
per cases;
suppose i = 0; then
not i in dom(P*F2) & not i in dom(Sum(Mx@)) by FINSEQ_3:24; then
(P*F2).i = 0 & (Sum(Mx@)).i = 0 by FUNCT_1:def 2;
hence (P*F2).i = (Sum(Mx@)).i;
end;
suppose i <> 0; then
E1: 1 <= i by NAT_1:14; then
i in dom (P*F2) by E0,FINSEQ_3:25; then
E2: i in dom F2 by FUNCT_1:11; then
F2.i c= union rng F2 by FUNCT_1:3,ZFMISC_1:74; then
F2.i c= Union F1 by A1,CARD_3:def 4; then
E3: F2.i /\ Union F1 = F2.i by XBOOLE_1:28;
E4: F2.i in rng F2 by E2,FUNCT_1:3;
E5: i in dom(Kx@) & i in dom(Mx@) by C5,A5,E0,E1,FINSEQ_3:25;
for p,q be object st p <> q holds ((Kx@).i).p misses ((Kx@).i).q
proof
let p,q be object;
assume SA0: p <> q;
per cases;
suppose SA1: p in dom((Kx@).i) & q in dom((Kx@).i); then
reconsider p1 = p, q1 = q as Nat;
E6: [i,p1] in Indices(Kx@) & [i,q1] in Indices(Kx@)
by SA1,E5,MATRIX_0:37; then
EE6: [p1,i] in Indices(Kx) & [q1,i] in Indices(Kx) by MATRIX_0:def 6;
(Kx@)*(i,p1) = ((Kx@).i).p & (Kx@)*(i,q1) = ((Kx@).i).q
by E6,MATRPROB:14; then
((Kx@).i).p = Kx*(p1,i) & ((Kx@).i).q = Kx*(q1,i)
by EE6,MATRIX_0:def 6; then
((Kx@).i).p = F2.i /\ F1.p1 & ((Kx@).i).q = F2.i /\ F1.q1 by EE6,KX1;
hence ((Kx@).i).p misses ((Kx@).i).q by SA0,PROB_2:def 2,XBOOLE_1:76;
end;
suppose not p in dom((Kx@).i); then
((Kx@).i).p = {} by FUNCT_1:def 2;
hence ((Kx@).i).p misses ((Kx@).i).q by XBOOLE_1:65;
end;
suppose not q in dom((Kx@).i); then
((Kx@).i).q = {} by FUNCT_1:def 2;
hence ((Kx@).i).p misses ((Kx@).i).q by XBOOLE_1:65;
end;
end; then
E8: (Kx@).i is disjoint_valued FinSequence of S by PROB_2:def 2;
now let x be object;
assume x in Union((Kx@).i); then
x in union rng ((Kx@).i) by CARD_3:def 4; then
consider A be set such that
E9: x in A & A in rng((Kx@).i) by TARSKI:def 4;
consider m be object such that
E10: m in dom((Kx@).i) & A = ((Kx@).i).m by E9,FUNCT_1:def 3;
reconsider m as Nat by E10;
E11: [i,m] in Indices (Kx@) by E10,E5,MATRIX_0:37; then
EE11: [m,i] in Indices(Kx) by MATRIX_0:def 6;
((Kx@).i).m = (Kx@)*(i,m) by E11,MATRPROB:14; then
((Kx@).i).m = (Kx)*(m,i) by EE11,MATRIX_0:def 6; then
((Kx@).i).m = F2.i /\ F1.m by EE11,KX1; then
E12: x in F2.i & x in F1.m by E9,E10,XBOOLE_0:def 4;
1 <= m & m <= len F1 by EE11,MATRIX_0:33; then
m in dom F1 by FINSEQ_3:25; then
F1.m in rng F1 by FUNCT_1:3; then
x in union rng F1 by E12,TARSKI:def 4; then
x in Union F1 by CARD_3:def 4;
hence x in (F2.i /\ Union F1) by E12,XBOOLE_0:def 4;
end; then
E13: Union((Kx@).i) c= (F2.i /\ Union F1) by TARSKI:def 3;
now let x be object;
assume x in F2.i /\ Union F1; then
E14: x in F2.i & x in Union F1 by XBOOLE_0:def 4; then
x in union rng F1 by CARD_3:def 4; then
consider A be set such that
E15: x in A & A in rng F1 by TARSKI:def 4;
consider m be object such that
E16: m in dom F1 & A = F1.m by E15,FUNCT_1:def 3;
reconsider m as Nat by E16;
1 <= i & i <= len F2 & 1 <= m & m <= len F1
by E2,E16,FINSEQ_3:25; then
EE17: [m,i] in Indices Kx by MATRIX_0:31; then
E17: [i,m] in Indices (Kx@) by MATRIX_0:def 6;
((Kx@).i).m = (Kx@)*(i,m) by E17,MATRPROB:14; then
((Kx@).i).m = Kx*(m,i) by EE17,MATRIX_0:def 6; then
((Kx@).i).m = F2.i /\ F1.m by EE17,KX1; then
E18: x in ((Kx@).i).m by E14,E15,E16,XBOOLE_0:def 4;
m in dom((Kx@).i) by E17,MATRIX_0:38; then
((Kx@).i).m in rng((Kx@).i) by FUNCT_1:3; then
x in union rng((Kx@).i) by E18,TARSKI:def 4;
hence x in Union((Kx@).i) by CARD_3:def 4;
end; then
F2.i /\ Union F1 c= Union((Kx@).i) by TARSKI:def 3; then
F2.i /\ Union F1 = Union((Kx@).i) by E13,XBOOLE_0:def 10; then
E19: P.(F2.i /\ Union F1) = Sum(P*((Kx@).i)) by E3,E4,E8,A3;
E20: i in Seg len (Mx@) by C5,A5,E0,E1;
E21: (Mx@).i = Line((Mx@),i) & (Kx@).i = Line((Kx@),i) by E5,MATRIX_0:60;
rng((Kx@).i) c= S; then
rng((Kx@).i) c= dom P by FUNCT_2:def 1; then
E22: dom(P*((Kx@).i)) = dom ((Kx@).i) by RELAT_1:27; then
len(P*((Kx@).i)) = len ((Kx@).i) by FINSEQ_3:29; then
F23: len(P*((Kx@).i)) = width (Kx@) by E21,MATRIX_0:def 7; then
E23: len(P*((Kx@).i)) = len ((Mx@).i) by C5,E21,MATRIX_0:def 7;
for k be Nat st 1 <= k & k <= len (P*((Kx@).i)) holds
(P*((Kx@).i)).k = ((Mx@).i).k
proof
let k be Nat;
assume E24: 1 <= k & k <= len (P*((Kx@).i)); then
k in dom((Kx@).i) & k in dom((Mx@).i) by E23,E22,FINSEQ_3:25; then
E25: [i,k] in Indices(Kx@) & [i,k] in Indices(Mx@) by E5,MATRPROB:13; then
EE25: [k,i] in Indices Kx & [k,i] in Indices Mx by MATRIX_0:def 6;
k in dom(P*((Kx@).i)) by E24,FINSEQ_3:25; then
(P*((Kx@).i)).k = P.(((Kx@).i).k) by FUNCT_1:12; then
(P*((Kx@).i)).k = P.((Kx@)*(i,k)) by E25,MATRPROB:14; then
(P*((Kx@).i)).k = P.(Kx*(k,i)) by EE25,MATRIX_0:def 6; then
(P*((Kx@).i)).k = P.(F2.i /\ F1.k) by EE25,KX1; then
(P*((Kx@).i)).k = Mx*(k,i) by EE25,A2; then
(P*((Kx@).i)).k = (Mx@)*(i,k) by EE25,MATRIX_0:def 6;
hence (P*((Kx@).i)).k = ((Mx@).i).k by E25,MATRPROB:14;
end; then
E27: P*((Kx@).i) = (Mx@).i by F23,C5,E21,MATRIX_0:def 7;
F2.i c= union rng F2 by E2,FUNCT_1:3,ZFMISC_1:74; then
F2.i c= Union F2 by CARD_3:def 4; then
F2.i /\ Union F1 = F2.i by A1,XBOOLE_1:28; then
(P*F2).i = Sum(P*((Kx@).i)) by E2,E19,FUNCT_1:13;
hence (P*F2).i = (Sum(Mx@)).i by E20,E27,E21,Th16;
end;
end;
consider SMF2 be Function of NAT,ExtREAL such that
A3: Sum(P*F2) = SMF2.(len(P*F2)) &
SMF2.0 = 0 &
for i be Nat st i < len (P*F2) holds
SMF2.(i+1) = SMF2.i + (P*F2).(i+1) by EXTREAL1:def 2;
consider LL be Function of NAT,ExtREAL such that
D7: SumAll(Mx@) = LL.(len (Sum(Mx@))) &
LL.0 = 0. &
for i be Nat st i < len (Sum(Mx@)) holds
LL.(i+1) = LL.i + (Sum(Mx@)).(i+1) by EXTREAL1:def 2;
defpred PK2[Nat] means $1 <= len(P*F2) implies SMF2.$1 = LL.$1;
D8: PK2[0] by A3,D7;
D9: for i be Nat st PK2[i] holds PK2[i+1]
proof
let i be Nat;
assume V1: PK2[i];
assume V3: i+1 <= len (P*F2); then
SMF2.(i+1) = SMF2.i + (P*F2).(i+1) by A3,NAT_1:13; then
SMF2.(i+1) = LL.i + (Sum(Mx@)).(i+1) by D6,V1,V3,NAT_1:13;
hence SMF2.(i+1) = LL.(i+1) by D7,V3,D2,NAT_1:13;
end;
for i be Nat holds PK2[i] from NAT_1:sch 2(D8,D9);
hence Sum(P*F2) = SumAll(Mx@) by A3,D2,D7;
end;
theorem Th42:
for X be set, S be with_empty_element semi-diff-closed
cap-closed Subset-Family of X, P be pre-Measure of S,
A be set st A in Ring_generated_by S
holds
for F1,F2 be disjoint_valued FinSequence of S st
A = Union F1 & A = Union F2 holds Sum(P*F1) = Sum(P*F2)
proof
let X be set,
S be with_empty_element semi-diff-closed cap-closed Subset-Family of X,
P be pre-Measure of S,
A be set;
assume A in Ring_generated_by S;
hereby let F1,F2 be disjoint_valued FinSequence of S;
assume A1: A = Union F1 & A = Union F2;
consider SMF1 be Function of NAT,ExtREAL such that
A2: Sum(P*F1) = SMF1.(len(P*F1)) &
SMF1.0 = 0 &
for i be Nat st i < len (P*F1) holds
SMF1.(i+1) = SMF1.i + (P*F1).(i+1) by EXTREAL1:def 2;
consider SMF2 be Function of NAT,ExtREAL such that
A3: Sum(P*F2) = SMF2.(len(P*F2)) &
SMF2.0 = 0 &
for i be Nat st i < len (P*F2) holds
SMF2.(i+1) = SMF2.i + (P*F2).(i+1) by EXTREAL1:def 2;
dom P = S by FUNCT_2:def 1; then
rng F1 c= dom P & rng F2 c= dom P; then
A4: dom (P*F1) = dom F1 & dom (P*F2) = dom F2 by RELAT_1:27; then
A5: dom (P*F1) = Seg len F1 & dom(P*F2) = Seg len F2 &
len (P*F1) = len F1 & len (P*F2) = len F2 by FINSEQ_1:def 3,FINSEQ_3:29;
per cases;
suppose A6: len (P*F1) = 0; then
P*F1 = {}; then
F1 = {} by A4; then
rng F1 = {}; then
Union F2 = {} by A1,CARD_3:def 4,ZFMISC_1:2; then
G7: union rng F2 = {} by CARD_3:def 4;
defpred S[Nat] means $1 <= len(P*F2) implies SMF2.$1 = 0;
A8: S[0] by A3;
A9: for i be Nat st S[i] holds S[i+1]
proof
let i be Nat;
assume A10: S[i];
assume A11: i+1 <= len (P*F2); then
A13: SMF2.(i+1) = SMF2.i + (P*F2).(i+1) & SMF2.i = 0 by A3,A10,NAT_1:13;
A14: i+1 in dom(P*F2) by A11,NAT_1:11,FINSEQ_3:25; then
F2.(i+1) = {} by A4,G7,ORDERS_1:6,FUNCT_1:3; then
P.(F2.(i+1)) = 0 by VALUED_0:def 19; then
(P*F2).(i+1) = 0 by A14,FUNCT_1:12;
hence SMF2.(i+1) = 0 by A13;
end;
for i be Nat holds S[i] from NAT_1:sch 2(A8,A9);
hence Sum(P*F1) = Sum(P*F2) by A2,A3,A6;
end;
suppose B6: len (P*F2) = 0; then
P*F2 = {}; then
F2 = {} by A4; then
rng F2 = {}; then
Union F1 = {} by A1,CARD_3:def 4,ZFMISC_1:2; then
E7: union rng F1 = {} by CARD_3:def 4;
defpred S[Nat] means $1 <= len(P*F1) implies SMF1.$1 = 0;
B8: S[0] by A2;
B9: for i be Nat st S[i] holds S[i+1]
proof
let i be Nat;
assume B10: S[i];
assume B11: i+1 <= len (P*F1); then
B13: SMF1.(i+1) = SMF1.i + (P*F1).(i+1) & SMF1.i = 0 by A2,B10,NAT_1:13;
B14: i+1 in dom(P*F1) by B11,NAT_1:11,FINSEQ_3:25; then
F1.(i+1) = {} by A4,E7,ORDERS_1:6,FUNCT_1:3; then
P.(F1.(i+1)) = 0 by VALUED_0:def 19; then
(P*F1).(i+1) = 0 by B14,FUNCT_1:12;
hence SMF1.(i+1) = 0 by B13;
end;
for i be Nat holds S[i] from NAT_1:sch 2(B8,B9);
hence Sum(P*F1) = Sum(P*F2) by A2,A3,B6;
end;
suppose
A15: len (P*F1) <> 0 & len (P*F2) <> 0;
defpred Mx[Nat,Nat,set] means $3 = P.(F1.$1 /\ F2.$2);
MX0: for i,j be Nat st [i,j] in [:Seg len F1, Seg len F2:]
ex A be Element of ExtREAL st Mx[i,j,A];
consider Mx be Matrix of len F1,len F2,ExtREAL such that
MX1: for i,j be Nat st
[i,j] in Indices Mx holds Mx[i,j,Mx*(i,j)] from MATRIX_0:sch 2(MX0);
C3: len Mx = len F1 by MATRIX_0:def 2; then
C4: width Mx = len F2 by A15,A5,MATRIX_0:20;
CC0: for F be disjoint_valued FinSequence of S st Union F in S
holds P.(Union F) = Sum(P*F) by Def8;
C0: F1 is non empty & F2 is non empty by A15; then
C10: Sum(P*F1) = SumAll(Mx) by A1,MX1,CC0,Th40;
D10:Sum(P*F2) = SumAll(Mx@) by C0,A1,MX1,CC0,Th41;
for i be Nat st i in dom Mx holds not -infty in rng(Mx.i)
proof
let i be Nat;
assume F1: i in dom Mx;
assume -infty in rng(Mx.i); then
consider j be object such that
F2: j in dom(Mx.i) & (Mx.i).j = -infty by FUNCT_1:def 3;
reconsider j as Nat by F2;
F3: [i,j] in Indices Mx by F1,F2,MATRPROB:13; then
(Mx.i).j = Mx*(i,j) by MATRPROB:14; then
F5: (Mx.i).j = P.(F1.i /\ F2.j) by F3,MX1;
i in Seg len Mx & j in Seg width Mx by F3,MATRPROB:12; then
i in dom F1 & j in dom F2 by C3,C4,FINSEQ_1:def 3; then
F1.i in rng F1 & F2.j in rng F2 by FUNCT_1:3; then
F1.i /\ F2.j in S by FINSUB_1:def 2;
hence contradiction by F2,F5,MEASURE1:def 2;
end;
hence Sum(P*F1) = Sum(P*F2) by C10,D10,Th28;
end;
end;
end;
theorem Th43:
for f1,f2 be FinSequence
st f1 is disjoint_valued & f2 is disjoint_valued
& union rng f1 misses union rng f2
holds f1^f2 is disjoint_valued
proof
let f1,f2 be FinSequence;
assume that
A1: f1 is disjoint_valued & f2 is disjoint_valued and
A2: union rng f1 misses union rng f2;
now let x,y be object;
assume A3: x <> y;
per cases;
suppose A4: x in dom (f1^f2) & y in dom (f1^f2); then
reconsider x1=x, y1=y as Nat;
per cases by A4,FINSEQ_1:25;
suppose x1 in dom f1 & y1 in dom f1; then
(f1^f2).x = f1.x & (f1^f2).y = f1.y by FINSEQ_1:def 7;
hence (f1^f2).x misses (f1^f2).y by A1,A3,PROB_2:def 2;
end;
suppose A6: x1 in dom f1
& ex n be Nat st n in dom f2 & y1=len f1 + n; then
consider n be Nat such that
A7: n in dom f2 & y1 = len f1 + n;
(f1^f2).x = f1.x by A6,FINSEQ_1:def 7; then
A8: (f1^f2).x in rng f1 by A6,FUNCT_1:3;
(f1^f2).y = f2.n by A7,FINSEQ_1:def 7; then
A9: (f1^f2).y in rng f2 by A7,FUNCT_1:3;
now assume (f1^f2).x meets (f1^f2).y; then
consider z be object such that
A10: z in (f1^f2).x & z in (f1^f2).y by XBOOLE_0:3;
z in union rng f1 & z in union rng f2 by A8,A9,A10,TARSKI:def 4;
hence contradiction by A2,XBOOLE_0:3;
end;
hence (f1^f2).x misses (f1^f2).y;
end;
suppose A11: y1 in dom f1
& ex n be Nat st n in dom f2 & x1=len f1 + n; then
consider n be Nat such that
A12: n in dom f2 & x1 = len f1 + n;
(f1^f2).x = f2.n by A12,FINSEQ_1:def 7; then
A13: (f1^f2).x in rng f2 by A12,FUNCT_1:3;
(f1^f2).y = f1.y by A11,FINSEQ_1:def 7; then
A14: (f1^f2).y in rng f1 by A11,FUNCT_1:3;
now assume (f1^f2).x meets (f1^f2).y; then
consider z be object such that
A15: z in (f1^f2).x & z in (f1^f2).y by XBOOLE_0:3;
z in union rng f1 & z in union rng f2 by A13,A14,A15,TARSKI:def 4;
hence contradiction by A2,XBOOLE_0:3;
end;
hence (f1^f2).x misses (f1^f2).y;
end;
suppose A16: (ex n be Nat st n in dom f2 & x1 = len f1 + n)
& (ex m be Nat st m in dom f2 & y1 = len f1 + m); then
consider n be Nat such that
A17: n in dom f2 & x1 = len f1 + n;
A18: (f1^f2).x = f2.n by A17,FINSEQ_1:def 7;
consider m be Nat such that
A19: m in dom f2 & y1 = len f1 + m by A16;
(f1^f2).y = f2.m by A19,FINSEQ_1:def 7;
hence (f1^f2).x misses (f1^f2).y by A1,A18,A17,A19,A3,PROB_2:def 2;
end;
end;
suppose not x in dom (f1^f2) or not y in dom(f1^f2); then
(f1^f2).x = {} or (f1^f2).y = {} by FUNCT_1:def 2;
hence (f1^f2).x misses (f1^f2).y by XBOOLE_1:65;
end;
end;
hence f1^f2 is disjoint_valued by PROB_2:def 2;
end;
theorem
for X be set, P be with_empty_element semi-diff-closed
Subset-Family of X,
M be pre-Measure of P,
A,B be set st A in P & B in P & A \ B in P & B c= A holds
M.A >= M.B
proof
let X be set, P be with_empty_element semi-diff-closed
Subset-Family of X,
M be pre-Measure of P,
A,B be set;
assume that
A1: A in P & B in P & A \ B in P and
A2: B c= A;
consider F be disjoint_valued FinSequence of P such that
A3: A \ B = Union F by A1,SRINGS_3:def 1;
A7:rng <*B*> = {B} by FINSEQ_1:38; then
reconsider G = <*B*> as disjoint_valued FinSequence of P
by FINSEQ_1:def 4,A1,ZFMISC_1:31;
now assume union rng G meets union rng F; then
consider x be object such that
A4: x in union rng G & x in union rng F by XBOOLE_0:3;
consider P be set such that
A5: x in P & P in rng G by A4,TARSKI:def 4;
P in {B} by A5,FINSEQ_1:38; then
A6: x in B by A5,TARSKI:def 1;
x in A \ B by A3,A4,CARD_3:def 4;
hence contradiction by A6,XBOOLE_0:def 5;
end; then
reconsider H = G^F as disjoint_valued FinSequence of P by Th43;
A8:union rng G = B by A7,ZFMISC_1:25;
rng H = rng G \/ rng F by FINSEQ_1:31; then
union rng H = union rng G \/ union rng F by ZFMISC_1:78; then
Union H = B \/ union rng F by A8,CARD_3:def 4
.= B \/ (A \ B) by A3,CARD_3:def 4; then
Union H = A \/ B by XBOOLE_1:39; then
Union H = A by A2,XBOOLE_1:12; then
A9:M.A = Sum(M*H) by A1,Def8;
Union G = B by A8,CARD_3:def 4; then
A10:M.B = Sum(M*G) by A1,Def8;
B0:now assume -infty in rng(M*G); then
consider n be Element of NAT such that
B1: n in dom(M*G) & -infty = (M*G).n by PARTFUN1:3;
M.(G.n) = -infty by B1,FUNCT_1:12;
hence contradiction by SUPINF_2:51;
end;
A11:now assume -infty in rng(M*F); then
consider n be Element of NAT such that
B2: n in dom(M*F) & -infty = (M*F).n by PARTFUN1:3;
M.(F.n) = -infty by B2,FUNCT_1:12;
hence contradiction by SUPINF_2:51;
end;
A12:now let n be Nat;
assume n in dom(M*F); then
(M*F).n = M.(F.n) & F.n in dom M by FUNCT_1:11,12;
hence (M*F).n >= 0 by SUPINF_2:51;
end;
M*H = (M*G)^(M*F) by FINSEQOP:9; then
Sum(M*H) = Sum(M*G) + Sum(M*F) by A11,B0,EXTREAL1:10;
hence M.B <= M.A by A9,A10,A12,MESFUNC5:53,XXREAL_3:39;
end;
theorem Th45:
for Y,S be non empty set, F be PartFunc of Y,S, M be
Function of S,ExtREAL st M is nonnegative holds M*F is nonnegative
proof
let Y,S be non empty set;
let F be PartFunc of Y,S;
let M be Function of S,ExtREAL;
assume A1: M is nonnegative;
now let n be object;
per cases;
suppose n in dom(M*F); then
(M*F).n = M.(F.n) by FUNCT_1:12;
hence (M*F).n >= 0 by A1,SUPINF_2:51;
end;
suppose not n in dom(M*F);
hence (M*F).n >= 0 by FUNCT_1:def 2;
end;
end;
hence thesis by SUPINF_2:51;
end;
theorem Th46:
for X be set, S be with_empty_element semi-diff-closed
cap-closed Subset-Family of X, P be pre-Measure of S
ex M be nonnegative additive zeroed Function of
(Ring_generated_by S),ExtREAL
st for A be set st A in Ring_generated_by S holds
for F be disjoint_valued FinSequence of S
st A = Union F holds M.A = Sum(P*F)
proof
let X be set,
S be with_empty_element semi-diff-closed cap-closed Subset-Family of X,
P be pre-Measure of S;
defpred P[object,object] means
for F be disjoint_valued FinSequence of S
st $1 = Union F holds $2 = Sum(P*F);
A1:for A be object st A in Ring_generated_by S
ex p be object st p in ExtREAL & P[A,p]
proof
let A be object;
assume
A2: A in Ring_generated_by S; then
A in DisUnion S by SRINGS_3:18; then
consider V be Subset of X such that
A3: A = V & ex F be disjoint_valued FinSequence of S st V = Union F;
consider F be disjoint_valued FinSequence of S such that
A4: V = Union F by A3;
set p = Sum(P*F);
take p;
thus p in ExtREAL & P[A,p] by A2,A3,A4,Th42;
end;
consider M be Function of (Ring_generated_by S),ExtREAL such that
A5: for A be object st A in Ring_generated_by S holds P[A,M.A]
from FUNCT_2:sch 1(A1);
A18:for A be Element of Ring_generated_by S holds 0 <= M.A
proof
let A be Element of Ring_generated_by S;
A in Ring_generated_by S; then
A in DisUnion S by SRINGS_3:18; then
consider V be Subset of X such that
A7: A = V & ex F be disjoint_valued FinSequence of S st V = Union F;
consider F be disjoint_valued FinSequence of S such that
A8: V = Union F by A7;
consider PF be sequence of ExtREAL such that
A10: Sum(P*F) = PF.(len(P*F)) & PF.0 = 0. &
for i be Nat st i < len(P*F) holds PF.(i+1) = PF.i + (P*F).(i+1)
by EXTREAL1:def 2;
defpred P2[Nat] means $1 <= len(P*F) implies PF.$1 >= 0;
A11:P2[0] by A10;
A12:for i be Nat st P2[i] holds P2[i+1]
proof
let i be Nat;
assume A13: P2[i];
assume A14: i+1 <= len(P*F); then
i+1 in dom(P*F) by NAT_1:11,FINSEQ_3:25; then
(P*F).(i+1) = P.(F.(i+1)) by FUNCT_1:12; then
A17: (P*F).(i+1) >= 0 by SUPINF_2:51;
PF.(i+1) = PF.i + (P*F).(i+1) by A14,A10,NAT_1:13;
hence PF.(i+1) >= 0 by A13,A14,A17,NAT_1:13;
end;
for i be Nat holds P2[i] from NAT_1:sch 2(A11,A12); then
Sum(P*F) >= 0 by A10;
hence 0 <= M.A by A7,A8,A5;
end;
for A,B be Element of Ring_generated_by S
st A misses B & A \/ B in Ring_generated_by S
holds M.(A \/ B) = M.A + M.B
proof
let A,B be Element of Ring_generated_by S;
assume A19: A misses B & A \/ B in Ring_generated_by S;
A in Ring_generated_by S; then
A in DisUnion S by SRINGS_3:18; then
consider V be Subset of X such that
A20: A = V & ex F be disjoint_valued FinSequence of S st V = Union F;
consider F be disjoint_valued FinSequence of S such that
A21: V = Union F by A20;
B in Ring_generated_by S; then
B in DisUnion S by SRINGS_3:18; then
consider W be Subset of X such that
A22: B = W & ex G be disjoint_valued FinSequence of S st W = Union G;
consider G be disjoint_valued FinSequence of S such that
A23: W = Union G by A22;
set H = F^G;
A24:A = union rng F & B = union rng G by A20,A21,A22,A23,CARD_3:def 4; then
reconsider H as disjoint_valued FinSequence of S by A19,Th43;
rng H = rng F \/ rng G by FINSEQ_1:31; then
union rng H = union rng F \/ union rng G by ZFMISC_1:78; then
A \/ B = Union H by A24,CARD_3:def 4; then
A25:M.(A \/ B) = Sum(P*H) by A5;
A26:M.A = Sum(P*F) & M.B = Sum(P*G) by A20,A21,A22,A23,A5;
P*F is nonnegative by Th45; then
A27:not -infty in rng(P*F) by SUPINF_2:def 9,def 12;
P*G is nonnegative by Th45; then
A28:not -infty in rng(P*G) by SUPINF_2:def 9,def 12;
P*H = (P*F)^(P*G) by FINSEQOP:9;
hence M.(A \/ B) = M.A + M.B by A25,A26,A27,A28,EXTREAL1:10;
end; then
A29:M is additive by MEASURE1:def 3;
reconsider E = {} as Element of S by SETFAM_1:def 8;
reconsider F = <*E*> as disjoint_valued FinSequence of S;
rng F = {{}} by FINSEQ_1:38; then
union rng F = {} by ZFMISC_1:25; then
Union F = {} by CARD_3:def 4; then
M.{} = Sum(P*F) by A5,FINSUB_1:7; then
M.{} = Sum(<*P.{}*>) by FINSEQ_2:35; then
M.{} = P.{} by EXTREAL1:8; then
M.{} = 0 by VALUED_0:def 19; then
reconsider M as nonnegative additive zeroed Function of
(Ring_generated_by S),ExtREAL by A18,A29,VALUED_0:def 19,MEASURE1:def 2;
take M;
thus thesis by A5;
end;
theorem
for X,Y be set, F,G be Function of NAT,bool X
st (for i be Nat holds G.i = F.i /\ Y) & Union F = Y
holds Union G = Union F
proof
let X,Y be set, F,G be Function of NAT,bool X;
assume that
A1: for i be Nat holds G.i = F.i /\ Y and
A2: Union F = Y;
now let x be object;
assume x in Union G; then
x in union rng G by CARD_3:def 4; then
consider A be set such that
A3: x in A & A in rng G by TARSKI:def 4;
consider i be Element of NAT such that
A4: A = G.i by A3,FUNCT_2:113;
dom F = NAT by FUNCT_2:def 1; then
A = F.i /\ Y & i in dom F by A1,A4; then
x in F.i & F.i in rng F by A3,XBOOLE_0:def 4,FUNCT_1:3; then
x in union rng F by TARSKI:def 4;
hence x in Union F by CARD_3:def 4;
end; then
A5:Union G c= Union F by TARSKI:def 3;
now let x be object;
assume A6: x in Union F; then
x in union rng F by CARD_3:def 4; then
consider A be set such that
A7: x in A & A in rng F by TARSKI:def 4;
consider i be Element of NAT such that
A8: A = F.i by A7,FUNCT_2:113;
dom G = NAT by FUNCT_2:def 1; then
x in F.i /\ Y & i in dom G by A2,A6,A7,A8,XBOOLE_0:def 4; then
x in G.i & G.i in rng G by A1,FUNCT_1:3; then
x in union rng G by TARSKI:def 4;
hence x in Union G by CARD_3:def 4;
end; then
Union F c= Union G by TARSKI:def 3;
hence thesis by A5,XBOOLE_0:def 10;
end;
theorem
for X be set, S be with_empty_element semi-diff-closed cap-closed
Subset-Family of X,
P be pre-Measure of S
ex M be Function of Ring_generated_by S,ExtREAL st
M.{} = 0 &
for K be disjoint_valued FinSequence of S
st Union K in Ring_generated_by S holds M.(Union K) = Sum(P*K)
proof
let X be set, S be with_empty_element semi-diff-closed cap-closed
Subset-Family of X,
P be pre-Measure of S;
consider M be nonnegative additive zeroed Function
of (Ring_generated_by S),ExtREAL such that
A1: for A be set st A in Ring_generated_by S holds
for F be disjoint_valued FinSequence of S st
A = Union F holds M.A = Sum(P*F) by Th46;
take M;
thus M.{} = 0 by VALUED_0:def 19;
thus for K be disjoint_valued FinSequence of S
st Union K in Ring_generated_by S holds M.(Union K) = Sum(P*K) by A1;
end;
theorem
for X,Z be set, P be with_empty_element semi-diff-closed cap-closed
Subset-Family of X,
K be disjoint_valued Function of NAT,Ring_generated_by P
st Z = {[n,F] where n is Nat, F is disjoint_valued FinSequence of P
: Union F = K.n & (K.n = {} implies F = <*{}*>) }
holds proj2 Z is FinSequenceSet of P
& (for x be object holds
x in rng K
iff ex F be FinSequence of P st F in proj2 Z & Union F = x)
& proj2 Z is with_non-empty_elements
proof
let X,Z be set, P be with_empty_element semi-diff-closed cap-closed
Subset-Family of X,
K be disjoint_valued Function of NAT,Ring_generated_by P;
assume A1: Z={[n,F] where n is Nat, F is disjoint_valued FinSequence of P
: Union F = K.n & (K.n = {} implies F = <*{}*>)};
now let a be object;
assume a in proj2 Z; then
consider k be object such that
A2: [k,a] in Z by XTUPLE_0:def 13;
consider n be Nat, F be disjoint_valued FinSequence of P such that
A3: [k,a] = [n,F] & Union F = K.n & (K.n = {} implies F = <*{}*>) by A1,A2;
thus a is FinSequence of P by A3,XTUPLE_0:1;
end;
hence proj2 Z is FinSequenceSet of P by FINSEQ_2:def 3;
hereby let x be object;
hereby assume x in rng K; then
consider n be Element of NAT such that
A6: x = K.n by FUNCT_2:113;
K.n in Ring_generated_by P; then
K.n in DisUnion P by SRINGS_3:18; then
consider A be Subset of X such that
A7: x = A & ex F be disjoint_valued FinSequence of P st A=Union F by A6;
consider F be disjoint_valued FinSequence of P such that
A8: A = Union F by A7;
per cases;
suppose A9: K.n = {};
A10: rng <*{}*> = { {} } by FINSEQ_1:38;
{} in P by SETFAM_1:def 8; then
reconsider F1 = <*{}*> as disjoint_valued FinSequence of P
by A10,ZFMISC_1:31,FINSEQ_1:def 4;
rng F1 = { {} } by FINSEQ_1:38; then
union rng F1 = {} by ZFMISC_1:25; then
B1: Union F1 = {} by CARD_3:def 4; then
[n,F1] in Z by A9,A1;
then F1 in proj2 Z by XTUPLE_0:def 13;
hence ex F be FinSequence of P st F in proj2 Z & Union F = x
by A9,B1,A6;
end;
suppose K.n <> {}; then
[n,F] in Z by A1,A6,A7,A8;
then F in proj2 Z by XTUPLE_0:def 13;
hence ex F be FinSequence of P st F in proj2 Z & Union F = x by A8,A7;
end;
end;
assume ex F be FinSequence of P st F in proj2 Z & Union F = x; then
consider z be FinSequence of P such that
A12: z in proj2 Z & Union z = x;
consider y be object such that
A13: [y,z] in Z by A12,XTUPLE_0:def 13;
consider n be Nat, F be disjoint_valued FinSequence of P such that
A14: [y,z] = [n,F] & Union F = K.n & (K.n = {} implies F = <*{}*>) by A1,A13;
y=n & z=F by A14,XTUPLE_0:1;
hence x in rng K by A12,A14,FUNCT_2:4,ORDINAL1:def 12;
end;
now assume {} in proj2 Z; then
consider y be object such that
A16: [ y,{} ] in Z by XTUPLE_0:def 13;
consider n be Nat, F be disjoint_valued FinSequence of P such that
A17: [ y,{} ] = [n,F] & Union F = K.n & (K.n = {} implies F = <*{}*>)
by A1,A16;
y=n & {}=F by A17,XTUPLE_0:1; then
union rng F = {} by ZFMISC_1:2;
hence contradiction by A17,XTUPLE_0:1,CARD_3:def 4;
end;
hence proj2 Z is with_non-empty_elements;
end;
theorem
for X be set, P be with_empty_element semi-diff-closed cap-closed
Subset-Family of X,
K be disjoint_valued Function of NAT,Ring_generated_by P
st rng K is with_non-empty_element holds
ex Y be non empty FinSequenceSet of P st
Y = {F where F is disjoint_valued FinSequence of P :
Union F in rng K & F <> {} }
& Y is with_non-empty_elements
proof
let X be set, P be with_empty_element semi-diff-closed cap-closed
Subset-Family of X,
K be disjoint_valued Function of NAT,Ring_generated_by P;
assume A0: rng K is with_non-empty_element;
set
Y = {F where F is disjoint_valued FinSequence of P :
Union F in rng K & F <> {} };
now let a be object;
assume a in Y; then
ex A be disjoint_valued FinSequence of P st
a = A & Union A in rng K & A <> {};
hence a is FinSequence of P;
end; then
reconsider Y as FinSequenceSet of P by FINSEQ_2:def 3;
consider k be non empty set such that
A2: k in rng K by A0;
consider i be Element of NAT such that
A3: k = K.i by A2,FUNCT_2:113;
K.i in Ring_generated_by P; then
K.i in DisUnion P by SRINGS_3:18; then
consider A be Subset of X such that
A4: K.i = A
& ex F be disjoint_valued FinSequence of P st A = Union F;
consider F be disjoint_valued FinSequence of P such that
A5: A = Union F by A4;
now assume F = {}; then
union rng F = {} by ZFMISC_1:2;
hence contradiction by A5,A4,A3,CARD_3:def 4;
end; then
F in Y by A2,A3,A4,A5; then
reconsider Y as non empty FinSequenceSet of P;
take Y;
thus Y = {A where A is disjoint_valued FinSequence of P :
Union A in rng K & A <> {} };
now assume {} in Y; then
ex A be disjoint_valued FinSequence of P st
{} = A & Union A in rng K & A <> {};
hence contradiction;
end;
hence Y is with_non-empty_elements;
end;
begin :: Pre-measure on semialgera and construction of measure
theorem Th51:
for X,Z be set, P be semialgebra_of_sets of X,
K be disjoint_valued Function of NAT,Field_generated_by P
st Z = {[n,F] where n is Nat, F is disjoint_valued FinSequence of P
: Union F = K.n & (K.n = {} implies F = <*{}*>) }
holds proj2 Z is FinSequenceSet of P
& (for x be object holds
x in rng K
iff ex F be FinSequence of P st F in proj2 Z & Union F = x)
& proj2 Z is with_non-empty_elements
proof
let X,Z be set, P be semialgebra_of_sets of X,
K be disjoint_valued Function of NAT,Field_generated_by P;
assume A1: Z={[n,F] where n is Nat, F is disjoint_valued FinSequence of P
: Union F = K.n & (K.n = {} implies F = <*{}*>)};
now let a be object;
assume a in proj2 Z; then
consider k be object such that
A2: [k,a] in Z by XTUPLE_0:def 13;
ex n be Nat, F be disjoint_valued FinSequence of P st
[k,a] = [n,F] & Union F = K.n & (K.n = {} implies F = <*{}*>) by A1,A2;
hence a is FinSequence of P by XTUPLE_0:1;
end;
hence proj2 Z is FinSequenceSet of P by FINSEQ_2:def 3;
hereby let x be object;
hereby assume x in rng K; then
consider n be Element of NAT such that
A6: x = K.n by FUNCT_2:113;
K.n in Field_generated_by P; then
K.n in DisUnion P by SRINGS_3:22; then
consider A be Subset of X such that
A7: x = A & ex F be disjoint_valued FinSequence of P st A=Union F by A6;
consider F be disjoint_valued FinSequence of P such that
A8: A = Union F by A7;
per cases;
suppose A9: K.n = {};
A10: rng <*{}*> = { {} } by FINSEQ_1:38;
{} in P by SETFAM_1:def 8; then
reconsider F1 = <*{}*> as disjoint_valued FinSequence of P
by A10,ZFMISC_1:31,FINSEQ_1:def 4;
rng F1 = { {} } by FINSEQ_1:38; then
union rng F1 = {} by ZFMISC_1:25; then
B1: Union F1 = {} by CARD_3:def 4; then
[n,F1] in Z by A9,A1;
then F1 in proj2 Z by XTUPLE_0:def 13;
hence ex F be FinSequence of P st F in proj2 Z & Union F = x
by A9,B1,A6;
end;
suppose K.n <> {}; then
[n,F] in Z by A1,A6,A7,A8;
then F in proj2 Z by XTUPLE_0:def 13;
hence ex F be FinSequence of P st F in proj2 Z & Union F = x by A8,A7;
end;
end;
assume ex F be FinSequence of P st F in proj2 Z & Union F = x; then
consider z be FinSequence of P such that
A12: z in proj2 Z & Union z = x;
consider y be object such that
A13: [y,z] in Z by A12,XTUPLE_0:def 13;
consider n be Nat, F be disjoint_valued FinSequence of P such that
A14: [y,z] = [n,F] & Union F = K.n & (K.n = {} implies F = <*{}*>) by A1,A13;
y=n & z=F by A14,XTUPLE_0:1;
hence x in rng K by A12,A14,ORDINAL1:def 12,FUNCT_2:4;
end;
now assume {} in proj2 Z; then
consider y be object such that
A16: [ y,{} ] in Z by XTUPLE_0:def 13;
consider n be Nat, F be disjoint_valued FinSequence of P such that
A17: [ y,{} ] = [n,F] & Union F = K.n & (K.n = {} implies F = <*{}*>)
by A1,A16;
y=n & {}=F by A17,XTUPLE_0:1; then
union rng F = {} by ZFMISC_1:2;
hence contradiction by A17,XTUPLE_0:1,CARD_3:def 4;
end;
hence proj2 Z is with_non-empty_elements;
end;
theorem Th54:
for X be set, S be semialgebra_of_sets of X, P be pre-Measure of S,
A be set holds
for F1,F2 be disjoint_valued FinSequence of S st
A = Union F1 & A = Union F2 holds Sum(P*F1) = Sum(P*F2)
proof
let X be set, S be semialgebra_of_sets of X, P be pre-Measure of S,
A be set;
hereby let F1,F2 be disjoint_valued FinSequence of S;
assume A1: A = Union F1 & A = Union F2;
consider SMF1 be Function of NAT,ExtREAL such that
A2: Sum(P*F1) = SMF1.(len(P*F1)) &
SMF1.0 = 0 &
for i be Nat st i < len (P*F1) holds
SMF1.(i+1) = SMF1.i + (P*F1).(i+1) by EXTREAL1:def 2;
consider SMF2 be Function of NAT,ExtREAL such that
A3: Sum(P*F2) = SMF2.(len(P*F2)) &
SMF2.0 = 0 &
for i be Nat st i < len (P*F2) holds
SMF2.(i+1) = SMF2.i + (P*F2).(i+1) by EXTREAL1:def 2;
dom P = S by FUNCT_2:def 1; then
rng F1 c= dom P & rng F2 c= dom P; then
A4: dom (P*F1) = dom F1 & dom (P*F2) = dom F2 by RELAT_1:27; then
A5: dom (P*F1) = Seg len F1 & dom(P*F2) = Seg len F2 &
len (P*F1) = len F1 & len (P*F2) = len F2 by FINSEQ_1:def 3,FINSEQ_3:29;
per cases;
suppose A6: len (P*F1) = 0; then
P*F1 = {}; then
F1 = {} by A4; then
rng F1 = {}; then
Union F2 = {} by A1,CARD_3:def 4,ZFMISC_1:2; then
A7: union rng F2 = {} by CARD_3:def 4;
defpred S[Nat] means $1 <= len(P*F2) implies SMF2.$1 = 0;
A8: S[0] by A3;
A9: for i be Nat st S[i] holds S[i+1]
proof
let i be Nat;
assume A10: S[i];
assume A11: i+1 <= len (P*F2); then
A13: SMF2.(i+1) = SMF2.i + (P*F2).(i+1) & SMF2.i = 0 by A3,A10,NAT_1:13;
A14: i+1 in dom(P*F2) by A11,NAT_1:11,FINSEQ_3:25; then
F2.(i+1) = {} by A4,A7,ORDERS_1:6,FUNCT_1:3; then
P.(F2.(i+1)) = 0 by VALUED_0:def 19; then
(P*F2).(i+1) = 0 by A14,FUNCT_1:12;
hence SMF2.(i+1) = 0 by A13;
end;
for i be Nat holds S[i] from NAT_1:sch 2(A8,A9);
hence Sum(P*F1) = Sum(P*F2) by A2,A3,A6;
end;
suppose B6: len (P*F2) = 0; then
P*F2 = {}; then
F2 = {} by A4; then
rng F2 = {}; then
Union F1 = {} by A1,CARD_3:def 4,ZFMISC_1:2; then
B7: union rng F1 = {} by CARD_3:def 4;
defpred S[Nat] means $1 <= len(P*F1) implies SMF1.$1 = 0;
B8: S[0] by A2;
B9: for i be Nat st S[i] holds S[i+1]
proof
let i be Nat;
assume B10: S[i];
assume B11: i+1 <= len (P*F1); then
B13: SMF1.(i+1) = SMF1.i + (P*F1).(i+1) & SMF1.i = 0 by A2,B10,NAT_1:13;
B14: i+1 in dom(P*F1) by B11,NAT_1:11,FINSEQ_3:25; then
F1.(i+1) = {} by A4,B7,ORDERS_1:6,FUNCT_1:3; then
P.(F1.(i+1)) = 0 by VALUED_0:def 19; then
(P*F1).(i+1) = 0 by B14,FUNCT_1:12;
hence SMF1.(i+1) = 0 by B13;
end;
for i be Nat holds S[i] from NAT_1:sch 2(B8,B9);
hence Sum(P*F1) = Sum(P*F2) by A2,A3,B6;
end;
suppose
A15: len (P*F1) <> 0 & len (P*F2) <> 0;
defpred Mx[Nat,Nat,set] means $3 = P.(F1.$1 /\ F2.$2);
MX0: for i,j be Nat st [i,j] in [:Seg len F1, Seg len F2:]
ex A be Element of ExtREAL st Mx[i,j,A];
consider Mx be Matrix of len F1,len F2,ExtREAL such that
MX1: for i,j be Nat st
[i,j] in Indices Mx holds Mx[i,j,Mx*(i,j)] from MATRIX_0:sch 2(MX0);
C3: len Mx = len F1 by MATRIX_0:def 2; then
C4: width Mx = len F2 by A15,A5,MATRIX_0:20;
CC0: for F be disjoint_valued FinSequence of S st Union F in S
holds P.(Union F) = Sum(P*F) by Def8;
F1 is non empty & F2 is non empty by A15; then
C10: Sum(P*F1) = SumAll(Mx) & Sum(P*F2) = SumAll(Mx@)
by A1,MX1,CC0,Th40,Th41;
for i be Nat st i in dom Mx holds not -infty in rng(Mx.i)
proof
let i be Nat;
assume F1: i in dom Mx;
assume -infty in rng(Mx.i); then
consider j be object such that
F2: j in dom(Mx.i) & (Mx.i).j = -infty by FUNCT_1:def 3;
reconsider j as Nat by F2;
F3: [i,j] in Indices Mx by F1,F2,MATRPROB:13; then
(Mx.i).j = Mx*(i,j) by MATRPROB:14; then
F5: (Mx.i).j = P.(F1.i /\ F2.j) by F3,MX1;
i in Seg len Mx & j in Seg width Mx by F3,MATRPROB:12; then
i in dom F1 & j in dom F2 by C3,C4,FINSEQ_1:def 3; then
F1.i in rng F1 & F2.j in rng F2 by FUNCT_1:3; then
F1.i /\ F2.j in S by FINSUB_1:def 2;
hence contradiction by F2,F5,MEASURE1:def 2;
end;
hence Sum(P*F1) = Sum(P*F2) by C10,Th28;
end;
end;
end;
theorem Th55:
for X be set, S be semialgebra_of_sets of X, P be pre-Measure of S
ex M be Measure of Field_generated_by S
st for A be set st A in Field_generated_by S holds
for F be disjoint_valued FinSequence of S
st A = Union F holds M.A = Sum(P*F)
proof
let X be set, S be semialgebra_of_sets of X, P be pre-Measure of S;
defpred P[object,object] means
for F be disjoint_valued FinSequence of S
st $1 = Union F holds $2 = Sum(P*F);
A1:for A be object st A in Field_generated_by S
ex p be object st p in ExtREAL & P[A,p]
proof
let A be object;
assume A in Field_generated_by S; then
A in DisUnion S by SRINGS_3:22; then
consider V be Subset of X such that
A3: A = V & ex F be disjoint_valued FinSequence of S st V = Union F;
consider F be disjoint_valued FinSequence of S such that
A4: V = Union F by A3;
set p = Sum(P*F);
take p;
thus p in ExtREAL & P[A,p] by A3,A4,Th54;
end;
consider M be Function of (Field_generated_by S),ExtREAL such that
A5: for A be object st A in Field_generated_by S holds P[A,M.A]
from FUNCT_2:sch 1(A1);
A18:for A be Element of Field_generated_by S holds 0 <= M.A
proof
let A be Element of Field_generated_by S;
A in Field_generated_by S; then
A in DisUnion S by SRINGS_3:22; then
consider V be Subset of X such that
A7: A = V & ex F be disjoint_valued FinSequence of S st V = Union F;
consider F be disjoint_valued FinSequence of S such that
A8: V = Union F by A7;
consider PF be sequence of ExtREAL such that
A10: Sum(P*F) = PF.(len(P*F)) & PF.0 = 0. &
for i be Nat st i < len(P*F) holds PF.(i+1) = PF.i + (P*F).(i+1)
by EXTREAL1:def 2;
defpred P2[Nat] means $1 <= len(P*F) implies PF.$1 >= 0;
A11:P2[0] by A10;
A12:for i be Nat st P2[i] holds P2[i+1]
proof
let i be Nat;
assume A13: P2[i];
assume A14: i+1 <= len(P*F); then
i+1 in dom(P*F) by NAT_1:11,FINSEQ_3:25; then
(P*F).(i+1) = P.(F.(i+1)) by FUNCT_1:12; then
A17: (P*F).(i+1) >= 0 by SUPINF_2:51;
PF.(i+1) = PF.i + (P*F).(i+1) by A14,A10,NAT_1:13;
hence PF.(i+1) >= 0 by A13,A14,NAT_1:13,A17;
end;
for i be Nat holds P2[i] from NAT_1:sch 2(A11,A12); then
Sum(P*F) >= 0 by A10;
hence 0 <= M.A by A7,A8,A5;
end;
A29:for A,B be Element of Field_generated_by S
st A misses B holds M.(A \/ B) = M.A + M.B
proof
let A,B be Element of Field_generated_by S;
assume A19: A misses B;
A in Field_generated_by S; then
A in DisUnion S by SRINGS_3:22; then
consider V be Subset of X such that
A20: A = V & ex F be disjoint_valued FinSequence of S st V = Union F;
consider F be disjoint_valued FinSequence of S such that
A21: V = Union F by A20;
B in Field_generated_by S; then
B in DisUnion S by SRINGS_3:22; then
consider W be Subset of X such that
A22: B = W & ex G be disjoint_valued FinSequence of S st W = Union G;
consider G be disjoint_valued FinSequence of S such that
A23: W = Union G by A22;
set H = F^G;
A24:A = union rng F & B = union rng G by A20,A21,A22,A23,CARD_3:def 4; then
reconsider H as disjoint_valued FinSequence of S by A19,Th43;
rng H = rng F \/ rng G by FINSEQ_1:31; then
union rng H = union rng F \/ union rng G by ZFMISC_1:78; then
A \/ B = Union H by A24,CARD_3:def 4; then
A25:M.(A \/ B) = Sum(P*H) by A5;
A26:M.A = Sum(P*F) & M.B = Sum(P*G) by A20,A21,A22,A23,A5;
P*F is nonnegative by Th45; then
A27:not -infty in rng(P*F) by SUPINF_2:def 12,def 9;
P*G is nonnegative by Th45; then
A28:not -infty in rng(P*G) by SUPINF_2:def 12,def 9;
P*H = (P*F)^(P*G) by FINSEQOP:9;
hence M.(A \/ B) = M.A + M.B by A25,A26,A27,A28,EXTREAL1:10;
end;
reconsider E = {} as Element of S by SETFAM_1:def 8;
reconsider F = <*E*> as disjoint_valued FinSequence of S;
rng F = {{}} by FINSEQ_1:38; then
union rng F = {} by ZFMISC_1:25; then
Union F = {} by CARD_3:def 4; then
M.{} = Sum(P*F) by A5,FINSUB_1:7; then
M.{} = Sum(<*P.{}*>) by FINSEQ_2:35; then
M.{} = P.{} by EXTREAL1:8; then
M.{} = 0 by VALUED_0:def 19; then
reconsider M as nonnegative additive zeroed Function of
(Field_generated_by S),ExtREAL
by A18,A29,VALUED_0:def 19,MEASURE1:def 2,def 8;
take M;
thus thesis by A5;
end;
theorem
for F be ExtREAL_sequence, n be Nat, a be R_eal st
(for k be Nat holds F.k = a) holds (Partial_Sums F).n = a*(n+1)
proof
let F be ExtREAL_sequence, n be Nat, a be R_eal;
assume A1: for k be Nat holds F.k = a;
defpred P[Nat] means (Partial_Sums F).$1 = a*($1 + 1);
(Partial_Sums F).0 = F.0 by MESFUNC9:def 1; then
(Partial_Sums F).0 = a by A1; then
A2:P[0] by XXREAL_3:81;
A3:for i be Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume A4: P[i];
i+1 in REAL & 1 in REAL by XREAL_0:def 1; then
reconsider i1= i+1, One=1 as R_eal by XBOOLE_0:def 3,XXREAL_0:def 4;
(Partial_Sums F).(i+1) = (Partial_Sums F).i + F.(i+1)
by MESFUNC9:def 1; then
(Partial_Sums F).(i+1) = a*(i+1) + a by A1,A4; then
(Partial_Sums F).(i+1) = a*(i+1) + a*1 by XXREAL_3:81; then
(Partial_Sums F).(i+1) = a*((i1)+One) by XXREAL_3:96;
hence P[i+1] by XXREAL_3:def 2;
end;
for i be Nat holds P[i] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
theorem Th57:
for X be non empty set, F be sequence of X, n be Nat
holds rng(F|Segm(n+1)) = rng(F|Segm n) \/ {F.n}
proof
let X be non empty set, F be sequence of X, n be Nat;
now let y be object;
assume y in rng(F|Segm(n+1)); then
consider x be object such that
A1: x in dom(F|Segm(n+1)) & y = (F|Segm(n+1)).x by FUNCT_1:def 3;
reconsider x as Nat by A1;
A4: y = F.x by A1,FUNCT_1:47;
x in dom F /\ Segm(n+1) by A1,RELAT_1:61; then
A2: x in dom F & x in Segm(n+1) by XBOOLE_0:def 4;
x < n+1 by A2,NAT_1:44; then
A3: x <= n by NAT_1:13;
per cases;
suppose x = n; then
y in {F.n} by A4,TARSKI:def 1;
hence y in rng(F|Segm n) \/ {F.n} by XBOOLE_0:def 3;
end;
suppose x <> n; then
x < n by A3,XXREAL_0:1; then
x in Segm n by NAT_1:44; then
x in dom F /\ Segm n by A2,XBOOLE_0:def 4; then
x in dom(F|Segm n) by RELAT_1:61; then
(F|Segm n).x in rng(F|Segm n) & (F|Segm n).x = F.x by FUNCT_1:3,47;
hence y in rng(F|Segm n) \/ {F.n} by A4,XBOOLE_0:def 3;
end;
end; then
A5:rng(F|Segm(n+1)) c= rng(F|Segm n) \/ {F.n} by TARSKI:def 3;
now let y be object;
assume A6: y in rng(F|Segm n) \/ {F.n};
per cases by A6,XBOOLE_0:def 3;
suppose A7: y in rng(F|Segm n);
n <= n+1 by NAT_1:11; then
F|Segm n c= F|Segm(n+1) by NAT_1:39,RELAT_1:75; then
rng(F|Segm n) c= rng(F|Segm(n+1)) by RELAT_1:11;
hence y in rng(F|Segm(n+1)) by A7;
end;
suppose y in {F.n}; then
A8: y = F.n by TARSKI:def 1;
n in NAT by ORDINAL1:def 12; then
n in dom F & n in Segm(n+1) by FUNCT_2:def 1,NAT_1:45; then
n in dom F /\ Segm(n+1) by XBOOLE_0:def 4; then
A9: n in dom(F|Segm(n+1)) by RELAT_1:61; then
F.n = (F|Segm(n+1)).n by FUNCT_1:47;
hence y in rng(F|Segm(n+1)) by A8,A9,FUNCT_1:3;
end;
end; then
rng(F|Segm n) \/ {F.n} c= rng(F|Segm(n+1)) by TARSKI:def 3;
hence thesis by A5,XBOOLE_0:def 10;
end;
theorem Th58:
for X be set, S be Field_Subset of X, M be Measure of S,
F be Sep_Sequence of S, n be Nat
holds union rng(F|Segm(n+1)) in S
& Partial_Sums(M*F).n = M.(union rng(F|Segm(n+1)))
proof
let X be set, S be Field_Subset of X, M be Measure of S,
F be Sep_Sequence of S, n be Nat;
A2: rng(F|Segm(0+1)) = rng(F|Segm 0) \/ {F.0} by Th57
.= {F.0}; then
A2a:union rng(F|Segm(0+1)) = F.0 by ZFMISC_1:25;
defpred P2[Nat] means union rng(F|Segm($1+1)) in S;
A14:P2[0] by A2a;
A15:for k be Nat st P2[k] holds P2[k+1]
proof
let k be Nat;
assume A16: P2[k];
union rng(F|Segm(k+1+1))
= union(rng(F|Segm(k+1)) \/ {F.(k+1)}) by Th57
.= union rng(F|Segm(k+1)) \/ union {F.(k+1)} by ZFMISC_1:78
.= union rng(F|Segm(k+1)) \/ F.(k+1) by ZFMISC_1:25;
hence union rng(F|Segm(k+1+1)) in S by A16,PROB_1:3;
end;
P1: for k be Nat holds P2[k] from NAT_1:sch 2(A14,A15);
hence union rng(F|Segm(n+1)) in S;
defpred P[Nat] means Partial_Sums(M*F).$1 = M.(union rng (F|Segm ($1+1)));
A1: Partial_Sums(M*F).0 = (M*F).0 by MESFUNC9:def 1
.= M.(F.0) by FUNCT_2:15;
A3: P[0] by A1,A2,ZFMISC_1:25;
A4: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A5: P[n];
A6: Partial_Sums(M*F).(n+1) = Partial_Sums(M*F).n + (M*F).(n+1)
by MESFUNC9:def 1
.= M.(union rng(F|Segm(n+1))) + M.(F.(n+1)) by A5,FUNCT_2:15;
A13: now assume ex x be object st x in union rng(F|Segm(n+1)) /\ F.(n+1); then
consider x be object such that
A7: x in union rng(F|Segm(n+1)) /\ F.(n+1);
A8: x in union rng(F|Segm(n+1)) & x in F.(n+1) by A7,XBOOLE_0:def 4; then
consider A be set such that
A9: x in A & A in rng(F|Segm(n+1)) by TARSKI:def 4;
consider k be object such that
A10: k in dom(F|Segm(n+1)) & A = (F|Segm(n+1)).k by A9,FUNCT_1:def 3;
reconsider k as Nat by A10;
A11: k < n+1 by A10,RELAT_1:57,NAT_1:44;
A = F.k by A10,FUNCT_1:47; then
x in F.k /\ F.(n+1) by A8,A9,XBOOLE_0:def 4;
hence contradiction by A11,PROB_2:def 2,XBOOLE_0:4;
end;
union rng(F|Segm(n+1)) in S by P1; then
M.(union rng(F|Segm(n+1))) + M.(F.(n+1))
= M.(union rng(F|Segm(n+1)) \/ F.(n+1)) by A13,XBOOLE_0:4,MEASURE1:def 8
.= M.( union rng(F|Segm(n+1)) \/ union {F.(n+1)} ) by ZFMISC_1:25
.= M.( union (rng(F|Segm(n+1)) \/ {F.(n+1)}) ) by ZFMISC_1:78
.= M.( union rng(F|Segm(n+1+1)) ) by Th57;
hence thesis by A6;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A3,A4);
hence Partial_Sums(M*F).n = M.(union rng (F|Segm (n+1)));
end;
theorem Th59:
for X be set, S be semialgebra_of_sets of X,
P be pre-Measure of S, M be Measure of Field_generated_by S
st ( for A be set st A in Field_generated_by S holds
for F be disjoint_valued FinSequence of S
st A = Union F holds M.A = Sum(P*F) )
holds M is completely-additive
proof
let X be set, S be semialgebra_of_sets of X,
P be pre-Measure of S, M be Measure of Field_generated_by S;
assume
A1: for A be set st A in Field_generated_by S holds
for F be disjoint_valued FinSequence of S st A = Union F
holds M.A = Sum(P*F);
now let FSets be Sep_Sequence of Field_generated_by S;
assume B0: union rng FSets in Field_generated_by S; then
union rng FSets in DisUnion S by SRINGS_3:22; then
consider A be Subset of X such that
B1: A = union rng FSets
& ex F be disjoint_valued FinSequence of S st A = Union F;
consider D be disjoint_valued FinSequence of S such that
B2: A = Union D by B1;
set Z = {[n,E] where n is Nat, E is disjoint_valued FinSequence of S
: Union E = FSets.n & (FSets.n={} implies E = <*{}*>) };
reconsider Y = proj2 Z as FinSequenceSet of S by Th51;
E4: Y is with_non-empty_elements by Th51;
per cases;
suppose rng FSets is with_non-empty_element; then
consider a be non empty set such that
E6: a in rng FSets;
ex E be FinSequence of S st E in Y & Union E = a by E6,Th51; then
reconsider Y as non empty with_non-empty_element FinSequenceSet of S
by E4;
defpred P[Element of NAT,object] means [$1,$2] in Z;
F2: for n be Element of NAT ex y be Element of Y st P[n,y]
proof
let n be Element of NAT;
FSets.n in Field_generated_by S; then
FSets.n in DisUnion S by SRINGS_3:22; then
consider A be Subset of X such that
F3: FSets.n = A
& ex F be disjoint_valued FinSequence of S st A = Union F;
consider F be disjoint_valued FinSequence of S such that
F4: A = Union F by F3;
per cases;
suppose F5: FSets.n = {};
F6: rng <*{}*> = { {} } by FINSEQ_1:38;
{} in S by SETFAM_1:def 8; then
reconsider E = <*{}*> as disjoint_valued FinSequence of S
by F6,ZFMISC_1:31,FINSEQ_1:def 4;
union rng E = {} by F6,ZFMISC_1:25; then
Union E = {} by CARD_3:def 4; then
F7: [n,E] in Z by F5; then
E in Y by XTUPLE_0:def 13;
hence ex y be Element of Y st P[n,y] by F7;
end;
suppose FSets.n <> {}; then
F8: [n,F] in Z by F4,F3; then
F in Y by XTUPLE_0:def 13;
hence ex y be Element of Y st P[n,y] by F8;
end;
end;
consider s be Function of NAT,Y such that
F9: for n be Element of NAT holds P[n,s.n] from FUNCT_2:sch 3(F2);
now let n be object;
assume n in dom s; then
reconsider n1=n as Element of NAT;
[n1,s.n1] in Z by F9; then
F11: ex m be Nat, E be disjoint_valued FinSequence of S st
[n1,s.n1] = [m,E] & Union E = FSets.m & (FSets.m={} implies E=<*{}*>);
now assume
F15: s.n = {}; then
union rng(s.n1) = {} by ZFMISC_1:2; then
Union s.n1 = {} by CARD_3:def 4;
hence contradiction by F11,F15,XTUPLE_0:1;
end;
hence s.n is non empty;
end; then
reconsider s as non-empty sequence of Y by FUNCT_1:def 9;
reconsider G = joined_seq s as sequence of S;
now let x,y be object;
assume F16: x <> y;
per cases;
suppose not x in NAT or not y in NAT; then
not x in dom G or not y in dom G; then
G.x = {} or G.y = {} by FUNCT_1:def 2;
hence G.x misses G.y by XBOOLE_1:65;
end;
suppose x in NAT & y in NAT; then
reconsider n1=x, n2=y as Element of NAT;
consider k1,m1 be Nat such that
F17: m1 in dom(s.k1) & (Partial_Sums(Length s)).k1 - len(s.k1) + m1-1 = n1
& G.n1 = (s.k1).m1 by Def4;
consider k2,m2 be Nat such that
F18: m2 in dom(s.k2) & (Partial_Sums(Length s)).k2 - len(s.k2) + m2-1 = n2
& G.n2 = (s.k2).m2 by Def4;
k1 is Element of NAT & k2 is Element of NAT by ORDINAL1:def 12; then
F21: [k1,s.k1] in Z & [k2,s.k2] in Z by F9; then
consider i1 be Nat, E1 be disjoint_valued FinSequence of S such that
F22: [k1,s.k1] = [i1,E1]
& Union E1 = FSets.i1 & (FSets.i1={} implies E1 = <*{}*>);
consider i2 be Nat, E2 be disjoint_valued FinSequence of S such that
F23: [k2,s.k2] = [i2,E2]
& Union E2 = FSets.i2 & (FSets.i2={} implies E2 = <*{}*>) by F21;
F24: k1=i1 & s.k1=E1 & k2=i2 & s.k2=E2 by F22,F23,XTUPLE_0:1;
now assume k1<>k2; then
FSets.i1 misses FSets.i2 by F24,PROB_2:def 2; then
union rng(s.k1) misses Union(s.k2) by F22,F23,F24,CARD_3:def 4; then
F25: union rng(s.k1) misses union rng(s.k2) by CARD_3:def 4;
G.n1 c= union rng(s.k1) & G.n2 c= union rng(s.k2)
by F17,F18,FUNCT_1:3,ZFMISC_1:74;
hence G.n1 misses G.n2 by F25,XBOOLE_1:64;
end;
hence G.x misses G.y by F16,F17,F18,F24,PROB_2:def 2;
end;
end; then
reconsider G as disjoint_valued sequence of S by PROB_2:def 2;
now let x be object;
assume x in Union FSets; then
x in union rng FSets by CARD_3:def 4; then
consider A be set such that
G1: x in A & A in rng FSets by TARSKI:def 4;
consider n be Element of NAT such that
G2: A = FSets.n by G1,FUNCT_2:113;
[n,s.n] in Z by F9; then
consider n2 be Nat, E2 be disjoint_valued FinSequence of S such that
G6: [n,s.n] = [n2,E2]
& Union E2 = FSets.n2 & (FSets.n2={} implies E2=<*{}*>);
n=n2 & s.n = E2 by G6,XTUPLE_0:1; then
x in union rng(s.n) by G1,G2,G6,CARD_3:def 4; then
consider A2 be set such that
G8: x in A2 & A2 in rng (s.n) by TARSKI:def 4;
consider m be object such that
G9: m in dom (s.n) & A2 = (s.n).m by G8,FUNCT_1:def 3;
reconsider m as Nat by G9;
consider N be Nat such that
G10: N = (Partial_Sums(Length s)).n - len(s.n) + m - 1
& G.N = (s.n).m by G9,Th13;
A2 in rng G by FUNCT_2:4,G9,G10,ORDINAL1:def 12; then
x in union rng G by G8,TARSKI:def 4;
hence x in Union G by CARD_3:def 4;
end; then
T0: Union FSets c= Union G by TARSKI:def 3;
now let x be object;
assume x in Union G; then
x in union rng G by CARD_3:def 4; then
consider A be set such that
G11: x in A & A in rng G by TARSKI:def 4;
consider n be Element of NAT such that
G12: A = G.n by G11,FUNCT_2:113;
consider k,m be Nat such that
G13: m in dom(s.k) & (Partial_Sums(Length s)).k - len(s.k) + m - 1 = n
& G.n = (s.k).m by Def4;
k is Element of NAT by ORDINAL1:def 12; then
[k,s.k] in Z by F9; then
consider k2 be Nat, E be disjoint_valued FinSequence of S such that
G14: [k,s.k] = [k2,E] & Union E = FSets.k2 & (FSets.k2={} implies E=<*{}*>);
G15: k = k2 & s.k = E by G14,XTUPLE_0:1;
x in (s.k).m & (s.k).m in rng(s.k) by G11,G12,G13,FUNCT_1:3; then
x in union rng(s.k) by TARSKI:def 4; then
G16: x in FSets.k2 by G14,G15,CARD_3:def 4;
FSets.k2 in rng FSets by FUNCT_2:4,ORDINAL1:def 12; then
x in union rng FSets by G16,TARSKI:def 4;
hence x in Union FSets by CARD_3:def 4;
end; then
Union G c= Union FSets by TARSKI:def 3; then
T1: Union FSets = Union G by T0,XBOOLE_0:def 10;
defpred Q[Nat,Nat,object] means
($1 + 1 <= len D implies $3 = D.($1 +1) /\ G.$2)
& ($1 + 1 > len D implies $3 = {});
D0: for i be Element of NAT for j be Element of NAT
ex z be Element of S st Q[i,j,z]
proof
let i,j be Element of NAT;
per cases;
suppose D1: i+1 <= len D; then
i+1 in dom D by NAT_1:11,FINSEQ_3:25; then
D.(i+1) in rng D by FUNCT_1:3; then
D.(i+1) /\ G.j in S by FINSUB_1:def 2;
hence ex z be Element of S st Q[i,j,z] by D1;
end;
suppose D4: i+1 > len D;
{} in S by SETFAM_1:def 8;
hence ex z be Element of S st Q[i,j,z] by D4;
end;
end;
consider LG be Function of [:NAT,NAT:],S such that
D5: for i be Element of NAT for j be Element of NAT
holds Q[i,j,LG.(i,j)] from BINOP_1:sch 3(D0);
D5a: for i,j be Nat holds
(i+1 <= len D implies LG.(i,j) = D.(i+1) /\ G.j)
& (i+1 > len D implies LG.(i,j) = {})
proof
let i,j be Nat;
reconsider i1=i, j1=j as Element of NAT by ORDINAL1:def 12;
DD5: now assume i+1 <= len D; then
LG.(i1,j1) = D.(i+1) /\ G.j by D5;
hence LG.(i,j) = D.(i+1) /\ G.j;
end;
now assume i+1 > len D; then
LG.(i1,j1) = {} by D5;
hence LG.(i,j) = {};
end;
hence thesis by DD5;
end;
Union FSets = union rng FSets by CARD_3:def 4; then
X2: M.(Union FSets) = Sum(P*D) by A1,B0,B1,B2;
consider SumPD be sequence of ExtREAL such that
X3: Sum(P*D) = SumPD.(len(P*D)) & SumPD.0 = 0.
& for i be Nat st i < len(P*D) holds SumPD.(i+1) = SumPD.i + (P*D).(i+1)
by EXTREAL1:def 2;
X4: for i be Element of NAT st i < len D holds
D.(i+1) = Union ProjMap1(LG,i)
proof
let i be Element of NAT;
assume X40: i < len D; then
1 <= i+1 & i+1 <= len D by NAT_1:11,13; then
i+1 in dom D by FINSEQ_3:25; then
X41: D.(i+1) in rng D by FUNCT_1:3;
now let x be object;
assume X44: x in D.(i+1); then
x in union rng D by X41,TARSKI:def 4; then
x in Union D by CARD_3:def 4; then
x in Union G by B1,B2,T1,CARD_3:def 4; then
x in union rng G by CARD_3:def 4; then
consider Gx be set such that
X42: x in Gx & Gx in rng G by TARSKI:def 4;
consider j be Element of NAT such that
X43: Gx = G.j by X42,FUNCT_2:113;
X46: dom ProjMap1(LG,i) = NAT by FUNCT_2:def 1;
X45: x in D.(i+1) /\ G.j by X44,X42,X43,XBOOLE_0:def 4;
i+1 <= len D implies LG.(i,j) = D.(i+1) /\ G.j by D5; then
X47: x in ProjMap1(LG,i).j by X40,NAT_1:13,X45,MESFUNC9:def 6;
ProjMap1(LG,i).j in rng ProjMap1(LG,i) by X46,FUNCT_1:3; then
x in union rng ProjMap1(LG,i) by X47,TARSKI:def 4;
hence x in Union ProjMap1(LG,i) by CARD_3:def 4;
end; then
X48: D.(i+1) c= Union ProjMap1(LG,i) by TARSKI:def 3;
now let x be object;
assume x in Union ProjMap1(LG,i); then
x in union rng ProjMap1(LG,i) by CARD_3:def 4; then
consider Px be set such that
X50: x in Px & Px in rng ProjMap1(LG,i) by TARSKI:def 4;
consider j be Element of NAT such that
X51: Px = ProjMap1(LG,i).j by X50,FUNCT_2:113;
ProjMap1(LG,i).j = LG.(i,j) by MESFUNC9:def 6; then
x in D.(i+1) /\ G.j by X50,X51,D5;
hence x in D.(i+1) by XBOOLE_0:def 4;
end; then
Union ProjMap1(LG,i) c= D.(i+1) by TARSKI:def 3;
hence thesis by X48,XBOOLE_0:def 10;
end;
X5: for i be Element of NAT st i < len D holds
(P*D).(i+1) <= (lim_in_cod2(Partial_Sums_in_cod2(P*LG))).i
proof
let i be Element of NAT;
assume X50: i < len D; then
X50a: 1 <= i+1 & i+1 <= len D by NAT_1:11,13; then
X51: i+1 in dom D by FINSEQ_3:25; then
X52: D.(i+1) in rng D by FUNCT_1:3;
now let x,y be object;
assume V1: x<>y;
per cases;
suppose
not x in dom(ProjMap1(LG,i)) or not y in dom(ProjMap1(LG,i)); then
ProjMap1(LG,i).x = {} or ProjMap1(LG,i).y = {} by FUNCT_1:def 2;
hence ProjMap1(LG,i).x misses ProjMap1(LG,i).y by XBOOLE_1:65;
end;
suppose x in dom(ProjMap1(LG,i)) & y in dom(ProjMap1(LG,i)); then
reconsider x1=x,y1=y as Element of NAT;
ProjMap1(LG,i).x = LG.(i,x1) & ProjMap1(LG,i).y = LG.(i,y1)
by MESFUNC9:def 6; then
ProjMap1(LG,i).x = D.(i+1) /\ G.x1 & ProjMap1(LG,i).y = D.(i+1) /\ G.y1
by X50a,D5;
hence ProjMap1(LG,i).x misses ProjMap1(LG,i).y
by V1,PROB_2:def 2,XBOOLE_1:76;
end;
end; then
X53: ProjMap1(LG,i) is disjoint_valued Function of NAT,S by PROB_2:def 2;
X54: D.(i+1) = Union ProjMap1(LG,i) by X4,X50;
X55: (P*D).(i+1) = P.(D.(i+1)) by X51,FUNCT_1:13
.= P.(Union ProjMap1(LG,i)) by X4,X50;
X56: now let k be Element of NAT;
P.(LG.(i,k)) = (P*LG).(i,k) by ZFMISC_1:87,FUNCT_2:15; then
ProjMap1(P*LG,i).k = P.(LG.(i,k)) by MESFUNC9:def 6
.= P.(ProjMap1(LG,i).k) by MESFUNC9:def 6;
hence (P*ProjMap1(LG,i)).k = (ProjMap1(P*LG,i)).k by FUNCT_2:15;
end;
SUM(P*(ProjMap1(LG,i))) = Sum(P*(ProjMap1(LG,i))) by MEASURE8:2
.= lim Partial_Sums(P*ProjMap1(LG,i)) by MESFUNC9:def 3
.= lim Partial_Sums(ProjMap1(P*LG,i)) by X56,FUNCT_2:def 8
.= lim ProjMap1(Partial_Sums_in_cod2(P*LG),i) by DBLSEQ_3:53
.= (lim_in_cod2(Partial_Sums_in_cod2(P*LG))).i by DBLSEQ_3:def 13;
hence thesis by X55,X52,X53,X54,Def8;
end;
defpred SPD[Nat] means
$1 < len(P*D) implies
SumPD.($1+1)
<= (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG)))).$1;
rng D c= S; then
rng D c= dom P by FUNCT_2:def 1; then
dom(P*D) = dom D by RELAT_1:27; then
X71: len(P*D) = len D by FINSEQ_3:29;
now assume X60: 0 < len(P*D); then
X61: (P*D).(0+1) <= (lim_in_cod2(Partial_Sums_in_cod2(P*LG))).0 by X5,X71;
SumPD.(0+1) = SumPD.0 + (P*D).(0+1) by X60,X3; then
SumPD.(0+1) = (P*D).1 by X3,XXREAL_3:4;
hence SumPD.(0+1)
<= (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG)))).0
by X61,MESFUNC9:def 1;
end; then
X62: SPD[0];
X63: for k be Nat st SPD[k] holds SPD[k+1]
proof
let k be Nat;
assume X64: SPD[k];
assume X65: k+1 < len(P*D); then
X67: (P*D).(k+1+1) <= (lim_in_cod2(Partial_Sums_in_cod2(P*LG))).(k+1)
by X5,X71;
SumPD.(k+1+1) = SumPD.(k+1) + (P*D).(k+1+1) by X3,X65; then
SumPD.(k+1+1)
<= (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG)))).k
+ (lim_in_cod2(Partial_Sums_in_cod2(P*LG))).(k+1)
by NAT_1:13,X67,X64,X65,XXREAL_3:36;
hence SumPD.(k+1+1)
<= (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG)))).(k+1)
by MESFUNC9:def 1;
end;
X68: for k be Nat holds SPD[k] from NAT_1:sch 2(X62,X63);
XX70:now assume D = {}; then
union rng D = {} by ZFMISC_1:2; then
X69: union rng FSets = {} by B1,B2,CARD_3:def 4;
union {a} c= union rng FSets by E6,ZFMISC_1:31,77;
hence contradiction by X69;
end; then
consider i1 be Nat such that
X70: len D = i1 + 1 by NAT_1:6;
reconsider i1 as Element of NAT by ORDINAL1:def 12;
i1 < len D by X70,NAT_1:13; then
X72: Sum(P*D)
<= (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG)))).i1
by X70,X71,X68,X3;
X73: len(P*D) >= i1 by X70,X71,NAT_1:11;
W3: Partial_Sums_in_cod2(P*LG) is convergent_in_cod2 by DBLSEQ_3:66; then
X80: lim_in_cod2(Partial_Sums_in_cod2(P*LG)) is nonnegative
by DBLSEQ_3:65; then
X74: (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG)))).i1
<= (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG)))).(len(P*D))
by X73,RINFSUP2:7,MESFUNC9:16;
(Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG)))).(len(P*D))
= (lim_in_cod2(Partial_Sums(P*LG))).(len(P*D))
proof
per cases;
suppose
X75: (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG)))).(len(P*D))
= +infty; then
ex k be Element of NAT st k <= len(P*D) &
ProjMap1(Partial_Sums_in_cod2(P*LG),k) is convergent_to_+infty
by DBLSEQ_3:74; then
lim ProjMap1(Partial_Sums_in_cod2(Partial_Sums_in_cod1(P*LG)),len(P*D))
= +infty by DBLSEQ_3:77; then
lim ProjMap1(Partial_Sums(P*LG),len(P*D)) = +infty by DBLSEQ_3:def 16;
hence
(Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG)))).(len(P*D))
= (lim_in_cod2(Partial_Sums(P*LG))).(len(P*D)) by X75,DBLSEQ_3:def 13;
end;
suppose
(Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG)))).(len(P*D))
<> +infty; then
X81: (Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG)))).(len(P*D))
< +infty by XXREAL_0:4;
for m be Element of NAT holds
ProjMap1(Partial_Sums_in_cod2(P*LG),m) is convergent_to_finite_number
proof
let m be Element of NAT;
W5: ProjMap1(Partial_Sums_in_cod2(P*LG),m) is convergent_to_+infty
or ProjMap1(Partial_Sums_in_cod2(P*LG),m) is convergent_to_finite_number
or ProjMap1(Partial_Sums_in_cod2(P*LG),m) is convergent_to_-infty
by W3,DBLSEQ_3:def 11,MESFUNC5:def 11;
per cases;
suppose m <= len(P*D); then
W1: Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG))).m
<= Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG))).(len(P*D))
by X80,MESFUNC9:16,RINFSUP2:7;
(lim_in_cod2(Partial_Sums_in_cod2(P*LG))).m
<= Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG))).m
by X80,DBLSEQ_3:4; then
W2: (lim_in_cod2(Partial_Sums_in_cod2(P*LG))).m
<= Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG))).(len(P*D))
by W1,XXREAL_0:2;
(lim_in_cod2(Partial_Sums_in_cod2(P*LG))).m >= 0
by X80,SUPINF_2:51; then
(lim_in_cod2(Partial_Sums_in_cod2(P*LG))).m in REAL
by W2,X81,XXREAL_0:14; then
lim ProjMap1(Partial_Sums_in_cod2(P*LG),m) in REAL
by DBLSEQ_3:def 13;
hence ProjMap1(Partial_Sums_in_cod2(P*LG),m)
is convergent_to_finite_number
by W5,MESFUNC5:def 12;
end;
suppose m > len(P*D); then
consider j be Nat such that
W7: m = len(P*D) + j by NAT_1:10;
defpred H[Nat] means
Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG))).(len(P*D)+$1)
= Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG))).(len(P*D));
W8: H[0];
W9: for i be Nat st H[i] holds H[i+1]
proof
let i be Nat;
assume W12: H[i];
W13: Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG))).(len(P*D)+i+1)
= Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG))).len(P*D)
+ (lim_in_cod2(Partial_Sums_in_cod2(P*LG))).(len(P*D)+i+1)
by W12,MESFUNC9:def 1;
for s be Nat holds
ProjMap1(Partial_Sums_in_cod2(P*LG),len(P*D)+i+1).s = 0
proof
let s be Nat;
reconsider s1 = s as Element of NAT by ORDINAL1:def 12;
W15: ProjMap1(Partial_Sums_in_cod2(P*LG),len(P*D)+i+1).s1
= (Partial_Sums_in_cod2(P*LG)).(len(P*D)+i+1,s)
by MESFUNC9:def 6;
P0: for k,j be Nat holds (P*LG).(len(P*D)+k+1,j) = 0
proof
let k,j be Nat;
reconsider k1=k, j1=j as Element of NAT by ORDINAL1:def 12;
len D + k +1 >= len D by NAT_1:11,12; then
P1: len D + k1 + 1 + 1> len D by NAT_1:13;
[len(P*D)+k1+1,j1] in [:NAT,NAT:] by ZFMISC_1:87; then
[len(P*D)+k1+1,j1] in dom LG by FUNCT_2:def 1; then
(P*LG).(len(P*D)+k+1,j)
= P.(LG.(len D + k1+1,j1)) by X71,FUNCT_1:13; then
(P*LG).(len(P*D)+k+1,j) = P.{} by D5,P1;
hence thesis by VALUED_0:def 19;
end;
defpred G[Nat] means
(Partial_Sums_in_cod2(P*LG)).(len(P*D)+i+1,$1) = 0;
(Partial_Sums_in_cod2(P*LG)).(len(P*D)+i+1,0)
= (P*LG).(len(P*D)+i+1,0) by DBLSEQ_3:def 14; then
W16: G[0] by P0;
W17: for j be Nat st G[j] holds G[j+1]
proof
let j be Nat;
assume P2: G[j];
(Partial_Sums_in_cod2(P*LG)).(len(P*D)+i+1,j+1)
= (Partial_Sums_in_cod2(P*LG)).(len(P*D)+i+1,j)
+ (P*LG).(len(P*D)+i+1,j+1) by DBLSEQ_3:def 14
.= (P*LG).(len(P*D)+i+1,j+1) by P2,XXREAL_3:4;
hence G[j+1] by P0;
end;
for j be Nat holds G[j] from NAT_1:sch 2(W16,W17);
hence ProjMap1(Partial_Sums_in_cod2(P*LG),len(P*D)+i+1).s = 0
by W15;
end; then
lim (ProjMap1(Partial_Sums_in_cod2(P*LG),len(P*D)+i+1)) = 0
by MESFUNC5:52; then
(lim_in_cod2(Partial_Sums_in_cod2(P*LG))).(len(P*D)+i+1) = 0
by DBLSEQ_3:def 13;
hence H[i+1] by W13,XXREAL_3:4;
end;
for i be Nat holds H[i] from NAT_1:sch 2(W8,W9); then
H[j]; then
W10: (lim_in_cod2(Partial_Sums_in_cod2(P*LG))).m
<= Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG))).(len(P*D))
by W7,X80,DBLSEQ_3:4;
(lim_in_cod2(Partial_Sums_in_cod2(P*LG))).m > -infty
by X80,SUPINF_2:51; then
(lim_in_cod2(Partial_Sums_in_cod2(P*LG))).m in REAL
by W10,X81,XXREAL_0:14; then
lim ProjMap1(Partial_Sums_in_cod2(P*LG),m) in REAL
by DBLSEQ_3:def 13;
hence ProjMap1(Partial_Sums_in_cod2(P*LG),m)
is convergent_to_finite_number
by W5,MESFUNC5:def 12;
end;
end; then
Partial_Sums (P*LG) is convergent_in_cod2_to_finite
by DBLSEQ_3:def 10,81; then
(Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG)))).(len(P*D))
= lim(ProjMap1(Partial_Sums_in_cod2
(Partial_Sums_in_cod1 (P*LG)),len(P*D))) by DBLSEQ_3:82
.= lim(ProjMap1(Partial_Sums (P*LG),len(P*D))) by DBLSEQ_3:def 16;
hence
(Partial_Sums(lim_in_cod2(Partial_Sums_in_cod2(P*LG)))).(len(P*D))
= (lim_in_cod2(Partial_Sums(P*LG))).(len(P*D)) by DBLSEQ_3:def 13;
end;
end; then
X100:Sum(P*D) <= (lim_in_cod2(Partial_Sums(P*LG))).(len(P*D))
by X74,X72,XXREAL_0:2;
for j be Nat holds
(Partial_Sums_in_cod1(P*LG)).(len(P*D),j) = (P*G).j
proof
let j be Nat;
reconsider j1=j as Element of NAT by ORDINAL1:def 12;
consider k,m be Nat such that
M0: m in dom(s.k) & (Partial_Sums(Length s)).k - len(s.k) + m - 1 = j
& G.j = (s.k).m by Def4;
reconsider k1=k as Element of NAT by ORDINAL1:def 12;
[k1,s.k1] in Z by F9; then
consider k2 be Nat, Sk be disjoint_valued FinSequence of S such that
M1: [k1,s.k1] = [k2,Sk]
& Union Sk = FSets.k2 & (FSets.k2={} implies Sk=<*{}*>);
M2: s.k = Sk & Union Sk = FSets.k & (FSets.k = {} implies Sk=<*{}*>)
by M1,XTUPLE_0:1;
defpred Cj[Nat,object] means $2 = D.$1 /\ G.j;
M3: for k be Nat st k in Seg len D
ex x be Element of S st Cj[k,x]
proof
let k be Nat;
assume
M5: k in Seg len D; then
1 <= k & k <= len D by FINSEQ_1:1; then
consider k1 be Nat such that
M4: k = k1+1 by NAT_1:6;
reconsider kk1=k1 as Element of NAT by ORDINAL1:def 12;
LG.(kk1,j1) = D.k /\ G.j by M4,M5,D5,FINSEQ_1:1;
hence thesis;
end;
consider Cj be FinSequence of S such that
M7: dom Cj = Seg len D
& for k be Nat st k in Seg len D holds Cj[k,Cj.k] from FINSEQ_1:sch 5(M3);
M7a: len Cj = len D by M7,FINSEQ_1:def 3;
now let x,y be object;
assume M61: x <> y;
per cases;
suppose M62: x in dom Cj & y in dom Cj; then
reconsider x1=x, y1=y as Nat;
Cj.x = D.x1 /\ G.j & Cj.y = D.y1 /\ G.j by M7,M62;
hence Cj.x misses Cj.y by M61,PROB_2:def 2,XBOOLE_1:76;
end;
suppose not x in dom Cj or not y in dom Cj; then
Cj.x = {} or Cj.y = {} by FUNCT_1:def 2;
hence Cj.x misses Cj.y by XBOOLE_1:65;
end;
end; then
reconsider Cj as disjoint_valued FinSequence of S by PROB_2:def 2;
now let x be object;
assume x in Union Cj; then
x in union rng Cj by CARD_3:def 4; then
consider V be set such that
M64: x in V & V in rng Cj by TARSKI:def 4;
consider y be object such that
M65: y in dom Cj & V = Cj.y by M64,FUNCT_1:def 3;
reconsider y as Nat by M65;
Cj.y = D.y /\ G.j by M65,M7;
hence x in G.j by M64,M65,XBOOLE_0:def 4;
end; then
M66: Union Cj c= G.j by TARSKI:def 3;
now let x be object;
assume M67a: x in G.j; then
x in Sk.m & Sk.m in rng Sk by M0,M2,FUNCT_1:3; then
x in union rng Sk by TARSKI:def 4; then
M67: x in FSets.k2 by M1,CARD_3:def 4;
dom FSets = NAT by FUNCT_2:def 1; then
FSets.k2 in rng FSets by FUNCT_1:3,ORDINAL1:def 12; then
x in union rng FSets by M67,TARSKI:def 4; then
x in union rng D by B1,B2,CARD_3:def 4; then
consider V be set such that
M68: x in V & V in rng D by TARSKI:def 4;
consider y be object such that
M69: y in dom D & V = D.y by M68,FUNCT_1:def 3;
reconsider y as Nat by M69;
M70: x in D.y /\ G.j by M67a,M68,M69,XBOOLE_0:def 4;
y in Seg len D by M69,FINSEQ_1:def 3; then
M71: x in Cj.y by M7,M70;
y in dom Cj by M69,FINSEQ_1:def 3,M7; then
Cj.y in rng Cj by FUNCT_1:3; then
x in union rng Cj by M71,TARSKI:def 4;
hence x in Union Cj by CARD_3:def 4;
end; then
G.j c= Union Cj by TARSKI:def 3; then
M6: Union Cj = G.j by M66,XBOOLE_0:def 10;
M6b: P.(G.j) = Sum(P*Cj) by M6,Def8;
j in NAT by ORDINAL1:def 12; then
j in dom G by FUNCT_2:def 1; then
M6a: (P*G).j = Sum(P*Cj) by M6b,FUNCT_1:13;
consider SumPCj be sequence of ExtREAL such that
M8: Sum(P*Cj) = SumPCj.(len (P*Cj)) & SumPCj.0 = 0. &
for i be Nat st i < len (P*Cj) holds
SumPCj.(i+1) = SumPCj.i+(P*Cj).(i+1) by EXTREAL1:def 2;
rng Cj c= S; then
rng Cj c= dom P by FUNCT_2:def 1; then
N9: dom(P*Cj) = dom Cj by RELAT_1:27; then
M9: len(P*Cj) = len Cj by FINSEQ_3:29;
M13: for i be Nat st i < len D holds (P*Cj).(i+1) = (P*LG).(i,j)
proof
let i be Nat;
assume i < len D; then
M11: 1<= i+1 & i+1 <= len D by NAT_1:11,13; then
M12: i+1 in Seg len D;
(P*Cj).(i+1) = P.(Cj.(i+1)) by M11,N9,M7a,FINSEQ_3:25,FUNCT_1:12; then
(P*Cj).(i+1) = P.(D.(i+1) /\ G.j) by M7,M12; then
M10: (P*Cj).(i+1) = P.(LG.(i,j)) by M11,D5a;
i in NAT & j in NAT by ORDINAL1:def 12; then
[i,j] in [:NAT,NAT:] by ZFMISC_1:87; then
[i,j] in dom LG by FUNCT_2:def 1;
hence (P*Cj).(i+1) = (P*LG).(i,j) by M10,FUNCT_1:13;
end;
MM15: len(P*D) +1 > len D by X71,NAT_1:13;
len(P*D) in NAT & j in NAT by ORDINAL1:def 12; then
[len(P*D),j] in [:NAT,NAT:] by ZFMISC_1:87; then
[len(P*D),j] in dom LG by FUNCT_2:def 1; then
(P*LG).(len(P*D),j) = P.(LG.(len(P*D),j)) by FUNCT_1:13; then
(P*LG).(len(P*D),j) = P.{} by MM15,D5a; then
M15: (P*LG).(len(P*D),j) = 0 by VALUED_0:def 19;
consider LENDM1 be Nat such that
M23: len D = LENDM1 + 1 by XX70,NAT_1:6;
M24: LENDM1 < len(P*D) by M23,X71,NAT_1:13;
defpred EQ[Nat] means $1 < len(P*D) implies
(Partial_Sums_in_cod1(P*LG)).($1,j) = SumPCj.($1 + 1);
(Partial_Sums_in_cod1(P*LG)).(0,j) = (P*LG).(0,j)
by DBLSEQ_3:def 15; then
M17: (Partial_Sums_in_cod1(P*LG)).(0,j) = (P*Cj).(0+1) by XX70,M13;
SumPCj.(0+1) = 0 + (P*Cj).(0+1) by XX70,M7a,M9,M8; then
M18: EQ[0] by M17,XXREAL_3:4;
M22: for k be Nat st EQ[k] holds EQ[k+1]
proof
let k be Nat;
assume M19: EQ[k];
assume M20: k+1 < len(P*D); then
(Partial_Sums_in_cod1(P*LG)).(k+1,j)
= SumPCj.(k+1) + (P*LG).(k+1,j) by M19,NAT_1:13,DBLSEQ_3:def 15
.= SumPCj.(k+1) + (P*Cj).(k+1+1) by M20,M13,X71;
hence (Partial_Sums_in_cod1(P*LG)).(k+1,j) = SumPCj.(k+1+1)
by M20,M9,M7a,M8,X71;
end;
for k be Nat holds EQ[k] from NAT_1:sch 2(M18,M22); then
(Partial_Sums_in_cod1(P*LG)).(LENDM1,j)
= (P*G).j by M6a,M8,M24,M23,M7a,M9; then
(Partial_Sums_in_cod1(P*LG)).(len(P*D),j)
= (P*G).j + 0 by M15,X71,M23,DBLSEQ_3:def 15;
hence thesis by XXREAL_3:4;
end; then
X120:M.(Union FSets) <= Sum(P*G) by X2,X100,DBLSEQ_3:41;
Partial_Sums (P*G) is non-decreasing by MESFUNC9:16; then
X123:Partial_Sums (P*G) is convergent by RINFSUP2:37;
X124:Partial_Sums(M*FSets) is subsequence of Partial_Sums(P*G)
proof
consider N be increasing sequence of NAT such that
Z0: for k be Nat holds N.k = (Partial_Sums(Length s)).k - 1 by Th11;
defpred P[Nat] means
((Partial_Sums(P*G))*N).$1 = (Partial_Sums(M*FSets)).$1;
[0,s.0] in Z by F9; then
consider n0 be Nat, E0 be disjoint_valued FinSequence of S such that
Z1: [0,s.0] = [n0,E0]
& Union E0 = FSets.n0 & (FSets.n0={} implies E0=<*{}*>);
Z2: n0 = 0 & E0 = s.0 by Z1,XTUPLE_0:1;
Z4: M.(Union E0) = Sum(P*E0) by A1,Z1;
consider SPE0 be sequence of ExtREAL such that
Z5: Sum(P*E0) = SPE0.(len(P*E0)) & SPE0.0 = 0. &
for i be Nat st i < len(P*E0) holds SPE0.(i+1)=SPE0.i + (P*E0).(i+1)
by EXTREAL1:def 2;
rng E0 c= S; then
rng E0 c= dom P by FUNCT_2:def 1; then
ZZ10: dom(P*E0) = dom E0 by RELAT_1:27; then
Z10: len(P*E0) = len E0 by FINSEQ_3:29;
len(s.0) >= 1 by FINSEQ_1:20; then
Z11: len(s.0) in dom(s.0) & 1 in dom(s.0) by FINSEQ_3:25; then
consider N0 be Nat such that
Z6: N0 = (Partial_Sums(Length s)).0 - len(s.0) + len(s.0) - 1
& G.N0 = (s.0).(len(s.0)) by Th13;
Z6d: N0 = N.0 by Z0,Z6;
N0 = (Length s).0 - 1 by Z6,SERIES_1:def 1; then
Z6c: N0+1 = len(s.0) by Def3; then
Z6b: N0 < len(s.0) by NAT_1:13;
defpred P0[Nat] means $1 < len(P*E0) implies
(Partial_Sums(P*G)).$1 = SPE0.($1+1);
consider z0 be Nat such that
Z7: z0 = (Partial_Sums(Length s)).0 - len(s.0) + 1 - 1
& G.z0 = (s.0).1 by Z11,Th13;
z0 = (Length s).0 - len(s.0) by Z7,SERIES_1:def 1; then
Z8: z0 = len(s.0) - len(s.0) by Def3;
Z12: (Partial_Sums(P*G)).0 = (P*G).0 by MESFUNC9:def 1
.= P.((s.0).1) by Z7,Z8,FUNCT_2:15
.= (P*E0).1 by Z11,Z2,FUNCT_1:13;
SPE0.(0+1) = 0+(P*E0).1 by Z5,Z10,Z2; then
ZZ1: P0[0] by Z12,XXREAL_3:4;
ZZ2: for i be Nat st P0[i] holds P0[i+1]
proof
let i be Nat;
assume Z13: P0[i];
assume Z14: i+1 < len(P*E0);
Z16: (Partial_Sums(P*G)).(i+1)
= (Partial_Sums(P*G)).i + (P*G).(i+1) by MESFUNC9:def 1
.= SPE0.(i+1) + P.(G.(i+1)) by Z14,NAT_1:13,Z13,FUNCT_2:15;
Z18: 1 <= i+1+1 & i+1+1 <= len(P*E0) by Z14,NAT_1:11,13; then
consider zi1 be Nat such that
Z17: zi1 = (Partial_Sums(Length s)).0 - len(s.0) + (i+1+1) - 1
& G.zi1 = (s.0).(i+1+1) by Th13,ZZ10,Z2,FINSEQ_3:25;
zi1 = (Length s).0 - len(s.0) + (i+1+1) - 1 by Z17,SERIES_1:def 1
.= len(s.0) - len(s.0) + (i+1+1) - 1 by Def3; then
P.(G.(i+1)) = (P*E0).(i+1+1) by Z17,Z18,ZZ10,Z2,FINSEQ_3:25,FUNCT_1:13;
hence (Partial_Sums(P*G)).(i+1) = SPE0.(i+1+1) by Z14,Z5,Z16;
end;
for i be Nat holds P0[i] from NAT_1:sch 2(ZZ1,ZZ2); then
(Partial_Sums(P*G)).N0 = M.(FSets.0)
by Z6b,Z6c,Z2,Z10,Z5,Z4,Z1; then
(Partial_Sums(P*G)).N0 = (M*FSets).0 by FUNCT_2:15; then
(Partial_Sums(P*G)).N0 = (Partial_Sums(M*FSets)).0
by MESFUNC9:def 1; then
Z100: P[0] by Z6d,FUNCT_2:15;
Z101: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume Z20: P[n];
[n+1,s.(n+1)] in Z by F9; then
consider N1 be Nat, E be disjoint_valued FinSequence of S such that
Z21: [n+1,s.(n+1)] = [N1,E]
& Union E = FSets.N1 & (FSets.N1={} implies E=<*{}*>);
Z22: n+1 = N1 & s.(n+1) = E by Z21,XTUPLE_0:1;
Z24: M.(Union E) = Sum(P*E) by A1,Z21;
consider SPE be sequence of ExtREAL such that
Z25: Sum(P*E) = SPE.(len(P*E)) & SPE.0 = 0. &
for i be Nat st i < len(P*E) holds SPE.(i+1) = SPE.i + (P*E).(i+1)
by EXTREAL1:def 2;
rng E c= S; then
rng E c= dom P by FUNCT_2:def 1; then
ZZ30: dom(P*E) = dom E by RELAT_1:27; then
Z30: len(P*E) = len E by FINSEQ_3:29;
len(s.(n+1)) >= 1 by FINSEQ_1:20; then
Z31: len(s.(n+1)) in dom(s.(n+1)) & 1 in dom(s.(n+1)) by FINSEQ_3:25; then
consider NEnd be Nat such that
Z26: NEnd = (Partial_Sums(Length s)).(n+1) - len(s.(n+1)) + len(s.(n+1))-1
& G.NEnd = (s.(n+1)).(len(s.(n+1))) by Th13;
Z26d: NEnd = N.(n+1) by Z0,Z26;
consider NSt be Nat such that
Z27: NSt = (Partial_Sums(Length s)).(n+1) - len(s.(n+1)) + 1 - 1
& G.NSt = (s.(n+1)).1 by Z31,Th13;
NSt = (Partial_Sums(Length s)).n + (Length s).(n+1) - len(s.(n+1))
by Z27,SERIES_1:def 1; then
Z28: NSt = (Partial_Sums(Length s)).n + len(s.(n+1)) - len(s.(n+1))
by Def3;
Z50: N.n = (Partial_Sums(Length s)).n - 1 by Z0;
defpred PE[Nat] means $1 < len(P*E) implies
(Partial_Sums(P*G)).(N.n + $1 + 1)
= (Partial_Sums(P*G)).(N.n) + SPE.($1 + 1);
Z40: (Partial_Sums(P*G)).(N.n + 1)
= (Partial_Sums(P*G)).(N.n) + (P*G).(N.n + 1) by MESFUNC9:def 1
.= (Partial_Sums(P*G)).(N.n) + P.(G.(N.n + 1)) by FUNCT_2:15
.= (Partial_Sums(P*G)).(N.n) + (P*E).1
by Z31,Z22,Z50,Z28,Z27,FUNCT_1:13;
SPE.(0+1) = SPE.0 + (P*E).(0+1) by Z25,Z30,Z22; then
Z60: PE[0] by Z40,Z25,XXREAL_3:4;
Z61: for j be Nat st PE[j] holds PE[j+1]
proof
let j be Nat;
assume Z52: PE[j];
assume Z53: j+1 < len(P*E); then
Z58a: 1 <= j+1+1 & j+1+1 <= len(P*E) by NAT_1:11,13; then
consider Nj be Nat such that
Z58: Nj = (Partial_Sums(Length s)).(n+1) - len(s.(n+1)) + (j+1+1) - 1
& G.Nj = (s.(n+1)).(j+1+1) by Th13,ZZ30,Z22,FINSEQ_3:25;
Z55: (Partial_Sums(P*G)).(N.n) > -infty by SUPINF_2:51;
Z56: P.(G.(N.n + j+1+1)) > -infty by SUPINF_2:51;
defpred SP[Nat] means $1 <= len(P*E) implies SPE.$1 >=0;
ZZ1: SP[0] by Z25;
ZZ2: for t be Nat st SP[t] holds SP[t+1]
proof
let t be Nat;
assume ZZ3: SP[t];
assume ZZ6: t+1 <= len(P*E); then
ZZ5: SPE.(t+1) = SPE.t + (P*E).(t+1) by Z25,NAT_1:13;
t+1 in dom(P*E) by NAT_1:11,ZZ6,FINSEQ_3:25; then
(P*E).(t+1) = P.(E.(t+1)) by FUNCT_1:12; then
(P*E).(t+1) >= 0 by SUPINF_2:51;
hence thesis by ZZ3,ZZ6,NAT_1:13,ZZ5;
end;
for t be Nat holds SP[t] from NAT_1:sch 2(ZZ1,ZZ2); then
Z57: SPE.(j+1) >=0 by Z53;
(Partial_Sums(P*G)).(N.n + (j+1) + 1)
= (Partial_Sums(P*G)).(N.n + (j+1)) + (P*G).(N.n + (j+1) + 1)
by MESFUNC9:def 1
.= ( (Partial_Sums(P*G)).(N.n) + SPE.(j+1) ) + P.(G.(N.n + j+1+1))
by Z53,Z52,NAT_1:13,FUNCT_2:15
.= (Partial_Sums(P*G)).(N.n) + ( SPE.(j+1) + P.(G.(N.n + j+1+1)) )
by Z55,Z56,Z57,XXREAL_3:29
.= (Partial_Sums(P*G)).(N.n) + ( SPE.(j+1) + (P*E).(j+1+1) )
by Z58a,Z58,Z50,Z28,Z27,Z22,ZZ30,FINSEQ_3:25,FUNCT_1:13;
hence thesis by Z53,Z25;
end;
Z62: for j be Nat holds PE[j] from NAT_1:sch 2(Z60,Z61);
Z59a: N.n + len(P*E)
= (Partial_Sums(Length s)).n - 1 + len(s.(n+1)) by Z0,Z30,Z22
.= (Partial_Sums(Length s)).n - 1 + (Length s).(n+1) by Def3
.= (Partial_Sums(Length s)).n + (Length s).(n+1) - 1
.= N.(n+1) by Z26,Z26d,SERIES_1:def 1;
consider sn1 be Nat such that
Z63: len(P*E) = sn1 + 1 by Z22,Z30,NAT_1:6;
sn1 < len(P*E) by Z63,NAT_1:13; then
TA: (Partial_Sums(P*G)).(N.n + sn1+1)
= (Partial_Sums(P*G)).(N.n) + Sum(P*E) by Z25,Z62,Z63
.= (Partial_Sums(P*G)).(N.n) + (M*FSets).(n+1)
by Z24,Z21,Z22,FUNCT_2:15;
(Partial_Sums(M*FSets)).(n+1)
= ((Partial_Sums(P*G))*N).n + (M*FSets).(n+1) by Z20,MESFUNC9:def 1
.= (Partial_Sums(P*G)).(N.(n+1))
by TA,Z59a,Z63,ORDINAL1:def 12,FUNCT_2:15
.= ((Partial_Sums(P*G))*N).(n+1) by FUNCT_2:15;
hence thesis;
end;
for n be Nat holds P[n] from NAT_1:sch 2(Z100,Z101); then
for n be Element of NAT holds
(Partial_Sums(M*FSets)).n = (Partial_Sums(P*G) * N).n;
hence Partial_Sums(M*FSets) is subsequence of Partial_Sums(P*G)
by FUNCT_2:def 8;
end;
X125:Sum(M*FSets) = Sum(P*G)
proof
per cases by X123,MESFUNC5:def 11,MESFUNC9:8;
suppose L1: Partial_Sums(P*G) is convergent_to_+infty; then
lim Partial_Sums(M*FSets) = +infty by X124,DBLSEQ_3:27; then
lim Partial_Sums(M*FSets) = lim Partial_Sums(P*G) by L1,MESFUNC9:7; then
Sum(M*FSets) = lim Partial_Sums(P*G) by MESFUNC9:def 3;
hence Sum(M*FSets) = Sum(P*G) by MESFUNC9:def 3;
end;
suppose Partial_Sums(P*G) is convergent_to_finite_number; then
lim Partial_Sums(M*FSets) = lim Partial_Sums(P*G)
by X124,DBLSEQ_3:26; then
Sum(M*FSets) = lim Partial_Sums(P*G) by MESFUNC9:def 3;
hence Sum(M*FSets) = Sum(P*G) by MESFUNC9:def 3;
end;
end;
H0: Partial_Sums(M*FSets) is non-decreasing by MESFUNC9:16;
for n be Nat holds Partial_Sums(M*FSets).n <= M.(union rng FSets)
proof
let n be Nat;
H1: union rng(FSets|Segm(n+1)) in Field_generated_by S by Th58;
rng (FSets|Segm(n+1)) c= rng FSets by RELAT_1:70; then
M.(union rng(FSets|Segm(n+1))) <= M.(union rng FSets)
by B0,H1,MEASURE1:8,ZFMISC_1:77;
hence Partial_Sums(M*FSets).n <= M.(union rng FSets) by Th58;
end; then
lim Partial_Sums(M*FSets) <= M.(union rng FSets)
by H0,RINFSUP2:37,MESFUNC9:9; then
Sum(M*FSets) <= M.(union rng FSets) by MESFUNC9:def 3; then
Sum(M*FSets) <= M.(Union FSets) by CARD_3:def 4; then
X126:M.(Union FSets) = Sum(M*FSets) by X125,X120,XXREAL_0:1;
Sum(M*FSets) = SUM(M*FSets) by MEASURE8:2;
hence SUM(M*FSets) = M.(union rng FSets) by X126,CARD_3:def 4;
end;
suppose LL1: rng FSets is empty-membered; then
union rng FSets = {} by Th52; then
L2: M.(union rng FSets) = 0 by VALUED_0:def 19;
LL3: for n be Nat holds (M*FSets).n = 0
proof
let n be Nat;
LL4: dom FSets = NAT by FUNCT_2:def 1; then
FSets.n in rng FSets by FUNCT_1:3,ORDINAL1:def 12; then
FSets.n = {} by LL1; then
(M*FSets).n = M.{} by LL4,ORDINAL1:def 12,FUNCT_1:13;
hence (M*FSets).n = 0 by VALUED_0:def 19;
end;
LL5: dom (Partial_Sums(M*FSets)) = NAT & dom (seq_const 0) = NAT
by FUNCT_2:def 1;
for n be object st n in dom(Partial_Sums(M*FSets)) holds
(Partial_Sums(M*FSets)).n = (seq_const 0).n
proof
let n be object;
assume n in dom(Partial_Sums(M*FSets)); then
reconsider n1 = n as Nat;
defpred P[Nat] means (Partial_Sums(M*FSets)).$1 = 0;
(Partial_Sums(M*FSets)).0 = (M*FSets).0 by MESFUNC9:def 1; then
LL8: P[0] by LL3;
LL9: for i be Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume P[i]; then
(Partial_Sums(M*FSets)).i + (M*FSets).(i+1) = (M*FSets).(i+1)
by XXREAL_3:4; then
(Partial_Sums(M*FSets)).(i+1) = (M*FSets).(i+1) by MESFUNC9:def 1;
hence P[i+1] by LL3;
end;
for i be Nat holds P[i] from NAT_1:sch 2(LL8,LL9); then
(Partial_Sums(M*FSets)).n1 = 0;
hence thesis;
end; then
Partial_Sums(M*FSets) = seq_const 0 by LL5,FUNCT_1:def 11; then
L4: Partial_Sums(M*FSets) is convergent_to_finite_number
& Partial_Sums(M*FSets) is convergent
& lim Partial_Sums(M*FSets) = lim (seq_const 0) by RINFSUP2:14;
SUM(M*FSets) = Sum(M*FSets) by MEASURE8:2;
hence SUM(M*FSets) = M.(union rng FSets) by L2,L4,MESFUNC9:def 3;
end;
end;
hence M is completely-additive by MEASURE8:def 11;
end;
definition
let X be set, S be semialgebra_of_sets of X, P be pre-Measure of S;
mode induced_Measure of S,P -> Measure of Field_generated_by S means :Def9:
for A be set st A in Field_generated_by S holds
for F be disjoint_valued FinSequence of S
st A = Union F holds it.A = Sum(P*F);
existence by Th55;
end;
theorem Th60:
for X be set, S be semialgebra_of_sets of X,
P be pre-Measure of S, M be induced_Measure of S,P holds
M is completely-additive
proof
let X be set, S be semialgebra_of_sets of X,
P be pre-Measure of S, M be induced_Measure of S,P;
for A be set st A in Field_generated_by S holds
for F be disjoint_valued FinSequence of S
st A = Union F holds M.A = Sum(P*F) by Def9;
hence thesis by Th59;
end;
theorem Th61:
for X be non empty set, S be semialgebra_of_sets of X,
P be pre-Measure of S, M be induced_Measure of S,P holds
(sigma_Meas(C_Meas M))|(sigma (Field_generated_by S)) is
sigma_Measure of sigma Field_generated_by S
proof
let X be non empty set, S be semialgebra_of_sets of X,
P be pre-Measure of S, M be induced_Measure of S,P;
M is completely-additive by Th60; then
consider N be sigma_Measure of sigma Field_generated_by S such that
A1: N is_extension_of M
& N = (sigma_Meas(C_Meas M))|(sigma (Field_generated_by S)) by MEASURE8:33;
thus thesis by A1;
end;
definition
let X be non empty set, S be semialgebra_of_sets of X,
P be pre-Measure of S, M be induced_Measure of S,P;
mode induced_sigma_Measure of S,M ->
sigma_Measure of sigma Field_generated_by S means :Def10:
it = (sigma_Meas(C_Meas M))|(sigma (Field_generated_by S));
existence
proof
(sigma_Meas(C_Meas M))|(sigma (Field_generated_by S)) is
sigma_Measure of sigma Field_generated_by S by Th61;
hence thesis;
end;
end;
theorem
for X be non empty set, S be semialgebra_of_sets of X,
P be pre-Measure of S, m be induced_Measure of S,P,
M be induced_sigma_Measure of S,m holds M is_extension_of m
proof
let X be non empty set, S be semialgebra_of_sets of X,
P be pre-Measure of S, m be induced_Measure of S,P,
M be induced_sigma_Measure of S,m;
m is completely-additive by Th60; then
consider N be sigma_Measure of sigma Field_generated_by S such that
A2: N is_extension_of m
& N = (sigma_Meas(C_Meas m))|(sigma (Field_generated_by S)) by MEASURE8:33;
thus M is_extension_of m by A2,Def10;
end;