OAI/Analysis/CircleDomains/Modulus/PrincipalNormalization.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Affine principal normalization of a sphere map

The analytic remainder at zero is bounded near zero. After inversion this gives the actual O(1/z) remainder at infinity, rather than only a formal Laurent coefficient calculation.

  1. def OAI.CircleDomainRigidity.IsPrincipalNormalized line 21
  2. theorem OAI.CircleDomainRigidity.affine_normalization_bigO line 25
  3. theorem OAI.CircleDomainRigidity.principal_normalize_at_infty line 45