OAI/Analysis/MatrixSigning/Matrices/RowDotBounds.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KS.W12.RowDot.storedLength line 14
2. theorem OAI.KS.W12.RowDot.payload_le_framed line 18
3. theorem OAI.KS.W12.RowDot.count_le_framed line 29
4. theorem OAI.KS.W12.RowDot.matrix_entry_length line 34
5. theorem OAI.KS.W12.RowDot.vector_entry_length line 41
6. theorem OAI.KS.W12.RowDot.dimension_le_vector line 47
7. theorem OAI.KS.W12.RowDot.matrix_parts_stored line 50
8. theorem OAI.KS.W12.RowDot.encodeNat_length_le_self line 62
9. theorem OAI.KS.W12.RowDot.pair_stream_length line 66
10. theorem OAI.KS.W12.RowDot.bodyTicks_stored line 94
11. theorem OAI.KS.W12.RowDot.loopTicks_stored line 122
12. theorem OAI.KS.W12.RowDot.totalTicks_stored line 147
13. theorem OAI.KS.W12.RowDot.polynomial_spec line 175