:: RSSPACE3 semantic presentation

definition

func the_set_of_l1RealSequences -> Subset of Linear_Space_of_RealSequences means :Def1: :: RSSPACE3:def 1
for b₁ being set holds
( b₁ in a₁ iff ( b₁ in the_set_of_RealSequences & seq_id b₁ is absolutely_summable ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines the_set_of_l1RealSequences RSSPACE3:def 1 :

theorem Th1: :: RSSPACE3:1

for b₁ being Real
for b₂ being Real_Sequence st b₂ is convergent holds
for b₃ being Real_Sequence st ( for b₄ being Nat holds b₃ . b₄ = abs ((b₂ . b₄) - b₁) ) holds
( b₃ is convergent & lim b₃ = abs ((lim b₂) - b₁) )

proof end;

registration

cluster the_set_of_l1RealSequences -> non empty ;
coherence

proof end;

end;

registration

cluster the_set_of_l1RealSequences -> non empty lineary-closed ;
coherence

proof end;

end;

Lemma3: RLSStruct(# the_set_of_l1RealSequences ,(Zero_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ) #) is Subspace of Linear_Space_of_RealSequences
by RSSPACE:13;

registration

cluster RLSStruct(# the_set_of_l1RealSequences ,(Zero_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ) #) -> Abelian add-associative right_zeroed right_complementable RealLinearSpace-like ;
coherence by RSSPACE:13;

end;

Lemma4: RLSStruct(# the_set_of_l1RealSequences ,(Zero_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ) #) is RealLinearSpace
;

Lemma5: ex b₁ being Function of the_set_of_l1RealSequences , REAL st
for b₂ being set st b₂ in the_set_of_l1RealSequences holds
b₁ . b₂ = Sum (abs (seq_id b₂))

proof end;

definition

func l_norm -> Function of the_set_of_l1RealSequences , REAL means :Def2: :: RSSPACE3:def 2
for b₁ being set st b₁ in the_set_of_l1RealSequences holds
a₁ . b₁ = Sum (abs (seq_id b₁));
existence by Lemma5;
uniqueness

proof end;

end;

:: deftheorem Def2 defines l_norm RSSPACE3:def 2 :

registration

let c₁ be non empty set ;
let c₂ be Element of c₁;
let c₃ be BinOp of c₁;
let c₄ be Function of [:REAL ,c₁:],c₁;
let c₅ be Function of c₁, REAL ;
cluster NORMSTR(# a₁,a₂,a₃,a₄,a₅ #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

theorem Th2: :: RSSPACE3:2

canceled;

theorem Th3: :: RSSPACE3:3

canceled;

theorem Th4: :: RSSPACE3:4

for b₁ being NORMSTR st RLSStruct(# the carrier of b₁,the Zero of b₁,the add of b₁,the Mult of b₁ #) is RealLinearSpace holds
b₁ is RealLinearSpace

proof end;

theorem Th5: :: RSSPACE3:5

for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ = 0 ) holds
( b₁ is absolutely_summable & Sum (abs b₁) = 0 )

proof end;

theorem Th6: :: RSSPACE3:6

for b₁ being Real_Sequence st b₁ is absolutely_summable & Sum (abs b₁) = 0 holds
for b₂ being Nat holds b₁ . b₂ = 0

proof end;

theorem Th7: :: RSSPACE3:7

NORMSTR(# the_set_of_l1RealSequences ,(Zero_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Add_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),(Mult_ the_set_of_l1RealSequences ,Linear_Space_of_RealSequences ),l_norm #) is RealLinearSpace by Lemma4, Th4;

definition end;

:: deftheorem Def3 defines l1_Space RSSPACE3:def 3 :

theorem Th8: :: RSSPACE3:8

( the carrier of l1_Space = the_set_of_l1RealSequences & ( for b₁ being set holds
( b₁ is VECTOR of l1_Space iff ( b₁ is Real_Sequence & seq_id b₁ is absolutely_summable ) ) ) & 0. l1_Space = Zeroseq & ( for b₁ being VECTOR of l1_Space holds b₁ = seq_id b₁ ) & ( for b₁, b₂ being VECTOR of l1_Space holds b₁ + b₂ = (seq_id b₁) + (seq_id b₂) ) & ( for b₁ being Real
for b₂ being VECTOR of l1_Space holds b₁ * b₂ = b₁ (#) (seq_id b₂) ) & ( for b₁ being VECTOR of l1_Space holds
( - b₁ = - (seq_id b₁) & seq_id (- b₁) = - (seq_id b₁) ) ) & ( for b₁, b₂ being VECTOR of l1_Space holds b₁ - b₂ = (seq_id b₁) - (seq_id b₂) ) & ( for b₁ being VECTOR of l1_Space holds seq_id b₁ is absolutely_summable ) & ( for b₁ being VECTOR of l1_Space holds ||.b₁.|| = Sum (abs (seq_id b₁)) ) )

proof end;

theorem Th9: :: RSSPACE3:9

for b₁, b₂ being Point of l1_Space
for b₃ being Real holds
( ( ||.b₁.|| = 0 implies b₁ = 0. l1_Space ) & ( b₁ = 0. l1_Space implies ||.b₁.|| = 0 ) & 0 <= ||.b₁.|| & ||.(b₁ + b₂).|| <= ||.b₁.|| + ||.b₂.|| & ||.(b₃ * b₁).|| = (abs b₃) * ||.b₁.|| )

proof end;

registration end;

Lemma13: for b₁ being Real
for b₂, b₃ being Real_Sequence st b₂ is convergent & b₃ is convergent holds
for b₄ being Real_Sequence st ( for b₅ being Nat holds b₄ . b₅ = (abs ((b₂ . b₅) - b₁)) + (b₃ . b₅) ) holds
( b₄ is convergent & lim b₄ = (abs ((lim b₂) - b₁)) + (lim b₃) )

proof end;

definition

let c₁ be non empty NORMSTR ;
let c₂, c₃ be Point of c₁;
func dist c₂,c₃ -> Real equals :: RSSPACE3:def 4
||.(a₂ - a₃).||;
coherence ;

end;

:: deftheorem Def4 defines dist RSSPACE3:def 4 :

definition

let c₁ be non empty NORMSTR ;
let c₂ be sequence of c₁;
attr a₂ is CCauchy means :Def5: :: RSSPACE3:def 5
for b₁ being Real st b₁ > 0 holds
ex b₂ being Nat st
for b₃, b₄ being Nat st b₃ >= b₂ & b₄ >= b₂ holds
dist (a₂ . b₃),(a₂ . b₄) < b₁;

end;

:: deftheorem Def5 defines CCauchy RSSPACE3:def 5 :

notation

let c₁ be non empty NORMSTR ;
let c₂ be sequence of c₁;
synonym Cauchy_sequence_by_Norm c₂ for CCauchy c₂;

end;

theorem Th10: :: RSSPACE3:10

for b₁ being non empty RealNormSpace
for b₂ being sequence of b₁ holds
( b₂ is CCauchy iff for b₃ being Real st b₃ > 0 holds
ex b₄ being Nat st
for b₅, b₆ being Nat st b₅ >= b₄ & b₆ >= b₄ holds
||.((b₂ . b₅) - (b₂ . b₆)).|| < b₃ )

proof end;

theorem Th11: :: RSSPACE3:11

for b₁ being sequence of l1_Space st b₁ is CCauchy holds
b₁ is convergent

proof end;