OAI/Analysis/CircleDomains/Sobolev/CircleEnergyChange.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Conformal invariance of the actual circle-coordinate energy

The chain rule identifies the pullback field with the intrinsic circle differential. Thus the change-of-variables formula controls the actual composed coordinate, without a chosen global real lift.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.integral_circleEnergy_change_variables line 20