OAI/Combinatorics/UniformKServer/PartitionLevel.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Instantiation of the level construction from the true post-request GeometricMass.mass. Tier qualifications are precisely the source exponential GeometricMass.mass test.

  1. structure OAI.UniformKServer.PartitionLevel.Input line 21
  2. def OAI.UniformKServer.PartitionLevel.Input.height line 38
  3. def OAI.UniformKServer.PartitionLevel.Input.localLog line 39
  4. def OAI.UniformKServer.PartitionLevel.Input.data line 42
  5. def OAI.UniformKServer.PartitionLevel.Input.order line 54
  6. theorem OAI.UniformKServer.PartitionLevel.Input.inner_one line 56
  7. theorem OAI.UniformKServer.PartitionLevel.Input.outer_pos line 60
  8. theorem OAI.UniformKServer.PartitionLevel.Input.localLog_nonneg line 65
  9. theorem OAI.UniformKServer.PartitionLevel.Input.localLog_bound line 72
  10. theorem OAI.UniformKServer.PartitionLevel.Input.qualification line 81
  11. def OAI.UniformKServer.PartitionLevel.Input.cutoff line 90
  12. theorem OAI.UniformKServer.PartitionLevel.Input.cutoff_le line 92
  13. theorem OAI.UniformKServer.PartitionLevel.Input.prefix_exists line 95
  14. theorem OAI.UniformKServer.PartitionLevel.Input.prefix_sum line 105