OAI/Combinatorics/UniformKServer/HeavyLabelParks.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The actual held heavy-key denominator and nearby-park geometry.

  1. theorem OAI.UniformKServer.PartitionTree.ball_mass line 18
  2. def OAI.UniformKServer.PartitionTree.heavyState line 22
  3. def OAI.UniformKServer.PartitionTree.nearHeavy line 26
  4. theorem OAI.UniformKServer.PartitionTree.label_individual line 31
  5. theorem OAI.UniformKServer.PartitionTree.heavy_inner_subset line 43
  6. theorem OAI.UniformKServer.PartitionTree.heavy_denominator line 53
  7. theorem OAI.UniformKServer.PartitionTree.label_anchor line 69
  8. theorem OAI.UniformKServer.PartitionTree.near_park_witness line 84