OAI/Combinatorics/UniformKServer/PartitionScales.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Final-map separation summed over geometric scales. The additive one in the level estimate is charged only at nonheavy scales, not at every scale.

  1. structure OAI.UniformKServer.PartitionScales.Input line 18
  2. def OAI.UniformKServer.PartitionScales.Input.level line 40
  3. def OAI.UniformKServer.PartitionScales.Input.isNonheavy line 55
  4. theorem OAI.UniformKServer.PartitionScales.Input.not_heavy line 58
  5. theorem OAI.UniformKServer.PartitionScales.Input.log_sum line 62
  6. theorem OAI.UniformKServer.PartitionScales.Input.nonheavy_count line 70
  7. def OAI.UniformKServer.PartitionScales.Input.coefficient line 79
  8. theorem OAI.UniformKServer.PartitionScales.Input.separation line 81