Verification Methods For Solutions Of Systems Of Equations

The traditional mathematical proofs are constructed using pencil and paper,but with the development of computer technology,the mathematical proofs of some problems have been accomplished by computer.Verification method is a method of using computer to prove that there exists a(unique)solution of a problem within computed bounds.In addi-tion,verification methods can solve the problem that numerical methods can not.The verification problem for algebraic systems of equations,which is to establish an effective verification method to give the inclusions of the solutions of systems of equa-tions,is also called the existence tests of the solutions of systems of equations,and is one of the most basic problems in the field of trusted verification research.In this thesis,we mainly study the verification methods for solutions of algebraic systems of equations and their INTLAB implementation.The verification problems for algebraic systems of equations arise from an amount of fields throughout computational science and engineering,for example,many problems in the high risk areas,such as rocket design,nuclear magnetic resonance(NMR)machine and digital machine theory,are finally translated into the verification problem for nonlinear systems of equations,and other problems,such as computational fluid dynamics(Stokes-type problems),constrained and weighted least squares estimation,constrained optimiza-tion,electromagnetism,electrical circuits and networks,mesh generation for computer graphics,etc.,eventually need to be translated into the solving and verification problem for linear systems of equations.Therefore,it is of important theoretical significance and high practical value to research,develop and perfect the verification methods for solutions of algebraic systems of equations and their computer implementation.Up to now,the method provided by Rump in 1983 is still the most popular verification method for the solutions of the general square nonlinear systems of equationsf(x)=0,(16)where f:Rn?Rn,f=(fi,f2,…,fn)T,fi,f2,…,fn are nonlinear functions of n variables.The method(i.e.,Theorem 3.1.2 and Algorithm 3.1.1)was established by using Brouwer's fixed-point theorem and an improved Krawczyk interval operator S(x,x)=-Rf(x)+(In-RJf(x+x))x,(17)where x?Rn,x?Rn,IRn and 0 ?x,Jf(x+x)=?{M ? IRn×n|x?x+x,Jf(x)?M},R ? Rn×n is an arbitrary nonsingular matrix.In Rump's verification method,the matrix R is taken to be Jf(x)-1,which means that there is S(x,x)=-Jf(x)-1f(x)+(In-Jf(x)-1 Jf(x+x))x=:SR(x,x),(18)where Jf(x)-1 is the inverse of the Jacobian matrix Jf(x)of the mapping f at x.From the point of view of practical computation,the S R(x,x)form(18)of the interval operator S(x,x)(17)needs to spend extra computational load and times to calculate the matrix Jf(x)and to carry out interval operations.If the matrix R presented in the interval operator S(x,x)(17)is taken to be(mid Jf(x+x))-1,i.e.,R=(mid Jf(x+x))-1,all the problems will be solved.In Chapter 3,we first give another form of the interval operator S(x,x)(17),i.e.,SH(x,x):=-(mid Jf(x+x))-1f(x)+1/4|(mid Jf(x+x))-1|wid Jf(x+x)wid x[-1,1]+1/2|(mid Jf(x+x))-q|wid Jf(x+x)|mid x|[-1,1](19)with R=(mid Jf(x+x))-1 and the midpoint-radius form of the interval quantities x ?Ipn,Jf(x?x)? IRnxn x=mid x+rad x[-1,1]=mid x+1/2-wid x[-1,1]and Jf(x+x)=mid Jf(x+x)+1/2+q/2wid Jf(x+x)[-1,1].Comparing the form SR(x,x)(18)with the form SH(x,x)(19)of the interval opera-tor S(x,x)(17),we can see that,in SH(x,x)(19)form,the matrix Jf(x)doesn't need to be calculated and the matrix mid Jf(x+x)in place of it can be obtained directly from the interval matrix Jf(x+x)which both forms SR(x,x)(18)and SH(x,x)(19)want to use,namely we do not have to spend extra computational load and times to calculate the matrix mid Jf(x+x);we can also see that,in SH(x,x)(19)form,interval multiplication is not involved because of(mid Jf(x+x))-1,wid Jf(x+x)? Rn×n and mid x,wid x?Rn,i.e.,they are point matrices and point vectors,whereas the operations between interval quanti-ties are unavoidable in SR(x,x)(18)form because the quantities In-Jf(x)-1Jf(x+x)and x are interval matrix and interval vector,respectively.Therefore,the verification algo-rithm with SH(x,x)(19)form instead of SR(x,x)(18)form will spend less computational load and times.In addition to the advantages mentioned above,the inclusion SH(x,x)(?)SR(x,x)can be satisfied under some assumptions,where x ?Rn denotes a nonsingular solution of nonlinear systems of equations(16),i.e.,the Jacobian matrix Jf(x)is nonsingular.Then,on the basis of Algorithm 3.1.1,we propose an improved verification algorithm(i.e.,Algorithm 3.3.1)with the form SH(x,x)(19)of the interval operator S(x,x)(17),and Theorem 3.1.2.Compared with the original algorithm 3.1.1,theoretical analyses and numerical results show that the improved verification algorithm 3.3.1 not only saves computing times,but also computes a narrower(or at least the same)inclusion of solution of nonlinear systems of equations(16)for certain classes of problems.Since the assumptions of the existence theorems(such as Theorems 3.1.1 and 3.1.2)based on Brouwer's fixed-point theorem are characterized by the information of all the points in an interval,it is not easy to satisfy the assumptions of this class of theorems.Therefore,the verification methods(i.e,verification methods of Rump type)established by the theorems can only solve the problem successfully with high precision initial values,which is very disadvantageous to the wide application of verification methods of Rump type.However,since the assumptions of Kantorovich Existence Theorem are character-ized by the information of a point,it is easier to satisfy the assumptions of the theorem.Therefore,the verification method based on Kantorovich Existence Theorem can solve the problem successfully for the initial values with low precision,which indicates that verification method of Kantorovich type will have a wide application prospect.In the history of the existence test of solutions,some scholars have done deep re-searches on the application of Kantorovich Existence Theorem to verify the existence of solutions of nonlinear systems of equations(16),but unfortunately,the research work is in the theoretical stage,no specific implementation algorithm is given.In Chapter 4,we research the implementation of verification method for solutions of nonlinear systems of equations(16),which was established based on Kantorovich Existence Theorem.Kantorovich Existence Theorem was proposed by the famous Soviet mathematician Kantorovich in the 1950s when he was studying the convergence and error estimate of Newton's methods for nonlinear systems of equations(16).Theorem 1(Kantorovich Existence Theorem)Let nonlinear mapping f(x):D(?)Rn?Rn and x? Rn be given such that1.the inverse matrix of f'(x)exists,and ?f'(x)-1 ???,?f'(x)-1 f(x)???;2.for all x? U(x,2?) D,f '(x)exists and satisfies Lipschitz condition?f(x)-f'(y)?? K?x-y?,x,y?U(x,2?).(20)If?:=????0.5,then there is a unique x ? U(x,?)with f(x)=0,where U(x,2?)denotes the 2? neigh-bourhood of x,and ?=.From theorem 1,it is not difficult to find that the difficulty of using Kantorovich Existence Theorem to verify the existence of solutions of nonlinear systems of equations(16)is to compute the constant coefficient k in Lipschitz condition(20).In order to solve this problem,a useful expression of Lipschitz constant k is given based on multivariate analysis theory,matrix theory and with tensor representation,i.e.,(21)where denote the second partial derivative of fi at x ? U(x,2?),i,j,k=1,2,…,n.According to interval analysis theory,for all x ? U(x,2?)we havewhere,(x)is inclusion isotonic interval extension of over the interval vector x=[x-2?,x+2?]? IRn,0 ?yi?IR,i,j,k=1,2,…,n,and the interval yi can be obtained directly from the INTLAB/Matlab commands Yi=fi(hessianinit(x))and yi=norm(Yi.hx,Inf),so,in the practical computation,the magnitude of the quantityis calculated by the interval yi,i.e.,Ki=yi,where yi is the right endpoint of yi Thus k=n max{k1,k2,…,kn}.On the basis of theoretical research,we use INTLAB/Matlab software to give a specific implementation algorithm(i.e.,Algorithms 4.3.1 and 4.3.2)for the verification method which was established based on Kantorovich Existence Theorem.Compared with the popular verification algorithms of Rump type(such as Algo?rithms 3.1.1 and 3.3.1),the theoretical analysis and numerical experiments show that Kantorovich's verification algorithm(i.e.,Algorithm 4.3.1 and its strategy for saving com-puting time,i.e.,Algorithm 4.3.2)has two advantages:One is that the algorithm can solve a problem with low precision initial values;the other is that the algorithm has the property of inheritance,i.e.,if the verification fails because of the low precision initial values,it needs to be verified again by improving the precision of initial values,in the new verification step the algorithm can use some results of the previous verification step to reduce computational load and computing times.In Chapter 5,we discuss the verification problem for saddle-point linear systems of equations(?)(22)where A ? Rn×n is symmetric positive definite(SPD),B has full rank,c?Rn and d ?Rm are given,x ?Rn and y?Rm are to be solved,n?m.The verification problem for saddle-point linear systems of equations(22)widely applied in the fields of computational science and engineering,such as computational fluid dynamics(Stokes-type problems),constrained and weighted least squares estima-tion,constrained optimization,electromagnetism,electrical circuits and networks,mesh generation for computer graphics,and so forth.Because the traditional verification methods for the solution of a linear system of equations use an approximation of the inverse of the coefficient matrix,but the condition number of coefficient matrix H?R(m+n)×(m+n)of saddle-point linear systems of equations(22)increases with the scale of the problem,and the inverse matrix of H is not sparse in general,these methods are not efficient for the saddle-point linear systems of equations(22)when the dimension l:=m+n is large.In order to avoid using the approximation of the inverse of the coefficient matrix H,in 2009,Kimura and Chen first solved the practical computation problem of the quantity?H-1?2 with an block diagonal preconditioner and its algebraic analysis theory,i.e.,(23)Then,they used the bound estimate of ?H-1?2(23)to give the error bounds for the solu-tions of systems of equations(22)as follows.(24)where u,u? Rl represent the exact solution of saddle-point linear systems of equations(22)and the numerical solution with a certain accuracy,respectivelyBy the symmetry of the matrices A and BBT,they gotwhere Q(A)denotes the spectral radius of the matrix A.Thus,according to the error bound(24),they had(25)In general,the error bound(25)is easier to implement than the error bound(24)Besides,ifthen(26)where A-1 and BBT 1denote the approximates of the inverse of the matrices A and BBT with a certain accuracy,respectivelyAccording to the symmetric positive definiteness of matrices A and BBT and the stability of numerical methods for computing the inverse of a matrix today,the numerical matrices A-1 and BBT-1are very close to the matrices A-1 and(BBT)-1,respectively,so the assumptions ?A-1A-In??<1? ?BBT 1(BBT)-Im??<1 are easy to hold.To sum up,the verification method established by Kimura and Chen can be summa-rized as follows:(?)(27)The advantages of the verification method(27)are that it avoids using the approxima-tion of the inverse of the coefficient matrix H,adopts the error bound(25)which is easier to implement,and uses the bound estimates of ?A-1?? and ?(BBT)-1??(26)to achieve the purpose of fast computation of ?A-1?? and ?(BBT)-1??,the disadvantage is that the quantity ?(BBT)-1 ? can sometimes be very large,which makes the results given by the verification method(27)of little practical value.Furthermore,the sparsity of matrix A and the non-sparsity of approximation of its inverse matrix A-1 will make it impossible to solve the verification problem for large sparse linear systems of saddle-point type(22)by computer.In order to overcome the shortcomings of the verification method(27),we give the following improved verification method for large sparse linear system of saddle-point type(22).First,by the symmetric positive definite of the matrices A-1 and(BBT)-1,we getwhere ?min(·)represents the minimum eigenvalue of the matrix A or BBT,respectively.Second,if there are a>0 and ?>0 such that the matrices A-?In and BBT-?Im are also symmetric positive definite,thenThus,we haveAnd finally,using the symmetry of the matrix A and the error bound(24),we also have(?)(29)To sum up,the verification method we established is as follows.(?)(30)In practical application,in order to ensure the success and effect of the verification,the positive real numbers ? and,? presented in the verification method(30)are generally taken to be ?=0.9?min(A)or 0.95?min(A),and,?=0.9?min(BBT)or 0.95 ?min(BBT),re-spectively,where ?min(·)denotes the numerical approximation of the minimum eigenvalue of symmetric positive definite matrix A or BBT,which can be obtained by inverse power method.Because the symmetric positive definiteness of matrices A and BBT and the ad-vanced technology of computing the max-and minimum eigenvalue of matrix today,the above solution is feasible.The positive definiteness of real symmetric matrices A-?In and BBT-?Im are proved by the INTLAB function isspd.The theoretical result#12 and numerical experiments show that the improved verification method(30)not only con-sumes less computational load and computing time than the original verification method(27),but also gives a smaller error bound than the verification method(27).Moreover,theoretical analyses and numerical results also show that the improved verification method(30)is still efficient for the saddle-point linear system of equations(22)when the dimension l(i.e.,m+n)is larger,so the scope of application of the verifi-cation method(30)is wider than that of the verification method(27).In addition,we give another proof of the bound estimate of ?H 1?2(23)with the special structure and properties of the saddle-point matrix H and the basic matrix theory in Chapter 5.Compared with the original proof method,the new proof method is simpler.