OAI/Combinatorics/KMedianRecovery/Sampling/SamplerResources.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Loop.runPack line 11
  2. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Loop.config_height line 13
  3. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Loop.runPack_bounds line 29
  4. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Loop.capPoly line 40
  5. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Loop.cap line 41
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Loop.length_cap line 42
  7. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Loop.fold_length_cap line 52
  8. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Loop.initial line 70
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Loop.initial_eq line 71
  10. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Loop.fixedContext line 74
  11. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Loop.fixedContext_computes line 75
  12. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Loop.run line 76
  13. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Loop.run_computes line 78
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Loop.run_pack line 81
  15. def OAI.MetricKMedianRecovery.BitMachine.BinarySeed.rows line 101
  16. def OAI.MetricKMedianRecovery.BitMachine.BinarySeed.rows_computes line 103
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySeed.rows_tensor line 106