dblseq_2.miz
begin
reserve Rseq,Rseq1,Rseq2 for
Function of
[:
NAT ,
NAT :],
REAL ;
definition
let f be
Function of
[:
NAT ,
NAT :],
REAL ;
:: original:
nonnegative-yielding
redefine
::
DBLSEQ_2:def1
attr f is
nonnegative-yielding means for i,j be
Nat holds (f
. (i,j))
>=
0 ;
compatibility
proof
thus f is
nonnegative-yielding implies for i,j be
Nat holds (f
. (i,j))
>=
0
proof
assume
A0: f is
nonnegative-yielding;
let i,j be
Nat;
i
in
NAT & j
in
NAT by
ORDINAL1:def 12;
then
[i, j]
in
[:
NAT ,
NAT :] by
ZFMISC_1:def 2;
hence thesis by
A0,
FUNCT_2: 4;
end;
assume
A1: for i,j be
Nat holds (f
. (i,j))
>=
0 ;
let r be
Real;
assume r
in (
rng f);
then
consider x be
Element of
[:
NAT ,
NAT :] such that
A2: r
= (f
. x) by
FUNCT_2: 113;
consider x1,x2 be
object such that
A3: x1
in
NAT & x2
in
NAT & x
=
[x1, x2] by
ZFMISC_1:def 2;
reconsider x1, x2 as
Nat by
A3;
r
= (f
. (x1,x2)) by
A3,
A2;
hence thesis by
A1;
end;
end
theorem ::
DBLSEQ_2:1
Rseq is
non-decreasing implies (for m be
Element of
NAT holds (
ProjMap1 (Rseq,m)) is
non-decreasing) & (for n be
Element of
NAT holds (
ProjMap2 (Rseq,n)) is
non-decreasing)
proof
assume
a1: Rseq is
non-decreasing;
hereby
let m be
Element of
NAT ;
now
let n1,n2 be
Nat;
a0: n1
in
NAT & n2
in
NAT by
ORDINAL1:def 12;
assume n1
<= n2;
then (Rseq
. (m,n1))
<= (Rseq
. (m,n2)) by
a1;
then ((
ProjMap1 (Rseq,m))
. n1)
<= (Rseq
. (m,n2)) by
a0,
MESFUNC9:def 6;
hence ((
ProjMap1 (Rseq,m))
. n1)
<= ((
ProjMap1 (Rseq,m))
. n2) by
a0,
MESFUNC9:def 6;
end;
hence (
ProjMap1 (Rseq,m)) is
non-decreasing by
SEQM_3: 6;
end;
hereby
let m be
Element of
NAT ;
now
let n1,n2 be
Nat;
a2: n1
in
NAT & n2
in
NAT by
ORDINAL1:def 12;
assume n1
<= n2;
then (Rseq
. (n1,m))
<= (Rseq
. (n2,m)) by
a1;
then ((
ProjMap2 (Rseq,m))
. n1)
<= (Rseq
. (n2,m)) by
a2,
MESFUNC9:def 7;
hence ((
ProjMap2 (Rseq,m))
. n1)
<= ((
ProjMap2 (Rseq,m))
. n2) by
a2,
MESFUNC9:def 7;
end;
hence (
ProjMap2 (Rseq,m)) is
non-decreasing by
SEQM_3: 6;
end;
end;
theorem ::
DBLSEQ_2:2
Rseq is
non-decreasing & Rseq is
convergent_in_cod1 implies (
lim_in_cod1 Rseq) is
non-decreasing
proof
assume that
a1: Rseq is
non-decreasing and
a2: Rseq is
convergent_in_cod1;
now
let i,j be
Nat;
assume
a4: i
<= j;
reconsider n1 = i, n2 = j as
Element of
NAT by
ORDINAL1:def 12;
a5: (
ProjMap2 (Rseq,n1)) is
convergent & (
ProjMap2 (Rseq,n2)) is
convergent by
a2;
now
let m be
Nat;
m
in
NAT by
ORDINAL1:def 12;
then ((
ProjMap2 (Rseq,n1))
. m)
= (Rseq
. (m,n1)) & ((
ProjMap2 (Rseq,n2))
. m)
= (Rseq
. (m,n2)) by
MESFUNC9:def 7;
hence ((
ProjMap2 (Rseq,n1))
. m)
<= ((
ProjMap2 (Rseq,n2))
. m) by
a1,
a4;
end;
then (
lim (
ProjMap2 (Rseq,n1)))
<= (
lim (
ProjMap2 (Rseq,n2))) by
a5,
SEQ_2: 18;
then ((
lim_in_cod1 Rseq)
. n1)
<= (
lim (
ProjMap2 (Rseq,n2))) by
DBLSEQ_1:def 5;
hence ((
lim_in_cod1 Rseq)
. i)
<= ((
lim_in_cod1 Rseq)
. j) by
DBLSEQ_1:def 5;
end;
hence (
lim_in_cod1 Rseq) is
non-decreasing by
SEQM_3: 6;
end;
theorem ::
DBLSEQ_2:3
Rseq is
non-decreasing & Rseq is
convergent_in_cod2 implies (
lim_in_cod2 Rseq) is
non-decreasing
proof
assume that
a1: Rseq is
non-decreasing and
a2: Rseq is
convergent_in_cod2;
now
let i,j be
Nat;
assume
a4: i
<= j;
reconsider m1 = i, m2 = j as
Element of
NAT by
ORDINAL1:def 12;
p1: (
ProjMap1 (Rseq,m1)) is
convergent & (
ProjMap1 (Rseq,m2)) is
convergent by
a2;
now
let n be
Nat;
n
in
NAT by
ORDINAL1:def 12;
then ((
ProjMap1 (Rseq,m1))
. n)
= (Rseq
. (m1,n)) & ((
ProjMap1 (Rseq,m2))
. n)
= (Rseq
. (m2,n)) by
MESFUNC9:def 6;
hence ((
ProjMap1 (Rseq,m1))
. n)
<= ((
ProjMap1 (Rseq,m2))
. n) by
a1,
a4;
end;
then (
lim (
ProjMap1 (Rseq,m1)))
<= (
lim (
ProjMap1 (Rseq,m2))) by
p1,
SEQ_2: 18;
then ((
lim_in_cod2 Rseq)
. m1)
<= (
lim (
ProjMap1 (Rseq,m2))) by
DBLSEQ_1:def 6;
hence ((
lim_in_cod2 Rseq)
. i)
<= ((
lim_in_cod2 Rseq)
. j) by
DBLSEQ_1:def 6;
end;
hence (
lim_in_cod2 Rseq) is
non-decreasing by
SEQM_3: 6;
end;
theorem ::
DBLSEQ_2:4
Rseq is
non-decreasing & Rseq is
P-convergent implies (for n,m be
Nat holds (Rseq
. (n,m))
<= (
P-lim Rseq))
proof
assume
a1: Rseq is
non-decreasing & Rseq is
P-convergent;
hereby
let n,m be
Nat;
reconsider n1 = n, m1 = m as
Element of
NAT by
ORDINAL1:def 12;
(Rseq
. (n,m)) is
Element of
REAL by
XREAL_0:def 1;
then
reconsider Rseq1 = (
[:
NAT ,
NAT :]
--> (Rseq
. (n,m))) as
Function of
[:
NAT ,
NAT :],
REAL by
FUNCOP_1: 46;
deffunc
F2(
Element of
NAT ,
Element of
NAT ) = (Rseq
. ((n
+ $1),(m
+ $2)));
consider Rseq2 be
Function of
[:
NAT ,
NAT :],
REAL such that
a4: for i be
Element of
NAT holds for j be
Element of
NAT holds (Rseq2
. (i,j))
=
F2(i,j) from
BINOP_1:sch 4;
a5:
now
let i,j be
Nat;
a6: (n
+ i)
>= n & (m
+ j)
>= m by
NAT_1: 11;
i
in
NAT & j
in
NAT by
ORDINAL1:def 12;
then (Rseq1
. (i,j))
= (Rseq
. (n,m)) & (Rseq2
. (i,j))
= (Rseq
. ((n
+ i),(m
+ j))) by
a4,
FUNCOP_1: 70;
hence (Rseq1
. (i,j))
<= (Rseq2
. (i,j)) by
a1,
a6;
end;
reconsider r = (Rseq
. (n,m)) as
Element of
REAL by
XREAL_0:def 1;
Rseq1
= (
[:
NAT ,
NAT :]
--> r);
then
a7: Rseq1 is
P-convergent & (
P-lim Rseq1)
= (Rseq
. (n,m)) by
DBLSEQ_1: 2;
deffunc
N(
Element of
NAT ) = (n
+ $1);
consider N be
Function of
NAT ,
NAT such that
b1: for i be
Element of
NAT holds (N
. i)
=
N(i) from
FUNCT_2:sch 4;
now
let k be
Nat;
k is
Element of
NAT by
ORDINAL1:def 12;
then
b2: (N
. k)
= (n
+ k) & (N
. (k
+ 1))
= (n
+ (k
+ 1)) by
b1;
k
< (k
+ 1) by
NAT_1: 13;
hence (N
. k)
< (N
. (k
+ 1)) by
b2,
XREAL_1: 6;
end;
then
reconsider N as
increasing
sequence of
NAT by
VALUED_1:def 13;
deffunc
M(
Element of
NAT ) = (m
+ $1);
consider M be
Function of
NAT ,
NAT such that
c1: for j be
Element of
NAT holds (M
. j)
=
M(j) from
FUNCT_2:sch 4;
now
let k be
Nat;
k is
Element of
NAT by
ORDINAL1:def 12;
then
c2: (M
. k)
= (m
+ k) & (M
. (k
+ 1))
= (m
+ (k
+ 1)) by
c1;
k
< (k
+ 1) by
NAT_1: 13;
hence (M
. k)
< (M
. (k
+ 1)) by
c2,
XREAL_1: 6;
end;
then
reconsider M as
increasing
sequence of
NAT by
VALUED_1:def 13;
for i,j be
Nat holds (Rseq2
. (i,j))
= (Rseq
. ((N
. i),(M
. j)))
proof
let i,j be
Nat;
c5: i
in
NAT & j
in
NAT by
ORDINAL1:def 12;
then (N
. i)
= (n
+ i) & (M
. j)
= (m
+ j) by
b1,
c1;
hence (Rseq2
. (i,j))
= (Rseq
. ((N
. i),(M
. j))) by
c5,
a4;
end;
then Rseq2 is
subsequence of Rseq by
DBLSEQ_1:def 14;
then Rseq2 is
P-convergent & (
P-lim Rseq2)
= (
P-lim Rseq) by
a1,
DBLSEQ_1: 17;
hence (Rseq
. (n,m))
<= (
P-lim Rseq) by
a5,
a7,
DBLSEQ_1: 15;
end;
end;
theorem ::
DBLSEQ_2:5
lmADD: (
dom (Rseq1
+ Rseq2))
=
[:
NAT ,
NAT :] & (
dom (Rseq1
- Rseq2))
=
[:
NAT ,
NAT :] & (for n,m be
Nat holds ((Rseq1
+ Rseq2)
. (n,m))
= ((Rseq1
. (n,m))
+ (Rseq2
. (n,m)))) & (for n,m be
Nat holds ((Rseq1
- Rseq2)
. (n,m))
= ((Rseq1
. (n,m))
- (Rseq2
. (n,m))))
proof
thus
A1: (
dom (Rseq1
+ Rseq2))
=
[:
NAT ,
NAT :] & (
dom (Rseq1
- Rseq2))
=
[:
NAT ,
NAT :] by
FUNCT_2:def 1;
hereby
let n,m be
Nat;
n
in
NAT & m
in
NAT by
ORDINAL1:def 12;
hence ((Rseq1
+ Rseq2)
. (n,m))
= ((Rseq1
. (n,m))
+ (Rseq2
. (n,m))) by
A1,
VALUED_1:def 1,
ZFMISC_1: 87;
end;
hereby
let n,m be
Nat;
n
in
NAT & m
in
NAT by
ORDINAL1:def 12;
hence ((Rseq1
- Rseq2)
. (n,m))
= ((Rseq1
. (n,m))
- (Rseq2
. (n,m))) by
A1,
VALUED_1: 13,
ZFMISC_1: 87;
end;
end;
theorem ::
DBLSEQ_2:6
for C,D,E be non
empty
set, f be
Function of
[:C, D:], E holds ex g be
Function of
[:D, C:], E st for d be
Element of D, c be
Element of C holds (g
. (d,c))
= (f
. (c,d))
proof
let C,D,E be non
empty
set;
let f be
Function of
[:C, D:], E;
deffunc
F(
Element of D,
Element of C) = (f
. ($2,$1));
consider IT be
Function of
[:D, C:], E such that
A1: for d be
Element of D, c be
Element of C holds (IT
. (d,c))
=
F(d,c) from
STACKS_1:sch 2;
take IT;
thus thesis by
A1;
end;
theorem ::
DBLSEQ_2:7
for C,D,E be
set, f be
Function of
[:C, D:], E holds f
= (
~ (
~ f)) by
FUNCT_4: 53;
scheme ::
DBLSEQ_2:sch1
RecEx2D1 { C() -> non
empty
set , D() -> non
empty
set , H() ->
Function of C(), D() , F(
set,
set,
Nat) ->
Element of D() } :
ex g be
Function of
[:C(),
NAT :], D() st for a be
Element of C() holds (g
. (a,
0 ))
= (H()
. a) & for n be
Nat holds (g
. (a,(n
+ 1)))
= F(.,a,n);
a1: for a be
Element of C() holds ex f be
Function of
NAT , D() st (f
.
0 )
= (H()
. a) & for n be
Nat holds (f
. (n
+ 1))
= F(.,a,n)
proof
let a be
Element of C();
defpred
P1[
Nat,
Element of D(),
Element of D()] means $3
= F($2,a,$1);
a2: for n be
Nat, x be
Element of D() holds ex y be
Element of D() st
P1[n, x, y];
thus ex f be
Function of
NAT , D() st (f
.
0 )
= (H()
. a) & for n be
Nat holds
P1[n, (f
. n), (f
. (n
+ 1))] from
RECDEF_1:sch 2(
a2);
end;
ex g be
Function of C(), (
Funcs (
NAT ,D())) st for a be
Element of C() holds ex f be
Function of
NAT , D() st (g
. a)
= f & (f
.
0 )
= (H()
. a) & for n be
Nat holds (f
. (n
+ 1))
= F(.,a,n)
proof
set h1 = {
[a, l] where a be
Element of C(), l be
Element of (
Funcs (
NAT ,D())) : ex f be
Function of
NAT , D() st f
= l & (f
.
0 )
= (H()
. a) & for n be
Nat holds (f
. (n
+ 1))
= F(.,a,n) };
a3:
now
let x,y1,y2 be
object;
assume
a4:
[x, y1]
in h1 &
[x, y2]
in h1;
then
consider a1 be
Element of C(), l1 be
Element of (
Funcs (
NAT ,D())) such that
a5:
[x, y1]
=
[a1, l1] & ex f be
Function of
NAT , D() st f
= l1 & (f
.
0 )
= (H()
. a1) & for n be
Nat holds (f
. (n
+ 1))
= F(.,a1,n);
consider a2 be
Element of C(), l2 be
Element of (
Funcs (
NAT ,D())) such that
a6:
[x, y2]
=
[a2, l2] & ex f be
Function of
NAT , D() st f
= l2 & (f
.
0 )
= (H()
. a2) & for n be
Nat holds (f
. (n
+ 1))
= F(.,a2,n) by
a4;
consider f1 be
Function of
NAT , D() such that
a7: f1
= l1 & (f1
.
0 )
= (H()
. a1) & for n be
Nat holds (f1
. (n
+ 1))
= F(.,a1,n) by
a5;
consider f2 be
Function of
NAT , D() such that
a8: f2
= l2 & (f2
.
0 )
= (H()
. a2) & for n be
Nat holds (f2
. (n
+ 1))
= F(.,a2,n) by
a6;
a9: a1
= x & y1
= l1 & a2
= x & y2
= l2 by
a5,
a6,
XTUPLE_0: 1;
now
let x be
Element of
NAT ;
defpred
P2[
Nat] means (f1
. $1)
= (f2
. $1);
a11:
P2[
0 ] by
a7,
a8,
a9;
a12:
now
let n be
Nat;
assume
P2[n];
then F(.,a2,n)
= (f2
. (n
+ 1)) by
a8;
hence
P2[(n
+ 1)] by
a7,
a9;
end;
for n be
Nat holds
P2[n] from
NAT_1:sch 2(
a11,
a12);
hence (f1
. x)
= (f2
. x);
end;
hence y1
= y2 by
a7,
a8,
a9,
FUNCT_2: 63;
end;
now
let x be
object;
assume x
in h1;
then ex a be
Element of C(), l be
Element of (
Funcs (
NAT ,D())) st x
=
[a, l] & ex f be
Function of
NAT , D() st f
= l & (f
.
0 )
= (H()
. a) & for n be
Nat holds (f
. (n
+ 1))
= F(.,a,n);
hence x
in
[:C(), (
Funcs (
NAT ,D())):] by
ZFMISC_1:def 2;
end;
then
reconsider h1 as
Relation of C(), (
Funcs (
NAT ,D())) by
TARSKI:def 3;
for x be
object holds x
in C() implies x
in (
dom h1)
proof
let x be
object;
assume x
in C();
then
reconsider x1 = x as
Element of C();
consider f be
Function of
NAT , D() such that
a15: (f
.
0 )
= (H()
. x) & for n be
Nat holds (f
. (n
+ 1))
= F(.,x1,n) by
a1;
reconsider f as
Element of (
Funcs (
NAT ,D())) by
FUNCT_2: 8;
[x, f]
in h1 by
a15;
hence thesis by
XTUPLE_0:def 12;
end;
then C()
c= (
dom h1);
then (
dom h1)
= C() by
XBOOLE_0:def 10;
then
reconsider h1 as
Function of C(), (
Funcs (
NAT ,D())) by
a3,
FUNCT_1:def 1,
FUNCT_2:def 1;
take h1;
thus for a be
Element of C() holds ex f be
Function of
NAT , D() st (h1
. a)
= f & (f
.
0 )
= (H()
. a) & for n be
Nat holds (f
. (n
+ 1))
= F(.,a,n)
proof
let a be
Element of C();
(
dom h1)
= C() by
FUNCT_2:def 1;
then
[a, (h1
. a)]
in h1 by
FUNCT_1: 1;
then
consider x be
Element of C(), l be
Element of (
Funcs (
NAT ,D())) such that
a16:
[a, (h1
. a)]
=
[x, l] & ex h be
Function of
NAT , D() st h
= l & (h
.
0 )
= (H()
. x) & for n be
Nat holds (h
. (n
+ 1))
= F(.,x,n);
a
= x & (h1
. a)
= l by
a16,
XTUPLE_0: 1;
hence thesis by
a16;
end;
end;
then
consider g be
Function of C(), (
Funcs (
NAT ,D())) such that
a17: for a be
Element of C() holds ex f be
Function of
NAT , D() st (g
. a)
= f & (f
.
0 )
= (H()
. a) & for n be
Nat holds (f
. (n
+ 1))
= F(.,a,n);
set h1 = {
[
[a, n], z] where n be
Element of
NAT , a be
Element of C(), z be
Element of D() : ex f be
Function of
NAT , D() st f
= (g
. a) & z
= (f
. n) };
a18:
now
let x,y1,y2 be
object;
assume
a19:
[x, y1]
in h1 &
[x, y2]
in h1;
then
consider n1 be
Element of
NAT , a1 be
Element of C(), z1 be
Element of D() such that
a20:
[x, y1]
=
[
[a1, n1], z1] & ex f1 be
Function of
NAT , D() st f1
= (g
. a1) & z1
= (f1
. n1);
consider n2 be
Element of
NAT , a2 be
Element of C(), z2 be
Element of D() such that
a21:
[x, y2]
=
[
[a2, n2], z2] & ex f2 be
Function of
NAT , D() st f2
= (g
. a2) & z2
= (f2
. n2) by
a19;
x
=
[a1, n1] & x
=
[a2, n2] by
a20,
a21,
XTUPLE_0: 1;
then a1
= a2 & n1
= n2 by
XTUPLE_0: 1;
hence y1
= y2 by
a20,
a21,
XTUPLE_0: 1;
end;
now
let x be
object;
assume x
in h1;
then
consider n1 be
Element of
NAT , a1 be
Element of C(), z1 be
Element of D() such that
a22: x
=
[
[a1, n1], z1] and ex f1 be
Function of
NAT , D() st f1
= (g
. a1) & z1
= (f1
. n1);
[a1, n1]
in
[:C(),
NAT :] by
ZFMISC_1:def 2;
hence x
in
[:
[:C(),
NAT :], D():] by
a22,
ZFMISC_1:def 2;
end;
then
reconsider h1 as
Relation of
[:C(),
NAT :], D() by
TARSKI:def 3;
for x be
object holds x
in
[:C(),
NAT :] implies x
in (
dom h1)
proof
let x be
object;
assume x
in
[:C(),
NAT :];
then
consider d,n be
object such that
a24: d
in C() & n
in
NAT & x
=
[d, n] by
ZFMISC_1:def 2;
reconsider d as
Element of C() by
a24;
reconsider n as
Element of
NAT by
a24;
consider h be
Function of
NAT , D() such that
a25: (g
. d)
= h and (h
.
0 )
= (H()
. d) & for n be
Nat holds (h
. (n
+ 1))
= F(.,d,n) by
a17;
(h
. n) is
Element of D();
then
consider z be
Element of D() such that
a26: ex f be
Function of
NAT , D() st f
= (g
. d) & z
= (f
. n) by
a25;
[x, z]
in h1 by
a24,
a26;
hence thesis by
XTUPLE_0:def 12;
end;
then
d2:
[:C(),
NAT :]
c= (
dom h1);
then (
dom h1)
=
[:C(),
NAT :] by
XBOOLE_0:def 10;
then
reconsider h1 as
Function of
[:C(),
NAT :], D() by
a18,
FUNCT_1:def 1,
FUNCT_2:def 1;
take h1;
thus for a be
Element of C() holds (h1
. (a,
0 ))
= (H()
. a) & for n be
Nat holds (h1
. (a,(n
+ 1)))
= F(.,a,n)
proof
let a be
Element of C();
consider h be
Function of
NAT , D() such that
a27: (g
. a)
= h & (h
.
0 )
= (H()
. a) & for n be
Nat holds (h
. (n
+ 1))
= F(.,a,n) by
a17;
a28:
now
let k be
Nat;
[a, (k
+ 1)]
in
[:C(),
NAT :] by
ZFMISC_1:def 2;
then
[a, (k
+ 1)]
in (
dom h1) by
FUNCT_2:def 1;
then
consider u be
object such that
a29:
[
[a, (k
+ 1)], u]
in h1 by
XTUPLE_0:def 12;
k
in
NAT by
ORDINAL1:def 12;
then
[a, k]
in
[:C(),
NAT :] by
ZFMISC_1:def 2;
then
[a, k]
in (
dom h1) by
FUNCT_2:def 1;
then
consider v be
object such that
a30:
[
[a, k], v]
in h1 by
XTUPLE_0:def 12;
consider n1 be
Element of
NAT , d1 be
Element of C(), z1 be
Element of D() such that
a31:
[
[a, k], v]
=
[
[d1, n1], z1] & ex f2 be
Function of
NAT , D() st f2
= (g
. d1) & z1
= (f2
. n1) by
a30;
consider f2 be
Function of
NAT , D() such that
a32: f2
= (g
. d1) & z1
= (f2
. n1) by
a31;
consider n be
Element of
NAT , d be
Element of C(), z be
Element of D() such that
a33:
[
[a, (k
+ 1)], u]
=
[
[d, n], z] & ex f1 be
Function of
NAT , D() st f1
= (g
. d) & z
= (f1
. n) by
a29;
[a, k]
=
[d1, n1] &
[a, (k
+ 1)]
=
[d, n] by
a31,
a33,
XTUPLE_0: 1;
then
a34: a
= d1 & k
= n1 & a
= d & (k
+ 1)
= n by
XTUPLE_0: 1;
hence (h1
. (a,(k
+ 1)))
= (h
. n) by
a27,
a29,
a33,
FUNCT_1: 1
.= F(.,a,n1) by
a27,
a32,
a34
.= F(.,a,k) by
a30,
a32,
a31,
a34,
FUNCT_1: 1;
end;
[a,
0 ]
in
[:C(),
NAT :] by
ZFMISC_1:def 2;
then
consider u be
object such that
a36:
[
[a,
0 ], u]
in h1 by
d2,
XTUPLE_0:def 12;
consider n be
Element of
NAT , d be
Element of C(), z be
Element of D() such that
a37:
[
[a,
0 ], u]
=
[
[d, n], z] & ex f1 be
Function of
NAT , D() st f1
= (g
. d) & z
= (f1
. n) by
a36;
[a,
0 ]
=
[d, n] & u
= z by
a37,
XTUPLE_0: 1;
then a
= d &
0
= n by
XTUPLE_0: 1;
hence thesis by
a27,
a28,
a36,
a37,
FUNCT_1: 1;
end;
end;
scheme ::
DBLSEQ_2:sch2
RecEx2D1R { C() -> non
empty
set , H() ->
Function of C(),
REAL , F(
set,
set,
Nat) ->
real
number } :
ex g be
Function of
[:C(),
NAT :],
REAL st for a be
Element of C() holds (g
. (a,
0 ))
= (H()
. a) & for n be
natural
number holds (g
. (a,(n
+ 1)))
= F(.,a,n);
defpred
P[
set,
set] means ex f be
Function of
NAT ,
REAL st $2
= f & (f
.
0 )
= (H()
. $1) & for n be
Nat holds (f
. (n
+ 1))
= F(.,$1,n);
c1: for a be
Element of C() holds ex f be
Element of (
Funcs (
NAT ,
REAL )) st
P[a, f]
proof
let a be
Element of C();
defpred
P1[
Nat,
set,
set] means $3
= F($2,a,$1);
c2: for n be
Nat holds for x be
Element of
REAL holds ex y be
Element of
REAL st
P1[n, x, y]
proof
let n be
Nat;
let x be
Element of
REAL ;
reconsider y = F(x,a,n) as
Element of
REAL by
XREAL_0:def 1;
take y;
thus thesis;
end;
reconsider A = (H()
. a) as
Element of
REAL ;
consider f be
Function of
NAT ,
REAL such that
c3: (f
.
0 )
= A & for n be
Nat holds
P1[n, (f
. n), (f
. (n
+ 1))] from
RECDEF_1:sch 2(
c2);
reconsider f as
Element of (
Funcs (
NAT ,
REAL )) by
FUNCT_2: 8;
take f;
thus thesis by
c3;
end;
consider g be
Function of C(), (
Funcs (
NAT ,
REAL )) such that
a17: for a be
Element of C() holds
P[a, (g
. a)] from
FUNCT_2:sch 3(
c1);
set h1 = {
[
[a, n], z] where n be
Element of
NAT , a be
Element of C(), z be
Element of
REAL : ex f be
Function of
NAT ,
REAL st f
= (g
. a) & z
= (f
. n) };
a18:
now
let x,y1,y2 be
object;
assume
a19:
[x, y1]
in h1 &
[x, y2]
in h1;
then
consider n1 be
Element of
NAT , a1 be
Element of C(), z1 be
Element of
REAL such that
a20:
[x, y1]
=
[
[a1, n1], z1] & ex f1 be
Function of
NAT ,
REAL st f1
= (g
. a1) & z1
= (f1
. n1);
consider n2 be
Element of
NAT , a2 be
Element of C(), z2 be
Element of
REAL such that
a21:
[x, y2]
=
[
[a2, n2], z2] & ex f2 be
Function of
NAT ,
REAL st f2
= (g
. a2) & z2
= (f2
. n2) by
a19;
x
=
[a1, n1] & x
=
[a2, n2] by
a20,
a21,
XTUPLE_0: 1;
then a1
= a2 & n1
= n2 by
XTUPLE_0: 1;
hence y1
= y2 by
a20,
a21,
XTUPLE_0: 1;
end;
now
let x be
object;
assume x
in h1;
then
consider n1 be
Element of
NAT , a1 be
Element of C(), z1 be
Element of
REAL such that
a22: x
=
[
[a1, n1], z1] and ex f1 be
Function of
NAT ,
REAL st f1
= (g
. a1) & z1
= (f1
. n1);
[a1, n1]
in
[:C(),
NAT :] by
ZFMISC_1:def 2;
hence x
in
[:
[:C(),
NAT :],
REAL :] by
a22,
ZFMISC_1:def 2;
end;
then
reconsider h1 as
Relation of
[:C(),
NAT :],
REAL by
TARSKI:def 3;
for x be
object holds x
in
[:C(),
NAT :] implies x
in (
dom h1)
proof
let x be
object;
assume x
in
[:C(),
NAT :];
then
consider d,n be
object such that
a24: d
in C() & n
in
NAT & x
=
[d, n] by
ZFMISC_1:def 2;
reconsider d as
Element of C() by
a24;
reconsider n as
Element of
NAT by
a24;
consider h be
Function of
NAT ,
REAL such that
a25: (g
. d)
= h and (h
.
0 )
= (H()
. d) and for n be
Nat holds (h
. (n
+ 1))
= F(.,d,n) by
a17;
(h
. n) is
Element of
REAL ;
then
consider z be
Element of
REAL such that
a26: ex f be
Function of
NAT ,
REAL st f
= (g
. d) & z
= (f
. n) by
a25;
[x, z]
in h1 by
a24,
a26;
hence thesis by
XTUPLE_0:def 12;
end;
then
d2:
[:C(),
NAT :]
c= (
dom h1);
then (
dom h1)
=
[:C(),
NAT :] by
XBOOLE_0:def 10;
then
reconsider h1 as
Function of
[:C(),
NAT :],
REAL by
a18,
FUNCT_1:def 1,
FUNCT_2:def 1;
take h1;
thus for a be
Element of C() holds (h1
. (a,
0 ))
= (H()
. a) & for n be
Nat holds (h1
. (a,(n
+ 1)))
= F(.,a,n)
proof
let a be
Element of C();
consider h be
Function of
NAT ,
REAL such that
a27: (g
. a)
= h & (h
.
0 )
= (H()
. a) & for n be
Nat holds (h
. (n
+ 1))
= F(.,a,n) by
a17;
a28:
now
let k be
Nat;
[a, (k
+ 1)]
in
[:C(),
NAT :] by
ZFMISC_1:def 2;
then
[a, (k
+ 1)]
in (
dom h1) by
FUNCT_2:def 1;
then
consider u be
object such that
a29:
[
[a, (k
+ 1)], u]
in h1 by
XTUPLE_0:def 12;
k
in
NAT by
ORDINAL1:def 12;
then
[a, k]
in
[:C(),
NAT :] by
ZFMISC_1:def 2;
then
[a, k]
in (
dom h1) by
FUNCT_2:def 1;
then
consider v be
object such that
a30:
[
[a, k], v]
in h1 by
XTUPLE_0:def 12;
consider n1 be
Element of
NAT , d1 be
Element of C(), z1 be
Element of
REAL such that
a31:
[
[a, k], v]
=
[
[d1, n1], z1] & ex f2 be
Function of
NAT ,
REAL st f2
= (g
. d1) & z1
= (f2
. n1) by
a30;
consider f2 be
Function of
NAT ,
REAL such that
a32: f2
= (g
. d1) & z1
= (f2
. n1) by
a31;
consider n be
Element of
NAT , d be
Element of C(), z be
Element of
REAL such that
a33:
[
[a, (k
+ 1)], u]
=
[
[d, n], z] & ex f1 be
Function of
NAT ,
REAL st f1
= (g
. d) & z
= (f1
. n) by
a29;
[a, k]
=
[d1, n1] &
[a, (k
+ 1)]
=
[d, n] by
a31,
a33,
XTUPLE_0: 1;
then
a34: a
= d1 & k
= n1 & a
= d & (k
+ 1)
= n by
XTUPLE_0: 1;
hence (h1
. (a,(k
+ 1)))
= (h
. n) by
a27,
a29,
a33,
FUNCT_1: 1
.= F(.,a,n1) by
a27,
a32,
a34
.= F(.,a,k) by
a30,
a32,
a31,
a34,
FUNCT_1: 1;
end;
[a,
0 ]
in
[:C(),
NAT :] by
ZFMISC_1:def 2;
then
consider u be
object such that
a36:
[
[a,
0 ], u]
in h1 by
d2,
XTUPLE_0:def 12;
consider n be
Element of
NAT , d be
Element of C(), z be
Element of
REAL such that
a37:
[
[a,
0 ], u]
=
[
[d, n], z] & ex f1 be
Function of
NAT ,
REAL st f1
= (g
. d) & z
= (f1
. n) by
a36;
[a,
0 ]
=
[d, n] & u
= z by
a37,
XTUPLE_0: 1;
then a
= d &
0
= n by
XTUPLE_0: 1;
hence thesis by
a27,
a28,
a36,
a37,
FUNCT_1: 1;
end;
end;
scheme ::
DBLSEQ_2:sch3
RecEx2D2 { C() -> non
empty
set , D() -> non
empty
set , H() ->
Function of C(), D() , F(
set,
set,
Nat) ->
Element of D() } :
ex g be
Function of
[:
NAT , C():], D() st for a be
Element of C() holds (g
. (
0 ,a))
= (H()
. a) & for n be
Nat holds (g
. ((n
+ 1),a))
= F(.,a,n);
consider h be
Function of
[:C(),
NAT :], D() such that
a1: for a be
Element of C() holds (h
. (a,
0 ))
= (H()
. a) & for n be
Nat holds (h
. (a,(n
+ 1)))
= F(.,a,n) from
RecEx2D1;
take g = (
~ h);
hereby
let a be
Element of C();
thus (g
. (
0 ,a))
= (h
. (a,
0 )) by
FUNCT_4:def 8
.= (H()
. a) by
a1;
thus for n be
Nat holds (g
. ((n
+ 1),a))
= F(.,a,n)
proof
let n be
Nat;
a2: n
in
NAT by
ORDINAL1:def 12;
(g
. ((n
+ 1),a))
= (h
. (a,(n
+ 1))) by
FUNCT_4:def 8;
then (g
. ((n
+ 1),a))
= F(.,a,n) by
a1;
hence (g
. ((n
+ 1),a))
= F(.,a,n) by
a2,
FUNCT_4:def 8;
end;
end;
end;
scheme ::
DBLSEQ_2:sch4
RecEx2D2R { C() -> non
empty
set , H() ->
Function of C(),
REAL , F(
set,
set,
Nat) ->
real
number } :
ex g be
Function of
[:
NAT , C():],
REAL st for a be
Element of C() holds (g
. (
0 ,a))
= (H()
. a) & for n be
Nat holds (g
. ((n
+ 1),a))
= F(.,a,n);
consider h be
Function of
[:C(),
NAT :],
REAL such that
a1: for a be
Element of C() holds (h
. (a,
0 ))
= (H()
. a) & for n be
Nat holds (h
. (a,(n
+ 1)))
= F(.,a,n) from
RecEx2D1R;
take g = (
~ h);
hereby
let a be
Element of C();
thus (g
. (
0 ,a))
= (h
. (a,
0 )) by
FUNCT_4:def 8
.= (H()
. a) by
a1;
thus for n be
Nat holds (g
. ((n
+ 1),a))
= F(.,a,n)
proof
let n be
Nat;
a2: n
in
NAT by
ORDINAL1:def 12;
(g
. ((n
+ 1),a))
= (h
. (a,(n
+ 1))) by
FUNCT_4:def 8;
then (g
. ((n
+ 1),a))
= F(.,a,n) by
a1;
hence (g
. ((n
+ 1),a))
= F(.,a,n) by
a2,
FUNCT_4:def 8;
end;
end;
end;
definition
let Rseq be
Function of
[:
NAT ,
NAT :],
REAL ;
::
DBLSEQ_2:def2
func
Partial_Sums_in_cod2 (Rseq) ->
Function of
[:
NAT ,
NAT :],
REAL means
:
DefCS: for n,m be
Nat holds (it
. (n,
0 ))
= (Rseq
. (n,
0 )) & (it
. (n,(m
+ 1)))
= ((it
. (n,m))
+ (Rseq
. (n,(m
+ 1))));
existence
proof
deffunc
F0(
Element of
NAT ) = (Rseq
. ($1,
0 ));
consider f0 be
Function of
NAT ,
REAL such that
a0: for n be
Element of
NAT holds (f0
. n)
=
F0(n) from
FUNCT_2:sch 4;
deffunc
F(
real
number,
Nat,
Nat) = ($1
+ (Rseq
. ($2,($3
+ 1))));
consider IT be
Function of
[:
NAT ,
NAT :],
REAL such that
a1: for a be
Element of
NAT holds (IT
. (a,
0 ))
= (f0
. a) & for n be
natural
number holds (IT
. (a,(n
+ 1)))
=
F(.,a,n) from
RecEx2D1R;
take IT;
hereby
let n,m be
Nat;
a2: n
in
NAT & m
in
NAT by
ORDINAL1:def 12;
then (IT
. (n,
0 ))
= (f0
. n) by
a1;
hence (IT
. (n,
0 ))
= (Rseq
. (n,
0 )) & (IT
. (n,(m
+ 1)))
= ((IT
. (n,m))
+ (Rseq
. (n,(m
+ 1)))) by
a0,
a1,
a2;
end;
end;
uniqueness
proof
let f1,f2 be
Function of
[:
NAT ,
NAT :],
REAL ;
assume that
a1: for n,m be
natural
number holds (f1
. (n,
0 ))
= (Rseq
. (n,
0 )) & (f1
. (n,(m
+ 1)))
= ((f1
. (n,m))
+ (Rseq
. (n,(m
+ 1)))) and
a2: for n,m be
natural
number holds (f2
. (n,
0 ))
= (Rseq
. (n,
0 )) & (f2
. (n,(m
+ 1)))
= ((f2
. (n,m))
+ (Rseq
. (n,(m
+ 1))));
a3: (
dom f1)
=
[:
NAT ,
NAT :] & (
dom f2)
=
[:
NAT ,
NAT :] by
FUNCT_2:def 1;
for n,m be
object st n
in
NAT & m
in
NAT holds (f1
. (n,m))
= (f2
. (n,m))
proof
let n,m be
object;
assume n
in
NAT & m
in
NAT ;
then
reconsider n1 = n, m1 = m as
Element of
NAT ;
defpred
P[
Nat] means (f1
. (n1,$1))
= (f2
. (n1,$1));
(f1
. (n1,
0 ))
= (Rseq
. (n1,
0 )) by
a1;
then
a4:
P[
0 ] by
a2;
a5: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat;
assume
a6:
P[k];
(f1
. (n1,(k
+ 1)))
= ((f1
. (n1,k))
+ (Rseq
. (n1,(k
+ 1)))) by
a1;
hence (f1
. (n1,(k
+ 1)))
= (f2
. (n1,(k
+ 1))) by
a2,
a6;
end;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
a4,
a5);
then
P[m1];
hence (f1
. (n,m))
= (f2
. (n,m));
end;
hence thesis by
a3,
FUNCT_3: 6;
end;
end
definition
let Rseq be
Function of
[:
NAT ,
NAT :],
REAL ;
::
DBLSEQ_2:def3
func
Partial_Sums_in_cod1 (Rseq) ->
Function of
[:
NAT ,
NAT :],
REAL means
:
DefRS: for n,m be
Nat holds (it
. (
0 ,m))
= (Rseq
. (
0 ,m)) & (it
. ((n
+ 1),m))
= ((it
. (n,m))
+ (Rseq
. ((n
+ 1),m)));
existence
proof
deffunc
F0(
Element of
NAT ) = (Rseq
. (
0 ,$1));
consider f0 be
Function of
NAT ,
REAL such that
a0: for n be
Element of
NAT holds (f0
. n)
=
F0(n) from
FUNCT_2:sch 4;
deffunc
F(
Real,
Nat,
Nat) = ($1
+ (Rseq
. (($3
+ 1),$2)));
consider IT be
Function of
[:
NAT ,
NAT :],
REAL such that
a1: for a be
Element of
NAT holds (IT
. (
0 ,a))
= (f0
. a) & for n be
natural
number holds (IT
. ((n
+ 1),a))
=
F(.,a,n) from
RecEx2D2R;
take IT;
hereby
let n,m be
natural
number;
a2: n
in
NAT & m
in
NAT by
ORDINAL1:def 12;
then (IT
. (
0 ,m))
= (f0
. m) by
a1;
hence (IT
. (
0 ,m))
= (Rseq
. (
0 ,m)) & (IT
. ((n
+ 1),m))
= ((IT
. (n,m))
+ (Rseq
. ((n
+ 1),m))) by
a0,
a1,
a2;
end;
end;
uniqueness
proof
let f1,f2 be
Function of
[:
NAT ,
NAT :],
REAL ;
assume that
a1: for n,m be
natural
number holds (f1
. (
0 ,m))
= (Rseq
. (
0 ,m)) & (f1
. ((n
+ 1),m))
= ((f1
. (n,m))
+ (Rseq
. ((n
+ 1),m))) and
a2: for n,m be
natural
number holds (f2
. (
0 ,m))
= (Rseq
. (
0 ,m)) & (f2
. ((n
+ 1),m))
= ((f2
. (n,m))
+ (Rseq
. ((n
+ 1),m)));
a3: (
dom f1)
=
[:
NAT ,
NAT :] & (
dom f2)
=
[:
NAT ,
NAT :] by
FUNCT_2:def 1;
for n,m be
object st n
in
NAT & m
in
NAT holds (f1
. (n,m))
= (f2
. (n,m))
proof
let n,m be
object;
assume n
in
NAT & m
in
NAT ;
then
reconsider n1 = n, m1 = m as
Element of
NAT ;
defpred
P[
Nat] means (f1
. ($1,m1))
= (f2
. ($1,m1));
(f1
. (
0 ,m1))
= (Rseq
. (
0 ,m1)) by
a1;
then
a4:
P[
0 ] by
a2;
a5: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat;
assume
a6:
P[k];
(f1
. ((k
+ 1),m1))
= ((f1
. (k,m1))
+ (Rseq
. ((k
+ 1),m1))) by
a1;
hence (f1
. ((k
+ 1),m1))
= (f2
. ((k
+ 1),m1)) by
a2,
a6;
end;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
a4,
a5);
then
P[n1];
hence (f1
. (n,m))
= (f2
. (n,m));
end;
hence thesis by
a3,
FUNCT_3: 6;
end;
end
theorem ::
DBLSEQ_2:8
thADD: (
Partial_Sums_in_cod2 (Rseq1
+ Rseq2))
= ((
Partial_Sums_in_cod2 Rseq1)
+ (
Partial_Sums_in_cod2 Rseq2)) & (
Partial_Sums_in_cod1 (Rseq1
+ Rseq2))
= ((
Partial_Sums_in_cod1 Rseq1)
+ (
Partial_Sums_in_cod1 Rseq2))
proof
set CS1 = (
Partial_Sums_in_cod2 Rseq1);
set CS2 = (
Partial_Sums_in_cod2 Rseq2);
set CS12 = (
Partial_Sums_in_cod2 (Rseq1
+ Rseq2));
set RS1 = (
Partial_Sums_in_cod1 Rseq1);
set RS2 = (
Partial_Sums_in_cod1 Rseq2);
set RS12 = (
Partial_Sums_in_cod1 (Rseq1
+ Rseq2));
now
let n be
Element of
NAT , m be
Element of
NAT ;
defpred
C[
Nat] means (CS12
. (n,$1))
= ((CS1
. (n,$1))
+ (CS2
. (n,$1)));
(CS12
. (n,
0 ))
= ((Rseq1
+ Rseq2)
. (n,
0 )) by
DefCS
.= ((Rseq1
. (n,
0 ))
+ (Rseq2
. (n,
0 ))) by
lmADD
.= ((CS1
. (n,
0 ))
+ (Rseq2
. (n,
0 ))) by
DefCS;
then
a1:
C[
0 ] by
DefCS;
a2: for k be
Nat st
C[k] holds
C[(k
+ 1)]
proof
let k be
Nat;
assume
a3:
C[k];
(CS12
. (n,(k
+ 1)))
= ((CS12
. (n,k))
+ ((Rseq1
+ Rseq2)
. (n,(k
+ 1)))) by
DefCS
.= (((CS1
. (n,k))
+ (CS2
. (n,k)))
+ ((Rseq1
. (n,(k
+ 1)))
+ (Rseq2
. (n,(k
+ 1))))) by
a3,
lmADD
.= ((((CS1
. (n,k))
+ (Rseq1
. (n,(k
+ 1))))
+ (CS2
. (n,k)))
+ (Rseq2
. (n,(k
+ 1))))
.= (((CS1
. (n,(k
+ 1)))
+ (CS2
. (n,k)))
+ (Rseq2
. (n,(k
+ 1)))) by
DefCS
.= ((CS1
. (n,(k
+ 1)))
+ ((CS2
. (n,k))
+ (Rseq2
. (n,(k
+ 1)))));
hence
C[(k
+ 1)] by
DefCS;
end;
for k be
Nat holds
C[k] from
NAT_1:sch 2(
a1,
a2);
then
C[m];
hence (CS12
. (n,m))
= ((CS1
+ CS2)
. (n,m)) by
lmADD;
end;
hence CS12
= (CS1
+ CS2) by
BINOP_1: 2;
now
let n,m be
Element of
NAT ;
defpred
R[
Nat] means (RS12
. ($1,m))
= ((RS1
. ($1,m))
+ (RS2
. ($1,m)));
(RS12
. (
0 ,m))
= ((Rseq1
+ Rseq2)
. (
0 ,m)) by
DefRS
.= ((Rseq1
. (
0 ,m))
+ (Rseq2
. (
0 ,m))) by
lmADD
.= ((RS1
. (
0 ,m))
+ (Rseq2
. (
0 ,m))) by
DefRS;
then
a4:
R[
0 ] by
DefRS;
a5: for k be
Nat st
R[k] holds
R[(k
+ 1)]
proof
let k be
Nat;
assume
a6:
R[k];
(RS12
. ((k
+ 1),m))
= ((RS12
. (k,m))
+ ((Rseq1
+ Rseq2)
. ((k
+ 1),m))) by
DefRS
.= (((RS1
. (k,m))
+ (RS2
. (k,m)))
+ ((Rseq1
. ((k
+ 1),m))
+ (Rseq2
. ((k
+ 1),m)))) by
a6,
lmADD
.= ((((RS1
. (k,m))
+ (Rseq1
. ((k
+ 1),m)))
+ (RS2
. (k,m)))
+ (Rseq2
. ((k
+ 1),m)))
.= (((RS1
. ((k
+ 1),m))
+ (RS2
. (k,m)))
+ (Rseq2
. ((k
+ 1),m))) by
DefRS
.= ((RS1
. ((k
+ 1),m))
+ ((RS2
. (k,m))
+ (Rseq2
. ((k
+ 1),m))));
hence
R[(k
+ 1)] by
DefRS;
end;
for k be
Nat holds
R[k] from
NAT_1:sch 2(
a4,
a5);
then
R[n];
hence (RS12
. (n,m))
= ((RS1
+ RS2)
. (n,m)) by
lmADD;
end;
hence RS12
= (RS1
+ RS2) by
BINOP_1: 2;
end;
theorem ::
DBLSEQ_2:9
Tr2: for n,m be
Nat holds ((
Partial_Sums_in_cod2 Rseq)
. (n,m))
= ((
Partial_Sums_in_cod1 (
~ Rseq))
. (m,n)) & ((
Partial_Sums_in_cod1 Rseq)
. (n,m))
= ((
Partial_Sums_in_cod2 (
~ Rseq))
. (m,n))
proof
hereby
let n,m be
Nat;
defpred
P[
Nat] means ((
Partial_Sums_in_cod2 Rseq)
. (n,$1))
= ((
Partial_Sums_in_cod1 (
~ Rseq))
. ($1,n));
Z: n
in
NAT & m
in
NAT by
ORDINAL1:def 12;
((
Partial_Sums_in_cod2 Rseq)
. (n,
0 ))
= (Rseq
. (n,
0 )) by
DefCS;
then ((
Partial_Sums_in_cod2 Rseq)
. (n,
0 ))
= ((
~ Rseq)
. (
0 ,n)) by
Z,
FUNCT_4:def 8;
then
a1:
P[
0 ] by
DefRS;
a2:
now
let k be
Nat;
assume
P[k];
then ((
Partial_Sums_in_cod2 Rseq)
. (n,(k
+ 1)))
= (((
Partial_Sums_in_cod1 (
~ Rseq))
. (k,n))
+ (Rseq
. (n,(k
+ 1)))) by
DefCS
.= (((
Partial_Sums_in_cod1 (
~ Rseq))
. (k,n))
+ ((
~ Rseq)
. ((k
+ 1),n))) by
FUNCT_4:def 8,
Z;
hence
P[(k
+ 1)] by
DefRS;
end;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
a1,
a2);
hence ((
Partial_Sums_in_cod2 Rseq)
. (n,m))
= ((
Partial_Sums_in_cod1 (
~ Rseq))
. (m,n));
Z: n
in
NAT & m
in
NAT by
ORDINAL1:def 12;
defpred
Q[
Nat] means ((
Partial_Sums_in_cod1 Rseq)
. ($1,m))
= ((
Partial_Sums_in_cod2 (
~ Rseq))
. (m,$1));
((
Partial_Sums_in_cod1 Rseq)
. (
0 ,m))
= (Rseq
. (
0 ,m)) by
DefRS;
then ((
Partial_Sums_in_cod1 Rseq)
. (
0 ,m))
= ((
~ Rseq)
. (m,
0 )) by
Z,
FUNCT_4:def 8;
then
a4:
Q[
0 ] by
DefCS;
a5:
now
let k be
Nat;
assume
Q[k];
then ((
Partial_Sums_in_cod1 Rseq)
. ((k
+ 1),m))
= (((
Partial_Sums_in_cod2 (
~ Rseq))
. (m,k))
+ (Rseq
. ((k
+ 1),m))) by
DefRS
.= (((
Partial_Sums_in_cod2 (
~ Rseq))
. (m,k))
+ ((
~ Rseq)
. (m,(k
+ 1)))) by
Z,
FUNCT_4:def 8;
hence
Q[(k
+ 1)] by
DefCS;
end;
for k be
Nat holds
Q[k] from
NAT_1:sch 2(
a4,
a5);
hence ((
Partial_Sums_in_cod1 Rseq)
. (n,m))
= ((
Partial_Sums_in_cod2 (
~ Rseq))
. (m,n));
end;
end;
theorem ::
DBLSEQ_2:10
(
Partial_Sums_in_cod2 Rseq)
= (
~ (
Partial_Sums_in_cod1 (
~ Rseq))) & (
Partial_Sums_in_cod2 (
~ Rseq))
= (
~ (
Partial_Sums_in_cod1 Rseq)) & (
~ (
Partial_Sums_in_cod2 Rseq))
= (
Partial_Sums_in_cod1 (
~ Rseq)) & (
~ (
Partial_Sums_in_cod2 (
~ Rseq)))
= (
Partial_Sums_in_cod1 Rseq)
proof
now
let n,m be
Element of
NAT ;
((
Partial_Sums_in_cod2 Rseq)
. (n,m))
= ((
Partial_Sums_in_cod1 (
~ Rseq))
. (m,n)) by
Tr2;
hence ((
Partial_Sums_in_cod2 Rseq)
. (n,m))
= ((
~ (
Partial_Sums_in_cod1 (
~ Rseq)))
. (n,m)) by
FUNCT_4:def 8;
end;
hence (
Partial_Sums_in_cod2 Rseq)
= (
~ (
Partial_Sums_in_cod1 (
~ Rseq))) by
BINOP_1: 2;
now
let n,m be
Element of
NAT ;
((
Partial_Sums_in_cod2 (
~ Rseq))
. (n,m))
= ((
Partial_Sums_in_cod1 Rseq)
. (m,n)) by
Tr2;
hence ((
Partial_Sums_in_cod2 (
~ Rseq))
. (n,m))
= ((
~ (
Partial_Sums_in_cod1 Rseq))
. (n,m)) by
FUNCT_4:def 8;
end;
hence
a1: (
Partial_Sums_in_cod2 (
~ Rseq))
= (
~ (
Partial_Sums_in_cod1 Rseq)) by
BINOP_1: 2;
now
let n,m be
Element of
NAT ;
((
~ (
Partial_Sums_in_cod2 Rseq))
. (n,m))
= ((
Partial_Sums_in_cod2 Rseq)
. (m,n)) by
FUNCT_4:def 8;
hence ((
~ (
Partial_Sums_in_cod2 Rseq))
. (n,m))
= ((
Partial_Sums_in_cod1 (
~ Rseq))
. (n,m)) by
Tr2;
end;
hence (
~ (
Partial_Sums_in_cod2 Rseq))
= (
Partial_Sums_in_cod1 (
~ Rseq)) by
BINOP_1: 2;
now
let n,m be
Element of
NAT ;
((
~ (
Partial_Sums_in_cod2 (
~ Rseq)))
. (n,m))
= ((
~ (
Partial_Sums_in_cod1 Rseq))
. (m,n)) by
a1,
FUNCT_4:def 8;
hence ((
~ (
Partial_Sums_in_cod2 (
~ Rseq)))
. (n,m))
= ((
Partial_Sums_in_cod1 Rseq)
. (n,m)) by
FUNCT_4:def 8;
end;
hence (
~ (
Partial_Sums_in_cod2 (
~ Rseq)))
= (
Partial_Sums_in_cod1 Rseq) by
BINOP_1: 2;
end;
definition
let Rseq be
Function of
[:
NAT ,
NAT :],
REAL ;
::
DBLSEQ_2:def4
func
Partial_Sums (Rseq) ->
Function of
[:
NAT ,
NAT :],
REAL equals (
Partial_Sums_in_cod2 (
Partial_Sums_in_cod1 Rseq));
correctness ;
end
theorem ::
DBLSEQ_2:11
ThRS: for n,m be
Nat holds ((
Partial_Sums Rseq)
. ((n
+ 1),m))
= (((
Partial_Sums_in_cod2 Rseq)
. ((n
+ 1),m))
+ ((
Partial_Sums Rseq)
. (n,m))) & ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (n,(m
+ 1)))
= (((
Partial_Sums_in_cod1 Rseq)
. (n,(m
+ 1)))
+ ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (n,m)))
proof
let n,m be
Nat;
set RPS = (
Partial_Sums Rseq);
set CPS = (
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq));
set ROW = (
Partial_Sums_in_cod1 Rseq);
set COL = (
Partial_Sums_in_cod2 Rseq);
defpred
P[
Nat] means (RPS
. ((n
+ 1),$1))
= ((COL
. ((n
+ 1),$1))
+ (RPS
. (n,$1)));
a1: (RPS
. (n,
0 ))
= (ROW
. (n,
0 )) by
DefCS;
(RPS
. ((n
+ 1),
0 ))
= (ROW
. ((n
+ 1),
0 )) by
DefCS
.= ((ROW
. (n,
0 ))
+ (Rseq
. ((n
+ 1),
0 ))) by
DefRS;
then
a3:
P[
0 ] by
a1,
DefCS;
a4: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat;
assume
A5:
P[k];
a6: (COL
. ((n
+ 1),(k
+ 1)))
= ((COL
. ((n
+ 1),k))
+ (Rseq
. ((n
+ 1),(k
+ 1)))) by
DefCS;
(RPS
. (n,(k
+ 1)))
= ((RPS
. (n,k))
+ (ROW
. (n,(k
+ 1)))) by
DefCS;
then ((COL
. ((n
+ 1),(k
+ 1)))
+ (RPS
. (n,(k
+ 1))))
= ((RPS
. ((n
+ 1),k))
+ ((Rseq
. ((n
+ 1),(k
+ 1)))
+ (ROW
. (n,(k
+ 1))))) by
A5,
a6
.= ((RPS
. ((n
+ 1),k))
+ (ROW
. ((n
+ 1),(k
+ 1)))) by
DefRS;
hence
P[(k
+ 1)] by
DefCS;
end;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
a3,
a4);
hence (RPS
. ((n
+ 1),m))
= ((COL
. ((n
+ 1),m))
+ (RPS
. (n,m)));
defpred
Q[
Nat] means (CPS
. ($1,(m
+ 1)))
= ((ROW
. ($1,(m
+ 1)))
+ (CPS
. ($1,m)));
b1: (CPS
. (
0 ,m))
= (COL
. (
0 ,m)) by
DefRS;
(CPS
. (
0 ,(m
+ 1)))
= (COL
. (
0 ,(m
+ 1))) by
DefRS
.= ((COL
. (
0 ,m))
+ (Rseq
. (
0 ,(m
+ 1)))) by
DefCS;
then
b3:
Q[
0 ] by
b1,
DefRS;
b4: for k be
Nat st
Q[k] holds
Q[(k
+ 1)]
proof
let k be
Nat;
assume
B5:
Q[k];
b6: (ROW
. ((k
+ 1),(m
+ 1)))
= ((ROW
. (k,(m
+ 1)))
+ (Rseq
. ((k
+ 1),(m
+ 1)))) by
DefRS;
(CPS
. ((k
+ 1),m))
= ((CPS
. (k,m))
+ (COL
. ((k
+ 1),m))) by
DefRS;
then ((ROW
. ((k
+ 1),(m
+ 1)))
+ (CPS
. ((k
+ 1),m)))
= ((CPS
. (k,(m
+ 1)))
+ ((Rseq
. ((k
+ 1),(m
+ 1)))
+ (COL
. ((k
+ 1),m)))) by
B5,
b6
.= ((CPS
. (k,(m
+ 1)))
+ (COL
. ((k
+ 1),(m
+ 1)))) by
DefCS;
hence
Q[(k
+ 1)] by
DefRS;
end;
for k be
Nat holds
Q[k] from
NAT_1:sch 2(
b3,
b4);
hence thesis;
end;
th103: for m,n be
Nat holds ((
Partial_Sums Rseq)
. (m,n))
= ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (m,n))
proof
defpred
P1[
Nat] means for m be
Nat holds ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (m,$1))
= ((
Partial_Sums Rseq)
. (m,$1));
defpred
P2[
Nat] means ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. ($1,
0 ))
= ((
Partial_Sums Rseq)
. ($1,
0 ));
Y3: ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (
0 ,
0 ))
= ((
Partial_Sums_in_cod2 Rseq)
. (
0 ,
0 )) by
DefRS
.= (Rseq
. (
0 ,
0 )) by
DefCS;
((
Partial_Sums Rseq)
. (
0 ,
0 ))
= ((
Partial_Sums_in_cod1 Rseq)
. (
0 ,
0 )) by
DefCS
.= (Rseq
. (
0 ,
0 )) by
DefRS;
then
Y1:
P2[
0 ] by
Y3;
Y2: for i be
Nat st
P2[i] holds
P2[(i
+ 1)]
proof
let i be
Nat;
assume
Y3:
P2[i];
Y4: ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. ((i
+ 1),
0 ))
= (((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (i,
0 ))
+ ((
Partial_Sums_in_cod2 Rseq)
. ((i
+ 1),
0 ))) by
DefRS
.= (((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (i,
0 ))
+ (Rseq
. ((i
+ 1),
0 ))) by
DefCS;
((
Partial_Sums Rseq)
. ((i
+ 1),
0 ))
= ((
Partial_Sums_in_cod1 Rseq)
. ((i
+ 1),
0 )) by
DefCS
.= (((
Partial_Sums_in_cod1 Rseq)
. (i,
0 ))
+ (Rseq
. ((i
+ 1),
0 ))) by
DefRS
.= (((
Partial_Sums Rseq)
. (i,
0 ))
+ (Rseq
. ((i
+ 1),
0 ))) by
DefCS;
hence
P2[(i
+ 1)] by
Y3,
Y4;
end;
for n be
Nat holds
P2[n] from
NAT_1:sch 2(
Y1,
Y2);
then
X1:
P1[
0 ];
X2: for j be
Nat st
P1[j] holds
P1[(j
+ 1)]
proof
let j be
Nat;
assume
Z3:
P1[j];
for m be
Nat holds ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (m,(j
+ 1)))
= ((
Partial_Sums Rseq)
. (m,(j
+ 1)))
proof
let n be
Nat;
defpred
P3[
Nat] means ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. ($1,(j
+ 1)))
= ((
Partial_Sums Rseq)
. ($1,(j
+ 1)));
Z4: ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (
0 ,(j
+ 1)))
= ((
Partial_Sums_in_cod2 Rseq)
. (
0 ,(j
+ 1))) by
DefRS
.= (((
Partial_Sums_in_cod2 Rseq)
. (
0 ,j))
+ (Rseq
. (
0 ,(j
+ 1)))) by
DefCS
.= (((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (
0 ,j))
+ (Rseq
. (
0 ,(j
+ 1)))) by
DefRS;
((
Partial_Sums Rseq)
. (
0 ,(j
+ 1)))
= (((
Partial_Sums Rseq)
. (
0 ,j))
+ ((
Partial_Sums_in_cod1 Rseq)
. (
0 ,(j
+ 1)))) by
DefCS
.= (((
Partial_Sums Rseq)
. (
0 ,j))
+ (Rseq
. (
0 ,(j
+ 1)))) by
DefRS
.= (((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (
0 ,j))
+ (Rseq
. (
0 ,(j
+ 1)))) by
Z3;
then
Z1:
P3[
0 ] by
Z4;
Z2: for i be
Nat st
P3[i] holds
P3[(i
+ 1)]
proof
let i be
Nat;
assume
P3[i];
Z6: ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (i,j))
= ((
Partial_Sums Rseq)
. (i,j)) by
Z3;
((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. ((i
+ 1),(j
+ 1)))
= (((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (i,(j
+ 1)))
+ ((
Partial_Sums_in_cod2 Rseq)
. ((i
+ 1),(j
+ 1)))) by
DefRS
.= ((((
Partial_Sums Rseq)
. (i,j))
+ ((
Partial_Sums_in_cod1 Rseq)
. (i,(j
+ 1))))
+ ((
Partial_Sums_in_cod2 Rseq)
. ((i
+ 1),(j
+ 1)))) by
Z6,
ThRS
.= ((((
Partial_Sums Rseq)
. (i,j))
+ ((
Partial_Sums_in_cod1 Rseq)
. (i,(j
+ 1))))
+ (((
Partial_Sums_in_cod2 Rseq)
. ((i
+ 1),j))
+ (Rseq
. ((i
+ 1),(j
+ 1))))) by
DefCS
.= ((((
Partial_Sums Rseq)
. (i,j))
+ (((
Partial_Sums_in_cod1 Rseq)
. (i,(j
+ 1)))
+ (Rseq
. ((i
+ 1),(j
+ 1)))))
+ ((
Partial_Sums_in_cod2 Rseq)
. ((i
+ 1),j)))
.= ((((
Partial_Sums Rseq)
. (i,j))
+ ((
Partial_Sums_in_cod1 Rseq)
. ((i
+ 1),(j
+ 1))))
+ ((
Partial_Sums_in_cod2 Rseq)
. ((i
+ 1),j))) by
DefRS
.= ((((
Partial_Sums Rseq)
. (i,j))
+ ((
Partial_Sums_in_cod2 Rseq)
. ((i
+ 1),j)))
+ ((
Partial_Sums_in_cod1 Rseq)
. ((i
+ 1),(j
+ 1))))
.= (((
Partial_Sums Rseq)
. ((i
+ 1),j))
+ ((
Partial_Sums_in_cod1 Rseq)
. ((i
+ 1),(j
+ 1)))) by
ThRS;
hence thesis by
DefCS;
end;
for n be
Nat holds
P3[n] from
NAT_1:sch 2(
Z1,
Z2);
hence thesis;
end;
hence
P1[(j
+ 1)];
end;
for m be
Nat holds
P1[m] from
NAT_1:sch 2(
X1,
X2);
hence thesis;
end;
theorem ::
DBLSEQ_2:12
th103a: (
Partial_Sums Rseq)
= (
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
proof
now
let x be
Element of
[:
NAT ,
NAT :];
consider n,m be
object such that
A1: n
in
NAT & m
in
NAT & x
=
[n, m] by
ZFMISC_1:def 2;
reconsider n1 = n, m1 = m as
Nat by
A1;
((
Partial_Sums Rseq)
. (n1,m1))
= ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (n1,m1)) by
th103;
hence ((
Partial_Sums Rseq)
. x)
= ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. x) by
A1;
end;
hence thesis;
end;
theorem ::
DBLSEQ_2:13
thRS2: for n,m be
Nat holds (Rseq
. ((n
+ 1),(m
+ 1)))
= (((((
Partial_Sums Rseq)
. ((n
+ 1),(m
+ 1)))
- ((
Partial_Sums Rseq)
. (n,(m
+ 1))))
- ((
Partial_Sums Rseq)
. ((n
+ 1),m)))
+ ((
Partial_Sums Rseq)
. (n,m)))
proof
let n,m be
Nat;
set RPS = (
Partial_Sums_in_cod2 (
Partial_Sums_in_cod1 Rseq));
A1: (RPS
. ((n
+ 1),(m
+ 1)))
= (((
Partial_Sums_in_cod1 Rseq)
. ((n
+ 1),(m
+ 1)))
+ (RPS
. ((n
+ 1),m))) by
DefCS
.= (((Rseq
. ((n
+ 1),(m
+ 1)))
+ ((
Partial_Sums_in_cod1 Rseq)
. (n,(m
+ 1))))
+ (RPS
. ((n
+ 1),m))) by
DefRS;
(RPS
. (n,(m
+ 1)))
= (((
Partial_Sums_in_cod1 Rseq)
. (n,(m
+ 1)))
+ (RPS
. (n,m))) by
DefCS;
hence thesis by
A1;
end;
theorem ::
DBLSEQ_2:14
for n,m be
Nat holds (Rseq
. ((n
+ 1),(m
+ 1)))
= (((((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. ((n
+ 1),(m
+ 1)))
- ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. ((n
+ 1),m)))
- ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (n,(m
+ 1))))
+ ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (n,m)))
proof
let n,m be
Nat;
set CPS = (
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq));
set CS = (
Partial_Sums_in_cod2 Rseq);
A1: (CPS
. ((n
+ 1),(m
+ 1)))
= ((CS
. ((n
+ 1),(m
+ 1)))
+ (CPS
. (n,(m
+ 1)))) by
DefRS
.= (((Rseq
. ((n
+ 1),(m
+ 1)))
+ (CS
. ((n
+ 1),m)))
+ (CPS
. (n,(m
+ 1)))) by
DefCS;
(CPS
. ((n
+ 1),m))
= ((CS
. ((n
+ 1),m))
+ (CPS
. (n,m))) by
DefRS;
hence thesis by
A1;
end;
theorem ::
DBLSEQ_2:15
(
Partial_Sums Rseq) is
P-convergent implies Rseq is
P-convergent & (
P-lim Rseq)
=
0
proof
set CPS = (
Partial_Sums Rseq);
assume
A1: CPS is
P-convergent;
set Plim = (
P-lim CPS);
a2: for e be
Real st
0
< e holds ex N be
Nat st for n,m be
Nat st n
>= N & m
>= N holds
|.((Rseq
. (n,m))
-
0 ).|
< e
proof
let e be
Real;
assume
A3:
0
< e;
set e1 = (e
/ 4);
consider N be
Nat such that
a4: for n,m be
Nat st n
>= N & m
>= N holds
|.((CPS
. (n,m))
- Plim).|
< e1 by
A1,
A3,
DBLSEQ_1:def 2;
take N1 = (N
+ 1);
hereby
let n1,m1 be
Nat;
assume
A5: n1
>= N1 & m1
>= N1;
then
a5: n1
> N & m1
> N by
NAT_1: 13;
then
reconsider n = (n1
- 1), m = (m1
- 1) as
Element of
NAT by
NAT_1: 20;
a6: n1
= (n
+ 1) & m1
= (m
+ 1);
(n
+ 1)
> N & (m
+ 1)
> N by
A5,
NAT_1: 13;
then
a7: n
>= N & m
>= N by
NAT_1: 13;
(Rseq
. (n1,m1))
= ((((CPS
. (n1,m1))
- (CPS
. (n,m1)))
- (CPS
. (n1,m)))
+ (CPS
. (n,m))) by
a6,
thRS2
.= ((((CPS
. (n1,m1))
- Plim)
- ((CPS
. (n1,m))
- Plim))
- (((CPS
. (n,m1))
- Plim)
- ((CPS
. (n,m))
- Plim)));
then
a8:
|.((Rseq
. (n1,m1))
-
0 ).|
<= (
|.(((CPS
. (n1,m1))
- Plim)
- ((CPS
. (n1,m))
- Plim)).|
+
|.(((CPS
. (n,m1))
- Plim)
- ((CPS
. (n,m))
- Plim)).|) by
COMPLEX1: 57;
a9:
|.(((CPS
. (n1,m1))
- Plim)
- ((CPS
. (n1,m))
- Plim)).|
<= (
|.((CPS
. (n1,m1))
- Plim).|
+
|.((CPS
. (n1,m))
- Plim).|) by
COMPLEX1: 57;
a10:
|.(((CPS
. (n,m1))
- Plim)
- ((CPS
. (n,m))
- Plim)).|
<= (
|.((CPS
. (n,m1))
- Plim).|
+
|.((CPS
. (n,m))
- Plim).|) by
COMPLEX1: 57;
|.((CPS
. (n1,m1))
- Plim).|
< e1 &
|.((CPS
. (n,m1))
- Plim).|
< e1 &
|.((CPS
. (n1,m))
- Plim).|
< e1 &
|.((CPS
. (n,m))
- Plim).|
< e1 by
a4,
a5,
a7;
then (
|.((CPS
. (n1,m1))
- Plim).|
+
|.((CPS
. (n1,m))
- Plim).|)
< (e1
+ e1) & (
|.((CPS
. (n,m1))
- Plim).|
+
|.((CPS
. (n,m))
- Plim).|)
< (e1
+ e1) by
XREAL_1: 8;
then
|.(((CPS
. (n1,m1))
- Plim)
- ((CPS
. (n1,m))
- Plim)).|
< (e1
+ e1) &
|.(((CPS
. (n,m1))
- Plim)
- ((CPS
. (n,m))
- Plim)).|
< (e1
+ e1) by
a9,
a10,
XXREAL_0: 2;
then (
|.(((CPS
. (n1,m1))
- Plim)
- ((CPS
. (n1,m))
- Plim)).|
+
|.(((CPS
. (n,m1))
- Plim)
- ((CPS
. (n,m))
- Plim)).|)
< ((e1
+ e1)
+ (e1
+ e1)) by
XREAL_1: 8;
hence
|.((Rseq
. (n1,m1))
-
0 ).|
< e by
a8,
XXREAL_0: 2;
end;
end;
hence Rseq is
P-convergent;
hence (
P-lim Rseq)
=
0 by
a2,
DBLSEQ_1:def 2;
end;
theorem ::
DBLSEQ_2:16
lm74: (
Partial_Sums (Rseq1
+ Rseq2))
= ((
Partial_Sums Rseq1)
+ (
Partial_Sums Rseq2))
proof
(
Partial_Sums (Rseq1
+ Rseq2))
= (
Partial_Sums_in_cod2 ((
Partial_Sums_in_cod1 Rseq1)
+ (
Partial_Sums_in_cod1 Rseq2))) by
thADD;
hence thesis by
thADD;
end;
theorem ::
DBLSEQ_2:17
(
Partial_Sums Rseq1) is
P-convergent & (
Partial_Sums Rseq2) is
P-convergent implies (
Partial_Sums (Rseq1
+ Rseq2)) is
P-convergent
proof
assume (
Partial_Sums Rseq1) is
P-convergent & (
Partial_Sums Rseq2) is
P-convergent;
then ((
Partial_Sums Rseq1)
+ (
Partial_Sums Rseq2)) is
P-convergent by
DBLSEQ_1: 11;
hence thesis by
lm74;
end;
theorem ::
DBLSEQ_2:18
th100: for m,n be
Element of
NAT holds ((
Partial_Sums_in_cod1 Rseq)
. (m,n))
= ((
Partial_Sums (
ProjMap2 (Rseq,n)))
. m) & ((
Partial_Sums_in_cod2 Rseq)
. (m,n))
= ((
Partial_Sums (
ProjMap1 (Rseq,m)))
. n)
proof
let m,n be
Element of
NAT ;
defpred
P[
Nat] means ((
Partial_Sums_in_cod1 Rseq)
. ($1,n))
= ((
Partial_Sums (
ProjMap2 (Rseq,n)))
. $1);
((
Partial_Sums (
ProjMap2 (Rseq,n)))
.
0 )
= ((
ProjMap2 (Rseq,n))
.
0 ) by
SERIES_1:def 1
.= (Rseq
. (
0 ,n)) by
MESFUNC9:def 7;
then
a1:
P[
0 ] by
DefRS;
a2: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat;
assume
P[k];
then ((
Partial_Sums_in_cod1 Rseq)
. ((k
+ 1),n))
= (((
Partial_Sums (
ProjMap2 (Rseq,n)))
. k)
+ (Rseq
. ((k
+ 1),n))) by
DefRS
.= (((
Partial_Sums (
ProjMap2 (Rseq,n)))
. k)
+ ((
ProjMap2 (Rseq,n))
. (k
+ 1))) by
MESFUNC9:def 7;
hence
P[(k
+ 1)] by
SERIES_1:def 1;
end;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
a1,
a2);
hence ((
Partial_Sums_in_cod1 Rseq)
. (m,n))
= ((
Partial_Sums (
ProjMap2 (Rseq,n)))
. m);
defpred
Q[
Nat] means ((
Partial_Sums_in_cod2 Rseq)
. (m,$1))
= ((
Partial_Sums (
ProjMap1 (Rseq,m)))
. $1);
((
Partial_Sums (
ProjMap1 (Rseq,m)))
.
0 )
= ((
ProjMap1 (Rseq,m))
.
0 ) by
SERIES_1:def 1
.= (Rseq
. (m,
0 )) by
MESFUNC9:def 6;
then
a3:
Q[
0 ] by
DefCS;
a4: for k be
Nat st
Q[k] holds
Q[(k
+ 1)]
proof
let k be
Nat;
assume
Q[k];
then ((
Partial_Sums_in_cod2 Rseq)
. (m,(k
+ 1)))
= (((
Partial_Sums (
ProjMap1 (Rseq,m)))
. k)
+ (Rseq
. (m,(k
+ 1)))) by
DefCS
.= (((
Partial_Sums (
ProjMap1 (Rseq,m)))
. k)
+ ((
ProjMap1 (Rseq,m))
. (k
+ 1))) by
MESFUNC9:def 6;
hence
Q[(k
+ 1)] by
SERIES_1:def 1;
end;
for k be
Nat holds
Q[k] from
NAT_1:sch 2(
a3,
a4);
hence thesis;
end;
theorem ::
DBLSEQ_2:19
th00: (
ProjMap1 ((
Partial_Sums Rseq),
0 ))
= (
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),
0 )) & (
ProjMap2 ((
Partial_Sums Rseq),
0 ))
= (
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),
0 ))
proof
A1:
now
let m be
Element of
NAT ;
((
ProjMap1 ((
Partial_Sums Rseq),
0 ))
. m)
= ((
Partial_Sums Rseq)
. (
0 ,m)) by
MESFUNC9:def 6
.= ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (
0 ,m)) by
th103a
.= ((
Partial_Sums_in_cod2 Rseq)
. (
0 ,m)) by
DefRS;
hence ((
ProjMap1 ((
Partial_Sums Rseq),
0 ))
. m)
= ((
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),
0 ))
. m) by
MESFUNC9:def 6;
end;
now
let n be
Element of
NAT ;
((
ProjMap2 ((
Partial_Sums Rseq),
0 ))
. n)
= ((
Partial_Sums Rseq)
. (n,
0 )) by
MESFUNC9:def 7
.= ((
Partial_Sums_in_cod1 Rseq)
. (n,
0 )) by
DefCS;
hence ((
ProjMap2 ((
Partial_Sums Rseq),
0 ))
. n)
= ((
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),
0 ))
. n) by
MESFUNC9:def 7;
end;
hence thesis by
A1;
end;
theorem ::
DBLSEQ_2:20
for C,D be non
empty
set, F1,F2 be
Function of
[:C, D:],
REAL , c be
Element of C holds (
ProjMap1 ((F1
+ F2),c))
= ((
ProjMap1 (F1,c))
+ (
ProjMap1 (F2,c)))
proof
let C,D be non
empty
set;
let F1,F2 be
Function of
[:C, D:],
REAL ;
let c be
Element of C;
(
dom (
ProjMap1 ((F1
+ F2),c)))
= D & (
dom (
ProjMap1 (F1,c)))
= D & (
dom (
ProjMap1 (F2,c)))
= D by
FUNCT_2:def 1;
then
A2: (
dom (
ProjMap1 ((F1
+ F2),c)))
= ((
dom (
ProjMap1 (F1,c)))
/\ (
dom (
ProjMap1 (F2,c))));
for d be
object st d
in (
dom (
ProjMap1 ((F1
+ F2),c))) holds ((
ProjMap1 ((F1
+ F2),c))
. d)
= (((
ProjMap1 (F1,c))
. d)
+ ((
ProjMap1 (F2,c))
. d))
proof
let d be
object;
assume
A3: d
in (
dom (
ProjMap1 ((F1
+ F2),c)));
then
A4: ((
ProjMap1 ((F1
+ F2),c))
. d)
= ((F1
+ F2)
. (c,d)) & ((
ProjMap1 (F1,c))
. d)
= (F1
. (c,d)) & ((
ProjMap1 (F2,c))
. d)
= (F2
. (c,d)) by
MESFUNC9:def 6;
reconsider d1 = d as
Element of D by
A3;
[c, d]
in
[:C, D:] by
A3,
ZFMISC_1:def 2;
then
[c, d]
in (
dom (F1
+ F2)) by
FUNCT_2:def 1;
hence thesis by
A4,
VALUED_1:def 1;
end;
hence thesis by
A2,
VALUED_1:def 1;
end;
theorem ::
DBLSEQ_2:21
for C,D be non
empty
set, F1,F2 be
Function of
[:C, D:],
REAL , d be
Element of D holds (
ProjMap2 ((F1
+ F2),d))
= ((
ProjMap2 (F1,d))
+ (
ProjMap2 (F2,d)))
proof
let C,D be non
empty
set;
let F1,F2 be
Function of
[:C, D:],
REAL ;
let d be
Element of D;
(
dom (
ProjMap2 ((F1
+ F2),d)))
= C & (
dom (
ProjMap2 (F1,d)))
= C & (
dom (
ProjMap2 (F2,d)))
= C by
FUNCT_2:def 1;
then
A2: (
dom (
ProjMap2 ((F1
+ F2),d)))
= ((
dom (
ProjMap2 (F1,d)))
/\ (
dom (
ProjMap2 (F2,d))));
for c be
object st c
in (
dom (
ProjMap2 ((F1
+ F2),d))) holds ((
ProjMap2 ((F1
+ F2),d))
. c)
= (((
ProjMap2 (F1,d))
. c)
+ ((
ProjMap2 (F2,d))
. c))
proof
let c be
object;
assume
A3: c
in (
dom (
ProjMap2 ((F1
+ F2),d)));
then
A4: ((
ProjMap2 ((F1
+ F2),d))
. c)
= ((F1
+ F2)
. (c,d)) & ((
ProjMap2 (F1,d))
. c)
= (F1
. (c,d)) & ((
ProjMap2 (F2,d))
. c)
= (F2
. (c,d)) by
MESFUNC9:def 7;
reconsider c1 = c as
Element of C by
A3;
[c, d]
in
[:C, D:] by
A3,
ZFMISC_1:def 2;
then
[c, d]
in (
dom (F1
+ F2)) by
FUNCT_2:def 1;
hence thesis by
A4,
VALUED_1:def 1;
end;
hence thesis by
A2,
VALUED_1:def 1;
end;
theorem ::
DBLSEQ_2:22
th01a: (
Partial_Sums Rseq) is
convergent_in_cod1 iff (
Partial_Sums_in_cod1 Rseq) is
convergent_in_cod1
proof
hereby
assume
A1: (
Partial_Sums Rseq) is
convergent_in_cod1;
now
let m be
Element of
NAT ;
defpred
P[
Nat] means for k be
Element of
NAT st k
= $1 holds (
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),k)) is
convergent;
now
let k be
Element of
NAT ;
assume k
=
0 ;
then (
ProjMap2 ((
Partial_Sums Rseq),k))
= (
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),k)) by
th00;
hence (
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),k)) is
convergent by
A1;
end;
then
A3:
P[
0 ];
A4: for m1 be
Nat st
P[m1] holds
P[(m1
+ 1)]
proof
let m1 be
Nat;
reconsider m = m1 as
Element of
NAT by
ORDINAL1:def 12;
assume
P[m1];
hereby
let k be
Element of
NAT ;
assume
B2: k
= (m1
+ 1);
then
reconsider k1 = (k
- 1) as
Element of
NAT by
NAT_1: 11,
NAT_1: 21;
B4: (
ProjMap2 ((
Partial_Sums Rseq),m)) is
convergent & (
ProjMap2 ((
Partial_Sums Rseq),k)) is
convergent by
A1;
now
let e be
Real;
assume
B6:
0
< e;
then
consider N1 be
Nat such that
B7: for n be
Nat st n
>= N1 holds
|.(((
ProjMap2 ((
Partial_Sums Rseq),m))
. n)
- (
lim (
ProjMap2 ((
Partial_Sums Rseq),m)))).|
< (e
/ 2) by
B4,
SEQ_2:def 7;
consider N2 be
Nat such that
B8: for n be
Nat st n
>= N2 holds
|.(((
ProjMap2 ((
Partial_Sums Rseq),k))
. n)
- (
lim (
ProjMap2 ((
Partial_Sums Rseq),k)))).|
< (e
/ 2) by
B4,
B6,
SEQ_2:def 7;
reconsider N = (
max (N1,N2)) as
Nat by
TARSKI: 1;
take N;
hereby
let n be
Nat;
assume
B9: n
>= N;
N
>= N1 & N
>= N2 by
XXREAL_0: 25;
then n
>= N1 & n
>= N2 by
B9,
XXREAL_0: 2;
then
|.(((
ProjMap2 ((
Partial_Sums Rseq),m))
. n)
- (
lim (
ProjMap2 ((
Partial_Sums Rseq),m)))).|
< (e
/ 2) &
|.(((
ProjMap2 ((
Partial_Sums Rseq),k))
. n)
- (
lim (
ProjMap2 ((
Partial_Sums Rseq),k)))).|
< (e
/ 2) by
B7,
B8;
then
B12: (
|.(((
ProjMap2 ((
Partial_Sums Rseq),m))
. n)
- (
lim (
ProjMap2 ((
Partial_Sums Rseq),m)))).|
+
|.(((
ProjMap2 ((
Partial_Sums Rseq),k))
. n)
- (
lim (
ProjMap2 ((
Partial_Sums Rseq),k)))).|)
< ((e
/ 2)
+ (e
/ 2)) by
XREAL_1: 8;
reconsider n1 = n as
Element of
NAT by
ORDINAL1:def 12;
((
ProjMap2 ((
Partial_Sums Rseq),k))
. n)
= ((
Partial_Sums Rseq)
. (n1,k)) by
MESFUNC9:def 7
.= (((
Partial_Sums Rseq)
. (n1,m))
+ ((
Partial_Sums_in_cod1 Rseq)
. (n1,k))) by
B2,
DefCS
.= (((
ProjMap2 ((
Partial_Sums Rseq),m))
. n)
+ ((
Partial_Sums_in_cod1 Rseq)
. (n1,k))) by
MESFUNC9:def 7
.= (((
ProjMap2 ((
Partial_Sums Rseq),m))
. n)
+ ((
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),k))
. n)) by
MESFUNC9:def 7;
then
|.(((
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),k))
. n)
- ((
lim (
ProjMap2 ((
Partial_Sums Rseq),k)))
- (
lim (
ProjMap2 ((
Partial_Sums Rseq),m))))).|
=
|.((((
ProjMap2 ((
Partial_Sums Rseq),k))
. n)
- (
lim (
ProjMap2 ((
Partial_Sums Rseq),k))))
- (((
ProjMap2 ((
Partial_Sums Rseq),m))
. n)
- (
lim (
ProjMap2 ((
Partial_Sums Rseq),m))))).|;
then
|.(((
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),k))
. n)
- ((
lim (
ProjMap2 ((
Partial_Sums Rseq),k)))
- (
lim (
ProjMap2 ((
Partial_Sums Rseq),m))))).|
<= (
|.(((
ProjMap2 ((
Partial_Sums Rseq),k))
. n)
- (
lim (
ProjMap2 ((
Partial_Sums Rseq),k)))).|
+
|.(((
ProjMap2 ((
Partial_Sums Rseq),m))
. n)
- (
lim (
ProjMap2 ((
Partial_Sums Rseq),m)))).|) by
COMPLEX1: 57;
hence
|.(((
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),k))
. n)
- ((
lim (
ProjMap2 ((
Partial_Sums Rseq),k)))
- (
lim (
ProjMap2 ((
Partial_Sums Rseq),m))))).|
< e by
B12,
XXREAL_0: 2;
end;
end;
hence (
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),k)) is
convergent by
SEQ_2:def 6;
end;
end;
for m1 be
Nat holds
P[m1] from
NAT_1:sch 2(
A3,
A4);
hence (
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),m)) is
convergent;
end;
hence (
Partial_Sums_in_cod1 Rseq) is
convergent_in_cod1;
end;
assume
C0: (
Partial_Sums_in_cod1 Rseq) is
convergent_in_cod1;
now
let m be
Element of
NAT ;
defpred
P[
Nat] means for k be
Element of
NAT st k
= $1 holds (
ProjMap2 ((
Partial_Sums Rseq),k)) is
convergent;
(
ProjMap2 ((
Partial_Sums Rseq),
0 ))
= (
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),
0 )) by
th00;
then
C1:
P[
0 ] by
C0;
C2: for m be
Nat st
P[m] holds
P[(m
+ 1)]
proof
let m be
Nat;
assume
C3:
P[m];
reconsider m1 = m as
Element of
NAT by
ORDINAL1:def 12;
hereby
let k be
Element of
NAT ;
assume
C4: k
= (m
+ 1);
then
reconsider k1 = (k
- 1) as
Element of
NAT by
NAT_1: 11,
NAT_1: 21;
for n be
Element of
NAT holds ((
ProjMap2 ((
Partial_Sums Rseq),k))
. n)
= (((
ProjMap2 ((
Partial_Sums Rseq),m1))
+ (
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),(m1
+ 1))))
. n)
proof
let n be
Element of
NAT ;
((
ProjMap2 ((
Partial_Sums Rseq),k))
. n)
= ((
Partial_Sums Rseq)
. (n,(m1
+ 1))) by
C4,
MESFUNC9:def 7
.= ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (n,(m1
+ 1))) by
th103a
.= (((
Partial_Sums_in_cod1 Rseq)
. (n,(m1
+ 1)))
+ ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (n,m1))) by
ThRS
.= (((
Partial_Sums_in_cod1 Rseq)
. (n,(m1
+ 1)))
+ ((
Partial_Sums Rseq)
. (n,m1))) by
th103a
.= (((
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),(m1
+ 1)))
. n)
+ ((
Partial_Sums Rseq)
. (n,m1))) by
MESFUNC9:def 7
.= (((
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),(m1
+ 1)))
. n)
+ ((
ProjMap2 ((
Partial_Sums Rseq),m1))
. n)) by
MESFUNC9:def 7;
hence thesis by
VALUED_1: 1;
end;
then
C5: (
ProjMap2 ((
Partial_Sums Rseq),k))
= ((
ProjMap2 ((
Partial_Sums Rseq),m1))
+ (
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),(m1
+ 1))));
(
ProjMap2 ((
Partial_Sums Rseq),m1)) is
convergent & (
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),(m1
+ 1))) is
convergent by
C3,
C0;
hence (
ProjMap2 ((
Partial_Sums Rseq),k)) is
convergent by
C5,
SEQ_2: 5;
end;
end;
for m be
Nat holds
P[m] from
NAT_1:sch 2(
C1,
C2);
hence (
ProjMap2 ((
Partial_Sums Rseq),m)) is
convergent;
end;
hence (
Partial_Sums Rseq) is
convergent_in_cod1;
end;
theorem ::
DBLSEQ_2:23
th01b: (
Partial_Sums Rseq) is
convergent_in_cod2 iff (
Partial_Sums_in_cod2 Rseq) is
convergent_in_cod2
proof
hereby
assume
A1: (
Partial_Sums Rseq) is
convergent_in_cod2;
now
let m be
Element of
NAT ;
defpred
P[
Nat] means for k be
Element of
NAT st k
= $1 holds (
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),k)) is
convergent;
now
let k be
Element of
NAT ;
assume k
=
0 ;
then (
ProjMap1 ((
Partial_Sums Rseq),k))
= (
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),k)) by
th00;
hence (
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),k)) is
convergent by
A1;
end;
then
A3:
P[
0 ];
A4: for m1 be
Nat st
P[m1] holds
P[(m1
+ 1)]
proof
let m1 be
Nat;
reconsider m = m1 as
Element of
NAT by
ORDINAL1:def 12;
assume
P[m1];
hereby
let k be
Element of
NAT ;
assume
B2: k
= (m1
+ 1);
then
reconsider k1 = (k
- 1) as
Element of
NAT by
NAT_1: 11,
NAT_1: 21;
B4: (
ProjMap1 ((
Partial_Sums Rseq),m)) is
convergent & (
ProjMap1 ((
Partial_Sums Rseq),k)) is
convergent by
A1;
now
let e be
Real;
assume
B6:
0
< e;
then
consider N1 be
Nat such that
B7: for n be
Nat st n
>= N1 holds
|.(((
ProjMap1 ((
Partial_Sums Rseq),m))
. n)
- (
lim (
ProjMap1 ((
Partial_Sums Rseq),m)))).|
< (e
/ 2) by
B4,
SEQ_2:def 7;
consider N2 be
Nat such that
B8: for n be
Nat st n
>= N2 holds
|.(((
ProjMap1 ((
Partial_Sums Rseq),k))
. n)
- (
lim (
ProjMap1 ((
Partial_Sums Rseq),k)))).|
< (e
/ 2) by
B4,
B6,
SEQ_2:def 7;
reconsider N = (
max (N1,N2)) as
Nat by
TARSKI: 1;
take N;
hereby
let n be
Nat;
assume
B9: n
>= N;
N
>= N1 & N
>= N2 by
XXREAL_0: 25;
then n
>= N1 & n
>= N2 by
B9,
XXREAL_0: 2;
then
|.(((
ProjMap1 ((
Partial_Sums Rseq),m))
. n)
- (
lim (
ProjMap1 ((
Partial_Sums Rseq),m)))).|
< (e
/ 2) &
|.(((
ProjMap1 ((
Partial_Sums Rseq),k))
. n)
- (
lim (
ProjMap1 ((
Partial_Sums Rseq),k)))).|
< (e
/ 2) by
B7,
B8;
then
B12: (
|.(((
ProjMap1 ((
Partial_Sums Rseq),m))
. n)
- (
lim (
ProjMap1 ((
Partial_Sums Rseq),m)))).|
+
|.(((
ProjMap1 ((
Partial_Sums Rseq),k))
. n)
- (
lim (
ProjMap1 ((
Partial_Sums Rseq),k)))).|)
< ((e
/ 2)
+ (e
/ 2)) by
XREAL_1: 8;
reconsider n1 = n as
Element of
NAT by
ORDINAL1:def 12;
((
ProjMap1 ((
Partial_Sums Rseq),k))
. n)
= ((
Partial_Sums Rseq)
. (k,n1)) by
MESFUNC9:def 6
.= ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. ((m
+ 1),n1)) by
B2,
th103a
.= (((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (m,n1))
+ ((
Partial_Sums_in_cod2 Rseq)
. ((m
+ 1),n1))) by
DefRS
.= (((
Partial_Sums Rseq)
. (m,n1))
+ ((
Partial_Sums_in_cod2 Rseq)
. (k,n1))) by
B2,
th103a
.= (((
ProjMap1 ((
Partial_Sums Rseq),m))
. n)
+ ((
Partial_Sums_in_cod2 Rseq)
. (k,n1))) by
MESFUNC9:def 6
.= (((
ProjMap1 ((
Partial_Sums Rseq),m))
. n)
+ ((
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),k))
. n)) by
MESFUNC9:def 6;
then
|.(((
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),k))
. n)
- ((
lim (
ProjMap1 ((
Partial_Sums Rseq),k)))
- (
lim (
ProjMap1 ((
Partial_Sums Rseq),m))))).|
=
|.((((
ProjMap1 ((
Partial_Sums Rseq),k))
. n)
- (
lim (
ProjMap1 ((
Partial_Sums Rseq),k))))
- (((
ProjMap1 ((
Partial_Sums Rseq),m))
. n)
- (
lim (
ProjMap1 ((
Partial_Sums Rseq),m))))).|;
then
|.(((
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),k))
. n)
- ((
lim (
ProjMap1 ((
Partial_Sums Rseq),k)))
- (
lim (
ProjMap1 ((
Partial_Sums Rseq),m))))).|
<= (
|.(((
ProjMap1 ((
Partial_Sums Rseq),k))
. n)
- (
lim (
ProjMap1 ((
Partial_Sums Rseq),k)))).|
+
|.(((
ProjMap1 ((
Partial_Sums Rseq),m))
. n)
- (
lim (
ProjMap1 ((
Partial_Sums Rseq),m)))).|) by
COMPLEX1: 57;
hence
|.(((
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),k))
. n)
- ((
lim (
ProjMap1 ((
Partial_Sums Rseq),k)))
- (
lim (
ProjMap1 ((
Partial_Sums Rseq),m))))).|
< e by
B12,
XXREAL_0: 2;
end;
end;
hence (
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),k)) is
convergent by
SEQ_2:def 6;
end;
end;
for m1 be
Nat holds
P[m1] from
NAT_1:sch 2(
A3,
A4);
hence (
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),m)) is
convergent;
end;
hence (
Partial_Sums_in_cod2 Rseq) is
convergent_in_cod2;
end;
assume
C0: (
Partial_Sums_in_cod2 Rseq) is
convergent_in_cod2;
now
let m be
Element of
NAT ;
defpred
P[
Nat] means for k be
Element of
NAT st k
= $1 holds (
ProjMap1 ((
Partial_Sums Rseq),k)) is
convergent;
(
ProjMap1 ((
Partial_Sums Rseq),
0 ))
= (
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),
0 )) by
th00;
then
C1:
P[
0 ] by
C0;
C2: for m be
Nat st
P[m] holds
P[(m
+ 1)]
proof
let m be
Nat;
assume
C3:
P[m];
reconsider m1 = m as
Element of
NAT by
ORDINAL1:def 12;
hereby
let k be
Element of
NAT ;
assume
C4: k
= (m
+ 1);
then
reconsider k1 = (k
- 1) as
Element of
NAT by
NAT_1: 11,
NAT_1: 21;
for n be
Element of
NAT holds ((
ProjMap1 ((
Partial_Sums Rseq),k))
. n)
= (((
ProjMap1 ((
Partial_Sums Rseq),m1))
+ (
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),(m1
+ 1))))
. n)
proof
let n be
Element of
NAT ;
((
ProjMap1 ((
Partial_Sums Rseq),k))
. n)
= ((
Partial_Sums Rseq)
. ((m1
+ 1),n)) by
C4,
MESFUNC9:def 6
.= (((
Partial_Sums_in_cod2 Rseq)
. ((m1
+ 1),n))
+ ((
Partial_Sums_in_cod2 (
Partial_Sums_in_cod1 Rseq))
. (m1,n))) by
ThRS
.= (((
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),(m1
+ 1)))
. n)
+ ((
Partial_Sums Rseq)
. (m1,n))) by
MESFUNC9:def 6
.= (((
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),(m1
+ 1)))
. n)
+ ((
ProjMap1 ((
Partial_Sums Rseq),m1))
. n)) by
MESFUNC9:def 6;
hence thesis by
VALUED_1: 1;
end;
then
C5: (
ProjMap1 ((
Partial_Sums Rseq),k))
= ((
ProjMap1 ((
Partial_Sums Rseq),m1))
+ (
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),(m1
+ 1))));
(
ProjMap1 ((
Partial_Sums Rseq),m1)) is
convergent & (
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),(m1
+ 1))) is
convergent by
C3,
C0;
hence (
ProjMap1 ((
Partial_Sums Rseq),k)) is
convergent by
C5,
SEQ_2: 5;
end;
end;
for m be
Nat holds
P[m] from
NAT_1:sch 2(
C1,
C2);
hence (
ProjMap1 ((
Partial_Sums Rseq),m)) is
convergent;
end;
hence (
Partial_Sums Rseq) is
convergent_in_cod2;
end;
theorem ::
DBLSEQ_2:24
th02a: (
Partial_Sums Rseq) is
convergent_in_cod1 implies for k be
Nat holds ((
lim_in_cod1 (
Partial_Sums Rseq))
. (k
+ 1))
= (((
lim_in_cod1 (
Partial_Sums Rseq))
. k)
+ ((
lim_in_cod1 (
Partial_Sums_in_cod1 Rseq))
. (k
+ 1)))
proof
assume
A1: (
Partial_Sums Rseq) is
convergent_in_cod1;
let k be
Nat;
reconsider k1 = k as
Element of
NAT by
ORDINAL1:def 12;
(
Partial_Sums_in_cod1 Rseq) is
convergent_in_cod1 by
A1,
th01a;
then
A2: (
ProjMap2 ((
Partial_Sums Rseq),k1)) is
convergent & (
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),(k1
+ 1))) is
convergent by
A1;
A3: ((
lim_in_cod1 (
Partial_Sums Rseq))
. (k
+ 1))
= (
lim (
ProjMap2 ((
Partial_Sums Rseq),(k1
+ 1)))) by
DBLSEQ_1:def 5;
A4: ((
lim_in_cod1 (
Partial_Sums Rseq))
. k)
= (
lim (
ProjMap2 ((
Partial_Sums Rseq),k1))) & ((
lim_in_cod1 (
Partial_Sums_in_cod1 Rseq))
. (k
+ 1))
= (
lim (
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),(k1
+ 1)))) by
DBLSEQ_1:def 5;
now
let j be
Element of
NAT ;
B1: ((
ProjMap2 ((
Partial_Sums Rseq),k1))
. j)
= ((
Partial_Sums_in_cod2 (
Partial_Sums_in_cod1 Rseq))
. (j,k1)) by
MESFUNC9:def 7;
((
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),(k1
+ 1)))
. j)
= ((
Partial_Sums_in_cod1 Rseq)
. (j,(k1
+ 1))) by
MESFUNC9:def 7;
then (((
ProjMap2 ((
Partial_Sums Rseq),k1))
. j)
+ ((
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),(k1
+ 1)))
. j))
= ((
Partial_Sums_in_cod2 (
Partial_Sums_in_cod1 Rseq))
. (j,(k1
+ 1))) by
B1,
DefCS
.= ((
ProjMap2 ((
Partial_Sums Rseq),(k1
+ 1)))
. j) by
MESFUNC9:def 7;
hence ((
ProjMap2 ((
Partial_Sums Rseq),(k1
+ 1)))
. j)
= (((
ProjMap2 ((
Partial_Sums Rseq),k1))
+ (
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),(k1
+ 1))))
. j) by
VALUED_1: 1;
end;
then (
ProjMap2 ((
Partial_Sums Rseq),(k1
+ 1)))
= ((
ProjMap2 ((
Partial_Sums Rseq),k1))
+ (
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),(k1
+ 1))));
hence thesis by
A3,
A4,
A2,
SEQ_2: 6;
end;
theorem ::
DBLSEQ_2:25
th02b: (
Partial_Sums Rseq) is
convergent_in_cod2 implies for k be
Nat holds ((
lim_in_cod2 (
Partial_Sums Rseq))
. (k
+ 1))
= (((
lim_in_cod2 (
Partial_Sums Rseq))
. k)
+ ((
lim_in_cod2 (
Partial_Sums_in_cod2 Rseq))
. (k
+ 1)))
proof
assume
A1: (
Partial_Sums Rseq) is
convergent_in_cod2;
let k be
Nat;
reconsider k1 = k as
Element of
NAT by
ORDINAL1:def 12;
(
Partial_Sums_in_cod2 Rseq) is
convergent_in_cod2 by
A1,
th01b;
then
A2: (
ProjMap1 ((
Partial_Sums Rseq),k1)) is
convergent & (
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),(k1
+ 1))) is
convergent by
A1;
A3: ((
lim_in_cod2 (
Partial_Sums Rseq))
. (k
+ 1))
= (
lim (
ProjMap1 ((
Partial_Sums Rseq),(k1
+ 1)))) by
DBLSEQ_1:def 6;
A4: ((
lim_in_cod2 (
Partial_Sums Rseq))
. k)
= (
lim (
ProjMap1 ((
Partial_Sums Rseq),k1))) & ((
lim_in_cod2 (
Partial_Sums_in_cod2 Rseq))
. (k
+ 1))
= (
lim (
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),(k1
+ 1)))) by
DBLSEQ_1:def 6;
now
let j be
Element of
NAT ;
B1: ((
ProjMap1 ((
Partial_Sums Rseq),k1))
. j)
= ((
Partial_Sums Rseq)
. (k1,j)) by
MESFUNC9:def 6
.= ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (k1,j)) by
th103a;
((
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),(k1
+ 1)))
. j)
= ((
Partial_Sums_in_cod2 Rseq)
. ((k1
+ 1),j)) by
MESFUNC9:def 6;
then (((
ProjMap1 ((
Partial_Sums Rseq),k1))
. j)
+ ((
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),(k1
+ 1)))
. j))
= ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. ((k1
+ 1),j)) by
B1,
DefRS
.= ((
Partial_Sums Rseq)
. ((k1
+ 1),j)) by
th103a
.= ((
ProjMap1 ((
Partial_Sums Rseq),(k1
+ 1)))
. j) by
MESFUNC9:def 6;
hence ((
ProjMap1 ((
Partial_Sums Rseq),(k1
+ 1)))
. j)
= (((
ProjMap1 ((
Partial_Sums Rseq),k1))
+ (
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),(k1
+ 1))))
. j) by
VALUED_1: 1;
end;
then (
ProjMap1 ((
Partial_Sums Rseq),(k1
+ 1)))
= ((
ProjMap1 ((
Partial_Sums Rseq),k1))
+ (
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),(k1
+ 1))));
hence thesis by
A3,
A4,
A2,
SEQ_2: 6;
end;
theorem ::
DBLSEQ_2:26
th03a: (
Partial_Sums Rseq) is
convergent_in_cod1 implies (
lim_in_cod1 (
Partial_Sums Rseq))
= (
Partial_Sums (
lim_in_cod1 (
Partial_Sums_in_cod1 Rseq)))
proof
assume
AS: (
Partial_Sums Rseq) is
convergent_in_cod1;
now
let m be
Nat;
reconsider m1 = m as
Element of
NAT by
ORDINAL1:def 12;
defpred
P[
Nat] means ((
Partial_Sums (
lim_in_cod1 (
Partial_Sums_in_cod1 Rseq)))
. $1)
= ((
lim_in_cod1 (
Partial_Sums Rseq))
. $1);
((
Partial_Sums (
lim_in_cod1 (
Partial_Sums_in_cod1 Rseq)))
.
0 )
= ((
lim_in_cod1 (
Partial_Sums_in_cod1 Rseq))
.
0 ) by
SERIES_1:def 1
.= (
lim (
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),
0 ))) by
DBLSEQ_1:def 5
.= (
lim (
ProjMap2 ((
Partial_Sums Rseq),
0 ))) by
th00
.= ((
lim_in_cod1 (
Partial_Sums Rseq))
.
0 ) by
DBLSEQ_1:def 5;
then
A1:
P[
0 ];
A2: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat;
assume
A3:
P[k];
reconsider k1 = k as
Element of
NAT by
ORDINAL1:def 12;
((
Partial_Sums (
lim_in_cod1 (
Partial_Sums_in_cod1 Rseq)))
. (k
+ 1))
= (((
lim_in_cod1 (
Partial_Sums Rseq))
. k)
+ ((
lim_in_cod1 (
Partial_Sums_in_cod1 Rseq))
. (k
+ 1))) by
A3,
SERIES_1:def 1;
hence thesis by
AS,
th02a;
end;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
A1,
A2);
hence ((
lim_in_cod1 (
Partial_Sums Rseq))
. m)
= ((
Partial_Sums (
lim_in_cod1 (
Partial_Sums_in_cod1 Rseq)))
. m);
end;
hence thesis;
end;
theorem ::
DBLSEQ_2:27
th03b: (
Partial_Sums Rseq) is
convergent_in_cod2 implies (
lim_in_cod2 (
Partial_Sums Rseq))
= (
Partial_Sums (
lim_in_cod2 (
Partial_Sums_in_cod2 Rseq)))
proof
assume
AS: (
Partial_Sums Rseq) is
convergent_in_cod2;
now
let n be
Nat;
reconsider n1 = n as
Element of
NAT by
ORDINAL1:def 12;
defpred
P[
Nat] means ((
Partial_Sums (
lim_in_cod2 (
Partial_Sums_in_cod2 Rseq)))
. $1)
= ((
lim_in_cod2 (
Partial_Sums Rseq))
. $1);
((
Partial_Sums (
lim_in_cod2 (
Partial_Sums_in_cod2 Rseq)))
.
0 )
= ((
lim_in_cod2 (
Partial_Sums_in_cod2 Rseq))
.
0 ) by
SERIES_1:def 1
.= (
lim (
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),
0 ))) by
DBLSEQ_1:def 6
.= (
lim (
ProjMap1 ((
Partial_Sums Rseq),
0 ))) by
th00
.= ((
lim_in_cod2 (
Partial_Sums Rseq))
.
0 ) by
DBLSEQ_1:def 6;
then
A1:
P[
0 ];
A2: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat;
assume
A3:
P[k];
reconsider k1 = k as
Element of
NAT by
ORDINAL1:def 12;
((
Partial_Sums (
lim_in_cod2 (
Partial_Sums_in_cod2 Rseq)))
. (k
+ 1))
= (((
lim_in_cod2 (
Partial_Sums Rseq))
. k)
+ ((
lim_in_cod2 (
Partial_Sums_in_cod2 Rseq))
. (k
+ 1))) by
A3,
SERIES_1:def 1;
hence thesis by
AS,
th02b;
end;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
A1,
A2);
hence ((
lim_in_cod2 (
Partial_Sums Rseq))
. n)
= ((
Partial_Sums (
lim_in_cod2 (
Partial_Sums_in_cod2 Rseq)))
. n);
end;
hence thesis;
end;
begin
theorem ::
DBLSEQ_2:28
lm80: Rseq is
nonnegative-yielding implies (
Partial_Sums_in_cod2 Rseq) is
nonnegative-yielding & (
Partial_Sums_in_cod1 Rseq) is
nonnegative-yielding
proof
assume
a1: Rseq is
nonnegative-yielding;
now
let i,j be
Nat;
defpred
C[
Nat] means ((
Partial_Sums_in_cod2 Rseq)
. (i,$1))
>=
0 ;
((
Partial_Sums_in_cod2 Rseq)
. (i,
0 ))
= (Rseq
. (i,
0 )) by
DefCS;
then
a2:
C[
0 ] by
a1;
a3: for k be
Nat st
C[k] holds
C[(k
+ 1)]
proof
let k be
Nat;
assume
C[k];
then
a4: ((
Partial_Sums_in_cod2 Rseq)
. (i,k))
>=
0 & (Rseq
. (i,(k
+ 1)))
>=
0 by
a1;
((
Partial_Sums_in_cod2 Rseq)
. (i,(k
+ 1)))
= (((
Partial_Sums_in_cod2 Rseq)
. (i,k))
+ (Rseq
. (i,(k
+ 1)))) by
DefCS;
hence
C[(k
+ 1)] by
a4;
end;
for k be
Nat holds
C[k] from
NAT_1:sch 2(
a2,
a3);
hence ((
Partial_Sums_in_cod2 Rseq)
. (i,j))
>=
0 ;
defpred
R[
Nat] means ((
Partial_Sums_in_cod1 Rseq)
. ($1,j))
>=
0 ;
((
Partial_Sums_in_cod1 Rseq)
. (
0 ,j))
= (Rseq
. (
0 ,j)) by
DefRS;
then
a5:
R[
0 ] by
a1;
a6: for k be
Nat st
R[k] holds
R[(k
+ 1)]
proof
let k be
Nat;
assume
R[k];
then
a7: ((
Partial_Sums_in_cod1 Rseq)
. (k,j))
>=
0 & (Rseq
. ((k
+ 1),j))
>=
0 by
a1;
((
Partial_Sums_in_cod1 Rseq)
. ((k
+ 1),j))
= (((
Partial_Sums_in_cod1 Rseq)
. (k,j))
+ (Rseq
. ((k
+ 1),j))) by
DefRS;
hence
R[(k
+ 1)] by
a7;
end;
for k be
Nat holds
R[k] from
NAT_1:sch 2(
a5,
a6);
hence ((
Partial_Sums_in_cod1 Rseq)
. (i,j))
>=
0 ;
end;
hence thesis;
end;
theorem ::
DBLSEQ_2:29
th80a: Rseq is
nonnegative-yielding implies (
Partial_Sums Rseq) is
non-decreasing
proof
set CPS = (
Partial_Sums Rseq);
assume
a1: Rseq is
nonnegative-yielding;
now
let n1,m1,n2,m2 be
Nat;
assume
b2: n1
>= n2 & m1
>= m2;
then
consider dn be
Nat such that
b3: n1
= (n2
+ dn) by
NAT_1: 10;
consider dm be
Nat such that
b4: m1
= (m2
+ dm) by
b2,
NAT_1: 10;
reconsider dn, dm as
Element of
NAT by
ORDINAL1:def 12;
defpred
P1[
Nat] means (CPS
. ((n2
+ $1),m2))
>= (CPS
. (n2,m2));
b5:
P1[
0 ];
b6: for k be
Nat st
P1[k] holds
P1[(k
+ 1)]
proof
let k be
Nat;
assume
a7:
P1[k];
b8: (CPS
. (((n2
+ k)
+ 1),m2))
= (((
Partial_Sums_in_cod2 Rseq)
. (((n2
+ k)
+ 1),m2))
+ (CPS
. ((n2
+ k),m2))) by
ThRS;
(
Partial_Sums_in_cod2 Rseq) is
nonnegative-yielding by
a1,
lm80;
then (CPS
. (((n2
+ k)
+ 1),m2))
>= (CPS
. ((n2
+ k),m2)) by
b8,
XREAL_1: 31;
hence
P1[(k
+ 1)] by
a7,
XXREAL_0: 2;
end;
for k be
Nat holds
P1[k] from
NAT_1:sch 2(
b5,
b6);
then
b9: (CPS
. (n1,m2))
>= (CPS
. (n2,m2)) by
b3;
defpred
P2[
Nat] means (CPS
. (n1,(m2
+ $1)))
>= (CPS
. (n1,m2));
b10:
P2[
0 ];
b11: for k be
Nat st
P2[k] holds
P2[(k
+ 1)]
proof
let k be
Nat;
assume
b12:
P2[k];
b13: (CPS
. (n1,((m2
+ k)
+ 1)))
= (((
Partial_Sums_in_cod1 Rseq)
. (n1,((m2
+ k)
+ 1)))
+ (CPS
. (n1,(m2
+ k)))) by
DefCS;
(
Partial_Sums_in_cod1 Rseq) is
nonnegative-yielding by
a1,
lm80;
then (CPS
. (n1,((m2
+ k)
+ 1)))
>= (CPS
. (n1,(m2
+ k))) by
b13,
XREAL_1: 31;
hence
P2[(k
+ 1)] by
b12,
XXREAL_0: 2;
end;
for k be
Nat holds
P2[k] from
NAT_1:sch 2(
b10,
b11);
then (CPS
. (n1,m1))
>= (CPS
. (n1,m2)) by
b4;
hence (CPS
. (n1,m1))
>= (CPS
. (n2,m2)) by
b9,
XXREAL_0: 2;
end;
hence (
Partial_Sums Rseq) is
non-decreasing;
end;
theorem ::
DBLSEQ_2:30
Rseq is
nonnegative-yielding implies ((
Partial_Sums Rseq) is
P-convergent iff (
Partial_Sums Rseq) is
bounded_below
bounded_above)
proof
assume Rseq is
nonnegative-yielding;
then
a2: (
Partial_Sums Rseq) is
non-decreasing by
th80a;
hence (
Partial_Sums Rseq) is
P-convergent implies (
Partial_Sums Rseq) is
bounded_below
bounded_above;
assume (
Partial_Sums Rseq) is
bounded_below
bounded_above;
hence (
Partial_Sums Rseq) is
P-convergent by
a2;
end;
theorem ::
DBLSEQ_2:31
lm84a: (for n,m be
Nat holds (Rseq1
. (n,m))
<= (Rseq2
. (n,m))) implies for i,j be
Nat holds ((
Partial_Sums_in_cod1 Rseq1)
. (i,j))
<= ((
Partial_Sums_in_cod1 Rseq2)
. (i,j)) & ((
Partial_Sums_in_cod2 Rseq1)
. (i,j))
<= ((
Partial_Sums_in_cod2 Rseq2)
. (i,j))
proof
set RS1 = (
Partial_Sums_in_cod1 Rseq1), RS2 = (
Partial_Sums_in_cod1 Rseq2);
set CS1 = (
Partial_Sums_in_cod2 Rseq1), CS2 = (
Partial_Sums_in_cod2 Rseq2);
assume
a1: for n,m be
Nat holds (Rseq1
. (n,m))
<= (Rseq2
. (n,m));
let i,j be
Nat;
defpred
R[
Nat] means (RS1
. ($1,j))
<= (RS2
. ($1,j));
(RS1
. (
0 ,j))
= (Rseq1
. (
0 ,j)) & (RS2
. (
0 ,j))
= (Rseq2
. (
0 ,j)) by
DefRS;
then
a2:
R[
0 ] by
a1;
a3: for k be
Nat st
R[k] holds
R[(k
+ 1)]
proof
let k be
Nat;
assume
R[k];
then
a4: (RS1
. (k,j))
<= (RS2
. (k,j)) & (Rseq1
. ((k
+ 1),j))
<= (Rseq2
. ((k
+ 1),j)) by
a1;
(RS1
. ((k
+ 1),j))
= ((RS1
. (k,j))
+ (Rseq1
. ((k
+ 1),j))) & (RS2
. ((k
+ 1),j))
= ((RS2
. (k,j))
+ (Rseq2
. ((k
+ 1),j))) by
DefRS;
hence
R[(k
+ 1)] by
a4,
XREAL_1: 7;
end;
for k be
Nat holds
R[k] from
NAT_1:sch 2(
a2,
a3);
hence (RS1
. (i,j))
<= (RS2
. (i,j));
defpred
C[
Nat] means (CS1
. (i,$1))
<= (CS2
. (i,$1));
(CS1
. (i,
0 ))
= (Rseq1
. (i,
0 )) & (CS2
. (i,
0 ))
= (Rseq2
. (i,
0 )) by
DefCS;
then
a5:
C[
0 ] by
a1;
a6: for k be
Nat st
C[k] holds
C[(k
+ 1)]
proof
let k be
Nat;
assume
C[k];
then
a7: (CS1
. (i,k))
<= (CS2
. (i,k)) & (Rseq1
. (i,(k
+ 1)))
<= (Rseq2
. (i,(k
+ 1))) by
a1;
(CS1
. (i,(k
+ 1)))
= ((CS1
. (i,k))
+ (Rseq1
. (i,(k
+ 1)))) & (CS2
. (i,(k
+ 1)))
= ((CS2
. (i,k))
+ (Rseq2
. (i,(k
+ 1)))) by
DefCS;
hence
C[(k
+ 1)] by
a7,
XREAL_1: 7;
end;
for k be
Nat holds
C[k] from
NAT_1:sch 2(
a5,
a6);
hence (CS1
. (i,j))
<= (CS2
. (i,j));
end;
theorem ::
DBLSEQ_2:32
lm84: Rseq1 is
nonnegative-yielding & (for n,m be
Nat holds (Rseq1
. (n,m))
<= (Rseq2
. (n,m))) implies for i,j be
Nat holds ((
Partial_Sums Rseq1)
. (i,j))
<= ((
Partial_Sums Rseq2)
. (i,j))
proof
set RPS1 = (
Partial_Sums Rseq1);
set RPS2 = (
Partial_Sums Rseq2);
assume
a1: Rseq1 is
nonnegative-yielding & for n,m be
Nat holds (Rseq1
. (n,m))
<= (Rseq2
. (n,m));
let i,j be
Nat;
defpred
P[
Nat] means (RPS1
. (i,$1))
<= (RPS2
. (i,$1));
a2:
P[
0 ]
proof
defpred
Q0[
Nat] means (RPS1
. ($1,
0 ))
<= (RPS2
. ($1,
0 ));
a3: (RPS1
. (
0 ,
0 ))
= ((
Partial_Sums_in_cod1 Rseq1)
. (
0 ,
0 )) by
DefCS
.= (Rseq1
. (
0 ,
0 )) by
DefRS;
(RPS2
. (
0 ,
0 ))
= ((
Partial_Sums_in_cod1 Rseq2)
. (
0 ,
0 )) by
DefCS
.= (Rseq2
. (
0 ,
0 )) by
DefRS;
then
a4:
Q0[
0 ] by
a1,
a3;
a5: for l be
Nat st
Q0[l] holds
Q0[(l
+ 1)]
proof
let l be
Nat;
assume
Q0[l];
(RPS1
. ((l
+ 1),
0 ))
= ((
Partial_Sums_in_cod1 Rseq1)
. ((l
+ 1),
0 )) & (RPS2
. ((l
+ 1),
0 ))
= ((
Partial_Sums_in_cod1 Rseq2)
. ((l
+ 1),
0 )) by
DefCS;
hence
Q0[(l
+ 1)] by
a1,
lm84a;
end;
for l be
Nat holds
Q0[l] from
NAT_1:sch 2(
a4,
a5);
hence
P[
0 ];
end;
a8: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat;
assume
A9:
P[k];
a10: ((
Partial_Sums_in_cod1 Rseq1)
. (i,(k
+ 1)))
<= ((
Partial_Sums_in_cod1 Rseq2)
. (i,(k
+ 1))) by
a1,
lm84a;
(RPS1
. (i,(k
+ 1)))
= (((
Partial_Sums_in_cod1 Rseq1)
. (i,(k
+ 1)))
+ (RPS1
. (i,k))) by
DefCS;
then (RPS1
. (i,(k
+ 1)))
<= (((
Partial_Sums_in_cod1 Rseq2)
. (i,(k
+ 1)))
+ (RPS2
. (i,k))) by
A9,
a10,
XREAL_1: 7;
hence
P[(k
+ 1)] by
DefCS;
end;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
a2,
a8);
hence (RPS1
. (i,j))
<= (RPS2
. (i,j));
end;
theorem ::
DBLSEQ_2:33
Rseq1 is
nonnegative-yielding & (for n,m be
Nat holds (Rseq1
. (n,m))
<= (Rseq2
. (n,m))) & (
Partial_Sums Rseq2) is
P-convergent implies (
Partial_Sums Rseq1) is
P-convergent
proof
set RPS1 = (
Partial_Sums Rseq1);
set RPS2 = (
Partial_Sums Rseq2);
assume that
a2: Rseq1 is
nonnegative-yielding & for n,m be
Nat holds (Rseq1
. (n,m))
<= (Rseq2
. (n,m)) and
a1: RPS2 is
P-convergent;
for n,m be
Nat holds
0
<= (Rseq2
. (n,m))
proof
let n,m be
Nat;
0
<= (Rseq1
. (n,m)) & (Rseq1
. (n,m))
<= (Rseq2
. (n,m)) by
a2;
hence
0
<= (Rseq2
. (n,m));
end;
then Rseq2 is
nonnegative-yielding;
then RPS2 is
non-decreasing by
th80a;
then RPS2 is
bounded_above by
a1;
then
consider M be
Real such that
a3: M is
UpperBound of (RPS2
.:
[:
NAT ,
NAT :]) by
XXREAL_2:def 10;
now
let a be
ExtReal;
assume a
in (RPS1
.:
[:
NAT ,
NAT :]);
then
consider x be
Element of
[:
NAT ,
NAT :] such that
a5: x
in
[:
NAT ,
NAT :] & a
= (RPS1
. x) by
FUNCT_2: 65;
consider n,m be
object such that
a6: n
in
NAT & m
in
NAT & x
=
[n, m] by
ZFMISC_1:def 2;
reconsider n, m as
Element of
NAT by
a6;
a7: (RPS1
. (n,m))
<= (RPS2
. (n,m)) by
a2,
lm84;
(RPS2
. (n,m))
<= M by
a3,
XXREAL_2:def 1,
a6,
FUNCT_2: 35;
hence a
<= M by
a5,
a6,
a7,
XXREAL_0: 2;
end;
then M is
UpperBound of (RPS1
.:
[:
NAT ,
NAT :]) by
XXREAL_2:def 1;
then
a8: RPS1 is
bounded_above by
XXREAL_2:def 10;
RPS1 is
non-decreasing by
a2,
th80a;
hence RPS1 is
P-convergent by
a8;
end;
theorem ::
DBLSEQ_2:34
th101: for rseq be
Real_Sequence, m be
Nat st rseq is
nonnegative holds (rseq
. m)
<= ((
Partial_Sums rseq)
. m)
proof
let rseq be
Real_Sequence, m be
Nat;
assume
A1: rseq is
nonnegative;
defpred
P[
Nat] means (rseq
. $1)
<= ((
Partial_Sums rseq)
. $1);
a3:
P[
0 ] by
SERIES_1:def 1;
a4: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat;
assume
P[k];
((
Partial_Sums rseq)
. (k
+ 1))
= (((
Partial_Sums rseq)
. k)
+ (rseq
. (k
+ 1))) by
SERIES_1:def 1;
hence
P[(k
+ 1)] by
XREAL_1: 31,
SERIES_3: 34,
A1;
end;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
a3,
a4);
hence (rseq
. m)
<= ((
Partial_Sums rseq)
. m);
end;
theorem ::
DBLSEQ_2:35
Rseq is
nonnegative-yielding implies (for m,n be
Nat holds (Rseq
. (m,n))
<= ((
Partial_Sums_in_cod1 Rseq)
. (m,n)) & (Rseq
. (m,n))
<= ((
Partial_Sums_in_cod2 Rseq)
. (m,n)))
proof
assume
a1: Rseq is
nonnegative-yielding;
hereby
let m1,n1 be
Nat;
reconsider m = m1, n = n1 as
Element of
NAT by
ORDINAL1:def 12;
now
let j be
Nat;
j
in
NAT by
ORDINAL1:def 12;
then ((
ProjMap2 (Rseq,n))
. j)
= (Rseq
. (j,n)) by
MESFUNC9:def 7;
hence ((
ProjMap2 (Rseq,n))
. j)
>=
0 by
a1;
end;
then ((
ProjMap2 (Rseq,n))
. m)
<= ((
Partial_Sums (
ProjMap2 (Rseq,n)))
. m) by
th101,
RINFSUP1:def 3;
then ((
ProjMap2 (Rseq,n))
. m)
<= ((
Partial_Sums_in_cod1 Rseq)
. (m,n)) by
th100;
hence (Rseq
. (m1,n1))
<= ((
Partial_Sums_in_cod1 Rseq)
. (m1,n1)) by
MESFUNC9:def 7;
now
let j be
Nat;
j
in
NAT by
ORDINAL1:def 12;
then ((
ProjMap1 (Rseq,m))
. j)
= (Rseq
. (m,j)) by
MESFUNC9:def 6;
hence ((
ProjMap1 (Rseq,m))
. j)
>=
0 by
a1;
end;
then (
ProjMap1 (Rseq,m)) is
nonnegative-yielding;
then ((
ProjMap1 (Rseq,m))
. n)
<= ((
Partial_Sums (
ProjMap1 (Rseq,m)))
. n) by
th101;
then ((
ProjMap1 (Rseq,m))
. n)
<= ((
Partial_Sums_in_cod2 Rseq)
. (m,n)) by
th100;
hence (Rseq
. (m1,n1))
<= ((
Partial_Sums_in_cod2 Rseq)
. (m1,n1)) by
MESFUNC9:def 6;
end;
end;
theorem ::
DBLSEQ_2:36
th1003: Rseq is
nonnegative-yielding implies (for i1,i2,j be
Nat st i1
<= i2 holds ((
Partial_Sums_in_cod1 Rseq)
. (i1,j))
<= ((
Partial_Sums_in_cod1 Rseq)
. (i2,j))) & (for i,j1,j2 be
Nat st j1
<= j2 holds ((
Partial_Sums_in_cod2 Rseq)
. (i,j1))
<= ((
Partial_Sums_in_cod2 Rseq)
. (i,j2)))
proof
assume
A1: Rseq is
nonnegative-yielding;
A2:
now
let i1,i2,j be
natural
number;
assume i1
<= i2;
then
consider k be
Nat such that
A3: i2
= (i1
+ k) by
NAT_1: 10;
defpred
P[
Nat] means $1
<= k implies ((
Partial_Sums_in_cod1 Rseq)
. (i1,j))
<= ((
Partial_Sums_in_cod1 Rseq)
. ((i1
+ $1),j));
A4:
P[
0 ];
A5: for l be
Nat st
P[l] holds
P[(l
+ 1)]
proof
let l be
Nat;
assume
A6:
P[l];
now
assume
A7: (l
+ 1)
<= k;
((
Partial_Sums_in_cod1 Rseq)
. (((i1
+ l)
+ 1),j))
= (((
Partial_Sums_in_cod1 Rseq)
. ((i1
+ l),j))
+ (Rseq
. (((i1
+ l)
+ 1),j))) by
DefRS;
then ((
Partial_Sums_in_cod1 Rseq)
. ((i1
+ l),j))
<= ((
Partial_Sums_in_cod1 Rseq)
. (((i1
+ l)
+ 1),j)) by
A1,
XREAL_1: 31;
hence ((
Partial_Sums_in_cod1 Rseq)
. (i1,j))
<= ((
Partial_Sums_in_cod1 Rseq)
. ((i1
+ (l
+ 1)),j)) by
A6,
A7,
NAT_1: 13,
XXREAL_0: 2;
end;
hence
P[(l
+ 1)];
end;
for l be
Nat holds
P[l] from
NAT_1:sch 2(
A4,
A5);
hence ((
Partial_Sums_in_cod1 Rseq)
. (i1,j))
<= ((
Partial_Sums_in_cod1 Rseq)
. (i2,j)) by
A3;
end;
now
let i,j1,j2 be
natural
number;
assume j1
<= j2;
then
consider k be
Nat such that
B3: j2
= (j1
+ k) by
NAT_1: 10;
defpred
P[
Nat] means $1
<= k implies ((
Partial_Sums_in_cod2 Rseq)
. (i,j1))
<= ((
Partial_Sums_in_cod2 Rseq)
. (i,(j1
+ $1)));
B4:
P[
0 ];
B5: for l be
Nat st
P[l] holds
P[(l
+ 1)]
proof
let l be
Nat;
assume
B6:
P[l];
now
assume
B7: (l
+ 1)
<= k;
((
Partial_Sums_in_cod2 Rseq)
. (i,((j1
+ l)
+ 1)))
= (((
Partial_Sums_in_cod2 Rseq)
. (i,(j1
+ l)))
+ (Rseq
. (i,((j1
+ l)
+ 1)))) by
DefCS;
then ((
Partial_Sums_in_cod2 Rseq)
. (i,(j1
+ l)))
<= ((
Partial_Sums_in_cod2 Rseq)
. (i,((j1
+ l)
+ 1))) by
A1,
XREAL_1: 31;
hence ((
Partial_Sums_in_cod2 Rseq)
. (i,j1))
<= ((
Partial_Sums_in_cod2 Rseq)
. (i,(j1
+ (l
+ 1)))) by
B6,
B7,
NAT_1: 13,
XXREAL_0: 2;
end;
hence
P[(l
+ 1)];
end;
for l be
Nat holds
P[l] from
NAT_1:sch 2(
B4,
B5);
hence ((
Partial_Sums_in_cod2 Rseq)
. (i,j1))
<= ((
Partial_Sums_in_cod2 Rseq)
. (i,j2)) by
B3;
end;
hence thesis by
A2;
end;
theorem ::
DBLSEQ_2:37
th105: Rseq is
nonnegative-yielding implies (for i1,i2,j be
Nat st i1
<= i2 holds ((
Partial_Sums Rseq)
. (i1,j))
<= ((
Partial_Sums Rseq)
. (i2,j))) & (for i,j1,j2 be
Nat st j1
<= j2 holds ((
Partial_Sums Rseq)
. (i,j1))
<= ((
Partial_Sums Rseq)
. (i,j2)))
proof
assume
A1: Rseq is
nonnegative-yielding;
hereby
let i1,i2,j be
Nat;
assume
A3: i1
<= i2;
defpred
P[
Nat] means ((
Partial_Sums Rseq)
. (i1,$1))
<= ((
Partial_Sums Rseq)
. (i2,$1));
((
Partial_Sums Rseq)
. (i1,
0 ))
= ((
Partial_Sums_in_cod1 Rseq)
. (i1,
0 )) & ((
Partial_Sums Rseq)
. (i2,
0 ))
= ((
Partial_Sums_in_cod1 Rseq)
. (i2,
0 )) by
DefCS;
then
A4:
P[
0 ] by
A3,
A1,
th1003;
A5: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat;
assume
A6:
P[k];
A7: ((
Partial_Sums_in_cod1 Rseq)
. (i1,(k
+ 1)))
<= ((
Partial_Sums_in_cod1 Rseq)
. (i2,(k
+ 1))) by
A3,
A1,
th1003;
((
Partial_Sums Rseq)
. (i1,(k
+ 1)))
= (((
Partial_Sums Rseq)
. (i1,k))
+ ((
Partial_Sums_in_cod1 Rseq)
. (i1,(k
+ 1)))) & ((
Partial_Sums Rseq)
. (i2,(k
+ 1)))
= (((
Partial_Sums Rseq)
. (i2,k))
+ ((
Partial_Sums_in_cod1 Rseq)
. (i2,(k
+ 1)))) by
DefCS;
hence thesis by
A6,
A7,
XREAL_1: 7;
end;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
A4,
A5);
hence ((
Partial_Sums Rseq)
. (i1,j))
<= ((
Partial_Sums Rseq)
. (i2,j));
end;
hereby
let i,j1,j2 be
Nat;
assume
B3: j1
<= j2;
defpred
Q[
Nat] means ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. ($1,j1))
<= ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. ($1,j2));
((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (
0 ,j1))
= ((
Partial_Sums_in_cod2 Rseq)
. (
0 ,j1)) & ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (
0 ,j2))
= ((
Partial_Sums_in_cod2 Rseq)
. (
0 ,j2)) by
DefRS;
then
B4:
Q[
0 ] by
B3,
A1,
th1003;
B5: for k be
Nat st
Q[k] holds
Q[(k
+ 1)]
proof
let k be
Nat;
assume
C6:
Q[k];
C7: ((
Partial_Sums_in_cod2 Rseq)
. ((k
+ 1),j1))
<= ((
Partial_Sums_in_cod2 Rseq)
. ((k
+ 1),j2)) by
B3,
A1,
th1003;
((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. ((k
+ 1),j1))
= (((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (k,j1))
+ ((
Partial_Sums_in_cod2 Rseq)
. ((k
+ 1),j1))) & ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. ((k
+ 1),j2))
= (((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (k,j2))
+ ((
Partial_Sums_in_cod2 Rseq)
. ((k
+ 1),j2))) by
DefRS;
hence thesis by
C6,
C7,
XREAL_1: 7;
end;
B6: for k be
Nat holds
Q[k] from
NAT_1:sch 2(
B4,
B5);
((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (i,j1))
= ((
Partial_Sums Rseq)
. (i,j1)) & ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (i,j2))
= ((
Partial_Sums Rseq)
. (i,j2)) by
th103;
hence ((
Partial_Sums Rseq)
. (i,j1))
<= ((
Partial_Sums Rseq)
. (i,j2)) by
B6;
end;
end;
theorem ::
DBLSEQ_2:38
Rseq is
nonnegative-yielding implies (for i1,i2,j1,j2 be
Nat st i1
<= i2 & j1
<= j2 holds ((
Partial_Sums Rseq)
. (i1,j1))
<= ((
Partial_Sums Rseq)
. (i2,j2)))
proof
assume
A1: Rseq is
nonnegative-yielding;
hereby
let i1,i2,j1,j2 be
Nat;
assume i1
<= i2 & j1
<= j2;
then ((
Partial_Sums Rseq)
. (i1,j1))
<= ((
Partial_Sums Rseq)
. (i1,j2)) & ((
Partial_Sums Rseq)
. (i1,j2))
<= ((
Partial_Sums Rseq)
. (i2,j2)) by
A1,
th105;
hence ((
Partial_Sums Rseq)
. (i1,j1))
<= ((
Partial_Sums Rseq)
. (i2,j2)) by
XXREAL_0: 2;
end;
end;
theorem ::
DBLSEQ_2:39
th1005: Rseq is
nonnegative-yielding implies for k be
Element of
NAT holds (
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),k)) is
non-decreasing & (
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),k)) is
non-decreasing & (
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),k)) is
nonnegative & (
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),k)) is
nonnegative & (
ProjMap2 ((
Partial_Sums_in_cod2 Rseq),k)) is
nonnegative & (
ProjMap1 ((
Partial_Sums_in_cod1 Rseq),k)) is
nonnegative
proof
assume
A1: Rseq is
nonnegative-yielding;
hereby
let k be
Element of
NAT ;
X1:
now
let i be
Nat;
i is
Element of
NAT by
ORDINAL1:def 12;
then
A3: ((
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),k))
. i)
= ((
Partial_Sums_in_cod1 Rseq)
. (i,k)) by
MESFUNC9:def 7;
((
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),k))
. (i
+ 1))
= ((
Partial_Sums_in_cod1 Rseq)
. ((i
+ 1),k)) by
MESFUNC9:def 7
.= (((
Partial_Sums_in_cod1 Rseq)
. (i,k))
+ (Rseq
. ((i
+ 1),k))) by
DefRS;
hence ((
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),k))
. i)
<= ((
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),k))
. (i
+ 1)) by
A1,
A3,
XREAL_1: 31;
end;
hence (
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),k)) is
non-decreasing by
VALUED_1:def 15;
X2:
now
let j be
Nat;
j is
Element of
NAT by
ORDINAL1:def 12;
then
A5: ((
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),k))
. j)
= ((
Partial_Sums_in_cod2 Rseq)
. (k,j)) by
MESFUNC9:def 6;
((
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),k))
. (j
+ 1))
= ((
Partial_Sums_in_cod2 Rseq)
. (k,(j
+ 1))) by
MESFUNC9:def 6
.= (((
Partial_Sums_in_cod2 Rseq)
. (k,j))
+ (Rseq
. (k,(j
+ 1)))) by
DefCS;
hence ((
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),k))
. j)
<= ((
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),k))
. (j
+ 1)) by
A1,
A5,
XREAL_1: 31;
end;
hence (
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),k)) is
non-decreasing by
VALUED_1:def 15;
B1: ((
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),k))
.
0 )
= ((
Partial_Sums_in_cod1 Rseq)
. (
0 ,k)) by
MESFUNC9:def 7
.= (Rseq
. (
0 ,k)) by
DefRS;
now
let i be
Nat;
((
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),k))
. (i
+
0 ))
>= ((
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),k))
.
0 ) by
X1,
SEQM_3: 5,
VALUED_1:def 15;
hence ((
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),k))
. i)
>=
0 by
B1,
A1;
end;
hence (
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),k)) is
nonnegative;
B2: ((
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),k))
.
0 )
= ((
Partial_Sums_in_cod2 Rseq)
. (k,
0 )) by
MESFUNC9:def 6
.= (Rseq
. (k,
0 )) by
DefCS;
now
let i be
Nat;
((
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),k))
. (i
+
0 ))
>= ((
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),k))
.
0 ) by
X2,
SEQM_3: 5,
VALUED_1:def 15;
hence ((
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),k))
. i)
>=
0 by
B2,
A1;
end;
hence (
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),k)) is
nonnegative;
now
let i be
Nat;
reconsider i1 = i as
Element of
NAT by
ORDINAL1:def 12;
B3: ((
ProjMap2 ((
Partial_Sums_in_cod2 Rseq),k))
. i)
= ((
Partial_Sums_in_cod2 Rseq)
. (i1,k)) by
MESFUNC9:def 7
.= ((
Partial_Sums (
ProjMap1 (Rseq,i1)))
. k) by
th100;
((
ProjMap1 (Rseq,i1))
. k)
= (Rseq
. (i1,k)) by
MESFUNC9:def 6;
then
B4: ((
ProjMap1 (Rseq,i1))
. k)
>=
0 by
A1;
now
let p be
Nat;
p is
Element of
NAT by
ORDINAL1:def 12;
then ((
ProjMap1 (Rseq,i1))
. p)
= (Rseq
. (i1,p)) by
MESFUNC9:def 6;
hence ((
ProjMap1 (Rseq,i1))
. p)
>=
0 by
A1;
end;
then (
ProjMap1 (Rseq,i1)) is
nonnegative-yielding;
hence ((
ProjMap2 ((
Partial_Sums_in_cod2 Rseq),k))
. i)
>=
0 by
B3,
B4,
th101;
end;
hence (
ProjMap2 ((
Partial_Sums_in_cod2 Rseq),k)) is
nonnegative;
now
let i be
Nat;
reconsider i1 = i as
Element of
NAT by
ORDINAL1:def 12;
B5: ((
ProjMap1 ((
Partial_Sums_in_cod1 Rseq),k))
. i)
= ((
Partial_Sums_in_cod1 Rseq)
. (k,i1)) by
MESFUNC9:def 6
.= ((
Partial_Sums (
ProjMap2 (Rseq,i1)))
. k) by
th100;
((
ProjMap2 (Rseq,i1))
. k)
= (Rseq
. (k,i1)) by
MESFUNC9:def 7;
then
B6: ((
ProjMap2 (Rseq,i1))
. k)
>=
0 by
A1;
now
let p be
Nat;
p is
Element of
NAT by
ORDINAL1:def 12;
then ((
ProjMap2 (Rseq,i1))
. p)
= (Rseq
. (p,i1)) by
MESFUNC9:def 7;
hence ((
ProjMap2 (Rseq,i1))
. p)
>=
0 by
A1;
end;
then (
ProjMap2 (Rseq,i1)) is
nonnegative-yielding;
hence ((
ProjMap1 ((
Partial_Sums_in_cod1 Rseq),k))
. i)
>=
0 by
B5,
B6,
th101;
end;
hence (
ProjMap1 ((
Partial_Sums_in_cod1 Rseq),k)) is
nonnegative;
end;
end;
theorem ::
DBLSEQ_2:40
th1006: Rseq is
nonnegative-yielding & (
Partial_Sums Rseq) is
P-convergent implies (
Partial_Sums_in_cod1 Rseq) is
convergent_in_cod1 & (
Partial_Sums_in_cod2 Rseq) is
convergent_in_cod2
proof
assume that
A1: Rseq is
nonnegative-yielding and
A2: (
Partial_Sums Rseq) is
P-convergent;
now
let k be
Element of
NAT ;
B1: (
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),k)) is
non-decreasing by
A1,
th1005;
now
let n be
Nat;
reconsider n1 = n as
Element of
NAT by
ORDINAL1:def 12;
B2: ((
Partial_Sums Rseq)
. (n,k))
= ((
Partial_Sums (
ProjMap1 ((
Partial_Sums_in_cod1 Rseq),n1)))
. k) by
th100;
B3: ((
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),k))
. n1)
= ((
Partial_Sums_in_cod1 Rseq)
. (n1,k)) by
MESFUNC9:def 7
.= ((
ProjMap1 ((
Partial_Sums_in_cod1 Rseq),n1))
. k) by
MESFUNC9:def 6;
now
let d be
Nat;
(
ProjMap1 ((
Partial_Sums_in_cod1 Rseq),n1)) is
nonnegative by
A1,
th1005;
hence ((
ProjMap1 ((
Partial_Sums_in_cod1 Rseq),n1))
. d)
>=
0 ;
end;
then (
ProjMap1 ((
Partial_Sums_in_cod1 Rseq),n1)) is
nonnegative-yielding;
then
B4: ((
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),k))
. n1)
<= ((
Partial_Sums Rseq)
. (n,k)) by
B2,
B3,
th101;
consider N be
Nat such that
B6: for n,m be
Nat st n
>= N & m
>= N holds
|.(((
Partial_Sums Rseq)
. (n,m))
- (
P-lim (
Partial_Sums Rseq))).|
< 1 by
A2,
DBLSEQ_1:def 2;
reconsider N1 = (
max (N,(
max (k,n)))) as
Nat by
TARSKI: 1;
B7: N1
>= N & N1
>= (
max (k,n)) & (
max (k,n))
>= k & (
max (k,n))
>= n by
XXREAL_0: 25;
then
|.(((
Partial_Sums Rseq)
. (N1,N1))
- (
P-lim (
Partial_Sums Rseq))).|
< 1 by
B6;
then (((
Partial_Sums Rseq)
. (N1,N1))
- (
P-lim (
Partial_Sums Rseq)))
<= 1 by
ABSVALUE: 5;
then (((
Partial_Sums Rseq)
. (N1,N1))
- (
P-lim (
Partial_Sums Rseq)))
< 2 by
XXREAL_0: 2;
then
B8: ((
Partial_Sums Rseq)
. (N1,N1))
< ((
P-lim (
Partial_Sums Rseq))
+ 2) by
XREAL_1: 19;
B9: N1
>= k & N1
>= n by
B7,
XXREAL_0: 2;
(
Partial_Sums Rseq) is
non-decreasing by
A1,
th80a;
then ((
Partial_Sums Rseq)
. (n,k))
<= ((
Partial_Sums Rseq)
. (N1,N1)) by
B9;
then ((
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),k))
. n)
<= ((
Partial_Sums Rseq)
. (N1,N1)) by
B4,
XXREAL_0: 2;
hence ((
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),k))
. n)
< ((
P-lim (
Partial_Sums Rseq))
+ 2) by
B8,
XXREAL_0: 2;
end;
then (
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),k)) is
bounded_above by
SEQ_2:def 3;
hence (
ProjMap2 ((
Partial_Sums_in_cod1 Rseq),k)) is
convergent by
B1;
end;
hence (
Partial_Sums_in_cod1 Rseq) is
convergent_in_cod1;
now
let k be
Element of
NAT ;
C1: (
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),k)) is
non-decreasing by
A1,
th1005;
now
let n be
Nat;
reconsider n1 = n as
Element of
NAT by
ORDINAL1:def 12;
B2: ((
Partial_Sums Rseq)
. (k,n))
= ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (k,n)) by
th103
.= ((
Partial_Sums (
ProjMap2 ((
Partial_Sums_in_cod2 Rseq),n1)))
. k) by
th100;
B3: ((
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),k))
. n1)
= ((
Partial_Sums_in_cod2 Rseq)
. (k,n1)) by
MESFUNC9:def 6
.= ((
ProjMap2 ((
Partial_Sums_in_cod2 Rseq),n1))
. k) by
MESFUNC9:def 7;
now
let d be
Nat;
(
ProjMap2 ((
Partial_Sums_in_cod2 Rseq),n1)) is
nonnegative by
A1,
th1005;
hence ((
ProjMap2 ((
Partial_Sums_in_cod2 Rseq),n1))
. d)
>=
0 ;
end;
then (
ProjMap2 ((
Partial_Sums_in_cod2 Rseq),n1)) is
nonnegative-yielding;
then
B4: ((
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),k))
. n1)
<= ((
Partial_Sums Rseq)
. (k,n)) by
B2,
B3,
th101;
consider N be
Nat such that
B6: for n,m be
Nat st n
>= N & m
>= N holds
|.(((
Partial_Sums Rseq)
. (n,m))
- (
P-lim (
Partial_Sums Rseq))).|
< 1 by
A2,
DBLSEQ_1:def 2;
reconsider N1 = (
max (N,(
max (k,n)))) as
Nat by
TARSKI: 1;
B7: N1
>= N & N1
>= (
max (k,n)) & (
max (k,n))
>= k & (
max (k,n))
>= n by
XXREAL_0: 25;
then
|.(((
Partial_Sums Rseq)
. (N1,N1))
- (
P-lim (
Partial_Sums Rseq))).|
< 1 by
B6;
then (((
Partial_Sums Rseq)
. (N1,N1))
- (
P-lim (
Partial_Sums Rseq)))
<= 1 by
ABSVALUE: 5;
then (((
Partial_Sums Rseq)
. (N1,N1))
- (
P-lim (
Partial_Sums Rseq)))
< 2 by
XXREAL_0: 2;
then
B8: ((
Partial_Sums Rseq)
. (N1,N1))
< ((
P-lim (
Partial_Sums Rseq))
+ 2) by
XREAL_1: 19;
B9: N1
>= k & N1
>= n by
B7,
XXREAL_0: 2;
(
Partial_Sums Rseq) is
non-decreasing by
A1,
th80a;
then ((
Partial_Sums Rseq)
. (k,n))
<= ((
Partial_Sums Rseq)
. (N1,N1)) by
B9;
then ((
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),k))
. n)
<= ((
Partial_Sums Rseq)
. (N1,N1)) by
B4,
XXREAL_0: 2;
hence ((
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),k))
. n)
< ((
P-lim (
Partial_Sums Rseq))
+ 2) by
B8,
XXREAL_0: 2;
end;
then (
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),k)) is
bounded_above by
SEQ_2:def 3;
hence (
ProjMap1 ((
Partial_Sums_in_cod2 Rseq),k)) is
convergent by
C1;
end;
hence (
Partial_Sums_in_cod2 Rseq) is
convergent_in_cod2;
end;
theorem ::
DBLSEQ_2:41
th1006a: Rseq is
nonnegative-yielding & (
Partial_Sums Rseq) is
P-convergent implies (
Partial_Sums Rseq) is
convergent_in_cod1 & (
Partial_Sums Rseq) is
convergent_in_cod2
proof
assume that
A1: Rseq is
nonnegative-yielding and
A2: (
Partial_Sums Rseq) is
P-convergent;
(
Partial_Sums_in_cod1 Rseq) is
convergent_in_cod1 & (
Partial_Sums_in_cod2 Rseq) is
convergent_in_cod2 by
A1,
A2,
th1006;
hence thesis by
th01a,
th01b;
end;
theorem ::
DBLSEQ_2:42
Rseq is
nonnegative-yielding & (
Partial_Sums Rseq) is
P-convergent implies (
lim_in_cod1 (
Partial_Sums_in_cod1 Rseq)) is
summable & (
lim_in_cod2 (
Partial_Sums_in_cod2 Rseq)) is
summable
proof
assume that
A1: Rseq is
nonnegative-yielding and
A2: (
Partial_Sums Rseq) is
P-convergent;
(
Partial_Sums Rseq) is
convergent_in_cod1 & (
Partial_Sums Rseq) is
convergent_in_cod2 by
A1,
A2,
th1006a;
then
A3: (
lim_in_cod1 (
Partial_Sums Rseq)) is
convergent & (
lim_in_cod2 (
Partial_Sums Rseq)) is
convergent by
A2;
then (
Partial_Sums (
lim_in_cod1 (
Partial_Sums_in_cod1 Rseq))) is
convergent by
A1,
A2,
th1006a,
th03a;
hence (
lim_in_cod1 (
Partial_Sums_in_cod1 Rseq)) is
summable by
SERIES_1:def 2;
(
Partial_Sums (
lim_in_cod2 (
Partial_Sums_in_cod2 Rseq))) is
convergent by
A3,
A1,
A2,
th1006a,
th03b;
hence (
lim_in_cod2 (
Partial_Sums_in_cod2 Rseq)) is
summable by
SERIES_1:def 2;
end;
theorem ::
DBLSEQ_2:43
Rseq is
nonnegative-yielding & (
Partial_Sums Rseq) is
P-convergent implies (
P-lim (
Partial_Sums Rseq))
= (
Sum (
lim_in_cod1 (
Partial_Sums_in_cod1 Rseq))) & (
P-lim (
Partial_Sums Rseq))
= (
Sum (
lim_in_cod2 (
Partial_Sums_in_cod2 Rseq)))
proof
assume that
A1: Rseq is
nonnegative-yielding and
A2: (
Partial_Sums Rseq) is
P-convergent;
A4: (
Partial_Sums Rseq) is
convergent_in_cod1 & (
Partial_Sums Rseq) is
convergent_in_cod2 by
A1,
A2,
th1006a;
A5: (
Sum (
lim_in_cod1 (
Partial_Sums_in_cod1 Rseq)))
= (
lim (
Partial_Sums (
lim_in_cod1 (
Partial_Sums_in_cod1 Rseq)))) by
SERIES_1:def 3;
for e be
Real st
0
< e holds ex M be
Nat st for m be
Nat st m
>= M holds
|.(((
lim_in_cod1 (
Partial_Sums Rseq))
. m)
- (
cod1_major_iterated_lim (
Partial_Sums Rseq))).|
< e by
A2,
A4,
DBLSEQ_1:def 7;
then (
cod1_major_iterated_lim (
Partial_Sums Rseq))
= (
lim (
lim_in_cod1 (
Partial_Sums Rseq))) by
A2,
A4,
SEQ_2:def 7
.= (
Sum (
lim_in_cod1 (
Partial_Sums_in_cod1 Rseq))) by
A5,
A1,
A2,
th1006a,
th03a;
hence (
P-lim (
Partial_Sums Rseq))
= (
Sum (
lim_in_cod1 (
Partial_Sums_in_cod1 Rseq))) by
A1,
A2,
th1006a,
DBLSEQ_1: 4;
A6: (
Sum (
lim_in_cod2 (
Partial_Sums_in_cod2 Rseq)))
= (
lim (
Partial_Sums (
lim_in_cod2 (
Partial_Sums_in_cod2 Rseq)))) by
SERIES_1:def 3;
for e be
Real st
0
< e holds ex M be
Nat st for m be
Nat st m
>= M holds
|.(((
lim_in_cod2 (
Partial_Sums Rseq))
. m)
- (
cod2_major_iterated_lim (
Partial_Sums Rseq))).|
< e by
A2,
A4,
DBLSEQ_1:def 8;
then (
cod2_major_iterated_lim (
Partial_Sums Rseq))
= (
lim (
lim_in_cod2 (
Partial_Sums Rseq))) by
A2,
A4,
SEQ_2:def 7
.= (
Sum (
lim_in_cod2 (
Partial_Sums_in_cod2 Rseq))) by
A6,
A1,
A2,
th1006a,
th03b;
hence (
P-lim (
Partial_Sums Rseq))
= (
Sum (
lim_in_cod2 (
Partial_Sums_in_cod2 Rseq))) by
A1,
A2,
th1006a,
DBLSEQ_1: 3;
end;
begin
theorem ::
DBLSEQ_2:44
TMP6: for s1,s2 be
Real_Sequence st s1 is
nonnegative & (s1,s2)
are_fiberwise_equipotent holds s2 is
nonnegative
proof
let s1,s2 be
Real_Sequence;
assume that
A1: s1 is
nonnegative and
A2: (s1,s2)
are_fiberwise_equipotent ;
consider H be
Function such that
A3: (
dom H)
= (
dom s2) & (
rng H)
= (
dom s1) & H is
one-to-one & s2
= (s1
* H) by
A2,
CLASSES1: 77;
A4: (
dom H)
=
NAT & (
rng H)
=
NAT by
A3,
FUNCT_2:def 1;
now
let m be
Nat;
A6: (H
. m)
in (
dom s1) by
A3,
A4,
ORDINAL1:def 12,
FUNCT_1: 3;
(s2
. m)
= (s1
. (H
. m)) by
A3,
A4,
ORDINAL1:def 12,
FUNCT_1: 13;
hence
0
<= (s2
. m) by
A1,
A6;
end;
hence s2 is
nonnegative;
end;
theorem ::
DBLSEQ_2:45
SH1: for X be non
empty
set, s be
sequence of X, n be
Nat holds (
dom (
Shift ((s
| (
Segm n)),1)))
= (
Seg n)
proof
let X be non
empty
set;
let s be
sequence of X;
let n be
Nat;
(
Segm n)
c=
NAT ;
then (
NAT
/\ (
Segm n))
= (
Segm n) by
XBOOLE_1: 28;
then ((
dom s)
/\ (
Segm n))
= (
Segm n) by
FUNCT_2:def 1;
then
A2: (
dom (s
| (
Segm n)))
= (
Segm n) by
RELAT_1: 61;
A3: (
dom (
Shift ((s
| (
Segm n)),1)))
= { (m
+ 1) where m be
Nat : m
in (
dom (s
| (
Segm n))) } by
VALUED_1:def 12;
now
let k be
object;
assume k
in (
dom (
Shift ((s
| (
Segm n)),1)));
then
consider m be
Nat such that
A4: k
= (m
+ 1) & m
in (
dom (s
| (
Segm n))) by
A3;
per cases ;
suppose n
=
0 ;
hence k
in (
Seg n) by
A4;
end;
suppose n
<>
0 ;
then
reconsider n1 = (n
- 1) as
Element of
NAT by
NAT_1: 20;
reconsider n1 as
Nat;
B3: n
= (n1
+ 1);
m
in (
Segm (n1
+ 1)) by
A4,
RELAT_1: 57;
then m
in (
succ (
Segm n1)) by
NAT_1: 38;
then m
in { l where l be
Nat : l
<= n1 } by
NAT_1: 54;
then
consider l be
Nat such that
A5: m
= l & l
<= n1;
1
<= (m
+ 1) & (m
+ 1)
<= n by
A5,
B3,
NAT_1: 11,
XREAL_1: 6;
hence k
in (
Seg n) by
A4,
FINSEQ_1: 1;
end;
end;
then
A6: (
dom (
Shift ((s
| (
Segm n)),1)))
c= (
Seg n);
now
let k be
object;
assume k
in (
Seg n);
then k
in { l where l be
Nat : 1
<= l & l
<= n } by
FINSEQ_1:def 1;
then
consider l be
Nat such that
A7: k
= l & 1
<= l & l
<= n;
0
< l by
A7;
then
reconsider l1 = (l
- 1) as
Element of
NAT by
NAT_1: 20;
0
< n by
A7;
then
reconsider i = (n
- 1) as
Element of
NAT by
NAT_1: 20;
B5: n
= (i
+ 1);
B9: k
= (l1
+ 1) by
A7;
l1
<= i by
A7,
XREAL_1: 9;
then l1
in { m where m be
Nat : m
<= i };
then l1
in (
succ (
Segm i)) by
NAT_1: 54;
then l1
in (
Segm n) by
B5,
NAT_1: 38;
hence k
in (
dom (
Shift ((s
| (
Segm n)),1))) by
A2,
A3,
B9;
end;
then (
Seg n)
c= (
dom (
Shift ((s
| (
Segm n)),1)));
hence (
dom (
Shift ((s
| (
Segm n)),1)))
= (
Seg n) by
A6,
XBOOLE_0:def 10;
end;
registration
let X be non
empty
set;
let s be
sequence of X;
let n be
Nat;
cluster (
Shift ((s
| (
Segm n)),1)) ->
FinSequence-like;
coherence
proof
(
dom (
Shift ((s
| (
Segm n)),1)))
= (
Seg n) by
SH1;
hence thesis by
FINSEQ_1:def 2;
end;
end
theorem ::
DBLSEQ_2:46
SH2: for X be non
empty
set, s be
sequence of X, n be
Nat holds (
Shift ((s
| (
Segm n)),1)) is
FinSequence of X
proof
let X be non
empty
set, s be
sequence of X, n be
Nat;
(
rng (
Shift ((s
| (
Segm n)),1)))
c= X;
hence thesis by
FINSEQ_1:def 4;
end;
theorem ::
DBLSEQ_2:47
SH3: for X be non
empty
set, s be
sequence of X, n,m be
Nat st (m
+ 1)
in (
dom (
Shift ((s
| (
Segm n)),1))) holds ((
Shift ((s
| (
Segm n)),1))
. (m
+ 1))
= (s
. m)
proof
let X be non
empty
set;
let s be
sequence of X;
let n,m be
Nat;
assume (m
+ 1)
in (
dom (
Shift ((s
| (
Segm n)),1)));
then
consider k be
Nat such that
A1: k
in (
dom (s
| (
Segm n))) & (m
+ 1)
= (k
+ 1) by
VALUED_1: 39;
((
Shift ((s
| (
Segm n)),1))
. (m
+ 1))
= ((s
| (
Segm n))
. m) by
A1,
VALUED_1:def 12;
hence ((
Shift ((s
| (
Segm n)),1))
. (m
+ 1))
= (s
. m) by
A1,
FUNCT_1: 47;
end;
theorem ::
DBLSEQ_2:48
SH4: for X be non
empty
set, s be
sequence of X holds (
Shift ((s
| (
Segm
0 )),1))
=
{} & (
Shift ((s
| (
Segm 1)),1))
=
<*(s
.
0 )*> & (
Shift ((s
| (
Segm 2)),1))
=
<*(s
.
0 ), (s
. 1)*> & for n be
Nat holds (
Shift ((s
| (
Segm (n
+ 1))),1))
= ((
Shift ((s
| (
Segm n)),1))
^
<*(s
. n)*>)
proof
let X be non
empty
set, s be
sequence of X;
thus (
Shift ((s
| (
Segm
0 )),1))
=
{} ;
A1: (
dom (
Shift ((s
| (
Segm 1)),1)))
= (
Seg 1) by
SH1;
then 1
in (
dom (
Shift ((s
| (
Segm 1)),1))) by
FINSEQ_1: 2,
TARSKI:def 1;
then ex n be
Nat st n
in (
dom (s
| (
Segm 1))) & 1
= (n
+ 1) by
VALUED_1: 39;
then
A3: ((
Shift ((s
| (
Segm 1)),1))
. 1)
= ((s
| (
Segm 1))
.
0 ) by
VALUED_1:def 12;
0
in
{
0 } by
TARSKI:def 1;
then
0
in (
Segm 1) by
CARD_1: 49,
ORDINAL1:def 17;
hence (
Shift ((s
| (
Segm 1)),1))
=
<*(s
.
0 )*> by
A1,
A3,
FUNCT_1: 49,
FINSEQ_1:def 8;
A6: (
dom (
Shift ((s
| (
Segm 2)),1)))
= (
Seg 2) by
SH1;
then
A4: (
len (
Shift ((s
| (
Segm 2)),1)))
= 2 by
FINSEQ_1:def 3;
A5: (
Segm 2)
=
{
0 , 1} by
CARD_1: 50,
ORDINAL1:def 17;
A7: 1
in (
dom (
Shift ((s
| (
Segm 2)),1))) & 2
in (
dom (
Shift ((s
| (
Segm 2)),1))) by
A6,
FINSEQ_1: 2,
TARSKI:def 2;
then ex n be
Nat st n
in (
dom (s
| (
Segm 2))) & 1
= (n
+ 1) by
VALUED_1: 39;
then
A9: ((
Shift ((s
| (
Segm 2)),1))
. 1)
= ((s
| (
Segm 2))
.
0 ) by
VALUED_1:def 12;
0
in (
Segm 2) by
A5,
TARSKI:def 2;
then
A10: ((
Shift ((s
| (
Segm 2)),1))
. 1)
= (s
.
0 ) by
A9,
FUNCT_1: 49;
ex m be
Nat st m
in (
dom (s
| (
Segm 2))) & 2
= (m
+ 1) by
A7,
VALUED_1: 39;
then
A12: ((
Shift ((s
| (
Segm 2)),1))
. 2)
= ((s
| (
Segm 2))
. 1) by
VALUED_1:def 12;
1
in (
Segm 2) by
A5,
TARSKI:def 2;
hence (
Shift ((s
| (
Segm 2)),1))
=
<*(s
.
0 ), (s
. 1)*> by
A4,
A10,
A12,
FUNCT_1: 49,
FINSEQ_1: 44;
hereby
let n be
Nat;
X3: n is
Element of
NAT by
ORDINAL1:def 12;
(
dom (
Shift ((s
| (
Segm (n
+ 1))),1)))
= (
Seg (n
+ 1)) & (
dom (
Shift ((s
| (
Segm n)),1)))
= (
Seg n) by
SH1;
then
A13: (
len (
Shift ((s
| (
Segm (n
+ 1))),1)))
= (n
+ 1) & (
len (
Shift ((s
| (
Segm n)),1)))
= n by
X3,
FINSEQ_1:def 3;
A14: (
len
<*(s
. n)*>)
= 1 by
FINSEQ_1: 40;
A15: for k be
Nat st k
in (
dom (
Shift ((s
| (
Segm n)),1))) holds ((
Shift ((s
| (
Segm (n
+ 1))),1))
. k)
= ((
Shift ((s
| (
Segm n)),1))
. k)
proof
let k be
Nat;
assume
A17: k
in (
dom (
Shift ((s
| (
Segm n)),1)));
then
A18: k
in (
Seg n) by
SH1;
then 1
<= k by
FINSEQ_1: 1;
then
reconsider k1 = (k
- 1) as
Element of
NAT by
NAT_1: 21;
(
Seg n)
c= (
Seg (n
+ 1)) by
FINSEQ_3: 18;
then k
in (
Seg (n
+ 1)) by
A18;
then
A19: k
in (
dom (
Shift ((s
| (
Segm (n
+ 1))),1))) by
SH1;
k
= (k1
+ 1);
then ((
Shift ((s
| (
Segm n)),1))
. k)
= (s
. k1) & ((
Shift ((s
| (
Segm (n
+ 1))),1))
. k)
= (s
. k1) by
A17,
A19,
SH3;
hence thesis;
end;
for k be
Nat st k
in (
dom
<*(s
. n)*>) holds ((
Shift ((s
| (
Segm (n
+ 1))),1))
. ((
len (
Shift ((s
| (
Segm n)),1)))
+ k))
= (
<*(s
. n)*>
. k)
proof
let k be
Nat;
assume k
in (
dom
<*(s
. n)*>);
then k
in (
Seg 1) by
FINSEQ_1:def 8;
then
A20: k
= 1 by
FINSEQ_1: 2,
TARSKI:def 1;
then
A23: (
<*(s
. n)*>
. k)
= (s
. n) by
FINSEQ_1:def 8;
A21: n is
Element of
NAT by
ORDINAL1:def 12;
(
dom (
Shift ((s
| (
Segm n)),1)))
= (
Seg n) by
SH1;
then
A22: (
len (
Shift ((s
| (
Segm n)),1)))
= n by
A21,
FINSEQ_1:def 3;
(n
+ 1)
in (
Seg (n
+ 1)) by
FINSEQ_1: 4;
then (n
+ 1)
in (
dom (
Shift ((s
| (
Segm (n
+ 1))),1))) by
SH1;
hence thesis by
A23,
A22,
A20,
SH3;
end;
hence (
Shift ((s
| (
Segm (n
+ 1))),1))
= ((
Shift ((s
| (
Segm n)),1))
^
<*(s
. n)*>) by
A13,
A14,
A15,
FINSEQ_3: 38;
end;
end;
theorem ::
DBLSEQ_2:49
SH5: for s be
Real_Sequence, n be
Nat holds ((
Partial_Sums s)
. n)
= (
Sum (
Shift ((s
| (
Segm (n
+ 1))),1)))
proof
let s be
Real_Sequence, n be
Nat;
defpred
P[
Nat] means ((
Partial_Sums s)
. $1)
= (
Sum (
Shift ((s
| (
Segm ($1
+ 1))),1)));
A1: ((
Partial_Sums s)
.
0 )
= (s
.
0 ) by
SERIES_1:def 1;
(
Shift ((s
| (
Segm (
0
+ 1))),1))
=
<*(s
.
0 )*> by
SH4;
then
A2:
P[
0 ] by
A1,
RVSUM_1: 73;
A3: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat;
assume
A4:
P[k];
A5: ((
Partial_Sums s)
. (k
+ 1))
= (((
Partial_Sums s)
. k)
+ (s
. (k
+ 1))) by
SERIES_1:def 1;
(
Shift ((s
| (
Segm ((k
+ 1)
+ 1))),1))
= ((
Shift ((s
| (
Segm (k
+ 1))),1))
^
<*(s
. (k
+ 1))*>) by
SH4;
hence
P[(k
+ 1)] by
A4,
A5,
RVSUM_1: 74;
end;
for k be
Nat holds
P[k] from
NAT_1:sch 2(
A2,
A3);
hence thesis;
end;
theorem ::
DBLSEQ_2:50
SH6: for X be non
empty
set, s1,s2 be
sequence of X, n be
Nat st (s1,s2)
are_fiberwise_equipotent holds ex m be
Nat, fs2 be
Subset of (
Shift ((s2
| (
Segm m)),1)) st ((
Shift ((s1
| (
Segm (n
+ 1))),1)),fs2)
are_fiberwise_equipotent
proof
let X be non
empty
set;
let s1,s2 be
sequence of X;
let n be
Nat;
assume
A1: (s1,s2)
are_fiberwise_equipotent ;
A4: (
dom s1)
=
NAT & (
dom s2)
=
NAT by
FUNCT_2:def 1;
then
consider P be
Permutation of (
dom s1) such that
A2: s1
= (s2
* P) by
A1,
CLASSES1: 80;
deffunc
F(
set) = ((P
. $1)
+ 1);
defpred
P2[
set] means $1 is
Nat;
{
F(i) where i be
Nat : i
<= n &
P2[i] } is
finite from
FINSEQ_1:sch 6;
then
reconsider D = {
F(i) where i be
Nat : i
<= n &
P2[i] } as
finite
set;
now
let x be
object;
assume x
in D;
then
consider i be
Nat such that
A3: x
=
F(i) & i
<= n &
P2[i];
thus x is
natural by
A3;
end;
then
reconsider D as
finite
natural-membered
set by
MEMBERED:def 6;
((P
.
0 )
+ 1)
in {
F(i) where i be
Nat : i
<= n &
P2[i] };
then
reconsider D as non
empty
finite
natural-membered
set;
reconsider m = (
max D) as
Nat by
TARSKI: 1;
take m;
set fs2 = {
[(j
+ 1), (s2
. j)] where j be
Nat : (j
+ 1)
in D };
now
let z be
object;
assume z
in fs2;
then
consider j be
Nat such that
A4: z
=
[(j
+ 1), (s2
. j)] & (j
+ 1)
in D;
1
<= (j
+ 1) & (j
+ 1)
<= m by
A4,
NAT_1: 11,
XXREAL_2:def 8;
then (j
+ 1)
in (
Seg m) by
FINSEQ_1: 1;
then
A6: (j
+ 1)
in (
dom (
Shift ((s2
| (
Segm m)),1))) by
SH1;
then ((
Shift ((s2
| (
Segm m)),1))
. (j
+ 1))
= (s2
. j) by
SH3;
hence z
in (
Shift ((s2
| (
Segm m)),1)) by
A4,
A6,
FUNCT_1:def 2;
end;
then fs2
c= (
Shift ((s2
| (
Segm m)),1));
then
reconsider fs2 as
Subset of (
Shift ((s2
| (
Segm m)),1));
take fs2;
defpred
P2[
object,
object] means ex i be
Nat st $1
= (i
+ 1) & $2
= ((P
. i)
+ 1);
P1: for x,y1,y2 be
object st x
in (
Seg (n
+ 1)) &
P2[x, y1] &
P2[x, y2] holds y1
= y2;
P2: for x be
object st x
in (
Seg (n
+ 1)) holds ex y be
object st
P2[x, y]
proof
let x be
object;
assume
A7: x
in (
Seg (n
+ 1));
then
reconsider x as
Nat;
1
<= x & x
<= (n
+ 1) by
A7,
FINSEQ_1: 1;
then
reconsider i = (x
- 1) as
Element of
NAT by
NAT_1: 21;
A8: x
= (i
+ 1);
ex y be
object st
P2[x, y]
proof
take y = ((P
. i)
+ 1);
thus thesis by
A8;
end;
hence thesis;
end;
now
let x be
object;
assume x
in (
dom fs2);
then
[x, (fs2
. x)]
in fs2 by
FUNCT_1:def 2;
then
consider j be
Nat such that
X2:
[x, (fs2
. x)]
=
[(j
+ 1), (s2
. j)] & (j
+ 1)
in D;
x
= (j
+ 1) & (fs2
. x)
= (s2
. j) by
X2,
XTUPLE_0: 1;
hence x
in { (i
+ 1) where i be
Nat : (i
+ 1)
in D } by
X2;
end;
then
X3: (
dom fs2)
c= { (i
+ 1) where i be
Nat : (i
+ 1)
in D };
now
let x be
object;
assume x
in { (i
+ 1) where i be
Nat : (i
+ 1)
in D };
then
consider i be
Nat such that
X4: x
= (i
+ 1) & (i
+ 1)
in D;
[x, (s2
. i)]
in fs2 by
X4;
hence x
in (
dom fs2) by
XTUPLE_0:def 12;
end;
then { (i
+ 1) where i be
Nat : (i
+ 1)
in D }
c= (
dom fs2);
then
X5: (
dom fs2)
= { (i
+ 1) where i be
Nat : (i
+ 1)
in D } by
X3,
XBOOLE_0:def 10;
consider P2 be
Function such that
A9: (
dom P2)
= (
Seg (n
+ 1)) & for x be
object st x
in (
Seg (n
+ 1)) holds
P2[x, (P2
. x)] from
FUNCT_1:sch 2(
P1,
P2);
A10: (
dom P2)
= (
dom (
Shift ((s1
| (
Segm (n
+ 1))),1))) by
A9,
SH1;
now
let y be
object;
assume y
in (
rng P2);
then
consider x be
object such that
B1: x
in (
dom P2) & y
= (P2
. x) by
FUNCT_1:def 3;
consider i be
Nat such that
B2: x
= (i
+ 1) & (P2
. x)
= ((P
. i)
+ 1) by
B1,
A9;
B5: i
<= n by
B2,
B1,
A9,
FINSEQ_1: 1,
XREAL_1: 6;
y
in D by
B5,
B1,
B2;
hence y
in (
dom fs2) by
X5,
B1,
B2;
end;
then
B6: (
rng P2)
c= (
dom fs2);
now
let y be
object;
assume y
in (
dom fs2);
then
consider i be
Nat such that
C1: y
= (i
+ 1) & (i
+ 1)
in D by
X5;
consider j be
Nat such that
C2: (i
+ 1)
= ((P
. j)
+ 1) & j
<= n & j is
Nat by
C1;
C3: 1
<= (j
+ 1) & (j
+ 1)
<= (n
+ 1) by
C2,
NAT_1: 11,
XREAL_1: 6;
then ex k be
Nat st (j
+ 1)
= (k
+ 1) & (P2
. (j
+ 1))
= ((P
. k)
+ 1) by
A9,
FINSEQ_1: 1;
hence y
in (
rng P2) by
C1,
C2,
C3,
A9,
FUNCT_1: 3,
FINSEQ_1: 1;
end;
then (
dom fs2)
c= (
rng P2);
then
A11: (
rng P2)
= (
dom fs2) by
B6,
XBOOLE_0:def 10;
now
let x1,x2 be
object;
assume
D1: x1
in (
dom P2) & x2
in (
dom P2) & (P2
. x1)
= (P2
. x2);
then
consider i1 be
Nat such that
D3: x1
= (i1
+ 1) & (P2
. x1)
= ((P
. i1)
+ 1) by
A9;
consider i2 be
Nat such that
D4: x2
= (i2
+ 1) & (P2
. x2)
= ((P
. i2)
+ 1) by
D1,
A9;
(
dom P)
=
NAT by
A4,
FUNCT_2:def 1;
then i1
in (
dom P) & i2
in (
dom P) by
ORDINAL1:def 12;
hence x1
= x2 by
D1,
D3,
D4,
FUNCT_1:def 4;
end;
then
A12: P2 is
one-to-one by
FUNCT_1:def 4;
E0: (
dom (fs2
* P2))
= (
dom P2) by
B6,
RELAT_1: 27;
then
E1: (
dom (fs2
* P2))
= (
dom (
Shift ((s1
| (
Segm (n
+ 1))),1))) by
A9,
SH1;
for x be
object st x
in (
dom (
Shift ((s1
| (
Segm (n
+ 1))),1))) holds ((
Shift ((s1
| (
Segm (n
+ 1))),1))
. x)
= ((fs2
* P2)
. x)
proof
let x be
object;
assume
E4: x
in (
dom (
Shift ((s1
| (
Segm (n
+ 1))),1)));
then
E2: x
in (
Seg (n
+ 1)) by
SH1;
reconsider i = x as
Nat by
E4;
1
<= i & i
<= (n
+ 1) by
E2,
FINSEQ_1: 1;
then
reconsider j = (i
- 1) as
Element of
NAT by
NAT_1: 21;
i
= (j
+ 1);
then
E11: ((
Shift ((s1
| (
Segm (n
+ 1))),1))
. x)
= ((s2
* P)
. j) by
A2,
E4,
SH3;
j
in
NAT ;
then j
in (
dom P) by
A4,
FUNCT_2:def 1;
then
E12: ((s2
* P)
. j)
= (s2
. (P
. j)) by
FUNCT_1: 13;
consider k be
Nat such that
E6: i
= (k
+ 1) & (P2
. i)
= ((P
. k)
+ 1) by
E2,
A9;
(P2
. x)
in (
dom fs2) by
A11,
E4,
E1,
E0,
FUNCT_1: 3;
then
[(P2
. x), (fs2
. (P2
. x))]
in fs2 by
FUNCT_1:def 2;
then
consider l be
Nat such that
E7:
[(P2
. x), (fs2
. (P2
. x))]
=
[(l
+ 1), (s2
. l)] & (l
+ 1)
in D;
(P2
. i)
= (l
+ 1) & (fs2
. (P2
. i))
= (s2
. l) by
E7,
XTUPLE_0: 1;
hence ((
Shift ((s1
| (
Segm (n
+ 1))),1))
. x)
= ((fs2
* P2)
. x) by
E11,
E12,
E6,
E4,
E1,
FUNCT_1: 12;
end;
hence ((
Shift ((s1
| (
Segm (n
+ 1))),1)),fs2)
are_fiberwise_equipotent by
A10,
A11,
A12,
E0,
FUNCT_1:def 11,
CLASSES1: 77;
end;
theorem ::
DBLSEQ_2:51
SH7: for X be non
empty
set, fs be
FinSequence of X, fss be
Subset of fs holds ((
Seq fss),fss)
are_fiberwise_equipotent
proof
let X be non
empty
set, fs be
FinSequence of X, fss be
Subset of fs;
(
dom fss)
c= (
dom fs) by
RELAT_1: 11;
then
A0: (
dom fss)
c= (
Seg (
len fs)) by
FINSEQ_1:def 3;
then
A1: fss is
FinSubsequence by
FINSEQ_1:def 12;
then
A2: (
Seq fss)
= (fss
* (
Sgm (
dom fss))) by
FINSEQ_1:def 14;
A3: (
rng (
Sgm (
dom fss)))
= (
dom fss) by
A1,
FINSEQ_1: 50;
then
A4: (
dom (
Sgm (
dom fss)))
= (
dom (
Seq fss)) by
A2,
RELAT_1: 27;
now
let x1,x2 be
object;
assume
A5: x1
in (
dom (
Sgm (
dom fss))) & x2
in (
dom (
Sgm (
dom fss))) & ((
Sgm (
dom fss))
. x1)
= ((
Sgm (
dom fss))
. x2);
reconsider i1 = x1, i2 = x2 as
Nat by
A5;
reconsider k1 = ((
Sgm (
dom fss))
. i1), k2 = ((
Sgm (
dom fss))
. i2) as
Nat;
A6: 1
<= i1 & 1
<= i2 & i1
<= (
len (
Sgm (
dom fss))) & i2
<= (
len (
Sgm (
dom fss))) by
A5,
FINSEQ_3: 25;
now
assume i1
<> i2;
then i1
< i2 or i1
> i2 by
XXREAL_0: 1;
hence contradiction by
A5,
A0,
A6,
FINSEQ_1:def 13;
end;
hence x1
= x2;
end;
hence thesis by
A2,
A3,
A4,
CLASSES1: 77,
FUNCT_1:def 4;
end;
theorem ::
DBLSEQ_2:52
SH8: for s1,s2 be
Real_Sequence, n be
Nat st (s1,s2)
are_fiberwise_equipotent & s1 is
nonnegative holds ex m be
Nat st ((
Partial_Sums s1)
. n)
<= ((
Partial_Sums s2)
. m)
proof
let s1,s2 be
Real_Sequence;
let n be
Nat;
assume that
A1: (s1,s2)
are_fiberwise_equipotent and
A2: s1 is
nonnegative;
B1: s2 is
nonnegative by
A1,
A2,
TMP6;
consider m be
Nat, F2 be
Subset of (
Shift ((s2
| (
Segm m)),1)) such that
A3: ((
Shift ((s1
| (
Segm (n
+ 1))),1)),F2)
are_fiberwise_equipotent by
A1,
SH6;
take m;
reconsider FS1 = (
Shift ((s1
| (
Segm (n
+ 1))),1)), FS2 = (
Shift ((s2
| (
Segm m)),1)) as
FinSequence of
REAL by
SH2;
reconsider F2 as
Subset of FS2;
((
Seq F2),F2)
are_fiberwise_equipotent by
SH7;
then
A4: (
Sum FS1)
= (
Sum (
Seq F2)) by
A3,
CLASSES1: 76,
RFINSEQ: 9;
now
let i be
Element of
NAT ;
assume
A6: i
in (
dom FS2);
then
reconsider i1 = (i
- 1) as
Element of
NAT by
NAT_1: 21,
FINSEQ_3: 25;
(i1
+ 1)
= i;
then (FS2
. i)
= (s2
. i1) by
A6,
SH3;
hence
0
<= (FS2
. i) by
A1,
A2,
TMP6,
RINFSUP1:def 3;
end;
then (
Sum (
Seq F2))
<= (
Sum FS2) by
GLIB_003: 2;
then
A7: ((
Partial_Sums s1)
. n)
<= (
Sum FS2) by
A4,
SH5;
(
Shift ((s2
| (
Segm (m
+ 1))),1))
= ((
Shift ((s2
| (
Segm m)),1))
^
<*(s2
. m)*>) by
SH4;
then (
Sum (
Shift ((s2
| (
Segm (m
+ 1))),1)))
= ((
Sum FS2)
+ (s2
. m)) by
RVSUM_1: 74;
then
A8: ((
Partial_Sums s2)
. m)
= ((
Sum FS2)
+ (s2
. m)) by
SH5;
((
Partial_Sums s2)
. m)
>= (
Sum FS2) by
A8,
XREAL_1: 31,
B1;
hence ((
Partial_Sums s1)
. n)
<= ((
Partial_Sums s2)
. m) by
A7,
XXREAL_0: 2;
end;
theorem ::
DBLSEQ_2:53
for s1,s2 be
Real_Sequence st (s1,s2)
are_fiberwise_equipotent & s1 is
nonnegative & s1 is
summable holds s2 is
summable & (
Sum s1)
= (
Sum s2)
proof
let s1,s2 be
Real_Sequence;
assume that
A1: (s1,s2)
are_fiberwise_equipotent & s1 is
nonnegative and
A2: s1 is
summable;
(
Partial_Sums s1) is
bounded_above by
A2,
A1,
SERIES_1: 17;
then
consider r be
Real such that
A5: for n be
Nat holds ((
Partial_Sums s1)
. n)
< r by
SEQ_2:def 3;
A3: for n be
Nat holds
0
<= (s2
. n) by
A1,
TMP6,
RINFSUP1:def 3;
B3:
now
let n be
Nat;
consider m be
Nat such that
A6: ((
Partial_Sums s2)
. n)
<= ((
Partial_Sums s1)
. m) by
A1,
TMP6,
SH8;
thus ((
Partial_Sums s2)
. n)
< r by
A5,
A6,
XXREAL_0: 2;
end;
then
B2: (
Partial_Sums s2) is
bounded_above by
SEQ_2:def 3;
hence
A7: s2 is
summable by
A3,
SERIES_1: 17;
A8: (
Partial_Sums s1) is
bounded_above & (
Partial_Sums s2) is
bounded_above by
A2,
B3,
SEQ_2:def 3,
A1,
SERIES_1: 17;
now
let n be
Nat;
consider m be
Nat such that
A11: ((
Partial_Sums s1)
. n)
<= ((
Partial_Sums s2)
. m) by
A1,
SH8;
((
Partial_Sums s2)
. m)
<= (
lim (
Partial_Sums s2)) by
A3,
B2,
SERIES_1: 16,
SEQ_4: 37;
hence ((
Partial_Sums s1)
. n)
<= (
lim (
Partial_Sums s2)) by
A11,
XXREAL_0: 2;
end;
then (
lim (
Partial_Sums s1))
<= (
lim (
Partial_Sums s2)) by
A2,
SERIES_1:def 2,
PREPOWER: 2;
then (
Sum s1)
<= (
lim (
Partial_Sums s2)) by
SERIES_1:def 3;
then
A12: (
Sum s1)
<= (
Sum s2) by
SERIES_1:def 3;
now
let m be
Nat;
consider n be
Nat such that
A13: ((
Partial_Sums s2)
. m)
<= ((
Partial_Sums s1)
. n) by
A1,
TMP6,
SH8;
((
Partial_Sums s1)
. n)
<= (
lim (
Partial_Sums s1)) by
A8,
A1,
SERIES_1: 16,
SEQ_4: 37;
hence ((
Partial_Sums s2)
. m)
<= (
lim (
Partial_Sums s1)) by
A13,
XXREAL_0: 2;
end;
then (
lim (
Partial_Sums s2))
<= (
lim (
Partial_Sums s1)) by
A7,
SERIES_1:def 2,
PREPOWER: 2;
then (
Sum s2)
<= (
lim (
Partial_Sums s1)) by
SERIES_1:def 3;
then (
Sum s2)
<= (
Sum s1) by
SERIES_1:def 3;
hence (
Sum s1)
= (
Sum s2) by
A12,
XXREAL_0: 1;
end;
begin
theorem ::
DBLSEQ_2:54
for D be non
empty
set, Rseq be
Function of
[:
NAT ,
NAT :], D, n,m be
Nat holds ex M be
Matrix of (n
+ 1), (m
+ 1), D st for i,j be
Nat st i
<= n & j
<= m holds (Rseq
. (i,j))
= (M
* ((i
+ 1),(j
+ 1)))
proof
let D be non
empty
set, Rseq be
Function of
[:
NAT ,
NAT :], D;
let n,m be
Nat;
defpred
P[
Nat,
Nat,
object] means ex i1,j1 be
Nat st i1
= ($1
- 1) & j1
= ($2
- 1) & $3
= (Rseq
. (i1,j1));
A1:
now
let i,j be
Nat;
assume
[i, j]
in
[:(
Seg (n
+ 1)), (
Seg (m
+ 1)):];
then (
[i, j]
`1 )
in (
Seg (n
+ 1)) & (
[i, j]
`2 )
in (
Seg (m
+ 1)) by
MCART_1: 10;
then 1
<= i & 1
<= j by
FINSEQ_1: 1;
then
reconsider i1 = (i
- 1), j1 = (j
- 1) as
Element of
NAT by
NAT_1: 21;
reconsider i1, j1 as
Nat;
(
dom Rseq)
=
[:
NAT ,
NAT :] by
FUNCT_2:def 1;
then
[i1, j1]
in (
dom Rseq) by
ZFMISC_1:def 2;
then
reconsider x = (Rseq
. (i1,j1)) as
Element of D by
FUNCT_2: 5;
take x;
thus
P[i, j, x];
end;
consider M be
Matrix of (n
+ 1), (m
+ 1), D such that
A2: for i,j be
Nat st
[i, j]
in (
Indices M) holds
P[i, j, (M
* (i,j))] from
MATRIX_0:sch 2(
A1);
take M;
hereby
let i,j be
Nat;
assume i
<= n & j
<= m;
then i
< (n
+ 1) & j
< (m
+ 1) by
NAT_1: 13;
then (i
+ 1)
in (
Seg (n
+ 1)) & (j
+ 1)
in (
Seg (m
+ 1)) by
FINSEQ_3: 11;
then
[(i
+ 1), (j
+ 1)]
in
[:(
Seg (n
+ 1)), (
Seg (m
+ 1)):] by
ZFMISC_1:def 2;
then
[(i
+ 1), (j
+ 1)]
in (
Indices M) by
MATRIX_0: 23;
then
consider i1,j1 be
Nat such that
A4: i1
= ((i
+ 1)
- 1) & j1
= ((j
+ 1)
- 1) & (M
* ((i
+ 1),(j
+ 1)))
= (Rseq
. (i1,j1)) by
A2;
thus (Rseq
. (i,j))
= (M
* ((i
+ 1),(j
+ 1))) by
A4;
end;
end;
theorem ::
DBLSEQ_2:55
for n,m be
Nat, Rseq be
Function of
[:
NAT ,
NAT :],
REAL , M be
Matrix of (n
+ 1), (m
+ 1),
REAL st (for i,j be
Nat st i
<= n & j
<= m holds (Rseq
. (i,j))
= (M
* ((i
+ 1),(j
+ 1)))) holds ((
Partial_Sums Rseq)
. (n,m))
= (
SumAll M)
proof
let n,m be
Nat;
let Rseq be
Function of
[:
NAT ,
NAT :],
REAL ;
let M be
Matrix of (n
+ 1), (m
+ 1),
REAL ;
assume
A1: for i,j be
Nat st i
<= n & j
<= m holds (Rseq
. (i,j))
= (M
* ((i
+ 1),(j
+ 1)));
A2: (
len M)
= (n
+ 1) by
MATRIX_0: 25;
then
A3: (
width M)
= (m
+ 1) by
MATRIX_0: 20;
X1: for i be
Nat st i
<= n holds ((
Partial_Sums_in_cod2 Rseq)
. (i,m))
= ((
LineSum M)
. (i
+ 1))
proof
let i be
Nat;
assume
B0: i
<= n;
then 1
<= (i
+ 1) & (i
+ 1)
<= (n
+ 1) by
NAT_1: 11,
XREAL_1: 6;
then
B01: (i
+ 1)
in (
Seg (n
+ 1)) by
FINSEQ_1: 1;
defpred
P1[
Nat] means ($1
+ 1)
<= (
width M) implies ((
Partial_Sums_in_cod2 Rseq)
. (i,$1))
= (
Sum ((
Line (M,(i
+ 1)))
| ($1
+ 1)));
now
assume (
0
+ 1)
<= (
width M);
B2: ((
Partial_Sums_in_cod2 Rseq)
. (i,
0 ))
= (Rseq
. (i,
0 )) by
DefCS;
(
len (
Line (M,(i
+ 1))))
= (m
+ 1) by
A3,
MATRIX_0:def 7;
then
B5: (
len ((
Line (M,(i
+ 1)))
| 1))
= 1 by
NAT_1: 11,
FINSEQ_1: 59;
1
<= (
width M) by
A3,
NAT_1: 11;
then
B4: 1
in (
Seg (
width M)) by
FINSEQ_1: 1;
(((
Line (M,(i
+ 1)))
| 1)
. 1)
= ((
Line (M,(i
+ 1)))
. 1) by
FINSEQ_3: 112;
then ((
Line (M,(i
+ 1)))
| (
0
+ 1))
=
<*(M
* ((i
+ 1),1))*> by
B5,
B4,
MATRIX_0:def 7,
FINSEQ_1: 40;
then
B6: (
Sum ((
Line (M,(i
+ 1)))
| (
0
+ 1)))
= (M
* ((i
+ 1),1)) by
RVSUM_1: 73;
thus ((
Partial_Sums_in_cod2 Rseq)
. (i,
0 ))
= (
Sum ((
Line (M,(i
+ 1)))
| (
0
+ 1))) by
A1,
B0,
B2,
B6;
end;
then
P0:
P1[
0 ];
P1: for k be
Nat st
P1[k] holds
P1[(k
+ 1)]
proof
let k be
Nat;
assume
C1:
P1[k];
now
assume
C2: ((k
+ 1)
+ 1)
<= (
width M);
then
C3: (k
+ 1)
<= ((k
+ 1)
+ 1) & ((k
+ 1)
+ 1)
<= (
len (
Line (M,(i
+ 1)))) by
MATRIX_0:def 7,
NAT_1: 11;
then
C5: (
len ((
Line (M,(i
+ 1)))
| ((k
+ 1)
+ 1)))
= ((k
+ 1)
+ 1) by
FINSEQ_1: 59;
then ((
Line (M,(i
+ 1)))
| ((k
+ 1)
+ 1))
= ((((
Line (M,(i
+ 1)))
| ((k
+ 1)
+ 1))
| (k
+ 1))
^
<*(((
Line (M,(i
+ 1)))
| ((k
+ 1)
+ 1))
/. (
len ((
Line (M,(i
+ 1)))
| ((k
+ 1)
+ 1))))*>) by
FINSEQ_5: 21;
then
C6: ((
Line (M,(i
+ 1)))
| ((k
+ 1)
+ 1))
= (((
Line (M,(i
+ 1)))
| (k
+ 1))
^
<*(((
Line (M,(i
+ 1)))
| (k
+ 2))
/. (k
+ 2))*>) by
C5,
FINSEQ_1: 82,
NAT_1: 11;
1
<= ((k
+ 1)
+ 1) by
NAT_1: 11;
then
C7: (k
+ 2)
in (
Seg (
width M)) by
C2,
FINSEQ_1: 1;
C8: (k
+ 1)
<= m by
A3,
C2,
XREAL_1: 6;
(k
+ 2)
in (
Seg (
len ((
Line (M,(i
+ 1)))
| (k
+ 2)))) by
C5,
FINSEQ_1: 4;
then (k
+ 2)
in (
dom ((
Line (M,(i
+ 1)))
| (k
+ 2))) by
FINSEQ_1:def 3;
then (((
Line (M,(i
+ 1)))
| (k
+ 2))
/. (k
+ 2))
= (((
Line (M,(i
+ 1)))
| (k
+ 2))
. (k
+ 2)) by
PARTFUN1:def 6;
then (((
Line (M,(i
+ 1)))
| (k
+ 2))
/. (k
+ 2))
= ((
Line (M,(i
+ 1)))
. (k
+ 2)) by
FINSEQ_3: 112;
then (((
Line (M,(i
+ 1)))
| (k
+ 2))
/. (k
+ 2))
= (M
* ((i
+ 1),(k
+ 2))) by
C7,
MATRIX_0:def 7;
then (
Sum ((
Line (M,(i
+ 1)))
| ((k
+ 1)
+ 1)))
= ((
Sum ((
Line (M,(i
+ 1)))
| (k
+ 1)))
+ (M
* ((i
+ 1),(k
+ 2)))) by
C6,
RVSUM_1: 74;
then (
Sum ((
Line (M,(i
+ 1)))
| ((k
+ 1)
+ 1)))
= (((
Partial_Sums_in_cod2 Rseq)
. (i,k))
+ (Rseq
. (i,(k
+ 1)))) by
C3,
B0,
A1,
C8,
C1,
C2,
XXREAL_0: 2;
hence ((
Partial_Sums_in_cod2 Rseq)
. (i,(k
+ 1)))
= (
Sum ((
Line (M,(i
+ 1)))
| ((k
+ 1)
+ 1))) by
DefCS;
end;
hence
P1[(k
+ 1)];
end;
C9: (m
+ 1)
= (
len (
Line (M,(i
+ 1)))) by
A3,
MATRIX_0:def 7;
for k be
Nat holds
P1[k] from
NAT_1:sch 2(
P0,
P1);
then ((
Partial_Sums_in_cod2 Rseq)
. (i,m))
= (
Sum ((
Line (M,(i
+ 1)))
| (m
+ 1))) by
A3;
then ((
Partial_Sums_in_cod2 Rseq)
. (i,m))
= (
Sum (
Line (M,(i
+ 1)))) by
C9,
FINSEQ_1: 58;
hence ((
Partial_Sums_in_cod2 Rseq)
. (i,m))
= ((
LineSum M)
. (i
+ 1)) by
B01,
A2,
MATRPROB: 20;
end;
defpred
P2[
Nat] means $1
<= n implies ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. ($1,m))
= (
Sum ((
LineSum M)
| ($1
+ 1)));
now
assume
0
<= n;
(
0
+ 1)
<= (n
+ 1) by
XREAL_1: 6;
then (
0
+ 1)
<= (
len (
LineSum M)) by
A2,
MATRPROB: 20;
then (
len ((
LineSum M)
| (
0
+ 1)))
= 1 by
FINSEQ_1: 59;
then
D2: ((
LineSum M)
| (
0
+ 1))
=
<*(((
LineSum M)
| (
0
+ 1))
. 1)*> by
FINSEQ_1: 40;
((
Partial_Sums_in_cod2 Rseq)
. (
0 ,m))
= ((
LineSum M)
. (
0
+ 1)) by
X1;
then ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (
0 ,m))
= ((
LineSum M)
. (
0
+ 1)) by
DefRS
.= (
Sum
<*((
LineSum M)
. (
0
+ 1))*>) by
RVSUM_1: 73;
hence ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (
0 ,m))
= (
Sum ((
LineSum M)
| (
0
+ 1))) by
D2,
FINSEQ_3: 112;
end;
then
P2:
P2[
0 ];
P3: for k be
Nat st
P2[k] holds
P2[(k
+ 1)]
proof
let k be
Nat;
assume
E1:
P2[k];
now
assume
E2: (k
+ 1)
<= n;
then (k
+ 1)
<= ((k
+ 1)
+ 1) & ((k
+ 1)
+ 1)
<= (n
+ 1) by
NAT_1: 11,
XREAL_1: 6;
then ((k
+ 1)
+ 1)
<= (
len (
LineSum M)) by
A2,
MATRPROB: 20;
then
E3: (
len ((
LineSum M)
| ((k
+ 1)
+ 1)))
= ((k
+ 1)
+ 1) by
FINSEQ_1: 59;
then
E5: ((
LineSum M)
| ((k
+ 1)
+ 1))
= ((((
LineSum M)
| ((k
+ 1)
+ 1))
| (k
+ 1))
^
<*(((
LineSum M)
| ((k
+ 1)
+ 1))
/. (
len ((
LineSum M)
| ((k
+ 1)
+ 1))))*>) by
FINSEQ_5: 21
.= (((
LineSum M)
| (k
+ 1))
^
<*(((
LineSum M)
| ((k
+ 1)
+ 1))
/. ((k
+ 1)
+ 1))*>) by
E3,
NAT_1: 11,
FINSEQ_1: 82;
E7: k
<= (k
+ 1) by
NAT_1: 11;
(k
+ 2)
in (
Seg (
len ((
LineSum M)
| (k
+ 2)))) by
E3,
FINSEQ_1: 4;
then (k
+ 2)
in (
dom ((
LineSum M)
| (k
+ 2))) by
FINSEQ_1:def 3;
then (((
LineSum M)
| (k
+ 2))
/. (k
+ 2))
= (((
LineSum M)
| (k
+ 2))
. (k
+ 2)) by
PARTFUN1:def 6
.= ((
LineSum M)
. (k
+ 2)) by
FINSEQ_3: 112;
then (
Sum ((
LineSum M)
| ((k
+ 1)
+ 1)))
= ((
Sum ((
LineSum M)
| (k
+ 1)))
+ ((
LineSum M)
. ((k
+ 1)
+ 1))) by
E5,
RVSUM_1: 74
.= (((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (k,m))
+ ((
Partial_Sums_in_cod2 Rseq)
. ((k
+ 1),m))) by
E1,
E7,
E2,
X1,
XXREAL_0: 2;
hence ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. ((k
+ 1),m))
= (
Sum ((
LineSum M)
| ((k
+ 1)
+ 1))) by
DefRS;
end;
hence
P2[(k
+ 1)];
end;
for k be
Nat holds
P2[k] from
NAT_1:sch 2(
P2,
P3);
then
X2: ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (n,m))
= (
Sum ((
LineSum M)
| (n
+ 1)));
(
len (
LineSum M))
= (n
+ 1) by
A2,
MATRPROB: 20;
then ((
LineSum M)
| (n
+ 1))
= (
LineSum M) by
FINSEQ_1: 58;
then ((
Partial_Sums_in_cod1 (
Partial_Sums_in_cod2 Rseq))
. (n,m))
= (
SumAll M) by
X2,
MATRPROB:def 3;
hence ((
Partial_Sums Rseq)
. (n,m))
= (
SumAll M) by
th103;
end;