OAI/Analysis/CircleDomains/Sobolev/ScalarModelExactEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The globally continued scalar has exactly its original source Dirichlet energy. Apply conformal energy transport to the global target scalar in the reverse direction and identify the source weak gradient.

  1. theorem OAI.CircleDomainRigidity.CompactScalarCircleModel.scalar_energy_eq line 18