OAI/Analysis/CircleDomains/Sobolev/LocalSobolevGluing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local Sobolev witnesses with one integrable gradient majorant give an actual witness on the whole open set, with a finite total energy.

  1. theorem OAI.CircleDomainRigidity.exists_local_sobolev_gluing line 13