OAI/Analysis/CircleDomains/Uniformization/RiemannDiskSeed.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A normalized nonconstant disk embedding from the existing square-root construction. This is the initial competitor for extremal circularization.

  1. structure OAI.CircleDomainRigidity.NormalizedDiskEmbedding line 17
  2. lemma OAI.CircleDomainRigidity.exists_normalized_disk_embedding line 23
  3. lemma OAI.CircleDomainRigidity.normalized_disk_derivative_bound line 54