OAI/Combinatorics/UniformKServer/CoarseData.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Persistent size/core elementary trackers, and their actual held active states. Constants and initialization allowances are uniform in the law and horizon. Companion §03, equations active-size-accuracy and coarse-data-budget.

  1. def OAI.UniformKServer.CoarseData.totalDrift line 18
  2. def OAI.UniformKServer.CoarseData.sizeEstimate line 20
  3. theorem OAI.UniformKServer.CoarseData.sizeEstimate_nonneg line 23
  4. theorem OAI.UniformKServer.CoarseData.sizeEstimate_comparison line 27
  5. theorem OAI.UniformKServer.CoarseData.average_sum line 38
  6. theorem OAI.UniformKServer.CoarseData.sizeEstimate_budget line 43
  7. def OAI.UniformKServer.CoarseData.coreChange line 69
  8. theorem OAI.UniformKServer.CoarseData.coreChange_budget line 72
  9. def OAI.UniformKServer.CoarseData.sizeTolerance line 100
  10. def OAI.UniformKServer.CoarseData.cutoff line 101
  11. def OAI.UniformKServer.CoarseData.activeState line 103
  12. def OAI.UniformKServer.CoarseData.heldSize line 106
  13. theorem OAI.UniformKServer.CoarseData.heldSize_nonneg line 109
  14. theorem OAI.UniformKServer.CoarseData.activeState_update line 112
  15. theorem OAI.UniformKServer.CoarseData.active_accuracy line 119
  16. theorem OAI.UniformKServer.CoarseData.inactive_small line 135
  17. theorem OAI.UniformKServer.CoarseData.inactive_zero line 145
  18. theorem OAI.UniformKServer.CoarseData.heldSize_path_budget line 159
  19. theorem OAI.UniformKServer.CoarseData.average_range_sum line 175
  20. theorem OAI.UniformKServer.CoarseData.average_const line 180
  21. theorem OAI.UniformKServer.CoarseData.heldSize_budget line 183
  22. theorem OAI.UniformKServer.CoarseData.sizeEstimate_measurable line 195
  23. theorem OAI.UniformKServer.CoarseData.activeState_measurable line 205