Quantitative Concavity of Log Determinant

Proved

FunctionalInequalities.Analysis.log_det_add_frobenius_sq_le_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is the quantitative matrix log-determinant inequality cited in the module documentation in connection with Lemma 4.2 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1).

Let $A,B$ be real $n\times n$ matrices and $K\in\mathbb R$ . Assume:

$A$ and $B$ are positive definite.
$K I-A$ is positive semidefinite.
$K I-B$ is positive semidefinite.

Then

\log\det B+\frac{\|B-A\|_F^2}{2K^2} \le \log\det A+\operatorname{tr}\!\left(A^{-1}(B-A)\right),

where $\|B-A\|_F^2=\sum_{i,j}(B_{ij}-A_{ij})^2$ . The declaration log_det_add_frobenius_sq_le_readable is a finite-dimensional matrix inequality; positivity and the upper bounds are expressed through PosDef and PosSemidef.

Original Lean declaration header

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

theorem log_det_add_frobenius_sq_le {n : ℕ} {A B : Matrix (Fin n) (Fin n) ℝ} {K : ℝ}
    (hA : A.PosDef) (hB : B.PosDef) (hAK : (K • (1 : Matrix (Fin n) (Fin n) ℝ) - A).PosSemidef)
    (hBK : (K • (1 : Matrix (Fin n) (Fin n) ℝ) - B).PosSemidef) :
    Real.log B.det + (∑ i, ∑ j, (B - A) i j ^ 2) / (2 * K ^ 2) ≤
      Real.log A.det + (A⁻¹ * (B - A)).trace

Module navigation

Module: Analysis/Matrix/LogDet.

Supporting theorems: scalar_log_gap.

Previous: scalar_log_gap.

Source excerpt, lines 347–351 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_LogDet

set_option maxHeartbeats 800000

Formal statement


theorem FunctionalInequalities.Analysis.log_det_add_frobenius_sq_le_readable {n : ℕ} {A B : Matrix (Fin n) (Fin n) ℝ} {K : ℝ}
    (hA : A.PosDef) (hB : B.PosDef) (hAK : (K • (1 : Matrix (Fin n) (Fin n) ℝ) - A).PosSemidef)
    (hBK : (K • (1 : Matrix (Fin n) (Fin n) ℝ) - B).PosSemidef) :
    Real.log B.det + (∑ i, ∑ j, (B - A) i j ^ 2) / (2 * K ^ 2) ≤
      Real.log A.det + (A⁻¹ * (B - A)).trace := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Matrix/LogDet.lean#L344-L484 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Matrix.LogDet`, declaration `FunctionalInequalities.Analysis.log_det_add_frobenius_sq_le`; the repository is private at upload time).

View graph