OAI/Combinatorics/KMedianRecovery/Recovery/NormalizeInput.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.P.clients line 11
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.P.clients_computes line 12
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.P.facilities line 13
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.P.facilities_computes line 14
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.P.points line 15
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.P.points_computes line 16
  7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.P.clients_bits line 17
  8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.P.facilities_bits line 19
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.P.points_bits line 21
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.raw line 27
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.raw_computes line 28
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.matrix line 29
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.matrix_computes line 30
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.points line 31
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.points_computes line 32
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.clients line 33
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.clients_computes line 34
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.clientCount line 35
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.clientCount_computes line 36
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.count line 37
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.count_computes line 38
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.plainFacilities line 39
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.plainFacilities_computes line 40
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.facilitiesInput line 41
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.facilitiesInput_computes line 42
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.facilities line 43
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.facilities_computes line 44
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.prep line 45
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.prep_computes line 46
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.rounded line 54
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.rounded_computes line 55
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.twice line 56
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.twice_computes line 57
  34. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.budget line 58
  35. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.budget_computes line 59
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.mesh line 60
  37. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.mesh_computes line 61
  38. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.cap line 62
  39. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.cap_computes line 63
  40. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.run line 64
  41. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.run_computes line 65
  42. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.prep_bits line 76
  43. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.facilities_bits line 81
  44. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryNormalizeInput.run_bits line 84