OAI/Combinatorics/UniformKServer/RoundingChain.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Chosen joint repairs form one adapted Markov chain on a fixed finite state space. The choices use the old distribution and current geometric data only.

  1. theorem OAI.UniformKServer.TreeRounding.Distribution.ext line 17
  2. def OAI.UniformKServer.TreeRounding.chosenStep line 20
  3. theorem OAI.UniformKServer.TreeRounding.chosenStep_bound line 28
  4. structure OAI.UniformKServer.TreeRounding.ChainInput line 38
  5. def OAI.UniformKServer.TreeRounding.ChainInput.step line 57
  6. def OAI.UniformKServer.TreeRounding.ChainInput.distribution line 62
  7. theorem OAI.UniformKServer.TreeRounding.ChainInput.chosen_congr line 66
  8. theorem OAI.UniformKServer.TreeRounding.ChainInput.distribution_causal line 84
  9. def OAI.UniformKServer.TreeRounding.ChainInput.joint line 100
  10. theorem OAI.UniformKServer.TreeRounding.ChainInput.joint_causal line 102
  11. theorem OAI.UniformKServer.TreeRounding.ChainInput.first line 110
  12. theorem OAI.UniformKServer.TreeRounding.ChainInput.second line 114
  13. theorem OAI.UniformKServer.TreeRounding.ChainInput.cost_bound line 118