OAI/Analysis/CircleDomains/Topology/SphericalCollarSplicing.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Spherical-energy forms of the two collar constructions. The outer neighborhoods and local energy bounds are derived, and all new interior dust contacts belong to one of the original paths.

  1. theorem OAI.CircleDomainRigidity.exists_sphere_open_closure_inside line 23
  2. theorem OAI.CircleDomainRigidity.exists_spherical_twoEnded_collar line 29
  3. theorem OAI.CircleDomainRigidity.exists_spherical_oneEnded_collar line 92