OAI/Combinatorics/UniformKServer/TreeRankData.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Fixed-tree finite count laws. Internal counts are exactly sums of child counts; leaves keep their own counts. All operations depend on the observed finite filtration only.

  1. structure OAI.UniformKServer.TreeRankData.Data line 19
  2. def OAI.UniformKServer.TreeRankData.single line 29
  3. def OAI.UniformKServer.TreeRankData.star line 38
  4. def OAI.UniformKServer.TreeRankData.input line 53
  5. def OAI.UniformKServer.TreeRankData.beta line 54
  6. def OAI.UniformKServer.TreeRankData.lower line 55
  7. theorem OAI.UniformKServer.TreeRankData.child_input line 58
  8. theorem OAI.UniformKServer.TreeRankData.child_lower line 61
  9. theorem OAI.UniformKServer.TreeRankData.parent_input line 64
  10. theorem OAI.UniformKServer.TreeRankData.parent_lower line 71
  11. theorem OAI.UniformKServer.TreeRankData.allowed line 75
  12. theorem OAI.UniformKServer.TreeRankData.lower_nonneg line 78
  13. theorem OAI.UniformKServer.TreeRankData.lower_bound line 83
  14. theorem OAI.UniformKServer.TreeRankData.empty_parent line 90
  15. theorem OAI.UniformKServer.TreeRankData.parent_le_lower line 103