OAI/Combinatorics/KMedianRecovery/Machines/MatchSize.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.capacityPoly line 12
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.capacity line 15
  3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.accBits_bound line 16
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.run line 37
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.run_computes line 38
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.pack line 40
  7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.pack_bounds line 43
  8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryMatch.run_pack line 54
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryRegular.pack line 106
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryRegular.poolInput line 108
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryRegular.poolInput_computes line 109
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryRegular.pool line 111
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryRegular.pool_computes line 112
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryRegular.context line 113
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryRegular.context_computes line 114
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryRegular.state0 line 121
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryRegular.state0_computes line 122
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryRegular.matchInput line 129
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryRegular.matchInput_computes line 130
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryRegular.matched line 131
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryRegular.matched_computes line 132
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryRegular.prunedInput line 133
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryRegular.prunedInput_computes line 134
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryRegular.run line 137
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryRegular.run_computes line 138
  26. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRegular.base_F line 145
  27. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRegular.pool_pack line 149
  28. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRegular.matchInput_pack line 155
  29. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRegular.run_pack line 163