OAI/Analysis/CircleDomains/Modulus/PhysicalLengthCharacterization.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Uniqueness and compact-interval exhaustion of physical-domain arclength. This identifies the dyadic construction with ordinary arclength on all open domain-time components, including paths that revisit points.

  1. theorem OAI.CircleDomainRigidity.measure_eq_of_compact_time_restrictions line 17
  2. theorem OAI.CircleDomainRigidity.physicalTimeLength_unique line 33
  3. theorem OAI.CircleDomainRigidity.physicalTimeLength_compact_mass line 45
  4. theorem OAI.CircleDomainRigidity.physicalTimeLength_exhaustion line 56
  5. theorem OAI.CircleDomainRigidity.physicalTimeLength_component_sum line 68