How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Matrix Differentiation and First-order Spectral Perturbation
1 · Prerequisites
- Algebraic Closure, Embeddings, and Separability
- Algebraic Extensions, Extension Degree, and Finite Fields
- Binary Operations, Monoids, Groups and Subgroups
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Composition Series, the Jordan–Hölder Theorem and Solvable Groups
- Congruences, the Integers Modulo n and the Chinese Remainder Theorem
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Cyclic Groups and Direct Products
- Determinants of Matrices over a Commutative Ring
- Diagonalisation and the Minimal Polynomial
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Divisibility, Greatest Common Divisors and Bézout's Identity
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Eigenvalues, Eigenvectors and the Characteristic Polynomial
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Group Homomorphisms and the Isomorphism Theorems
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Matrix Norms, Condition Numbers and Numerical Stability
- Metric Spaces
- Mixed Partials, Taylor Formulae, and Extrema
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Order, Zorn's Lemma, and the Axiom of Choice
- Polynomial Rings, the Division Algorithm and Roots
- Primes, Euclid's Lemma and the Fundamental Theorem of Arithmetic
- Properties of the Integral and the Working FTC
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Simple Field Extensions and the Construction of the Complex Numbers
- Splitting Fields
- Suprema and Infima
- Sylow's Theorems, p-Groups and Nilpotent Groups
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- The Derivative and the Mean Value Theorems
- The Determinant of a Linear Operator, Cofactors and Cramer's Rule
- The Fundamental Theorem of Algebra
- The Fundamental Theorem of Finite Abelian Groups
- The Galois Correspondence
- The Inverse and Implicit Function Theorems
- The Inverse Function Theorem Completed
- The Riemann Integral: Definition and Integrability
- The Spectral Theorem, Positive Operators and Singular Value Decomposition
- The Total Derivative in ℝᵐ → ℝⁿ
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Triangularisation, Generalised Eigenspaces and Jordan Canonical Form
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
This page works over the underlying real vector space throughout. It first packages the differential rules that later perturbation formulas actually use: sum, product, adjoint, inverse, determinant, trace, and least-squares gradients.
The spectral half stays strictly in the simple-spectrum regime. After the left/right eigendata, projector, and reduced resolvent are in place, the page uses the real implicit-function theorem to produce local branches and then derives the first-order eigenvalue, projector, eigenvector, and singular value formulas. The closing counterexamples record exactly where simplicity, gauge-fixing, and first-order differentiability fail.
3 · Logical flowchart
4 · Definitions, theorems and proofs
The real Frechet derivative on real and complex matrix spaces with the Frobenius norm
Definition
Let be an open subset of a real matrix space or of a complex matrix space viewed as a real vector space, and let take values in a finite-dimensional real normed vector space . We say that is real Fr'echet differentiable at if there is a real-linear map such that
That map is the real Fr'echet derivative of at and is denoted .
Matrix differentials obey the sum rule, product rule, and adjoint rule
Statement
In the real Fr'echet sense on matrix spaces:
- for fixed ;
- ;
- .
Equivalently, differential notation gives , , and .
Facts & Assumptions
Given: Compatible matrices and perturbation directions.
Real Fr'echet differentiability means (The real Frechet derivative on real and complex matrix spaces with the Frobenius norm).
Proof
For the sum map, , so the linear term is already . For the adjoint map, , so the linear term is . Both have zero remainder in the sense of [F1].
For the product map, The bilinear term satisfies , so [F1] identifies the derivative as . This is exactly the product rule.
On the invertible locus,
Statement
Let be invertible. Then the inversion map is real Fr'echet differentiable at , and for every direction ,
Facts & Assumptions
Given: An invertible matrix and a perturbation direction .
Matrix differentials satisfy the product rule (Matrix differentials obey the sum rule, product rule, and adjoint rule).
Proof
Because is invertible, . Since is a polynomial in the real coordinates of with value at , there is such that is invertible whenever . For such , the identities give and hence
Shrink so that whenever . From step 1.1, so . Applying this bound to the second identity in step 1.1 yields Therefore inversion is real Fr'echet differentiable at with derivative .
Differentiating the identity and using the product rule [L1] gives Left-multiplying by recovers which is the formula claimed in the statement.
The determinant differential is at every matrix, and Jacobi's formula holds on the invertible locus
Statement
Let be an matrix and let be a direction matrix. Then
If is invertible, then
Facts & Assumptions
Given: An matrix and a perturbation direction .
On the invertible locus, the derivative of inversion is (On the invertible locus, ).
Proof
The determinant is multilinear in the columns. In , the coefficient of comes from replacing exactly one column of by the corresponding column of . Those cofactors are precisely the entries of , so .
If is invertible, then . Substituting this identity into step 1.1 gives , which is Jacobi's formula on the invertible locus. The domain restriction matters because appears explicitly there, unlike the adjugate formula of step 1.1.
Trace and Frobenius-linear matrix functionals differentiate by inspection
Statement
For square matrices,
For a fixed matrix , the real-valued Frobenius-linear functional
satisfies
Thus the Frobenius gradient of is .
Facts & Assumptions
Given: A matrix , a perturbation direction , and a fixed matrix .
Real Fr'echet differentiability identifies the first-order linear term in (The real Frechet derivative on real and complex matrix spaces with the Frobenius norm).
Proof
The trace is linear, so . Likewise, Each increment is already linear in .
Therefore [F1] gives the displayed derivatives. The Frobenius gradient is the unique matrix satisfying for every , and step 1.1 shows that .
Matrix quadratic forms have the expected first derivative and Hessian
Statement
Fix a matrix and consider the real-valued quadratic form
Then
so the gradient is , and the Hessian is the constant Hermitian map .
Facts & Assumptions
Given: A fixed matrix , a vector , and a perturbation direction .
Matrix differentials satisfy the product and adjoint rules (Matrix differentials obey the sum rule, product rule, and adjoint rule).
Frobenius-linear functionals differentiate by inspection (Trace and Frobenius-linear matrix functionals differentiate by inspection).
Proof
Expanding at gives Hence so the gradient is .
The derivative of the gradient map is the constant linear map . Therefore the Hessian is .
The Frobenius least-squares objective has gradient and Hessian in the vector variable
Statement
For fixed and , let
Then
so the gradient is and the Hessian is the constant map .
Facts & Assumptions
Given: A fixed matrix , a fixed vector , a vector , and a direction .
The quadratic form has gradient and Hessian (Matrix quadratic forms have the expected first derivative and Hessian).
Proof
Write only heuristically; directly, Expanding yields
The gradient map from step 1.1 is , whose derivative is the constant linear map . Thus the Hessian is .
Compatible left and right eigenvectors for a simple eigenvalue
Definition
Let , equipped with the standard Hermitian inner product, and let be a simple eigenvalue of . A nonzero vector is a right eigenvector for if
A nonzero vector is a left eigenvector for if
equivalently .
Such and are called compatible left and right eigenvectors for the simple eigenvalue .
For a simple eigenvalue, left and right eigenvectors pair nontrivially and may be normalized by
Statement
Let be a simple eigenvalue of , and let be compatible right and left eigenvectors. Then . Consequently, after rescaling either vector, one may impose the normalization
Facts & Assumptions
Given: A simple eigenvalue of and compatible nonzero vectors with and .
Compatible left and right eigenvectors for a simple eigenvalue satisfy the displayed equations above (Compatible left and right eigenvectors for a simple eigenvalue).
Proof
Assume for contradiction that . Then . Also , so . Because is simple, and , hence . Therefore for some .
Step 1.1 gives while , so starts a Jordan chain of length for . That contradicts the simplicity of . Hence . Scaling by yields the normalization .
The normwise condition number of a simple eigenvalue
Definition
Let be a simple eigenvalue of . The normwise first-order condition number of is
where, for any compatible nonzero right and left eigenvectors , we set
The denominator is nonzero by For a simple eigenvalue, left and right eigenvectors pair nontrivially and may be normalized by . Any other compatible pair differs by nonzero rescalings because the two eigenspaces are one-dimensional, and those factors cancel from the quotient, so this definition is independent of the chosen pair. The later eigenvalue-derivative theorem shows that this functional is the actual derivative of every local simple eigenvalue branch.
The simple spectral projector
Definition
Let be a simple eigenvalue of , and let be compatible nonzero right and left eigenvectors. Since , the rank-one map
is well defined. It is the simple spectral projector onto the eigendirection along .
The simple spectral projector is unchanged by nonzero rescalings of the left and right eigenvectors
Statement
Let be the simple spectral projector of a simple eigenvalue. If , then the projector formed from and is still .
Facts & Assumptions
Given: A simple spectral projector and nonzero scalars .
The projector attached to compatible eigenvectors is (The simple spectral projector ).
Proof
By [F1], one has . Since also , the rescaled denominator satisfies Therefore the rescaled projector is well defined, and using [F1] again gives
Thus nonzero rescaling changes numerator and denominator by the same nonzero factor and leaves the spectral projector unchanged.
The reduced resolvent, or group inverse, on the complementary invariant subspace of a simple eigenvalue
Definition
Let be a simple eigenvalue of , and let be its simple spectral projector. The reduced resolvent, also called the group inverse at , is the unique linear map satisfying
It acts as the inverse of on the complementary invariant subspace and vanishes on the eigendirection.
The reduced resolvent satisfies the standard projector and inverse identities on the complementary invariant subspace
Statement
Let be a simple eigenvalue of , let be compatible eigenvectors normalized by , and let . Then the restriction of to is a bijection . If is its inverse on and , then
and this is unique.
Facts & Assumptions
Given: A simple eigenvalue , normalized compatible eigenvectors , and the projector .
Under the normalization , the simple spectral projector is (The simple spectral projector ).
Proof
Every vector decomposes uniquely as , with the second term in . If and , then is a right eigenvector for the simple eigenvalue , so for some scalar . Applying gives , hence . Therefore the restriction of to is injective, and since both domain and codomain have dimension , it is bijective.
Define to be the inverse of that restriction on and to vanish on . Then by construction. For with , [F1] gives , so . Therefore , and similarly . Thus all displayed identities hold.
If is another linear map with the same identities, then because and . On one has , and the injectivity from step 1.1 gives . Hence , so the reduced resolvent of The reduced resolvent, or group inverse, on the complementary invariant subspace of a simple eigenvalue is well defined and unique.
A simple eigenvalue and a gauge-fixed right eigenvector admit local branches in the underlying real matrix space
Statement
Let be a square matrix with simple eigenvalue , and choose compatible eigenvectors normalized by . Then, in a neighborhood of inside the underlying real matrix space, there exist unique maps and such that
with and .
Facts & Assumptions
Given: A base matrix , a simple eigenvalue , and normalized compatible eigenvectors .
For a simple eigenvalue, one may normalize compatible left and right eigenvectors by (For a simple eigenvalue, left and right eigenvectors pair nontrivially and may be normalized by ).
The parametrized implicit-function theorem gives a unique local solution once the derivative in the solved-for variables is invertible (The parametrized implicit function theorem with regularity).
Proof
Consider the real map . Its derivative in at is . If this derivative vanishes, then left-multiplying the first component by gives , hence by [L1]. Then and , so is a multiple of whose pairing with is zero; therefore . Thus the derivative is injective. Because domain and codomain have the same real dimension, it is invertible.
The hypotheses of [L2] now apply to at . Therefore there are neighborhoods and unique maps and solving . Those equations are exactly and , with the required base values.
Along a differentiable matrix path, a simple eigenvalue satisfies under the normalization
Statement
Let be differentiable, and let be a simple eigenvalue with differentiable compatible eigenvectors normalized by . Then
Facts & Assumptions
Given: A differentiable matrix path , a differentiable simple eigenpair branch , and the normalization .
Simple eigenpairs admit local differentiable branches after gauge fixing (A simple eigenvalue and a gauge-fixed right eigenvector admit local branches in the underlying real matrix space).
Proof
Differentiate the eigenvalue equation : Left-multiply by . Since , the terms with cancel.
Step 1.1 leaves . The normalization therefore gives .
The normwise condition number of a simple eigenvalue is
Statement
Let be a simple eigenvalue of , and let be compatible nonzero right and left eigenvectors. Then
In particular, for the normalization one has .
Facts & Assumptions
Given: A simple eigenvalue of and compatible nonzero vectors .
The condition number is (The normwise condition number of a simple eigenvalue).
For any differentiable branch normalized by , (Along a differentiable matrix path, a simple eigenvalue satisfies under the normalization ).
Proof
Normalize first so that . Then [L1] gives by Cauchy-Schwarz. Taking the supremum over in [F1] yields .
Let and , and define . Then and . Hence [F1] and [L1] give the reverse inequality, so under the normalization . Undoing the normalization inserts the factor and gives the general formula.
The derivative of the simple spectral projector is expressed by the reduced resolvent and the perturbation
Statement
Let be differentiable, let be a simple eigenvalue branch, let be the corresponding simple spectral projector, and let be the reduced resolvent at . Then
Facts & Assumptions
Given: A differentiable simple spectral projector branch for a simple eigenvalue branch of , and the reduced resolvent at .
The reduced resolvent satisfies and (The reduced resolvent satisfies the standard projector and inverse identities on the complementary invariant subspace).
Proof
Differentiate at : Left-multiplying by and using [L1] together with gives Differentiating and right-multiplying by similarly gives
Differentiating gives . Because , this decomposes as . Substituting the two identities from step 1.1 yields which is the claimed formula.
In a fixed gauge, the derivative of a simple right eigenvector is obtained by applying the reduced resolvent to the perturbation
Statement
Let be differentiable, let be a simple eigenvalue branch, and let be the right eigenvector branch chosen in the fixed gauge , where is the left eigenvector at . If is the reduced resolvent at , then
Facts & Assumptions
Given: A differentiable simple eigenpair branch in the fixed gauge and the reduced resolvent at .
The reduced resolvent satisfies and (The reduced resolvent satisfies the standard projector and inverse identities on the complementary invariant subspace).
The eigenvalue derivative is (Along a differentiable matrix path, a simple eigenvalue satisfies under the normalization ).
Proof
Differentiate at : Apply and use [L1]: Because the fixed gauge gives , the derivative lies in , so .
Step 1.1 therefore gives . Since by [L1], the term disappears and .
For a Hermitian simple eigenvalue, one may take and the first-order formulas simplify accordingly
Statement
If is a differentiable Hermitian matrix path, and is a differentiable simple eigenpair branch with , then one may choose the phase locally so that . With that choice,
Facts & Assumptions
Given: A differentiable Hermitian matrix path and a differentiable simple unit eigenvector branch .
For a simple eigenpair, the eigenvalue derivative is , and in a fixed gauge the eigenvector derivative is (Along a differentiable matrix path, a simple eigenvalue satisfies under the normalization , In a fixed gauge, the derivative of a simple right eigenvector is obtained by applying the reduced resolvent to the perturbation).
Proof
If and , then taking adjoints shows . Thus the same unit eigenvector can serve as both left and right eigenvector. Multiplying by a unit complex phase if necessary imposes the gauge .
Substitute into the formulas summarized in [L1]. This gives and, in the chosen gauge, .
If is a simple singular value with left and right singular vectors , then its real directional derivative is
Statement
Let be a matrix, let be a simple singular value of , and let be corresponding unit left and right singular vectors, so and . Then the real directional derivative of in the direction is
Facts & Assumptions
Given: A matrix , a simple positive singular value , unit singular vectors , and a perturbation direction .
For a Hermitian simple eigenvalue, the directional derivative is for the corresponding unit eigenvector (For a Hermitian simple eigenvalue, one may take and the first-order formulas simplify accordingly).
A simple eigenvalue of a differentiable matrix path admits a local eigenvalue branch after gauge fixing (A simple eigenvalue and a gauge-fixed right eigenvector admit local branches in the underlying real matrix space).
Proof
Form the Hermitian block path Then is a unit eigenvector of with eigenvalue , because If , then and , so . Since is a simple positive singular value, the eigenspace of for is one-dimensional, and then is determined by . Hence is a simple eigenvalue of the Hermitian matrix .
Because is differentiable and step 1.1 shows that is a simple eigenvalue of , [L2] gives a local eigenvalue branch through . The derivative of the block path is Applying [L1] to this Hermitian simple eigenvalue branch gives
Expanding the quadratic form from step 2.1 gives
A defective Jordan block can split under perturbation at square-root scale
Statement refuted
Every eigenvalue varies differentiably to first order through a defective point.
Consider
Its eigenvalues are , so the splitting occurs at square-root scale rather than linearly.
Facts & Assumptions
Given: The perturbed Jordan block .
Eigenvalues are roots of the characteristic polynomial (Eigenvalues, eigenvectors, eigenspaces , and the spectrum of an endomorphism).
Counterexample
By [F1], Therefore the eigenvalues are exactly .
The functions do not admit ordinary linear first-order expansions at . Hence a defective eigenvalue need not possess differentiable ordered branches through the perturbation, refuting the claim.
An ordered eigenvector branch need not extend differentiably through an eigenvalue crossing
Statement refuted
An eigenvector branch chosen by ordering eigenvalues can always be continued differentiably through a crossing.
The family
shows otherwise: the eigendirection belonging to the larger eigenvalue is for and for .
Facts & Assumptions
Given: The symmetric family .
Simple eigenpair branches exist locally only while the eigenvalue stays simple (A simple eigenvalue and a gauge-fixed right eigenvector admit local branches in the underlying real matrix space).
Counterexample
For , the larger eigenvalue is with eigendirection . For , the larger eigenvalue is with eigendirection . At , the eigenvalue has multiplicity .
Any branch chosen by ordering the eigenvalues by size must jump from on the left to on the right, so it is not even continuous, let alone differentiable, through the crossing. This agrees with [L1], which applies only on the simple-spectrum locus.
5 · Examples, counterexamples and false statements
None yet.