OAI/Combinatorics/KMedianRecovery/Branching/CategoricalTable.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.optionBits line 11
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.tableBits line 12
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.choicesBits line 14
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.seedBits line 15
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.drawPack line 16
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.drawItems line 18
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.drawItems_computes line 19
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.drawRow line 21
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.drawRow_computes line 23
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.drawPick line 26
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.drawPick_computes line 29
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.draw line 35
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.draw_computes line 36
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.omitted line 37
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.drawn line 39
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.drawPick_pack line 41
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.drawItems_pack line 47
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.encode_flatten line 51
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.draw_pack line 55
  20. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.drawn_toFinset line 60
  21. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.omitted_update line 66
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.omitted_end line 73
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.advancePack line 77
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.advanceItem line 79
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.advanceItem_computes line 83
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.advance line 89
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.advance_computes line 91
  28. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.advanceItem_pack line 94
  29. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.advance_pack line 106