OAI/Analysis/CircleDomains/Modulus/RestrictedFragmentCosts.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Disjoint restricted original fragments never exceed the original cost. The physical arclength measure has no atoms and the collar cut tolls vanish.

  1. theorem OAI.CircleDomainRigidity.timeToll_Icc_eq_Ioo line 21
  2. theorem OAI.CircleDomainRigidity.physicalTollCost_affine line 32
  3. theorem OAI.CircleDomainRigidity.sum_restricted_physicalTollCost_le line 50