Copyright (c) 1991 Association of Mizar Users
environ vocabulary BHSP_1, PRE_TOPC, NORMSP_1, ORDINAL2, SEQM_3, SEQ_1, RLVECT_1, METRIC_1, FUNCT_1, ARYTM_1, ARYTM_3, ABSVALUE, RELAT_1, SEQ_2, LATTICES, BHSP_3, ARYTM; notation TARSKI, ORDINAL1, NUMBERS, XREAL_0, REAL_1, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, SEQ_1, SEQM_3, ABSVALUE, STRUCT_0, PRE_TOPC, RLVECT_1, NORMSP_1, BHSP_1, BHSP_2; constructors REAL_1, NAT_1, SEQ_1, ABSVALUE, BHSP_2, MEMBERED, XBOOLE_0; clusters FUNCT_1, SEQM_3, STRUCT_0, XREAL_0, RELSET_1, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; theorems REAL_1, NAT_1, REAL_2, AXIOMS, FUNCT_1, SEQ_2, SEQM_3, SEQ_4, FUNCT_2, ABSVALUE, RLVECT_1, BHSP_1, BHSP_2, NORMSP_1, RELAT_1, RELSET_1, XREAL_0, XBOOLE_1, XCMPLX_0, XCMPLX_1; schemes NAT_1, SEQ_1, BHSP_1; begin reserve X for RealUnitarySpace, x, g, g1, h for Point of X, a, p, r, M, M1, M2 for Real, seq, seq1, seq2, seq3 for sequence of X, Nseq,Nseq1,Nseq2 for increasing Seq_of_Nat, Rseq for Real_Sequence, k, l, l1, l2, l3, n, m, m1, m2 for Nat; deffunc 0'(RealUnitarySpace) = 0.$1; definition let X; let seq; attr seq is Cauchy means :Def1: for r st r > 0 ex k st for n, m st ( n >= k & m >= k ) holds dist((seq.n), (seq.m)) < r; synonym seq is_Cauchy_sequence; end; theorem seq is constant implies seq is_Cauchy_sequence proof assume A1: seq is constant; let r such that A2: r > 0; take k = 0; let n, m such that n >= k & m >= k; dist((seq.n), (seq.m)) = dist((seq.n), (seq.n)) by A1,BHSP_1:70 .= 0 by BHSP_1:41; hence dist((seq.n), (seq.m)) < r by A2; end; theorem seq is_Cauchy_sequence iff for r st r > 0 ex k st for n, m st ( n >= k & m >= k ) holds ||.(seq.n) - (seq.m).|| < r proof thus seq is_Cauchy_sequence implies for r st r > 0 ex k st for n, m st ( n >= k & m >= k ) holds ||.(seq.n) - (seq.m).|| < r proof assume A1: seq is_Cauchy_sequence; let r; assume r > 0; then consider l such that A2: for n, m st ( n >= l & m >= l ) holds dist((seq.n), (seq.m)) < r by A1,Def1; take k = l; let n, m; assume n >= k & m >= k; then dist((seq.n), (seq.m)) < r by A2; hence thesis by BHSP_1:def 5; end; ( for r st r > 0 ex k st for n, m st ( n >= k & m >= k ) holds ||.(seq.n) - (seq.m).|| < r ) implies seq is_Cauchy_sequence proof assume A3: for r st r > 0 ex k st for n, m st ( n >= k & m >= k ) holds ||.(seq.n) - (seq.m).|| < r; let r; assume r > 0; then consider l such that A4: for n, m st ( n >= l & m >= l ) holds ||.(seq.n) - (seq.m).|| < r by A3; take k = l; let n, m; assume n >= k & m >= k; then ||.(seq.n) - (seq.m).|| < r by A4; hence dist((seq.n), (seq.m)) < r by BHSP_1:def 5; end; hence thesis; end; theorem seq1 is_Cauchy_sequence & seq2 is_Cauchy_sequence implies seq1 + seq2 is_Cauchy_sequence proof assume that A1: seq1 is_Cauchy_sequence and A2: seq2 is_Cauchy_sequence; let r; assume r > 0; then A3: r/2 > 0 by SEQ_2:3; then consider m1 such that A4: for n, m st ( n >= m1 & m >= m1 ) holds dist((seq1.n), (seq1.m)) < r/2 by A1,Def1; consider m2 such that A5: for n, m st ( n >= m2 & m >= m2 ) holds dist((seq2.n), (seq2.m)) < r/2 by A2,A3,Def1; take k = m1 + m2; let n, m such that A6: n >= k & m >= k; m1 + m2 >= m1 by NAT_1:37; then n >= m1 & m >= m1 by A6,AXIOMS:22; then A7: dist((seq1.n), (seq1.m)) < r/2 by A4; k >= m2 by NAT_1:37; then n >= m2 & m >= m2 by A6,AXIOMS:22; then dist((seq2.n), (seq2.m)) < r/2 by A5; then dist((seq1.n), (seq1.m)) + dist((seq2.n), (seq2.m)) < r/2 + r/2 by A7,REAL_1:67; then A8: dist((seq1.n), (seq1.m)) + dist((seq2.n), (seq2.m)) < r by XCMPLX_1:66; dist((seq1 + seq2).n, (seq1 + seq2).m) = dist((seq1.n) + (seq2.n), (seq1 + seq2).m) by NORMSP_1:def 5 .= dist((seq1.n) + (seq2.n), (seq1.m) + (seq2.m)) by NORMSP_1:def 5; then dist((seq1 + seq2).n, (seq1 + seq2).m) <= dist((seq1.n), (seq1.m)) + dist((seq2.n), (seq2.m)) by BHSP_1:47; hence dist((seq1 + seq2).n, (seq1 + seq2).m) < r by A8,AXIOMS:22; end; theorem seq1 is_Cauchy_sequence & seq2 is_Cauchy_sequence implies seq1 - seq2 is_Cauchy_sequence proof assume that A1: seq1 is_Cauchy_sequence and A2: seq2 is_Cauchy_sequence; let r; assume r > 0; then A3: r/2 > 0 by SEQ_2:3; then consider m1 such that A4: for n, m st ( n >= m1 & m >= m1 ) holds dist((seq1.n), (seq1.m)) < r/2 by A1,Def1; consider m2 such that A5: for n, m st ( n >= m2 & m >= m2 ) holds dist((seq2.n), (seq2.m)) < r/2 by A2,A3,Def1; take k = m1 + m2; let n, m such that A6: n >= k & m >= k; m1 + m2 >= m1 by NAT_1:37; then n >= m1 & m >= m1 by A6,AXIOMS:22; then A7: dist((seq1.n), (seq1.m)) < r/2 by A4; k >= m2 by NAT_1:37; then n >= m2 & m >= m2 by A6,AXIOMS:22; then dist((seq2.n), (seq2.m)) < r/2 by A5; then dist((seq1.n), (seq1.m)) + dist((seq2.n), (seq2.m)) < r/2 + r/2 by A7,REAL_1:67; then A8: dist((seq1.n), (seq1.m)) + dist((seq2.n), (seq2.m)) < r by XCMPLX_1:66; dist((seq1 - seq2).n, (seq1 - seq2).m) = dist((seq1.n) - (seq2.n), (seq1 - seq2).m) by NORMSP_1:def 6 .= dist((seq1.n) - (seq2.n), (seq1.m) - (seq2.m)) by NORMSP_1:def 6; then dist((seq1 - seq2).n, (seq1 - seq2).m) <= dist((seq1.n), (seq1.m)) + dist((seq2.n), (seq2.m)) by BHSP_1:48; hence dist((seq1 - seq2).n, (seq1 - seq2).m) < r by A8,AXIOMS:22; end; theorem Th5: seq is_Cauchy_sequence implies a * seq is_Cauchy_sequence proof assume A1: seq is_Cauchy_sequence; A2: now assume A3: a = 0; let r; assume r > 0; then consider m1 such that A4: for n, m st ( n >= m1 & m >= m1 ) holds dist((seq.n), (seq.m)) < r by A1,Def1; take k = m1; let n, m; assume n >= k & m >= k; then A5: dist((seq.n), (seq.m)) < r by A4; dist(a * (seq.n), a * (seq.m)) = dist(0'(X), 0 * (seq.m)) by A3,RLVECT_1:23 .= dist(0'(X), 0'(X)) by RLVECT_1:23 .= 0 by BHSP_1:41; then dist(a * (seq.n), a * (seq.m)) < r by A5,BHSP_1:44; then dist((a * seq).n, a * (seq.m)) < r by NORMSP_1:def 8; hence dist((a * seq).n, (a * seq).m) < r by NORMSP_1:def 8; end; now assume A6: a <> 0; then A7: abs(a) > 0 by ABSVALUE:6; let r such that A8: r > 0; A9: abs(a) <> 0 by A6,ABSVALUE:6; 0/abs(a) = 0; then r/abs(a) > 0 by A7,A8,REAL_1:73; then consider m1 such that A10: for n, m st ( n >= m1 & m >= m1 ) holds dist((seq.n), (seq.m)) < r/abs(a) by A1,Def1; take k = m1; let n, m; assume n >= k & m >= k; then A11: dist((seq.n), (seq.m)) < r/abs(a) by A10; A12: dist(a * (seq.n), a * (seq.m)) = ||.(a * (seq.n)) - (a * (seq.m)).|| by BHSP_1:def 5 .= ||.a * ((seq.n) - (seq.m)).|| by RLVECT_1:48 .= abs(a) * ||.(seq.n) - (seq.m).|| by BHSP_1:33 .= abs(a) * dist((seq.n), (seq.m)) by BHSP_1:def 5; abs(a) * (r/abs(a)) = abs(a) * (abs(a)" * r) by XCMPLX_0:def 9 .= abs(a) *abs(a)" * r by XCMPLX_1:4 .= 1 * r by A9,XCMPLX_0:def 7 .= r; then dist((a * (seq.n)), (a * (seq.m))) < r by A7,A11,A12,REAL_1:70; then dist((a * seq).n, (a * (seq.m))) < r by NORMSP_1:def 8; hence dist((a * seq).n, (a * seq).m) < r by NORMSP_1:def 8; end; hence thesis by A2,Def1; end; theorem seq is_Cauchy_sequence implies - seq is_Cauchy_sequence proof assume seq is_Cauchy_sequence; then (-1) * seq is_Cauchy_sequence by Th5; hence thesis by BHSP_1:77; end; theorem Th7: seq is_Cauchy_sequence implies seq + x is_Cauchy_sequence proof assume A1: seq is_Cauchy_sequence; let r; assume r > 0; then consider m1 such that A2: for n, m st ( n >= m1 & m >= m1 ) holds dist((seq.n), (seq.m)) < r by A1,Def1; take k = m1; let n, m; assume n >= k & m >= k; then A3: dist((seq.n), (seq.m)) < r by A2; dist((seq.n) + x, (seq.m) + x) <= dist((seq.n), (seq.m)) + dist(x, x) by BHSP_1:47; then dist((seq.n) + x, (seq.m) + x) <= dist((seq.n), (seq.m)) + 0 by BHSP_1:41; then dist((seq.n) + x, (seq.m) + x) < r by A3,AXIOMS:22; then dist((seq + x).n, (seq.m) + x) < r by BHSP_1:def 12; hence dist((seq + x).n, (seq + x).m) < r by BHSP_1:def 12; end; theorem seq is_Cauchy_sequence implies seq - x is_Cauchy_sequence proof assume seq is_Cauchy_sequence; then seq + (-x) is_Cauchy_sequence by Th7; hence thesis by BHSP_1:78; end; theorem seq is convergent implies seq is_Cauchy_sequence proof assume seq is convergent; then consider h such that A1: for r st r > 0 ex k st for n st n >= k holds dist((seq.n), h) < r by BHSP_2:def 1; let r; assume r > 0; then r/2 > 0 by SEQ_2:3; then consider m1 such that A2: for n st n >= m1 holds dist((seq.n), h) < r/2 by A1; take k = m1; let n, m; assume A3: n >= k & m >= k; then A4: dist((seq.n), h) < r/2 by A2; A5: dist((seq.m), h) < r/2 by A2,A3; A6: dist((seq.n), (seq.m)) <= dist((seq.n), h) + dist(h, (seq.m)) by BHSP_1:42; dist((seq.n), h) + dist(h, (seq.m)) < r/2 + r/2 by A4,A5,REAL_1:67; then dist((seq.n), h) + dist(h, (seq.m)) < r by XCMPLX_1:66; hence dist((seq.n), (seq.m)) < r by A6,AXIOMS:22; end; definition let X; let seq1, seq2; pred seq1 is_compared_to seq2 means :Def2: for r st r > 0 ex m st for n st n >= m holds dist(seq1.n, seq2.n) < r; end; theorem Th10: seq is_compared_to seq proof let r such that A1: r > 0; take m = 0; let n such that n >= m; thus dist((seq.n), (seq.n)) < r by A1,BHSP_1:41; end; theorem Th11: seq1 is_compared_to seq2 implies seq2 is_compared_to seq1 proof assume A1: seq1 is_compared_to seq2; let r; assume r > 0; then consider k such that A2: for n st n >= k holds dist((seq1.n), (seq2.n)) < r by A1,Def2; take m = k; let n; assume n >= m; hence thesis by A2; end; definition let X; let seq1, seq2; redefine pred seq1 is_compared_to seq2; reflexivity by Th10; symmetry by Th11; end; theorem seq1 is_compared_to seq2 & seq2 is_compared_to seq3 implies seq1 is_compared_to seq3 proof assume that A1: seq1 is_compared_to seq2 and A2: seq2 is_compared_to seq3; let r; assume r > 0; then A3: r/2 > 0 by SEQ_2:3; then consider m1 such that A4: for n st n >= m1 holds dist((seq1.n), (seq2.n)) < r/2 by A1,Def2; consider m2 such that A5: for n st n >= m2 holds dist((seq2.n), (seq3.n)) < r/2 by A2,A3,Def2; take m = m1 + m2; let n such that A6: n >= m; m1 + m2 >= m1 by NAT_1:37; then n >= m1 by A6,AXIOMS:22; then A7: dist((seq1.n), (seq2.n)) < r/2 by A4; m >= m2 by NAT_1:37; then n >= m2 by A6,AXIOMS:22; then dist((seq2.n), (seq3.n)) < r/2 by A5; then dist((seq1.n), (seq2.n)) + dist((seq2.n), (seq3.n)) < r/2 + r/2 by A7,REAL_1:67; then A8: dist((seq1.n), (seq2.n)) + dist((seq2.n), (seq3.n)) < r by XCMPLX_1:66; dist((seq1.n), (seq3.n)) <= dist((seq1.n), (seq2.n)) + dist((seq2.n), (seq3.n)) by BHSP_1:42; hence dist((seq1.n), (seq3.n)) < r by A8,AXIOMS:22; end; theorem seq1 is_compared_to seq2 iff for r st r > 0 ex m st for n st n >= m holds ||.(seq1.n) - (seq2.n).|| < r proof thus seq1 is_compared_to seq2 implies for r st r > 0 ex m st for n st n >= m holds ||.(seq1.n) - (seq2.n).|| < r proof assume A1: seq1 is_compared_to seq2; let r; assume r > 0; then consider m1 such that A2: for n st n >= m1 holds dist((seq1.n), (seq2.n)) < r by A1,Def2; take m = m1; let n; assume n >= m; then dist((seq1.n), (seq2.n)) < r by A2; hence thesis by BHSP_1:def 5; end; ( for r st r > 0 ex m st for n st n >= m holds ||.(seq1.n) - (seq2.n).|| < r ) implies seq1 is_compared_to seq2 proof assume A3: for r st r > 0 ex m st for n st n >= m holds ||.(seq1.n) - (seq2.n).|| < r; let r; assume r > 0; then consider m1 such that A4: for n st n >= m1 holds ||.(seq1.n) - (seq2.n).|| < r by A3; take m = m1; let n; assume n >= m; then ||.(seq1.n) - (seq2.n).|| < r by A4; hence thesis by BHSP_1:def 5; end; hence thesis; end; theorem ( ex k st for n st n >= k holds seq1.n = seq2.n ) implies seq1 is_compared_to seq2 proof assume A1: ex k st for n st n >= k holds seq1.n = seq2.n; let r such that A2: r > 0; consider m such that A3: for n st n >= m holds seq1.n = seq2.n by A1; take k = m; let n; assume n >= k; then dist((seq1.n), (seq2.n)) = dist((seq1.n), (seq1.n)) by A3 .= 0 by BHSP_1:41; hence dist((seq1.n), (seq2.n)) < r by A2; end; theorem seq1 is_Cauchy_sequence & seq1 is_compared_to seq2 implies seq2 is_Cauchy_sequence proof assume that A1: seq1 is_Cauchy_sequence and A2: seq1 is_compared_to seq2; let r; assume r > 0; then A3: r/3 > 0 by SEQ_4:4; then consider m1 such that A4: for n, m st ( n >= m1 & m >= m1 ) holds dist((seq1.n), (seq1.m)) < r/3 by A1,Def1; consider m2 such that A5: for n st n >= m2 holds dist((seq1.n), (seq2.n)) < r/3 by A2,A3,Def2; take k = m1 + m2; let n, m such that A6: n >= k & m >= k; m1 + m2 >= m1 by NAT_1:37; then n >= m1 & m >= m1 by A6,AXIOMS:22; then A7: dist((seq1.n), (seq1.m)) < r/3 by A4; A8: k >= m2 by NAT_1:37; then n >= m2 by A6,AXIOMS:22; then A9: dist((seq1.n), (seq2.n)) < r/3 by A5; m >= m2 by A6,A8,AXIOMS:22; then A10: dist((seq1.m), (seq2.m)) < r/3 by A5; A11: dist((seq2.n), (seq1.n)) + dist((seq1.n), (seq1.m)) < r/3 + r/3 by A7,A9,REAL_1:67; dist((seq2.n), (seq1.m)) <= dist((seq2.n), (seq1.n)) + dist((seq1.n), (seq1.m)) by BHSP_1:42; then dist((seq2.n), (seq1.m)) < r/3 + r/3 by A11,AXIOMS:22; then dist((seq2.n), (seq1.m)) + dist((seq1.m), (seq2.m)) < r/3 + r/3 + r/3 by A10,REAL_1:67; then A12: dist((seq2.n), (seq1.m)) + dist((seq1.m), (seq2.m)) < r by XCMPLX_1 :69; dist((seq2.n), (seq2.m)) <= dist((seq2.n), (seq1.m)) + dist((seq1.m), (seq2.m)) by BHSP_1:42; hence dist((seq2.n), (seq2.m)) < r by A12,AXIOMS:22; end; theorem seq1 is convergent & seq1 is_compared_to seq2 implies seq2 is convergent proof assume that A1: seq1 is convergent and A2: seq1 is_compared_to seq2; now let r; assume r > 0; then A3: r/2 > 0 by SEQ_2:3; then consider m1 such that A4: for n st n >= m1 holds dist((seq1.n), (lim seq1)) < r/2 by A1,BHSP_2:def 2; consider m2 such that A5: for n st n >= m2 holds dist((seq1.n), (seq2.n)) < r/2 by A2,A3,Def2; take m = m1 + m2; let n such that A6: n >= m; m1 + m2 >= m1 by NAT_1:37; then n >= m1 by A6,AXIOMS:22; then A7: dist((seq1.n), (lim seq1)) < r/2 by A4; m >= m2 by NAT_1:37; then n >= m2 by A6,AXIOMS:22; then dist((seq1.n), (seq2.n)) < r/2 by A5; then dist((seq2.n), (seq1.n)) + dist((seq1.n), (lim seq1)) < r/2 + r/2 by A7,REAL_1:67; then A8: dist((seq2.n), (seq1.n)) + dist((seq1.n), (lim seq1)) < r by XCMPLX_1:66; dist((seq2.n), (lim seq1)) <= dist((seq2.n), (seq1.n)) + dist((seq1.n), (lim seq1)) by BHSP_1:42; hence dist((seq2.n), (lim seq1)) < r by A8,AXIOMS:22; end; hence thesis by BHSP_2:def 1; end; theorem seq1 is convergent & lim seq1 = g & seq1 is_compared_to seq2 implies seq2 is convergent & lim seq2 = g proof assume that A1: seq1 is convergent and A2: lim seq1 = g and A3: seq1 is_compared_to seq2; A4: now let r; assume r > 0; then A5: r/2 > 0 by SEQ_2:3; then consider m1 such that A6: for n st n >= m1 holds dist((seq1.n), g) < r/2 by A1,A2,BHSP_2:def 2; consider m2 such that A7: for n st n >= m2 holds dist((seq1.n), (seq2.n)) < r/2 by A3,A5,Def2; take m = m1 + m2; let n such that A8: n >= m; m1 + m2 >= m1 by NAT_1:37; then n >= m1 by A8,AXIOMS:22; then A9: dist((seq1.n), g) < r/2 by A6; m >= m2 by NAT_1:37; then n >= m2 by A8,AXIOMS:22; then dist((seq1.n), (seq2.n)) < r/2 by A7; then dist((seq2.n), (seq1.n)) + dist((seq1.n), g) < r/2 + r/2 by A9,REAL_1:67; then A10: dist((seq2.n), (seq1.n)) + dist((seq1.n), g) < r by XCMPLX_1:66; dist((seq2.n), g) <= dist((seq2.n), (seq1.n)) + dist((seq1.n), g) by BHSP_1:42; hence dist((seq2.n), g) < r by A10,AXIOMS:22; end; then seq2 is convergent by BHSP_2:def 1; hence thesis by A4,BHSP_2:def 2; end; definition let X; let seq; attr seq is bounded means :Def3: ex M st M > 0 & for n holds ||.seq.n.|| <= M; end; theorem Th18: seq1 is bounded & seq2 is bounded implies seq1 + seq2 is bounded proof assume that A1: seq1 is bounded and A2: seq2 is bounded; consider M1 such that A3: M1 > 0 and A4: for n holds ||.seq1.n.|| <= M1 by A1,Def3; consider M2 such that A5: M2 > 0 and A6: for n holds ||.seq2.n.|| <= M2 by A2,Def3; A7: M1 + M2 > 0 + 0 by A3,A5,REAL_1:67; now let n; A8: ||.seq1.n.|| <= M1 by A4; ||.seq2.n.|| <= M2 by A6; then A9: ||.seq1.n.|| + ||.seq2.n.|| <= M1 + M2 by A8,REAL_1:55; ||.(seq1 + seq2).n.|| = ||.seq1.n + seq2.n.|| by NORMSP_1:def 5; then ||.(seq1 + seq2).n.|| <= ||.seq1.n.|| + ||.seq2.n.|| by BHSP_1:36; hence ||.(seq1 + seq2).n.|| <= M1 + M2 by A9,AXIOMS:22; end; hence thesis by A7,Def3; end; theorem Th19: seq is bounded implies -seq is bounded proof assume seq is bounded; then consider M such that A1: M > 0 and A2: for n holds ||.seq.n.|| <= M by Def3; now let n; ||.(- seq).n.|| = ||.- (seq.n).|| by BHSP_1:def 10 .= ||.seq.n.|| by BHSP_1:37; hence ||.(- seq).n.|| <= M by A2; end; hence thesis by A1,Def3; end; theorem seq1 is bounded & seq2 is bounded implies seq1 - seq2 is bounded proof assume that A1: seq1 is bounded and A2: seq2 is bounded; A3: - seq2 is bounded by A2,Th19; seq1 - seq2 = seq1 + (- seq2) by BHSP_1:71; hence thesis by A1,A3,Th18; end; theorem seq is bounded implies a * seq is bounded proof assume seq is bounded; then consider M such that A1: M > 0 and A2: for n holds ||.seq.n.|| <= M by Def3; A3: a = 0 implies a * seq is bounded proof assume A4: a = 0; now let n; ||.(a * seq).n.|| = ||.0 * (seq.n).|| by A4,NORMSP_1:def 8 .= ||.0'(X).|| by RLVECT_1:23 .= 0 by BHSP_1:32; hence ||.(a * seq).n.|| <= M by A1; end; hence thesis by A1,Def3; end; a <> 0 implies a * seq is bounded proof assume a <> 0; then abs(a) > 0 by ABSVALUE:6; then A5: abs(a) * M > 0 by A1,REAL_2:122; now let n; A6: ||.seq.n.|| <= M by A2; A7: ||.(a * seq).n.|| = ||.a * (seq.n).|| by NORMSP_1:def 8 .= abs(a) * ||.seq.n.|| by BHSP_1:33; abs(a) >= 0 by ABSVALUE:5; hence ||.(a * seq).n.|| <= abs(a) * M by A6,A7,AXIOMS:25; end; hence thesis by A5,Def3; end; hence thesis by A3; end; theorem seq is constant implies seq is bounded proof assume seq is constant; then consider x such that A1: for n holds seq.n = x by NORMSP_1:def 4; A2: x = 0'(X) implies seq is bounded proof assume A3: x = 0'(X); consider M being real number such that A4: M > 0 by REAL_1:76; reconsider M as Real by XREAL_0:def 1; now let n; seq.n = 0'(X) by A1,A3; hence ||.seq.n.|| <= M by A4,BHSP_1:32; end; hence thesis by A4,Def3; end; x <> 0'(X) implies seq is bounded proof assume x <> 0'(X); then A5: ||.x.|| >= 0 & ||.x.|| <> 0 by BHSP_1:32,34; consider M being real number such that A6: ||.x.|| < M by REAL_1:76; reconsider M as Real by XREAL_0:def 1; for n holds ||.seq.n.|| <= M by A1,A6; hence thesis by A5,A6,Def3; end; hence thesis by A2; end; theorem Th23: for m ex M st ( M > 0 & for n st n <= m holds ||.seq.n.|| < M ) proof defpred _P[Nat] means ex M st ( M > 0 & for n st n <= $1 holds ||.seq.n.|| < M ); A1: _P[0] proof take M = ||.(seq.0).|| + 1; ||.(seq.0).|| >= 0 by BHSP_1:34; then ||.(seq.0).|| + 1 > 0 + 0 by REAL_1:67; hence M > 0; let n such that A2: n <= 0; n = 0 by A2,NAT_1:18; then ||.seq.n.|| + 0 < M by REAL_1:67; hence ||.seq.n.|| < M; end; A3: for m st _P[m] holds _P[m+1] proof let m; given M1 such that A4: M1 > 0 and A5: for n st n <= m holds ||.seq.n.|| < M1; A6: now assume A7: ||.seq.(m+1).|| <= M1; take M = M1 + 1; M1 + 1 > 0 + 0 by A4,REAL_1:67; hence M > 0; let n such that A8: n <= m + 1; A9: now assume m >= n; then A10: ||.seq.n.|| < M1 by A5; M > M1 + 0 by REAL_1:67; hence ||.seq.n.|| < M by A10,AXIOMS:22; end; now assume A11: n = m + 1; M > M1 + 0 by REAL_1:67; hence ||.seq.n.|| < M by A7,A11,AXIOMS:22; end; hence ||.seq.n.|| < M by A8,A9,NAT_1:26; end; now assume A12: ||.seq.(m+1).|| >= M1; take M = ||.seq.(m+1).|| + 1; ||.seq.(m+1).|| >= 0 by BHSP_1:34; then M > 0 + 0 by REAL_1:67; hence M > 0; let n such that A13: n <= m + 1; A14: now assume m >= n; then ||.seq.n.|| < M1 by A5; then ||.seq.n.|| < ||.seq.(m+1).|| by A12,AXIOMS:22; then ||.seq.n.|| + 0 < M by REAL_1:67; hence ||.seq.n.|| < M; end; now assume n = m + 1; then ||.seq.n.|| + 0 < M by REAL_1:67; hence ||.seq.n.|| < M; end; hence ||.seq.n.|| < M by A13,A14,NAT_1:26; end; hence ex M st ( M > 0 & for n st n <= m + 1 holds ||.seq.n.|| < M ) by A6; end; thus for m holds _P[m] from Ind(A1,A3); end; theorem Th24: seq is convergent implies seq is bounded proof assume seq is convergent; then consider g such that A1: for r st r > 0 ex m st for n st n >= m holds ||.seq.n - g.|| < r by BHSP_2:9; consider m1 such that A2: for n st n >= m1 holds ||.seq.n - g.|| < 1 by A1; A3: now take p = ||.g.|| + 1; ||.g.|| >= 0 by BHSP_1:34; then 0 + 0 < p by REAL_1:67; hence p > 0; let n; assume n >= m1; then A4: ||.seq.n - g.|| < 1 by A2; ||.seq.n.|| - ||.g.|| <= ||.seq.n - g.|| by BHSP_1:38; then ||.seq.n.|| - ||.g.|| < 1 by A4,AXIOMS:22; hence ||.seq.n.|| < p by REAL_1:84; end; now consider M1 such that A5: M1 > 0 and A6: for n st n >= m1 holds ||.seq.n.|| < M1 by A3; consider M2 such that A7: M2 > 0 and A8: for n st n <= m1 holds ||.seq.n.|| < M2 by Th23; take M = M1 + M2; M > 0 + 0 by A5,A7,REAL_1:67; hence M > 0; A9: M > M1 + 0 by A7,REAL_1:67; A10: M > 0 + M2 by A5,REAL_1:67; let n; A11: now assume n >= m1; then ||.seq.n.|| < M1 by A6; hence ||.seq.n.|| <= M by A9,AXIOMS:22; end; now assume n <= m1; then ||.seq.n.|| < M2 by A8; hence ||.seq.n.|| <= M by A10,AXIOMS:22; end; hence ||.seq.n.|| <= M by A11; end; hence thesis by Def3; end; theorem seq1 is bounded & seq1 is_compared_to seq2 implies seq2 is bounded proof assume that A1: seq1 is bounded and A2: seq1 is_compared_to seq2; consider p such that A3: p > 0 and A4: for n holds ||.seq1.n.|| <= p by A1,Def3; consider m1 such that A5: for n st n >= m1 holds dist((seq1.n), (seq2.n)) < 1 by A2,Def2; A6: p + 1 > 0 + 0 by A3,REAL_1:67; A7: ex M st ( M > 0 & for n st n >= m1 holds ||.seq2.n.|| < M ) proof take M = p + 1; now let n; assume n >= m1; then dist((seq1.n), (seq2.n)) < 1 by A5; then A8: ||.seq2.n - seq1.n.|| < 1 by BHSP_1:def 5; ||.seq2.n.|| - ||.seq1.n.|| <= ||.seq2.n - seq1.n.|| by BHSP_1:38; then ||.seq2.n.|| - ||.seq1.n.|| < 1 by A8,AXIOMS:22; then A9: ||.seq2.n.|| < ||.seq1.n.|| + 1 by REAL_1:84; ||.seq1.n.|| <= p by A4; then ||.seq1.n.|| + 1 <= p + 1 by AXIOMS:24; hence ||.seq2.n.|| < M by A9,AXIOMS:22; end; hence thesis by A6; end; now consider M1 such that A10: M1 > 0 and A11: for n st n >= m1 holds ||.seq2.n.|| < M1 by A7; consider M2 such that A12: M2 > 0 and A13: for n st n <= m1 holds ||.seq2.n.|| < M2 by Th23; take M = M1 + M2; M > 0 + 0 by A10,A12,REAL_1:67; hence M > 0; A14: M > M1 + 0 by A12,REAL_1:67; A15: M > 0 + M2 by A10,REAL_1:67; let n; A16: now assume n >= m1; then ||.seq2.n.|| < M1 by A11; hence ||.seq2.n.|| <= M by A14,AXIOMS:22; end; now assume n <= m1; then ||.seq2.n.|| < M2 by A13; hence ||.seq2.n.|| <= M by A15,AXIOMS:22; end; hence ||.seq2.n.|| <= M by A16; end; hence thesis by Def3; end; definition let X, Nseq, seq; redefine func seq * Nseq -> sequence of X; coherence proof A1: dom Nseq = NAT by FUNCT_2:def 1; A2: rng seq c= the carrier of X by RELSET_1:12; rng Nseq c= NAT by SEQM_3:def 8; then rng Nseq c= dom seq by FUNCT_2:def 1; then A3: dom (seq * Nseq) = NAT by A1,RELAT_1:46; rng (seq * Nseq) c= rng seq by RELAT_1:45; then rng (seq * Nseq) c= the carrier of X by A2,XBOOLE_1:1; then seq * Nseq is Function of NAT, the carrier of X by A3,FUNCT_2:def 1,RELSET_1:11; hence thesis by NORMSP_1:def 3; end; end; definition let X be non empty 1-sorted, s1, s be sequence of X; pred s1 is_subsequence_of s means :Def4: ex N being increasing Seq_of_Nat st s1 = s * N; end; theorem Th26: for X being RealUnitarySpace, s being sequence of X, N being increasing Seq_of_Nat for n being Nat holds (s * N).n=s.(N.n) proof let X be RealUnitarySpace, s be sequence of X, N be increasing Seq_of_Nat; let n be Nat; dom (s * N) = NAT by FUNCT_2:def 1; hence (s * N).n = s.(N.n) by FUNCT_1:22; end; theorem seq is_subsequence_of seq proof deffunc _F(Nat) = $1; consider Rseq such that A1: for n holds Rseq.n = _F(n) from ExRealSeq; now let n; Rseq.n = n & Rseq.(n+1) = n+1 by A1; hence Rseq.n < Rseq.(n+1) by NAT_1:38; end; then A2: Rseq is increasing by SEQM_3:def 11; for n holds Rseq.n is Nat by A1; then reconsider Rseq as increasing Seq_of_Nat by A2,SEQM_3:29; take Nseq = Rseq; now let n; thus (seq * Nseq).n = seq.(Nseq.n) by Th26 .= seq.n by A1; end; hence thesis by FUNCT_2:113; end; theorem seq1 is_subsequence_of seq2 & seq2 is_subsequence_of seq3 implies seq1 is_subsequence_of seq3 proof assume that A1: seq1 is_subsequence_of seq2 and A2: seq2 is_subsequence_of seq3; consider Nseq1 such that A3: seq1 = seq2 * Nseq1 by A1,Def4; consider Nseq2 such that A4: seq2 = seq3 * Nseq2 by A2,Def4; take Nseq = Nseq2 * Nseq1; thus seq1 = seq3 * Nseq by A3,A4,RELAT_1:55; end; theorem Th29: seq is constant & seq1 is_subsequence_of seq implies seq1 is constant proof assume that A1: seq is constant and A2: seq1 is_subsequence_of seq; consider Nseq such that A3: seq1 = seq * Nseq by A2,Def4; now let n; seq.(Nseq.n) = seq.(Nseq.(n + 1)) by A1,BHSP_1:70; then (seq * Nseq).(n + 1) = seq.(Nseq.n) by Th26; hence seq1.n = seq1.(n+1) by A3,Th26; end; hence thesis by BHSP_1:68; end; theorem seq is constant & seq1 is_subsequence_of seq implies seq = seq1 proof assume that A1: seq is constant and A2: seq1 is_subsequence_of seq; consider Nseq such that A3: seq1 = seq * Nseq by A2,Def4; now let n; thus seq1.n = seq.(Nseq.n) by A3,Th26 .= seq.n by A1,BHSP_1:70; end; hence thesis by FUNCT_2:113; end; theorem Th31: seq is bounded & seq1 is_subsequence_of seq implies seq1 is bounded proof assume that A1: seq is bounded and A2: seq1 is_subsequence_of seq; consider M1 such that A3: M1 > 0 and A4: for n holds ||.seq.n.|| <= M1 by A1,Def3; consider Nseq such that A5: seq1 = seq * Nseq by A2,Def4; take M = M1; now let n; seq1.n = seq.(Nseq.n) by A5,Th26; hence ||.seq1.n.|| <= M by A4; end; hence thesis by A3; end; theorem Th32: seq is convergent & seq1 is_subsequence_of seq implies seq1 is convergent proof assume that A1: seq is convergent and A2: seq1 is_subsequence_of seq; consider g1 such that A3: for r st r > 0 ex m st for n st n >= m holds ||.(seq.n) - g1.|| < r by A1,BHSP_2:9; consider Nseq such that A4: seq1 = seq * Nseq by A2,Def4; now let r; assume r > 0; then consider m1 such that A5: for n st n >= m1 holds ||.(seq.n) - g1.|| < r by A3; take m = m1; let n such that A6: n >= m; Nseq.n >= n by SEQM_3:33; then A7: Nseq.n >= m by A6,AXIOMS:22; seq1.n = seq.(Nseq.n) by A4,Th26; hence ||.(seq1.n) - g1.|| < r by A5,A7; end; hence thesis by BHSP_2:9; end; theorem Th33: seq1 is_subsequence_of seq & seq is convergent implies lim seq1=lim seq proof assume that A1: seq1 is_subsequence_of seq and A2: seq is convergent; A3: seq1 is convergent by A1,A2,Th32; consider Nseq such that A4: seq1 = seq * Nseq by A1,Def4; now let r; assume r > 0; then consider m1 such that A5: for n st n >= m1 holds dist((seq.n), (lim seq)) < r by A2,BHSP_2:def 2; take m = m1; let n such that A6: n >= m; Nseq.n >= n by SEQM_3:33; then A7: Nseq.n >= m by A6,AXIOMS:22; seq1.n = seq.(Nseq.n) by A4,Th26; hence dist((seq1.n), (lim seq)) < r by A5,A7; end; hence thesis by A3,BHSP_2:def 2; end; theorem Th34: seq is_Cauchy_sequence & seq1 is_subsequence_of seq implies seq1 is_Cauchy_sequence proof assume that A1: seq is_Cauchy_sequence and A2: seq1 is_subsequence_of seq; consider Nseq such that A3: seq1 = seq * Nseq by A2,Def4; now let r; assume r > 0; then consider l such that A4: for n, m st ( n >= l & m >= l ) holds dist((seq.n), (seq.m)) < r by A1,Def1; take k = l; let n, m such that A5: n >= k & m >= k; Nseq.n >= n & Nseq.m >= m by SEQM_3:33; then A6: Nseq.n >= k & Nseq.m >= k by A5,AXIOMS:22; seq1.n = seq.(Nseq.n) & seq1.m = seq.(Nseq.m) by A3,Th26; hence dist((seq1.n), (seq1.m)) < r by A4,A6; end; hence thesis by Def1; end; definition let X; let seq; let k; func seq ^\k -> sequence of X means :Def5: for n holds it.n=seq.(n + k); existence proof deffunc _F(Nat) = seq.($1 + k); thus ex IT being sequence of X st for n holds IT.n=_F(n) from Ex_Seq_in_RUS; end; uniqueness proof let seq1, seq2; assume that A1: for n holds seq1.n = seq.(n + k) and A2: for n holds seq2.n = seq.(n + k); now let n; seq1.n = seq.(n + k) by A1; hence seq1.n = seq2.n by A2; end; hence seq1 = seq2 by FUNCT_2:113; end; end; theorem seq ^\0 = seq proof now let n; thus (seq ^\0).n = seq.(n + 0) by Def5 .= seq.n; end; hence thesis by FUNCT_2:113; end; theorem (seq ^\k)^\m = (seq ^\m)^\k proof now let n; thus ((seq ^\k)^\m).n = (seq ^\k).(n + m) by Def5 .= seq.(n + m + k) by Def5 .= seq.(n + k + m) by XCMPLX_1:1 .= (seq ^\m).(n + k) by Def5 .= ((seq ^\m)^\k).n by Def5; end; hence thesis by FUNCT_2:113; end; theorem (seq ^\k)^\m=seq ^\(k + m) proof now let n; thus ((seq ^\k)^\m).n = (seq ^\k).(n + m) by Def5 .= seq.(n + m + k) by Def5 .= seq.(n + (k + m)) by XCMPLX_1:1 .= (seq ^\(k + m)).n by Def5; end; hence thesis by FUNCT_2:113; end; theorem Th38: (seq1 + seq2) ^\k = (seq1 ^\k) + (seq2 ^\k) proof now let n; thus ((seq1 + seq2) ^\k).n = (seq1 + seq2).(n + k) by Def5 .= seq1.(n + k) + seq2.(n + k) by NORMSP_1:def 5 .= (seq1 ^\k).n + seq2.(n + k) by Def5 .= (seq1 ^\k).n + (seq2 ^\k).n by Def5 .= ((seq1 ^\k) + (seq2 ^\k)).n by NORMSP_1:def 5; end; hence thesis by FUNCT_2:113; end; theorem Th39: (-seq) ^\k = -(seq ^\k) proof now let n; thus ((-seq) ^\k).n = (-seq).(n + k) by Def5 .= -(seq.(n + k)) by BHSP_1:def 10 .= -((seq ^\ k).n) by Def5 .= (-(seq ^\k)).n by BHSP_1:def 10; end; hence thesis by FUNCT_2:113; end; theorem (seq1 - seq2) ^\k = (seq1 ^\k) - (seq2 ^\k) proof thus (seq1 - seq2) ^\k = (seq1 + (-seq2)) ^\k by BHSP_1:71 .= (seq1 ^\k) + ((-seq2) ^\k) by Th38 .= (seq1 ^\k) + -(seq2 ^\k) by Th39 .= (seq1 ^\k) - (seq2 ^\k) by BHSP_1:71; end; theorem (a * seq) ^\k = a * (seq ^\k) proof now let n; thus ((a * seq) ^\k).n = (a * seq).(n + k) by Def5 .= a * (seq.(n + k)) by NORMSP_1:def 8 .= a * ((seq ^\k).n) by Def5 .= (a * (seq ^\k)).n by NORMSP_1:def 8; end; hence thesis by FUNCT_2:113; end; theorem (seq * Nseq) ^\k = seq * (Nseq ^\k) proof now let n; thus ((seq * Nseq) ^\k).n = (seq * Nseq).(n + k) by Def5 .= seq.(Nseq.(n + k)) by Th26 .= seq.((Nseq ^\k).n) by SEQM_3:def 9 .= (seq * (Nseq ^\k)).n by Th26; end; hence thesis by FUNCT_2:113; end; theorem Th43: seq ^\k is_subsequence_of seq proof deffunc _F(Nat) = $1 + k; consider Rseq such that A1: for n holds Rseq.n = _F(n) from ExRealSeq; now let n; A2: Rseq.n = n + k & Rseq.(n + 1) = n + 1 + k by A1; n + k < n + k + 1 by NAT_1:38; hence Rseq.n < Rseq.(n + 1) by A2,XCMPLX_1:1; end; then A3: Rseq is increasing by SEQM_3:def 11; now let n; n + k is Nat; hence Rseq.n is Nat by A1; end; then reconsider Rseq as increasing Seq_of_Nat by A3,SEQM_3:29; take Nseq=Rseq; now let n; thus (seq * Nseq).n = seq.(Nseq.n) by Th26 .= seq.(n + k) by A1 .= (seq ^\k).n by Def5; end; hence thesis by FUNCT_2:113; end; theorem seq is convergent implies ((seq ^\k) is convergent & lim (seq ^\k)=lim seq) proof assume A1: seq is convergent; A2: seq ^\k is_subsequence_of seq by Th43; hence seq ^\k is convergent by A1,Th32; thus lim (seq ^\k) = lim seq by A1,A2,Th33; end; canceled; theorem seq is convergent & (ex k st seq = seq1 ^\k) implies seq1 is convergent proof assume that A1: seq is convergent and A2: ex k st seq = seq1 ^\k; consider k such that A3: seq = seq1 ^\k by A2; consider g1 such that A4: for r st r > 0 ex m st for n st n >= m holds ||.seq.n - g1.|| < r by A1,BHSP_2:9; now take g = g1; let r; assume r > 0; then consider m1 such that A5: for n st n >= m1 holds ||.seq.n - g.|| < r by A4; take m = m1 + k; let n; assume A6: n >= m; then consider m2 such that A7: n = m1 + k + m2 by NAT_1:28; n - k = m1 + k + m2 + -k by A7,XCMPLX_0:def 8 .= m1 + m2 + k + -k by XCMPLX_1:1 .= m1 + m2 + k - k by XCMPLX_0:def 8 .= m1 + m2 + (k - k) by XCMPLX_1:29 .= m1 + m2 + 0 by XCMPLX_1:14 .= m1 + m2; then consider l such that A8: l = n - k; A9: now assume l < m1; then l + k < m1 + k by REAL_1:53; then n - (k - k) < m1 + k by A8,XCMPLX_1:37; then n - 0 < m1 + k by XCMPLX_1:14; hence contradiction by A6; end; A10: l + k = n - (k - k) by A8,XCMPLX_1:37 .= n - 0 by XCMPLX_1:14 .= n; ||.seq.l - g.|| < r by A5,A9; hence ||.seq1.n - g.|| < r by A3,A10,Def5; end; hence thesis by BHSP_2:9; end; theorem seq is_Cauchy_sequence & (ex k st seq = seq1 ^\k) implies seq1 is_Cauchy_sequence proof assume that A1: seq is_Cauchy_sequence and A2: ex k st seq = seq1 ^\k; consider k such that A3: seq = seq1 ^\k by A2; let r; assume r > 0; then consider l1 such that A4: for n, m st ( n >= l1 & m >= l1 ) holds dist((seq.n), (seq.m)) < r by A1,Def1; take l = l1 + k; let n, m; assume A5: n >= l & m >= l; then consider m1 such that A6: n = l1 + k + m1 by NAT_1:28; A7: n - k = l1 + k + m1 + -k by A6,XCMPLX_0:def 8 .= l1 + m1 + k + -k by XCMPLX_1:1 .= l1 + m1 + k - k by XCMPLX_0:def 8 .= l1 + m1 + (k - k) by XCMPLX_1:29 .= l1 + m1 + 0 by XCMPLX_1:14 .= l1 + m1; consider m2 such that A8: m = l1 + k + m2 by A5,NAT_1:28; A9: m - k = l1 + k + m2 + -k by A8,XCMPLX_0:def 8 .= l1 + m2 + k + -k by XCMPLX_1:1 .= l1 + m2 + k - k by XCMPLX_0:def 8 .= l1 + m2 + (k - k) by XCMPLX_1:29 .= l1 + m2 + 0 by XCMPLX_1:14 .= l1 + m2; consider l2 such that A10: l2 = n - k by A7; A11: now assume l2 < l1; then l2 + k < l1 + k by REAL_1:53; then n - (k - k) < l1 + k by A10,XCMPLX_1:37; then n - 0 < l1 + k by XCMPLX_1:14; hence contradiction by A5; end; consider l3 such that A12: l3 = m - k by A9; A13: now assume l3 < l1; then l3 + k < l1 + k by REAL_1:53; then m - (k - k) < l1 + k by A12,XCMPLX_1:37; then m - 0 < l1 + k by XCMPLX_1:14; hence contradiction by A5; end; A14: l2 + k = n - (k - k) by A10,XCMPLX_1:37 .= n - 0 by XCMPLX_1:14 .= n; A15: l3 + k = m - (k - k) by A12,XCMPLX_1:37 .= m - 0 by XCMPLX_1:14 .= m; dist((seq.l2), (seq.l3)) < r by A4,A11,A13; then dist((seq1.n), (seq.l3)) < r by A3,A14,Def5; hence dist((seq1.n), (seq1.m)) < r by A3,A15,Def5; end; theorem seq is_Cauchy_sequence implies (seq ^\k) is_Cauchy_sequence proof assume A1: seq is_Cauchy_sequence; seq ^\k is_subsequence_of seq by Th43; hence thesis by A1,Th34; end; theorem seq1 is_compared_to seq2 implies (seq1 ^\k) is_compared_to (seq2 ^\k) proof assume A1: seq1 is_compared_to seq2; let r; assume r > 0; then consider m1 such that A2: for n st n >= m1 holds dist((seq1.n), (seq2.n)) < r by A1,Def2; take m = m1; let n such that A3: n >= m; n + k >= n by NAT_1:29; then n + k >= m by A3,AXIOMS:22; then dist((seq1.(n + k)), (seq2.(n + k))) < r by A2; then dist((seq1 ^\k).n, (seq2.(n + k))) < r by Def5; hence dist((seq1 ^\k).n, (seq2 ^\k).n) < r by Def5; end; theorem seq is bounded implies (seq ^\k) is bounded proof assume A1: seq is bounded; seq ^\k is_subsequence_of seq by Th43; hence thesis by A1,Th31; end; theorem seq is constant implies (seq ^\k) is constant proof assume A1: seq is constant; seq ^\k is_subsequence_of seq by Th43; hence thesis by A1,Th29; end; definition let X; attr X is complete means :Def6: for seq holds seq is_Cauchy_sequence implies seq is convergent; synonym X is_complete_space; end; canceled; theorem X is_complete_space & seq is_Cauchy_sequence implies seq is bounded proof assume that A1: X is_complete_space and A2: seq is_Cauchy_sequence; seq is convergent by A1,A2,Def6; hence thesis by Th24; end; definition let X; attr X is Hilbert means X is RealUnitarySpace & X is_complete_space; synonym X is_Hilbert_space; end;