OAI/Analysis/HyperbolicCones/FiniteTopology.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Paper256.FiniteMatrix.sym_neg_norm_le line 14
2. theorem OAI.Paper256.FiniteMatrix.sym_le_norm line 28
3. theorem OAI.Paper256.FiniteMatrix.posDef_of_scalar_lower_bound line 40
4. theorem OAI.Paper256.FiniteMatrix.posDef_scalar_lower_bound line 45
5. theorem OAI.Paper256.FiniteMatrix.isOpen_posDef line 59
6. def OAI.Paper256.FiniteMatrix.quadraticEvaluation line 75
7. theorem OAI.Paper256.FiniteMatrix.isClosed_posSemidef line 80
8. theorem OAI.Paper256.FiniteMatrix.posSemidef_of_tendsto line 101