OAI/Analysis/CircleDomains/Rigidity/TraceMaskOpenSobolev.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The local smooth and plateau witnesses join on the actual open union. The source differential is charged only on the original domain, and balloon derivatives are charged to the constructed global L² density.

  1. theorem OAI.CircleDomainRigidity.trace_mask_open_sobolev line 17