:: Banach Space of Bounded Real Sequences
::  by Yasumasa Suzuki
::
:: Received January 6, 2004
:: Copyright (c) 2004-2021 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, SEQ_1, SUBSET_1, FUNCT_1, XXREAL_0, ORDINAL2, RELAT_1,
      XXREAL_2, RSSPACE, TARSKI, XBOOLE_0, NAT_1, CARD_1, RLSUB_1, REAL_1,
      RLVECT_1, VALUED_1, ARYTM_3, ALGSTR_0, COMPLEX1, SEQ_4, NORMSP_1,
      STRUCT_0, SUPINF_2, ARYTM_1, ZFMISC_1, REALSET1, PRE_TOPC, MEMBER_1,
      RSSPACE3, SEQ_2, FUNCOP_1, FUNCSDOM, FUNCT_2, LOPBAN_1, REWRITE1,
      RSSPACE4, METRIC_1, RELAT_2, NORMSP_0, FUNCT_7, ASYMPT_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, RELAT_1, PRE_TOPC,
      DOMAIN_1, FUNCOP_1, REALSET1, XXREAL_0, XXREAL_2, XCMPLX_0, COMPLEX1,
      REAL_1, ORDINAL1, NAT_1, STRUCT_0, ALGSTR_0, XREAL_0, NUMBERS, FUNCT_1,
      RELSET_1, FUNCT_2, INTEGRA2, RLVECT_1, NORMSP_0, NORMSP_1, VALUED_1,
      SEQ_1, SEQ_2, SEQ_4, RLSUB_1, PARTFUN1, RSSPACE, RSSPACE3, LOPBAN_1;
 constructors REAL_1, COMPLEX1, REALSET1, RLSUB_1, INTEGRA2, RSSPACE3,
      LOPBAN_1, RVSUM_1, SEQ_4, RELSET_1, BINOP_2, SEQ_2, SERIES_1, COMSEQ_2,
      BINOP_1, SEQ_1, FUNCSDOM;
 registrations SUBSET_1, RELAT_1, ORDINAL1, FUNCT_2, NUMBERS, XREAL_0,
      MEMBERED, REALSET1, STRUCT_0, RLVECT_1, RFUNCT_1, SEQ_2, NORMSP_1,
      RSSPACE3, VALUED_0, RSSPACE, VALUED_1, SEQ_4, NORMSP_0, RELSET_1, NAT_1,
      SEQ_1;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;


begin

definition
  func the_set_of_BoundedRealSequences -> Subset of
  Linear_Space_of_RealSequences means
:: RSSPACE4:def 1

  for x being object holds x in it iff x
  in the_set_of_RealSequences & seq_id x is bounded;
end;

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

registration
  cluster RLSStruct (# the_set_of_BoundedRealSequences, Zero_(
      the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences), Add_(
      the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences), Mult_(
the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences) #) -> Abelian
    add-associative right_zeroed right_complementable vector-distributive
    scalar-distributive scalar-associative scalar-unital;
end;

definition
  func linfty_norm -> Function of the_set_of_BoundedRealSequences, REAL means
:: RSSPACE4:def 2

  for x be object st x in the_set_of_BoundedRealSequences
  holds it.x = upper_bound rng abs seq_id x;
end;

theorem :: RSSPACE4:1
  for rseq be Real_Sequence holds rseq is bounded &
  upper_bound rng abs rseq = 0
  iff for n be Nat holds rseq.n = 0;

registration
  cluster NORMSTR (# the_set_of_BoundedRealSequences, Zero_(
      the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences), Add_(
      the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences), Mult_(
the_set_of_BoundedRealSequences,Linear_Space_of_RealSequences), linfty_norm #)
    -> Abelian add-associative right_zeroed right_complementable
    vector-distributive scalar-distributive scalar-associative scalar-unital;
end;

definition
  func linfty_Space -> non empty NORMSTR equals
:: RSSPACE4:def 3
  NORMSTR (#
    the_set_of_BoundedRealSequences, Zero_(the_set_of_BoundedRealSequences,
    Linear_Space_of_RealSequences), Add_(the_set_of_BoundedRealSequences,
    Linear_Space_of_RealSequences), Mult_(the_set_of_BoundedRealSequences,
    Linear_Space_of_RealSequences), linfty_norm #);
end;

theorem :: RSSPACE4:2
  the carrier of linfty_Space = the_set_of_BoundedRealSequences & (
for x be set holds x is VECTOR of linfty_Space iff x is Real_Sequence & seq_id
  x is bounded ) & 0.linfty_Space = Zeroseq & ( for u be VECTOR of linfty_Space
holds u = seq_id u ) & ( for u,v be VECTOR of linfty_Space holds u+v =seq_id(u)
+seq_id(v) ) &
( for r be Real for u be VECTOR of linfty_Space holds r*u =r(#)
seq_id(u) ) & ( for u be VECTOR of linfty_Space holds -u = -seq_id u & seq_id(-
  u) = -seq_id u ) & ( for u,v be VECTOR of linfty_Space holds u-v =seq_id(u)-
  seq_id(v) ) & ( for v be VECTOR of linfty_Space holds seq_id v is bounded ) &
  for v be VECTOR of linfty_Space holds ||.v.|| = upper_bound rng abs seq_id v;

theorem :: RSSPACE4:3
  for x, y being Point of linfty_Space,
   a be Real holds ( ||.x.|| =
  0 iff x = 0.linfty_Space ) & 0 <= ||.x.|| & ||.x+y.|| <= ||.x.|| + ||.y.|| &
  ||. a*x .|| = |.a.| * ||.x.||;

registration
  cluster linfty_Space -> reflexive discerning RealNormSpace-like
  vector-distributive scalar-distributive scalar-associative scalar-unital
  Abelian add-associative right_zeroed right_complementable;
end;

theorem :: RSSPACE4:4
  for vseq be sequence of linfty_Space st vseq is
  Cauchy_sequence_by_Norm holds vseq is convergent;

begin

definition
  let X be non empty set;
  let Y be RealNormSpace;
  let IT be Function of X, the carrier of Y;
  attr IT is bounded means
:: RSSPACE4:def 4

  ex K being Real st 0 <= K & for x being Element of X holds ||. IT.x .|| <= K;
end;

theorem :: RSSPACE4:5
  for X be non empty set for Y be RealNormSpace holds for f be
Function of X,the carrier of Y st (for x be Element of X holds f.x=0.Y) holds f
  is bounded;

registration
  let X be non empty set;
  let Y be RealNormSpace;
  cluster bounded for Function of X,the carrier of Y;
end;

definition
  let X be non empty set;
  let Y be RealNormSpace;
  func BoundedFunctions(X,Y) -> Subset of RealVectSpace(X,Y) means
:: RSSPACE4:def 5

  for
  x being set holds x in it iff x is bounded Function of X,the carrier of Y;
end;

registration
  let X be non empty set;
  let Y be RealNormSpace;
  cluster BoundedFunctions(X,Y) -> non empty;
end;

theorem :: RSSPACE4:6
  for X be non empty set for Y be RealNormSpace holds
  BoundedFunctions(X,Y) is linearly-closed;

theorem :: RSSPACE4:7
  for X be non empty set for Y be RealNormSpace holds RLSStruct (#
BoundedFunctions(X,Y), Zero_(BoundedFunctions(X,Y), RealVectSpace(X,Y)), Add_(
    BoundedFunctions(X,Y), RealVectSpace(X,Y)), Mult_(BoundedFunctions(X,Y),
    RealVectSpace(X,Y)) #) is Subspace of RealVectSpace(X,Y);

registration
  let X be non empty set;
  let Y be RealNormSpace;
  cluster RLSStruct (# BoundedFunctions(X,Y), Zero_(BoundedFunctions(X,Y),
RealVectSpace(X,Y)), Add_(BoundedFunctions(X,Y), RealVectSpace(X,Y)), Mult_(
      BoundedFunctions(X,Y), RealVectSpace(X,Y)) #) -> Abelian add-associative
    right_zeroed right_complementable vector-distributive
    scalar-distributive scalar-associative scalar-unital;
end;

definition
  let X be non empty set;
  let Y be RealNormSpace;
  func R_VectorSpace_of_BoundedFunctions(X,Y) -> RealLinearSpace equals
:: RSSPACE4:def 6
RLSStruct (# BoundedFunctions(X,Y), Zero_(BoundedFunctions(X,Y), RealVectSpace(
X,Y)), Add_(BoundedFunctions(X,Y), RealVectSpace(X,Y)), Mult_(BoundedFunctions(
    X,Y), RealVectSpace(X,Y)) #);
end;

registration
  let X be non empty set;
  let Y be RealNormSpace;
  cluster R_VectorSpace_of_BoundedFunctions(X,Y) -> strict;
end;

theorem :: RSSPACE4:8
  for X be non empty set for Y be RealNormSpace for f,g,h be
  VECTOR of R_VectorSpace_of_BoundedFunctions(X,Y) for f9,g9,h9 be bounded
  Function of X,the carrier of Y st f9=f & g9=g & h9=h holds (h = f+g iff for x
  be Element of X holds h9.x = f9.x + g9.x );

theorem :: RSSPACE4:9
  for X be non empty set for Y be RealNormSpace for f,h be VECTOR
  of R_VectorSpace_of_BoundedFunctions(X,Y) for f9,h9 be bounded Function of X,
  the carrier of Y st f9=f & h9=h
for a be Real holds h = a*f iff for x be
  Element of X holds h9.x = a*f9.x;

theorem :: RSSPACE4:10
  for X be non empty set for Y be RealNormSpace holds 0.
  R_VectorSpace_of_BoundedFunctions(X,Y) =(X -->0.Y);

definition
  let X be non empty set;
  let Y be RealNormSpace;
  let f be object such that
 f in BoundedFunctions(X,Y);
  func modetrans(f,X,Y) -> bounded Function of X,the carrier of Y equals
:: RSSPACE4:def 7


  f;
end;

definition
  let X be non empty set;
  let Y be RealNormSpace;
  let u be Function of X,the carrier of Y;
  func PreNorms(u) -> non empty Subset of REAL equals
:: RSSPACE4:def 8
  the set of all ||.u.t.|| where t is
  Element of X ;
end;

theorem :: RSSPACE4:11
  for X be non empty set for Y be RealNormSpace for g be bounded
  Function of X,the carrier of Y holds PreNorms(g) is bounded_above;

theorem :: RSSPACE4:12
  for X be non empty set for Y be RealNormSpace for g be Function of X,
  the carrier of Y holds g is bounded iff PreNorms(g) is bounded_above;

definition
  let X be non empty set;
  let Y be RealNormSpace;
  func BoundedFunctionsNorm(X,Y) -> Function of BoundedFunctions(X,Y), REAL
  means
:: RSSPACE4:def 9

  for x be object st x in BoundedFunctions(X,Y) holds it.x = upper_bound
  PreNorms(modetrans(x,X,Y));
end;

theorem :: RSSPACE4:13
  for X be non empty set for Y be RealNormSpace for f be bounded
  Function of X,the carrier of Y holds modetrans(f,X,Y)=f;

theorem :: RSSPACE4:14
  for X be non empty set for Y be RealNormSpace for f be bounded
Function of X,the carrier of Y holds BoundedFunctionsNorm(X,Y).f =
 upper_bound PreNorms
  (f);

definition
  let X be non empty set;
  let Y be RealNormSpace;
  func R_NormSpace_of_BoundedFunctions(X,Y) -> non empty NORMSTR equals
:: RSSPACE4:def 10
NORMSTR (# BoundedFunctions(X,Y), Zero_(BoundedFunctions(X,Y), RealVectSpace(X,
Y)), Add_(BoundedFunctions(X,Y), RealVectSpace(X,Y)), Mult_(BoundedFunctions(X,
    Y), RealVectSpace(X,Y)), BoundedFunctionsNorm(X,Y) #);
end;

theorem :: RSSPACE4:15
  for X be non empty set for Y be RealNormSpace holds (X --> 0.Y)
  = 0.R_NormSpace_of_BoundedFunctions(X,Y);

theorem :: RSSPACE4:16
  for X be non empty set for Y be RealNormSpace for f being Point
  of R_NormSpace_of_BoundedFunctions(X,Y) for g be bounded Function of X,the
  carrier of Y st g=f holds for t be Element of X holds ||.g.t.|| <= ||.f.||;

theorem :: RSSPACE4:17
  for X be non empty set for Y be RealNormSpace for f being Point of
  R_NormSpace_of_BoundedFunctions(X,Y) holds 0 <= ||.f.||;

theorem :: RSSPACE4:18
  for X be non empty set for Y be RealNormSpace for f being Point
  of R_NormSpace_of_BoundedFunctions(X,Y) st f = 0.
  R_NormSpace_of_BoundedFunctions(X,Y) holds 0 = ||.f.||;

theorem :: RSSPACE4:19
  for X be non empty set for Y be RealNormSpace for f,g,h be Point
of R_NormSpace_of_BoundedFunctions(X,Y) for f9,g9,h9 be bounded Function of X,
the carrier of Y st f9=f & g9=g & h9=h holds (h = f+g iff for x be Element of X
  holds h9.x = f9.x + g9.x );

theorem :: RSSPACE4:20
  for X be non empty set for Y be RealNormSpace for f,h be Point
of R_NormSpace_of_BoundedFunctions(X,Y) for f9,h9 be bounded Function of X,the
carrier of Y st f9=f & h9=h
for a be Real holds h = a*f iff for x be Element of
  X holds h9.x = a*f9.x;

theorem :: RSSPACE4:21
  for X be non empty set for Y be RealNormSpace for f, g being
Point of R_NormSpace_of_BoundedFunctions(X,Y)
 for a be Real holds ( ||.f.|| = 0
iff f = 0.R_NormSpace_of_BoundedFunctions(X,Y) ) & ||.a*f.|| = |.a.| * ||.f.||
  & ||.f+g.|| <= ||.f.|| + ||.g.||;

theorem :: RSSPACE4:22
  for X be non empty set for Y be RealNormSpace holds
  R_NormSpace_of_BoundedFunctions(X,Y) is
   reflexive discerning RealNormSpace-like;

theorem :: RSSPACE4:23
  for X be non empty set for Y be RealNormSpace holds
  R_NormSpace_of_BoundedFunctions(X,Y) is RealNormSpace;

registration
  let X be non empty set;
  let Y be RealNormSpace;
  cluster R_NormSpace_of_BoundedFunctions(X,Y) ->
   reflexive discerning RealNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
 Abelian add-associative right_zeroed right_complementable;
end;

theorem :: RSSPACE4:24
  for X be non empty set for Y be RealNormSpace for f,g,h be Point
of R_NormSpace_of_BoundedFunctions(X,Y) for f9,g9,h9 be bounded Function of X,
the carrier of Y st f9=f & g9=g & h9=h holds (h = f-g iff for x be Element of X
  holds h9.x = f9.x - g9.x );

theorem :: RSSPACE4:25
  for X be non empty set for Y be RealNormSpace st Y is complete
  for seq be sequence of R_NormSpace_of_BoundedFunctions(X,Y) st seq is
  Cauchy_sequence_by_Norm holds seq is convergent;

theorem :: RSSPACE4:26
  for X be non empty set for Y be RealBanachSpace holds
  R_NormSpace_of_BoundedFunctions(X,Y) is RealBanachSpace;

registration
  let X be non empty set;
  let Y be RealBanachSpace;
  cluster R_NormSpace_of_BoundedFunctions (X,Y) -> complete;
end;