OAI/Analysis/CircleDomains/Rigidity/MatchedRealMaskSobolev.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Apply the proved open-set Sobolev gluing to the constructed masks. The only scalar hypotheses concern the actual smooth pullback on the original domain.

  1. def OAI.CircleDomainRigidity.MatchedConformalEnds.realPlaneDomain line 18
  2. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.realPlaneDomain_open line 21
  3. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.physical_maskDomain line 25
  4. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.MatchedRealMask.sobolev line 41