OAI/Analysis/CircleDomains/Uniformization/ModelUniformBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform omitted-set and working-disk bounds for the actual compact scalar models. The constants depend on the source exterior radius alone.

  1. theorem OAI.CircleDomainRigidity.CompactScalarModel.uniform_omitted_and_image_bound line 14