OAI/Analysis/CircleDomains/Selection/SelectedLevelPresentation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Presentations of selected real and mean coordinates, retaining their functions, compact laws, and the data for subsequent code-law bounds.

  1. structure OAI.CircleDomainRigidity.RealCoordinatePresentation line 17
  2. structure OAI.CircleDomainRigidity.MeanCoordinatePresentation line 33
  3. abbrev OAI.CircleDomainRigidity.SelectedLevelPresentation line 66
  4. theorem OAI.CircleDomainRigidity.SelectedLevelPresentation.generic_levels line 75