OAI/Analysis/CircleDomains/Selection/MarkedFiniteHitSplit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A finite split for separated hit configurations. Nonsmallness supplies a candidate against the mean configuration measure; its atomic norm bound and the hit-integral identity give the compact-law split.

  1. theorem OAI.CircleDomainRigidity.MarkedHit.exists_finite_hit_configuration_split line 19