OAI/Analysis/CircleDomains/Selection/SparseBaseCodes.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Injective retagging preserves the complete base-code conditions and cost finiteness. It is a Borel operation on the actual code space.

  1. theorem OAI.CircleDomainRigidity.allowedTaggedPath_sparse line 19
  2. theorem OAI.CircleDomainRigidity.endpointCode_sparse line 29
  3. def OAI.CircleDomainRigidity.sparseBaseCode line 35
  4. theorem OAI.CircleDomainRigidity.measurable_sparseBaseCode line 40
  5. theorem OAI.CircleDomainRigidity.baseCodeOccupation_sparse line 50
  6. theorem OAI.CircleDomainRigidity.pathCostMeasure_sparse_finite_iff line 55
  7. def OAI.CircleDomainRigidity.sparseFiniteCostCode line 64
  8. theorem OAI.CircleDomainRigidity.measurable_sparseFiniteCostCode line 70