OAI/Combinatorics/UniformKServer/TierRadius.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

One universal finite radius seed covers every possible input-driven center, so the seed law is independent of the hidden input.

  1. def OAI.UniformKServer.TierRadius.probability line 18
  2. abbrev OAI.UniformKServer.TierRadius.Sample line 19
  3. def OAI.UniformKServer.TierRadius.law line 20
  4. def OAI.UniformKServer.TierRadius.entry line 22
  5. theorem OAI.UniformKServer.TierRadius.cover_inner line 33
  6. theorem OAI.UniformKServer.TierRadius.cover_outer line 44
  7. theorem OAI.UniformKServer.TierRadius.local_bound line 53
  8. theorem OAI.UniformKServer.TierRadius.hit_zero line 76