OAI/Combinatorics/UniformKServer/StarRanks.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The actual rank processes of a finite hidden count law on its positive support. No martingale or allocation estimate is part of the data.

  1. structure OAI.UniformKServer.StarRanks.Data line 18
  2. def OAI.UniformKServer.StarRanks.input line 27
  3. def OAI.UniformKServer.StarRanks.parentInput line 31
  4. def OAI.UniformKServer.StarRanks.held line 35
  5. def OAI.UniformKServer.StarRanks.flags line 38
  6. def OAI.UniformKServer.StarRanks.coreInput line 41
  7. theorem OAI.UniformKServer.StarRanks.mass_pos line 44
  8. theorem OAI.UniformKServer.StarRanks.child_bound line 48
  9. theorem OAI.UniformKServer.StarRanks.size_sum line 51
  10. theorem OAI.UniformKServer.StarRanks.rank_sum line 57
  11. theorem OAI.UniformKServer.StarRanks.parent_size_bound line 64
  12. theorem OAI.UniformKServer.StarRanks.held_nonneg line 78
  13. theorem OAI.UniformKServer.StarRanks.held_sum line 81
  14. theorem OAI.UniformKServer.StarRanks.held_min line 92
  15. theorem OAI.UniformKServer.StarRanks.zero_flags line 96
  16. theorem OAI.UniformKServer.StarRanks.core_bound line 100