The abstract of the Mizar article:

Banach Space of Absolute Summable Real Sequences

by

Yasumasa Suzuki,

Noboru Endou, and

Yasunari Shidama

Received August 8, 2003

MML identifier: RSSPACE3

[ Mizar article, MML identifier index ]

environ

 vocabulary PRE_TOPC, NORMSP_1, RLVECT_1, FUNCT_1, ARYTM, ARYTM_1, ARYTM_3,
      RELAT_1, ABSVALUE, ORDINAL2, PROB_1, RLSUB_1, SEQ_1, SEQ_2, SEQM_3,
      SERIES_1, SUPINF_2, RSSPACE, RSSPACE3, METRIC_1, BINOP_1;
 notation TARSKI, SUBSET_1, XBOOLE_0, ZFMISC_1, ORDINAL1, NUMBERS, XREAL_0,
      STRUCT_0, REAL_1, NAT_1, FUNCT_1, FUNCT_2, RELAT_1, BINOP_1, PRE_TOPC,
      RLVECT_1, ABSVALUE, RLSUB_1, NORMSP_1, SEQ_1, SEQ_2, SEQM_3, SERIES_1,
      PARTFUN1, RSSPACE;
 constructors REAL_1, NAT_1, DOMAIN_1, SEQ_2, SERIES_1, PREPOWER, PARTFUN1,
      RLSUB_1, RSSPACE, MEMBERED;
 clusters RELSET_1, STRUCT_0, RLVECT_1, NORMSP_1, SEQ_1, XREAL_0, MEMBERED,
      ORDINAL2;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;


begin :: l1_Space:The Space of Absolute Summable Real Sequences

definition
  func the_set_of_l1RealSequences -> Subset of
     Linear_Space_of_RealSequences means
:: RSSPACE3:def 1
   for x being set holds x in it
     iff
   (x in the_set_of_RealSequences & seq_id(x) is absolutely_summable);
end;

definition
  cluster the_set_of_l1RealSequences -> non empty;
end;

theorem :: RSSPACE3:1
the_set_of_l1RealSequences is lineary-closed;

theorem :: RSSPACE3:2
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;

definition
  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;
end;

theorem :: RSSPACE3:3
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;

definition
  func l_norm -> Function of the_set_of_l1RealSequences, REAL means
:: RSSPACE3:def 2
  for x be set st x in the_set_of_l1RealSequences holds
    it.x = Sum(abs(seq_id(x)));
end;

definition let X be non empty set,
               Z be Element of X, A be BinOp of X,
               M be Function of [:REAL, X:], X,
               N be Function of X, REAL;
  cluster NORMSTR (# X, Z, A, M, N #) -> non empty;
end;

theorem :: RSSPACE3:4
for l be NORMSTR st RLSStruct (# the carrier of l, the Zero of l,
        the add of l, the Mult of l #)
  is RealLinearSpace holds l is RealLinearSpace;

theorem :: RSSPACE3:5
for rseq be Real_Sequence
   st (for n be Nat holds rseq.n=0) holds
   rseq is absolutely_summable & Sum(abs(rseq))=0;

theorem :: RSSPACE3:6
for rseq be Real_Sequence st
 ( rseq is absolutely_summable & Sum(abs(rseq))=0 ) holds
  for n be Nat holds rseq.n =0;

theorem :: 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;

definition
  func l1_Space -> non empty NORMSTR equals
:: RSSPACE3:def 3
   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 #);
end;

begin :: l1_Space is Banach

theorem :: RSSPACE3:8
  the carrier of l1_Space = the_set_of_l1RealSequences &
( for x be set holds
   x is Element of l1_Space
  iff x is Real_Sequence & seq_id(x) is absolutely_summable ) &
( for x be set holds
   x is VECTOR of l1_Space
   iff x is Real_Sequence & seq_id(x) is absolutely_summable ) &
0.l1_Space = Zeroseq &
( for u be VECTOR of l1_Space holds u =seq_id(u) ) &
( for u,v be VECTOR of l1_Space holds u+v =seq_id(u)+seq_id(v) ) &
( for r be Real for u be VECTOR of l1_Space holds r*u =r(#)seq_id(u) ) &
( for u be VECTOR of l1_Space holds
   -u = -seq_id(u) & seq_id(-u) = -seq_id(u) ) &
( for u,v be VECTOR of l1_Space holds u-v =seq_id(u)-seq_id(v) ) &
( for v be VECTOR of l1_Space holds seq_id(v) is absolutely_summable ) &
( for v be VECTOR of l1_Space holds ||.v.|| = Sum(abs(seq_id(v))) );

theorem :: RSSPACE3:9
for x, y being Point of l1_Space, a be Real holds
  ( ||.x.|| = 0 iff x = 0.l1_Space ) &
  0 <= ||.x.|| &
  ||.x+y.|| <= ||.x.|| +  ||.y.|| &
  ||.(a*x).|| = abs(a) * ||.x.||;

definition
  cluster l1_Space -> RealNormSpace-like RealLinearSpace-like
       Abelian add-associative right_zeroed right_complementable;
end;

definition let X be non empty NORMSTR, x, y be Point of X;
  func dist(x,y) -> Real equals
:: RSSPACE3:def 4
  ||.x - y.||;
end;

definition
 let NRM be non empty NORMSTR;
 let seqt be sequence of NRM;
 attr seqt is CCauchy means
:: RSSPACE3:def 5
 for r1 be Real st r1 > 0 ex k1 be Nat st
  for n1, m1 be Nat st n1 >= k1 & m1 >= k1 holds
   dist(seqt.n1, seqt.m1) < r1;
  synonym seqt is Cauchy_sequence_by_Norm;
end;

reserve NRM for non empty RealNormSpace;
reserve seq for sequence of NRM;

theorem :: RSSPACE3:10
seq is Cauchy_sequence_by_Norm iff for r be Real st r > 0
 ex k be Nat st for n, m be Nat st
  n >= k & m >= k holds ||.(seq.n) - (seq.m).|| < r;

theorem :: RSSPACE3:11
for vseq be sequence of l1_Space st vseq is Cauchy_sequence_by_Norm
 holds vseq is convergent;