OAI/Analysis/CircleDomains/Transfer/CompletedChart.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The actual completed region in the finite real chart

These identifications pass the spherical disk completion to the real coordinates used by the energy estimates, preserving the original core and the exact open extension domain.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.isClosed_realChartDomain line 21
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.realChartDomain_union line 25
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.realChartDomain_sphericalCore line 28
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.realChartDomain_sphericalDiskUnion line 34
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.isClosed_real_completedRegion line 48
  6. theorem OAI.CircleDomainRigidity.FiniteTransfer.real_completedRegion_subset_extension line 52
  7. theorem OAI.CircleDomainRigidity.FiniteTransfer.real_core_avoids_filling line 62
  8. theorem OAI.CircleDomainRigidity.FiniteTransfer.real_boundary_in_domain_and_plateau line 72