OAI/Analysis/CircleDomains/Selection/DelayedBaseCodes.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

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_delay line 19
  2. theorem OAI.CircleDomainRigidity.endpointCode_delay line 29
  3. def OAI.CircleDomainRigidity.delayBaseCode line 35
  4. theorem OAI.CircleDomainRigidity.measurable_delayBaseCode line 40
  5. theorem OAI.CircleDomainRigidity.baseCodeOccupation_delay line 50
  6. theorem OAI.CircleDomainRigidity.pathCostMeasure_delay_finite_iff line 55
  7. def OAI.CircleDomainRigidity.delayFiniteCostCode line 64
  8. theorem OAI.CircleDomainRigidity.measurable_delayFiniteCostCode line 70