OAI/Analysis/CircleDomains/Sobolev/LocalCoordinateMetric.lean

Metric selection for coordinates defined near a compact surface piece

Only smoothness on an open neighborhood of the retained compact piece is required. A smooth cutoff extends the coordinates for the metric-selection argument, and local agreement identifies the resulting metric energy with the actual original coordinate differentials on that piece.