OAI/Analysis/CircleDomains/Transfer/TransportedRealCoordinates.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Real barrier coordinates on normalized circle models

Real coordinates are transported by the actual smooth inverse. The ordinary real gradient has the same energy as its intrinsic circle differential, so the proved change-of-variables formula applies without discarding the real lift or its values.

  1. theorem OAI.CircleDomainRigidity.transported_real_coordinate line 23
  2. theorem OAI.CircleDomainRigidity.circleGradient_coe_eq_planarGradient line 43
  3. theorem OAI.CircleDomainRigidity.integral_transported_real_coordinate line 51