OAI/Analysis/MatrixSigning/Arithmetic/ArithmeticEncodingSize.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KS.W01.ratLength line 11
  2. theorem OAI.KS.W01.intPayload_le_natAbs line 13
  3. theorem OAI.KS.W01.natAbs_le_intPayload_add_one line 16
  4. theorem OAI.KS.W01.natAbs_size_le_payload_size_add_one line 19
  5. theorem OAI.KS.W01.rational_parts_size_le_length line 28
  6. theorem OAI.KS.W01.rational_parts_le_two_pow_length line 36
  7. theorem OAI.KS.W01.ratLength_le_of_parts line 43
  8. theorem OAI.KS.W01.ratLength_mul_le line 54
  9. theorem OAI.KS.W01.ratLength_add_le line 63
  10. theorem OAI.KS.W01.ratLength_neg_le line 72
  11. theorem OAI.KS.W01.ratLength_sub_le line 78
  12. theorem OAI.KS.W01.mul_parts_size_le line 88
  13. theorem OAI.KS.W01.add_parts_size_le line 99
  14. def OAI.KS.W01.complexLength line 110
  15. theorem OAI.KS.W01.complexLength_eq line 112
  16. theorem OAI.KS.W01.complexLength_add_le line 116
  17. theorem OAI.KS.W01.complexLength_mul_le line 124