OAI/Combinatorics/UniformKServer/LazyFinance.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A literal labeled strongly-lazy simulation. Fixed-label mismatch suffices for the movement telescope; no forbidden move or future request is used.

  1. def OAI.UniformKServer.LazyFinance.mismatch line 16
  2. theorem OAI.UniformKServer.LazyFinance.mismatch_nonneg line 18
  3. theorem OAI.UniformKServer.LazyFinance.mismatch_triangle line 20
  4. def OAI.UniformKServer.LazyFinance.choice line 25
  5. theorem OAI.UniformKServer.LazyFinance.lazy line 29
  6. theorem OAI.UniformKServer.LazyFinance.at_request line 34
  7. theorem OAI.UniformKServer.LazyFinance.step line 46
  8. theorem OAI.UniformKServer.LazyFinance.initial_bound line 61