OAI/Combinatorics/UniformKServer/LevelTierEdits.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Actual full-tape one-tier edit estimates. Prefix and suffix may depend arbitrarily on the tape; the noncoverage ledger is not conditioned on either.

  1. def OAI.UniformKServer.LevelMap.Data.tierTrigger line 22
  2. def OAI.UniformKServer.LevelMap.Data.tierEdit line 26
  3. theorem OAI.UniformKServer.LevelMap.Data.tierEdit_frozen line 30
  4. theorem OAI.UniformKServer.LevelMap.Data.tier_expect_bound line 42
  5. theorem OAI.UniformKServer.LevelMap.Data.tier_stationary line 59
  6. theorem OAI.UniformKServer.LevelMap.Data.tier_mover line 83