:: Real Normed Space
:: by Jan Popio{\l}ek
::
:: Received September 20, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, RLVECT_1, STRUCT_0, SUBSET_1, ALGSTR_0, BINOP_1,
FUNCT_1, ZFMISC_1, XBOOLE_0, REAL_1, PRE_TOPC, SUPINF_2, RLSUB_1,
FUNCOP_1, CARD_1, RELAT_1, COMPLEX1, ARYTM_3, XXREAL_0, ARYTM_1, NAT_1,
TARSKI, SEQ_2, ORDINAL2, NORMSP_1, NORMSP_0, RELAT_2, METRIC_1, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, COMPLEX1, REAL_1, NAT_1, FUNCT_1, FUNCOP_1, FUNCT_2, BINOP_1,
RELAT_1, COMSEQ_2, SEQ_2, DOMAIN_1, STRUCT_0, ALGSTR_0, PRE_TOPC,
RLVECT_1, RLSUB_1, XXREAL_0, NORMSP_0;
constructors BINOP_1, DOMAIN_1, FUNCOP_1, XXREAL_0, REAL_1, NAT_1, COMPLEX1,
SEQ_2, RLSUB_1, VALUED_1, RELSET_1, NORMSP_0, COMSEQ_2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0,
STRUCT_0, RLVECT_1, ALGSTR_0, NORMSP_0, XCMPLX_0, VALUED_0, NAT_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions RLVECT_1, STRUCT_0, ALGSTR_0;
equalities RLVECT_1, STRUCT_0, ALGSTR_0, NORMSP_0;
expansions NORMSP_0;
theorems TARSKI, NAT_1, FUNCT_1, SEQ_2, ABSVALUE, RLVECT_1, RLSUB_1, FUNCT_2,
RELSET_1, XBOOLE_0, XCMPLX_0, FUNCOP_1, XREAL_1, COMPLEX1, XXREAL_0,
ORDINAL1, ALGSTR_0, RELAT_1, NORMSP_0;
schemes FUNCT_2, NAT_1;
begin
definition
struct(RLSStruct, N-ZeroStr) NORMSTR (# carrier -> set,
ZeroF -> Element of the carrier,
addF -> BinOp of the carrier, Mult -> Function of [:REAL, the carrier:], the
carrier, normF -> Function of the carrier, REAL #);
end;
registration
cluster non empty strict for NORMSTR;
existence
proof
set A = the non empty set,Z = the Element of A,a = the BinOp of A,M =the
Function of [:REAL,A:],A,n = the Function of A,REAL;
take NORMSTR(#A,Z,a,M,n#);
thus the carrier of NORMSTR(#A,Z,a,M,n#) is non empty;
thus thesis;
end;
end;
reserve a, b for Real;
deffunc 09(NORMSTR) = 0.$1;
set V = the RealLinearSpace;
Lm1: the carrier of (0).V = {0.V} by RLSUB_1:def 3;
reconsider niltonil = (the carrier of (0).V) --> In(0,REAL)
as Function of the carrier
of (0).V, REAL;
0.V is VECTOR of (0).V by Lm1,TARSKI:def 1;
then
Lm2: niltonil.(0.V) = 0 by FUNCOP_1:7;
Lm3: for u being VECTOR of (0).V, a holds niltonil.(a * u) = |.a.| * niltonil
.u
proof
let u be VECTOR of (0).V;
let a;
niltonil.u = 0 by FUNCOP_1:7;
hence thesis by FUNCOP_1:7;
end;
Lm4: for u, v being VECTOR of (0).V holds niltonil.(u + v) <= niltonil.u +
niltonil.v
proof
let u, v be VECTOR of (0).V;
u = 0.V & v = 0.V by Lm1,TARSKI:def 1;
hence thesis by Lm1,Lm2,TARSKI:def 1;
end;
reconsider X = NORMSTR (# the carrier of (0).V, 0.(0).V, the addF of (0).V,
the Mult of (0).V, niltonil #) as non empty NORMSTR;
Lm5: now
let x, y be Point of X;
let a;
reconsider u = x, w = y as VECTOR of (0).V;
09(X) = 0.V by RLSUB_1:11;
hence ||.x.|| = 0 iff x = 09(X) by Lm1,FUNCOP_1:7,TARSKI:def 1;
a * x = a * u;
hence ||.a * x.|| = |.a.| * ||.x.|| by Lm3;
x + y = u + w;
hence ||.x + y.|| <= ||.x.|| + ||.y.|| by Lm4;
end;
definition
let IT be non empty NORMSTR;
attr IT is RealNormSpace-like means
:Def1:
for x, y being Point of IT, a holds ||.a * x.|| = |.a.| * ||.x.|| & ||.x + y
.|| <= ||.x.|| + ||.y.||;
end;
registration
cluster reflexive discerning RealNormSpace-like vector-distributive
scalar-distributive scalar-associative scalar-unital Abelian add-associative
right_zeroed right_complementable strict for non empty NORMSTR;
existence
proof
take X;
thus X is reflexive
by Lm5;
thus X is discerning by Lm5;
thus X is RealNormSpace-like by Lm5;
thus X is vector-distributive scalar-distributive scalar-associative
scalar-unital
proof
thus for a being Real for v,w being VECTOR of X holds a * (v + w)
= a * v + a * w
proof
let a be Real;
let v,w be VECTOR of X;
reconsider v9= v, w9 = w as VECTOR of (0).V;
thus a * (v + w) = a *( v9 + w9) .= a * v9 + a * w9 by RLVECT_1:def 5
.= a * v + a * w;
end;
thus for a,b being Real for v being VECTOR of X holds (a + b) * v
= a * v + b * v
proof
let a,b be Real;
let v be VECTOR of X;
reconsider v9= v as VECTOR of (0).V;
thus (a + b) * v = (a + b) * v9 .= a * v9 + b * v9 by RLVECT_1:def 6
.= a * v + b * v;
end;
thus for a,b being Real for v being VECTOR of X holds (a * b) * v
= a * (b * v)
proof
let a,b be Real;
let v be VECTOR of X;
reconsider v9= v as VECTOR of (0).V;
thus (a * b) * v = (a * b) * v9
.= a * (b * v9) by RLVECT_1:def 7
.= a * (b * v);
end;
let v be VECTOR of X;
reconsider v9= v as VECTOR of (0).V;
thus 1 * v = 1 * v9 .= v by RLVECT_1:def 8;
end;
A1: for x,y be VECTOR of X for x9,y9 be VECTOR of (0).V st x = x9 & y = y9
holds x + y= x9 + y9 & for a holds a * x = a * x9;
thus for v,w being VECTOR of X holds v + w = w + v
proof
let v,w be VECTOR of X;
reconsider v9= v, w9= w as VECTOR of (0).V;
thus v + w = w9+ v9 by A1
.= w + v;
end;
thus for u,v,w being VECTOR of X holds (u + v) + w = u + (v + w)
proof
let u,v,w be VECTOR of X;
reconsider u9= u, v9= v, w9= w as VECTOR of (0).V;
thus (u + v) + w = (u9 + v9) + w9 .= u9 + (v9 + w9) by RLVECT_1:def 3
.= u + (v + w);
end;
thus for v being VECTOR of X holds v + 0.X = v
proof
let v be VECTOR of X;
reconsider v9= v as VECTOR of (0).V;
thus v + 0.X = v9+ 0.(0).V .=v;
end;
thus X is right_complementable
proof
let v be VECTOR of X;
reconsider v9= v as VECTOR of (0).V;
consider w9 be VECTOR of (0).V such that
A2: v9 + w9 = 0.(0).V by ALGSTR_0:def 11;
reconsider w = w9 as VECTOR of X;
take w;
thus thesis by A2;
end;
thus thesis;
end;
end;
definition
mode RealNormSpace is reflexive discerning RealNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable
non empty NORMSTR;
end;
reserve RNS for RealNormSpace;
reserve x, y, z, g, g1, g2 for Point of RNS;
theorem
||.0.RNS.|| = 0;
theorem Th2:
||.-x.|| = ||.x.||
proof
A1: |.-1.| = -(-1) by ABSVALUE:def 1
.= 1;
||.-x.|| = ||.(-1) * x.|| by RLVECT_1:16
.= |.-1.| * ||.x.|| by Def1;
hence thesis by A1;
end;
theorem Th3:
||.x - y.|| <= ||.x.|| + ||.y.||
proof
||.x - y.|| <= ||.x.|| + ||.(-y).|| by Def1;
hence thesis by Th2;
end;
theorem Th4:
0 <= ||.x.||
proof
||.x - x.|| = ||.09(RNS).|| by RLVECT_1:15
.= 0;
then 0 <= (||.x.|| + ||.x.||)/2 by Th3;
hence thesis;
end;
registration
let RNS,x;
cluster ||.x.|| -> non negative;
coherence by Th4;
end;
theorem
||.a * x + b * y.|| <= |.a.| * ||.x.|| + |.b.| * ||.y.||
proof
||.a * x + b * y.|| <= ||.a * x.|| + ||.b * y.|| by Def1;
then ||.a * x + b * y.|| <= |.a.| * ||.x.|| + ||.b * y.|| by Def1;
hence thesis by Def1;
end;
theorem Th6:
||.x - y.|| = 0 iff x = y
proof
||.x - y.|| = 0 iff x - y = 09(RNS) by NORMSP_0:def 5;
hence thesis by RLVECT_1:15,21;
end;
theorem Th7:
||.x - y.|| = ||.y - x.||
proof
x - y = - (y - x) by RLVECT_1:33;
hence thesis by Th2;
end;
theorem Th8:
||.x.|| - ||.y.|| <= ||.x - y.||
proof
(x - y) + y = x - (y - y) by RLVECT_1:29
.= x - 09(RNS) by RLVECT_1:15
.= x;
then ||.x.|| <= ||.x - y.|| + ||.y.|| by Def1;
hence thesis by XREAL_1:20;
end;
theorem Th9:
|.||.x.|| - ||.y.||.| <= ||.x - y.||
proof
(y - x) + x = y - (x - x) by RLVECT_1:29
.= y - 09(RNS) by RLVECT_1:15
.= y;
then ||.y.|| <= ||.y - x.|| + ||.x.|| by Def1;
then ||.y.|| - ||.x.|| <= ||.y - x.|| by XREAL_1:20;
then ||.y.|| - ||.x.|| <= ||.x - y.|| by Th7;
then
A1: -(||.y.|| - ||.x.||) >= -||.x - y.|| by XREAL_1:24;
||.x.|| - ||.y.|| <= ||.x - y.|| by Th8;
hence thesis by A1,ABSVALUE:5;
end;
theorem Th10:
||.x - z.|| <= ||.x - y.|| + ||.y - z.||
proof
x - z = x + (09(RNS) + (-z))
.= x + (((-y) + y) + (-z)) by RLVECT_1:5
.= x + ((-y) + (y + (-z))) by RLVECT_1:def 3
.= (x - y) + (y - z) by RLVECT_1:def 3;
hence thesis by Def1;
end;
theorem
x <> y implies ||.x - y.|| <> 0 by Th6;
reserve S, S1, S2 for sequence of RNS;
reserve k, n, m, m1, m2 for Nat;
reserve r for Real;
reserve f for Function;
reserve d, s, t for set;
theorem
for RNS being non empty 1-sorted, x being Element of RNS holds f is
sequence of RNS iff ( dom f = NAT & for d st d in NAT holds f.d is Element of
RNS )
proof
let RNS be non empty 1-sorted;
let x be Element of RNS;
thus f is sequence of RNS implies ( dom f = NAT & for d st d in NAT holds f.
d is Element of RNS )
proof
assume
A1: f is sequence of RNS;
then
A2: rng f c= the carrier of RNS by RELAT_1:def 19;
A3: dom f = NAT by A1,FUNCT_2:def 1;
for d st d in NAT holds f.d is Element of RNS
proof
let d;
assume d in NAT;
then f.d in rng f by A3,FUNCT_1:def 3;
hence thesis by A2;
end;
hence thesis by A1,FUNCT_2:def 1;
end;
thus ( dom f = NAT & for d st d in NAT holds f.d is Element of RNS ) implies
f is sequence of RNS
proof
assume that
A4: dom f = NAT and
A5: for d st d in NAT holds f.d is Element of RNS;
for s being object st s in rng f holds s in the carrier of RNS
proof
let s be object;
assume s in rng f;
then consider d being object such that
A6: d in dom f and
A7: s = f.d by FUNCT_1:def 3;
f.d is Element of RNS by A4,A5,A6;
hence thesis by A7;
end;
then rng f c= the carrier of RNS by TARSKI:def 3;
hence thesis by A4,FUNCT_2:def 1,RELSET_1:4;
end;
end;
theorem
for RNS being non empty 1-sorted, x being Element of RNS ex S being
sequence of RNS st rng S = {x}
proof
let RNS be non empty 1-sorted;
let x be Element of RNS;
consider f such that
A1: dom f = NAT and
A2: rng f = {x} by FUNCT_1:5;
reconsider f as sequence of RNS by A1,A2,FUNCT_2:def 1,RELSET_1:4;
take f;
thus thesis by A2;
end;
theorem
for RNS being non empty 1-sorted, S being sequence of RNS st (ex x
being Element of RNS st for n being Nat holds S.n = x) ex x being Element of
RNS st rng S={x}
proof
let RNS be non empty 1-sorted;
let S be sequence of RNS;
given z being Element of RNS such that
A1: for n being Nat holds S.n = z;
take x = z;
now
let s be object;
assume s in {x}; then
A2: s = x by TARSKI:def 1;
now
assume
A3: not s in rng S;
now
let n;
n in NAT by ORDINAL1:def 12;
then n in dom S by FUNCT_2:def 1;
then S.n <> x by A2,A3,FUNCT_1:def 3;
hence contradiction by A1;
end;
hence contradiction;
end;
hence s in rng S;
end;
then
A4: {x} c= rng S by TARSKI:def 3;
now
let t be object;
assume t in rng S;
then consider d being object such that
A5: d in dom S and
A6: S.d = t by FUNCT_1:def 3;
d in NAT by A5,FUNCT_2:def 1;
then t = z by A1,A6;
hence t in {x} by TARSKI:def 1;
end;
then rng S c= {x} by TARSKI:def 3;
hence thesis by A4,XBOOLE_0:def 10;
end;
theorem
for RNS being non empty 1-sorted, S being sequence of RNS st ex x
being Element of RNS st rng S = {x} holds for n holds S.n = S.(n+1)
proof
let RNS be non empty 1-sorted;
let S be sequence of RNS;
given z being Element of RNS such that
A1: rng S = {z};
let n;
n in NAT by ORDINAL1:def 12;
then n in dom S by FUNCT_2:def 1;
then S.n in {z} by A1,FUNCT_1:def 3;
then
A2: S.n = z by TARSKI:def 1;
(n+1) in NAT;
then (n+1) in dom S by FUNCT_2:def 1;
then S.(n+1) in {z} by A1,FUNCT_1:def 3;
hence thesis by A2,TARSKI:def 1;
end;
theorem
for RNS being non empty 1-sorted, S being sequence of RNS st for n
holds S.n = S.(n+1) holds for n, k holds S.n = S.(n+k)
proof
let RNS be non empty 1-sorted;
let S be sequence of RNS;
assume
A1: for n holds S.n = S.(n+1);
let n;
defpred P[Nat] means S.n = S.(n+$1);
A2: now
let k such that
A3: P[k];
S.(n+k) = S.(n+k+1) by A1;
hence P[k+1] by A3;
end;
A4: P[0];
thus for k holds P[k] from NAT_1:sch 2(A4,A2);
end;
theorem
for RNS being non empty 1-sorted, S being sequence of RNS st for n, k
holds S.n = S.(n+k) holds for n, m holds S.n = S.m
proof
let RNS be non empty 1-sorted;
let S be sequence of RNS;
assume
A1: for n, k holds S.n = S.(n+k);
let n, m;
A2: now
assume m <= n;
then consider k being Nat such that
A3: n = m + k by NAT_1:10;
reconsider k as Nat;
n=m+k by A3;
hence thesis by A1;
end;
now
assume n <= m;
then consider k being Nat such that
A4: m = n + k by NAT_1:10;
reconsider k as Nat;
m=n+k by A4;
hence thesis by A1;
end;
hence thesis by A2;
end;
theorem
for RNS being non empty 1-sorted, S being sequence of RNS st for n, m
holds S.n = S.m ex x being Element of RNS st for n being Nat holds S.n = x
proof
let RNS be non empty 1-sorted;
let S be sequence of RNS;
assume that
A1: for n, m holds S.n = S.m and
A2: for x being Element of RNS ex n being Nat st S.n <> x;
now
let n;
set z = S.n;
consider k being Nat such that
A3: S.k <> z by A2;
thus contradiction by A1,A3;
end;
hence thesis;
end;
definition
let RNS be non empty addLoopStr;
let S1, S2 be sequence of RNS;
func S1 + S2 -> sequence of RNS means
:Def2:
for n holds it.n = S1.n + S2.n;
existence
proof
deffunc F(Nat) = S1.$1 + S2.$1;
consider S being sequence of RNS such that
A1: for n being Element of NAT holds S.n = F(n) from FUNCT_2:sch 4;
take S;
let n;
n in NAT by ORDINAL1:def 12;
hence thesis by A1;
end;
uniqueness
proof
let S, T be sequence of RNS;
assume that
A2: for n holds S.n = S1.n + S2.n and
A3: for n holds T.n = S1.n + S2.n;
for n be Element of NAT holds S.n = T.n
proof
let n be Element of NAT;
S.n = S1.n + S2.n by A2;
hence thesis by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
definition
let RNS be non empty addLoopStr;
let S1, S2 be sequence of RNS;
func S1 - S2 -> sequence of RNS means
:Def3:
for n holds it.n = S1.n - S2.n;
existence
proof
deffunc F(Nat) = S1.$1 - S2.$1;
consider S being sequence of RNS such that
A1: for n being Element of NAT holds S.n = F(n) from FUNCT_2:sch 4;
take S;
let n;
n in NAT by ORDINAL1:def 12;
hence thesis by A1;
end;
uniqueness
proof
let S, T be sequence of RNS;
assume that
A2: for n holds S.n = S1.n - S2.n and
A3: for n holds T.n = S1.n - S2.n;
for n being Element of NAT holds S.n = T.n
proof
let n be Element of NAT;
S.n = S1.n - S2.n by A2;
hence thesis by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
definition
let RNS be non empty addLoopStr;
let S be sequence of RNS;
let x be Element of RNS;
func S - x -> sequence of RNS means
:Def4:
for n holds it.n = S.n - x;
existence
proof
deffunc F(Nat) = S.$1 - x;
consider S being sequence of RNS such that
A1: for n being Element of NAT holds S.n = F(n) from FUNCT_2:sch 4;
take S;
let n;
n in NAT by ORDINAL1:def 12;
hence thesis by A1;
end;
uniqueness
proof
let S1, S2 be sequence of RNS;
assume that
A2: for n holds S1.n = S.n - x and
A3: for n holds S2.n = S.n - x;
for n being Element of NAT holds S1.n = S2.n
proof
let n be Element of NAT;
S1.n = S.n - x by A2;
hence thesis by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
definition
let RNS be non empty RLSStruct;
let S be sequence of RNS;
let a be Real;
func a * S -> sequence of RNS means
:Def5:
for n holds it.n = a * S.n;
existence
proof
deffunc F(Nat) = a * S.$1;
consider S being sequence of RNS such that
A1: for n being Element of NAT holds S.n = F(n) from FUNCT_2:sch 4;
take S;
let n;
n in NAT by ORDINAL1:def 12;
hence thesis by A1;
end;
uniqueness
proof
let S1, S2 be sequence of RNS;
assume that
A2: for n holds S1.n = a * S.n and
A3: for n holds S2.n = a * S.n;
for n being Element of NAT holds S1.n = S2.n
proof
let n be Element of NAT;
S1.n = a * S.n by A2;
hence thesis by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
definition
let RNS, S;
attr S is convergent means
ex g st for r st 0 < r ex m st for n st m <= n holds ||.(S.n) - g.|| < r;
end;
theorem Th19:
S1 is convergent & S2 is convergent implies S1 + S2 is convergent
proof
assume that
A1: S1 is convergent and
A2: S2 is convergent;
consider g1 such that
A3: for r st 0 < r ex m st for n st m <= n holds ||.(S1.n) - g1.|| < r
by A1;
consider g2 such that
A4: for r st 0 < r ex m st for n st m <= n holds ||.(S2.n) - g2.|| < r
by A2;
take g = g1 + g2;
let r;
assume
A5: 0 < r;
then consider m1 such that
A6: for n st m1 <= n holds ||.(S1.n) - g1.|| < r/2 by A3;
consider m2 such that
A7: for n st m2 <= n holds ||.(S2.n) - g2.|| < r/2 by A4,A5;
take k = m1 + m2;
let n such that
A8: k <= n;
m2 <= k by NAT_1:12;
then m2 <= n by A8,XXREAL_0:2;
then
A9: ||.(S2.n) - g2.|| < r/2 by A7;
A10: ||.(S1 + S2).n - g.|| = ||.-(g1+g2) + ((S1.n) + (S2.n)).|| by Def2
.= ||.((-g1)+(-g2)) + ((S1.n) + (S2.n)).|| by RLVECT_1:31
.= ||.(S1.n) + ((-g1)+(-g2)) + (S2.n).|| by RLVECT_1:def 3
.= ||.(S1.n) - g1 + (-g2) + (S2.n).|| by RLVECT_1:def 3
.= ||.(S1.n) - g1 + ((S2.n) - g2).|| by RLVECT_1:def 3;
A11: ||.(S1.n) - g1 + ((S2.n) - g2).|| <= ||.(S1.n) - g1.|| + ||.(S2.n) - g2
.|| by Def1;
m1 <= m1 + m2 by NAT_1:12;
then m1 <= n by A8,XXREAL_0:2;
then ||.(S1.n) - g1.|| < r/2 by A6;
then ||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| < r/2 + r/2 by A9,XREAL_1:8;
hence thesis by A10,A11,XXREAL_0:2;
end;
theorem Th20:
S1 is convergent & S2 is convergent implies S1 - S2 is convergent
proof
assume that
A1: S1 is convergent and
A2: S2 is convergent;
consider g1 such that
A3: for r st 0 < r ex m st for n st m <= n holds ||.(S1.n) - g1.|| < r
by A1;
consider g2 such that
A4: for r st 0 < r ex m st for n st m <= n holds ||.(S2.n) - g2.|| < r
by A2;
take g = g1 - g2;
let r;
assume
A5: 0 < r;
then consider m1 such that
A6: for n st m1 <= n holds ||.(S1.n) - g1.|| < r/2 by A3;
consider m2 such that
A7: for n st m2 <= n holds ||.(S2.n) - g2.|| < r/2 by A4,A5;
take k = m1 + m2;
let n such that
A8: k <= n;
m2 <= k by NAT_1:12;
then m2 <= n by A8,XXREAL_0:2;
then
A9: ||.(S2.n) - g2.|| < r/2 by A7;
A10: ||.(S1 - S2).n - g.|| = ||.((S1.n) - (S2.n)) - (g1 - g2).|| by Def3
.= ||.(((S1.n) - (S2.n)) - g1) + g2.|| by RLVECT_1:29
.= ||. ((S1.n) - (g1 + (S2.n))) + g2.|| by RLVECT_1:27
.= ||. (((S1.n) - g1 ) - (S2.n)) + g2.|| by RLVECT_1:27
.= ||. ((S1.n) - g1 ) - ((S2.n) - g2).|| by RLVECT_1:29;
A11: ||.((S1.n) - g1) - ((S2.n) - g2).|| <= ||.(S1.n) - g1.|| + ||.(S2.n) -
g2.|| by Th3;
m1 <= m1 + m2 by NAT_1:12;
then m1 <= n by A8,XXREAL_0:2;
then ||.(S1.n) - g1.|| < r/2 by A6;
then ||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| < r/2 + r/2 by A9,XREAL_1:8;
hence thesis by A10,A11,XXREAL_0:2;
end;
theorem Th21:
S is convergent implies S - x is convergent
proof
assume S is convergent;
then consider g such that
A1: for r st 0 < r ex m st for n st m <= n holds ||.(S.n) - g.|| < r;
take h = g - x;
let r;
assume 0 < r;
then consider m1 such that
A2: for n st m1 <= n holds ||.(S.n) - g.|| < r by A1;
take k = m1;
let n;
assume k <= n;
then
A3: ||.(S.n) - g.|| < r by A2;
||.(S.n) - g.|| = ||.((S.n) - 09(RNS)) - g.||
.= ||.((S.n) - (x - x)) - g.|| by RLVECT_1:15
.= ||.(((S.n) - x) + x) - g.|| by RLVECT_1:29
.= ||.((S.n) - x) + ((-g) + x).|| by RLVECT_1:def 3
.= ||.((S.n) - x) - h.|| by RLVECT_1:33;
hence thesis by A3,Def4;
end;
theorem Th22:
S is convergent implies a * S is convergent
proof
assume S is convergent;
then consider g such that
A1: for r st 0 < r ex m st for n st m <= n holds ||.(S.n) - g.|| < r;
take h = a * g;
A2: now
assume
A3: a <> 0; then
A4: 0 < |.a.| by COMPLEX1:47;
let r;
assume 0 < r;
then consider m1 such that
A5: for n st m1 <= n holds ||.(S.n) - g.|| < r/|.a.| by A1,A4;
take k = m1;
let n;
assume k <= n; then
A6: ||.(S.n) - g.|| < r/|.a.| by A5;
A7: 0 <> |.a.| by A3,COMPLEX1:47;
A8: |.a.| * (r/|.a.|) = |.a.| * (|.a.|" * r) by XCMPLX_0:def 9
.= |.a.| *|.a.|" * r
.= 1 * r by A7,XCMPLX_0:def 7
.= r;
||.(a * (S.n)) - (a * g).|| = ||.a * ((S.n) - g).|| by RLVECT_1:34
.= |.a.| * ||.(S.n) - g.|| by Def1;
then ||.(a *(S.n)) - h.|| < r by A4,A6,A8,XREAL_1:68;
hence ||.(a * S).n - h.|| < r by Def5;
end;
now
assume
A9: a = 0;
let r;
assume 0 < r;
then consider m1 such that
A10: for n st m1 <= n holds ||.(S.n) - g.|| < r by A1;
take k = m1;
let n;
assume k <= n; then
A11: ||.(S.n) - g.|| < r by A10;
||.a * (S.n) - a * g.|| = ||.0 * (S.n) - 09(RNS).|| by A9,RLVECT_1:10
.= ||.09(RNS) - 09(RNS).|| by RLVECT_1:10
.= ||.09(RNS).||
.= 0;
then ||.a * (S.n) - h.|| < r by A11;
hence ||.(a * S).n - h.|| < r by Def5;
end;
hence thesis by A2;
end;
theorem Th23:
S is convergent implies ||.S.|| is convergent
proof
assume S is convergent;
then consider g such that
A1: for r st 0 < r ex m st for n st m <= n holds ||.(S.n) - g.|| < r;
now
let r be Real;
assume
A2: 0 < r;
consider m1 such that
A3: for n st m1 <= n holds ||.(S.n) - g.|| < r by A1,A2;
reconsider k = m1 as Nat;
take k;
now
let n be Nat;
assume
A4: k <= n;
reconsider nn = n as Nat;
A5: ||.(S.nn) - g.|| < r by A3,A4;
|. ||.(S.nn).|| - ||.g.|| .| <= ||.(S.nn) - g.|| by Th9;
then |. ||.(S.nn).|| - ||.g.|| .| < r by A5,XXREAL_0:2;
hence |. ||.S.||.n qua Real - ||.g.|| .| < r by NORMSP_0:def 4;
end;
hence for n being Nat st k <= n holds |. ||.S.||.n - ||.g.|| .| < r;
end;
hence thesis by SEQ_2:def 6;
end;
definition
let RNS, S;
assume
A1: S is convergent;
func lim S -> Point of RNS means
:Def7:
for r st 0 < r ex m st for n st m <= n holds ||.(S.n) - it.|| < r;
existence by A1;
uniqueness
proof
for x, y st ( for r st 0 < r ex m st for n st m <= n holds ||.(S.n) -
x.|| < r ) & ( for r st 0 < r ex m st for n st m <= n holds ||.(S.n) - y.|| < r
) holds x = y
proof
given x, y such that
A2: for r st 0 < r ex m st for n st m <= n holds ||.(S.n) - x.|| < r and
A3: for r st 0 < r ex m st for n st m <= n holds ||.(S.n) - y.|| < r and
A4: x <> y;
A5: ||.x - y.|| <> 0 by A4,Th6;
then
A6: 0/4 < ||.x - y.||/4;
then consider m1 such that
A7: for n st m1 <= n holds ||.(S.n) - x.|| < ||.x - y.||/4 by A2;
consider m2 such that
A8: for n st m2 <= n holds ||.(S.n) - y.|| < ||.x - y.||/4 by A3,A6;
A9: now
||.x - y.|| <= ||.x - (S.m1).|| + ||.(S.m1) - y.|| by Th10;
then
A10: ||.x - y.|| <= ||.(S.m1) - x.|| + ||.(S.m1) - y.|| by Th7;
assume m2 <= m1; then
A11: ||.(S.m1) - y.|| < ||.x - y.||/4 by A8;
||.(S.m1) - x.|| < ||.x - y.||/4 by A7;
then
||.(S.m1) - x.|| + ||.(S.m1) - y.|| < ||.x - y.||/4 + ||.x - y.||
/4 by A11,XREAL_1:8;
then not ||.x - y.||/2 < ||.x - y.|| by A10,XXREAL_0:2;
hence contradiction by A5,XREAL_1:216;
end;
now
||.x - y.|| <= ||.x - (S.m2).|| + ||.(S.m2) - y.|| by Th10;
then
A12: ||.x - y.|| <= ||.(S.m2) - x.|| + ||.(S.m2) - y.|| by Th7;
assume m1 <= m2;
then
A13: ||.(S.m2) - x.|| < ||.x - y.||/4 by A7;
||.(S.m2) - y.|| < ||.x - y.||/4 by A8;
then
||.(S.m2) - x.|| + ||.(S.m2) - y.|| < ||.x - y.||/4 + ||.x - y.||
/4 by A13,XREAL_1:8;
then not ||.x - y.||/2 < ||.x - y.|| by A12,XXREAL_0:2;
hence contradiction by A5,XREAL_1:216;
end;
hence contradiction by A9;
end;
hence thesis;
end;
end;
theorem
S is convergent & lim S = g implies ||.S - g.|| is convergent & lim
||.S - g.|| = 0
proof
assume that
A1: S is convergent and
A2: lim S = g;
A3: now
let r be Real;
assume
A4: 0 < r;
consider m1 such that
A5: for n st m1 <= n holds ||.(S.n) - g.|| < r by A1,A2,A4,Def7;
reconsider k = m1 as Nat;
take k;
let n be Nat;
assume
A6: k <= n;
reconsider nn=n as Nat;
||.(S.nn) - g.|| < r by A5,A6;
then
A7: ||.((S.nn) - g ) - 09(RNS).|| < r;
|.||.(S.nn) - g.|| - ||.09(RNS).||.| <= ||.((S.nn) - g ) - 09(RNS).||
by Th9;
then |.||.(S.nn) - g.|| - ||.09(RNS).||.| < r by A7,XXREAL_0:2;
then |.(||.(S - g).nn.|| - 0).| < r by Def4;
hence |.(||.S - g.||.n - 0).| < r by NORMSP_0:def 4;
end;
||.S - g.|| is convergent by A1,Th21,Th23;
hence thesis by A3,SEQ_2:def 7;
end;
theorem
S1 is convergent & S2 is convergent implies lim (S1 + S2) = (lim S1) +
(lim S2)
proof
assume that
A1: S1 is convergent and
A2: S2 is convergent;
set g2 = lim S2;
set g1 = lim S1;
set g = g1 + g2;
A3: now
let r;
assume 0 < r; then
A4: 0< r/2;
then consider m1 such that
A5: for n st m1 <= n holds ||.(S1.n) - g1.|| < r/2 by A1,Def7;
consider m2 such that
A6: for n st m2 <= n holds ||.(S2.n) - g2.|| < r/2 by A2,A4,Def7;
take k = m1 + m2;
let n such that
A7: k <= n;
m2 <= k by NAT_1:12;
then m2 <= n by A7,XXREAL_0:2;
then
A8: ||.(S2.n) - g2.|| < r/2 by A6;
A9: ||.(S1 + S2).n - g.|| = ||.-(g1+g2) + ((S1.n) + (S2.n)).|| by Def2
.= ||.((-g1)+(-g2)) + ((S1.n) + (S2.n)).|| by RLVECT_1:31
.= ||.(S1.n) + ((-g1)+(-g2)) + (S2.n).|| by RLVECT_1:def 3
.= ||.(S1.n) - g1 + (-g2) + (S2.n).|| by RLVECT_1:def 3
.= ||.(S1.n) - g1 + ((S2.n) - g2).|| by RLVECT_1:def 3;
A10: ||.(S1.n) - g1 + ((S2.n) - g2).|| <= ||.(S1.n) - g1.|| + ||.(S2.n) -
g2.|| by Def1;
m1 <= m1 + m2 by NAT_1:12;
then m1 <= n by A7,XXREAL_0:2;
then ||.(S1.n) - g1.|| < r/2 by A5;
then ||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| < r/2 + r/2 by A8,XREAL_1:8;
hence ||.(S1 + S2).n - g.|| < r by A9,A10,XXREAL_0:2;
end;
S1 + S2 is convergent by A1,A2,Th19;
hence thesis by A3,Def7;
end;
theorem
S1 is convergent & S2 is convergent implies lim (S1 - S2) = (lim S1) -
(lim S2)
proof
assume that
A1: S1 is convergent and
A2: S2 is convergent;
set g2 = lim S2;
set g1 = lim S1;
set g = g1 - g2;
A3: now
let r;
assume 0 < r; then
A4: 0< r/2;
then consider m1 such that
A5: for n st m1 <= n holds ||.(S1.n) - g1.|| < r/2 by A1,Def7;
consider m2 such that
A6: for n st m2 <= n holds ||.(S2.n) - g2.|| < r/2 by A2,A4,Def7;
take k = m1 + m2;
let n such that
A7: k <= n;
m2 <= k by NAT_1:12;
then m2 <= n by A7,XXREAL_0:2;
then
A8: ||.(S2.n) - g2.|| < r/2 by A6;
A9: ||.(S1 - S2).n - g.|| = ||.((S1.n) - (S2.n)) - (g1 - g2).|| by Def3
.= ||.(((S1.n) - (S2.n)) - g1) + g2.|| by RLVECT_1:29
.= ||. ((S1.n) - (g1 + (S2.n))) + g2.|| by RLVECT_1:27
.= ||. (((S1.n) - g1 ) - (S2.n)) + g2.|| by RLVECT_1:27
.= ||. ((S1.n) - g1 ) - ((S2.n) - g2).|| by RLVECT_1:29;
A10: ||.((S1.n) - g1) - ((S2.n) - g2).|| <= ||.(S1.n) - g1.|| + ||.(S2.n)
- g2.|| by Th3;
m1 <= m1 + m2 by NAT_1:12;
then m1 <= n by A7,XXREAL_0:2;
then ||.(S1.n) - g1.|| < r/2 by A5;
then ||.(S1.n) - g1.|| + ||.(S2.n) - g2.|| < r/2 + r/2 by A8,XREAL_1:8;
hence ||.(S1 - S2).n - g.|| < r by A9,A10,XXREAL_0:2;
end;
S1 - S2 is convergent by A1,A2,Th20;
hence thesis by A3,Def7;
end;
theorem
S is convergent implies lim (S - x) = (lim S) - x
proof
set g = lim S;
set h = g - x;
assume
A1: S is convergent;
A2: now
let r;
assume 0 < r;
then consider m1 such that
A3: for n st m1 <= n holds ||.(S.n) - g.|| < r by A1,Def7;
take k = m1;
let n;
assume k <= n; then
A4: ||.(S.n) - g.|| < r by A3;
||.(S.n) - g.|| = ||.((S.n) - 09(RNS)) - g.||
.= ||.((S.n) - (x - x)) - g.|| by RLVECT_1:15
.= ||.(((S.n) - x) + x) - g.|| by RLVECT_1:29
.= ||.((S.n) - x) + ((-g) + x).|| by RLVECT_1:def 3
.= ||.((S.n) - x) - h.|| by RLVECT_1:33;
hence ||.(S - x).n - h.|| < r by A4,Def4;
end;
S - x is convergent by A1,Th21;
hence thesis by A2,Def7;
end;
theorem
S is convergent implies lim (a * S) = a * (lim S)
proof
set g = lim S;
set h = a * g;
assume
A1: S is convergent;
A2: now
assume
A3: a = 0;
let r;
assume 0 < r;
then consider m1 such that
A4: for n st m1 <= n holds ||.(S.n) - g.|| < r by A1,Def7;
take k = m1;
let n;
assume k <= n; then
A5: ||.(S.n) - g.|| < r by A4;
||.a * (S.n) - a * g.|| = ||.0 * (S.n) - 09(RNS).|| by A3,RLVECT_1:10
.= ||.09(RNS) - 09(RNS).|| by RLVECT_1:10
.= ||.09(RNS).||
.= 0;
then ||.a * (S.n) - h.|| < r by A5;
hence ||.(a * S).n - h.|| < r by Def5;
end;
A6: now
assume
A7: a <> 0; then
A8: 0 < |.a.| by COMPLEX1:47;
let r;
assume 0 < r;
then 0 < r/|.a.| by A8;
then consider m1 such that
A9: for n st m1 <= n holds ||.(S.n) - g.|| < r/|.a.| by A1,Def7;
take k = m1;
let n;
assume k <= n; then
A10: ||.(S.n) - g.|| < r/|.a.| by A9;
A11: 0 <> |.a.| by A7,COMPLEX1:47;
A12: |.a.| * (r/|.a.|) = |.a.| * (|.a.|" * r) by XCMPLX_0:def 9
.= |.a.| *|.a.|" * r
.= 1 * r by A11,XCMPLX_0:def 7
.= r;
||.(a * (S.n)) - (a * g).|| = ||.a * ((S.n) - g).|| by RLVECT_1:34
.= |.a.| * ||.(S.n) - g.|| by Def1;
then ||.(a *(S.n)) - h.|| < r by A8,A10,A12,XREAL_1:68;
hence ||.(a * S).n - h.|| < r by Def5;
end;
a * S is convergent by A1,Th22;
hence thesis by A2,A6,Def7;
end;