OAI/Combinatorics/KMedianRecovery/Machines/LoopMachine.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledLoop.pack line 11
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledLoop.input line 14
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledLoop.input_computes line 16
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledLoop.next line 23
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledLoop.next_computes line 25
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledLoop.step line 39
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledLoop.step_computes line 41
  8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledLoop.step_pack line 48
  9. lemma OAI.MetricKMedianRecovery.RationalHeight.Height.le_pow line 88
  10. lemma OAI.MetricKMedianRecovery.RationalHeight.Height.ceil_le_pow line 96
  11. lemma OAI.MetricKMedianRecovery.RationalHeight.Height.clog_ceil line 98
  12. lemma OAI.MetricKMedianRecovery.CanonicalLengthSearch.heightBudget_le line 103
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.bound_mono line 111
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.boundPoly line 115
  15. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.boundPoly_eval line 121