OAI/Analysis/CircleDomains/Selection/PrincipalExteriorGerm.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A holomorphic exterior map tending to the identity has an actual principal Laurent germ. The first two divided differences give the coefficient and the analytic remainder; no Laurent estimate is assumed.

  1. def OAI.CircleDomainRigidity.invertedPrincipalRemainder line 14
  2. theorem OAI.CircleDomainRigidity.invertedPrincipalRemainder_analytic line 17
  3. theorem OAI.CircleDomainRigidity.principal_exterior_expansion line 33
  4. theorem OAI.CircleDomainRigidity.principal_bigO_of_exterior_holomorphic line 56