OAI/Combinatorics/UniformKServer/KeySizeTracker.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The unreset affine entropy tracker for each fixed heavy-key slot. Filtering is charged at the old measurable coefficient on every step.

  1. structure OAI.UniformKServer.KeySizeTracker.Input line 18
  2. def OAI.UniformKServer.KeySizeTracker.keep line 33
  3. def OAI.UniformKServer.KeySizeTracker.held line 35
  4. def OAI.UniformKServer.KeySizeTracker.charge line 39
  5. def OAI.UniformKServer.KeySizeTracker.pot line 42
  6. def OAI.UniformKServer.KeySizeTracker.ell line 43
  7. theorem OAI.UniformKServer.KeySizeTracker.held_range line 45
  8. theorem OAI.UniformKServer.KeySizeTracker.comparisons line 50
  9. theorem OAI.UniformKServer.KeySizeTracker.held_measurable line 60
  10. theorem OAI.UniformKServer.KeySizeTracker.slope_bound line 69
  11. theorem OAI.UniformKServer.KeySizeTracker.potential_bound line 78
  12. theorem OAI.UniformKServer.KeySizeTracker.step_release line 93
  13. theorem OAI.UniformKServer.KeySizeTracker.potential_step line 101
  14. theorem OAI.UniformKServer.KeySizeTracker.expected_step line 109
  15. theorem OAI.UniformKServer.KeySizeTracker.budget line 131