OAI/Analysis/CircleDomains/Sobolev/ModelPairBarrierEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual compact target barrier has exactly the saved local source energy. Its gradient on the model holes and on the exterior both vanish.

  1. theorem OAI.CircleDomainRigidity.CompactScalarModel.pairBarrier_energy line 19