OAI/Combinatorics/UniformKServer/EpochSideCharge.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Prepared side jumps: no parameter drift is charged at unchanged held coordinates. Wholesale jumps use the actual prepared feasibility inequality.

  1. theorem OAI.UniformKServer.EpochSideCharge.whole line 18
  2. theorem OAI.UniformKServer.EpochSideCharge.jump line 33