DeterminantCompression.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The determinant comparison used when the first sine mode is split off from a discrete Jacobi matrix. The complementary block need not commute with the first block or with the curvature matrices at other times.

theorem OAI.PositiveEinsteinFour.Jacobi.det_le_exp_trace line 20

Source documentation

The trace form of the arithmetic-geometric mean estimate.

theorem det_le_exp_trace {n : Type*} [Fintype n] [DecidableEq n]
    {A : Matrix n n ℝ} (hA : A.PosSemidef) :
    A.det ≤ Real.exp (A.trace - Fintype.card n) := by
…

theorem OAI.PositiveEinsteinFour.Jacobi.det_le_one_of_trace_le_card line 39

theorem OAI.PositiveEinsteinFour.Jacobi.det_fromBlocks_le_first line 50

Source documentation

Discarding the complementary modes costs no determinant when their trace is at most their dimension. This is the finite-matrix step in the upper radial comparison.

theorem det_fromBlocks_le_first {m n : Type*}
    [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n]
    {P : Matrix m m ℝ} {C : Matrix m n ℝ} {Q : Matrix n n ℝ}
    (hP : P.PosDef) (hA : (fromBlocks P C Cᴴ Q).PosSemidef)
    (htrace : Q.trace ≤ Fintype.card n) :
    (fromBlocks P C Cᴴ Q).det ≤ P.det := by
…

theorem OAI.PositiveEinsteinFour.Jacobi.det_posDef_fromBlocks_le_first line 70

Source documentation

In a positive definite block matrix, the first compression is already positive definite; no extra hypothesis on it is necessary.

theorem det_posDef_fromBlocks_le_first {m n : Type*}
    [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n]
    {P : Matrix m m ℝ} {C : Matrix m n ℝ} {Q : Matrix n n ℝ}
    (hA : (fromBlocks P C Cᴴ Q).PosDef)
    (htrace : Q.trace ≤ Fintype.card n) :
    (fromBlocks P C Cᴴ Q).det ≤ P.det := by
…