OAI/Algebra/FormulaHitting/OutputBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.NCHitting.length_flatMap_uniform line 9
  2. theorem OAI.NCHitting.getElem?_flatMap_uniform line 23
  3. theorem OAI.NCHitting.rows_length line 49
  4. theorem OAI.NCHitting.generate_output_length line 56
  5. theorem OAI.NCHitting.encodedEntry_numerator_le line 69
  6. theorem OAI.NCHitting.encodedEntry_denominator_size_le line 73
  7. theorem OAI.NCHitting.generate_entry_bounds line 82
  8. theorem OAI.NCHitting.flattened_entry line 100
  9. theorem OAI.NCHitting.generate_entry_code line 123
  10. theorem OAI.NCHitting.generate_entry_decode line 142