OAI/Analysis/CircleDomains/Transfer/RoundOuterCore.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The fixed round outer zero contour is an actual smooth source core.

  1. def OAI.CircleDomainRigidity.roundOuterJordan line 17
  2. theorem OAI.CircleDomainRigidity.roundOuterJordan_interior line 20
  3. abbrev OAI.CircleDomainRigidity.roundOuterCore line 25
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.outer_region_subset_source line 57
  5. abbrev OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.outerCore line 62
  6. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.outerCore_interior line 65
  7. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealModelExhaustion.component_inside_outerCore line 68