OAI/Combinatorics/KMedianRecovery/Machines/NormalizationMachine.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalization.pack line 12
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalization.count line 14
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalization.count_computes line 15
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalization.mesh line 16
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalization.mesh_computes line 18
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalization.capArgument line 20
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalization.capArgument_computes line 22
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalization.cap line 25
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalization.cap_computes line 27
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalization.roundingInput line 30
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalization.roundingInput_computes line 32
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalization.run line 38
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryNormalization.run_computes line 39
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryNormalization.count_pack line 40
  15. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryNormalization.mesh_pack line 43
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryNormalization.cap_pack line 48
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryNormalization.roundingInput_pack line 53
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryNormalization.run_pack line 59