OAI/Analysis/CircleDomains/Modulus/NormalizedUniformBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One uniform bound for normalized finite circle models

The exterior coefficient estimate controls a physical circle and the annulus outside it. The compact-exterior separation argument traps all other image points and every omitted point on its bounded side.

  1. theorem OAI.CircleDomainRigidity.normalized_model_uniform_bound line 23