OAI/Analysis/CircleDomains/Reflection/ReflectedSphereNormalization.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Normalize the pole of the actual conjugated reflection to infinity. The result is an actual plane homeomorphism.

  1. def OAI.CircleDomainRigidity.AnalyticReflectionData.reflectedSphere line 17
  2. lemma OAI.CircleDomainRigidity.AnalyticReflectionData.reflectedSphere_pole line 22
  3. lemma OAI.CircleDomainRigidity.AnalyticReflectionData.reflectedSphere_infty line 33
  4. lemma OAI.CircleDomainRigidity.AnalyticReflectionData.reflectedSphere_coe line 40
  5. def OAI.CircleDomainRigidity.AnalyticReflectionData.poleParameter line 52
  6. lemma OAI.CircleDomainRigidity.AnalyticReflectionData.poleParameter_infty line 55
  7. lemma OAI.CircleDomainRigidity.AnalyticReflectionData.poleParameter_zero line 61
  8. lemma OAI.CircleDomainRigidity.AnalyticReflectionData.poleParameter_coe line 67
  9. lemma OAI.CircleDomainRigidity.AnalyticReflectionData.poleNormalized_fixes_infty line 74
  10. def OAI.CircleDomainRigidity.AnalyticReflectionData.poleNormalized line 79
  11. lemma OAI.CircleDomainRigidity.AnalyticReflectionData.poleNormalized_zero line 83
  12. lemma OAI.CircleDomainRigidity.AnalyticReflectionData.poleNormalized_coe line 89