OAI/Combinatorics/KMedianRecovery/Branching/CategoricalSize.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.optionBits_length line 11
  2. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.tableBits_length line 18
  3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.stateBits_length line 32
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.runCapPoly line 38
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.runCap line 39
  6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.stateBits_length_bound line 40
  7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.step_clock_le line 48
  8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.fold_clock_le line 55
  9. lemma OAI.MetricKMedianRecovery.FiniteSampling.adaptiveRun_list line 64
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.runPack line 74
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.initial line 77
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.initial_computes line 79
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.context line 85
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.context_computes line 86
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.run line 88
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.run_computes line 90
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.initial_pack line 93
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.context_pack line 97
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.runPack_dimensions line 100
  20. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.run_pack line 108
  21. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCategorical.run_ofFn line 123