OAI/Combinatorics/KMedianRecovery/Encoding/StateBits2.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.heightBound_height line 8
  2. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLabel.encode_length_bound line 13
  3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.labels_length line 25
  4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryFiniteContext.setBits_length line 34
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledState.encode line 48
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledState.labelBound line 52
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledState.bankBound line 53
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledState.historyBound line 54
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledState.bound line 55
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledState.bank_labels line 58
  11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledState.mapped_labels line 73
  12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledState.history_length line 89
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupledState.length_bound line 106