OAI/Combinatorics/KMedianRecovery/Recovery/InitialCorrect.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryInitial.run_pack line 14
  2. def OAI.MetricKMedianRecovery.RationalPhaseFuel.exponent line 97
  3. lemma OAI.MetricKMedianRecovery.RationalPhaseFuel.exponent_le_iff line 99
  4. lemma OAI.MetricKMedianRecovery.RationalPhaseFuel.to_limit line 107
  5. lemma OAI.MetricKMedianRecovery.RationalPhaseFuel.exponent_bound line 110
  6. lemma OAI.MetricKMedianRecovery.RationalPhaseFuel.exists_multiplier line 118
  7. def OAI.MetricKMedianRecovery.RationalPhaseFuel.next line 122
  8. lemma OAI.MetricKMedianRecovery.RationalPhaseFuel.next_min line 124
  9. lemma OAI.MetricKMedianRecovery.RationalPhaseFuel.iterate_next line 130
  10. lemma OAI.MetricKMedianRecovery.RationalHeight.Height.le_bound line 139
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFuel.pack line 156
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFuel.threshold line 158
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFuel.power line 159
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFuel.count line 160
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFuel.threshold_computes line 161
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFuel.power_computes line 163
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFuel.count_computes line 165
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFuel.step line 167
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFuel.step_computes line 170
  20. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFuel.step_pack line 176
  21. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFuel.iterate_pack line 182
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFuel.pack_length line 189
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFuel.coefficient line 194
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFuel.cap line 195
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFuel.fuel line 197
  26. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFuel.iterate_length line 200
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFuel.initial line 212
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFuel.initial_computes line 213
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFuel.iterated line 215
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFuel.iterated_computes line 217
  31. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFuel.iterated_encode line 221
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFuel.run line 237
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFuel.run_computes line 238
  34. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPhaseFuel.run_encode line 242