OAI/Analysis/MatrixSigning/Complexity/BitSupport.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.RationalBits.Parts line 9
  2. lemma OAI.CurrentKS.RationalBits.Parts.mono line 11
  3. lemma OAI.CurrentKS.RationalBits.Parts.mul line 14
  4. lemma OAI.CurrentKS.RationalBits.Parts.add line 16
  5. lemma OAI.CurrentKS.RationalBits.Parts.inv line 19
  6. lemma OAI.CurrentKS.RationalBits.Parts.div line 21
  7. lemma OAI.CurrentKS.RationalBits.Parts.neg line 23
  8. lemma OAI.CurrentKS.RationalBits.Parts.abs line 25
  9. lemma OAI.CurrentKS.RationalBits.parts_size line 29
  10. def OAI.CurrentKS.RationalBits.LinearBits line 36
  11. lemma OAI.CurrentKS.RationalBits.LinearBits.coordinate line 39
  12. lemma OAI.CurrentKS.RationalBits.LinearBits.constant line 43
  13. lemma OAI.CurrentKS.RationalBits.LinearBits.add line 47
  14. lemma OAI.CurrentKS.RationalBits.LinearBits.mul line 54
  15. lemma OAI.CurrentKS.RationalBits.LinearBits.inv line 61
  16. lemma OAI.CurrentKS.RationalBits.LinearBits.div line 64
  17. lemma OAI.CurrentKS.RationalBits.LinearBits.abs line 67
  18. lemma OAI.CurrentKS.RationalBits.LinearBits.pow line 70
  19. lemma OAI.CurrentKS.RationalBits.LinearBits.choose line 75
  20. lemma OAI.CurrentKS.RationalBits.LinearBits.min line 85
  21. lemma OAI.CurrentKS.RationalBits.LinearBits.max line 88
  22. lemma OAI.CurrentKS.frame_length line 98
  23. lemma OAI.CurrentKS.payload_length line 103
  24. lemma OAI.CurrentKS.encodeNat_length line 113
  25. lemma OAI.CurrentKS.int_parts_length line 116
  26. lemma OAI.CurrentKS.nat_parts_length line 134
  27. lemma OAI.CurrentKS.RationalEntry.parts_length line 141
  28. lemma OAI.CurrentKS.Input.matrix_length line 145
  29. lemma OAI.CurrentKS.Input.length_eq line 150
  30. lemma OAI.CurrentKS.Input.count_le_length line 156
  31. lemma OAI.CurrentKS.Input.each_matrix_le_length line 164
  32. lemma OAI.CurrentKS.Input.each_complex_le_length line 171
  33. lemma OAI.CurrentKS.complex_encode_pos line 183
  34. lemma OAI.CurrentKS.Input.dimension_le_length line 189
  35. lemma OAI.CurrentKS.Input.real_parts line 205
  36. lemma OAI.CurrentKS.Input.imag_parts line 212
  37. lemma OAI.CurrentKS.RationalBits.parts_zero line 224
  38. lemma OAI.CurrentKS.RationalBits.parts_one line 225
  39. lemma OAI.CurrentKS.RationalBits.sum_parts line 227
  40. lemma OAI.CurrentKS.RationalBits.Parts.binary_size line 237
  41. lemma OAI.CurrentKS.RationalInput.coordinates_parts line 252
  42. lemma OAI.CurrentKS.RationalInput.trace_parts line 259
  43. lemma OAI.CurrentKS.RationalInput.scale_parts line 263
  44. lemma OAI.CurrentKS.RationalInput.orientation_parts line 267
  45. theorem OAI.CurrentKS.RationalInput.normalized_parts_input_length line 273
  46. theorem OAI.CurrentKS.RationalInput.normalized_binary_size line 286