OAI/Combinatorics/UniformKServer/GeometricMass.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The actual geometric scales and the posterior ball masses at a request. The shift comparison is proved from metric ball inclusion, rather than assumed as an abstract scalar inequality. The scale count is independent of aspect.

  1. def OAI.UniformKServer.GeometricMass.radius line 18
  2. def OAI.UniformKServer.GeometricMass.mass line 19
  3. theorem OAI.UniformKServer.GeometricMass.radius_pos line 21
  4. theorem OAI.UniformKServer.GeometricMass.mass_nonneg line 24
  5. theorem OAI.UniformKServer.GeometricMass.mass_mono line 29
  6. theorem OAI.UniformKServer.GeometricMass.mass_total line 38
  7. theorem OAI.UniformKServer.GeometricMass.mass_center line 44
  8. theorem OAI.UniformKServer.GeometricMass.radius_shift line 50
  9. theorem OAI.UniformKServer.GeometricMass.mass_shift line 57
  10. def OAI.UniformKServer.GeometricMass.logarithm line 65
  11. theorem OAI.UniformKServer.GeometricMass.logarithm_nonneg line 68
  12. theorem OAI.UniformKServer.GeometricMass.log_sum line 77
  13. def OAI.UniformKServer.GeometricMass.nonheavy line 94
  14. theorem OAI.UniformKServer.GeometricMass.nonheavy_log line 97
  15. theorem OAI.UniformKServer.GeometricMass.nonheavy_count line 105