OAI/Analysis/CircleDomains/Modulus/ReversedPhysicalLength.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Reversing time preserves the actual physical-domain length. Dyadic cells are matched with their reversed indices before summing.

  1. theorem OAI.CircleDomainRigidity.symm_timeClip line 16
  2. theorem OAI.CircleDomainRigidity.symm_dyadicLeft line 25
  3. theorem OAI.CircleDomainRigidity.symm_dyadicRight line 37
  4. theorem OAI.CircleDomainRigidity.pathsInsideOn_reversed_iff line 44
  5. theorem OAI.CircleDomainRigidity.physicalDyadicPath_reversed line 56
  6. theorem OAI.CircleDomainRigidity.variation_reversedPath line 83
  7. theorem OAI.CircleDomainRigidity.physicalDomainLength_reversed line 90