OAI/Analysis/CircleDomains/Uniformization/LimitConformality.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Conformality of the normalized limit

HurwitzZeroFreeLimit records the zero-free form of the same published Hurwitz theorem already used for injective limits: Ahlfors, Complex Analysis, third edition (1979), Chapter 5, Theorem 2, p. 178. Applied to the derivatives, it gives a nonzero limiting derivative unless the limit is constant. The latter alternative is ruled out on each core.

  1. def OAI.CircleDomainRigidity.HurwitzZeroFreeLimit line 22
  2. theorem OAI.CircleDomainRigidity.finite_part_deriv_ne_zero line 29
  3. theorem OAI.CircleDomainRigidity.deriv_ne_zero_of_holomorphic_limits line 41
  4. theorem OAI.CircleDomainRigidity.deriv_ne_zero_on_exhaustion line 60
  5. theorem OAI.CircleDomainRigidity.isConformalAt_extendAtInfinity_coe line 76
  6. theorem OAI.CircleDomainRigidity.isConformalOn_extendAtInfinity line 84