OAI/Analysis/MatrixSigning/Potential/PairHilbert.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CurrentKS.Variational.PairHilbert line 16
2. def OAI.CurrentKS.Variational.pairEquiv line 21
3. def OAI.CurrentKS.Variational.pairHilbertCone line 24
4. lemma OAI.CurrentKS.Variational.pairHilbertCone_pointed line 35
5. lemma OAI.CurrentKS.Variational.isClosed_pairHilbertCone line 44
6. lemma OAI.CurrentKS.Variational.pairHilbert_interior line 47
7. def OAI.CurrentKS.Variational.onPairHilbert line 55
8. lemma OAI.CurrentKS.Variational.linConstraint_symmetric line 58
9. lemma OAI.CurrentKS.Variational.linConstraint_stationary line 69
10. theorem OAI.CurrentKS.Variational.linConstraint_inverse_norm line 80