OAI/Analysis/CircleDomains/Modulus/InterleavedCollarCost.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Gluing retained fragments and genuine short joining arcs into one allowed collar path, with the sum of their actual costs.

  1. abbrev OAI.CircleDomainRigidity.TaggedPhysicalPath line 19
  2. def OAI.CircleDomainRigidity.physicalTollCost line 22
  3. theorem OAI.CircleDomainRigidity.exists_allowed_interleaved_collar line 26