OAI/Analysis/CircleDomains/Uniformization/ScalarModelCoefficients.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A common exterior radius bounds the actual coefficient of every model. Consequently the retained model class has near-maximal real coefficients.

  1. theorem OAI.CircleDomainRigidity.finite_differentiable_of_sphere_conformal line 14
  2. theorem OAI.CircleDomainRigidity.CompactScalarModel.coefficient_bound line 28
  3. def OAI.CircleDomainRigidity.CompactScalarModel.coefficientSet line 40
  4. theorem OAI.CircleDomainRigidity.CompactScalarModel.coefficientSet_bddAbove line 43
  5. theorem OAI.CircleDomainRigidity.CompactScalarModel.exists_near_maximal line 50
  6. theorem OAI.CircleDomainRigidity.CompactScalarModel.increment_le_of_near_maximal line 61