:: Hilbert Space of Complex Sequences
::  by Noboru Endou
::
:: Received February 24, 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, COMSEQ_1, ARYTM_3, FUNCT_1, SUBSET_1, COMPLEX1, ARYTM_1,
      RELAT_1, XCMPLX_0, SERIES_1, CARD_1, REAL_1, XXREAL_0, SQUARE_1, CARD_3,
      ORDINAL2, SEQ_2, VALUED_1, CSSPACE, RSSPACE, SUPINF_2, RLVECT_1,
      ALGSTR_0, ZFMISC_1, STRUCT_0, REALSET1, PROB_2, BHSP_1, SEQ_1, PRE_TOPC,
      FUNCOP_1, NAT_1, BHSP_3, NORMSP_1, XXREAL_2, REWRITE1, CSSPACE2;
 notations SUBSET_1, ZFMISC_1, ORDINAL1, XCMPLX_0, XXREAL_0, NUMBERS, COMPLEX1,
      XREAL_0, NAT_1, STRUCT_0, ALGSTR_0, RELAT_1, DOMAIN_1, PARTFUN1, FUNCT_1,
      FUNCT_2, BINOP_1, FUNCOP_1, REALSET1, PRE_TOPC, SQUARE_1, VALUED_1,
      SEQ_1, SEQ_2, SERIES_1, COMSEQ_1, COMSEQ_2, COMSEQ_3, NORMSP_0, CLVECT_1,
      CLVECT_2, CSSPACE;
 constructors BINOP_1, FUNCOP_1, REAL_1, SQUARE_1, COMSEQ_2, COMSEQ_3,
      REALSET1, CLVECT_2, SEQ_2, RELSET_1, CFUNCDOM;
 registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS,
      XCMPLX_0, XXREAL_0, MEMBERED, COMSEQ_2, COMSEQ_3, REALSET1, STRUCT_0,
      CSSPACE, VALUED_1, VALUED_0, SEQ_2, XREAL_0, SQUARE_1, NAT_1, INT_1;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;


begin

theorem :: CSSPACE2:1
  the carrier of Complex_l2_Space = the_set_of_l2ComplexSequences & (for
x be set holds x is Element of Complex_l2_Space iff x is Complex_Sequence & |.
seq_id(x).|(#)|.seq_id(x).| is summable) & (for x be set holds x is Element of
  Complex_l2_Space iff x is Complex_Sequence & seq_id(x)(#)(seq_id(x))*' is
  absolutely_summable ) & 0.Complex_l2_Space = CZeroseq & (for u be VECTOR of
  Complex_l2_Space holds u =seq_id(u)) & (for u,v be VECTOR of Complex_l2_Space
  holds u+v =seq_id(u)+seq_id(v)) & (for r be Complex for u be VECTOR of
  Complex_l2_Space holds r*u =r(#)seq_id(u)) & (for u be VECTOR of
  Complex_l2_Space holds -u =-seq_id(u) & seq_id(-u)=-seq_id(u)) & (for u,v be
VECTOR of Complex_l2_Space holds u-v =seq_id(u)-seq_id(v)) & for v,w be VECTOR
  of Complex_l2_Space holds |.seq_id(v).|(#)|.seq_id(w).| is summable & for v,w
  be VECTOR of Complex_l2_Space holds v.|.w = Sum(seq_id(v)(#)(seq_id(w))*');

theorem :: CSSPACE2:2
  for x,y,z being Point of Complex_l2_Space for a be Complex holds
  ( x.|.x = 0 iff x = 0.Complex_l2_Space ) & Re(x.|.x) >= 0 & Im(x.|.x) = 0 & x
  .|.y = (y.|.x)*' & (x+y).|.z = x.|.z + y.|.z & (a*x).|.y = a*(x.|.y);

registration
  cluster Complex_l2_Space -> ComplexUnitarySpace-like;
end;

registration
  cluster Complex_l2_Space -> complete;
end;

registration
 cluster complete for ComplexUnitarySpace;
end;

definition
  mode ComplexHilbertSpace is complete ComplexUnitarySpace;
end;

begin  :: Some corollaries of complex sequences

theorem :: CSSPACE2:3
  for z1, z2 be Complex st (Re z1)*(Im z2) = (Re z2)*(Im z1) & (Re z1)*(
  Re z2)+(Im z1)*(Im z2) >= 0 holds |.z1 + z2.| = |.z1.| + |.z2.|;

theorem :: CSSPACE2:4
  for x,y be Complex holds 2*|.x*y.| <= |.x.|^2 + |.y.|^2;

theorem :: CSSPACE2:5
  for x,y be Complex holds |.x+y.|*|.x+y.| <= 2*|.x.|*|.x.| + 2*|.y.|*|.
  y.| & |.x.|*|.x.| <= 2*|.x-y.|*|.x-y.| + 2*|.y.|*|.y.|;

::$CT

theorem :: CSSPACE2:7
  for seq be Complex_Sequence holds Partial_Sums (seq*') = (Partial_Sums
  seq) *';

theorem :: CSSPACE2:8
  for seq be Complex_Sequence, n be Nat st
  (for i be Nat holds (Re seq).i >= 0 & (Im seq).i = 0)
  holds (|.Partial_Sums seq.|).n = (Partial_Sums |.seq.|).n;

theorem :: CSSPACE2:9
  for seq be Complex_Sequence st seq is summable holds Sum (seq*') = (
  Sum seq)*';

theorem :: CSSPACE2:10
  for seq be Complex_Sequence st seq is absolutely_summable holds |. Sum
  seq .| <= Sum |.seq.|;

theorem :: CSSPACE2:11
  for seq be Complex_Sequence st seq is summable &
   (for n be Nat holds (Re seq).n >= 0 & (Im seq).n = 0)
   holds |. Sum seq .| = Sum |.seq.|;

theorem :: CSSPACE2:12
  for seq be Complex_Sequence, n be Nat holds (Re (seq(#)seq
  *')).n >= 0 & (Im (seq(#)seq*')).n = 0;

theorem :: CSSPACE2:13
  for seq be Complex_Sequence st seq is absolutely_summable & Sum |.seq
  .|=0 holds for n be Nat holds seq.n =0c;

theorem :: CSSPACE2:14
  for seq being Complex_Sequence holds |.seq.| = |.seq*'.|;

theorem :: CSSPACE2:15
  for c be Complex, seq be Complex_Sequence st seq is convergent for
rseq be Real_Sequence st (for m be Nat holds rseq .m = |.seq.m-c.|*
|.seq.m-c.|) holds rseq is convergent & lim rseq = |.lim seq-c.|*|.lim seq-c.|;

theorem :: CSSPACE2:16
  for c be Complex, seq1 be Real_Sequence, seq be Complex_Sequence st
  seq is convergent & seq1 is convergent for rseq be Real_Sequence st (for i be
  Nat holds rseq.i = |.seq.i-c.|*|.seq.i-c.|+seq1.i) holds rseq is
  convergent & lim rseq = |.lim seq-c.|*|.lim seq-c.|+lim seq1;