OAI/Analysis/CircleDomains/Topology/PeriodicCircleDescent.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A smooth period-one plane curve descends smoothly to the geometric unit circle. The proof uses actual local logarithmic branches.

  1. lemma OAI.CircleDomainRigidity.toCircle_normalizedArgument line 14
  2. lemma OAI.CircleDomainRigidity.normalizedArgument_circleExp line 21
  3. lemma OAI.CircleDomainRigidity.normalizedArgument_injective_circle line 26
  4. def OAI.CircleDomainRigidity.periodicCircleDescent line 32
  5. lemma OAI.CircleDomainRigidity.periodicCircleDescent_exp line 35
  6. lemma OAI.CircleDomainRigidity.periodicCircleDescent_smooth line 39
  7. lemma OAI.CircleDomainRigidity.periodicCircleDescent_injective line 54
  8. lemma OAI.CircleDomainRigidity.periodicCircleDescent_range line 68