OAI/Combinatorics/UniformKServer/PilotScales.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.UniformKServer.PilotScales.scale_logarithms line 9
  2. theorem OAI.UniformKServer.PilotScales.capped_log line 82
  3. theorem OAI.UniformKServer.PilotScales.shell_sum line 97
  4. def OAI.UniformKServer.PilotScales.increment line 121

    Source documentation

    Relative increments of positive monotone masses have only logarithmic total.

    def increment (m : ℕ → ℝ) (i : ℕ) : ℝ :=
…
  5. theorem OAI.UniformKServer.PilotScales.increment_nonneg line 124
  6. theorem OAI.UniformKServer.PilotScales.relative_increment line 131
  7. theorem OAI.UniformKServer.PilotScales.increment_sum line 139
  8. def OAI.UniformKServer.PilotScales.convolution line 153
  9. theorem OAI.UniformKServer.PilotScales.geometric_bound line 156
  10. theorem OAI.UniformKServer.PilotScales.convolution_pointwise line 166
  11. theorem OAI.UniformKServer.PilotScales.convolution_total line 182
  12. theorem OAI.UniformKServer.PilotScales.convolution_succ line 203
  13. def OAI.UniformKServer.PilotScales.mass line 218
  14. def OAI.UniformKServer.PilotScales.moment line 221
  15. def OAI.UniformKServer.PilotScales.radius line 224
  16. theorem OAI.UniformKServer.PilotScales.mass_nonneg line 226
  17. theorem OAI.UniformKServer.PilotScales.mass_mono line 234
  18. theorem OAI.UniformKServer.PilotScales.moment_bound line 245
  19. theorem OAI.UniformKServer.PilotScales.moment_shell line 255
  20. theorem OAI.UniformKServer.PilotScales.radius_pos line 270
  21. theorem OAI.UniformKServer.PilotScales.radius_mono line 273
  22. theorem OAI.UniformKServer.PilotScales.moment_convolution line 282
  23. theorem OAI.UniformKServer.PilotScales.pilot_moment_sum line 309