OAI/Combinatorics/UniformKServer/MarkovFlow.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Eliminate a finite private state by its exact configuration/action flows. No private state or future observation is exposed in the resulting rows.

  1. structure OAI.UniformKServer.MarkovFlow.Model line 16
  2. def OAI.UniformKServer.MarkovFlow.Model.successor line 24
  3. def OAI.UniformKServer.MarkovFlow.Model.joint line 27
  4. def OAI.UniformKServer.MarkovFlow.Model.advance line 30
  5. def OAI.UniformKServer.MarkovFlow.Model.evolve line 33
  6. def OAI.UniformKServer.MarkovFlow.Model.process line 37
  7. theorem OAI.UniformKServer.MarkovFlow.Model.evolve_append line 39
  8. theorem OAI.UniformKServer.MarkovFlow.Model.process_snoc line 47
  9. theorem OAI.UniformKServer.MarkovFlow.Model.joint_first line 52
  10. theorem OAI.UniformKServer.MarkovFlow.Model.advance_expect line 57
  11. def OAI.UniformKServer.MarkovFlow.Model.actions line 63
  12. def OAI.UniformKServer.MarkovFlow.Model.flow line 66
  13. theorem OAI.UniformKServer.MarkovFlow.Model.sum_row line 70
  14. theorem OAI.UniformKServer.MarkovFlow.Model.action_cost line 82
  15. theorem OAI.UniformKServer.MarkovFlow.Model.sum_inflow line 88
  16. theorem OAI.UniformKServer.MarkovFlow.Model.action_support line 101
  17. theorem OAI.UniformKServer.MarkovFlow.Model.valid line 115