OAI/Analysis/MatrixSigning/Complexity/ComplexScalarCosts.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W15.ComplexMachine.negativeOneWire line 13
2. theorem OAI.KS.W15.ComplexMachine.negativeOneWire_eq line 14
3. def OAI.KS.W15.ComplexMachine.negNode line 16
4. def OAI.KS.W15.ComplexMachine.negNodeTicks line 21
5. theorem OAI.KS.W15.ComplexMachine.negNode_spec line 24
6. theorem OAI.KS.W15.ComplexMachine.mulNodeTicks_le line 44
7. theorem OAI.KS.W15.ComplexMachine.addNodeTicks_le line 56
8. theorem OAI.KS.W15.ComplexMachine.negNodeTicks_le line 68