:: Exponential Function 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, CLOPBAN2, SUBSET_1, NAT_1, SEQ_1, RELAT_1, COMSEQ_3,
      ARYTM_3, CARD_1, PREPOWER, FUNCT_1, MESFUNC1, LOPBAN_4, SEQ_2, ORDINAL2,
      ARYTM_1, SUPINF_2, REAL_1, XXREAL_0, NORMSP_1, PRE_TOPC, XXREAL_2,
      SERIES_1, COMPLEX1, SIN_COS, XBOOLE_0, STRUCT_0, NEWTON, REALSET1,
      VALUED_1, XCMPLX_0, LOPBAN_3, CARD_3, VALUED_0, RSSPACE3, ALGSTR_0;
 notations RELAT_1, FUNCT_1, SUBSET_1, FUNCT_2, PRE_TOPC, XCMPLX_0, XXREAL_0,
      XREAL_0, ORDINAL1, NUMBERS, CLOPBAN3, COMPLEX1, REAL_1, NAT_1, STRUCT_0,
      ALGSTR_0, NEWTON, RLVECT_1, SEQ_1, SEQ_2, SEQM_3, SERIES_1, LOPBAN_4,
      NAT_D, SIN_COS, BHSP_4, NORMSP_0, CLVECT_1, CSSPACE3, CLOPBAN2, LOPBAN_3,
      NORMSP_1;
 constructors REAL_1, SQUARE_1, SEQ_2, COMSEQ_3, NAT_D, SIN_COS, BHSP_4,
      LOPBAN_4, CSSPACE3, CLOPBAN3, RELSET_1, COMSEQ_2, NUMBERS, LOPBAN_3;
 registrations ORDINAL1, RELSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0,
      MEMBERED, STRUCT_0, CLOPBAN2, CLOPBAN3, VALUED_0, SEQ_2, NEWTON, NAT_1,
      FUNCT_2;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;


begin :: Basic Properties of Exponential Function on Complex Banach Algebra

reserve X for Complex_Banach_Algebra,
  w,z,z1,z2 for Element of X,
  k,l,m,n,n1, n2 for Nat,
  seq,seq1,seq2,s,s9 for sequence of X,
  rseq for Real_Sequence;

theorem :: CLOPBAN4:1
  seq1 is convergent & seq2 is convergent & lim(seq1-seq2)=0.X
  implies lim seq1 = lim seq2;

theorem :: CLOPBAN4:2
  for z st for n being Nat holds s.n = z holds lim s = z;

theorem :: CLOPBAN4:3
  s is convergent & s9 is convergent implies s * s9 is convergent;

theorem :: CLOPBAN4:4
  s is convergent implies z * s is convergent;

theorem :: CLOPBAN4:5
  s is convergent implies s*z is convergent;

theorem :: CLOPBAN4:6
  s is convergent implies lim (z * s) =z* lim(s);

theorem :: CLOPBAN4:7
  s is convergent implies lim (s*z) = lim(s)*z;

theorem :: CLOPBAN4:8
  s is convergent & s9 is convergent implies lim(s*s9)=(lim s)*(lim s9);

theorem :: CLOPBAN4:9
  Partial_Sums(z * seq) = z * Partial_Sums(seq) & Partial_Sums(seq
  *z ) = Partial_Sums(seq) *z;

theorem :: CLOPBAN4:10
  ||.Partial_Sums(seq).k.|| <= Partial_Sums(||.seq.||).k;

theorem :: CLOPBAN4:11
  (for n st n <= m holds seq1.n = seq2.n) implies Partial_Sums(
  seq1).m =Partial_Sums(seq2).m;

theorem :: CLOPBAN4:12
  (for n holds ||. seq.n .|| <= rseq.n) & rseq is convergent & lim
  (rseq)=0 implies seq is convergent & lim(seq)=0.X;

definition
  let X,z;
  func z ExpSeq -> sequence of X means
:: CLOPBAN4:def 1

  for n holds it.n = 1r/(n!) * (z #N n);
end;

scheme :: CLOPBAN4:sch 1
  ExNormSpaceCASE {CNS()->non empty Complex_Banach_Algebra, F(Nat,
Nat)-> Point of CNS() }: for k holds ex seq be sequence of CNS() st
for n holds (n <= k implies seq.n=F(k,n)) & (n > k implies seq.n=0.CNS());

definition
  let n,X,z,w;

  func Expan(n,z,w) -> sequence of X means
:: CLOPBAN4:def 2

  for k be Nat
holds ( k <= n implies it.k=((Coef(n)).k) * (z #N k) * (w #N (n-' k)) ) & (n <
  k implies it.k=0.X);
end;

definition
  let n,X,z,w;
  func Expan_e(n,z,w) -> sequence of X means
:: CLOPBAN4:def 3

  for k be Nat
holds ( k <= n implies it.k=((Coef_e(n)).k) * (z #N k) * (w #N (n-' k)) ) & ( n
  < k implies it.k=0.X );
end;

definition
  let n,X,z,w;
  func Alfa(n,z,w) -> sequence of X means
:: CLOPBAN4:def 4

  for k be Nat holds
( k <= n implies it.k= (z ExpSeq).k * Partial_Sums(w ExpSeq).(n-'k) ) & ( n < k
  implies it.k=0.X);
end;

definition
  let X,z,w,n;
  func Conj(n,z,w) -> sequence of X means
:: CLOPBAN4:def 5

  for k be Nat holds
( k <= n implies it.k= (z ExpSeq).k * (Partial_Sums(w ExpSeq).n -Partial_Sums(w
  ExpSeq).(n-'k))) & ( n < k implies it.k=0.X );
end;

theorem :: CLOPBAN4:13
  z ExpSeq.(n+1) = (1r/(n+1) * z) * (z ExpSeq.n) & z ExpSeq.0=1.X
  & ||.(z ExpSeq).n.|| <= (||.z.|| rExpSeq ).n;

theorem :: CLOPBAN4:14
  0 < k implies (Shift seq).k=seq.(k -' 1);

theorem :: CLOPBAN4:15
  Partial_Sums(seq).k=Partial_Sums(Shift seq).k+seq.k;

theorem :: CLOPBAN4:16
  for z,w st z,w are_commutative holds (z+w) #N n = Partial_Sums(
  Expan(n,z,w)).n;

theorem :: CLOPBAN4:17
  Expan_e(n,z,w) = (1r/(n!)) * Expan(n,z,w);

theorem :: CLOPBAN4:18
  for z,w st z,w are_commutative holds 1r/(n!) *((z+w) #N n) =
  Partial_Sums(Expan_e(n,z,w)).n;

theorem :: CLOPBAN4:19
  0.X ExpSeq is norm_summable & Sum(0.X ExpSeq)=1.X;

registration
  let X;
  let z be Element of X;
  cluster z ExpSeq -> norm_summable;
end;

theorem :: CLOPBAN4:20
  (z ExpSeq).0 = 1.X & Expan(0,z,w).0 = 1.X;

theorem :: CLOPBAN4:21
  l <= k implies (Alfa(k+1,z,w)).l = (Alfa(k,z,w)).l + Expan_e(k+1 ,z,w).l;

theorem :: CLOPBAN4:22
  Partial_Sums((Alfa(k+1,z,w))).k = (Partial_Sums( Alfa(k,z,w) )).
  k + (Partial_Sums( Expan_e(k+1,z,w) )).k;

theorem :: CLOPBAN4:23
  (z ExpSeq).k=(Expan_e(k,z,w)).k;

theorem :: CLOPBAN4:24
  for z,w st z,w are_commutative holds Partial_Sums((z+w) ExpSeq).
  n = Partial_Sums(Alfa(n,z,w)).n;

theorem :: CLOPBAN4:25
  for z,w st z,w are_commutative holds Partial_Sums(z ExpSeq).k *
Partial_Sums(w ExpSeq).k - Partial_Sums((z+w) ExpSeq).k = Partial_Sums(Conj(k,z
  ,w)).k;

theorem :: CLOPBAN4:26
  0 <= (||. z .|| rExpSeq).n;

theorem :: CLOPBAN4:27
  ||. Partial_Sums((z ExpSeq)).k .|| <= Partial_Sums(||.z.||
  rExpSeq).k & Partial_Sums((||.z.|| rExpSeq)).k <= Sum(||.z.|| rExpSeq) & ||.
  Partial_Sums(( z ExpSeq)).k .|| <= Sum(||.z.|| rExpSeq);

theorem :: CLOPBAN4:28
  1 <= Sum(||.z.|| rExpSeq);

theorem :: CLOPBAN4:29
  |.(Partial_Sums(||.z.|| rExpSeq)).n.| = Partial_Sums(||.z.||
rExpSeq).n & ( n <= m implies |.(Partial_Sums(||.z.|| rExpSeq).m-Partial_Sums
  (||.z.|| rExpSeq).n).|
    = Partial_Sums(||.z.|| rExpSeq).m-Partial_Sums(||.z.||
  rExpSeq).n );

theorem :: CLOPBAN4:30
  |.Partial_Sums(||.Conj(k,z,w).||).n.|=Partial_Sums(||.Conj(k,z, w).||).n;

theorem :: CLOPBAN4:31
  for p being Real st p>0 ex n st for k st n <= k holds
  |.Partial_Sums(||.Conj(k,z,w).||).k.| < p;

theorem :: CLOPBAN4:32
  for seq st for k holds seq.k=Partial_Sums((Conj(k,z,w))).k holds
  seq is convergent & lim(seq)=0.X;

definition
  let X;
  func exp_ X -> Function of the carrier of X, the carrier of X means
:: CLOPBAN4:def 6

  for z being Element of X holds it.z=Sum(z ExpSeq);
end;

definition
  let X,z;
  func exp z -> Element of X equals
:: CLOPBAN4:def 7
  (exp_ X).z;
end;

theorem :: CLOPBAN4:33
  for z holds exp(z)=Sum(z ExpSeq);

theorem :: CLOPBAN4:34
  for z1,z2 st z1,z2 are_commutative holds exp(z1+z2)=exp(z1) *exp
  (z2) & exp(z2+z1)=exp(z2) *exp(z1) & exp(z1+z2)=exp(z2+z1) & exp(z1),exp(z2)
  are_commutative;

theorem :: CLOPBAN4:35
  for z1,z2 st z1,z2 are_commutative holds z1 * exp(z2)=exp(z2) * z1;

theorem :: CLOPBAN4:36
  exp(0.X) = 1.X;

theorem :: CLOPBAN4:37
  exp(z)*exp(-z)= 1.X & exp(-z)*exp(z)= 1.X;

theorem :: CLOPBAN4:38
  exp(z) is invertible & (exp(z))" = exp(-z) & exp(-z) is invertible & (
  exp(-z))" = exp(z);

theorem :: CLOPBAN4:39
  for z for s,t be Complex holds s*z,t*z are_commutative;

theorem :: CLOPBAN4:40
  for z for s,t be Complex holds exp(s*z)*exp(t*z) = exp((s+t)*z) & exp(
t*z)*exp(s*z) = exp((t+s)*z) & exp((s+t)*z) = exp((t+s)*z) & exp(s*z),exp(t*z)
  are_commutative;