OAI/Analysis/CircleDomains/Selection/PriorLevelFamily.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The exact weighted-level data consumed by the barrier construction. Both earlier real coordinates and the constructed masked means supply it.

  1. structure OAI.CircleDomainRigidity.PriorLevelFamily line 16
  2. theorem OAI.CircleDomainRigidity.PriorLevelFamily.length line 24
  3. def OAI.CircleDomainRigidity.PriorLevelFamily.ofReal line 33
  4. def OAI.CircleDomainRigidity.PriorLevelFamily.ofMeans line 44