OAI/Combinatorics/UniformKServer/StarPotentialBounds.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Law- and horizon-independent endpoint bounds for the actual three persistent star potentials.

  1. theorem OAI.UniformKServer.StarPotentialBounds.mass_size line 18
  2. theorem OAI.UniformKServer.StarPotentialBounds.mass_bound line 24
  3. theorem OAI.UniformKServer.StarPotentialBounds.deficit_k line 27
  4. theorem OAI.UniformKServer.StarPotentialBounds.alpha_potential line 31
  5. theorem OAI.UniformKServer.StarPotentialBounds.side_mass line 44
  6. theorem OAI.UniformKServer.StarPotentialBounds.side_potential line 48
  7. theorem OAI.UniformKServer.StarPotentialBounds.switch_potential line 62
  8. theorem OAI.UniformKServer.StarPotentialBounds.switch_wholesale line 69
  9. theorem OAI.UniformKServer.StarPotentialBounds.average_interval line 79