OAI/Analysis/MatrixSigning/Optimization/NegativeWitness.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KS.W17.quadratic_single line 11
2. theorem OAI.KS.W17.negativeDiagonal_witness line 15
3. theorem OAI.KS.W17.quadratic_twoSingle line 20
4. def OAI.KS.W17.zeroPivotWitness line 27
5. theorem OAI.KS.W17.zeroPivotWitness_value line 30
6. theorem OAI.KS.W17.zeroPivotWitness_negative line 39