:: Real Normed Space
:: by Jan Popio{\l}ek
::
:: Received September 20, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

definition
attrc1 is strict ;
struct NORMSTR  ->  RLSStruct , N-ZeroStr ;
aggrNORMSTR(# carrier, ZeroF, addF, Mult, normF #) ->  NORMSTR ;
end;

registration
cluster non empty strict for NORMSTR ;
existence
 ex b1 being NORMSTR st
( not b1 is empty & b1 is strict )
proofend;
end;

deffunc H1( NORMSTR ) ->  Element of the carrier of $1 = 0. $1;

set V = the RealLinearSpace;

Lm1:  the carrier of ((0). the RealLinearSpace) = {(0. the RealLinearSpace)}
by RLSUB_1:def_3;

reconsider niltonil = the carrier of ((0). the RealLinearSpace) --> 0 as Function of the carrier of ((0). the RealLinearSpace),REAL by FUNCOP_1:45;

 0. the RealLinearSpace is VECTOR of ((0). the RealLinearSpace)
by Lm1, TARSKI:def_1;

then Lm2:  niltonil . (0. the RealLinearSpace) = 0
by FUNCOP_1:7;

Lm3:  for u being VECTOR of ((0). the RealLinearSpace)
for a being Real holds niltonil . (a * u) = (abs a) * (niltonil . u)
proofend;

Lm4:  for u, v being VECTOR of ((0). the RealLinearSpace) holds niltonil . (u + v) <= (niltonil . u) + (niltonil . v)
proofend;

reconsider X = NORMSTR(# the carrier of ((0). the RealLinearSpace),(0. ((0). the RealLinearSpace)), the addF of ((0). the RealLinearSpace), the Mult of ((0). the RealLinearSpace),niltonil #) as non empty NORMSTR ;

Lm5: now__::_thesis:_for_x,_y_being_Point_of_X
for_a_being_Real_holds_
(_(_||.x.||_=_0_implies_x_=_H1(X)_)_&amp;_(_x_=_H1(X)_implies_||.x.||_=_0_)_&amp;_||.(a_*_x).||_=_(abs_a)_*_||.x.||_&amp;_||.(x_+_y).||_<=_||.x.||_+_||.y.||_)
let x, y be Point of X; ::_thesis: for a being Real holds
( ( ||.x.|| = 0 implies x = H1(X) ) &amp; ( x = H1(X) implies ||.x.|| = 0 ) &amp; ||.(a * x).|| = (abs a) * ||.x.|| &amp; ||.(x + y).|| <= ||.x.|| + ||.y.|| )
let a be Real; ::_thesis: ( ( ||.x.|| = 0 implies x = H1(X) ) &amp; ( x = H1(X) implies ||.x.|| = 0 ) &amp; ||.(a * x).|| = (abs a) * ||.x.|| &amp; ||.(x + y).|| <= ||.x.|| + ||.y.|| )
reconsider u = x, w = y as VECTOR of ((0). the RealLinearSpace) ;
 H1(X) = 0. the RealLinearSpace by RLSUB_1:11;
hence  ( ||.x.|| = 0 iff x = H1(X) ) by Lm1, FUNCOP_1:7, TARSKI:def_1; ::_thesis: ( ||.(a * x).|| = (abs a) * ||.x.|| &amp; ||.(x + y).|| <= ||.x.|| + ||.y.|| )
 a * x = a * u ;
hence  ||.(a * x).|| = (abs a) * ||.x.|| by Lm3; ::_thesis: ||.(x + y).|| <= ||.x.|| + ||.y.||
 x + y = u + w ;
hence  ||.(x + y).|| <= ||.x.|| + ||.y.|| by Lm4; ::_thesis: verum
end;

definition
let IT be non empty NORMSTR ;
attrIT is RealNormSpace-like  means :Def1: :: NORMSP_1:def 1
 for x, y being Point of IT
for a being Real holds
( ||.(a * x).|| = (abs a) * ||.x.|| &amp; ||.(x + y).|| <= ||.x.|| + ||.y.|| );
end;

:: deftheorem Def1 defines RealNormSpace-like NORMSP_1:def_1_:_
 for IT being non empty NORMSTR holds
( IT is RealNormSpace-like iff for x, y being Point of IT
for a being Real holds
( ||.(a * x).|| = (abs a) * ||.x.|| &amp; ||.(x + y).|| <= ||.x.|| + ||.y.|| ) );

registration
cluster non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive strict RealNormSpace-like for NORMSTR ;
existence
 ex b1 being non empty NORMSTR st
( b1 is reflexive &amp; b1 is discerning &amp; b1 is RealNormSpace-like &amp; b1 is vector-distributive &amp; b1 is scalar-distributive &amp; b1 is scalar-associative &amp; b1 is scalar-unital &amp; b1 is Abelian &amp; b1 is add-associative &amp; b1 is right_zeroed &amp; b1 is right_complementable &amp; b1 is strict )
proofend;
end;

definition
mode RealNormSpace is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like NORMSTR ;
end;

theorem :: NORMSP_1:1
for RNS being RealNormSpace holds ||.(0. RNS).|| = 0 ;

theorem Th2: :: NORMSP_1:2
for RNS being RealNormSpace
for x being Point of RNS holds ||.(- x).|| = ||.x.||
proofend;

theorem Th3: :: NORMSP_1:3
for RNS being RealNormSpace
for x, y being Point of RNS holds ||.(x - y).|| <= ||.x.|| + ||.y.||
proofend;

theorem Th4: :: NORMSP_1:4
for RNS being RealNormSpace
for x being Point of RNS holds 0 <= ||.x.||
proofend;

registration
let RNS be RealNormSpace;
let x be Point of RNS;
cluster||.x.|| ->  non negative ;
coherence
 not ||.x.|| is negative by Th4;
end;

theorem :: NORMSP_1:5
for a, b being Real
for RNS being RealNormSpace
for x, y being Point of RNS holds ||.((a * x) + (b * y)).|| <= ((abs a) * ||.x.||) + ((abs b) * ||.y.||)
proofend;

theorem Th6: :: NORMSP_1:6
for RNS being RealNormSpace
for x, y being Point of RNS holds
( ||.(x - y).|| = 0 iff x = y )
proofend;

theorem Th7: :: NORMSP_1:7
for RNS being RealNormSpace
for x, y being Point of RNS holds ||.(x - y).|| = ||.(y - x).||
proofend;

theorem Th8: :: NORMSP_1:8
for RNS being RealNormSpace
for x, y being Point of RNS holds ||.x.|| - ||.y.|| <= ||.(x - y).||
proofend;

theorem Th9: :: NORMSP_1:9
for RNS being RealNormSpace
for x, y being Point of RNS holds abs (||.x.|| - ||.y.||) <= ||.(x - y).||
proofend;

theorem Th10: :: NORMSP_1:10
for RNS being RealNormSpace
for x, z, y being Point of RNS holds ||.(x - z).|| <= ||.(x - y).|| + ||.(y - z).||
proofend;

theorem :: NORMSP_1:11
for RNS being RealNormSpace
for x, y being Point of RNS st x <> y holds
||.(x - y).|| <> 0 by Th6;

theorem :: NORMSP_1:12
for f being Function
for RNS being non empty 1-sorted
for x being Element of RNS holds
( f is sequence of RNS iff ( dom f = NAT &amp; ( for d being set st d in NAT holds
f . d is Element of RNS ) ) )
proofend;

theorem :: NORMSP_1:13
for RNS being non empty 1-sorted
for x being Element of RNS ex S being sequence of RNS st rng S = {x}
proofend;

theorem :: NORMSP_1:14
for RNS being non empty 1-sorted
for S being sequence of RNS st ex x being Element of RNS st
for n being Nat holds S . n = x holds
ex x being Element of RNS st rng S = {x}
proofend;

theorem :: NORMSP_1:15
for RNS being non empty 1-sorted
for S being sequence of RNS st ex x being Element of RNS st rng S = {x} holds
for n being Element of NAT holds S . n = S . (n + 1)
proofend;

theorem :: NORMSP_1:16
for RNS being non empty 1-sorted
for S being sequence of RNS st ( for n being Element of NAT holds S . n = S . (n + 1) ) holds
for n, k being Element of NAT holds S . n = S . (n + k)
proofend;

theorem :: NORMSP_1:17
for RNS being non empty 1-sorted
for S being sequence of RNS st ( for n, k being Element of NAT holds S . n = S . (n + k) ) holds
for n, m being Element of NAT holds S . n = S . m
proofend;

theorem :: NORMSP_1:18
for RNS being non empty 1-sorted
for S being sequence of RNS st ( for n, m being Element of NAT holds S . n = S . m ) holds
ex x being Element of RNS st
for n being Nat holds S . n = x
proofend;

Lm6:  for RNS being non empty 1-sorted
for S being sequence of RNS
for n being Element of NAT holds S . n is Element of RNS
;

definition
let RNS be non empty 1-sorted ;
let S be sequence of RNS;
let n be Element of NAT ;
:: original:.
redefine funcS . n ->  Element of RNS;
coherence
 S . n is Element of RNS by Lm6;
end;

definition
let RNS be non empty addLoopStr ;
let S1, S2 be sequence of RNS;
funcS1 + S2 ->  sequence of RNS means :Def2: :: NORMSP_1:def 2
 for n being Element of NAT holds it . n = (S1 . n) + (S2 . n);
existence
 ex b1 being sequence of RNS st
for n being Element of NAT holds b1 . n = (S1 . n) + (S2 . n)
proofend;
uniqueness
 for b1, b2 being sequence of RNS st ( for n being Element of NAT holds b1 . n = (S1 . n) + (S2 . n) ) &amp; ( for n being Element of NAT holds b2 . n = (S1 . n) + (S2 . n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines + NORMSP_1:def_2_:_
 for RNS being non empty addLoopStr
for S1, S2, b4 being sequence of RNS holds
( b4 = S1 + S2 iff for n being Element of NAT holds b4 . n = (S1 . n) + (S2 . n) );

definition
let RNS be non empty addLoopStr ;
let S1, S2 be sequence of RNS;
funcS1 - S2 ->  sequence of RNS means :Def3: :: NORMSP_1:def 3
 for n being Element of NAT holds it . n = (S1 . n) - (S2 . n);
existence
 ex b1 being sequence of RNS st
for n being Element of NAT holds b1 . n = (S1 . n) - (S2 . n)
proofend;
uniqueness
 for b1, b2 being sequence of RNS st ( for n being Element of NAT holds b1 . n = (S1 . n) - (S2 . n) ) &amp; ( for n being Element of NAT holds b2 . n = (S1 . n) - (S2 . n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines - NORMSP_1:def_3_:_
 for RNS being non empty addLoopStr
for S1, S2, b4 being sequence of RNS holds
( b4 = S1 - S2 iff for n being Element of NAT holds b4 . n = (S1 . n) - (S2 . n) );

definition
let RNS be non empty addLoopStr ;
let S be sequence of RNS;
let x be Element of RNS;
funcS - x ->  sequence of RNS means :Def4: :: NORMSP_1:def 4
 for n being Element of NAT holds it . n = (S . n) - x;
existence
 ex b1 being sequence of RNS st
for n being Element of NAT holds b1 . n = (S . n) - x
proofend;
uniqueness
 for b1, b2 being sequence of RNS st ( for n being Element of NAT holds b1 . n = (S . n) - x ) &amp; ( for n being Element of NAT holds b2 . n = (S . n) - x ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines - NORMSP_1:def_4_:_
 for RNS being non empty addLoopStr
for S being sequence of RNS
for x being Element of RNS
for b4 being sequence of RNS holds
( b4 = S - x iff for n being Element of NAT holds b4 . n = (S . n) - x );

definition
let RNS be non empty RLSStruct ;
let S be sequence of RNS;
let a be Real;
funca * S ->  sequence of RNS means :Def5: :: NORMSP_1:def 5
 for n being Element of NAT holds it . n = a * (S . n);
existence
 ex b1 being sequence of RNS st
for n being Element of NAT holds b1 . n = a * (S . n)
proofend;
uniqueness
 for b1, b2 being sequence of RNS st ( for n being Element of NAT holds b1 . n = a * (S . n) ) &amp; ( for n being Element of NAT holds b2 . n = a * (S . n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines * NORMSP_1:def_5_:_
 for RNS being non empty RLSStruct
for S being sequence of RNS
for a being Real
for b4 being sequence of RNS holds
( b4 = a * S iff for n being Element of NAT holds b4 . n = a * (S . n) );

definition
let RNS be RealNormSpace;
let S be sequence of RNS;
attrS is convergent  means :Def6: :: NORMSP_1:def 6
 ex g being Point of RNS st
for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - g).|| < r;
end;

:: deftheorem Def6 defines convergent NORMSP_1:def_6_:_
 for RNS being RealNormSpace
for S being sequence of RNS holds
( S is convergent iff ex g being Point of RNS st
for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - g).|| < r );

theorem Th19: :: NORMSP_1:19
for RNS being RealNormSpace
for S1, S2 being sequence of RNS st S1 is convergent &amp; S2 is convergent holds
S1 + S2 is convergent
proofend;

theorem Th20: :: NORMSP_1:20
for RNS being RealNormSpace
for S1, S2 being sequence of RNS st S1 is convergent &amp; S2 is convergent holds
S1 - S2 is convergent
proofend;

theorem Th21: :: NORMSP_1:21
for RNS being RealNormSpace
for x being Point of RNS
for S being sequence of RNS st S is convergent holds
S - x is convergent
proofend;

theorem Th22: :: NORMSP_1:22
for a being Real
for RNS being RealNormSpace
for S being sequence of RNS st S is convergent holds
a * S is convergent
proofend;

theorem Th23: :: NORMSP_1:23
for RNS being RealNormSpace
for S being sequence of RNS st S is convergent holds
||.S.|| is convergent
proofend;

definition
let RNS be RealNormSpace;
let S be sequence of RNS;
assume A1: S is convergent ;
func lim S ->  Point of RNS means :Def7: :: NORMSP_1:def 7
 for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - it).|| < r;
existence
 ex b1 being Point of RNS st
for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - b1).|| < r by A1, Def6;
uniqueness
 for b1, b2 being Point of RNS st ( for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - b1).|| < r ) &amp; ( for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - b2).|| < r ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines lim NORMSP_1:def_7_:_
 for RNS being RealNormSpace
for S being sequence of RNS st S is convergent holds
for b3 being Point of RNS holds
( b3 = lim S iff for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - b3).|| < r );

theorem :: NORMSP_1:24
for RNS being RealNormSpace
for g being Point of RNS
for S being sequence of RNS st S is convergent &amp; lim S = g holds
( ||.(S - g).|| is convergent &amp; lim ||.(S - g).|| = 0 )
proofend;

theorem :: NORMSP_1:25
for RNS being RealNormSpace
for S1, S2 being sequence of RNS st S1 is convergent &amp; S2 is convergent holds
lim (S1 + S2) = (lim S1) + (lim S2)
proofend;

theorem :: NORMSP_1:26
for RNS being RealNormSpace
for S1, S2 being sequence of RNS st S1 is convergent &amp; S2 is convergent holds
lim (S1 - S2) = (lim S1) - (lim S2)
proofend;

theorem :: NORMSP_1:27
for RNS being RealNormSpace
for x being Point of RNS
for S being sequence of RNS st S is convergent holds
lim (S - x) = (lim S) - x
proofend;

theorem :: NORMSP_1:28
for a being Real
for RNS being RealNormSpace
for S being sequence of RNS st S is convergent holds
lim (a * S) = a * (lim S)
proofend;