:: The Product Space of Real Normed Spaces and Its Properties
::  by Noboru Endou , Yasunari Shidama and Keiichi Miyajima
::
:: Received July 9, 2007
:: Copyright (c) 2007-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 SEQ_1, SUBSET_1, NUMBERS, FUNCT_1, COMPLEX1, ARYTM_1, SEQ_2,
      ORDINAL2, CARD_1, ARYTM_3, XXREAL_0, FINSEQ_1, NAT_1, RVSUM_1, SQUARE_1,
      RELAT_1, CARD_3, FINSEQ_2, ZFMISC_1, MCART_1, PRVECT_1, XBOOLE_0,
      RLVECT_1, GROUP_2, STRUCT_0, ALGSTR_0, BINOP_1, VECTSP_1, REAL_1,
      SUPINF_2, FUNCT_6, FINSEQOP, SETWISEO, NORMSP_1, TARSKI, PRE_TOPC,
      EUCLID, FUNCT_2, REAL_NS1, REWRITE1, RSSPACE3, PRVECT_2, NORMSP_0,
      METRIC_1, RELAT_2, FUNCT_7;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_3, XCMPLX_0,
      XXREAL_0, NUMBERS, XREAL_0, COMPLEX1, NAT_1, RELAT_1, FUNCT_1, RVSUM_1,
      STRUCT_0, ALGSTR_0, FUNCT_2, FUNCT_3, BINOP_1, REAL_1, SEQ_1, COMSEQ_2,
      SEQ_2, RLVECT_1, VECTSP_1, SETWISEO, FINSEQ_1, FINSEQ_2, FINSEQOP,
      SQUARE_1, PRE_TOPC, EUCLID, PRVECT_1, NORMSP_0, NORMSP_1, RSSPACE3,
      LOPBAN_1, REAL_NS1;
 constructors FUNCT_3, FINSEQOP, REAL_1, SEQ_2, COMPLEX1, SQUARE_1, BINOP_2,
      SETWISEO, PRVECT_1, RSSPACE3, LOPBAN_1, REAL_NS1, RVSUM_1, NORMSP_1,
      RELSET_1, COMSEQ_2, NUMBERS;
 registrations STRUCT_0, FINSEQ_2, FINSEQ_1, CARD_3, RLVECT_1, PRVECT_1,
      XREAL_0, MEMBERED, NORMSP_1, REAL_NS1, ORDINAL1, FUNCT_1, FUNCT_2,
      RELAT_1, XBOOLE_0, NUMBERS, VALUED_0, NORMSP_0, EUCLID, SQUARE_1;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: The Product Space of Real Linear Spaces

theorem :: PRVECT_2:1
  for s,t be Real_Sequence, g be Real st
  for n be Element of NAT holds t.n = |.s.n-g.| holds
  s is convergent & lim s = g iff t is convergent & lim t = 0;

theorem :: PRVECT_2:2
  for x,y be FinSequence of REAL st len x = len y &
  for i be Element of NAT st i in Seg len x holds 0 <= x.i & x.i <= y.i
    holds |.x.| <= |.y.|;

theorem :: PRVECT_2:3
  for F be FinSequence of REAL st
  for i be Element of NAT st i in dom F holds F.i = 0 holds Sum F = 0;

definition
  let f be Function;
  let X be set;
  mode MultOps of X,f -> Function means
:: PRVECT_2:def 1

    dom it = dom f &
    for i being set st i in dom f holds it.i is Function of [:X,f.i:],f.i;
end;

registration
  let F be Domain-Sequence;
  let X be set;
  cluster -> FinSequence-like for MultOps of X,F;
end;

theorem :: PRVECT_2:4
  for X be set, F be Domain-Sequence, p be FinSequence holds
    (p is MultOps of X,F iff len p = len F &
    for i be set st i in dom F holds p.i is Function of [:X,F.i:],F.i);

definition
  let F be Domain-Sequence;
  let X be set;
  let p be MultOps of X,F;
  let i be Element of dom F;
  redefine func p.i -> Function of [:X,F.i:],F.i;
end;

theorem :: PRVECT_2:5
  for X be non empty set, F be Domain-Sequence,
      f,g being Function of [:X,product F:],product F st
  for x be Element of X, d being Element of product F,
      i being Element of dom F holds (f.(x,d)).i = (g.(x,d)).i holds f = g;

definition
  let F be Domain-Sequence;
  let X be non empty set;
  let p be MultOps of X,F;
  func [:p:] -> Function of [:X,product F:],product F means
:: PRVECT_2:def 2
  for x be Element of X, d being Element of product F,
      i being Element of dom F holds (it.(x,d)).i = (p.i).(x,d.i);
end;

definition
  let R be Relation;
  attr R is RealLinearSpace-yielding means
:: PRVECT_2:def 3
  for S be set st S in rng R holds S is RealLinearSpace;
end;

registration
  cluster non empty RealLinearSpace-yielding for FinSequence;
end;

definition
  mode RealLinearSpace-Sequence is non empty RealLinearSpace-yielding
    FinSequence;
end;

definition
  let G be RealLinearSpace-Sequence;
  let j be Element of dom G;
  redefine func G.j -> RealLinearSpace;
end;

registration
  cluster RealLinearSpace-yielding -> non-empty-addLoopStr-yielding
    for Relation;
end;

definition
  let G be RealLinearSpace-Sequence, j be Element of dom carr G;
  redefine func G.j -> RealLinearSpace;
end;

definition
::$CD 4
  let G be RealLinearSpace-Sequence;
  func multop G -> MultOps of REAL,carr G means
:: PRVECT_2:def 8

  len it = len carr G &
  for j be Element of dom carr G holds it.j = the Mult of G.j;
end;

definition
  let G be RealLinearSpace-Sequence;
  func product G -> strict non empty RLSStruct equals
:: PRVECT_2:def 9
    RLSStruct(# product carr G, zeros G, [:addop G:], [:multop G:] #);
end;

registration
  let G be RealLinearSpace-Sequence;
  cluster product G -> Abelian add-associative right_zeroed
    right_complementable vector-distributive scalar-distributive
    scalar-associative scalar-unital;
end;

begin :: The Product Space of Real Normed Spaces

definition
  let R be Relation;
  attr R is RealNormSpace-yielding means
:: PRVECT_2:def 10

  for x be set st x in rng R holds x is RealNormSpace;
end;

registration
  cluster non empty RealNormSpace-yielding for FinSequence;
end;

definition
  mode RealNormSpace-Sequence is non empty RealNormSpace-yielding FinSequence;
end;

definition
  let G be RealNormSpace-Sequence;
  let j be Element of dom G;
  redefine func G.j -> RealNormSpace;
end;

registration
  cluster RealNormSpace-yielding -> RealLinearSpace-yielding for FinSequence;
end;

definition
  let G be RealNormSpace-Sequence;
  let x be Element of product carr G;
  func normsequence(G,x) -> Element of REAL len G means
:: PRVECT_2:def 11

  len it = len G
  & for j be Element of dom G holds it.j=(the normF of G.j).(x.j);
end;

definition
  let G be RealNormSpace-Sequence;
  func productnorm G -> Function of product carr (G qua
  RealLinearSpace-Sequence),REAL means
:: PRVECT_2:def 12

  for x being Element of product carr G holds it.x = |.normsequence(G,x).|;
end;

definition
  let G be RealNormSpace-Sequence;
  func product G -> strict non empty NORMSTR means
:: PRVECT_2:def 13

  the RLSStruct of it
  = product (G qua RealLinearSpace-Sequence) & the normF of it = productnorm G;
end;

reserve G for RealNormSpace-Sequence;

theorem :: PRVECT_2:6
  product G = NORMSTR(# product carr G,zeros G,[:addop G:],[:multop
    G:], productnorm G #);

theorem :: PRVECT_2:7
  for x be VECTOR of product G, y be Element of product carr G st
    x = y holds ||.x.|| = |.normsequence(G,y).|;

theorem :: PRVECT_2:8
  for x,y,z be Element of product carr G, i be Nat st
  i in dom x & z = [:addop G :].(x,y) holds
  normsequence(G,z).i <= (normsequence(G,x) + normsequence(G,y)).i;

theorem :: PRVECT_2:9
  for x be Element of product carr G, i be Nat st
    i in dom x holds 0 <= normsequence(G,x).i;

registration
  let G be RealNormSpace-Sequence;
  cluster product G -> reflexive discerning RealNormSpace-like
  vector-distributive scalar-distributive scalar-associative scalar-unital
  Abelian add-associative right_zeroed right_complementable;
end;

theorem :: PRVECT_2:10
  for G be RealNormSpace-Sequence, i be Element of dom G,
      x be Point of product G, y be Element of product carr G,
      xi be Point of G.i st y = x
  & xi = y.i holds ||.xi.|| <= ||.x.||;

theorem :: PRVECT_2:11
  for G be RealNormSpace-Sequence, i be Element of dom G,
      x,y be Point of product G, xi,yi be Point of G.i,
      zx,zy be Element of product carr G
  st xi=zx.i & zx=x & yi=zy.i & zy=y holds ||.yi - xi.|| <= ||.y - x.||;

theorem :: PRVECT_2:12
  for G be RealNormSpace-Sequence, seq be sequence of product G,
      x0 be Point of product G, y0 be Element of product carr G st
    x0 = y0 & seq is convergent & lim seq=x0 holds
    for i be Element of dom G ex seqi be sequence of
G.i st seqi is convergent & y0.i = lim seqi & for m be Element of NAT holds ex
  seqm be Element of product carr G st seqm= seq.m & seqi.m=seqm.i;

theorem :: PRVECT_2:13
  for G be RealNormSpace-Sequence, seq be sequence of (product G),
      x0 be Point of product G, y0 be Element of product carr G st x0=y0 &
  for i be Element of dom G
  ex seqi be sequence of G.i st seqi is convergent & y0.i = lim seqi &
  for m be Element of NAT holds ex seqm be Element of product carr G st
  seqm = seq.m & seqi.m=seqm.i holds seq is convergent & lim seq=x0;

theorem :: PRVECT_2:14
  for G be RealNormSpace-Sequence st
    for i be Element of dom G holds G.i is complete holds
  product G is complete;