OAI/Analysis/MatrixSigning/Potential/SchurBlock.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.Variational.schurBlock line 15
  2. lemma OAI.CurrentKS.Variational.schurBlock_psd_iff line 18
  3. def OAI.CurrentKS.Variational.valueBlock₁ line 27
  4. def OAI.CurrentKS.Variational.valueBlock₂ line 30
  5. lemma OAI.CurrentKS.Variational.valueBlocks_iff line 33
  6. def OAI.CurrentKS.Variational.oracleBox line 48
  7. def OAI.CurrentKS.Variational.valueSpectrahedron line 53
  8. lemma OAI.CurrentKS.Variational.mem_valueSpectrahedron line 56
  9. lemma OAI.CurrentKS.Variational.sublevel_oracleBox line 67