OAI/Analysis/CircleDomains/Selection/AtomicLevelFiniteness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Square-summable point weights and level-incidence bounds give finite atomic payment on almost every prior level.

  1. theorem OAI.CircleDomainRigidity.ae_finite_atomic_level_payment line 15