OAI/Combinatorics/KMedian/Compression/CompressionBounds.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.lawStep line 13
  2. theorem OAI.MetricKMedian.IntegerLaw.BinaryCompression.input_iterate line 16
  3. theorem OAI.MetricKMedian.IntegerLaw.BinaryCompression.lawStep_denominator line 24
  4. theorem OAI.MetricKMedian.IntegerLaw.BinaryCompression.iterate_denominator line 33
  5. theorem OAI.MetricKMedian.IntegerLaw.BinaryCompression.input_bounds line 47
  6. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.height line 70
  7. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.heightPolynomial line 71
  8. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.statePolynomial line 72
  9. theorem OAI.MetricKMedian.IntegerLaw.BinaryCompression.heightPolynomial_eval line 74
  10. theorem OAI.MetricKMedian.IntegerLaw.BinaryCompression.statePolynomial_eval line 77
  11. theorem OAI.MetricKMedian.IntegerLaw.BinaryCompression.Input.encode_length line 81
  12. theorem OAI.MetricKMedian.IntegerLaw.BinaryCompression.size_arithmetic line 87
  13. theorem OAI.MetricKMedian.IntegerLaw.BinaryCompression.state_size line 92
  14. theorem OAI.MetricKMedian.IntegerLaw.BinaryCompression.compressSteps_eq_iterate line 120