OAI/Combinatorics/KMedianRecovery/Sampling/SamplerUpdate.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.active line 12
  2. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.active_computes line 13
  3. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.old line 15
  4. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.old_computes line 16
  5. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.remove line 17
  6. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.remove_computes line 19
  7. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.add line 22
  8. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.add_computes line 24
  9. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.run line 27
  10. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.run_computes line 32
  11. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.context_some line 40
  12. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.active_none line 46
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.active_some line 49
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.old_pair line 55
  15. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.remove_pair line 61
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.add_pair line 72
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.optionRadius_eq_nil line 91
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.finset_eq_nil line 95
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.run_pair line 99