OAI/Analysis/CircleDomains/Uniformization/HurwitzZeroFreeProof.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Discharge the zero-free Hurwitz input. A positive lower bound on a circle bounds the reciprocals inside by maximum modulus. Isolated zeros and the analytic identity principle then give the connected-domain form.

  1. theorem OAI.CircleDomainRigidity.nonzero_limit_center_of_nonzero_circle line 15
  2. theorem OAI.CircleDomainRigidity.hurwitzZeroFreeLimit line 53