OAI/Analysis/CircleDomains/Uniformization/PrincipalTaylorCoefficients.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The principal Laurent coefficients are the Taylor coefficients of its inverted remainder. The inverted derivative retains their exact weights.

  1. lemma OAI.CircleDomainRigidity.diskTaylorCoefficient_mul_pow line 14
  2. lemma OAI.CircleDomainRigidity.diskTaylorCoefficient_deriv line 35
  3. lemma OAI.CircleDomainRigidity.invertedPrincipalDerivative_coefficient line 44
  4. lemma OAI.CircleDomainRigidity.principal_laurent_hasSum line 56