OAI/Analysis/CircleDomains/Selection/TagDelay.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Moving the same tags to later slots preserves the actual residual times and all admissibility rules. The tuple measure decreases geometrically.

  1. def OAI.CircleDomainRigidity.inactiveTag line 16
  2. def OAI.CircleDomainRigidity.delayTags line 18
  3. theorem OAI.CircleDomainRigidity.delayTags_before line 21
  4. theorem OAI.CircleDomainRigidity.delayTags_add line 24
  5. theorem OAI.CircleDomainRigidity.continuous_delayTags line 28
  6. def OAI.CircleDomainRigidity.delayTaggedPath line 37
  7. theorem OAI.CircleDomainRigidity.continuous_delayTaggedPath line 40
  8. theorem OAI.CircleDomainRigidity.residualTimes_delay line 44
  9. theorem OAI.CircleDomainRigidity.residualImage_delay line 61
  10. theorem OAI.CircleDomainRigidity.inactiveTag_rules line 69
  11. theorem OAI.CircleDomainRigidity.tagRules_delay line 83
  12. theorem OAI.CircleDomainRigidity.residualIncidence_delay line 92
  13. theorem OAI.CircleDomainRigidity.residualToll_delay line 101
  14. theorem OAI.CircleDomainRigidity.residualConstraintFamily_delay line 108