OAI/Analysis/CircleDomains/Sobolev/PotentialSobolevWitness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual barrier belongs to the Euclidean Sobolev space used by our smooth approximation library.

  1. theorem OAI.CircleDomainRigidity.potential_rectangle_memW1p line 22