OAI/Analysis/CircleDomains/Modulus/LaurentNormalization.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Principal normalization at infinity

A holomorphic germ fixing zero with nonzero derivative has a reciprocal with one simple pole. Two divided differences isolate its pole and constant terms and leave an analytic first-order remainder. This gives the affine normalization used before taking limits of circle models.

  1. theorem OAI.CircleDomainRigidity.analyticAt_dslope_zero line 22
  2. theorem OAI.CircleDomainRigidity.reciprocal_germ_normalization line 27
  3. theorem OAI.CircleDomainRigidity.finiteCoord_sphereInv line 62
  4. theorem OAI.CircleDomainRigidity.analyticAt_infty_chart line 67
  5. theorem OAI.CircleDomainRigidity.affine_normalization_expansion line 94