Smoothness and derivatives of the determinant

The determinant of a square matrix over a nontrivially normed field is a continuous multilinear map of its rows. Its differential at every matrix, including singular matrices, is the sum of row replacements, or equivalently Jacobi's adjugate formula:

D det (A) H = trace (adjugate A * H).

At an invertible matrix this is det A * trace (A⁻¹ * H), and at the identity it is trace H. The matrix determinant is smooth, the matrix index may be empty, and none of the matrix results require the field to be complete. The determinant of a continuous linear endomorphism of a finite-dimensional normed space is also smooth; this result assumes a complete field.

The multilinear proof generalizes the real determinant calculus in the KLS formalization. It uses ContinuousMultilinearMap.hasFDerivAt and the algebraic identity Matrix.sum_det_updateRow_eq_trace_adjugate_mul.

The normed structure on matrices is Mathlib's L∞ operator norm, available through open scoped Matrix.Norms.Operator.

Main results

• Matrix.contDiff_det: the matrix determinant is smooth without scalar completeness.
• ContinuousLinearMap.contDiff_det: the determinant of a continuous linear endomorphism of a finite-dimensional normed space is smooth over a complete field.
• Matrix.differentiable_det: the determinant is differentiable at every matrix.
• Matrix.fderiv_det_eq_sum_updateRow: its differential is the sum of row replacements.
• Matrix.fderiv_det_updateRow: the row-replacement formula for a field with one row fixed.
• Matrix.fderiv_det_apply_adjugate: Jacobi's formula, including singular matrices.
• Matrix.hasDerivAt_det_one_add_smul: t ↦ det (1 + t • B) has derivative trace B at 0.
• Matrix.hasFDerivAt_det_one: the derivative at the identity is the trace.
• Matrix.hasFDerivAt_det, Matrix.fderiv_det_apply: the inverse form at an invertible matrix.

theorem Matrix.contDiff_det {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {r : WithTop ℕ∞} : ContDiff 𝕜 r det

The determinant is smooth, including at singular matrices.

theorem Matrix.differentiable_det {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] : Differentiable 𝕜 det

The determinant is differentiable at every matrix over a nontrivially normed field.

theorem Matrix.fderiv_det_eq_sum_updateRow {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] (A H : Matrix n n 𝕜) : (fderiv 𝕜 det A) H = ∑ i : n, (A.updateRow i (H i)).det

The differential of the determinant is the sum of determinants with one row replaced.

theorem Matrix.fderiv_det_updateRow {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (A : E → n → n → 𝕜) (x : E) (hA : ∀ (k l : n), DifferentiableAt 𝕜 (fun (y : E) => A y k l) x) (j : n) (c : n → 𝕜) (v : E) : (fderiv 𝕜 (fun (y : E) => (updateRow (A y) j c).det) x) v = ∑ k : n, if k = j then 0 else ((updateRow (A x) j c).updateRow k fun (l : n) => (fderiv 𝕜 (fun (y : E) => A y k l) x) v).det

The determinant of a differentiable matrix field with one row fixed has differential equal to the sum of row replacements over the other rows. No completeness assumption is needed.

theorem Matrix.fderiv_det_apply_adjugate {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] (A H : Matrix n n 𝕜) : (fderiv 𝕜 det A) H = (A.adjugate * H).trace

Jacobi's adjugate formula, valid at singular as well as invertible matrices.

theorem Matrix.fderiv_det_apply {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {A : Matrix n n 𝕜} (hA : IsUnit A.det) (H : Matrix n n 𝕜) : (fderiv 𝕜 det A) H = A.det * (A⁻¹ * H).trace

Jacobi's inverse formula, evaluated on a direction at an invertible matrix.

theorem Matrix.hasFDerivAt_det_one {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] : HasFDerivAt det { toLinearMap := traceLinearMap n 𝕜 𝕜, cont := ⋯ } 1

The Fréchet derivative of the determinant at the identity is the trace.

theorem Matrix.hasDerivAt_det_one_add_smul {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] (B : Matrix n n 𝕜) : HasDerivAt (fun (t : 𝕜) => (1 + t • B).det) B.trace 0

The determinant along the line through the identity in the direction B has derivative trace B at the identity.

theorem Matrix.hasFDerivAt_det {n : Type u_1} [Fintype n] [DecidableEq n] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {A : Matrix n n 𝕜} (hA : IsUnit A.det) : HasFDerivAt det (A.det • { toLinearMap := traceLinearMap n 𝕜 𝕜, cont := ⋯ } ∘SL (ContinuousLinearMap.mul 𝕜 (Matrix n n 𝕜)) A⁻¹) A

Jacobi's inverse formula. At a matrix with invertible determinant, the differential is H ↦ det A * trace (A⁻¹ * H).

theorem ContinuousLinearMap.contDiff_det {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] [CompleteSpace 𝕜] {r : WithTop ℕ∞} : ContDiff 𝕜 r fun (f : E →L[𝕜] E) => LinearMap.det ↑f

The determinant of an endomorphism of a finite-dimensional normed space is smooth.