OAI/Analysis/CircleDomains/Topology/AffineBoundaryTolls.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact dust tolls of an affine path restriction. The preterminal cost corresponds to a half-open old interval, so cut points are never charged twice.

  1. theorem OAI.CircleDomainRigidity.preterminalToll_eq_timeToll line 20
  2. theorem OAI.CircleDomainRigidity.boundaryToll_eq_timeToll line 28
  3. theorem OAI.CircleDomainRigidity.affine_image_preterminal line 34
  4. theorem OAI.CircleDomainRigidity.preterminalToll_affine line 42
  5. theorem OAI.CircleDomainRigidity.boundaryToll_affine line 49
  6. theorem OAI.CircleDomainRigidity.interiorToll_affine line 56
  7. theorem OAI.CircleDomainRigidity.sum_restricted_preterminalToll_le line 66