OAI/Combinatorics/UniformKServer/HeavyRadius.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

A finite exact realization of the uniform heavy-ball radius. The same finite signature records membership for every possible center. Thus selecting a center by the input-driven schedule does not alter the radius distribution.

  1. def OAI.UniformKServer.HeavyRadius.probability line 19
  2. theorem OAI.UniformKServer.HeavyRadius.probability_bounds line 22
  3. abbrev OAI.UniformKServer.HeavyRadius.Sample line 25
  4. def OAI.UniformKServer.HeavyRadius.law line 27
  5. def OAI.UniformKServer.HeavyRadius.scalar line 29
  6. theorem OAI.UniformKServer.HeavyRadius.scalar_mem line 32
  7. theorem OAI.UniformKServer.HeavyRadius.signature_eq line 36
  8. def OAI.UniformKServer.HeavyRadius.radius line 40
  9. theorem OAI.UniformKServer.HeavyRadius.radius_bounds line 43
  10. theorem OAI.UniformKServer.HeavyRadius.covers line 50
  11. theorem OAI.UniformKServer.HeavyRadius.probability_lipschitz line 60
  12. theorem OAI.UniformKServer.HeavyRadius.separation line 77