:: NORMSP_1 semantic presentation

definition

attr c₁ is strict;
struct NORMSTR -> RLSStruct ;
aggr NORMSTR(# carrier, Zero, add, Mult, norm #) -> NORMSTR ;
sel norm c₁ -> Function of the carrier of c₁, REAL ;

end;

registration

cluster non empty NORMSTR ;
existence

proof end;

end;

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

definition

let X be non empty NORMSTR ;
let x be Point of X;
func ||.x.|| -> Real equals :: NORMSP_1:def 1
the norm of X . x;
coherence ;

end;

:: deftheorem defines ||. NORMSP_1:def 1 :

consider V being RealLinearSpace;

Lm1: the carrier of ((0). V) = {(0. V)}
by RLSUB_1:def 3;

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

Lm2: for u being VECTOR of ((0). V) holds niltonil . u = 0
by FUNCOP_1:13;

0. V is VECTOR of ((0). V)
by Lm1, TARSKI:def 1;

then Lm3: niltonil . (0. V) = 0
by Lm2;

Lm4: for u being VECTOR of ((0). V)
for a being Real holds niltonil . (a * u) = (abs a) * (niltonil . u)

proof end;

Lm5: for u, v being VECTOR of ((0). V) holds niltonil . (u + v) <= (niltonil . u) + (niltonil . v)

proof end;

reconsider X = NORMSTR(# the carrier of ((0). V),the Zero of ((0). V),the add of ((0). V),the Mult of ((0). V),niltonil #) as non empty NORMSTR by STRUCT_0:def 1;

Lm6: now

let x, y be Point of X; :: thesis:
let a be Real; :: thesis:
reconsider u = x, w = y as VECTOR of ((0). V) ;
thus ( ||.x.|| = 0 iff x = H₁(X) ) :: thesis:

proof

H₁(X) = the Zero of X
.= 0. ((0). V)
.= 0. V by RLSUB_1:19 ;
hence ( ||.x.|| = 0 iff x = H₁(X) ) by Lm1, Lm3, TARSKI:def 1; :: thesis:

end;

a * x = the Mult of X . [a,u]
.= a * u ;
hence ||.(a * x).|| = (abs a) * ||.x.|| by Lm4; :: thesis:
x + y = the add of X . [x,y]
.= u + w ;
hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by Lm5; :: thesis:

end;

definition

let IT be non empty NORMSTR ;
attr IT is RealNormSpace-like means :Def2: :: NORMSP_1:def 2
for x, y being Point of IT
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. IT ) & ( x = 0. IT implies ||.x.|| = 0 ) & ||.(a * x).|| = (abs a) * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| );

end;

:: deftheorem Def2 defines RealNormSpace-like NORMSP_1:def 2 :

registration

cluster non empty Abelian add-associative right_zeroed right_complementable RealLinearSpace-like strict RealNormSpace-like NORMSTR ;
existence

proof end;

end;

definition

mode RealNormSpace is non empty Abelian add-associative right_zeroed right_complementable RealLinearSpace-like RealNormSpace-like NORMSTR ;

end;

theorem :: NORMSP_1:1

canceled;

theorem :: NORMSP_1:2

canceled;

theorem :: NORMSP_1:3

canceled;

theorem :: NORMSP_1:4

canceled;

theorem :: NORMSP_1:5

for RNS being RealNormSpace holds ||.(0. RNS).|| = 0 by Def2;

theorem Th6: :: NORMSP_1:6

for RNS being RealNormSpace
for x being Point of RNS holds ||.(- x).|| = ||.x.||

proof end;

theorem Th7: :: NORMSP_1:7

for RNS being RealNormSpace
for x, y being Point of RNS holds ||.(x - y).|| <= ||.x.|| + ||.y.||

proof end;

theorem Th8: :: NORMSP_1:8

for RNS being RealNormSpace
for x being Point of RNS holds 0 <= ||.x.||

proof end;

theorem :: NORMSP_1:9

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.||)

proof end;

theorem Th10: :: NORMSP_1:10

for RNS being RealNormSpace
for x, y being Point of RNS holds
( ||.(x - y).|| = 0 iff x = y )

proof end;

theorem Th11: :: NORMSP_1:11

for RNS being RealNormSpace
for x, y being Point of RNS holds ||.(x - y).|| = ||.(y - x).||

proof end;

theorem Th12: :: NORMSP_1:12

for RNS being RealNormSpace
for x, y being Point of RNS holds ||.x.|| - ||.y.|| <= ||.(x - y).||

proof end;

theorem Th13: :: NORMSP_1:13

for RNS being RealNormSpace
for x, y being Point of RNS holds abs (||.x.|| - ||.y.||) <= ||.(x - y).||

proof end;

theorem Th14: :: NORMSP_1:14

for RNS being RealNormSpace
for x, z, y being Point of RNS holds ||.(x - z).|| <= ||.(x - y).|| + ||.(y - z).||

proof end;

theorem :: NORMSP_1:15

for RNS being RealNormSpace
for x, y being Point of RNS st x <> y holds
||.(x - y).|| <> 0 by Th10;

definition

let RNS be 1-sorted ;
mode sequence of RNS is Function of NAT ,the carrier of RNS;

end;

theorem :: NORMSP_1:16

canceled;

theorem :: NORMSP_1:17

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 & ( for d being set st d in NAT holds
f . d is Element of RNS ) ) )

proof end;

theorem :: NORMSP_1:18

canceled;

theorem Th19: :: NORMSP_1:19

for RNS being non empty 1-sorted
for x being Element of RNS ex S being sequence of RNS st rng S = {x}

proof end;

theorem Th20: :: NORMSP_1:20

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}

proof end;

theorem Th21: :: NORMSP_1:21

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 Nat holds S . n = S . (n + 1)

proof end;

theorem Th22: :: NORMSP_1:22

for RNS being non empty 1-sorted
for S being sequence of RNS st ( for n being Nat holds S . n = S . (n + 1) ) holds
for n, k being Nat holds S . n = S . (n + k)

proof end;

theorem Th23: :: NORMSP_1:23

for RNS being non empty 1-sorted
for S being sequence of RNS st ( for n, k being Nat holds S . n = S . (n + k) ) holds
for n, m being Nat holds S . n = S . m

proof end;

theorem Th24: :: NORMSP_1:24

for RNS being non empty 1-sorted
for S being sequence of RNS st ( for n, m being Nat holds S . n = S . m ) holds
ex x being Element of RNS st
for n being Nat holds S . n = x

proof end;

theorem :: NORMSP_1:25

for RNS being RealNormSpace ex S being sequence of RNS st rng S = {(0. RNS)} by Th19;

definition

let RNS be non empty 1-sorted ;
let S be sequence of RNS;
canceled;
:: original: constant
redefine attr S is constant means :Def4: :: NORMSP_1:def 4
ex x being Element of RNS st
for n being Nat holds S . n = x;
compatibility

proof end;

end;

:: deftheorem NORMSP_1:def 3 :

:: deftheorem Def4 defines constant NORMSP_1:def 4 :

theorem :: NORMSP_1:26

canceled;

theorem :: NORMSP_1:27

for RNS being non empty 1-sorted
for S being sequence of RNS holds
( S is constant iff ex x being Element of RNS st rng S = {x} )

proof end;

Lm7: for RNS being non empty 1-sorted
for S being sequence of RNS
for n being 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 Nat;
:: original: .
redefine func S . n -> Element of RNS;
coherence by Lm7;

end;

definition

let RNS be RealLinearSpace;
let S1, S2 be sequence of RNS;
func S1 + S2 -> sequence of RNS means :Def5: :: NORMSP_1:def 5
for n being Nat holds it . n = (S1 . n) + (S2 . n);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines + NORMSP_1:def 5 :

definition

let RNS be RealLinearSpace;
let S1, S2 be sequence of RNS;
func S1 - S2 -> sequence of RNS means :Def6: :: NORMSP_1:def 6
for n being Nat holds it . n = (S1 . n) - (S2 . n);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines - NORMSP_1:def 6 :

definition

let RNS be RealLinearSpace;
let S be sequence of RNS;
let x be Element of RNS;
func S - x -> sequence of RNS means :Def7: :: NORMSP_1:def 7
for n being Nat holds it . n = (S . n) - x;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines - NORMSP_1:def 7 :

definition

let RNS be RealLinearSpace;
let S be sequence of RNS;
let a be Real;
func a * S -> sequence of RNS means :Def8: :: NORMSP_1:def 8
for n being Nat holds it . n = a * (S . n);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines * NORMSP_1:def 8 :

definition

let RNS be RealNormSpace;
let S be sequence of RNS;
attr S is convergent means :Def9: :: NORMSP_1:def 9
ex g being Point of RNS st
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - g).|| < r;

end;

:: deftheorem Def9 defines convergent NORMSP_1:def 9 :

theorem :: NORMSP_1:28

canceled;

theorem :: NORMSP_1:29

canceled;

theorem :: NORMSP_1:30

canceled;

theorem :: NORMSP_1:31

canceled;

theorem :: NORMSP_1:32

canceled;

theorem :: NORMSP_1:33

canceled;

theorem Th34: :: NORMSP_1:34

for RNS being RealNormSpace
for S1, S2 being sequence of RNS st S1 is convergent & S2 is convergent holds
S1 + S2 is convergent

proof end;

theorem Th35: :: NORMSP_1:35

for RNS being RealNormSpace
for S1, S2 being sequence of RNS st S1 is convergent & S2 is convergent holds
S1 - S2 is convergent

proof end;

theorem Th36: :: NORMSP_1:36

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

proof end;

theorem Th37: :: NORMSP_1:37

for a being Real
for RNS being RealNormSpace
for S being sequence of RNS st S is convergent holds
a * S is convergent

proof end;

definition

let RNS be RealNormSpace;
let S be sequence of RNS;
func ||.S.|| -> Real_Sequence means :Def10: :: NORMSP_1:def 10
for n being Nat holds it . n = ||.(S . n).||;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines ||. NORMSP_1:def 10 :

theorem :: NORMSP_1:38

canceled;

theorem Th39: :: NORMSP_1:39

for RNS being RealNormSpace
for S being sequence of RNS st S is convergent holds
||.S.|| is convergent

proof end;

definition

let RNS be RealNormSpace;
let S be sequence of RNS;
assume A1: S is convergent ;
func lim S -> Point of RNS means :Def11: :: NORMSP_1:def 11
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((S . n) - it).|| < r;
existence by A1, Def9;
uniqueness

proof end;

end;

:: deftheorem Def11 defines lim NORMSP_1:def 11 :

theorem :: NORMSP_1:40

canceled;

theorem :: NORMSP_1:41

for RNS being RealNormSpace
for g being Point of RNS
for S being sequence of RNS st S is convergent & lim S = g holds
( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 )

proof end;

theorem :: NORMSP_1:42

for RNS being RealNormSpace
for S1, S2 being sequence of RNS st S1 is convergent & S2 is convergent holds
lim (S1 + S2) = (lim S1) + (lim S2)

proof end;

theorem :: NORMSP_1:43

for RNS being RealNormSpace
for S1, S2 being sequence of RNS st S1 is convergent & S2 is convergent holds
lim (S1 - S2) = (lim S1) - (lim S2)

proof end;

theorem :: NORMSP_1:44

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

proof end;

theorem :: NORMSP_1:45

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)

proof end;