OAI/Combinatorics/UniformKServer/LazyMarkov.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Strongly-lazy metric serving from finite private virtual states. The exact old and new marginals, legal actions, and potential charge are all explicit.

  1. structure OAI.UniformKServer.LazyMarkov.Input line 17
  2. def OAI.UniformKServer.LazyMarkov.Input.model line 24
  3. def OAI.UniformKServer.LazyMarkov.Input.potential line 29
  4. def OAI.UniformKServer.LazyMarkov.Input.transport line 32
  5. def OAI.UniformKServer.LazyMarkov.Input.charge line 36
  6. theorem OAI.UniformKServer.LazyMarkov.Input.marginal_next line 40
  7. theorem OAI.UniformKServer.LazyMarkov.Input.legal line 48
  8. theorem OAI.UniformKServer.LazyMarkov.Input.step line 52
  9. theorem OAI.UniformKServer.LazyMarkov.Input.initial_marginal line 83
  10. theorem OAI.UniformKServer.LazyMarkov.Input.initial_potential line 89