:: Series on Complex {B}anach Algebra
::  by Noboru Endou
::
:: Received April 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, RLVECT_1, ALGSTR_0, XBOOLE_0, CLVECT_1, NAT_1, SUBSET_1,
      FUNCT_1, SUPINF_2, SERIES_1, ARYTM_3, CARD_1, SEQ_2, FUNCOP_1, REAL_1,
      XXREAL_0, NORMSP_1, ARYTM_1, CARD_3, ORDINAL2, LOPBAN_3, RSSPACE3,
      VALUED_0, RELAT_1, COMPLEX1, XCMPLX_0, XXREAL_2, CLOPBAN1, SEQ_1, POWER,
      CLOPBAN2, MESFUNC1, VECTSP_1, PREPOWER, STRUCT_0, COMSEQ_3, PRE_TOPC,
      VALUED_1;
 notations TARSKI, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, PRE_TOPC, DOMAIN_1,
      FUNCOP_1, XXREAL_0, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, ORDINAL1, NAT_1,
      STRUCT_0, ALGSTR_0, NUMBERS, RLVECT_1, VECTSP_1, NORMSP_1, VALUED_1,
      SEQ_1, VALUED_0, SEQ_2, SERIES_1, PREPOWER, POWER, NORMSP_0, CLVECT_1,
      CSSPACE3, BHSP_4, CLOPBAN1, CLOPBAN2, LOPBAN_3, RECDEF_1;
 constructors DOMAIN_1, REAL_1, COMPLEX1, SEQ_2, PREPOWER, SERIES_1, BHSP_4,
      CSSPACE3, CLOPBAN2, RECDEF_1, RELSET_1, BINOP_2, COMSEQ_2, BINOP_1;
 registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0,
      XREAL_0, MEMBERED, STRUCT_0, CLOPBAN2, VALUED_1, FUNCT_2, VALUED_0,
      FUNCOP_1, NORMSP_0, XCMPLX_0, NAT_1, INT_1;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;


begin :: Basic Properties of Sequences of Complex Normed Space

theorem :: CLOPBAN3:1
  for X be add-associative right_zeroed right_complementable non
empty CNORMSTR for seq be sequence of X st (for n be Nat holds seq.
  n = 0.X) holds for m be Nat holds (Partial_Sums seq).m = 0.X;

definition
  let X be ComplexNormSpace;

  let seq be sequence of X;
  attr seq is summable means
:: CLOPBAN3:def 1

  Partial_Sums seq is convergent;
end;

registration
  let X be ComplexNormSpace;
  cluster summable for sequence of X;
end;

definition
  let X be ComplexNormSpace;
  let seq be sequence of X;
  func Sum seq -> Element of X equals
:: CLOPBAN3:def 2
  lim Partial_Sums seq;
end;

definition
  let X be ComplexNormSpace;
  let seq be sequence of X;
  attr seq is norm_summable means
:: CLOPBAN3:def 3

  ||.seq.|| is summable;
end;

theorem :: CLOPBAN3:2
  for X be ComplexNormSpace, seq be sequence of X,
    m be Nat holds 0 <= ||.seq.||.m;

theorem :: CLOPBAN3:3
  for X be ComplexNormSpace, x,y,z be Element of X holds ||.x-y.||
  = ||.(x-z)+(z-y).||;

theorem :: CLOPBAN3:4
  for X be ComplexNormSpace, seq be sequence of X holds seq is
  convergent implies
  for s be Real st 0 < s ex n be Nat st for m be
  Nat st n<=m holds ||.seq.m -seq.n.||<s;

theorem :: CLOPBAN3:5
  for X be ComplexNormSpace, seq be sequence of X holds seq is
Cauchy_sequence_by_Norm iff
 for p be Real st p > 0 holds ex n be Nat
  st for m be Nat st n <= m holds ||.seq.m-seq.n.||< p;

theorem :: CLOPBAN3:6
  for X be ComplexNormSpace, seq be sequence of X st (for n be
  Nat holds seq.n = 0.X) holds for m be Nat holds (
  Partial_Sums ||.seq.||).m = 0;

theorem :: CLOPBAN3:7
  for X be ComplexNormSpace, seq,seq1 be sequence of X holds seq1
  is subsequence of seq & seq is convergent implies seq1 is convergent;

theorem :: CLOPBAN3:8
  for X be ComplexNormSpace, seq,seq1 be sequence of X holds seq1
  is subsequence of seq & seq is convergent implies lim seq1=lim seq;

:: Norm Space versions of SEQ_4_33 - SEQ_4_39

theorem :: CLOPBAN3:9
  for X be ComplexNormSpace, seq,seq1 be sequence of X, k be Element of
NAT holds seq is convergent implies (seq ^\k) is convergent & lim (seq ^\k)=lim
  seq;

theorem :: CLOPBAN3:10
  for X be ComplexNormSpace, seq,seq1 be sequence of X holds seq
  is convergent & (ex k be Nat st seq=seq1 ^\k) implies seq1 is
  convergent;

theorem :: CLOPBAN3:11
  for X be ComplexNormSpace, seq,seq1 be sequence of X holds seq
is convergent & (ex k be Nat st seq=seq1 ^\k) implies lim seq1 =lim
  seq;

theorem :: CLOPBAN3:12
  for X be ComplexNormSpace, seq be sequence of X holds seq is
  constant implies seq is convergent;

theorem :: CLOPBAN3:13
  for X be ComplexNormSpace, seq be sequence of X st (for n be
  Nat holds seq.n = 0.X) holds seq is norm_summable;

registration
  let X be ComplexNormSpace;
  cluster norm_summable for sequence of X;
end;

:: Norm Space versions of SERIES_1_7 - SERIES_1_16

theorem :: CLOPBAN3:14
  for X be ComplexNormSpace, s be sequence of X holds s is
  summable implies s is convergent & lim s = 0.X;

theorem :: CLOPBAN3:15
  for X be ComplexNormSpace, s1,s2 be sequence of X holds
  Partial_Sums(s1)+Partial_Sums(s2) = Partial_Sums(s1+s2);

theorem :: CLOPBAN3:16
  for X be ComplexNormSpace, s1,s2 be sequence of X holds
  Partial_Sums(s1)-Partial_Sums(s2) = Partial_Sums(s1-s2);

registration
  let X be ComplexNormSpace;
  let seq be norm_summable sequence of X;
  cluster ||.seq.|| -> summable for Real_Sequence;
end;

registration
  let X be ComplexNormSpace;
  cluster summable -> convergent for sequence of X;
end;

theorem :: CLOPBAN3:17
  for X be ComplexNormSpace, seq1,seq2 be sequence of X st seq1 is
summable & seq2 is summable holds seq1+seq2 is summable & Sum(seq1+seq2) = Sum(
  seq1)+Sum(seq2);

theorem :: CLOPBAN3:18
  for X be ComplexNormSpace, seq1,seq2 be sequence of X st seq1 is
summable & seq2 is summable holds seq1-seq2 is summable & Sum(seq1-seq2)= Sum(
  seq1)-Sum(seq2);

registration
  let X be ComplexNormSpace;
  let seq1,seq2 be summable sequence of X;
  cluster seq1 + seq2 -> summable;
  cluster seq1 - seq2 -> summable;
end;

theorem :: CLOPBAN3:19
  for X be ComplexNormSpace, seq be sequence of X, z be Complex
  holds Partial_Sums(z * seq) = z * Partial_Sums(seq);

theorem :: CLOPBAN3:20
  for X be ComplexNormSpace, seq be summable sequence of X, z be
  Complex holds z *seq is summable & Sum(z *seq)= z * Sum(seq);

registration
  let X be ComplexNormSpace;
  let z be Complex, seq be summable sequence of X;
  cluster z *seq -> summable;
end;

theorem :: CLOPBAN3:21
  for X be ComplexNormSpace, s,s1 be sequence of X st for n be
Nat holds s1.n=s.0 holds Partial_Sums(s^\1) = (Partial_Sums(s)^\1) -
  s1;

theorem :: CLOPBAN3:22
  for X be ComplexNormSpace, s be sequence of X holds s is
  summable implies for n be Nat holds s^\n is summable;

registration
  let X be ComplexNormSpace;
  let seq be summable sequence of X, n be Nat;
  cluster seq^\n -> summable for sequence of X;
end;

theorem :: CLOPBAN3:23
  for X be ComplexNormSpace, seq be sequence of X holds
  Partial_Sums ||.seq.|| is bounded_above iff seq is norm_summable;

registration
  let X be ComplexNormSpace;
  let seq be norm_summable sequence of X;
  cluster Partial_Sums ||.seq.|| -> bounded_above for Real_Sequence;
end;

theorem :: CLOPBAN3:24
  for X be ComplexBanachSpace, seq be sequence of X holds seq is
  summable iff
   for p be Real st 0 <p holds ex n be Nat st for m be
Nat st n <= m holds ||.Partial_Sums(seq).m-Partial_Sums(seq).n.||<p;

theorem :: CLOPBAN3:25
  for X be ComplexNormSpace, s be sequence of X,
    n,m be Nat st n<=m
  holds ||.Partial_Sums(s).m - Partial_Sums(s).n.|| <= |.
  Partial_Sums(||.s.||).m - Partial_Sums(||.s.||).n.|;

theorem :: CLOPBAN3:26
  for X be ComplexBanachSpace, seq be sequence of X holds seq is
  norm_summable implies seq is summable;

theorem :: CLOPBAN3:27
  for X be ComplexNormSpace, rseq1 be Real_Sequence, seq2 be sequence of
X holds rseq1 is summable & (ex m be Nat st for n be Nat
  st m<=n holds ||.seq2.n.|| <= rseq1.n ) implies seq2 is norm_summable;

theorem :: CLOPBAN3:28
  for X be ComplexNormSpace, seq1,seq2 be sequence of X holds (for n be
  Nat holds 0 <= ||.seq1.||.n & ||.seq1.||.n <= ||.seq2.||.n) & seq2
is norm_summable implies seq1 is norm_summable & Sum ||.seq1.|| <= Sum ||.seq2
  .||;

theorem :: CLOPBAN3:29
  for X be ComplexNormSpace, seq be sequence of X holds (for n be
  Nat holds ||.seq.||.n>0) & (ex m be Nat st for n be
Nat st n >=m holds ||.seq.||.(n+1)/||.seq.||.n >= 1) implies not seq
  is norm_summable;

theorem :: CLOPBAN3:30
  for X be ComplexNormSpace, seq be sequence of X, rseq1 be
Real_Sequence holds (for n be Nat holds rseq1.n = n-root (||.seq.||.
  n)) & rseq1 is convergent & lim rseq1 < 1 implies seq is norm_summable;

theorem :: CLOPBAN3:31
  for X be ComplexNormSpace, seq be sequence of X, rseq1 be
Real_Sequence holds (for n be Nat holds rseq1.n = n-root (||.seq.||.
n)) & (ex m be Nat st for n be Nat st m<=n holds rseq1.n
  >= 1) implies ||.seq.|| is not summable;

theorem :: CLOPBAN3:32
  for X be ComplexNormSpace, seq be sequence of X, rseq1 be
Real_Sequence holds (for n be Nat holds rseq1.n = n-root (||.seq.||.
  n)) & rseq1 is convergent & lim rseq1 > 1 implies seq is not norm_summable;

theorem :: CLOPBAN3:33
  for X be ComplexNormSpace, seq be sequence of X, rseq1 be
  Real_Sequence st ||.seq.|| is non-increasing & (for n be Nat holds
  rseq1.n = 2 to_power n *||.seq.||.(2 to_power n)) holds (seq is norm_summable
  iff rseq1 is summable);

theorem :: CLOPBAN3:34
  for X be ComplexNormSpace, seq be sequence of X, p be Real st p>1 & (
for n be Nat st n >=1 holds ||.seq.||.n = 1/ (n to_power p) ) holds
  seq is norm_summable;

theorem :: CLOPBAN3:35
  for X be ComplexNormSpace, seq be sequence of X, p be Real holds p<=1
  & (for n be Nat st n >=1 holds ||.seq.||.n=1/n to_power p) implies
  not seq is norm_summable;

theorem :: CLOPBAN3:36
  for X be ComplexNormSpace, seq be sequence of X, rseq1 be
Real_Sequence holds (for n be Nat holds seq.n<>0.X & rseq1.n=||.seq
  .||.(n+1)/||.seq.||.n) & rseq1 is convergent & lim rseq1 < 1 implies seq is
  norm_summable;

theorem :: CLOPBAN3:37
  for X be ComplexNormSpace, seq be sequence of X holds
   (for n be Nat holds seq.n<>0.X) &
   (ex m be Nat st for n be Nat st
   n >=m holds ||.seq.||.(n+1)/||.seq.||.n >= 1) implies seq is not
  norm_summable;

registration
  let X be ComplexBanachSpace;
  cluster norm_summable -> summable for sequence of X;
end;

begin :: Basic Properties of Sequence of Complex_Banach_Algebra

theorem :: CLOPBAN3:38
  for X be Complex_Banach_Algebra holds for x,y,z being Element of
  X, a,b be Complex holds
a*(x*y) = (a*x)*y & a*(x+y) = a*x + a*y & (a+b)*x = a*x + b*x & (a*
b)*x = a*(b*x) & (a*b)*(x*y)=(a*x)*(b*y) & a*(x*y)=x*(a*y) & 0.X * x = 0.X & x*
0.X =0.X & x*(y-z) = x*y-x*z & (y-z)*x = y*x-z*x & x+y-z = x+(y-z) & x-y+z = x-
(y-z) & x-y-z = x-(y+z) & x+y=(x-z)+(z+y) & x-y=(x-z)+(z-y) & x=(x-y)+y & x=y-(
  y-x) & ( ||.x.|| = 0 iff x = 0.X ) & ||.a * x.|| = |.a.| * ||.x.|| & ||.x + y
.|| <= ||.x.|| + ||.y.|| & ||. x*y .|| <= ||.x.|| * ||.y.|| & ||. 1.X .|| = 1;

registration
  cluster -> well-unital for Complex_Banach_Algebra;
end;

definition
::$CD 3
end;

definition
  let X be Complex_Banach_Algebra;
  let z be Element of X;
  func z GeoSeq -> sequence of X means
:: CLOPBAN3:def 7

  it.0 = 1.X & for n be Nat holds it.(n+1) = it.n * z;
end;

definition
  let X be Complex_Banach_Algebra;
  let z be Element of X, n be Nat;
  func z #N n -> Element of X equals
:: CLOPBAN3:def 8
  z GeoSeq.n;
end;

theorem :: CLOPBAN3:39
  for X be Complex_Banach_Algebra, z be Element of X holds z #N 0 = 1.X;

theorem :: CLOPBAN3:40
  for X be Complex_Banach_Algebra, z be Element of X holds
  ||.z.|| < 1 implies z GeoSeq is summable norm_summable;

theorem :: CLOPBAN3:41
  for X be Complex_Banach_Algebra, x be Point of X st ||.1.X - x .|| < 1
holds (1.X - x) GeoSeq is summable & (1.X - x) GeoSeq is norm_summable;

theorem :: CLOPBAN3:42
  for X be Complex_Banach_Algebra, x be Point of X st ||.1.X - x .|| < 1
  holds x is invertible & x" = Sum ((1.X - x) GeoSeq );