OAI/Analysis/CircleDomains/Rigidity/LocalTraceMaskSobolev.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The local mask witness uses only smoothness of the raw scalar on the actual source open set; a compact cutoff constructs the auxiliary global extension and its differential agrees on the requested rectangle.

  1. theorem OAI.CircleDomainRigidity.local_masked_scalar_rectangle_sobolev line 14