OAI/Combinatorics/UniformKServer/RoundedState.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A fixed finite state space for the causal rounding kernels. It records only bounded integer subtree counts, not an assumed distribution.

  1. theorem OAI.UniformKServer.TreeRounding.rounded_le line 18
  2. def OAI.UniformKServer.TreeRounding.bounded line 27
  3. abbrev OAI.UniformKServer.TreeRounding.State line 29
  4. def OAI.UniformKServer.TreeRounding.State.value line 33
  5. def OAI.UniformKServer.TreeRounding.State.realization line 35
  6. def OAI.UniformKServer.TreeRounding.stateOf line 38
  7. theorem OAI.UniformKServer.TreeRounding.stateOf_value line 44
  8. theorem OAI.UniformKServer.TreeRounding.stateOf_tuple line 50
  9. structure OAI.UniformKServer.TreeRounding.Distribution line 54