OAI/Analysis/HyperbolicCones/FormPositive.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Positivity of the Choi--Lam form, including its principal-minor argument.

  1. theorem OAI.Paper256.cyclic_cubic_nonnegative line 14
  2. theorem OAI.Paper256.zMatrix_det_nonnegative line 31
  3. theorem OAI.Paper256.quadratic_two_nonnegative line 35
  4. theorem OAI.Paper256.quadratic_three_nonnegative line 48
  5. theorem OAI.Paper256.posSemidef_three_of_principal_minors line 70

    Source documentation

    For a symmetric three-by-three matrix, its principal minors certify positivity.

    theorem posSemidef_three_of_principal_minors (M : Mat 3 ℝ) (hM : M.IsHermitian)
    (hdiag : ∀ i, 0 ≤ M i i)
    (h01 : M 0 1 ^ 2 ≤ M 0 0 * M 1 1)
    (h02 : M 0 2 ^ 2 ≤ M 0 0 * M 2 2)
    (h12 : M 1 2 ^ 2 ≤ M 1 1 * M 2 2) (hdet : 0 ≤ Matrix.det M) :
    M.PosSemidef := by
…

    Mentions: OAI.Paper256.Mat

  6. theorem OAI.Paper256.zMatrix_posSemidef line 90
  7. theorem OAI.Paper256.choiLam_nonnegative line 104
  8. theorem OAI.Paper256.qMatrix_posSemidef line 108