:: The Exponential Function on {B}anach Algebra
::  by Yasunari Shidama
::
:: Received February 13, 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, LOPBAN_2, SUBSET_1, NAT_1, SEQ_1, XBOOLE_0, ALGSTR_0,
      RELAT_1, COMSEQ_3, ARYTM_3, CARD_1, PREPOWER, FUNCT_1, MESFUNC1, SEQ_2,
      ORDINAL2, ARYTM_1, SUPINF_2, REAL_1, XXREAL_0, NORMSP_1, PRE_TOPC,
      XXREAL_2, SERIES_1, COMPLEX1, SIN_COS, REALSET1, STRUCT_0, VALUED_1,
      NEWTON, LOPBAN_3, CARD_3, VALUED_0, RSSPACE3, LOPBAN_4;
 notations SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, XXREAL_0, XREAL_0, VALUED_0,
      PRE_TOPC, ALGSTR_0, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1, NORMSP_0,
      NORMSP_1, RSSPACE3, SEQ_1, SEQ_2, NEWTON, REAL_1, NAT_1, STRUCT_0,
      SERIES_1, NAT_D, SIN_COS, RLVECT_1, BHSP_4, LOPBAN_2, LOPBAN_3;
 constructors REAL_1, SQUARE_1, SEQ_2, COMSEQ_3, NAT_D, SIN_COS, BHSP_4,
      RSSPACE3, LOPBAN_3, RELSET_1, COMSEQ_2;
 registrations ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, MEMBERED, SIN_COS,
      STRUCT_0, GROUP_1, LOPBAN_2, LOPBAN_3, VALUED_0, SEQ_2, NUMBERS, FUNCT_2,
      NEWTON;
 requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;


begin :: Basic Properties of Exponential Function on Banach Algebra

reserve X for 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;

definition
  let X be non empty multMagma;
  let x,y be Element of X;
  pred x,y are_commutative means
:: LOPBAN_4:def 1

  x * y = y * x;
  reflexivity;
  symmetry;
end;

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

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

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

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

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

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

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

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

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

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

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

theorem :: LOPBAN_4: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;
  let z be Element of X;
  func z rExpSeq -> sequence of X means
:: LOPBAN_4:def 2

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

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

theorem :: LOPBAN_4:13
  (for k st 0 < k holds ((k-'1)! ) * k = k!) & for m,k st k <= m
  holds ((m-'k)! ) * (m+1-k) = (m+1-'k)!;

definition
  let n be Nat;
  func Coef(n) -> Real_Sequence means
:: LOPBAN_4:def 3

  for k be Nat holds (k
  <= n implies it.k = n! /( (k! ) * (( n -' k)!) ) ) &(k > n implies it.k=0);
end;

definition
  let n be Nat;
  func Coef_e(n) -> Real_Sequence means
:: LOPBAN_4:def 4

  for k be Nat holds (
  k <= n implies it.k = 1/((k! ) * ((n -' k)! ))) & (k > n implies it.k=0);
end;

definition
  let X be non empty ZeroStr, seq be sequence of X;
  func Shift seq -> sequence of X means
:: LOPBAN_4:def 5

  it.0 = 0.X & for k be Nat holds it.(k+1) = seq.k;
end;

definition
  let n;
  let X;
  let z,w be Element of X;
  func Expan(n,z,w) -> sequence of X means
:: LOPBAN_4:def 6

  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;
  let X;
  let z,w be Element of X;
  func Expan_e(n,z,w) -> sequence of X means
:: LOPBAN_4:def 7

  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;
  let X;
  let z,w be Element of X;
  func Alfa(n,z,w) -> sequence of X means
:: LOPBAN_4:def 8

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

definition
  let X;
  let z, w be Element of X;
  let n be Nat;
  func Conj(n,z,w) -> sequence of X means
:: LOPBAN_4:def 9

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

theorem :: LOPBAN_4:14
  z rExpSeq.(n+1) = (1/(n+1) * z) * (z rExpSeq.n) & z rExpSeq.0=1.
  X & ||.(z rExpSeq).n.|| <= (||.z.|| rExpSeq ).n;

theorem :: LOPBAN_4:15
  for X being non empty ZeroStr, seq being sequence of X holds 0 <
  k implies (Shift(seq)).k=seq.(k -' 1);

theorem :: LOPBAN_4:16
  Partial_Sums(seq).k=Partial_Sums(Shift(seq)).k+seq.k;

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

theorem :: LOPBAN_4:18
  Expan_e(n,z,w)=(1/(n!)) * Expan(n,z,w);

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

theorem :: LOPBAN_4:20
  0.X rExpSeq is norm_summable & Sum(0.X rExpSeq)=1.X;

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

theorem :: LOPBAN_4:21
  (z rExpSeq).0 = 1.X & Expan(0,z,w).0 = 1.X;

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

theorem :: LOPBAN_4:23
  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 :: LOPBAN_4:24
  (z rExpSeq).k=(Expan_e(k,z,w)).k;

theorem :: LOPBAN_4:25
  for z,w st z,w are_commutative holds Partial_Sums((z+w) rExpSeq)
  .n = Partial_Sums(Alfa(n,z,w)).n;

theorem :: LOPBAN_4:26
  for z,w st z,w are_commutative holds Partial_Sums(z rExpSeq).k *
Partial_Sums(w rExpSeq).k -Partial_Sums((z+w) rExpSeq).k = Partial_Sums(Conj(k,
  z,w)).k;

theorem :: LOPBAN_4:27
 for n being Nat holds 0 <= (||. z .|| rExpSeq).n;

theorem :: LOPBAN_4:28
 for k being Nat holds
  ||. Partial_Sums((z rExpSeq)).k .|| <= Partial_Sums(||.z.||
  rExpSeq).k & Partial_Sums((||.z.|| rExpSeq)).k <= Sum(||.z.|| rExpSeq) & ||.
  Partial_Sums(( z rExpSeq)).k .|| <= Sum(||.z.|| rExpSeq);

theorem :: LOPBAN_4:29
  1 <= Sum(||.z.|| rExpSeq);

theorem :: LOPBAN_4:30
  |.(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 :: LOPBAN_4:31
  |.Partial_Sums(||.Conj(k,z,w).||).n.|=Partial_Sums(||.Conj(k,z, w).||).n;

theorem :: LOPBAN_4:32
  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 :: LOPBAN_4:33
  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 be Banach_Algebra;
  func exp_ X -> Function of the carrier of X, the carrier of X means
:: LOPBAN_4:def 10

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

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

theorem :: LOPBAN_4:34
  for z holds exp(z)=Sum(z rExpSeq);

theorem :: LOPBAN_4:35
  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 :: LOPBAN_4:36
  for z1,z2 st z1,z2 are_commutative holds z1* exp(z2)=exp(z2)*z1;

theorem :: LOPBAN_4:37
  exp(0.X) = 1.X;

theorem :: LOPBAN_4:38
  exp(z)*exp(-z)= 1.X & exp(-z)*exp(z)= 1.X;

theorem :: LOPBAN_4:39
  exp(z) is invertible & (exp(z))" = exp(-z) & exp(-z) is invertible & (
  exp(-z))" = exp(z);

theorem :: LOPBAN_4:40
  for z for s,t be Real holds s*z,t*z are_commutative;

theorem :: LOPBAN_4:41
  for z for s,t be Real 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;