OAI/Combinatorics/KMedianRecovery/Sampling/SamplerTraceMachine.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Trace.rows line 10
  2. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Trace.rows_computes line 12
  3. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Trace.input line 15
  4. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Trace.input_computes line 17
  5. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Trace.prefixBits line 20
  6. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Trace.prefixBits_computes line 22
  7. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Trace.atPrefix line 24
  8. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Trace.atPrefix_computes line 26
  9. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Trace.run line 31
  10. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Trace.run_computes line 33
  11. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Trace.pack line 36
  12. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Trace.input_pack line 38
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Trace.atPrefix_pack line 46
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Trace.run_pack line 58