:: Eigenvalues of a Linear Transformation
::  by Karol P\c{a}k
::
:: Received July 11, 2008
:: Copyright (c) 2008-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, NAT_1, VECTSP_1, SUBSET_1, MATRIX_1, FINSEQ_2, ZFMISC_1,
      RELAT_1, TARSKI, CARD_1, ARYTM_3, FUNCT_1, FREEALG, FINSET_1, FINSEQ_1,
      MESFUNC1, GROUP_1, SUPINF_2, LAPLACE, XBOOLE_0, ARYTM_1, XXREAL_0,
      POLYNOM1, POLYNOM2, MATRIX_3, CARD_3, AFINSQ_1, ORDINAL4, POLYNOM3,
      STRUCT_0, PARTFUN1, RANKNULL, RLSUB_1, RLVECT_5, PRVECT_1, RLVECT_3,
      ALGSTR_0, VECTSP10, MATRLIN, MATRLIN2, POLYNOM5, NEWTON, MONOID_0,
      BINOP_1, RLVECT_1, LATTICES, RLSUB_2, FINSEQ_4, MCART_1, RLVECT_2,
      VALUED_1, FUNCT_2, VECTSP11, MSSUBFAM, UNIALG_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, CARD_1,
      XCMPLX_0, ALGSTR_0, XXREAL_0, FINSET_1, RELAT_1, FUNCT_1, PARTFUN1,
      FUNCT_2, NAT_1, FINSEQ_1, BINOP_1, STRUCT_0, RLVECT_1, GROUP_1, VECTSP_1,
      FINSEQ_2, MATRIX_0, MATRIX_1, NAT_D, GROUP_4, MATRIX_3, DOMAIN_1,
      MEASURE6, PRVECT_1, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7, VECTSP_9,
      FINSEQOP, MATRIX13, MATRLIN, LAPLACE, MOD_2, RANKNULL, POLYNOM3,
      MONOID_0, ALGSEQ_1, POLYNOM4, POLYNOM5, MATRLIN2;
 constructors FINSOP_1, GROUP_4, VECTSP_7, VECTSP_9, MATRIX13, REALSET1,
      LAPLACE, VECTSP_5, RANKNULL, MONOID_0, POLYNOM4, POLYNOM5, MATRLIN2,
      BINOP_2, RELSET_1, MATRIX_1, ALGSEQ_1;
 registrations XBOOLE_0, FUNCT_1, FINSET_1, STRUCT_0, VECTSP_1, FUNCT_2,
      ORDINAL1, XXREAL_0, NAT_1, FINSEQ_1, FINSEQ_2, SEQM_3, MATRIX13, XREAL_0,
      VECTSP_9, RANKNULL, POLYNOM3, POLYNOM5, MONOID_0, CARD_1, RELSET_1,
      MOD_2, GRCAT_1, PRVECT_1, MATRLIN2;
 requirements ARITHM, NUMERALS, REAL, BOOLE, SUBSET;


begin :: Preliminaries

reserve i,j,m,n,k for Nat,
  x,y for set,
  K for Field,
  a for Element of K;

theorem :: VECTSP11:1
  for A,B be Matrix of K for nt be Element of n-tuples_on NAT, mt
be Element of m-tuples_on NAT st [:rng nt,rng mt:] c= Indices A holds Segm(A+B,
  nt,mt) = Segm(A,nt,mt) + Segm(B,nt,mt);

theorem :: VECTSP11:2
  for P be without_zero finite Subset of NAT st P c= Seg n holds
  Segm(1.(K,n),P,P) = 1.(K,card P);

theorem :: VECTSP11:3
  for A,B be Matrix of K for P, Q be without_zero finite Subset of
  NAT st [:P,Q:] c= Indices A holds Segm(A+B,P,Q) = Segm(A,P,Q) + Segm(B,P,Q);

theorem :: VECTSP11:4
  for A,B be Matrix of n,K st i in Seg n & j in Seg n holds Delete(
  A+B,i,j)=Delete(A,i,j) + Delete(B,i,j);

theorem :: VECTSP11:5
  for A be Matrix of n,K st i in Seg n & j in Seg n holds Delete(a*
  A,i,j)=a*Delete(A,i,j);

theorem :: VECTSP11:6
  i in Seg n implies Delete(1.(K,n),i,i)=1.(K,n-'1);

theorem :: VECTSP11:7
  for A,B be Matrix of n,K ex P be Polynomial of K st len P <= n+1
  & for x be Element of K holds eval(P,x) = Det(A+x*B);

:: The Characteristic Polynomials of Square Matrixs

theorem :: VECTSP11:8
  for A be Matrix of n,K ex P be Polynomial of K st len P = n+1 &
  for x be Element of K holds eval(P,x) = Det(A+x*1.(K,n));

registration
  let K;
  cluster non trivial finite-dimensional for VectSp of K;
end;

begin :: Maps with Eigenvalues

definition
  let R be non empty doubleLoopStr;
  let V be non empty ModuleStr over R;
  let IT be Function of V,V;
  attr IT is with_eigenvalues means
:: VECTSP11:def 1

  ex v be Vector of V, a be Scalar of R st v <> 0.V & IT.v = a*v;
end;

reserve V for non trivial VectSp of K,
  V1,V2 for VectSp of K,
  f for linear-transformation of V1,V1,
  v,w for Vector of V,
  v1 for Vector of V1,
  L for Scalar of K;

registration
  let K,V;
  cluster with_eigenvalues for linear-transformation of V,V;
end;

definition
  let R be non empty doubleLoopStr;
  let V be non empty ModuleStr over R;
  let f be Function of V,V such that
 f is with_eigenvalues;
  mode eigenvalue of f -> Element of R means
:: VECTSP11:def 2

    ex v be Vector of V st v <> 0.V & f.v = it * v;
end;

definition
  let R be non empty doubleLoopStr;
  let V be non empty ModuleStr over R;
  let f be Function of V,V;
  let L be Scalar of R such that
 f is with_eigenvalues & L is eigenvalue of f;
  mode eigenvector of f,L -> Vector of V means
:: VECTSP11:def 3

    f.it = L * it;
end;

theorem :: VECTSP11:9
  for a st a <> 0.K for f be with_eigenvalues Function of V,V for L be
eigenvalue of f holds a*f is with_eigenvalues & a*L is eigenvalue of a*f & ( w
  is eigenvector of f,L iff w is eigenvector of a*f,a*L );

theorem :: VECTSP11:10
  for f1,f2 be with_eigenvalues Function of V,V for L1,L2 be Scalar of K
  st L1 is eigenvalue of f1 & L2 is eigenvalue of f2 & ex v st v is eigenvector
of f1,L1 & v is eigenvector of f2,L2 & v<>0.V holds f1+f2 is with_eigenvalues &
  L1+L2 is eigenvalue of f1+f2 & for w st w is eigenvector of f1,L1 & w is
  eigenvector of f2,L2 holds w is eigenvector of f1+f2,L1+L2;

theorem :: VECTSP11:11
  id V is with_eigenvalues & 1_K is eigenvalue of id V & for v
  holds v is eigenvector of id V,1_K;

theorem :: VECTSP11:12
  for L be eigenvalue of id V holds L = 1_K;

theorem :: VECTSP11:13
  ker f is non trivial implies f is with_eigenvalues & 0.K is eigenvalue of f;

theorem :: VECTSP11:14
  f is with_eigenvalues & L is eigenvalue of f iff ker (f+(-L)*id
  V1) is non trivial;

theorem :: VECTSP11:15
  for V1 be finite-dimensional VectSp of K, b1,b19 be OrdBasis of
  V1 for f be linear-transformation of V1,V1 holds f is with_eigenvalues & L is
  eigenvalue of f iff Det AutEqMt(f+(-L)*id V1,b1,b19) =0.K;

theorem :: VECTSP11:16
  for K be algebraic-closed Field, V1 be non trivial finite-dimensional
  VectSp of K, f be linear-transformation of V1,V1 holds f is with_eigenvalues;

theorem :: VECTSP11:17
  for f,L st f is with_eigenvalues & L is eigenvalue of f holds v1
  is eigenvector of f,L iff v1 in ker (f+(-L)*id V1);

definition
  let S be 1-sorted;
  let F be Function of S,S;
  let n be Nat;
  func F |^ n -> Function of S,S means
:: VECTSP11:def 4

  for F9 be Element of GFuncs the
  carrier of S st F9=F holds it = Product(n|-> F9);
end;

reserve S for 1-sorted,
  F for Function of S,S;

theorem :: VECTSP11:18
  F |^ 0 = id S;

theorem :: VECTSP11:19
  F |^ 1 = F;

theorem :: VECTSP11:20
  F |^(i+j) = (F |^ j) * (F |^ i);

theorem :: VECTSP11:21
  for s1,s2 be Element of S,n,m st (F|^m).s1 = s2 & (F|^n).s2 = s2 holds
  (F|^(m+i*n)).s1 = s2;

theorem :: VECTSP11:22
  for K be add-associative right_zeroed right_complementable Abelian
  associative well-unital distributive non empty doubleLoopStr, V1 be Abelian
  add-associative right_zeroed right_complementable vector-distributive
  scalar-distributive scalar-associative scalar-unital
   non empty
  ModuleStr over K for W be Subspace of V1, f be Function of V1,V1, fW be
  Function of W,W st fW=f|W holds (f|^n)|W=fW|^n;

registration
  let K,V1;
  let f be linear-transformation of V1,V1;
  let n be Nat;
  cluster f |^ n ->  homogeneous additive;
end;

theorem :: VECTSP11:23
  (f|^i).v1 = 0.V1 implies (f|^(i+j)).v1=0.V1;

begin :: Generalized Eigenspace of a Linear Transformation

definition
  let K,V1,f;
  func UnionKers f -> strict Subspace of V1 means
:: VECTSP11:def 5

  the carrier of it = { v where v is Vector of V1:ex n st (f|^n).v = 0.V1};
end;

theorem :: VECTSP11:24
  v1 in UnionKers f iff ex n st (f|^n).v1 = 0.V1;

theorem :: VECTSP11:25
  ker (f|^i) is Subspace of UnionKers f;

theorem :: VECTSP11:26
  ker (f|^i) is Subspace of ker (f|^(i+j));

theorem :: VECTSP11:27
  for V be finite-dimensional VectSp of K,f be linear-transformation of
  V,V ex n st UnionKers f = ker (f|^n);

theorem :: VECTSP11:28
  f|ker (f|^n) is linear-transformation of ker (f|^n),ker (f|^n);

theorem :: VECTSP11:29
  f|ker ((f+L*id V1)|^n) is linear-transformation of ker ((f+L*id V1)|^n
  ), ker ((f+L*id V1)|^n);

theorem :: VECTSP11:30
  f|(UnionKers f) is linear-transformation of UnionKers f, UnionKers f;

theorem :: VECTSP11:31
  f|(UnionKers (f+L*id V1)) is linear-transformation of UnionKers
  (f+L*id V1), UnionKers (f+L*id V1);

theorem :: VECTSP11:32
  f|im (f|^n) is linear-transformation of im (f|^n),im (f|^n);

theorem :: VECTSP11:33
  f|im ((f+L*id V1)|^n) is linear-transformation of im ((f+L*id V1)|^n),
  im ((f+L*id V1)|^n);

theorem :: VECTSP11:34
  UnionKers f = ker (f|^n) implies ker (f|^n) /\ im (f|^n) = (0). V1;

theorem :: VECTSP11:35
  for V be finite-dimensional VectSp of K, f be linear-transformation of
V,V,n st UnionKers f = ker (f|^n) holds V is_the_direct_sum_of ker (f|^n),im (f
  |^n);

theorem :: VECTSP11:36
  for I be Linear_Compl of UnionKers f holds f|I is one-to-one;

theorem :: VECTSP11:37
  for I be Linear_Compl of UnionKers (f+(-L)*id V1), fI be
  linear-transformation of I,I st fI = f|I for v be Vector of I st fI.v = L * v
  holds v = 0.V1;

theorem :: VECTSP11:38
  n >= 1 implies ex h be linear-transformation of V1,V1 st (f + L*
id V1) |^ n = f * h + ((L*id V1) |^ n) & for i holds (f |^ i) * h = h * (f |^ i
  );

theorem :: VECTSP11:39
  for L1,L2 be Scalar of K st f is with_eigenvalues & L1 <> L2 & L2 is
  eigenvalue of f for I be Linear_Compl of UnionKers (f+(-L1)*id V1), fI be
linear-transformation of I,I st fI = f|I holds fI is with_eigenvalues & not L1
  is eigenvalue of fI & L2 is eigenvalue of fI & UnionKers (f+(-L2)*id V1) is
  Subspace of I;

:: Main Lemmas for Expansion of Matrices of Nilpotent Linear Transformations

theorem :: VECTSP11:40
  for U be finite Subset of V1 st U is linearly-independent for u be
Vector of V1 st u in U for L be Linear_Combination of U\{u} holds card U=card (
  U\{u}\/{u+Sum(L)}) & U\{u}\/{u+Sum(L)} is linearly-independent;

theorem :: VECTSP11:41
  for A be Subset of V1 for L be Linear_Combination of V2, f be
linear-transformation of V1,V2 st Carrier L c= f.:A ex M be Linear_Combination
  of A st f.(Sum M)=Sum L;

theorem :: VECTSP11:42
  for f be linear-transformation of V1,V2 for A be Subset of V1,B be
Subset of V2 st f.:A = B holds f.:(the carrier of Lin A) = the carrier of Lin B
;

theorem :: VECTSP11:43
  for L be Linear_Combination of V1, F be FinSequence of V1, f be
linear-transformation of V1,V2 st f|(Carrier L /\ rng F) is one-to-one & rng F
c= Carrier L ex Lf be Linear_Combination of V2 st Carrier Lf = f.:(Carrier L /\
rng F) & f*(L(#)F) = Lf(#)(f*F) & for v1 st v1 in Carrier L /\ rng F holds L.v1
  =Lf.(f.v1);

theorem :: VECTSP11:44
  for A,B be Subset of V1 for L be Linear_Combination of V1 st Carrier L
c= A\/B & Sum L = 0.V1 for f be additive homogeneous Function of V1,V2
st f|B is one-to-one &
f.:B is linearly-independent Subset of V2 & f.:A c= {0.V2} holds Carrier L c= A
;