OAI/Analysis/CircleDomains/Uniformization/RiemannRootCompetitor.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A missing disk value gives a genuine holomorphic square-root competitor; its derivative is computed before the final normalization.

  1. lemma OAI.CircleDomainRigidity.exists_root_disk_competitor line 13