OAI/Analysis/CircleDomains/Modulus/CountablePhysicalCost.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact physical time and weighted occupation measures for collar concatenations. Parameter multiplicity is preserved.

  1. theorem OAI.CircleDomainRigidity.physicalTimeLength_collarPieces line 19
  2. theorem OAI.CircleDomainRigidity.physicalDomainLength_collarPieces line 30
  3. theorem OAI.CircleDomainRigidity.physicalCost_collarPieces line 43