OAI/Combinatorics/UniformKServer/LabelParks.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Actual fixed-coordinate parks and true posterior sizes of each level key.

  1. def OAI.UniformKServer.PartitionTree.labelVertices line 18
  2. def OAI.UniformKServer.PartitionTree.keyRegion line 22
  3. def OAI.UniformKServer.PartitionTree.labelPark line 26
  4. def OAI.UniformKServer.PartitionTree.labelTracker line 31
  5. theorem OAI.UniformKServer.PartitionTree.keyRegion_measurable line 36
  6. theorem OAI.UniformKServer.PartitionTree.labelTracker_size line 45
  7. theorem OAI.UniformKServer.PartitionTree.labelPark_nonneg line 52
  8. theorem OAI.UniformKServer.PartitionTree.label_region line 57
  9. theorem OAI.UniformKServer.PartitionTree.label_domination line 72
  10. theorem OAI.UniformKServer.PartitionTree.labelPark_measurable line 92