OAI/Analysis/CircleDomains/Rigidity/TraceMaskPlateauSobolev.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

On a zero-cutoff neighborhood the primitive has a fixed endpoint. Consequently its local Sobolev regularity does not require regularity of the raw scalar, including point-to-disk component matches.

  1. theorem OAI.CircleDomainRigidity.fixed_endpoint_mask_rectangle_sobolev line 14
  2. theorem OAI.CircleDomainRigidity.plateau_mask_rectangle_sobolev line 34