OAI/Combinatorics/UniformKServer/EpochAlphaCharge.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Actual epoch schedule charging of the prepared alpha jump. The zero core mass branch is free; sparse refreshes and wholesale charges are distinct.

  1. def OAI.UniformKServer.EpochAlphaCharge.sizeCharge line 18
  2. def OAI.UniformKServer.EpochAlphaCharge.param line 19
  3. theorem OAI.UniformKServer.EpochAlphaCharge.eta_le line 23
  4. theorem OAI.UniformKServer.EpochAlphaCharge.side_nonneg line 33
  5. theorem OAI.UniformKServer.EpochAlphaCharge.size_nonneg line 41
  6. theorem OAI.UniformKServer.EpochAlphaCharge.sparse line 49
  7. theorem OAI.UniformKServer.EpochAlphaCharge.not_reset_base line 59
  8. theorem OAI.UniformKServer.EpochAlphaCharge.jump line 67