OAI/Combinatorics/UniformKServer/TreeDistribution.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Initial and next rounded configurations live in one fixed finite alphabet; conditional extension states are eliminated by exact finite push-forward.

  1. def OAI.UniformKServer.TreeRounding.Law.finiteLaw line 20
  2. def OAI.UniformKServer.TreeRounding.Distribution.supportLaw line 22
  3. theorem OAI.UniformKServer.TreeRounding.Distribution.support_mean line 29
  4. theorem OAI.UniformKServer.TreeRounding.map_positive line 33
  5. theorem OAI.UniformKServer.TreeRounding.distribution_initial line 44
  6. def OAI.UniformKServer.TreeRounding.stateDistance line 59
  7. structure OAI.UniformKServer.TreeRounding.Coupling line 62
  8. theorem OAI.UniformKServer.TreeRounding.distribution_step line 68