OAI/Combinatorics/KMedianRecovery/Sampling/SamplingStateMachine.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingState.encode line 12
  2. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingState.optionBits line 13
  3. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySamplingState.arrays_eq line 14
  4. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingState.remove line 21
  5. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingState.remove_computes line 23
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySamplingState.remove_pair line 27
  7. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingState.add line 34
  8. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingState.add_computes line 36
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySamplingState.add_pair line 38
  10. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingState.keep line 42
  11. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingState.keep_computes line 45
  12. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingState.retain line 50
  13. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingState.retain_computes line 51
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySamplingState.retain_pair line 53
  15. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingState.context line 61
  16. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingState.referenceInput line 63
  17. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingState.referenceInput_computes line 64
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySamplingState.referenceInput_pair line 66
  19. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingState.reference line 77
  20. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingState.reference_computes line 78
  21. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySamplingState.reference_pair line 79
  22. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingOracle.pack line 91
  23. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingOracle.row line 93
  24. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingOracle.row_computes line 94
  25. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySamplingOracle.row_pair line 96
  26. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingOracle.reference line 99
  27. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingOracle.reference_computes line 100
  28. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySamplingOracle.reference_pair line 102
  29. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingOracle.weight line 108
  30. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingOracle.weight_computes line 109
  31. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySamplingOracle.weight_pair line 111
  32. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingOracle.weights line 115
  33. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingOracle.weights_computes line 116
  34. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySamplingOracle.weights_pack line 120
  35. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingOracle.total line 126
  36. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingOracle.total_computes line 127
  37. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySamplingOracle.total_pack line 129