OAI/Combinatorics/KMedian/Compression/CompressionListStep.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.IntegerLaw.BinaryCompression.Row line 14
  2. abbrev OAI.MetricKMedian.IntegerLaw.BinaryCompression.Rows line 15
  3. abbrev OAI.MetricKMedian.IntegerLaw.BinaryCompression.er line 16
  4. abbrev OAI.MetricKMedian.IntegerLaw.BinaryCompression.em line 17
  5. abbrev OAI.MetricKMedian.IntegerLaw.BinaryCompression.es line 18
  6. abbrev OAI.MetricKMedian.IntegerLaw.BinaryCompression.LawData line 19
  7. abbrev OAI.MetricKMedian.IntegerLaw.BinaryCompression.el line 20
  8. abbrev OAI.MetricKMedian.IntegerLaw.BinaryCompression.Data line 21
  9. abbrev OAI.MetricKMedian.IntegerLaw.BinaryCompression.ed line 22
  10. structure OAI.MetricKMedian.IntegerLaw.BinaryCompression.Input line 24
  11. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.Input.lawData line 30
  12. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.Input.features line 31
  13. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.Input.raw line 32
  14. abbrev OAI.MetricKMedian.IntegerLaw.BinaryCompression.Input.encode line 33
  15. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.Input.large line 35
  16. instance OAI.MetricKMedian.IntegerLaw.BinaryCompression.(instance at line 36) line 36
  17. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.Input.nextLaw line 37
  18. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.Input.step line 40
  19. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.Input.affine line 41
  20. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.rawProgram line 43
  21. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.lawProgram line 45
  22. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.featuresProgram line 47
  23. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.dimProgram line 49
  24. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.largeProgram line 52
  25. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.dummy line 69
  26. theorem OAI.MetricKMedian.IntegerLaw.BinaryCompression.dummy_large line 70
  27. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.productiveProgram line 74
  28. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.nextLawProgram line 89
  29. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.stepProgram line 98