OAI/Analysis/CircleDomains/Sobolev/BarrierL2Error.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The manuscript's three-term barrier estimate, including the energy on the altered horizontal support.

  1. theorem OAI.CircleDomainRigidity.barrier_L2_error line 13