OAI/Analysis/MatrixSigning/Complexity/RationalGridBits.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.RationalGridSize.Grid line 7
  2. lemma OAI.CurrentKS.RationalGridSize.Grid.zero line 9
  3. lemma OAI.CurrentKS.RationalGridSize.Grid.one line 10
  4. lemma OAI.CurrentKS.RationalGridSize.Grid.integer line 11
  5. lemma OAI.CurrentKS.RationalGridSize.Grid.neg line 12
  6. lemma OAI.CurrentKS.RationalGridSize.Grid.add line 14
  7. lemma OAI.CurrentKS.RationalGridSize.Grid.sub line 16
  8. lemma OAI.CurrentKS.RationalGridSize.Grid.mul_integer line 18
  9. lemma OAI.CurrentKS.RationalGridSize.Grid.den_le line 22
  10. lemma OAI.CurrentKS.RationalGridSize.numerator_le_den line 25
  11. lemma OAI.CurrentKS.RationalGridSize.coordinate_size_bound line 37
  12. def OAI.CurrentKS.RationalGridSize.bitSize line 44
  13. lemma OAI.CurrentKS.RationalGridSize.coordinate_bit_bound line 46
  14. lemma OAI.CurrentKS.RationalGridSize.size_mul_le line 54
  15. lemma OAI.CurrentKS.RationalGridSize.size_prod_le line 59