OAI/Combinatorics/UniformKServer/EpochAlphaJump.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual held-size epoch jump is charged to sparse size changes, a side-reference refresh, or a wholesale epoch. All primitives are evaluated at the common-core prepared state, including the zero-input boundary.

  1. theorem OAI.UniformKServer.EpochAlphaJump.regular line 19
  2. theorem OAI.UniformKServer.EpochAlphaJump.marked line 34
  3. theorem OAI.UniformKServer.EpochAlphaJump.scale_bound line 62
  4. theorem OAI.UniformKServer.EpochAlphaJump.total_upper line 73
  5. theorem OAI.UniformKServer.EpochAlphaJump.reference_upper line 80
  6. theorem OAI.UniformKServer.EpochAlphaJump.side_input line 86
  7. theorem OAI.UniformKServer.EpochAlphaJump.marked_sized line 99