OAI/Analysis/CircleDomains/Uniformization/CircularizationShift.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact restart identities for the deterministic finite circularization.

  1. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.iterate_add line 12
  2. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.stageMap_add line 20
  3. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.cumulativeMap_add line 25
  4. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.cyclicSchedule_cycle_add line 35
  5. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.iterate_cycle_add line 39
  6. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.selectedCenter_cycle_add line 47
  7. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.selectedRadius_cycle_add line 55
  8. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.visitTime_succ line 63