OAI/Analysis/CircleDomains/Topology/TransportedCircleCoordinates.lean

Actual pushed-forward circle coordinates

A smooth coordinate on an open part of the source is composed with the actual inverse of a normalized smooth sphere equivalence. Its target domain is the actual image of that source region. It is smooth there, its pullback is locally the original coordinate, and the full Dirichlet change-of-variables formula follows.