OAI/Analysis/CircleDomains/Modulus/CountablePhysicalLength.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite physical length of the actual collar concatenation. The bound is proved before applying allowed-path stability.

  1. theorem OAI.CircleDomainRigidity.physicalDyadicLength_collarPieces_le line 17
  2. theorem OAI.CircleDomainRigidity.physicalDomainLength_collarPieces_le line 38
  3. def OAI.CircleDomainRigidity.finitePhysicalCollarConcatenation line 65