OAI/Combinatorics/UniformKServer/TreeAllocationMovement.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Global allocation movement with an absolute, degree/depth independent coefficient. The finite additive term is displayed as a function of the fixed tree, its radii and k, not of a law or a horizon.

  1. def OAI.UniformKServer.TreeAllocationMovement.integral line 19
  2. theorem OAI.UniformKServer.TreeAllocationMovement.integral_sum line 22
  3. theorem OAI.UniformKServer.TreeAllocationMovement.integral_nonneg line 26
  4. def OAI.UniformKServer.TreeAllocationMovement.nodeMove line 29
  5. def OAI.UniformKServer.TreeAllocationMovement.hiddenMove line 32
  6. def OAI.UniformKServer.TreeAllocationMovement.movement line 35
  7. def OAI.UniformKServer.TreeAllocationMovement.hiddenCost line 38
  8. def OAI.UniformKServer.TreeAllocationMovement.allowance line 41
  9. theorem OAI.UniformKServer.TreeAllocationMovement.local_movement line 44
  10. theorem OAI.UniformKServer.TreeAllocationMovement.node_nonneg line 59
  11. theorem OAI.UniformKServer.TreeAllocationMovement.root_move line 62
  12. theorem OAI.UniformKServer.TreeAllocationMovement.movement_nonneg line 65
  13. theorem OAI.UniformKServer.TreeAllocationMovement.global_movement line 73