:: Real Linear Space of Real Sequences
::  by Noboru Endou , Yasumasa Suzuki and Yasunari Shidama
::
:: Received April 3, 2003
:: Copyright (c) 2003-2012 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, XBOOLE_0, SEQ_1, FUNCT_2, TARSKI, REAL_1, BINOP_1,
      SUBSET_1, FUNCT_1, ARYTM_3, ZFMISC_1, VALUED_1, CARD_1, FUNCOP_1, NAT_1,
      RLVECT_1, RELAT_1, SUPINF_2, ARYTM_1, STRUCT_0, ALGSTR_0, XREAL_0,
      ORDINAL1, RLSUB_1, REALSET1, SERIES_1, XXREAL_0, SQUARE_1, CARD_3,
      BHSP_1, COMPLEX1, SEQ_2, ORDINAL2, XXREAL_2, VALUED_0, RSSPACE;
 notations TARSKI, SUBSET_1, XBOOLE_0, ZFMISC_1, ORDINAL1, NUMBERS, XCMPLX_0,
      XXREAL_0, XREAL_0, COMPLEX1, STRUCT_0, ALGSTR_0, REAL_1, NAT_1, RELAT_1,
      FUNCT_1, PARTFUN1, FUNCT_2, REALSET1, FUNCOP_1, RLVECT_1, RLSUB_1,
      BHSP_1, SQUARE_1, VALUED_1, SEQ_1, SEQ_2, SERIES_1, BINOP_1;
 constructors PARTFUN1, BINOP_1, FUNCOP_1, REAL_1, SQUARE_1, NAT_1, NAT_D,
      SEQ_2, SEQM_3, SERIES_1, REALSET1, RLSUB_1, BHSP_1, SEQ_1, VALUED_1,
      RELSET_1, COMSEQ_2;
 registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED,
      REALSET1, STRUCT_0, RLVECT_1, BHSP_1, ALGSTR_0, VALUED_1, FUNCT_2,
      VALUED_0, SERIES_1;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;


begin

definition
  func the_set_of_RealSequences -> non empty set means
:: RSSPACE:def 1

  for x being set holds x in it iff x is Real_Sequence;
end;

definition
  let a be set such that
 a in the_set_of_RealSequences;
  func seq_id(a) -> Real_Sequence equals
:: RSSPACE:def 2

  a;
end;

definition
  let a be set such that
 a in REAL;
  func R_id(a) -> Real equals
:: RSSPACE:def 3

  a;
end;

definition
  func l_add -> BinOp of the_set_of_RealSequences means
:: RSSPACE:def 4

  for a,b being
  Element of the_set_of_RealSequences holds it.(a,b) = seq_id(a)+seq_id(b);
end;

definition
  func l_mult -> Function of [: REAL, the_set_of_RealSequences :],
  the_set_of_RealSequences means
:: RSSPACE:def 5

  for r,x be set st r in REAL & x in
  the_set_of_RealSequences holds it.(r,x) = R_id(r)(#)seq_id(x);
end;

definition
  func Zeroseq -> Element of the_set_of_RealSequences means
:: RSSPACE:def 6

  for n be Element of NAT holds (seq_id it).n=0;
end;

theorem :: RSSPACE:1
  for x be Real_Sequence holds seq_id x = x;

theorem :: RSSPACE:2
  for v,w being VECTOR of RLSStruct(#the_set_of_RealSequences,Zeroseq,
    l_add,l_mult#) holds v + w = seq_id(v)+seq_id(w);

theorem :: RSSPACE:3
  for r being Real, v being VECTOR of RLSStruct(#
the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds r * v = r(#)seq_id(v);

registration
  cluster RLSStruct (# the_set_of_RealSequences, Zeroseq, l_add, l_mult #) ->
    Abelian;
end;

theorem :: RSSPACE:4
  for u,v,w being VECTOR of RLSStruct(# the_set_of_RealSequences,
    Zeroseq,l_add,l_mult #) holds (u + v) + w = u + (v + w);

theorem :: RSSPACE:5
  for v being VECTOR of RLSStruct(# the_set_of_RealSequences,
    Zeroseq,l_add,l_mult #) holds v + 0.RLSStruct(# the_set_of_RealSequences,
    Zeroseq,l_add,l_mult #) = v;

theorem :: RSSPACE:6
  for v being VECTOR of RLSStruct(# the_set_of_RealSequences,
    Zeroseq,l_add,l_mult #) ex w being VECTOR of RLSStruct(#
    the_set_of_RealSequences,Zeroseq,l_add,l_mult #) st v + w = 0.RLSStruct(#
    the_set_of_RealSequences,Zeroseq,l_add,l_mult #);

theorem :: RSSPACE:7
  for a being Real, v,w being VECTOR of RLSStruct(#
the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds a * (v + w) = a * v + a
  * w;

theorem :: RSSPACE:8
  for a,b being Real, v being VECTOR of RLSStruct(#
the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds (a + b) * v = a * v + b
  * v;

theorem :: RSSPACE:9
  for a,b be Real, v being VECTOR of RLSStruct(#
the_set_of_RealSequences,Zeroseq,l_add,l_mult #) holds (a * b) * v = a * (b * v
  );

theorem :: RSSPACE:10
  for v being VECTOR of RLSStruct(# the_set_of_RealSequences,
    Zeroseq,l_add,l_mult #) holds 1 * v = v;

definition
  func Linear_Space_of_RealSequences -> RLSStruct equals
:: RSSPACE:def 7
  RLSStruct (#
    the_set_of_RealSequences, Zeroseq, l_add, l_mult #);
end;

registration
  cluster Linear_Space_of_RealSequences -> strict non empty;
end;

registration
  cluster Linear_Space_of_RealSequences -> Abelian add-associative
    right_zeroed right_complementable vector-distributive
    scalar-distributive scalar-associative scalar-unital;
end;

definition
  let X be RealLinearSpace;
  let X1 be Subset of X such that
 X1 is linearly-closed non empty;
  func Add_(X1,X) -> BinOp of X1 equals
:: RSSPACE:def 8

  (the addF of X)||X1;
end;

definition
  let X be RealLinearSpace;
  let X1 be Subset of X such that
 X1 is linearly-closed non empty;
  func Mult_(X1,X) -> Function of [:REAL,X1:], X1 equals
:: RSSPACE:def 9

  (the Mult of X) | [:REAL,X1:];
end;

definition
  let X be RealLinearSpace, X1 be Subset of X such that
 X1 is linearly-closed non empty;
  func Zero_(X1,X) -> Element of X1 equals
:: RSSPACE:def 10

  0.X;
end;

theorem :: RSSPACE:11
  for V be RealLinearSpace, V1 be Subset of V st V1 is
linearly-closed non empty holds RLSStruct (# V1,Zero_(V1,V), Add_(V1,V),Mult_(
    V1,V) #) is Subspace of V;

definition
  func the_set_of_l2RealSequences -> Subset of Linear_Space_of_RealSequences
  means
:: RSSPACE:def 11

  for x being set holds x in it iff x in the_set_of_RealSequences &
  seq_id(x)(#)seq_id(x) is summable;
end;

registration
  cluster the_set_of_l2RealSequences -> linearly-closed non empty;
end;

theorem :: RSSPACE:12
  RLSStruct(# the_set_of_l2RealSequences, Zero_(
    the_set_of_l2RealSequences,Linear_Space_of_RealSequences), Add_(
    the_set_of_l2RealSequences,Linear_Space_of_RealSequences), Mult_(
    the_set_of_l2RealSequences,Linear_Space_of_RealSequences) #) is Subspace of
  Linear_Space_of_RealSequences;

theorem :: RSSPACE:13
  RLSStruct (# the_set_of_l2RealSequences, Zero_(
    the_set_of_l2RealSequences,Linear_Space_of_RealSequences), Add_(
    the_set_of_l2RealSequences,Linear_Space_of_RealSequences), Mult_(
the_set_of_l2RealSequences,Linear_Space_of_RealSequences) #) is RealLinearSpace
;

theorem :: RSSPACE:14
  the carrier of Linear_Space_of_RealSequences =
  the_set_of_RealSequences & (for x be set holds x is VECTOR of
  Linear_Space_of_RealSequences iff x is Real_Sequence ) & (for u be VECTOR of
  Linear_Space_of_RealSequences holds u =seq_id(u) ) & (for u,v be VECTOR of
Linear_Space_of_RealSequences holds u+v =seq_id(u)+seq_id(v) ) & for r be Real
  for u be VECTOR of Linear_Space_of_RealSequences holds r*u =r(#)seq_id(u);

definition
  func l_scalar -> Function of [:the_set_of_l2RealSequences,
  the_set_of_l2RealSequences:], REAL means
:: RSSPACE:def 12
  for x,y be set st x in
  the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds it.(x,y) =
  Sum(seq_id(x)(#)seq_id(y));
end;

registration
  cluster UNITSTR (# the_set_of_l2RealSequences, Zero_(
      the_set_of_l2RealSequences,Linear_Space_of_RealSequences), Add_(
      the_set_of_l2RealSequences,Linear_Space_of_RealSequences), Mult_(
the_set_of_l2RealSequences,Linear_Space_of_RealSequences), l_scalar #) -> non
    empty;
end;

definition
  func l2_Space -> non empty UNITSTR equals
:: RSSPACE:def 13
  UNITSTR (#
    the_set_of_l2RealSequences, Zero_(the_set_of_l2RealSequences,
    Linear_Space_of_RealSequences), Add_(the_set_of_l2RealSequences,
    Linear_Space_of_RealSequences), Mult_(the_set_of_l2RealSequences,
    Linear_Space_of_RealSequences), l_scalar #);
end;

theorem :: RSSPACE:15
  for l be RLSStruct st the RLSStruct of l is RealLinearSpace
  holds l is RealLinearSpace;

theorem :: RSSPACE:16
  for rseq be Real_Sequence st (for n be Element of NAT holds rseq.n=0)
  holds rseq is summable & Sum rseq = 0;

theorem :: RSSPACE:17
  for rseq be Real_Sequence st (for n be Element of NAT holds 0 <= rseq.
n) & rseq is summable & Sum rseq=0 holds for n be Element of NAT holds rseq.n =
  0;

registration
  cluster l2_Space -> Abelian add-associative right_zeroed
    right_complementable vector-distributive scalar-distributive
    scalar-associative scalar-unital;
end;