OAI/Analysis/CircleDomains/Rigidity/CountableTraceEnumeration.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Enumerate a countable family without repetitions. Missing natural codes carry zero radii, so empty and finite families use the same bounds.

  1. def OAI.CircleDomainRigidity.traceEnumeration line 11
  2. theorem OAI.CircleDomainRigidity.traceEnumeration_encode line 14
  3. theorem OAI.CircleDomainRigidity.traceEnumeration_missing line 18
  4. theorem OAI.CircleDomainRigidity.traceEnumeration_map line 22
  5. theorem OAI.CircleDomainRigidity.traceEnumeration_nonneg line 30
  6. theorem OAI.CircleDomainRigidity.traceEnumeration_summable_sq line 39
  7. theorem OAI.CircleDomainRigidity.traceEnumeration_ball_disjoint line 45