OAI/Analysis/CircleDomains/Sobolev/ScalarImageEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Conformal invariance gives the exact original energy on the open image for the corresponding smooth scalar.

  1. theorem OAI.CircleDomainRigidity.RetainedRealCircleModel.imageScalar_energy line 20