OAI/Analysis/CircleDomains/Selection/RegularLevelPeriodicParametrization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Actual smooth embedded circles parametrizing the components of a compact regular planar level. The parametrization comes from its tangent flow.

  1. lemma OAI.CircleDomainRigidity.CompactRegularLevelFlow.exists_regular_period_one line 13
  2. lemma OAI.CircleDomainRigidity.exists_smooth_circle_of_compact_regular_level line 54