OAI/Combinatorics/KMedianRecovery/Sampling/SamplerUpdateParts.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.input line 12
  2. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.input_computes line 13
  3. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.clientInput line 14
  4. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.clientInput_computes line 15
  5. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.chosen line 16
  6. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.chosen_computes line 18
  7. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.radius line 20
  8. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.radius_computes line 21
  9. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.within line 23
  10. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.within_computes line 26
  11. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.ball line 29
  12. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.ball_computes line 31
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.chosen_pair line 34
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.radius_pair line 42
  15. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.within_pair line 51
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Update.ball_pair line 54