OAI/Analysis/CircleDomains/Selection/ExclusionTolls.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Infinite auxiliary tolls enforce avoidance without changing the cost of the original paths. They are used only inside the collar construction.

  1. def OAI.CircleDomainRigidity.exclusionToll line 17
  2. theorem OAI.CircleDomainRigidity.le_exclusionToll line 20
  3. theorem OAI.CircleDomainRigidity.exclusionToll_eq line 24
  4. theorem OAI.CircleDomainRigidity.timeToll_mono_weight line 28
  5. theorem OAI.CircleDomainRigidity.avoids_of_finite_exclusionToll line 32
  6. theorem OAI.CircleDomainRigidity.physicalTollCost_exclusion line 43
  7. theorem OAI.CircleDomainRigidity.interiorPhysicalTollCost_mono_weight line 51