OAI/Analysis/CircleDomains/Topology/SphericalGridPreparation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Grid preparation while retaining a neighborhood of infinity

The physical domain has compact complement in the finite chart. The retained core is an actual regular sublevel, contains every prescribed closed part of the domain, and has compact complement. Its compactly supported cutoff leaves the coordinates unchanged near infinity.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_regular_core_cutoff_and_grid line 22