OAI/Analysis/CircleDomains/Modulus/PhysicalLengthRestriction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The global time measure restricts to ordinary physical arclength on every compact interval contained in the open physical-domain times.

  1. theorem OAI.CircleDomainRigidity.physicalSubpath_length_inter line 20
  2. theorem OAI.CircleDomainRigidity.physicalDyadicTimeLength_restrict line 36
  3. theorem OAI.CircleDomainRigidity.physicalStageTimeLength_restrict line 67
  4. theorem OAI.CircleDomainRigidity.physicalTimeLength_restrict_compact line 89