OAI/Analysis/CircleDomains/Uniformization/SmoothMetricUniformization.lean

Smooth finite metric circle models and their inverses

The smooth version of the same compact uniformization input records that the uniformizing map is a diffeomorphism for the original smooth structure. This is the smooth-isothermal-coordinate conclusion of Jost, Compact Riemann Surfaces, third edition (2006), Theorem 3.11.1, pp. 155--158, followed by Ahlfors, Conformal Invariants (1973), Theorem 10-3, p. 142. Only a smooth metric on the sphere, standard near infinity, is required. The weaker metric-only input follows immediately.