OAI/Combinatorics/KMedian/Programs/DependentSparseProgram.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedian.SparseIntegerLaw.DependentProgram.Bundle line 13
  2. def OAI.MetricKMedian.SparseIntegerLaw.DependentProgram.Bundle.raw line 19
  3. def OAI.MetricKMedian.SparseIntegerLaw.DependentProgram.Bundle.encode line 21
  4. def OAI.MetricKMedian.SparseIntegerLaw.DependentProgram.Bundle.branch line 23
  5. def OAI.MetricKMedian.SparseIntegerLaw.DependentProgram.Bundle.compress line 26
  6. def OAI.MetricKMedian.SparseIntegerLaw.DependentProgram.Bundle.compressionInput line 28
  7. theorem OAI.MetricKMedian.SparseIntegerLaw.DependentProgram.trim_view line 32
  8. def OAI.MetricKMedian.SparseIntegerLaw.DependentProgram.contextProgram line 39
  9. def OAI.MetricKMedian.SparseIntegerLaw.DependentProgram.statesProgram line 41
  10. def OAI.MetricKMedian.SparseIntegerLaw.DependentProgram.lawProgram line 44
  11. def OAI.MetricKMedian.SparseIntegerLaw.DependentProgram.compressionInputProgram line 48
  12. def OAI.MetricKMedian.SparseIntegerLaw.DependentProgram.compressProgram line 64
  13. theorem OAI.MetricKMedian.SparseIntegerLaw.DependentProgram.raw_branch line 81
  14. def OAI.MetricKMedian.SparseIntegerLaw.DependentProgram.branchProgram line 97