Log-Determinant Trace Characterization

This is a matrix characterization used in the weak Monge–Ampère route.

Let $A$ be a positive semidefinite real $n\times n$ matrix and let $b\in\mathbb R$. Then the following are equivalent:

1. for every positive definite matrix $J$,

2. $A$ is positive definite and $e^b\le\det A$.

The statement is finite-dimensional and purely algebraic; it expresses the logarithmic determinant as an infimum of positive-definite trace functionals.

Original Lean declaration header

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

theorem forall_posDef_add_log_det_le_trace_iff {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ}
    (hA : A.PosSemidef) (b : ℝ) :
    (∀ J : Matrix (Fin n) (Fin n) ℝ, J.PosDef → b + Real.log J.det + n ≤ (J * A).trace) ↔
      (A.PosDef ∧ Real.exp b ≤ A.det)

Module navigation

Module: Analysis/Matrix/LogDet.

Next: scalar_log_gap.

Source excerpt, lines 113–116 · Frozen source 408915f.