OAI/Analysis/CircleDomains/Uniformization/SmoothMetricPlaneModel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A principally normalized smooth plane model for the actual metric. The finite-point metric equations are derived from the constructed coefficient.

  1. lemma OAI.CircleDomainRigidity.sphereLocalMap_onePointCongr_coe line 15
  2. lemma OAI.CircleDomainRigidity.smooth_metric_plane_model line 20