OAI/Analysis/CircleDomains/Selection/RealCoordinateFamily.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Assemble the actual bounded physical coordinates and their square-summable band budgets into the coordinate family consumed by finite transfer.

  1. theorem OAI.CircleDomainRigidity.boundary_width_nonneg line 22
  2. def OAI.CircleDomainRigidity.realCoordinateDataFamily line 33
  3. def OAI.CircleDomainRigidity.realCoordinateFamily line 114
  4. theorem OAI.CircleDomainRigidity.realCoordinateFamily_naturalCompatibility line 133