OAI/Analysis/CircleDomains/Selection/CircuitReparametrization.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Changing the starting point or direction of a periodic circuit preserves its image and the absolute value of its one-form integral.

  1. theorem OAI.CircleDomainRigidity.periodic_eq_of_close line 16
  2. theorem OAI.CircleDomainRigidity.periodic_shift_injOn line 35
  3. theorem OAI.CircleDomainRigidity.periodic_shift line 44
  4. theorem OAI.CircleDomainRigidity.periodic_reverse line 50
  5. theorem OAI.CircleDomainRigidity.deriv_periodic line 57
  6. theorem OAI.CircleDomainRigidity.planarFormIntegral_shift line 63
  7. theorem OAI.CircleDomainRigidity.planarFormIntegral_reverse line 78
  8. theorem OAI.CircleDomainRigidity.circleFormIntegral_shift line 95
  9. theorem OAI.CircleDomainRigidity.circleFormIntegral_reverse line 100