OAI/Analysis/MatrixSigning/Matrices/InvH.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.Hermitian.invH line 15
  2. theorem OAI.CurrentKS.Hermitian.invH_val line 17
  3. def OAI.CurrentKS.Hermitian.pd line 19
  4. lemma OAI.CurrentKS.Hermitian.pd_smul line 21
  5. lemma OAI.CurrentKS.Hermitian.psd_smul line 26
  6. lemma OAI.CurrentKS.Hermitian.convex_pd line 31
  7. theorem OAI.CurrentKS.Hermitian.inverse_convex line 37
  8. lemma OAI.CurrentKS.Hermitian.isClosed_lowerBound line 59
  9. lemma OAI.CurrentKS.Hermitian.isClosed_upperBound line 64
  10. lemma OAI.CurrentKS.Hermitian.isClosed_orderBox line 69
  11. theorem OAI.CurrentKS.Hermitian.inverse_antitone line 75
  12. lemma OAI.CurrentKS.Hermitian.scalar_posDef line 82
  13. lemma OAI.CurrentKS.Hermitian.scalar_inv line 85
  14. theorem OAI.CurrentKS.Hermitian.le_trace_smul_one line 92
  15. theorem OAI.CurrentKS.Hermitian.isCompact_orderBox line 114