environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, FUNCT_1, RELAT_1, XBOOLE_0, ARYTM_3, ARYTM_1, XXREAL_0, CARD_1, TARSKI, NAT_1, ZFMISC_1, VALUED_0, ORDINAL2, SEQ_2, ORDINAL1, XREAL_0, COMPLEX1, XXREAL_2, FINSET_1, MEMBERED, MESFUNC9, SEQ_1, VALUED_1, DBLSEQ_1, QC_LANG1, FUNCT_2, SERIES_1, DBLSEQ_2, FINSEQ_1, FUNCOP_1, SUPINF_2, CLASSES1, CARD_3, ORDINAL4, REAL_1, PARTFUN1, MATRIX_1, MCART_1, MATRIXC1, INCSP_1, TREES_1, PARTFUN3;
notations HIDDEN, VALUED_1, TARSKI, XBOOLE_0, XTUPLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, ORDINAL1, XXREAL_2, NUMBERS, BINOP_1, XCMPLX_0, FUNCOP_1, MEMBERED, COMPLEX1, XXREAL_0, XREAL_0, SEQ_1, NAT_1, FUNCT_4, MESFUNC9, FUNCT_2, SEQ_2, FINSET_1, DBLSEQ_1, SERIES_1, PARTFUN3, RINFSUP1, CLASSES1, FINSEQ_1, GLIB_003, RVSUM_1, MATRIX_0, MATRPROB;
definitions FUNCT_1, PARTFUN3, RINFSUP1;
theorems TARSKI, XREAL_0, NAT_1, FUNCT_1, XXREAL_0, ZFMISC_1, XREAL_1, FUNCT_2, RELAT_1, MESFUNC9, ORDINAL1, VALUED_1, COMPLEX1, MEMBERED, XXREAL_2, RINFSUP1, SEQM_3, SEQ_2, SEQ_4, DBLSEQ_1, BINOP_1, XTUPLE_0, XBOOLE_0, FUNCT_3, SERIES_1, SERIES_3, CARD_1, XBOOLE_1, FUNCOP_1, CLASSES1, RFINSEQ, FINSEQ_1, FINSEQ_3, RVSUM_1, GLIB_003, PREPOWER, MCART_1, MATRIX_0, FINSEQ_5, PARTFUN1, MATRPROB, ABSVALUE, FUNCT_4, SUBSET_1;
schemes FUNCT_2, STACKS_1, RECDEF_1, NAT_1, BINOP_1, FINSEQ_1, FUNCT_1, MATRIX_0;
registrations ORDINAL1, XXREAL_0, XREAL_0, XBOOLE_0, NUMBERS, XCMPLX_0, FINSET_1, MEMBERED, VALUED_0, XXREAL_2, RELSET_1, SEQ_4, FUNCT_1, FUNCT_2, VALUED_1, BINOP_2, NAT_1, CARD_1, RELAT_1, DBLSEQ_1, XTUPLE_0, FUNCT_4;
constructors HIDDEN, TOPMETR, NAT_D, MESFUNC9, SEQ_2, COMSEQ_2, SEQ_4, DBLSEQ_1, SERIES_1, CLASSES1, PARTFUN3, GLIB_003, RVSUM_1, FUNCT_4, MATRPROB;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities BINOP_1, VALUED_0, DBLSEQ_1, FUNCT_2, RELAT_1;
expansions MEASURE6, DBLSEQ_1, FUNCT_2, TARSKI, XTUPLE_0, PARTFUN3, RINFSUP1;
theorem lmADD:
for
Rseq1,
Rseq2 being
Function of
[:NAT,NAT:],
REAL holds
(
dom (Rseq1 + Rseq2) = [:NAT,NAT:] &
dom (Rseq1 - Rseq2) = [:NAT,NAT:] & ( for
n,
m being
Nat holds
(Rseq1 + Rseq2) . (
n,
m)
= (Rseq1 . (n,m)) + (Rseq2 . (n,m)) ) & ( for
n,
m being
Nat holds
(Rseq1 - Rseq2) . (
n,
m)
= (Rseq1 . (n,m)) - (Rseq2 . (n,m)) ) )
scheme
RecEx2D1{
F1()
-> non
empty set ,
F2()
-> non
empty set ,
F3()
-> Function of
F1(),
F2(),
F4(
set ,
set ,
Nat)
-> Element of
F2() } :
ex
g being
Function of
[:F1(),NAT:],
F2() st
for
a being
Element of
F1() holds
(
g . (
a,
0)
= F3()
. a & ( for
n being
Nat holds
g . (
a,
(n + 1))
= F4(
(g . (a,n)),
a,
n) ) )
scheme
RecEx2D2{
F1()
-> non
empty set ,
F2()
-> non
empty set ,
F3()
-> Function of
F1(),
F2(),
F4(
set ,
set ,
Nat)
-> Element of
F2() } :
ex
g being
Function of
[:NAT,F1():],
F2() st
for
a being
Element of
F1() holds
(
g . (
0,
a)
= F3()
. a & ( for
n being
Nat holds
g . (
(n + 1),
a)
= F4(
(g . (n,a)),
a,
n) ) )
definition
let Rseq be
Function of
[:NAT,NAT:],
REAL;
existence
ex b1 being Function of [:NAT,NAT:],REAL st
for n, m being Nat holds
( b1 . (n,0) = Rseq . (n,0) & b1 . (n,(m + 1)) = (b1 . (n,m)) + (Rseq . (n,(m + 1))) )
uniqueness
for b1, b2 being Function of [:NAT,NAT:],REAL st ( for n, m being Nat holds
( b1 . (n,0) = Rseq . (n,0) & b1 . (n,(m + 1)) = (b1 . (n,m)) + (Rseq . (n,(m + 1))) ) ) & ( for n, m being Nat holds
( b2 . (n,0) = Rseq . (n,0) & b2 . (n,(m + 1)) = (b2 . (n,m)) + (Rseq . (n,(m + 1))) ) ) holds
b1 = b2
end;
definition
let Rseq be
Function of
[:NAT,NAT:],
REAL;
existence
ex b1 being Function of [:NAT,NAT:],REAL st
for n, m being Nat holds
( b1 . (0,m) = Rseq . (0,m) & b1 . ((n + 1),m) = (b1 . (n,m)) + (Rseq . ((n + 1),m)) )
uniqueness
for b1, b2 being Function of [:NAT,NAT:],REAL st ( for n, m being Nat holds
( b1 . (0,m) = Rseq . (0,m) & b1 . ((n + 1),m) = (b1 . (n,m)) + (Rseq . ((n + 1),m)) ) ) & ( for n, m being Nat holds
( b2 . (0,m) = Rseq . (0,m) & b2 . ((n + 1),m) = (b2 . (n,m)) + (Rseq . ((n + 1),m)) ) ) holds
b1 = b2
end;
th103:
for Rseq being Function of [:NAT,NAT:],REAL
for m, n being Nat holds (Partial_Sums Rseq) . (m,n) = (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (m,n)
theorem lm84a:
for
Rseq1,
Rseq2 being
Function of
[:NAT,NAT:],
REAL st ( for
n,
m being
Nat holds
Rseq1 . (
n,
m)
<= Rseq2 . (
n,
m) ) holds
for
i,
j being
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) )
theorem th1003:
for
Rseq being
Function of
[:NAT,NAT:],
REAL st
Rseq is
nonnegative-yielding holds
( ( for
i1,
i2,
j being
Nat st
i1 <= i2 holds
(Partial_Sums_in_cod1 Rseq) . (
i1,
j)
<= (Partial_Sums_in_cod1 Rseq) . (
i2,
j) ) & ( for
i,
j1,
j2 being
Nat st
j1 <= j2 holds
(Partial_Sums_in_cod2 Rseq) . (
i,
j1)
<= (Partial_Sums_in_cod2 Rseq) . (
i,
j2) ) )
theorem th105:
for
Rseq being
Function of
[:NAT,NAT:],
REAL st
Rseq is
nonnegative-yielding holds
( ( for
i1,
i2,
j being
Nat st
i1 <= i2 holds
(Partial_Sums Rseq) . (
i1,
j)
<= (Partial_Sums Rseq) . (
i2,
j) ) & ( for
i,
j1,
j2 being
Nat st
j1 <= j2 holds
(Partial_Sums Rseq) . (
i,
j1)
<= (Partial_Sums Rseq) . (
i,
j2) ) )