Jacobi Formula for the Determinant

Proved

FunctionalInequalities.Analysis.fderiv_det_eq_det_mul_trace_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readableletwin2026log-concave

This is Jacobi’s formula for a real square matrix.

Let $M,N$ be matrices indexed by a finite type, and assume $\det M$ is a unit, equivalently that $M$ is invertible. Then the Fréchet derivative of the determinant at $M$ in direction $N$ is

D(\det)_M[N]=\det(M)\,\operatorname{tr}(M^{-1}N).

The result is a finite-dimensional algebraic identity and imposes no symmetry, positivity, or regularity assumptions on $M$ or $N$ . In Lean it is expressed by fderiv ℝ Matrix.det M N and matrix multiplication and trace.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem fderiv_det_eq_det_mul_trace (M N : Matrix ι ι ℝ) (hM : IsUnit M.det) :
    fderiv ℝ Matrix.det M N = M.det * Matrix.trace (M⁻¹ * N)

Module navigation

Module: Analysis/Matrix/DeterminantDerivative.

Source excerpt, lines 46–47 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_DeterminantDerivative

variable {ι : Type*} [Fintype ι] [DecidableEq ι]

Formal statement


theorem FunctionalInequalities.Analysis.fderiv_det_eq_det_mul_trace_readable (M N : Matrix ι ι ℝ) (hM : IsUnit M.det) :
    fderiv ℝ Matrix.det M N = M.det * Matrix.trace (M⁻¹ * N) := by sorry

Source

Source: Letwin, The KLS constant is O(log^(1/4) n) (arXiv:2607.24164v1), Lemma 2.4. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Matrix/DeterminantDerivative.lean#L45-L68 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Matrix.DeterminantDerivative`, declaration `FunctionalInequalities.Analysis.fderiv_det_eq_det_mul_trace`; the repository is private at upload time).

View graph