OAI/Combinatorics/KMedianRecovery/Branching/RationalSurrogate.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.contextBits line 12
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.clientValues line 16
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.clientValues_computes line 18
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.redValues line 23
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.redValues_computes line 25
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.clientValues_pack line 30
  7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.redValues_pack line 36
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.surrogateQ line 43
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.surrogateQ_cast line 47
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.surrogate line 54
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.surrogate_computes line 57
  12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.surrogate_pack line 63
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.savingQ line 77
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.savingQ_cast line 80
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.saving line 87
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.saving_computes line 90
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCompletion.saving_pack line 93
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.pack line 107
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.oracleInput line 111
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.oracleInput_computes line 112
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.row line 114
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.row_computes line 115
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.distances line 119
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.distances_computes line 120
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.base line 125
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.base_computes line 126
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.capRow line 128
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.capRow_computes line 129
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.weight line 131
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.weight_computes line 133
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.redRow line 139
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.redRow_computes line 140
  33. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.row_pair line 145
  34. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.distances_pair line 148
  35. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.base_zero line 154
  36. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.base_one line 157
  37. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.capRow_zero line 160
  38. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.capRow_one line 163
  39. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.weight_pair line 166
  40. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.redRow_pair line 170
  41. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.clients line 175
  42. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.clients_computes line 176
  43. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.reds line 181
  44. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.reds_computes line 182
  45. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.run line 187
  46. def OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.run_computes line 188
  47. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBranchRows.run_pack line 190