OAI/Analysis/MatrixSigning/Matrices/PivotScannerBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KS.W23.PivotScannerBounds.classifier_code_length line 14
2. theorem OAI.KS.W23.PivotScannerBounds.classify_payload_bound line 19
3. theorem OAI.KS.W23.PivotScannerBounds.row_body_payload_bound line 39
4. theorem OAI.KS.W23.PivotScannerBounds.entry_payload_bound line 50
5. theorem OAI.KS.W23.PivotScannerBounds.loop_payload_bound line 58
6. theorem OAI.KS.W23.PivotScannerBounds.initialize_bound line 69
7. theorem OAI.KS.W23.PivotScannerBounds.finish_payload_bound line 76
8. theorem OAI.KS.W23.PivotScannerBounds.row_payload_bound line 85
9. theorem OAI.KS.W23.PivotScannerBounds.decision_payload_ticks line 106
10. theorem OAI.KS.W23.PivotScannerBounds.decision_payload_spec line 118