OAI/Combinatorics/UniformKServer/RankData.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Exact size rank and held core flags from companion §03.

  1. def OAI.UniformKServer.RankData.sizeRank line 15
  2. theorem OAI.UniformKServer.RankData.sizeRank_nonneg line 17
  3. theorem OAI.UniformKServer.RankData.sizeRank_zero line 21
  4. theorem OAI.UniformKServer.RankData.sizeRank_one line 22
  5. theorem OAI.UniformKServer.RankData.sizeRank_convex line 24
  6. theorem OAI.UniformKServer.RankData.sizeRank_sqrt line 37
  7. theorem OAI.UniformKServer.RankData.sizeRank_sqrt_lipschitz line 41
  8. theorem OAI.UniformKServer.RankData.sizeRank_le_complement line 51
  9. theorem OAI.UniformKServer.RankData.sizeRank_at_cutoff line 61
  10. def OAI.UniformKServer.RankData.core line 70
  11. theorem OAI.UniformKServer.RankData.core_small line 73
  12. theorem OAI.UniformKServer.RankData.noncore_large line 81
  13. theorem OAI.UniformKServer.RankData.small_core line 89
  14. theorem OAI.UniformKServer.RankData.core_refresh line 98
  15. def OAI.UniformKServer.RankData.coreCount line 109
  16. def OAI.UniformKServer.RankData.coreMass line 110
  17. def OAI.UniformKServer.RankData.flex line 111
  18. def OAI.UniformKServer.RankData.totalRank line 113
  19. def OAI.UniformKServer.RankData.totalSize line 114
  20. theorem OAI.UniformKServer.RankData.core_mass_bounds line 116
  21. theorem OAI.UniformKServer.RankData.core_decomposition line 125
  22. theorem OAI.UniformKServer.RankData.rank_size_domination line 136
  23. theorem OAI.UniformKServer.RankData.core_flex_domination line 144
  24. theorem OAI.UniformKServer.RankData.inactive_ranks line 163