OAI/Combinatorics/UniformKServer/StarBudget.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Uniform-in-law coarse charges of the actual input. In particular a parent refresh pays for the entire old and new star without a factor of ell.

  1. theorem OAI.UniformKServer.StarBudget.total_held_parent line 18
  2. theorem OAI.UniformKServer.StarBudget.total_held_reference line 28
  3. theorem OAI.UniformKServer.StarBudget.parent_step line 39
  4. theorem OAI.UniformKServer.StarBudget.parent_path_budget line 51
  5. theorem OAI.UniformKServer.StarBudget.parent_budget line 60
  6. theorem OAI.UniformKServer.StarBudget.size_budget line 74