OAI/Combinatorics/UniformKServer/ActualPartitions.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The actual true-posterior partition, on every positive finite hidden law. All inputs are the real post-request counts, not a fitted proxy mass.

  1. structure OAI.UniformKServer.ActualPartitions.Config line 19
  2. def OAI.UniformKServer.ActualPartitions.Config.input line 35
  3. theorem OAI.UniformKServer.ActualPartitions.Config.lifetime_large line 56
  4. theorem OAI.UniformKServer.ActualPartitions.Config.separation line 66
  5. theorem OAI.UniformKServer.ActualPartitions.Config.past_centers line 72
  6. theorem OAI.UniformKServer.ActualPartitions.Config.past_mass line 77
  7. theorem OAI.UniformKServer.ActualPartitions.Config.past_heavy line 82
  8. theorem OAI.UniformKServer.ActualPartitions.Config.past_qualify line 91